2
(include-book "../Supporting-Books/seq")
3
(include-book "../Supporting-Books/meta")
4
(include-book "../Supporting-Books/det-macros")
5
(include-book "../Supporting-Books/records")
8
:set-irrelevant-formals-ok t
11
(defun equalb (a b) (equal a b))
13
(defun nequal (a b) (not (equal a b))) (defun add-1 (a) (+ a 1))
15
(defun sub-1 (a) (- a 1))
17
(encapsulate ((intrp_mod_dmem (x1) t))
18
(local (defun intrp_mod_dmem (x1) (declare (ignore x1)) 1))
19
(defthm intrp_mod_dmem-type (integerp (intrp_mod_dmem x1))))
21
(encapsulate ((nextdmem (x3 x2 x1) t))
22
(local (defun nextdmem (x3 x2 x1)
23
(declare (ignore x3) (ignore x2) (ignore x1))
25
(defthm nextdmem-type (integerp (nextdmem x3 x2 x1))))
27
(encapsulate ((dmem_read (x2 x1) t))
28
(local (defun dmem_read (x2 x1)
29
(declare (ignore x2) (ignore x1))
31
(defthm dmem_read-type (integerp (dmem_read x2 x1))))
33
(encapsulate ((nextintrp (x1) t))
34
(local (defun nextintrp (x1) (declare (ignore x1)) 1))
35
(defthm nextintrp-type (integerp (nextintrp x1))))
37
(encapsulate ((isinterrupt (x1) t))
38
(local (defun isinterrupt (x1) (declare (ignore x1)) nil))
39
(defthm isinterrupt-type (booleanp (isinterrupt x1))))
41
(encapsulate ((rf0 (x1) t))
42
(local (defun rf0 (x1) (declare (ignore x1)) 1))
43
(defthm rf0-type (integerp (rf0 x1))))
45
(encapsulate ((imem0 (x1) t))
46
(local (defun imem0 (x1) (declare (ignore x1)) 1))
47
(defthm imem0-type (integerp (imem0 x1))))
49
(encapsulate ((src1 (x1) t))
50
(local (defun src1 (x1) (declare (ignore x1)) 1))
51
(defthm src1-type (integerp (src1 x1))))
53
(encapsulate ((src2 (x1) t))
54
(local (defun src2 (x1) (declare (ignore x1)) 1))
55
(defthm src2-type (integerp (src2 x1))))
57
(encapsulate ((opcode (x1) t))
58
(local (defun opcode (x1) (declare (ignore x1)) 1))
59
(defthm op-type (integerp (opcode x1))))
61
(encapsulate ((dest (x1) t))
62
(local (defun dest (x1) (declare (ignore x1)) 1))
63
(defthm dest-type (integerp (dest x1))))
65
(encapsulate ((alu (x3 x2 x1) t))
66
(local (defun alu (x3 x2 x1)
67
(declare (ignore x3) (ignore x2) (ignore x1))
69
(defthm alu-type (integerp (alu x3 x2 x1))))
71
(encapsulate ((getregwrite (x1) t))
72
(local (defun getregwrite (x1) (declare (ignore x1)) nil))
73
(defthm getregwrite-type (booleanp (getregwrite x1))))
75
(encapsulate ((getmemtoreg (x1) t))
76
(local (defun getmemtoreg (x1) (declare (ignore x1)) nil))
77
(defthm getmemtoreg-type (booleanp (getmemtoreg x1))))
79
(encapsulate ((getuseimm (x1) t))
80
(local (defun getuseimm (x1) (declare (ignore x1)) nil))
81
(defthm getuseimm-type (booleanp (getuseimm x1))))
83
(encapsulate ((getimm (x1) t))
84
(local (defun getimm (x1) (declare (ignore x1)) 1))
85
(defthm getimm-type (integerp (getimm x1))))
87
(encapsulate ((getmemwrite (x1) t))
88
(local (defun getmemwrite (x1) (declare (ignore x1)) nil))
89
(defthm getmemwrite-type (booleanp (getmemwrite x1))))
91
(encapsulate ((getisbranch (x1) t))
92
(local (defun getisbranch (x1) (declare (ignore x1)) nil))
93
(defthm getisbranch-type (booleanp (getisbranch x1))))
95
(encapsulate ((takebranch (x3 x2 x1) t))
96
(local (defun takebranch (x3 x2 x1)
97
(declare (ignore x3) (ignore x2) (ignore x1))
99
(defthm takebranch-type (booleanp (takebranch x3 x2 x1))))
101
(encapsulate ((selecttargetpc (x3 x2 x1) t))
102
(local (defun selecttargetpc (x3 x2 x1)
103
(declare (ignore x3) (ignore x2) (ignore x1))
105
(defthm selecttargetpc-type (integerp (selecttargetpc x3 x2 x1))))
107
(encapsulate ((alu_exception (x3 x2 x1) t))
108
(local (defun alu_exception (x3 x2 x1)
109
(declare (ignore x3) (ignore x2) (ignore x1))
111
(defthm alu_exception-type (booleanp (alu_exception x3 x2 x1))))
113
(encapsulate ((getreturnfromexception (x1) t))
114
(local (defun getreturnfromexception (x1)
115
(declare (ignore x1))
117
(defthm getreturnfromexception-type
118
(booleanp (getreturnfromexception x1))))
120
(encapsulate ((nextbpstate (x1) t))
121
(local (defun nextbpstate (x1) (declare (ignore x1)) 1))
122
(defthm nextbpstate-type (integerp (nextbpstate x1))))
124
(encapsulate ((predictdirection (x1) t))
125
(local (defun predictdirection (x1) (declare (ignore x1)) nil))
126
(defthm predictdirection-type (booleanp (predictdirection x1))))
128
(encapsulate ((predicttarget (x1) t))
129
(local (defun predicttarget (x1) (declare (ignore x1)) 1))
130
(defthm predicttarget-type (integerp (predicttarget x1))))
132
(defun read-pimem_a (a pimem)
133
(declare (xargs :measure (acl2-count pimem)))
134
(if (endp pimem) (imem0 a)
135
(if (g 0 (car pimem)) (imem0 a) (read-pimem_a a (cdr pimem)))))
137
(defun read-prf_a (a prf)
138
(declare (xargs :measure (acl2-count prf)))
139
(if (endp prf) (rf0 a)
140
(if (g 0 (car prf)) (rf0 a)
142
((g 1 (car prf)) (rf0 a))
143
((g 2 (car prf)) (read-prf_a a (cdr prf)))
144
((and (and (and (and (and (g 3 (car prf))
145
(equal a (g 4 (car prf))))
151
(t (read-prf_a a (cdr prf)))))))
153
(defun read-simem_a (a simem)
154
(declare (xargs :measure (acl2-count simem)))
155
(if (endp simem) (imem0 a)
156
(if (g 0 (car simem)) (imem0 a) (read-simem_a a (cdr simem)))))
158
(defun read-srf_a (a srf)
159
(declare (xargs :measure (acl2-count srf)))
160
(if (endp srf) (rf0 a)
161
(if (g 0 (car srf)) (rf0 a)
163
((g 1 (car srf)) (rf0 a))
164
((g 2 (car srf)) (read-prf_a a (g 3 (car srf))))
165
((and (and (and (and (and (g 4 (car srf))
166
(equal a (dest (g 5 (car srf)))))
172
(t (read-srf_a a (cdr srf)))))))
174
(defun u-state_a (impl spec) (seq nil 'impl impl 'spec spec))
177
(pimem ppc pintrp bpstate ffbpstate ffpintrp
178
ffpredicteddirection ffpredictedtarget ffwrt ffinst
179
ffppc prf fdpintrp fdbpstate fdppc fdwrt fdinst
180
fdpredicteddirection fdpredictedtarget debpstate
181
depintrp deppc desrc1 desrc2 dearg1 dearg2 dedest deop
182
deimm deuseimm deisreturnfromexception deregwrite
183
dememwrite dememtoreg deisbranch dewrt
184
depredicteddirection depredictedtarget embpstate
185
empintrp emppc emis_alu_exception emis_taken_branch
186
emtargetpc emarg2 emresult emdest emwrt
187
emisreturnfromexception emmispredictedtaken
188
emmispredictednottaken emregwrite emmemwrite emmemtoreg
189
pdmemhist_2 pdmemhist_1 pdmem pepchist_2 pepchist_1 pepc
190
pisexceptionhist_2 pisexceptionhist_1 pisexception
191
mmbpstate mmpintrp mmisreturnfromexception
192
mmis_alu_exception mmppc mmval mmdest mmwrt mmregwrite
193
mwbpstate mwpintrp mwisreturnfromexception
194
mwis_alu_exception mwppc mwval mwdest mwwrt mwregwrite)
195
(seq nil 'pimem pimem 'ppc ppc 'pintrp pintrp 'bpstate bpstate
196
'ffbpstate ffbpstate 'ffpintrp ffpintrp 'ffpredicteddirection
197
ffpredicteddirection 'ffpredictedtarget ffpredictedtarget
198
'ffwrt ffwrt 'ffinst ffinst 'ffppc ffppc 'prf prf 'fdpintrp
199
fdpintrp 'fdbpstate fdbpstate 'fdppc fdppc 'fdwrt fdwrt 'fdinst
200
fdinst 'fdpredicteddirection fdpredicteddirection
201
'fdpredictedtarget fdpredictedtarget 'debpstate debpstate
202
'depintrp depintrp 'deppc deppc 'desrc1 desrc1 'desrc2 desrc2
203
'dearg1 dearg1 'dearg2 dearg2 'dedest dedest 'deop deop 'deimm
204
deimm 'deuseimm deuseimm 'deisreturnfromexception
205
deisreturnfromexception 'deregwrite deregwrite 'dememwrite
206
dememwrite 'dememtoreg dememtoreg 'deisbranch deisbranch 'dewrt
207
dewrt 'depredicteddirection depredicteddirection
208
'depredictedtarget depredictedtarget 'embpstate embpstate
209
'empintrp empintrp 'emppc emppc 'emis_alu_exception
210
emis_alu_exception 'emis_taken_branch emis_taken_branch
211
'emtargetpc emtargetpc 'emarg2 emarg2 'emresult emresult
212
'emdest emdest 'emwrt emwrt 'emisreturnfromexception
213
emisreturnfromexception 'emmispredictedtaken
214
emmispredictedtaken 'emmispredictednottaken
215
emmispredictednottaken 'emregwrite emregwrite 'emmemwrite
216
emmemwrite 'emmemtoreg emmemtoreg 'pdmemhist_2 pdmemhist_2
217
'pdmemhist_1 pdmemhist_1 'pdmem pdmem 'pepchist_2 pepchist_2
218
'pepchist_1 pepchist_1 'pepc pepc 'pisexceptionhist_2
219
pisexceptionhist_2 'pisexceptionhist_1 pisexceptionhist_1
220
'pisexception pisexception 'mmbpstate mmbpstate 'mmpintrp
221
mmpintrp 'mmisreturnfromexception mmisreturnfromexception
222
'mmis_alu_exception mmis_alu_exception 'mmppc mmppc 'mmval
223
mmval 'mmdest mmdest 'mmwrt mmwrt 'mmregwrite mmregwrite
224
'mwbpstate mwbpstate 'mwpintrp mwpintrp
225
'mwisreturnfromexception mwisreturnfromexception
226
'mwis_alu_exception mwis_alu_exception 'mwppc mwppc 'mwval
227
mwval 'mwdest mwdest 'mwwrt mwwrt 'mwregwrite mwregwrite))
229
(defun initpimem_a (pimem) (cons (s 0 t (s 1 nil nil)) pimem))
231
(defun nextpimem_a (pimem) (cons (s 0 nil (s 1 nil nil)) pimem))
233
(defun initppc_a (pc0) pc0)
236
(initi pc0 commit_impl commit_pc mem1_is_interrupt emppc
237
mem1_is_returnfromexception pepc mem1_is_alu_exception
238
alu_exception_handler mem1_mispredicted_taken
239
mem1_mispredicted_nottaken emtargetpc stall ppc
240
if_predict_branch_taken predicted_target)
243
(commit_impl commit_pc)
244
(mem1_is_interrupt emppc)
245
(mem1_is_returnfromexception pepc)
246
(mem1_is_alu_exception alu_exception_handler)
247
(mem1_mispredicted_taken (add-1 emppc))
248
(mem1_mispredicted_nottaken emtargetpc)
250
(if_predict_branch_taken predicted_target)
253
(defun initpintrp_a (intrp0) intrp0)
256
(initi intrp0 commit_impl commit_intrp stall pintrp)
259
(commit_impl commit_intrp)
261
(t (nextintrp pintrp))))
263
(defun initbpstate_a (bpstate0) bpstate0)
266
(initi bpstate0 commit_impl commit_bpstate stall bpstate)
269
(commit_impl commit_bpstate)
271
(t (nextbpstate bpstate))))
273
(defun initffbpstate_a (ffbpstate0) ffbpstate0)
275
(defun nextffbpstate_a (initi ffbpstate0 stall ffbpstate bpstate)
276
(cond (initi ffbpstate0) (stall ffbpstate) (t bpstate)))
278
(defun initffpintrp_a (ffpintrp0) ffpintrp0)
280
(defun nextffpintrp_a (initi ffpintrp0 stall ffpintrp pintrp)
281
(cond (initi ffpintrp0) (stall ffpintrp) (t pintrp)))
283
(defun initffpredicteddirection_a (ffpredicteddirection0)
284
ffpredicteddirection0)
286
(defun nextffpredicteddirection_a
287
(initi ffpredicteddirection0 stall ffpredicteddirection
288
if_predict_branch_taken)
290
(initi ffpredicteddirection0)
291
(stall ffpredicteddirection)
292
(t if_predict_branch_taken)))
294
(defun initffpredictedtarget_a (ffpredictedtarget0)
297
(defun nextffpredictedtarget_a
298
(initi ffpredictedtarget0 stall ffpredictedtarget
301
(initi ffpredictedtarget0)
302
(stall ffpredictedtarget)
303
(t predicted_target)))
305
(defun initffwrt_a () nil)
307
(defun nextffwrt_a (initi commit_impl squash stall ffwrt)
315
(defun initffinst_a (ffinst0) ffinst0)
317
(defun nextffinst_a (initi ffinst0 stall ffinst if_inst)
318
(cond (initi ffinst0) (stall ffinst) (t if_inst)))
320
(defun initffppc_a (ffppc0) ffppc0)
322
(defun nextffppc_a (initi ffppc0 stall ffppc ppc)
323
(cond (initi ffppc0) (stall ffppc) (t ppc)))
325
(defun initprf_a (prf) (cons (s 0 t (s 1 nil nil)) prf))
328
(prf initi commit_impl mwwrt mwdest mwregwrite
329
wb_is_alu_exception_bar wb_is_interrupt_bar
330
wb_is_returnfromexception_bar mwval)
337
(s 6 wb_is_alu_exception_bar
338
(s 7 wb_is_interrupt_bar
339
(s 8 wb_is_returnfromexception_bar
340
(s 9 mwval nil))))))))))
343
(defun initfdpintrp_a (fdpintrp0) fdpintrp0)
345
(defun nextfdpintrp_a (initi fdpintrp0 stall fdpintrp ffpintrp)
346
(cond (initi fdpintrp0) (stall fdpintrp) (t ffpintrp)))
348
(defun initfdbpstate_a (fdbpstate0) fdbpstate0)
350
(defun nextfdbpstate_a (initi fdbpstate0 stall fdbpstate ffbpstate)
351
(cond (initi fdbpstate0) (stall fdbpstate) (t ffbpstate)))
353
(defun initfdppc_a (fdppc0) fdppc0)
355
(defun nextfdppc_a (initi fdppc0 stall fdppc ffppc)
356
(cond (initi fdppc0) (stall fdppc) (t ffppc)))
358
(defun initfdwrt_a () nil)
360
(defun nextfdwrt_a (initi commit_impl squash stall fdwrt ffwrt)
368
(defun initfdinst_a (fdinst0) fdinst0)
370
(defun nextfdinst_a (initi fdinst0 stall fdinst ffinst)
371
(cond (initi fdinst0) (stall fdinst) (t ffinst)))
373
(defun initfdpredicteddirection_a (fdpredicteddirection0)
374
fdpredicteddirection0)
376
(defun nextfdpredicteddirection_a
377
(initi fdpredicteddirection0 stall fdpredicteddirection
378
ffpredicteddirection)
380
(initi fdpredicteddirection0)
381
(stall fdpredicteddirection)
382
(t ffpredicteddirection)))
384
(defun initfdpredictedtarget_a (fdpredictedtarget0)
387
(defun nextfdpredictedtarget_a
388
(initi fdpredictedtarget0 stall fdpredictedtarget
391
(initi fdpredictedtarget0)
392
(stall fdpredictedtarget)
393
(t ffpredictedtarget)))
395
(defun initdebpstate_a (debpstate0) debpstate0)
397
(defun nextdebpstate_a (initi debpstate0 fdbpstate)
398
(cond (initi debpstate0) (t fdbpstate)))
400
(defun initdepintrp_a (depintrp0) depintrp0)
402
(defun nextdepintrp_a (initi depintrp0 fdpintrp)
403
(cond (initi depintrp0) (t fdpintrp)))
405
(defun initdeppc_a (deppc0) deppc0)
407
(defun nextdeppc_a (initi deppc0 fdppc)
408
(cond (initi deppc0) (t fdppc)))
410
(defun initdesrc1_a (desrc10) desrc10)
412
(defun nextdesrc1_a (initi desrc10 if_id_src1)
413
(cond (initi desrc10) (t if_id_src1)))
415
(defun initdesrc2_a (desrc20) desrc20)
417
(defun nextdesrc2_a (initi desrc20 if_id_src2)
418
(cond (initi desrc20) (t if_id_src2)))
420
(defun initdearg1_a (a1) a1)
423
(initi a1 if_id_src1 prf commit_impl mwwrt mwdest mwregwrite
424
wb_is_alu_exception_bar wb_is_interrupt_bar
425
wb_is_returnfromexception_bar mwval)
428
(t (read-prf_a if_id_src1
429
(nextprf_a prf initi commit_impl mwwrt mwdest mwregwrite
430
wb_is_alu_exception_bar wb_is_interrupt_bar
431
wb_is_returnfromexception_bar mwval)))))
433
(defun initdearg2_a (a2) a2)
436
(initi a2 if_id_src2 prf commit_impl mwwrt mwdest mwregwrite
437
wb_is_alu_exception_bar wb_is_interrupt_bar
438
wb_is_returnfromexception_bar mwval)
441
(t (read-prf_a if_id_src2
442
(nextprf_a prf initi commit_impl mwwrt mwdest mwregwrite
443
wb_is_alu_exception_bar wb_is_interrupt_bar
444
wb_is_returnfromexception_bar mwval)))))
446
(defun initdedest_a (dedest0) dedest0)
448
(defun nextdedest_a (initi dedest0 fdinst)
449
(cond (initi dedest0) (t (dest fdinst))))
451
(defun initdeop_a (deop0) deop0)
453
(defun nextdeop_a (initi deop0 fdinst)
454
(cond (initi deop0) (t (opcode fdinst))))
456
(defun initdeimm_a (deimm0) deimm0)
458
(defun nextdeimm_a (initi deimm0 fdinst)
459
(cond (initi deimm0) (t (getimm fdinst))))
461
(defun initdeuseimm_a (deuseimm0) deuseimm0)
463
(defun nextdeuseimm_a (initi deuseimm0 fdinst)
464
(cond (initi deuseimm0) (t (getuseimm fdinst))))
466
(defun initdeisreturnfromexception_a (deisreturnfromexception0)
467
deisreturnfromexception0)
469
(defun nextdeisreturnfromexception_a
470
(initi deisreturnfromexception0 fdinst)
472
(initi deisreturnfromexception0)
473
(t (getreturnfromexception fdinst))))
475
(defun initderegwrite_a (deregwrite0) deregwrite0)
477
(defun nextderegwrite_a (initi deregwrite0 id_regwrite)
478
(cond (initi deregwrite0) (t id_regwrite)))
480
(defun initdememwrite_a (dememwrite0) dememwrite0)
482
(defun nextdememwrite_a (initi dememwrite0 id_memwrite)
483
(cond (initi dememwrite0) (t id_memwrite)))
485
(defun initdememtoreg_a (dememtoreg0) dememtoreg0)
487
(defun nextdememtoreg_a (initi dememtoreg0 fdinst)
488
(cond (initi dememtoreg0) (t (getmemtoreg fdinst))))
490
(defun initdeisbranch_a (deisbranch0) deisbranch0)
492
(defun nextdeisbranch_a (initi deisbranch0 fdinst)
493
(cond (initi deisbranch0) (t (getisbranch fdinst))))
495
(defun initdewrt_a () nil)
497
(defun nextdewrt_a (initi commit_impl squash stall fdwrt)
502
(t (and (not stall) fdwrt))))
504
(defun initdepredicteddirection_a (depredicteddirection0)
505
depredicteddirection0)
507
(defun nextdepredicteddirection_a
508
(initi depredicteddirection0 stall depredicteddirection
509
fdpredicteddirection)
511
(initi depredicteddirection0)
512
(stall depredicteddirection)
513
(t fdpredicteddirection)))
515
(defun initdepredictedtarget_a (depredictedtarget0)
518
(defun nextdepredictedtarget_a
519
(initi depredictedtarget0 stall depredictedtarget
522
(initi depredictedtarget0)
523
(stall depredictedtarget)
524
(t fdpredictedtarget)))
526
(defun initembpstate_a (embpstate0) embpstate0)
528
(defun nextembpstate_a (initi embpstate0 debpstate)
529
(cond (initi embpstate0) (t debpstate)))
531
(defun initempintrp_a (empintrp0) empintrp0)
533
(defun nextempintrp_a (initi empintrp0 depintrp)
534
(cond (initi empintrp0) (t depintrp)))
536
(defun initemppc_a (emppc0) emppc0)
538
(defun nextemppc_a (initi emppc0 deppc)
539
(cond (initi emppc0) (t deppc)))
541
(defun initemis_alu_exception_a (emis_alu_exception0)
544
(defun nextemis_alu_exception_a
545
(initi emis_alu_exception0 ex_is_alu_exception)
546
(cond (initi emis_alu_exception0) (t ex_is_alu_exception)))
548
(defun initemis_taken_branch_a (emis_taken_branch0)
551
(defun nextemis_taken_branch_a
552
(initi emis_taken_branch0 ex_is_taken_branch)
553
(cond (initi emis_taken_branch0) (t ex_is_taken_branch)))
555
(defun initemtargetpc_a (emtargetpc0) emtargetpc0)
557
(defun nextemtargetpc_a (initi emtargetpc0 ex_targetpc)
558
(cond (initi emtargetpc0) (t ex_targetpc)))
560
(defun initemarg2_a (emarg20) emarg20)
562
(defun nextemarg2_a (initi emarg20 ex_fwd_src2)
563
(cond (initi emarg20) (t ex_fwd_src2)))
565
(defun initemresult_a (emresult0) emresult0)
567
(defun nextemresult_a (initi emresult0 ex_result)
568
(cond (initi emresult0) (t ex_result)))
570
(defun initemdest_a (emdest0) emdest0)
572
(defun nextemdest_a (initi emdest0 dedest)
573
(cond (initi emdest0) (t dedest)))
575
(defun initemwrt_a () nil)
577
(defun nextemwrt_a (initi commit_impl squash dewrt)
578
(cond (initi nil) (commit_impl nil) (squash nil) (t dewrt)))
580
(defun initemisreturnfromexception_a (emisreturnfromexception0)
581
emisreturnfromexception0)
583
(defun nextemisreturnfromexception_a
584
(initi emisreturnfromexception0 deisreturnfromexception)
585
(cond (initi emisreturnfromexception0) (t deisreturnfromexception)))
587
(defun initemmispredictedtaken_a (emmispredictedtaken0)
588
emmispredictedtaken0)
590
(defun nextemmispredictedtaken_a
591
(initi emmispredictedtaken0 mispredicted_taken)
592
(cond (initi emmispredictedtaken0) (t mispredicted_taken)))
594
(defun initemmispredictednottaken_a (emmispredictednottaken0)
595
emmispredictednottaken0)
597
(defun nextemmispredictednottaken_a
598
(initi emmispredictednottaken0 mispredicted_nottaken)
599
(cond (initi emmispredictednottaken0) (t mispredicted_nottaken)))
601
(defun initemregwrite_a (emregwrite0) emregwrite0)
603
(defun nextemregwrite_a (initi emregwrite0 deregwrite)
604
(cond (initi emregwrite0) (t deregwrite)))
606
(defun initemmemwrite_a (emmemwrite0) emmemwrite0)
608
(defun nextemmemwrite_a (initi emmemwrite0 dememwrite)
609
(cond (initi emmemwrite0) (t dememwrite)))
611
(defun initemmemtoreg_a (emmemtoreg0) emmemtoreg0)
613
(defun nextemmemtoreg_a (initi emmemtoreg0 dememtoreg)
614
(cond (initi emmemtoreg0) (t dememtoreg)))
616
(defun initpdmemhist_2_a (dmem0) dmem0)
618
(defun nextpdmemhist_2_a (initi dmem0 pdmemhist_1)
619
(cond (initi dmem0) (t pdmemhist_1)))
621
(defun initpdmemhist_1_a (dmem0) dmem0)
623
(defun nextpdmemhist_1_a (initi dmem0 pdmem)
624
(cond (initi dmem0) (t pdmem)))
626
(defun initpdmem_a (dmem0) dmem0)
629
(initi dmem0 commit_impl pdmemhist_2 mem1_is_interrupt pdmem
630
emwrt emmemwrite mem1_is_alu_exception_bar
631
mem1_is_returnfromexception_bar emresult emarg2)
634
(commit_impl pdmemhist_2)
635
(mem1_is_interrupt (intrp_mod_dmem pdmem))
636
((and (and (and emwrt emmemwrite) mem1_is_alu_exception_bar)
637
mem1_is_returnfromexception_bar)
638
(nextdmem pdmem emresult emarg2))
641
(defun initpepchist_2_a (epc0) epc0)
643
(defun nextpepchist_2_a (initi epc0 pepchist_1)
644
(cond (initi epc0) (t pepchist_1)))
646
(defun initpepchist_1_a (epc0) epc0)
648
(defun nextpepchist_1_a (initi epc0 pepc)
649
(cond (initi epc0) (t pepc)))
651
(defun initpepc_a (epc0) epc0)
654
(initi epc0 commit_impl pepchist_2 mem1_is_alu_exception
655
mem1_is_returnfromexception_bar mem1_is_interrupt_bar
659
(commit_impl pepchist_2)
660
((and (and mem1_is_alu_exception mem1_is_returnfromexception_bar)
661
mem1_is_interrupt_bar)
665
(defun initpisexceptionhist_2_a (isexception0) isexception0)
667
(defun nextpisexceptionhist_2_a
668
(initi isexception0 pisexceptionhist_1)
669
(cond (initi isexception0) (t pisexceptionhist_1)))
671
(defun initpisexceptionhist_1_a (isexception0) isexception0)
673
(defun nextpisexceptionhist_1_a (initi isexception0 pisexception)
674
(cond (initi isexception0) (t pisexception)))
676
(defun initpisexception_a (isexception0) isexception0)
678
(defun nextpisexception_a
679
(initi isexception0 commit_impl pisexceptionhist_2
680
mem1_is_alu_exception mem1_is_returnfromexception
681
mem1_is_interrupt_bar mem1_is_returnfromexception_bar
685
(commit_impl pisexceptionhist_2)
686
((and (or mem1_is_alu_exception mem1_is_returnfromexception)
687
mem1_is_interrupt_bar)
688
(and mem1_is_alu_exception mem1_is_returnfromexception_bar))
691
(defun initmmbpstate_a (mmbpstate0) mmbpstate0)
693
(defun nextmmbpstate_a (initi mmbpstate0 embpstate)
694
(cond (initi mmbpstate0) (t embpstate)))
696
(defun initmmpintrp_a (mmpintrp0) mmpintrp0)
698
(defun nextmmpintrp_a (initi mmpintrp0 empintrp)
699
(cond (initi mmpintrp0) (t empintrp)))
701
(defun initmmisreturnfromexception_a (mmisreturnfromexception0)
702
mmisreturnfromexception0)
704
(defun nextmmisreturnfromexception_a
705
(initi mmisreturnfromexception0 emisreturnfromexception)
706
(cond (initi mmisreturnfromexception0) (t emisreturnfromexception)))
708
(defun initmmis_alu_exception_a (mmis_alu_exception0)
711
(defun nextmmis_alu_exception_a
712
(initi mmis_alu_exception0 emis_alu_exception)
713
(cond (initi mmis_alu_exception0) (t emis_alu_exception)))
715
(defun initmmppc_a (mmppc0) mmppc0)
717
(defun nextmmppc_a (initi mmppc0 emppc)
718
(cond (initi mmppc0) (t emppc)))
720
(defun initmmval_a (mmval0) mmval0)
722
(defun nextmmval_a (initi mmval0 emmemtoreg mem1_readdata emresult)
723
(cond (initi mmval0) (emmemtoreg mem1_readdata) (t emresult)))
725
(defun initmmdest_a (mmdest0) mmdest0)
727
(defun nextmmdest_a (initi mmdest0 emdest)
728
(cond (initi mmdest0) (t emdest)))
730
(defun initmmwrt_a () nil)
732
(defun nextmmwrt_a (initi commit_impl emwrt)
733
(cond (initi nil) (commit_impl nil) (t emwrt)))
735
(defun initmmregwrite_a (mmregwrite0) mmregwrite0)
737
(defun nextmmregwrite_a (initi mmregwrite0 emregwrite)
738
(cond (initi mmregwrite0) (t emregwrite)))
740
(defun initmwbpstate_a (mwbpstate0) mwbpstate0)
742
(defun nextmwbpstate_a (initi mwbpstate0 mmbpstate)
743
(cond (initi mwbpstate0) (t mmbpstate)))
745
(defun initmwpintrp_a (mwpintrp0) mwpintrp0)
747
(defun nextmwpintrp_a (initi mwpintrp0 mmpintrp)
748
(cond (initi mwpintrp0) (t mmpintrp)))
750
(defun initmwisreturnfromexception_a (mwisreturnfromexception0)
751
mwisreturnfromexception0)
753
(defun nextmwisreturnfromexception_a
754
(initi mwisreturnfromexception0 mmisreturnfromexception)
755
(cond (initi mwisreturnfromexception0) (t mmisreturnfromexception)))
757
(defun initmwis_alu_exception_a (mwis_alu_exception0)
760
(defun nextmwis_alu_exception_a
761
(initi mwis_alu_exception0 mmis_alu_exception)
762
(cond (initi mwis_alu_exception0) (t mmis_alu_exception)))
764
(defun initmwppc_a (mwppc0) mwppc0)
766
(defun nextmwppc_a (initi mwppc0 mmppc)
767
(cond (initi mwppc0) (t mmppc)))
769
(defun initmwval_a (mwval0) mwval0)
771
(defun nextmwval_a (initi mwval0 mmval)
772
(cond (initi mwval0) (t mmval)))
774
(defun initmwdest_a (mwdest0) mwdest0)
776
(defun nextmwdest_a (initi mwdest0 mmdest)
777
(cond (initi mwdest0) (t mmdest)))
779
(defun initmwwrt_a () nil)
781
(defun nextmwwrt_a (initi commit_impl mmwrt)
782
(cond (initi nil) (commit_impl nil) (t mmwrt)))
784
(defun initmwregwrite_a (mwregwrite0) mwregwrite0)
786
(defun nextmwregwrite_a (initi mwregwrite0 mmregwrite)
787
(cond (initi mwregwrite0) (t mmregwrite)))
789
(defun impl-simulate_a
790
(impl initi pc0 commit_impl commit_pc alu_exception_handler
791
intrp0 commit_intrp bpstate0 commit_bpstate ffbpstate0
792
ffpintrp0 ffpredicteddirection0 ffpredictedtarget0
793
ffinst0 ffppc0 fdpintrp0 fdbpstate0 fdppc0 fdinst0
794
fdpredicteddirection0 fdpredictedtarget0 debpstate0
795
depintrp0 deppc0 desrc10 desrc20 a1 a2 dedest0 deop0
796
deimm0 deuseimm0 deisreturnfromexception0 deregwrite0
797
dememwrite0 dememtoreg0 deisbranch0 depredicteddirection0
798
depredictedtarget0 embpstate0 empintrp0 emppc0
799
emis_alu_exception0 emis_taken_branch0 emtargetpc0
800
emarg20 emresult0 emdest0 emisreturnfromexception0
801
emmispredictedtaken0 emmispredictednottaken0 emregwrite0
802
emmemwrite0 emmemtoreg0 dmem0 epc0 isexception0
803
mmbpstate0 mmpintrp0 mmisreturnfromexception0
804
mmis_alu_exception0 mmppc0 mmval0 mmdest0 mmregwrite0
805
mwbpstate0 mwpintrp0 mwisreturnfromexception0
806
mwis_alu_exception0 mwppc0 mwval0 mwdest0 mwregwrite0)
807
(let* ((pimem (g 'pimem impl)) (ppc (g 'ppc impl))
808
(pintrp (g 'pintrp impl)) (bpstate (g 'bpstate impl))
809
(ffbpstate (g 'ffbpstate impl)) (ffpintrp (g 'ffpintrp impl))
810
(ffpredicteddirection (g 'ffpredicteddirection impl))
811
(ffpredictedtarget (g 'ffpredictedtarget impl))
812
(ffwrt (g 'ffwrt impl)) (ffinst (g 'ffinst impl))
813
(ffppc (g 'ffppc impl)) (prf (g 'prf impl))
814
(fdpintrp (g 'fdpintrp impl)) (fdbpstate (g 'fdbpstate impl))
815
(fdppc (g 'fdppc impl)) (fdwrt (g 'fdwrt impl))
816
(fdinst (g 'fdinst impl))
817
(fdpredicteddirection (g 'fdpredicteddirection impl))
818
(fdpredictedtarget (g 'fdpredictedtarget impl))
819
(debpstate (g 'debpstate impl)) (depintrp (g 'depintrp impl))
820
(deppc (g 'deppc impl)) (desrc1 (g 'desrc1 impl))
821
(desrc2 (g 'desrc2 impl)) (dearg1 (g 'dearg1 impl))
822
(dearg2 (g 'dearg2 impl)) (dedest (g 'dedest impl))
823
(deop (g 'deop impl)) (deimm (g 'deimm impl))
824
(deuseimm (g 'deuseimm impl))
825
(deisreturnfromexception (g 'deisreturnfromexception impl))
826
(deregwrite (g 'deregwrite impl))
827
(dememwrite (g 'dememwrite impl))
828
(dememtoreg (g 'dememtoreg impl))
829
(deisbranch (g 'deisbranch impl)) (dewrt (g 'dewrt impl))
830
(depredicteddirection (g 'depredicteddirection impl))
831
(depredictedtarget (g 'depredictedtarget impl))
832
(embpstate (g 'embpstate impl)) (empintrp (g 'empintrp impl))
833
(emppc (g 'emppc impl))
834
(emis_alu_exception (g 'emis_alu_exception impl))
835
(emis_taken_branch (g 'emis_taken_branch impl))
836
(emtargetpc (g 'emtargetpc impl)) (emarg2 (g 'emarg2 impl))
837
(emresult (g 'emresult impl)) (emdest (g 'emdest impl))
838
(emwrt (g 'emwrt impl))
839
(emisreturnfromexception (g 'emisreturnfromexception impl))
840
(emmispredictedtaken (g 'emmispredictedtaken impl))
841
(emmispredictednottaken (g 'emmispredictednottaken impl))
842
(emregwrite (g 'emregwrite impl))
843
(emmemwrite (g 'emmemwrite impl))
844
(emmemtoreg (g 'emmemtoreg impl))
845
(pdmemhist_2 (g 'pdmemhist_2 impl))
846
(pdmemhist_1 (g 'pdmemhist_1 impl)) (pdmem (g 'pdmem impl))
847
(pepchist_2 (g 'pepchist_2 impl))
848
(pepchist_1 (g 'pepchist_1 impl)) (pepc (g 'pepc impl))
849
(pisexceptionhist_2 (g 'pisexceptionhist_2 impl))
850
(pisexceptionhist_1 (g 'pisexceptionhist_1 impl))
851
(pisexception (g 'pisexception impl))
852
(mmbpstate (g 'mmbpstate impl)) (mmpintrp (g 'mmpintrp impl))
853
(mmisreturnfromexception (g 'mmisreturnfromexception impl))
854
(mmis_alu_exception (g 'mmis_alu_exception impl))
855
(mmppc (g 'mmppc impl)) (mmval (g 'mmval impl))
856
(mmdest (g 'mmdest impl)) (mmwrt (g 'mmwrt impl))
857
(mmregwrite (g 'mmregwrite impl))
858
(mwbpstate (g 'mwbpstate impl)) (mwpintrp (g 'mwpintrp impl))
859
(mwisreturnfromexception (g 'mwisreturnfromexception impl))
860
(mwis_alu_exception (g 'mwis_alu_exception impl))
861
(mwppc (g 'mwppc impl)) (mwval (g 'mwval impl))
862
(mwdest (g 'mwdest impl)) (mwwrt (g 'mwwrt impl))
863
(mwregwrite (g 'mwregwrite impl)))
864
(let* ((if_inst (read-pimem_a ppc pimem))
865
(predicted_direction (predictdirection bpstate))
866
(predicted_target (predicttarget bpstate))
867
(if_predict_branch_taken
868
(and (getisbranch if_inst) predicted_direction))
869
(if_id_src1 (src1 fdinst)) (if_id_src2 (src2 fdinst))
870
(stall (and (and deregwrite dewrt)
871
(or (equal if_id_src1 dedest)
872
(equal if_id_src2 dedest))))
873
(id_regwrite (getregwrite fdinst))
874
(id_memwrite (getmemwrite fdinst))
876
(and (and mwwrt (equal desrc1 mwdest)) mwregwrite))
878
(and (and mwwrt (equal desrc2 mwdest)) mwregwrite))
880
(and (and mmwrt (equal desrc1 mmdest)) mmregwrite))
882
(and (and mmwrt (equal desrc2 mmdest)) mmregwrite))
885
(ex_mem2_equal_src1 mmval)
886
(ex_wb_equal_src1 mwval)
890
(ex_mem2_equal_src2 mmval)
891
(ex_wb_equal_src2 mwval)
893
(ex_data2 (cond (deuseimm deimm) (t ex_fwd_src2)))
894
(ex_result (alu deop ex_fwd_src1 ex_data2))
895
(ex_is_alu_exception_temp
896
(alu_exception deop ex_fwd_src1 ex_data2))
898
(and (and ex_is_alu_exception_temp dewrt)
899
(or (or deregwrite dememwrite) deisbranch)))
900
(ex_is_taken_branch_temp
901
(takebranch deop ex_fwd_src1 ex_fwd_src2))
903
(and (and ex_is_taken_branch_temp dewrt) deisbranch))
904
(ex_targetpc (selecttargetpc deop ex_fwd_src1 deppc))
905
(equal_targetpc (equal ex_targetpc depredictedtarget))
906
(equal_targetpc_bar (not equal_targetpc))
907
(ex_predicteddirection depredicteddirection)
908
(mispredicted_nottaken_case1
909
(and ex_is_taken_branch (not ex_predicteddirection)))
910
(mispredicted_nottaken_case2
911
(and ex_is_taken_branch equal_targetpc_bar))
912
(mispredicted_nottaken
913
(or mispredicted_nottaken_case1
914
mispredicted_nottaken_case2))
916
(and (and ex_predicteddirection deisbranch)
917
(not ex_is_taken_branch)))
918
(mem1_readdata (dmem_read pdmem emresult))
919
(mem1_is_taken_branch (and emwrt emis_taken_branch))
920
(mem1_is_alu_exception (and emwrt emis_alu_exception))
921
(mem1_is_returnfromexception
922
(and emwrt emisreturnfromexception))
923
(mem1_is_returnfromexception_bar
924
(not mem1_is_returnfromexception))
925
(mem1_is_alu_exception_bar (not mem1_is_alu_exception))
926
(mem1_mispredicted_taken (and emmispredictedtaken emwrt))
927
(mem1_mispredicted_nottaken
928
(and emmispredictednottaken emwrt))
930
(or mem1_mispredicted_nottaken mem1_mispredicted_taken))
931
(mem1_is_interrupt_temp (isinterrupt empintrp))
932
(mem1_is_interrupt (and mem1_is_interrupt_temp emwrt))
933
(mem1_is_interrupt_bar (not mem1_is_interrupt))
934
(squash (or (or (or mem1_mispredicted
935
mem1_is_alu_exception)
937
mem1_is_returnfromexception))
938
(wb_is_alu_exception_bar (not mwis_alu_exception))
939
(wb_is_returnfromexception
940
(and mwwrt mwisreturnfromexception))
941
(wb_is_returnfromexception_bar
942
(not wb_is_returnfromexception))
943
(wb_is_interrupt_temp (isinterrupt mwpintrp))
944
(wb_is_interrupt (and wb_is_interrupt_temp mwwrt))
945
(wb_is_interrupt_bar (not wb_is_interrupt)))
946
(impl-state_a (nextpimem_a pimem)
947
(nextppc_a initi pc0 commit_impl commit_pc mem1_is_interrupt
948
emppc mem1_is_returnfromexception pepc
949
mem1_is_alu_exception alu_exception_handler
950
mem1_mispredicted_taken mem1_mispredicted_nottaken
951
emtargetpc stall ppc if_predict_branch_taken
953
(nextpintrp_a initi intrp0 commit_impl commit_intrp stall
955
(nextbpstate_a initi bpstate0 commit_impl commit_bpstate
957
(nextffbpstate_a initi ffbpstate0 stall ffbpstate bpstate)
958
(nextffpintrp_a initi ffpintrp0 stall ffpintrp pintrp)
959
(nextffpredicteddirection_a initi ffpredicteddirection0
960
stall ffpredicteddirection if_predict_branch_taken)
961
(nextffpredictedtarget_a initi ffpredictedtarget0 stall
962
ffpredictedtarget predicted_target)
963
(nextffwrt_a initi commit_impl squash stall ffwrt)
964
(nextffinst_a initi ffinst0 stall ffinst if_inst)
965
(nextffppc_a initi ffppc0 stall ffppc ppc)
966
(nextprf_a prf initi commit_impl mwwrt mwdest mwregwrite
967
wb_is_alu_exception_bar wb_is_interrupt_bar
968
wb_is_returnfromexception_bar mwval)
969
(nextfdpintrp_a initi fdpintrp0 stall fdpintrp ffpintrp)
970
(nextfdbpstate_a initi fdbpstate0 stall fdbpstate ffbpstate)
971
(nextfdppc_a initi fdppc0 stall fdppc ffppc)
972
(nextfdwrt_a initi commit_impl squash stall fdwrt ffwrt)
973
(nextfdinst_a initi fdinst0 stall fdinst ffinst)
974
(nextfdpredicteddirection_a initi fdpredicteddirection0
975
stall fdpredicteddirection ffpredicteddirection)
976
(nextfdpredictedtarget_a initi fdpredictedtarget0 stall
977
fdpredictedtarget ffpredictedtarget)
978
(nextdebpstate_a initi debpstate0 fdbpstate)
979
(nextdepintrp_a initi depintrp0 fdpintrp)
980
(nextdeppc_a initi deppc0 fdppc)
981
(nextdesrc1_a initi desrc10 if_id_src1)
982
(nextdesrc2_a initi desrc20 if_id_src2)
983
(nextdearg1_a initi a1 if_id_src1 prf commit_impl mwwrt
984
mwdest mwregwrite wb_is_alu_exception_bar
985
wb_is_interrupt_bar wb_is_returnfromexception_bar mwval)
986
(nextdearg2_a initi a2 if_id_src2 prf commit_impl mwwrt
987
mwdest mwregwrite wb_is_alu_exception_bar
988
wb_is_interrupt_bar wb_is_returnfromexception_bar mwval)
989
(nextdedest_a initi dedest0 fdinst)
990
(nextdeop_a initi deop0 fdinst)
991
(nextdeimm_a initi deimm0 fdinst)
992
(nextdeuseimm_a initi deuseimm0 fdinst)
993
(nextdeisreturnfromexception_a initi
994
deisreturnfromexception0 fdinst)
995
(nextderegwrite_a initi deregwrite0 id_regwrite)
996
(nextdememwrite_a initi dememwrite0 id_memwrite)
997
(nextdememtoreg_a initi dememtoreg0 fdinst)
998
(nextdeisbranch_a initi deisbranch0 fdinst)
999
(nextdewrt_a initi commit_impl squash stall fdwrt)
1000
(nextdepredicteddirection_a initi depredicteddirection0
1001
stall depredicteddirection fdpredicteddirection)
1002
(nextdepredictedtarget_a initi depredictedtarget0 stall
1003
depredictedtarget fdpredictedtarget)
1004
(nextembpstate_a initi embpstate0 debpstate)
1005
(nextempintrp_a initi empintrp0 depintrp)
1006
(nextemppc_a initi emppc0 deppc)
1007
(nextemis_alu_exception_a initi emis_alu_exception0
1008
ex_is_alu_exception)
1009
(nextemis_taken_branch_a initi emis_taken_branch0
1011
(nextemtargetpc_a initi emtargetpc0 ex_targetpc)
1012
(nextemarg2_a initi emarg20 ex_fwd_src2)
1013
(nextemresult_a initi emresult0 ex_result)
1014
(nextemdest_a initi emdest0 dedest)
1015
(nextemwrt_a initi commit_impl squash dewrt)
1016
(nextemisreturnfromexception_a initi
1017
emisreturnfromexception0 deisreturnfromexception)
1018
(nextemmispredictedtaken_a initi emmispredictedtaken0
1020
(nextemmispredictednottaken_a initi emmispredictednottaken0
1021
mispredicted_nottaken)
1022
(nextemregwrite_a initi emregwrite0 deregwrite)
1023
(nextemmemwrite_a initi emmemwrite0 dememwrite)
1024
(nextemmemtoreg_a initi emmemtoreg0 dememtoreg)
1025
(nextpdmemhist_2_a initi dmem0 pdmemhist_1)
1026
(nextpdmemhist_1_a initi dmem0 pdmem)
1027
(nextpdmem_a initi dmem0 commit_impl pdmemhist_2
1028
mem1_is_interrupt pdmem emwrt emmemwrite
1029
mem1_is_alu_exception_bar
1030
mem1_is_returnfromexception_bar emresult emarg2)
1031
(nextpepchist_2_a initi epc0 pepchist_1)
1032
(nextpepchist_1_a initi epc0 pepc)
1033
(nextpepc_a initi epc0 commit_impl pepchist_2
1034
mem1_is_alu_exception mem1_is_returnfromexception_bar
1035
mem1_is_interrupt_bar emppc pepc)
1036
(nextpisexceptionhist_2_a initi isexception0
1038
(nextpisexceptionhist_1_a initi isexception0 pisexception)
1039
(nextpisexception_a initi isexception0 commit_impl
1040
pisexceptionhist_2 mem1_is_alu_exception
1041
mem1_is_returnfromexception mem1_is_interrupt_bar
1042
mem1_is_returnfromexception_bar pisexception)
1043
(nextmmbpstate_a initi mmbpstate0 embpstate)
1044
(nextmmpintrp_a initi mmpintrp0 empintrp)
1045
(nextmmisreturnfromexception_a initi
1046
mmisreturnfromexception0 emisreturnfromexception)
1047
(nextmmis_alu_exception_a initi mmis_alu_exception0
1049
(nextmmppc_a initi mmppc0 emppc)
1050
(nextmmval_a initi mmval0 emmemtoreg mem1_readdata emresult)
1051
(nextmmdest_a initi mmdest0 emdest)
1052
(nextmmwrt_a initi commit_impl emwrt)
1053
(nextmmregwrite_a initi mmregwrite0 emregwrite)
1054
(nextmwbpstate_a initi mwbpstate0 mmbpstate)
1055
(nextmwpintrp_a initi mwpintrp0 mmpintrp)
1056
(nextmwisreturnfromexception_a initi
1057
mwisreturnfromexception0 mmisreturnfromexception)
1058
(nextmwis_alu_exception_a initi mwis_alu_exception0
1060
(nextmwppc_a initi mwppc0 mmppc)
1061
(nextmwval_a initi mwval0 mmval)
1062
(nextmwdest_a initi mwdest0 mmdest)
1063
(nextmwwrt_a initi commit_impl mmwrt)
1064
(nextmwregwrite_a initi mwregwrite0 mmregwrite)))))
1066
(defun impl-initialize_a
1067
(impl pc0 intrp0 bpstate0 ffbpstate0 ffpintrp0
1068
ffpredicteddirection0 ffpredictedtarget0 ffinst0 ffppc0
1069
fdpintrp0 fdbpstate0 fdppc0 fdinst0 fdpredicteddirection0
1070
fdpredictedtarget0 debpstate0 depintrp0 deppc0 desrc10
1071
desrc20 a1 a2 dedest0 deop0 deimm0 deuseimm0
1072
deisreturnfromexception0 deregwrite0 dememwrite0
1073
dememtoreg0 deisbranch0 depredicteddirection0
1074
depredictedtarget0 embpstate0 empintrp0 emppc0
1075
emis_alu_exception0 emis_taken_branch0 emtargetpc0
1076
emarg20 emresult0 emdest0 emisreturnfromexception0
1077
emmispredictedtaken0 emmispredictednottaken0 emregwrite0
1078
emmemwrite0 emmemtoreg0 dmem0 epc0 isexception0
1079
mmbpstate0 mmpintrp0 mmisreturnfromexception0
1080
mmis_alu_exception0 mmppc0 mmval0 mmdest0 mmregwrite0
1081
mwbpstate0 mwpintrp0 mwisreturnfromexception0
1082
mwis_alu_exception0 mwppc0 mwval0 mwdest0 mwregwrite0)
1083
(let* ((pimem (g 'pimem impl)) (ppc (g 'ppc impl))
1084
(pintrp (g 'pintrp impl)) (bpstate (g 'bpstate impl))
1085
(ffbpstate (g 'ffbpstate impl)) (ffpintrp (g 'ffpintrp impl))
1086
(ffpredicteddirection (g 'ffpredicteddirection impl))
1087
(ffpredictedtarget (g 'ffpredictedtarget impl))
1088
(ffwrt (g 'ffwrt impl)) (ffinst (g 'ffinst impl))
1089
(ffppc (g 'ffppc impl)) (prf (g 'prf impl))
1090
(fdpintrp (g 'fdpintrp impl)) (fdbpstate (g 'fdbpstate impl))
1091
(fdppc (g 'fdppc impl)) (fdwrt (g 'fdwrt impl))
1092
(fdinst (g 'fdinst impl))
1093
(fdpredicteddirection (g 'fdpredicteddirection impl))
1094
(fdpredictedtarget (g 'fdpredictedtarget impl))
1095
(debpstate (g 'debpstate impl)) (depintrp (g 'depintrp impl))
1096
(deppc (g 'deppc impl)) (desrc1 (g 'desrc1 impl))
1097
(desrc2 (g 'desrc2 impl)) (dearg1 (g 'dearg1 impl))
1098
(dearg2 (g 'dearg2 impl)) (dedest (g 'dedest impl))
1099
(deop (g 'deop impl)) (deimm (g 'deimm impl))
1100
(deuseimm (g 'deuseimm impl))
1101
(deisreturnfromexception (g 'deisreturnfromexception impl))
1102
(deregwrite (g 'deregwrite impl))
1103
(dememwrite (g 'dememwrite impl))
1104
(dememtoreg (g 'dememtoreg impl))
1105
(deisbranch (g 'deisbranch impl)) (dewrt (g 'dewrt impl))
1106
(depredicteddirection (g 'depredicteddirection impl))
1107
(depredictedtarget (g 'depredictedtarget impl))
1108
(embpstate (g 'embpstate impl)) (empintrp (g 'empintrp impl))
1109
(emppc (g 'emppc impl))
1110
(emis_alu_exception (g 'emis_alu_exception impl))
1111
(emis_taken_branch (g 'emis_taken_branch impl))
1112
(emtargetpc (g 'emtargetpc impl)) (emarg2 (g 'emarg2 impl))
1113
(emresult (g 'emresult impl)) (emdest (g 'emdest impl))
1114
(emwrt (g 'emwrt impl))
1115
(emisreturnfromexception (g 'emisreturnfromexception impl))
1116
(emmispredictedtaken (g 'emmispredictedtaken impl))
1117
(emmispredictednottaken (g 'emmispredictednottaken impl))
1118
(emregwrite (g 'emregwrite impl))
1119
(emmemwrite (g 'emmemwrite impl))
1120
(emmemtoreg (g 'emmemtoreg impl))
1121
(pdmemhist_2 (g 'pdmemhist_2 impl))
1122
(pdmemhist_1 (g 'pdmemhist_1 impl)) (pdmem (g 'pdmem impl))
1123
(pepchist_2 (g 'pepchist_2 impl))
1124
(pepchist_1 (g 'pepchist_1 impl)) (pepc (g 'pepc impl))
1125
(pisexceptionhist_2 (g 'pisexceptionhist_2 impl))
1126
(pisexceptionhist_1 (g 'pisexceptionhist_1 impl))
1127
(pisexception (g 'pisexception impl))
1128
(mmbpstate (g 'mmbpstate impl)) (mmpintrp (g 'mmpintrp impl))
1129
(mmisreturnfromexception (g 'mmisreturnfromexception impl))
1130
(mmis_alu_exception (g 'mmis_alu_exception impl))
1131
(mmppc (g 'mmppc impl)) (mmval (g 'mmval impl))
1132
(mmdest (g 'mmdest impl)) (mmwrt (g 'mmwrt impl))
1133
(mmregwrite (g 'mmregwrite impl))
1134
(mwbpstate (g 'mwbpstate impl)) (mwpintrp (g 'mwpintrp impl))
1135
(mwisreturnfromexception (g 'mwisreturnfromexception impl))
1136
(mwis_alu_exception (g 'mwis_alu_exception impl))
1137
(mwppc (g 'mwppc impl)) (mwval (g 'mwval impl))
1138
(mwdest (g 'mwdest impl)) (mwwrt (g 'mwwrt impl))
1139
(mwregwrite (g 'mwregwrite impl)))
1140
(let* ((if_inst (read-pimem_a ppc pimem))
1141
(predicted_direction (predictdirection bpstate))
1142
(predicted_target (predicttarget bpstate))
1143
(if_predict_branch_taken
1144
(and (getisbranch if_inst) predicted_direction))
1145
(if_id_src1 (src1 fdinst)) (if_id_src2 (src2 fdinst))
1146
(stall (and (and deregwrite dewrt)
1147
(or (equal if_id_src1 dedest)
1148
(equal if_id_src2 dedest))))
1149
(id_regwrite (getregwrite fdinst))
1150
(id_memwrite (getmemwrite fdinst))
1152
(and (and mwwrt (equal desrc1 mwdest)) mwregwrite))
1154
(and (and mwwrt (equal desrc2 mwdest)) mwregwrite))
1156
(and (and mmwrt (equal desrc1 mmdest)) mmregwrite))
1158
(and (and mmwrt (equal desrc2 mmdest)) mmregwrite))
1161
(ex_mem2_equal_src1 mmval)
1162
(ex_wb_equal_src1 mwval)
1166
(ex_mem2_equal_src2 mmval)
1167
(ex_wb_equal_src2 mwval)
1169
(ex_data2 (cond (deuseimm deimm) (t ex_fwd_src2)))
1170
(ex_result (alu deop ex_fwd_src1 ex_data2))
1171
(ex_is_alu_exception_temp
1172
(alu_exception deop ex_fwd_src1 ex_data2))
1173
(ex_is_alu_exception
1174
(and (and ex_is_alu_exception_temp dewrt)
1175
(or (or deregwrite dememwrite) deisbranch)))
1176
(ex_is_taken_branch_temp
1177
(takebranch deop ex_fwd_src1 ex_fwd_src2))
1179
(and (and ex_is_taken_branch_temp dewrt) deisbranch))
1180
(ex_targetpc (selecttargetpc deop ex_fwd_src1 deppc))
1181
(equal_targetpc (equal ex_targetpc depredictedtarget))
1182
(equal_targetpc_bar (not equal_targetpc))
1183
(ex_predicteddirection depredicteddirection)
1184
(mispredicted_nottaken_case1
1185
(and ex_is_taken_branch (not ex_predicteddirection)))
1186
(mispredicted_nottaken_case2
1187
(and ex_is_taken_branch equal_targetpc_bar))
1188
(mispredicted_nottaken
1189
(or mispredicted_nottaken_case1
1190
mispredicted_nottaken_case2))
1192
(and (and ex_predicteddirection deisbranch)
1193
(not ex_is_taken_branch)))
1194
(mem1_readdata (dmem_read pdmem emresult))
1195
(mem1_is_taken_branch (and emwrt emis_taken_branch))
1196
(mem1_is_alu_exception (and emwrt emis_alu_exception))
1197
(mem1_is_returnfromexception
1198
(and emwrt emisreturnfromexception))
1199
(mem1_is_returnfromexception_bar
1200
(not mem1_is_returnfromexception))
1201
(mem1_is_alu_exception_bar (not mem1_is_alu_exception))
1202
(mem1_mispredicted_taken (and emmispredictedtaken emwrt))
1203
(mem1_mispredicted_nottaken
1204
(and emmispredictednottaken emwrt))
1206
(or mem1_mispredicted_nottaken mem1_mispredicted_taken))
1207
(mem1_is_interrupt_temp (isinterrupt empintrp))
1208
(mem1_is_interrupt (and mem1_is_interrupt_temp emwrt))
1209
(mem1_is_interrupt_bar (not mem1_is_interrupt))
1210
(squash (or (or (or mem1_mispredicted
1211
mem1_is_alu_exception)
1213
mem1_is_returnfromexception))
1214
(wb_is_alu_exception_bar (not mwis_alu_exception))
1215
(wb_is_returnfromexception
1216
(and mwwrt mwisreturnfromexception))
1217
(wb_is_returnfromexception_bar
1218
(not wb_is_returnfromexception))
1219
(wb_is_interrupt_temp (isinterrupt mwpintrp))
1220
(wb_is_interrupt (and wb_is_interrupt_temp mwwrt))
1221
(wb_is_interrupt_bar (not wb_is_interrupt)))
1222
(impl-state_a (initpimem_a pimem) (initppc_a pc0)
1223
(initpintrp_a intrp0) (initbpstate_a bpstate0)
1224
(initffbpstate_a ffbpstate0) (initffpintrp_a ffpintrp0)
1225
(initffpredicteddirection_a ffpredicteddirection0)
1226
(initffpredictedtarget_a ffpredictedtarget0) (initffwrt_a)
1227
(initffinst_a ffinst0) (initffppc_a ffppc0) (initprf_a prf)
1228
(initfdpintrp_a fdpintrp0) (initfdbpstate_a fdbpstate0)
1229
(initfdppc_a fdppc0) (initfdwrt_a) (initfdinst_a fdinst0)
1230
(initfdpredicteddirection_a fdpredicteddirection0)
1231
(initfdpredictedtarget_a fdpredictedtarget0)
1232
(initdebpstate_a debpstate0) (initdepintrp_a depintrp0)
1233
(initdeppc_a deppc0) (initdesrc1_a desrc10)
1234
(initdesrc2_a desrc20) (initdearg1_a a1) (initdearg2_a a2)
1235
(initdedest_a dedest0) (initdeop_a deop0)
1236
(initdeimm_a deimm0) (initdeuseimm_a deuseimm0)
1237
(initdeisreturnfromexception_a deisreturnfromexception0)
1238
(initderegwrite_a deregwrite0)
1239
(initdememwrite_a dememwrite0)
1240
(initdememtoreg_a dememtoreg0)
1241
(initdeisbranch_a deisbranch0) (initdewrt_a)
1242
(initdepredicteddirection_a depredicteddirection0)
1243
(initdepredictedtarget_a depredictedtarget0)
1244
(initembpstate_a embpstate0) (initempintrp_a empintrp0)
1245
(initemppc_a emppc0)
1246
(initemis_alu_exception_a emis_alu_exception0)
1247
(initemis_taken_branch_a emis_taken_branch0)
1248
(initemtargetpc_a emtargetpc0) (initemarg2_a emarg20)
1249
(initemresult_a emresult0) (initemdest_a emdest0)
1251
(initemisreturnfromexception_a emisreturnfromexception0)
1252
(initemmispredictedtaken_a emmispredictedtaken0)
1253
(initemmispredictednottaken_a emmispredictednottaken0)
1254
(initemregwrite_a emregwrite0)
1255
(initemmemwrite_a emmemwrite0)
1256
(initemmemtoreg_a emmemtoreg0) (initpdmemhist_2_a dmem0)
1257
(initpdmemhist_1_a dmem0) (initpdmem_a dmem0)
1258
(initpepchist_2_a epc0) (initpepchist_1_a epc0)
1259
(initpepc_a epc0) (initpisexceptionhist_2_a isexception0)
1260
(initpisexceptionhist_1_a isexception0)
1261
(initpisexception_a isexception0)
1262
(initmmbpstate_a mmbpstate0) (initmmpintrp_a mmpintrp0)
1263
(initmmisreturnfromexception_a mmisreturnfromexception0)
1264
(initmmis_alu_exception_a mmis_alu_exception0)
1265
(initmmppc_a mmppc0) (initmmval_a mmval0)
1266
(initmmdest_a mmdest0) (initmmwrt_a)
1267
(initmmregwrite_a mmregwrite0) (initmwbpstate_a mwbpstate0)
1268
(initmwpintrp_a mwpintrp0)
1269
(initmwisreturnfromexception_a mwisreturnfromexception0)
1270
(initmwis_alu_exception_a mwis_alu_exception0)
1271
(initmwppc_a mwppc0) (initmwval_a mwval0)
1272
(initmwdest_a mwdest0) (initmwwrt_a)
1273
(initmwregwrite_a mwregwrite0)))))
1275
(defun spec-state_a (simem spc sintrp srf sdmem sepc sisexception)
1276
(seq nil 'simem simem 'spc spc 'sintrp sintrp 'srf srf 'sdmem sdmem
1277
'sepc sepc 'sisexception sisexception))
1279
(defun initsimem_a (simem) (cons (s 0 t (s 1 nil nil)) simem))
1281
(defun nextsimem_a (simem) (cons (s 0 nil (s 1 nil nil)) simem))
1283
(defun initspc_a (pc0) pc0)
1286
(initi pc0 project_impl project_pc isa is_interrupt spc
1287
is_returnfromexception sepc is_alu_exception
1288
alu_exception_handler is_taken_branch targetpc)
1291
(project_impl project_pc)
1292
((and isa is_interrupt) spc)
1293
((and isa is_returnfromexception) sepc)
1294
((and isa is_alu_exception) alu_exception_handler)
1295
((and isa is_taken_branch) targetpc)
1299
(defun initsintrp_a (intrp0) intrp0)
1302
(initi intrp0 project_impl project_intrp isa sintrp)
1305
(project_impl project_intrp)
1306
(isa (nextintrp sintrp))
1309
(defun initsrf_a (srf) (cons (s 0 t (s 1 nil nil)) srf))
1312
(srf initi project_impl impl.prf isa inst regwrite
1313
is_alu_exception_bar is_interrupt_bar
1314
is_returnfromexception_bar val)
1322
(s 7 is_alu_exception_bar
1323
(s 8 is_interrupt_bar
1324
(s 9 is_returnfromexception_bar
1325
(s 10 val nil)))))))))))
1328
(defun initsdmem_a (dmem0) dmem0)
1331
(initi dmem0 project_impl impl.pdmemhist_2 isa is_interrupt
1332
sdmem memwrite is_alu_exception_bar
1333
is_returnfromexception_bar result arg2_temp)
1336
(project_impl impl.pdmemhist_2)
1337
((and isa is_interrupt) (intrp_mod_dmem sdmem))
1338
((and (and (and isa memwrite) is_alu_exception_bar)
1339
is_returnfromexception_bar)
1340
(nextdmem sdmem result arg2_temp))
1343
(defun initsepc_a (epc0) epc0)
1346
(initi epc0 isa is_alu_exception is_returnfromexception_bar
1347
is_interrupt_bar spc sepc)
1350
((and (and (and isa is_alu_exception) is_returnfromexception_bar)
1355
(defun initsisexception_a (isexception0) isexception0)
1357
(defun nextsisexception_a
1358
(initi isexception0 isa is_alu_exception is_returnfromexception
1359
is_interrupt_bar is_returnfromexception_bar
1362
(initi isexception0)
1363
((and (and isa (or is_alu_exception is_returnfromexception))
1365
(and is_alu_exception is_returnfromexception_bar))
1368
(defun spec-simulate_a
1369
(spec initi pc0 project_impl project_pc isa
1370
alu_exception_handler intrp0 project_intrp impl.prf dmem0
1371
impl.pdmemhist_2 epc0 isexception0)
1372
(let* ((simem (g 'simem spec)) (spc (g 'spc spec))
1373
(sintrp (g 'sintrp spec)) (srf (g 'srf spec))
1374
(sdmem (g 'sdmem spec)) (sepc (g 'sepc spec))
1375
(sisexception (g 'sisexception spec)))
1376
(let* ((inst (read-simem_a spc simem))
1377
(regwrite (getregwrite inst)) (memtoreg (getmemtoreg inst))
1378
(memwrite (getmemwrite inst)) (isbranch (getisbranch inst))
1379
(is_returnfromexception (getreturnfromexception inst))
1380
(is_interrupt (isinterrupt sintrp))
1381
(is_interrupt_bar (not is_interrupt))
1382
(useimm (getuseimm inst)) (imm (getimm inst))
1383
(arg1 (read-srf_a (src1 inst) srf))
1384
(arg2_temp (read-srf_a (src2 inst) srf))
1385
(arg2 (cond (useimm imm) (t arg2_temp)))
1386
(result (alu (opcode inst) arg1 arg2))
1387
(is_alu_exception_temp
1388
(alu_exception (opcode inst) arg1 arg2))
1390
(and is_alu_exception_temp
1391
(or (or regwrite memwrite) isbranch)))
1392
(is_alu_exception_bar (not is_alu_exception))
1393
(is_returnfromexception_bar (not is_returnfromexception))
1394
(is_taken_branch_temp
1395
(takebranch (opcode inst) arg1 arg2_temp))
1396
(is_taken_branch (and is_taken_branch_temp isbranch))
1397
(targetpc (selecttargetpc (opcode inst) arg1 spc))
1398
(readdata (dmem_read sdmem result))
1399
(val (cond (memtoreg readdata) (t result))))
1400
(spec-state_a (nextsimem_a simem)
1401
(nextspc_a initi pc0 project_impl project_pc isa
1402
is_interrupt spc is_returnfromexception sepc
1403
is_alu_exception alu_exception_handler is_taken_branch
1405
(nextsintrp_a initi intrp0 project_impl project_intrp isa
1407
(nextsrf_a srf initi project_impl impl.prf isa inst regwrite
1408
is_alu_exception_bar is_interrupt_bar
1409
is_returnfromexception_bar val)
1410
(nextsdmem_a initi dmem0 project_impl impl.pdmemhist_2 isa
1411
is_interrupt sdmem memwrite is_alu_exception_bar
1412
is_returnfromexception_bar result arg2_temp)
1413
(nextsepc_a initi epc0 isa is_alu_exception
1414
is_returnfromexception_bar is_interrupt_bar spc sepc)
1415
(nextsisexception_a initi isexception0 isa is_alu_exception
1416
is_returnfromexception is_interrupt_bar
1417
is_returnfromexception_bar sisexception)))))
1419
(defun spec-initialize_a (spec pc0 intrp0 dmem0 epc0 isexception0)
1420
(let* ((simem (g 'simem spec)) (spc (g 'spc spec))
1421
(sintrp (g 'sintrp spec)) (srf (g 'srf spec))
1422
(sdmem (g 'sdmem spec)) (sepc (g 'sepc spec))
1423
(sisexception (g 'sisexception spec)))
1424
(let* ((inst (read-simem_a spc simem))
1425
(regwrite (getregwrite inst)) (memtoreg (getmemtoreg inst))
1426
(memwrite (getmemwrite inst)) (isbranch (getisbranch inst))
1427
(is_returnfromexception (getreturnfromexception inst))
1428
(is_interrupt (isinterrupt sintrp))
1429
(is_interrupt_bar (not is_interrupt))
1430
(useimm (getuseimm inst)) (imm (getimm inst))
1431
(arg1 (read-srf_a (src1 inst) srf))
1432
(arg2_temp (read-srf_a (src2 inst) srf))
1433
(arg2 (cond (useimm imm) (t arg2_temp)))
1434
(result (alu (opcode inst) arg1 arg2))
1435
(is_alu_exception_temp
1436
(alu_exception (opcode inst) arg1 arg2))
1438
(and is_alu_exception_temp
1439
(or (or regwrite memwrite) isbranch)))
1440
(is_alu_exception_bar (not is_alu_exception))
1441
(is_returnfromexception_bar (not is_returnfromexception))
1442
(is_taken_branch_temp
1443
(takebranch (opcode inst) arg1 arg2_temp))
1444
(is_taken_branch (and is_taken_branch_temp isbranch))
1445
(targetpc (selecttargetpc (opcode inst) arg1 spc))
1446
(readdata (dmem_read sdmem result))
1447
(val (cond (memtoreg readdata) (t result))))
1448
(spec-state_a (initsimem_a simem) (initspc_a pc0)
1449
(initsintrp_a intrp0) (initsrf_a srf) (initsdmem_a dmem0)
1450
(initsepc_a epc0) (initsisexception_a isexception0)))))
1453
(st initi isa project_impl project_pc project_intrp commit_impl
1454
commit_pc commit_bpstate commit_intrp pc0
1455
alu_exception_handler intrp0 bpstate0 ffbpstate0 ffpintrp0
1456
ffpredicteddirection0 ffpredictedtarget0 ffinst0 ffppc0
1457
fdpintrp0 fdbpstate0 fdppc0 fdinst0 fdpredicteddirection0
1458
fdpredictedtarget0 debpstate0 depintrp0 deppc0 desrc10
1459
desrc20 a1 a2 dedest0 deop0 deimm0 deuseimm0
1460
deisreturnfromexception0 deregwrite0 dememwrite0
1461
dememtoreg0 deisbranch0 depredicteddirection0
1462
depredictedtarget0 embpstate0 empintrp0 emppc0
1463
emis_alu_exception0 emis_taken_branch0 emtargetpc0 emarg20
1464
emresult0 emdest0 emisreturnfromexception0
1465
emmispredictedtaken0 emmispredictednottaken0 emregwrite0
1466
emmemwrite0 emmemtoreg0 dmem0 epc0 isexception0 mmbpstate0
1467
mmpintrp0 mmisreturnfromexception0 mmis_alu_exception0
1468
mmppc0 mmval0 mmdest0 mmregwrite0 mwbpstate0 mwpintrp0
1469
mwisreturnfromexception0 mwis_alu_exception0 mwppc0 mwval0
1470
mwdest0 mwregwrite0 impl.prf impl.pdmemhist_2)
1472
(impl-simulate_a (g 'impl st) initi pc0 commit_impl commit_pc
1473
alu_exception_handler intrp0 commit_intrp bpstate0
1474
commit_bpstate ffbpstate0 ffpintrp0 ffpredicteddirection0
1475
ffpredictedtarget0 ffinst0 ffppc0 fdpintrp0 fdbpstate0
1476
fdppc0 fdinst0 fdpredicteddirection0 fdpredictedtarget0
1477
debpstate0 depintrp0 deppc0 desrc10 desrc20 a1 a2 dedest0
1478
deop0 deimm0 deuseimm0 deisreturnfromexception0 deregwrite0
1479
dememwrite0 dememtoreg0 deisbranch0 depredicteddirection0
1480
depredictedtarget0 embpstate0 empintrp0 emppc0
1481
emis_alu_exception0 emis_taken_branch0 emtargetpc0 emarg20
1482
emresult0 emdest0 emisreturnfromexception0
1483
emmispredictedtaken0 emmispredictednottaken0 emregwrite0
1484
emmemwrite0 emmemtoreg0 dmem0 epc0 isexception0 mmbpstate0
1485
mmpintrp0 mmisreturnfromexception0 mmis_alu_exception0
1486
mmppc0 mmval0 mmdest0 mmregwrite0 mwbpstate0 mwpintrp0
1487
mwisreturnfromexception0 mwis_alu_exception0 mwppc0 mwval0
1488
mwdest0 mwregwrite0)
1489
(spec-simulate_a (g 'spec st) initi pc0 project_impl project_pc
1490
isa alu_exception_handler intrp0 project_intrp impl.prf
1491
dmem0 impl.pdmemhist_2 epc0 isexception0)))
1494
(st initi isa project_impl project_pc project_intrp commit_impl
1495
commit_pc commit_bpstate commit_intrp pc0 intrp0 bpstate0
1496
ffbpstate0 ffpintrp0 ffpredicteddirection0
1497
ffpredictedtarget0 ffinst0 ffppc0 fdpintrp0 fdbpstate0
1498
fdppc0 fdinst0 fdpredicteddirection0 fdpredictedtarget0
1499
debpstate0 depintrp0 deppc0 desrc10 desrc20 a1 a2 dedest0
1500
deop0 deimm0 deuseimm0 deisreturnfromexception0 deregwrite0
1501
dememwrite0 dememtoreg0 deisbranch0 depredicteddirection0
1502
depredictedtarget0 embpstate0 empintrp0 emppc0
1503
emis_alu_exception0 emis_taken_branch0 emtargetpc0 emarg20
1504
emresult0 emdest0 emisreturnfromexception0
1505
emmispredictedtaken0 emmispredictednottaken0 emregwrite0
1506
emmemwrite0 emmemtoreg0 dmem0 epc0 isexception0 mmbpstate0
1507
mmpintrp0 mmisreturnfromexception0 mmis_alu_exception0
1508
mmppc0 mmval0 mmdest0 mmregwrite0 mwbpstate0 mwpintrp0
1509
mwisreturnfromexception0 mwis_alu_exception0 mwppc0 mwval0
1510
mwdest0 mwregwrite0)
1512
(impl-initialize_a (g 'impl st) pc0 intrp0 bpstate0 ffbpstate0
1513
ffpintrp0 ffpredicteddirection0 ffpredictedtarget0 ffinst0
1514
ffppc0 fdpintrp0 fdbpstate0 fdppc0 fdinst0
1515
fdpredicteddirection0 fdpredictedtarget0 debpstate0
1516
depintrp0 deppc0 desrc10 desrc20 a1 a2 dedest0 deop0 deimm0
1517
deuseimm0 deisreturnfromexception0 deregwrite0 dememwrite0
1518
dememtoreg0 deisbranch0 depredicteddirection0
1519
depredictedtarget0 embpstate0 empintrp0 emppc0
1520
emis_alu_exception0 emis_taken_branch0 emtargetpc0 emarg20
1521
emresult0 emdest0 emisreturnfromexception0
1522
emmispredictedtaken0 emmispredictednottaken0 emregwrite0
1523
emmemwrite0 emmemtoreg0 dmem0 epc0 isexception0 mmbpstate0
1524
mmpintrp0 mmisreturnfromexception0 mmis_alu_exception0
1525
mmppc0 mmval0 mmdest0 mmregwrite0 mwbpstate0 mwpintrp0
1526
mwisreturnfromexception0 mwis_alu_exception0 mwppc0 mwval0
1527
mwdest0 mwregwrite0)
1528
(spec-initialize_a (g 'spec st) pc0 intrp0 dmem0 epc0
1532
(ppc_v impl.ppc prf_v a1 impl.prf pimem_v impl.pimem pdmem_v
1533
impl.pdmem pepc_v impl.pepc pisexception_v
1534
impl.pisexception ffwrt_v impl.ffwrt ffppc_v impl.ffppc
1535
ffinst_v impl.ffinst fdwrt_v impl.fdwrt fdppc_v
1536
impl.fdppc fdinst_v impl.fdinst dewrt_v impl.dewrt
1537
deppc_v impl.deppc deop_v impl.deop dearg1_v impl.dearg1
1538
dearg2_v impl.dearg2 dedest_v impl.dedest desrc1_v
1539
impl.desrc1 desrc2_v impl.desrc2 deimm_v impl.deimm
1540
deuseimm_v impl.deuseimm deisbranch_v impl.deisbranch
1541
dememtoreg_v impl.dememtoreg dememwrite_v
1542
impl.dememwrite deisreturnfromexception_v
1543
impl.deisreturnfromexception deregwrite_v
1544
impl.deregwrite emwrt_v impl.emwrt emtargetpc_v
1545
impl.emtargetpc emdest_v impl.emdest emarg2_v
1546
impl.emarg2 emregwrite_v impl.emregwrite emresult_v
1547
impl.emresult emis_taken_branch_v impl.emis_taken_branch
1548
emmemtoreg_v impl.emmemtoreg emis_alu_exception_v
1549
impl.emis_alu_exception emisreturnfromexception_v
1550
impl.emisreturnfromexception emmemwrite_v
1551
impl.emmemwrite mmwrt_v impl.mmwrt mmval_v impl.mmval
1552
mmdest_v impl.mmdest mmregwrite_v impl.mmregwrite
1553
mmisreturnfromexception_v impl.mmisreturnfromexception
1554
mmis_alu_exception_v impl.mmis_alu_exception mwwrt_v
1555
impl.mwwrt mwval_v impl.mwval mwdest_v impl.mwdest
1556
mwregwrite_v impl.mwregwrite mwisreturnfromexception_v
1557
impl.mwisreturnfromexception mwis_alu_exception_v
1558
impl.mwis_alu_exception)
1559
(declare (xargs :normalize nil))
1560
(and (and (and (and (and (and (and (and
1570
(equal ppc_v impl.ppc)
1572
(read-prf_a a1 prf_v)
1582
(equal pepc_v impl.pepc))
1583
(equalb pisexception_v
1585
(equalb ffwrt_v impl.ffwrt))
1589
(equal ffppc_v impl.ffppc))
1592
(equalb fdwrt_v impl.fdwrt))
1596
(equal fdppc_v impl.fdppc))
1597
(equal fdinst_v impl.fdinst))))
1598
(equalb dewrt_v impl.dewrt))
1632
(equalb deisbranch_v
1634
(equalb dememtoreg_v
1636
(equalb dememwrite_v
1639
deisreturnfromexception_v
1640
impl.deisreturnfromexception))
1641
(equalb deregwrite_v
1643
(equalb emwrt_v impl.emwrt))
1661
(equalb emregwrite_v
1665
(equalb emis_taken_branch_v
1666
impl.emis_taken_branch))
1667
(equalb emmemtoreg_v
1669
(equalb emis_alu_exception_v
1670
impl.emis_alu_exception))
1672
emisreturnfromexception_v
1673
impl.emisreturnfromexception))
1674
(equalb emmemwrite_v
1676
(equalb mmwrt_v impl.mmwrt))
1681
(equal mmval_v impl.mmval))
1682
(equal mmdest_v impl.mmdest))
1683
(equalb mmregwrite_v
1685
(equalb mmisreturnfromexception_v
1686
impl.mmisreturnfromexception))
1687
(equalb mmis_alu_exception_v
1688
impl.mmis_alu_exception))))
1689
(equalb mwwrt_v impl.mwwrt))
1691
(and (and (and (and (and impl.mwwrt
1692
(equal mwval_v impl.mwval))
1693
(equal mwdest_v impl.mwdest))
1694
(equalb mwregwrite_v impl.mwregwrite))
1695
(equalb mwisreturnfromexception_v
1696
impl.mwisreturnfromexception))
1697
(equalb mwis_alu_exception_v
1698
impl.mwis_alu_exception)))))
1701
(impl.mwwrt zero impl.mmwrt impl.emwrt impl.dewrt impl.fdwrt
1705
(impl.mmwrt (add-1 zero))
1706
(impl.emwrt (add-1 (add-1 zero)))
1707
(impl.dewrt (add-1 (add-1 (add-1 zero))))
1708
(impl.fdwrt (add-1 (add-1 (add-1 (add-1 zero)))))
1709
(impl.ffwrt (add-1 (add-1 (add-1 (add-1 (add-1 zero))))))
1710
(t (add-1 (add-1 (add-1 (add-1 (add-1 (add-1 zero)))))))))
1713
(impl.mwwrt impl.mwppc impl.mmwrt impl.mmppc impl.emwrt
1714
impl.emppc impl.dewrt impl.deppc impl.fdwrt impl.fdppc
1715
impl.ffwrt impl.ffppc impl.ppc)
1717
(impl.mwwrt impl.mwppc)
1718
(impl.mmwrt impl.mmppc)
1719
(impl.emwrt impl.emppc)
1720
(impl.dewrt impl.deppc)
1721
(impl.fdwrt impl.fdppc)
1722
(impl.ffwrt impl.ffppc)
1725
(defun committedbpstate
1726
(impl.mwwrt impl.mwbpstate impl.mmwrt impl.mmbpstate impl.emwrt
1727
impl.embpstate impl.dewrt impl.debpstate impl.fdwrt
1728
impl.fdbpstate impl.ffwrt impl.ffbpstate impl.bpstate)
1730
(impl.mwwrt impl.mwbpstate)
1731
(impl.mmwrt impl.mmbpstate)
1732
(impl.emwrt impl.embpstate)
1733
(impl.dewrt impl.debpstate)
1734
(impl.fdwrt impl.fdbpstate)
1735
(impl.ffwrt impl.ffbpstate)
1738
(defun committedintrp
1739
(impl.mwwrt impl.mwpintrp impl.mmwrt impl.mmpintrp impl.emwrt
1740
impl.empintrp impl.dewrt impl.depintrp impl.fdwrt
1741
impl.fdpintrp impl.ffwrt impl.ffpintrp impl.pintrp)
1743
(impl.mwwrt impl.mwpintrp)
1744
(impl.mmwrt impl.mmpintrp)
1745
(impl.emwrt impl.empintrp)
1746
(impl.dewrt impl.depintrp)
1747
(impl.fdwrt impl.fdpintrp)
1748
(impl.ffwrt impl.ffpintrp)
1753
(implies (and (integerp intrp_exception_handler)
1754
(integerp intrp0) (integerp pc0)
1755
(integerp dmem0) (integerp epc0)
1756
(booleanp isexception0) (integerp bpstate0)
1757
(integerp alu_exception_handler) (integerp a)
1758
(integerp zero) (integerp ffpintrp0)
1759
(integerp fdpintrp0) (integerp depintrp0)
1760
(integerp empintrp0) (integerp mmpintrp0)
1761
(integerp mwpintrp0) (integerp fdbpstate0)
1762
(booleanp fdpredicteddirection0)
1763
(integerp fdpredictedtarget0)
1764
(booleanp emmispredictednottaken0)
1765
(integerp debpstate0)
1766
(booleanp depredicteddirection0)
1767
(integerp depredictedtarget0)
1768
(booleanp emmispredictedtaken0)
1769
(integerp embpstate0) (integerp mmbpstate0)
1770
(integerp mwbpstate0)
1771
(integerp ffpredictedtarget0)
1772
(integerp ffbpstate0)
1773
(booleanp ffpredicteddirection0)
1774
(integerp emppc0) (integerp mmppc0)
1775
(integerp mwppc0) (booleanp deisbranch0)
1776
(booleanp emis_taken_branch0)
1777
(integerp emtargetpc0) (integerp ffppc0)
1778
(integerp fdppc0) (integerp deppc0)
1779
(integerp mwval0) (integerp emresult0)
1780
(booleanp deregwrite0) (booleanp emregwrite0)
1781
(booleanp mwregwrite0) (integerp mwdest0)
1782
(integerp deop0) (integerp fddest0)
1783
(integerp dedest0) (integerp op0) (integerp s0)
1784
(integerp a1) (integerp a2) (integerp d0)
1785
(integerp d1) (integerp x0) (integerp fdop0)
1786
(booleanp w0) (booleanp w1) (integerp fdsrc10)
1787
(integerp fdsrc20) (integerp emdest0)
1788
(integerp emval0) (integerp desrc10)
1789
(integerp desrc20) (integerp fdinst0)
1790
(integerp deimm0) (booleanp deuseimm0)
1791
(booleanp dememtoreg0) (booleanp emmemtoreg0)
1792
(integerp emimm0) (booleanp emuseimm0)
1793
(booleanp dememwrite0) (booleanp emmemwrite0)
1794
(integerp emarg20) (integerp ffinst0)
1795
(integerp mmval0) (integerp mmdest0)
1796
(booleanp mmregwrite0) (integerp mmresult0)
1797
(booleanp mmmemwrite0) (integerp mmarg20)
1798
(booleanp emis_alu_exception0)
1799
(booleanp mmis_alu_exception0)
1800
(booleanp mwis_alu_exception0)
1801
(booleanp deisreturnfromexception0)
1802
(booleanp emisreturnfromexception0)
1803
(booleanp mmisreturnfromexception0)
1804
(booleanp mwisreturnfromexception0))
1805
(let* ((st0 (initialize_a nil nil nil nil pc0 intrp0
1806
nil pc0 bpstate0 intrp0 pc0 intrp0
1807
bpstate0 ffbpstate0 ffpintrp0
1808
ffpredicteddirection0
1809
ffpredictedtarget0 ffinst0 ffppc0
1810
fdpintrp0 fdbpstate0 fdppc0 fdinst0
1811
fdpredicteddirection0
1812
fdpredictedtarget0 debpstate0
1813
depintrp0 deppc0 desrc10 desrc20 a1
1814
a2 dedest0 deop0 deimm0 deuseimm0
1815
deisreturnfromexception0 deregwrite0
1816
dememwrite0 dememtoreg0 deisbranch0
1817
depredicteddirection0
1818
depredictedtarget0 embpstate0
1819
empintrp0 emppc0 emis_alu_exception0
1820
emis_taken_branch0 emtargetpc0
1821
emarg20 emresult0 emdest0
1822
emisreturnfromexception0
1823
emmispredictedtaken0
1824
emmispredictednottaken0 emregwrite0
1825
emmemwrite0 emmemtoreg0 dmem0 epc0
1826
isexception0 mmbpstate0 mmpintrp0
1827
mmisreturnfromexception0
1828
mmis_alu_exception0 mmppc0 mmval0
1829
mmdest0 mmregwrite0 mwbpstate0
1830
mwpintrp0 mwisreturnfromexception0
1831
mwis_alu_exception0 mwppc0 mwval0
1832
mwdest0 mwregwrite0))
1833
(st1 (simulate_a st0 nil nil nil pc0 intrp0
1834
nil pc0 bpstate0 intrp0 pc0
1835
alu_exception_handler intrp0 bpstate0
1836
ffbpstate0 ffpintrp0
1837
ffpredicteddirection0
1838
ffpredictedtarget0 ffinst0 ffppc0
1839
fdpintrp0 fdbpstate0 fdppc0 fdinst0
1840
fdpredicteddirection0
1841
fdpredictedtarget0 debpstate0
1842
depintrp0 deppc0 desrc10 desrc20 a1
1843
a2 dedest0 deop0 deimm0 deuseimm0
1844
deisreturnfromexception0 deregwrite0
1845
dememwrite0 dememtoreg0 deisbranch0
1846
depredicteddirection0
1847
depredictedtarget0 embpstate0
1848
empintrp0 emppc0 emis_alu_exception0
1849
emis_taken_branch0 emtargetpc0
1850
emarg20 emresult0 emdest0
1851
emisreturnfromexception0
1852
emmispredictedtaken0
1853
emmispredictednottaken0 emregwrite0
1854
emmemwrite0 emmemtoreg0 dmem0 epc0
1855
isexception0 mmbpstate0 mmpintrp0
1856
mmisreturnfromexception0
1857
mmis_alu_exception0 mmppc0 mmval0
1858
mmdest0 mmregwrite0 mwbpstate0
1859
mwpintrp0 mwisreturnfromexception0
1860
mwis_alu_exception0 mwppc0 mwval0
1862
(g 'prf (g 'impl st0))
1863
(g 'pdmemhist_2 (g 'impl st0))))
1864
(st2 (simulate_a st1 nil nil nil pc0 intrp0
1865
nil pc0 bpstate0 intrp0 pc0
1866
alu_exception_handler intrp0 bpstate0
1867
ffbpstate0 ffpintrp0
1868
ffpredicteddirection0
1869
ffpredictedtarget0 ffinst0 ffppc0
1870
fdpintrp0 fdbpstate0 fdppc0 fdinst0
1871
fdpredicteddirection0
1872
fdpredictedtarget0 debpstate0
1873
depintrp0 deppc0 desrc10 desrc20 a1
1874
a2 dedest0 deop0 deimm0 deuseimm0
1875
deisreturnfromexception0 deregwrite0
1876
dememwrite0 dememtoreg0 deisbranch0
1877
depredicteddirection0
1878
depredictedtarget0 embpstate0
1879
empintrp0 emppc0 emis_alu_exception0
1880
emis_taken_branch0 emtargetpc0
1881
emarg20 emresult0 emdest0
1882
emisreturnfromexception0
1883
emmispredictedtaken0
1884
emmispredictednottaken0 emregwrite0
1885
emmemwrite0 emmemtoreg0 dmem0 epc0
1886
isexception0 mmbpstate0 mmpintrp0
1887
mmisreturnfromexception0
1888
mmis_alu_exception0 mmppc0 mmval0
1889
mmdest0 mmregwrite0 mwbpstate0
1890
mwpintrp0 mwisreturnfromexception0
1891
mwis_alu_exception0 mwppc0 mwval0
1893
(g 'prf (g 'impl st1))
1894
(g 'pdmemhist_2 (g 'impl st1))))
1895
(st3 (simulate_a st2 nil nil nil pc0 intrp0
1896
nil pc0 bpstate0 intrp0 pc0
1897
alu_exception_handler intrp0 bpstate0
1898
ffbpstate0 ffpintrp0
1899
ffpredicteddirection0
1900
ffpredictedtarget0 ffinst0 ffppc0
1901
fdpintrp0 fdbpstate0 fdppc0 fdinst0
1902
fdpredicteddirection0
1903
fdpredictedtarget0 debpstate0
1904
depintrp0 deppc0 desrc10 desrc20 a1
1905
a2 dedest0 deop0 deimm0 deuseimm0
1906
deisreturnfromexception0 deregwrite0
1907
dememwrite0 dememtoreg0 deisbranch0
1908
depredicteddirection0
1909
depredictedtarget0 embpstate0
1910
empintrp0 emppc0 emis_alu_exception0
1911
emis_taken_branch0 emtargetpc0
1912
emarg20 emresult0 emdest0
1913
emisreturnfromexception0
1914
emmispredictedtaken0
1915
emmispredictednottaken0 emregwrite0
1916
emmemwrite0 emmemtoreg0 dmem0 epc0
1917
isexception0 mmbpstate0 mmpintrp0
1918
mmisreturnfromexception0
1919
mmis_alu_exception0 mmppc0 mmval0
1920
mmdest0 mmregwrite0 mwbpstate0
1921
mwpintrp0 mwisreturnfromexception0
1922
mwis_alu_exception0 mwppc0 mwval0
1924
(g 'prf (g 'impl st2))
1925
(g 'pdmemhist_2 (g 'impl st2))))
1926
(st4 (simulate_a st3 nil nil nil pc0 intrp0
1927
nil pc0 bpstate0 intrp0 pc0
1928
alu_exception_handler intrp0 bpstate0
1929
ffbpstate0 ffpintrp0
1930
ffpredicteddirection0
1931
ffpredictedtarget0 ffinst0 ffppc0
1932
fdpintrp0 fdbpstate0 fdppc0 fdinst0
1933
fdpredicteddirection0
1934
fdpredictedtarget0 debpstate0
1935
depintrp0 deppc0 desrc10 desrc20 a1
1936
a2 dedest0 deop0 deimm0 deuseimm0
1937
deisreturnfromexception0 deregwrite0
1938
dememwrite0 dememtoreg0 deisbranch0
1939
depredicteddirection0
1940
depredictedtarget0 embpstate0
1941
empintrp0 emppc0 emis_alu_exception0
1942
emis_taken_branch0 emtargetpc0
1943
emarg20 emresult0 emdest0
1944
emisreturnfromexception0
1945
emmispredictedtaken0
1946
emmispredictednottaken0 emregwrite0
1947
emmemwrite0 emmemtoreg0 dmem0 epc0
1948
isexception0 mmbpstate0 mmpintrp0
1949
mmisreturnfromexception0
1950
mmis_alu_exception0 mmppc0 mmval0
1951
mmdest0 mmregwrite0 mwbpstate0
1952
mwpintrp0 mwisreturnfromexception0
1953
mwis_alu_exception0 mwppc0 mwval0
1955
(g 'prf (g 'impl st3))
1956
(g 'pdmemhist_2 (g 'impl st3))))
1957
(st5 (simulate_a st4 nil nil nil pc0 intrp0
1958
nil pc0 bpstate0 intrp0 pc0
1959
alu_exception_handler intrp0 bpstate0
1960
ffbpstate0 ffpintrp0
1961
ffpredicteddirection0
1962
ffpredictedtarget0 ffinst0 ffppc0
1963
fdpintrp0 fdbpstate0 fdppc0 fdinst0
1964
fdpredicteddirection0
1965
fdpredictedtarget0 debpstate0
1966
depintrp0 deppc0 desrc10 desrc20 a1
1967
a2 dedest0 deop0 deimm0 deuseimm0
1968
deisreturnfromexception0 deregwrite0
1969
dememwrite0 dememtoreg0 deisbranch0
1970
depredicteddirection0
1971
depredictedtarget0 embpstate0
1972
empintrp0 emppc0 emis_alu_exception0
1973
emis_taken_branch0 emtargetpc0
1974
emarg20 emresult0 emdest0
1975
emisreturnfromexception0
1976
emmispredictedtaken0
1977
emmispredictednottaken0 emregwrite0
1978
emmemwrite0 emmemtoreg0 dmem0 epc0
1979
isexception0 mmbpstate0 mmpintrp0
1980
mmisreturnfromexception0
1981
mmis_alu_exception0 mmppc0 mmval0
1982
mmdest0 mmregwrite0 mwbpstate0
1983
mwpintrp0 mwisreturnfromexception0
1984
mwis_alu_exception0 mwppc0 mwval0
1986
(g 'prf (g 'impl st4))
1987
(g 'pdmemhist_2 (g 'impl st4))))
1988
(st6 (simulate_a st5 nil nil nil pc0 intrp0
1989
nil pc0 bpstate0 intrp0 pc0
1990
alu_exception_handler intrp0 bpstate0
1991
ffbpstate0 ffpintrp0
1992
ffpredicteddirection0
1993
ffpredictedtarget0 ffinst0 ffppc0
1994
fdpintrp0 fdbpstate0 fdppc0 fdinst0
1995
fdpredicteddirection0
1996
fdpredictedtarget0 debpstate0
1997
depintrp0 deppc0 desrc10 desrc20 a1
1998
a2 dedest0 deop0 deimm0 deuseimm0
1999
deisreturnfromexception0 deregwrite0
2000
dememwrite0 dememtoreg0 deisbranch0
2001
depredicteddirection0
2002
depredictedtarget0 embpstate0
2003
empintrp0 emppc0 emis_alu_exception0
2004
emis_taken_branch0 emtargetpc0
2005
emarg20 emresult0 emdest0
2006
emisreturnfromexception0
2007
emmispredictedtaken0
2008
emmispredictednottaken0 emregwrite0
2009
emmemwrite0 emmemtoreg0 dmem0 epc0
2010
isexception0 mmbpstate0 mmpintrp0
2011
mmisreturnfromexception0
2012
mmis_alu_exception0 mmppc0 mmval0
2013
mmdest0 mmregwrite0 mwbpstate0
2014
mwpintrp0 mwisreturnfromexception0
2015
mwis_alu_exception0 mwppc0 mwval0
2017
(g 'prf (g 'impl st5))
2018
(g 'pdmemhist_2 (g 'impl st5))))
2019
(st7 (simulate_a st6 nil nil nil pc0 intrp0
2020
nil pc0 bpstate0 intrp0 pc0
2021
alu_exception_handler intrp0 bpstate0
2022
ffbpstate0 ffpintrp0
2023
ffpredicteddirection0
2024
ffpredictedtarget0 ffinst0 ffppc0
2025
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2026
fdpredicteddirection0
2027
fdpredictedtarget0 debpstate0
2028
depintrp0 deppc0 desrc10 desrc20 a1
2029
a2 dedest0 deop0 deimm0 deuseimm0
2030
deisreturnfromexception0 deregwrite0
2031
dememwrite0 dememtoreg0 deisbranch0
2032
depredicteddirection0
2033
depredictedtarget0 embpstate0
2034
empintrp0 emppc0 emis_alu_exception0
2035
emis_taken_branch0 emtargetpc0
2036
emarg20 emresult0 emdest0
2037
emisreturnfromexception0
2038
emmispredictedtaken0
2039
emmispredictednottaken0 emregwrite0
2040
emmemwrite0 emmemtoreg0 dmem0 epc0
2041
isexception0 mmbpstate0 mmpintrp0
2042
mmisreturnfromexception0
2043
mmis_alu_exception0 mmppc0 mmval0
2044
mmdest0 mmregwrite0 mwbpstate0
2045
mwpintrp0 mwisreturnfromexception0
2046
mwis_alu_exception0 mwppc0 mwval0
2048
(g 'prf (g 'impl st6))
2049
(g 'pdmemhist_2 (g 'impl st6))))
2050
(ppc_v (g 'ppc (g 'impl st7)))
2051
(prf_v (g 'prf (g 'impl st7)))
2052
(pdmem_v (g 'pdmem (g 'impl st7)))
2053
(pimem_v (g 'pimem (g 'impl st7)))
2054
(deop_v (g 'deop (g 'impl st7)))
2055
(desrc2_v (g 'desrc2 (g 'impl st7)))
2056
(dearg1_v (g 'dearg1 (g 'impl st7)))
2057
(dearg2_v (g 'dearg2 (g 'impl st7)))
2058
(dedest_v (g 'dedest (g 'impl st7)))
2059
(dewrt_v (g 'dewrt (g 'impl st7)))
2060
(fdwrt_v (g 'fdwrt (g 'impl st7)))
2061
(fdinst_v (g 'fdinst (g 'impl st7)))
2062
(emdest_v (g 'emdest (g 'impl st7)))
2063
(emwrt_v (g 'emwrt (g 'impl st7)))
2064
(desrc1_v (g 'desrc1 (g 'impl st7)))
2065
(desrc2_v (g 'desrc2 (g 'impl st7)))
2066
(deregwrite_v (g 'deregwrite (g 'impl st7)))
2067
(emregwrite_v (g 'emregwrite (g 'impl st7)))
2068
(deimm_v (g 'deimm (g 'impl st7)))
2069
(deuseimm_v (g 'deuseimm (g 'impl st7)))
2070
(emresult_v (g 'emresult (g 'impl st7)))
2071
(dememtoreg_v (g 'dememtoreg (g 'impl st7)))
2072
(emmemtoreg_v (g 'emmemtoreg (g 'impl st7)))
2073
(dememwrite_v (g 'dememwrite (g 'impl st7)))
2074
(emmemwrite_v (g 'emmemwrite (g 'impl st7)))
2075
(emarg2_v (g 'emarg2 (g 'impl st7)))
2076
(ffwrt_v (g 'ffwrt (g 'impl st7)))
2077
(ffinst_v (g 'ffinst (g 'impl st7)))
2078
(mmval_v (g 'mmval (g 'impl st7)))
2079
(mmdest_v (g 'mmdest (g 'impl st7)))
2080
(mmwrt_v (g 'mmwrt (g 'impl st7)))
2081
(mmregwrite_v (g 'mmregwrite (g 'impl st7)))
2082
(mwval_v (g 'mwval (g 'impl st7)))
2083
(mwdest_v (g 'mwdest (g 'impl st7)))
2084
(mwwrt_v (g 'mwwrt (g 'impl st7)))
2085
(mwregwrite_v (g 'mwregwrite (g 'impl st7)))
2086
(deisbranch_v (g 'deisbranch (g 'impl st7)))
2087
(emis_taken_branch_v
2088
(g 'emis_taken_branch (g 'impl st7)))
2089
(emtargetpc_v (g 'emtargetpc (g 'impl st7)))
2090
(ffppc_v (g 'ffppc (g 'impl st7)))
2091
(fdppc_v (g 'fdppc (g 'impl st7)))
2092
(deppc_v (g 'deppc (g 'impl st7)))
2093
(emis_alu_exception_v
2094
(g 'emis_alu_exception (g 'impl st7)))
2095
(mmis_alu_exception_v
2096
(g 'mmis_alu_exception (g 'impl st7)))
2097
(mwis_alu_exception_v
2098
(g 'mwis_alu_exception (g 'impl st7)))
2099
(deisreturnfromexception_v
2100
(g 'deisreturnfromexception (g 'impl st7)))
2101
(mmisreturnfromexception_v
2102
(g 'mmisreturnfromexception (g 'impl st7)))
2103
(mwisreturnfromexception_v
2104
(g 'mwisreturnfromexception (g 'impl st7)))
2105
(emisreturnfromexception_v
2106
(g 'emisreturnfromexception (g 'impl st7)))
2107
(mmisreturnfromexception_v
2108
(g 'mmisreturnfromexception (g 'impl st7)))
2109
(mwisreturnfromexception_v
2110
(g 'mwisreturnfromexception (g 'impl st7)))
2111
(pepc_v (g 'pepc (g 'impl st7)))
2113
(g 'pisexception (g 'impl st7)))
2114
(i_pc0 (committedpc (g 'mwwrt (g 'impl st7))
2115
(g 'mwppc (g 'impl st7))
2116
(g 'mmwrt (g 'impl st7))
2117
(g 'mmppc (g 'impl st7))
2118
(g 'emwrt (g 'impl st7))
2119
(g 'emppc (g 'impl st7))
2120
(g 'dewrt (g 'impl st7))
2121
(g 'deppc (g 'impl st7))
2122
(g 'fdwrt (g 'impl st7))
2123
(g 'fdppc (g 'impl st7))
2124
(g 'ffwrt (g 'impl st7))
2125
(g 'ffppc (g 'impl st7))
2126
(g 'ppc (g 'impl st7))))
2127
(st8 (simulate_a st7 nil nil nil pc0 intrp0 t
2128
i_pc0 committedbpstate committedintrp
2129
pc0 alu_exception_handler intrp0
2130
bpstate0 ffbpstate0 ffpintrp0
2131
ffpredicteddirection0
2132
ffpredictedtarget0 ffinst0 ffppc0
2133
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2134
fdpredicteddirection0
2135
fdpredictedtarget0 debpstate0
2136
depintrp0 deppc0 desrc10 desrc20 a1
2137
a2 dedest0 deop0 deimm0 deuseimm0
2138
deisreturnfromexception0 deregwrite0
2139
dememwrite0 dememtoreg0 deisbranch0
2140
depredicteddirection0
2141
depredictedtarget0 embpstate0
2142
empintrp0 emppc0 emis_alu_exception0
2143
emis_taken_branch0 emtargetpc0
2144
emarg20 emresult0 emdest0
2145
emisreturnfromexception0
2146
emmispredictedtaken0
2147
emmispredictednottaken0 emregwrite0
2148
emmemwrite0 emmemtoreg0 dmem0 epc0
2149
isexception0 mmbpstate0 mmpintrp0
2150
mmisreturnfromexception0
2151
mmis_alu_exception0 mmppc0 mmval0
2152
mmdest0 mmregwrite0 mwbpstate0
2153
mwpintrp0 mwisreturnfromexception0
2154
mwis_alu_exception0 mwppc0 mwval0
2156
(g 'prf (g 'impl st7))
2157
(g 'pdmemhist_2 (g 'impl st7))))
2159
(equiv_ma ppc_v (g 'ppc (g 'impl st8))
2160
prf_v a1 (g 'prf (g 'impl st8))
2161
pimem_v (g 'pimem (g 'impl st8))
2162
pdmem_v (g 'pdmem (g 'impl st8))
2163
pepc_v (g 'pepc (g 'impl st8))
2165
(g 'pisexception (g 'impl st8))
2166
ffwrt_v (g 'ffwrt (g 'impl st8))
2167
ffppc_v (g 'ffppc (g 'impl st8))
2168
ffinst_v (g 'ffinst (g 'impl st8))
2169
fdwrt_v (g 'fdwrt (g 'impl st8))
2170
fdppc_v (g 'fdppc (g 'impl st8))
2171
fdinst_v (g 'fdinst (g 'impl st8))
2172
dewrt_v (g 'dewrt (g 'impl st8))
2173
deppc_v (g 'deppc (g 'impl st8))
2174
deop_v (g 'deop (g 'impl st8))
2175
dearg1_v (g 'dearg1 (g 'impl st8))
2176
dearg2_v (g 'dearg2 (g 'impl st8))
2177
dedest_v (g 'dedest (g 'impl st8))
2178
desrc1_v (g 'desrc1 (g 'impl st8))
2179
desrc2_v (g 'desrc2 (g 'impl st8))
2180
deimm_v (g 'deimm (g 'impl st8))
2181
deuseimm_v (g 'deuseimm (g 'impl st8))
2183
(g 'deisbranch (g 'impl st8))
2185
(g 'dememtoreg (g 'impl st8))
2187
(g 'dememwrite (g 'impl st8))
2188
deisreturnfromexception_v
2189
(g 'deisreturnfromexception
2192
(g 'deregwrite (g 'impl st8)) emwrt_v
2193
(g 'emwrt (g 'impl st8)) emtargetpc_v
2194
(g 'emtargetpc (g 'impl st8)) emdest_v
2195
(g 'emdest (g 'impl st8)) emarg2_v
2196
(g 'emarg2 (g 'impl st8)) emregwrite_v
2197
(g 'emregwrite (g 'impl st8))
2198
emresult_v (g 'emresult (g 'impl st8))
2200
(g 'emis_taken_branch (g 'impl st8))
2202
(g 'emmemtoreg (g 'impl st8))
2203
emis_alu_exception_v
2204
(g 'emis_alu_exception (g 'impl st8))
2205
emisreturnfromexception_v
2206
(g 'emisreturnfromexception
2209
(g 'emmemwrite (g 'impl st8)) mmwrt_v
2210
(g 'mmwrt (g 'impl st8)) mmval_v
2211
(g 'mmval (g 'impl st8)) mmdest_v
2212
(g 'mmdest (g 'impl st8)) mmregwrite_v
2213
(g 'mmregwrite (g 'impl st8))
2214
mmisreturnfromexception_v
2215
(g 'mmisreturnfromexception
2217
mmis_alu_exception_v
2218
(g 'mmis_alu_exception (g 'impl st8))
2219
mwwrt_v (g 'mwwrt (g 'impl st8))
2220
mwval_v (g 'mwval (g 'impl st8))
2221
mwdest_v (g 'mwdest (g 'impl st8))
2223
(g 'mwregwrite (g 'impl st8))
2224
mwisreturnfromexception_v
2225
(g 'mwisreturnfromexception
2227
mwis_alu_exception_v
2228
(g 'mwis_alu_exception (g 'impl st8))))
2229
(st9 (simulate_a st8 nil nil nil pc0 intrp0
2230
nil pc0 bpstate0 intrp0 pc0
2231
alu_exception_handler intrp0 bpstate0
2232
ffbpstate0 ffpintrp0
2233
ffpredicteddirection0
2234
ffpredictedtarget0 ffinst0 ffppc0
2235
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2236
fdpredicteddirection0
2237
fdpredictedtarget0 debpstate0
2238
depintrp0 deppc0 desrc10 desrc20 a1
2239
a2 dedest0 deop0 deimm0 deuseimm0
2240
deisreturnfromexception0 deregwrite0
2241
dememwrite0 dememtoreg0 deisbranch0
2242
depredicteddirection0
2243
depredictedtarget0 embpstate0
2244
empintrp0 emppc0 emis_alu_exception0
2245
emis_taken_branch0 emtargetpc0
2246
emarg20 emresult0 emdest0
2247
emisreturnfromexception0
2248
emmispredictedtaken0
2249
emmispredictednottaken0 emregwrite0
2250
emmemwrite0 emmemtoreg0 dmem0 epc0
2251
isexception0 mmbpstate0 mmpintrp0
2252
mmisreturnfromexception0
2253
mmis_alu_exception0 mmppc0 mmval0
2254
mmdest0 mmregwrite0 mwbpstate0
2255
mwpintrp0 mwisreturnfromexception0
2256
mwis_alu_exception0 mwppc0 mwval0
2258
(g 'prf (g 'impl st8))
2259
(g 'pdmemhist_2 (g 'impl st8))))
2261
(equiv_ma ppc_v (g 'ppc (g 'impl st9))
2262
prf_v a1 (g 'prf (g 'impl st9))
2263
pimem_v (g 'pimem (g 'impl st9))
2264
pdmem_v (g 'pdmem (g 'impl st9))
2265
pepc_v (g 'pepc (g 'impl st9))
2267
(g 'pisexception (g 'impl st9))
2268
ffwrt_v (g 'ffwrt (g 'impl st9))
2269
ffppc_v (g 'ffppc (g 'impl st9))
2270
ffinst_v (g 'ffinst (g 'impl st9))
2271
fdwrt_v (g 'fdwrt (g 'impl st9))
2272
fdppc_v (g 'fdppc (g 'impl st9))
2273
fdinst_v (g 'fdinst (g 'impl st9))
2274
dewrt_v (g 'dewrt (g 'impl st9))
2275
deppc_v (g 'deppc (g 'impl st9))
2276
deop_v (g 'deop (g 'impl st9))
2277
dearg1_v (g 'dearg1 (g 'impl st9))
2278
dearg2_v (g 'dearg2 (g 'impl st9))
2279
dedest_v (g 'dedest (g 'impl st9))
2280
desrc1_v (g 'desrc1 (g 'impl st9))
2281
desrc2_v (g 'desrc2 (g 'impl st9))
2282
deimm_v (g 'deimm (g 'impl st9))
2283
deuseimm_v (g 'deuseimm (g 'impl st9))
2285
(g 'deisbranch (g 'impl st9))
2287
(g 'dememtoreg (g 'impl st9))
2289
(g 'dememwrite (g 'impl st9))
2290
deisreturnfromexception_v
2291
(g 'deisreturnfromexception
2294
(g 'deregwrite (g 'impl st9)) emwrt_v
2295
(g 'emwrt (g 'impl st9)) emtargetpc_v
2296
(g 'emtargetpc (g 'impl st9)) emdest_v
2297
(g 'emdest (g 'impl st9)) emarg2_v
2298
(g 'emarg2 (g 'impl st9)) emregwrite_v
2299
(g 'emregwrite (g 'impl st9))
2300
emresult_v (g 'emresult (g 'impl st9))
2302
(g 'emis_taken_branch (g 'impl st9))
2304
(g 'emmemtoreg (g 'impl st9))
2305
emis_alu_exception_v
2306
(g 'emis_alu_exception (g 'impl st9))
2307
emisreturnfromexception_v
2308
(g 'emisreturnfromexception
2311
(g 'emmemwrite (g 'impl st9)) mmwrt_v
2312
(g 'mmwrt (g 'impl st9)) mmval_v
2313
(g 'mmval (g 'impl st9)) mmdest_v
2314
(g 'mmdest (g 'impl st9)) mmregwrite_v
2315
(g 'mmregwrite (g 'impl st9))
2316
mmisreturnfromexception_v
2317
(g 'mmisreturnfromexception
2319
mmis_alu_exception_v
2320
(g 'mmis_alu_exception (g 'impl st9))
2321
mwwrt_v (g 'mwwrt (g 'impl st9))
2322
mwval_v (g 'mwval (g 'impl st9))
2323
mwdest_v (g 'mwdest (g 'impl st9))
2325
(g 'mwregwrite (g 'impl st9))
2326
mwisreturnfromexception_v
2327
(g 'mwisreturnfromexception
2329
mwis_alu_exception_v
2330
(g 'mwis_alu_exception (g 'impl st9))))
2331
(st10 (simulate_a st9 nil nil nil pc0 intrp0
2332
nil pc0 bpstate0 intrp0 pc0
2333
alu_exception_handler intrp0
2334
bpstate0 ffbpstate0 ffpintrp0
2335
ffpredicteddirection0
2336
ffpredictedtarget0 ffinst0 ffppc0
2337
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2338
fdpredicteddirection0
2339
fdpredictedtarget0 debpstate0
2340
depintrp0 deppc0 desrc10 desrc20 a1
2341
a2 dedest0 deop0 deimm0 deuseimm0
2342
deisreturnfromexception0 deregwrite0
2343
dememwrite0 dememtoreg0 deisbranch0
2344
depredicteddirection0
2345
depredictedtarget0 embpstate0
2346
empintrp0 emppc0 emis_alu_exception0
2347
emis_taken_branch0 emtargetpc0
2348
emarg20 emresult0 emdest0
2349
emisreturnfromexception0
2350
emmispredictedtaken0
2351
emmispredictednottaken0 emregwrite0
2352
emmemwrite0 emmemtoreg0 dmem0 epc0
2353
isexception0 mmbpstate0 mmpintrp0
2354
mmisreturnfromexception0
2355
mmis_alu_exception0 mmppc0 mmval0
2356
mmdest0 mmregwrite0 mwbpstate0
2357
mwpintrp0 mwisreturnfromexception0
2358
mwis_alu_exception0 mwppc0 mwval0
2360
(g 'prf (g 'impl st9))
2361
(g 'pdmemhist_2 (g 'impl st9))))
2363
(equiv_ma ppc_v (g 'ppc (g 'impl st10))
2364
prf_v a1 (g 'prf (g 'impl st10))
2365
pimem_v (g 'pimem (g 'impl st10))
2366
pdmem_v (g 'pdmem (g 'impl st10))
2367
pepc_v (g 'pepc (g 'impl st10))
2369
(g 'pisexception (g 'impl st10))
2370
ffwrt_v (g 'ffwrt (g 'impl st10))
2371
ffppc_v (g 'ffppc (g 'impl st10))
2372
ffinst_v (g 'ffinst (g 'impl st10))
2373
fdwrt_v (g 'fdwrt (g 'impl st10))
2374
fdppc_v (g 'fdppc (g 'impl st10))
2375
fdinst_v (g 'fdinst (g 'impl st10))
2376
dewrt_v (g 'dewrt (g 'impl st10))
2377
deppc_v (g 'deppc (g 'impl st10))
2378
deop_v (g 'deop (g 'impl st10))
2379
dearg1_v (g 'dearg1 (g 'impl st10))
2380
dearg2_v (g 'dearg2 (g 'impl st10))
2381
dedest_v (g 'dedest (g 'impl st10))
2382
desrc1_v (g 'desrc1 (g 'impl st10))
2383
desrc2_v (g 'desrc2 (g 'impl st10))
2384
deimm_v (g 'deimm (g 'impl st10))
2386
(g 'deuseimm (g 'impl st10))
2388
(g 'deisbranch (g 'impl st10))
2390
(g 'dememtoreg (g 'impl st10))
2392
(g 'dememwrite (g 'impl st10))
2393
deisreturnfromexception_v
2394
(g 'deisreturnfromexception
2397
(g 'deregwrite (g 'impl st10)) emwrt_v
2398
(g 'emwrt (g 'impl st10)) emtargetpc_v
2399
(g 'emtargetpc (g 'impl st10))
2400
emdest_v (g 'emdest (g 'impl st10))
2401
emarg2_v (g 'emarg2 (g 'impl st10))
2403
(g 'emregwrite (g 'impl st10))
2405
(g 'emresult (g 'impl st10))
2407
(g 'emis_taken_branch (g 'impl st10))
2409
(g 'emmemtoreg (g 'impl st10))
2410
emis_alu_exception_v
2411
(g 'emis_alu_exception (g 'impl st10))
2412
emisreturnfromexception_v
2413
(g 'emisreturnfromexception
2416
(g 'emmemwrite (g 'impl st10)) mmwrt_v
2417
(g 'mmwrt (g 'impl st10)) mmval_v
2418
(g 'mmval (g 'impl st10)) mmdest_v
2419
(g 'mmdest (g 'impl st10))
2421
(g 'mmregwrite (g 'impl st10))
2422
mmisreturnfromexception_v
2423
(g 'mmisreturnfromexception
2425
mmis_alu_exception_v
2426
(g 'mmis_alu_exception (g 'impl st10))
2427
mwwrt_v (g 'mwwrt (g 'impl st10))
2428
mwval_v (g 'mwval (g 'impl st10))
2429
mwdest_v (g 'mwdest (g 'impl st10))
2431
(g 'mwregwrite (g 'impl st10))
2432
mwisreturnfromexception_v
2433
(g 'mwisreturnfromexception
2435
mwis_alu_exception_v
2436
(g 'mwis_alu_exception (g 'impl st10))))
2437
(st11 (simulate_a st10 nil nil nil pc0 intrp0
2438
nil pc0 bpstate0 intrp0 pc0
2439
alu_exception_handler intrp0
2440
bpstate0 ffbpstate0 ffpintrp0
2441
ffpredicteddirection0
2442
ffpredictedtarget0 ffinst0 ffppc0
2443
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2444
fdpredicteddirection0
2445
fdpredictedtarget0 debpstate0
2446
depintrp0 deppc0 desrc10 desrc20 a1
2447
a2 dedest0 deop0 deimm0 deuseimm0
2448
deisreturnfromexception0 deregwrite0
2449
dememwrite0 dememtoreg0 deisbranch0
2450
depredicteddirection0
2451
depredictedtarget0 embpstate0
2452
empintrp0 emppc0 emis_alu_exception0
2453
emis_taken_branch0 emtargetpc0
2454
emarg20 emresult0 emdest0
2455
emisreturnfromexception0
2456
emmispredictedtaken0
2457
emmispredictednottaken0 emregwrite0
2458
emmemwrite0 emmemtoreg0 dmem0 epc0
2459
isexception0 mmbpstate0 mmpintrp0
2460
mmisreturnfromexception0
2461
mmis_alu_exception0 mmppc0 mmval0
2462
mmdest0 mmregwrite0 mwbpstate0
2463
mwpintrp0 mwisreturnfromexception0
2464
mwis_alu_exception0 mwppc0 mwval0
2466
(g 'prf (g 'impl st10))
2467
(g 'pdmemhist_2 (g 'impl st10))))
2469
(equiv_ma ppc_v (g 'ppc (g 'impl st11))
2470
prf_v a1 (g 'prf (g 'impl st11))
2471
pimem_v (g 'pimem (g 'impl st11))
2472
pdmem_v (g 'pdmem (g 'impl st11))
2473
pepc_v (g 'pepc (g 'impl st11))
2475
(g 'pisexception (g 'impl st11))
2476
ffwrt_v (g 'ffwrt (g 'impl st11))
2477
ffppc_v (g 'ffppc (g 'impl st11))
2478
ffinst_v (g 'ffinst (g 'impl st11))
2479
fdwrt_v (g 'fdwrt (g 'impl st11))
2480
fdppc_v (g 'fdppc (g 'impl st11))
2481
fdinst_v (g 'fdinst (g 'impl st11))
2482
dewrt_v (g 'dewrt (g 'impl st11))
2483
deppc_v (g 'deppc (g 'impl st11))
2484
deop_v (g 'deop (g 'impl st11))
2485
dearg1_v (g 'dearg1 (g 'impl st11))
2486
dearg2_v (g 'dearg2 (g 'impl st11))
2487
dedest_v (g 'dedest (g 'impl st11))
2488
desrc1_v (g 'desrc1 (g 'impl st11))
2489
desrc2_v (g 'desrc2 (g 'impl st11))
2490
deimm_v (g 'deimm (g 'impl st11))
2492
(g 'deuseimm (g 'impl st11))
2494
(g 'deisbranch (g 'impl st11))
2496
(g 'dememtoreg (g 'impl st11))
2498
(g 'dememwrite (g 'impl st11))
2499
deisreturnfromexception_v
2500
(g 'deisreturnfromexception
2503
(g 'deregwrite (g 'impl st11)) emwrt_v
2504
(g 'emwrt (g 'impl st11)) emtargetpc_v
2505
(g 'emtargetpc (g 'impl st11))
2506
emdest_v (g 'emdest (g 'impl st11))
2507
emarg2_v (g 'emarg2 (g 'impl st11))
2509
(g 'emregwrite (g 'impl st11))
2511
(g 'emresult (g 'impl st11))
2513
(g 'emis_taken_branch (g 'impl st11))
2515
(g 'emmemtoreg (g 'impl st11))
2516
emis_alu_exception_v
2517
(g 'emis_alu_exception (g 'impl st11))
2518
emisreturnfromexception_v
2519
(g 'emisreturnfromexception
2522
(g 'emmemwrite (g 'impl st11)) mmwrt_v
2523
(g 'mmwrt (g 'impl st11)) mmval_v
2524
(g 'mmval (g 'impl st11)) mmdest_v
2525
(g 'mmdest (g 'impl st11))
2527
(g 'mmregwrite (g 'impl st11))
2528
mmisreturnfromexception_v
2529
(g 'mmisreturnfromexception
2531
mmis_alu_exception_v
2532
(g 'mmis_alu_exception (g 'impl st11))
2533
mwwrt_v (g 'mwwrt (g 'impl st11))
2534
mwval_v (g 'mwval (g 'impl st11))
2535
mwdest_v (g 'mwdest (g 'impl st11))
2537
(g 'mwregwrite (g 'impl st11))
2538
mwisreturnfromexception_v
2539
(g 'mwisreturnfromexception
2541
mwis_alu_exception_v
2542
(g 'mwis_alu_exception (g 'impl st11))))
2543
(st12 (simulate_a st11 nil nil nil pc0 intrp0
2544
nil pc0 bpstate0 intrp0 pc0
2545
alu_exception_handler intrp0
2546
bpstate0 ffbpstate0 ffpintrp0
2547
ffpredicteddirection0
2548
ffpredictedtarget0 ffinst0 ffppc0
2549
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2550
fdpredicteddirection0
2551
fdpredictedtarget0 debpstate0
2552
depintrp0 deppc0 desrc10 desrc20 a1
2553
a2 dedest0 deop0 deimm0 deuseimm0
2554
deisreturnfromexception0 deregwrite0
2555
dememwrite0 dememtoreg0 deisbranch0
2556
depredicteddirection0
2557
depredictedtarget0 embpstate0
2558
empintrp0 emppc0 emis_alu_exception0
2559
emis_taken_branch0 emtargetpc0
2560
emarg20 emresult0 emdest0
2561
emisreturnfromexception0
2562
emmispredictedtaken0
2563
emmispredictednottaken0 emregwrite0
2564
emmemwrite0 emmemtoreg0 dmem0 epc0
2565
isexception0 mmbpstate0 mmpintrp0
2566
mmisreturnfromexception0
2567
mmis_alu_exception0 mmppc0 mmval0
2568
mmdest0 mmregwrite0 mwbpstate0
2569
mwpintrp0 mwisreturnfromexception0
2570
mwis_alu_exception0 mwppc0 mwval0
2572
(g 'prf (g 'impl st11))
2573
(g 'pdmemhist_2 (g 'impl st11))))
2575
(equiv_ma ppc_v (g 'ppc (g 'impl st12))
2576
prf_v a1 (g 'prf (g 'impl st12))
2577
pimem_v (g 'pimem (g 'impl st12))
2578
pdmem_v (g 'pdmem (g 'impl st12))
2579
pepc_v (g 'pepc (g 'impl st12))
2581
(g 'pisexception (g 'impl st12))
2582
ffwrt_v (g 'ffwrt (g 'impl st12))
2583
ffppc_v (g 'ffppc (g 'impl st12))
2584
ffinst_v (g 'ffinst (g 'impl st12))
2585
fdwrt_v (g 'fdwrt (g 'impl st12))
2586
fdppc_v (g 'fdppc (g 'impl st12))
2587
fdinst_v (g 'fdinst (g 'impl st12))
2588
dewrt_v (g 'dewrt (g 'impl st12))
2589
deppc_v (g 'deppc (g 'impl st12))
2590
deop_v (g 'deop (g 'impl st12))
2591
dearg1_v (g 'dearg1 (g 'impl st12))
2592
dearg2_v (g 'dearg2 (g 'impl st12))
2593
dedest_v (g 'dedest (g 'impl st12))
2594
desrc1_v (g 'desrc1 (g 'impl st12))
2595
desrc2_v (g 'desrc2 (g 'impl st12))
2596
deimm_v (g 'deimm (g 'impl st12))
2598
(g 'deuseimm (g 'impl st12))
2600
(g 'deisbranch (g 'impl st12))
2602
(g 'dememtoreg (g 'impl st12))
2604
(g 'dememwrite (g 'impl st12))
2605
deisreturnfromexception_v
2606
(g 'deisreturnfromexception
2609
(g 'deregwrite (g 'impl st12)) emwrt_v
2610
(g 'emwrt (g 'impl st12)) emtargetpc_v
2611
(g 'emtargetpc (g 'impl st12))
2612
emdest_v (g 'emdest (g 'impl st12))
2613
emarg2_v (g 'emarg2 (g 'impl st12))
2615
(g 'emregwrite (g 'impl st12))
2617
(g 'emresult (g 'impl st12))
2619
(g 'emis_taken_branch (g 'impl st12))
2621
(g 'emmemtoreg (g 'impl st12))
2622
emis_alu_exception_v
2623
(g 'emis_alu_exception (g 'impl st12))
2624
emisreturnfromexception_v
2625
(g 'emisreturnfromexception
2628
(g 'emmemwrite (g 'impl st12)) mmwrt_v
2629
(g 'mmwrt (g 'impl st12)) mmval_v
2630
(g 'mmval (g 'impl st12)) mmdest_v
2631
(g 'mmdest (g 'impl st12))
2633
(g 'mmregwrite (g 'impl st12))
2634
mmisreturnfromexception_v
2635
(g 'mmisreturnfromexception
2637
mmis_alu_exception_v
2638
(g 'mmis_alu_exception (g 'impl st12))
2639
mwwrt_v (g 'mwwrt (g 'impl st12))
2640
mwval_v (g 'mwval (g 'impl st12))
2641
mwdest_v (g 'mwdest (g 'impl st12))
2643
(g 'mwregwrite (g 'impl st12))
2644
mwisreturnfromexception_v
2645
(g 'mwisreturnfromexception
2647
mwis_alu_exception_v
2648
(g 'mwis_alu_exception (g 'impl st12))))
2649
(st13 (simulate_a st12 nil nil nil pc0 intrp0
2650
nil pc0 bpstate0 intrp0 pc0
2651
alu_exception_handler intrp0
2652
bpstate0 ffbpstate0 ffpintrp0
2653
ffpredicteddirection0
2654
ffpredictedtarget0 ffinst0 ffppc0
2655
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2656
fdpredicteddirection0
2657
fdpredictedtarget0 debpstate0
2658
depintrp0 deppc0 desrc10 desrc20 a1
2659
a2 dedest0 deop0 deimm0 deuseimm0
2660
deisreturnfromexception0 deregwrite0
2661
dememwrite0 dememtoreg0 deisbranch0
2662
depredicteddirection0
2663
depredictedtarget0 embpstate0
2664
empintrp0 emppc0 emis_alu_exception0
2665
emis_taken_branch0 emtargetpc0
2666
emarg20 emresult0 emdest0
2667
emisreturnfromexception0
2668
emmispredictedtaken0
2669
emmispredictednottaken0 emregwrite0
2670
emmemwrite0 emmemtoreg0 dmem0 epc0
2671
isexception0 mmbpstate0 mmpintrp0
2672
mmisreturnfromexception0
2673
mmis_alu_exception0 mmppc0 mmval0
2674
mmdest0 mmregwrite0 mwbpstate0
2675
mwpintrp0 mwisreturnfromexception0
2676
mwis_alu_exception0 mwppc0 mwval0
2678
(g 'prf (g 'impl st12))
2679
(g 'pdmemhist_2 (g 'impl st12))))
2681
(equiv_ma ppc_v (g 'ppc (g 'impl st13))
2682
prf_v a1 (g 'prf (g 'impl st13))
2683
pimem_v (g 'pimem (g 'impl st13))
2684
pdmem_v (g 'pdmem (g 'impl st13))
2685
pepc_v (g 'pepc (g 'impl st13))
2687
(g 'pisexception (g 'impl st13))
2688
ffwrt_v (g 'ffwrt (g 'impl st13))
2689
ffppc_v (g 'ffppc (g 'impl st13))
2690
ffinst_v (g 'ffinst (g 'impl st13))
2691
fdwrt_v (g 'fdwrt (g 'impl st13))
2692
fdppc_v (g 'fdppc (g 'impl st13))
2693
fdinst_v (g 'fdinst (g 'impl st13))
2694
dewrt_v (g 'dewrt (g 'impl st13))
2695
deppc_v (g 'deppc (g 'impl st13))
2696
deop_v (g 'deop (g 'impl st13))
2697
dearg1_v (g 'dearg1 (g 'impl st13))
2698
dearg2_v (g 'dearg2 (g 'impl st13))
2699
dedest_v (g 'dedest (g 'impl st13))
2700
desrc1_v (g 'desrc1 (g 'impl st13))
2701
desrc2_v (g 'desrc2 (g 'impl st13))
2702
deimm_v (g 'deimm (g 'impl st13))
2704
(g 'deuseimm (g 'impl st13))
2706
(g 'deisbranch (g 'impl st13))
2708
(g 'dememtoreg (g 'impl st13))
2710
(g 'dememwrite (g 'impl st13))
2711
deisreturnfromexception_v
2712
(g 'deisreturnfromexception
2715
(g 'deregwrite (g 'impl st13)) emwrt_v
2716
(g 'emwrt (g 'impl st13)) emtargetpc_v
2717
(g 'emtargetpc (g 'impl st13))
2718
emdest_v (g 'emdest (g 'impl st13))
2719
emarg2_v (g 'emarg2 (g 'impl st13))
2721
(g 'emregwrite (g 'impl st13))
2723
(g 'emresult (g 'impl st13))
2725
(g 'emis_taken_branch (g 'impl st13))
2727
(g 'emmemtoreg (g 'impl st13))
2728
emis_alu_exception_v
2729
(g 'emis_alu_exception (g 'impl st13))
2730
emisreturnfromexception_v
2731
(g 'emisreturnfromexception
2734
(g 'emmemwrite (g 'impl st13)) mmwrt_v
2735
(g 'mmwrt (g 'impl st13)) mmval_v
2736
(g 'mmval (g 'impl st13)) mmdest_v
2737
(g 'mmdest (g 'impl st13))
2739
(g 'mmregwrite (g 'impl st13))
2740
mmisreturnfromexception_v
2741
(g 'mmisreturnfromexception
2743
mmis_alu_exception_v
2744
(g 'mmis_alu_exception (g 'impl st13))
2745
mwwrt_v (g 'mwwrt (g 'impl st13))
2746
mwval_v (g 'mwval (g 'impl st13))
2747
mwdest_v (g 'mwdest (g 'impl st13))
2749
(g 'mwregwrite (g 'impl st13))
2750
mwisreturnfromexception_v
2751
(g 'mwisreturnfromexception
2753
mwis_alu_exception_v
2754
(g 'mwis_alu_exception (g 'impl st13))))
2755
(st14 (simulate_a st13 nil nil nil pc0 intrp0
2756
nil pc0 bpstate0 intrp0 pc0
2757
alu_exception_handler intrp0
2758
bpstate0 ffbpstate0 ffpintrp0
2759
ffpredicteddirection0
2760
ffpredictedtarget0 ffinst0 ffppc0
2761
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2762
fdpredicteddirection0
2763
fdpredictedtarget0 debpstate0
2764
depintrp0 deppc0 desrc10 desrc20 a1
2765
a2 dedest0 deop0 deimm0 deuseimm0
2766
deisreturnfromexception0 deregwrite0
2767
dememwrite0 dememtoreg0 deisbranch0
2768
depredicteddirection0
2769
depredictedtarget0 embpstate0
2770
empintrp0 emppc0 emis_alu_exception0
2771
emis_taken_branch0 emtargetpc0
2772
emarg20 emresult0 emdest0
2773
emisreturnfromexception0
2774
emmispredictedtaken0
2775
emmispredictednottaken0 emregwrite0
2776
emmemwrite0 emmemtoreg0 dmem0 epc0
2777
isexception0 mmbpstate0 mmpintrp0
2778
mmisreturnfromexception0
2779
mmis_alu_exception0 mmppc0 mmval0
2780
mmdest0 mmregwrite0 mwbpstate0
2781
mwpintrp0 mwisreturnfromexception0
2782
mwis_alu_exception0 mwppc0 mwval0
2784
(g 'prf (g 'impl st13))
2785
(g 'pdmemhist_2 (g 'impl st13))))
2787
(equiv_ma ppc_v (g 'ppc (g 'impl st14))
2788
prf_v a1 (g 'prf (g 'impl st14))
2789
pimem_v (g 'pimem (g 'impl st14))
2790
pdmem_v (g 'pdmem (g 'impl st14))
2791
pepc_v (g 'pepc (g 'impl st14))
2793
(g 'pisexception (g 'impl st14))
2794
ffwrt_v (g 'ffwrt (g 'impl st14))
2795
ffppc_v (g 'ffppc (g 'impl st14))
2796
ffinst_v (g 'ffinst (g 'impl st14))
2797
fdwrt_v (g 'fdwrt (g 'impl st14))
2798
fdppc_v (g 'fdppc (g 'impl st14))
2799
fdinst_v (g 'fdinst (g 'impl st14))
2800
dewrt_v (g 'dewrt (g 'impl st14))
2801
deppc_v (g 'deppc (g 'impl st14))
2802
deop_v (g 'deop (g 'impl st14))
2803
dearg1_v (g 'dearg1 (g 'impl st14))
2804
dearg2_v (g 'dearg2 (g 'impl st14))
2805
dedest_v (g 'dedest (g 'impl st14))
2806
desrc1_v (g 'desrc1 (g 'impl st14))
2807
desrc2_v (g 'desrc2 (g 'impl st14))
2808
deimm_v (g 'deimm (g 'impl st14))
2810
(g 'deuseimm (g 'impl st14))
2812
(g 'deisbranch (g 'impl st14))
2814
(g 'dememtoreg (g 'impl st14))
2816
(g 'dememwrite (g 'impl st14))
2817
deisreturnfromexception_v
2818
(g 'deisreturnfromexception
2821
(g 'deregwrite (g 'impl st14)) emwrt_v
2822
(g 'emwrt (g 'impl st14)) emtargetpc_v
2823
(g 'emtargetpc (g 'impl st14))
2824
emdest_v (g 'emdest (g 'impl st14))
2825
emarg2_v (g 'emarg2 (g 'impl st14))
2827
(g 'emregwrite (g 'impl st14))
2829
(g 'emresult (g 'impl st14))
2831
(g 'emis_taken_branch (g 'impl st14))
2833
(g 'emmemtoreg (g 'impl st14))
2834
emis_alu_exception_v
2835
(g 'emis_alu_exception (g 'impl st14))
2836
emisreturnfromexception_v
2837
(g 'emisreturnfromexception
2840
(g 'emmemwrite (g 'impl st14)) mmwrt_v
2841
(g 'mmwrt (g 'impl st14)) mmval_v
2842
(g 'mmval (g 'impl st14)) mmdest_v
2843
(g 'mmdest (g 'impl st14))
2845
(g 'mmregwrite (g 'impl st14))
2846
mmisreturnfromexception_v
2847
(g 'mmisreturnfromexception
2849
mmis_alu_exception_v
2850
(g 'mmis_alu_exception (g 'impl st14))
2851
mwwrt_v (g 'mwwrt (g 'impl st14))
2852
mwval_v (g 'mwval (g 'impl st14))
2853
mwdest_v (g 'mwdest (g 'impl st14))
2855
(g 'mwregwrite (g 'impl st14))
2856
mwisreturnfromexception_v
2857
(g 'mwisreturnfromexception
2859
mwis_alu_exception_v
2860
(g 'mwis_alu_exception (g 'impl st14))))
2862
(or (or equiv_ma_2 equiv_ma_5) equiv_ma_6))
2863
(st15 (simulate_a st14 t nil nil pc0 intrp0
2864
nil pc0 bpstate0 intrp0 pc0
2865
alu_exception_handler intrp0
2866
bpstate0 ffbpstate0 ffpintrp0
2867
ffpredicteddirection0
2868
ffpredictedtarget0 ffinst0 ffppc0
2869
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2870
fdpredicteddirection0
2871
fdpredictedtarget0 debpstate0
2872
depintrp0 deppc0 desrc10 desrc20 a1
2873
a2 dedest0 deop0 deimm0 deuseimm0
2874
deisreturnfromexception0 deregwrite0
2875
dememwrite0 dememtoreg0 deisbranch0
2876
depredicteddirection0
2877
depredictedtarget0 embpstate0
2878
empintrp0 emppc0 emis_alu_exception0
2879
emis_taken_branch0 emtargetpc0
2880
emarg20 emresult0 emdest0
2881
emisreturnfromexception0
2882
emmispredictedtaken0
2883
emmispredictednottaken0 emregwrite0
2884
emmemwrite0 emmemtoreg0 dmem0 epc0
2885
isexception0 mmbpstate0 mmpintrp0
2886
mmisreturnfromexception0
2887
mmis_alu_exception0 mmppc0 mmval0
2888
mmdest0 mmregwrite0 mwbpstate0
2889
mwpintrp0 mwisreturnfromexception0
2890
mwis_alu_exception0 mwppc0 mwval0
2892
(g 'prf (g 'impl st14))
2893
(g 'pdmemhist_2 (g 'impl st14))))
2894
(st16 (simulate_a st15 nil nil nil pc0 intrp0
2895
nil pc0 bpstate0 intrp0 pc0
2896
alu_exception_handler intrp0
2897
bpstate0 ffbpstate0 ffpintrp0
2898
ffpredicteddirection0
2899
ffpredictedtarget0 ffinst0 ffppc0
2900
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2901
fdpredicteddirection0
2902
fdpredictedtarget0 debpstate0
2903
depintrp0 deppc0 desrc10 desrc20 a1
2904
a2 dedest0 deop0 deimm0 deuseimm0
2905
deisreturnfromexception0 deregwrite0
2906
dememwrite0 dememtoreg0 deisbranch0
2907
depredicteddirection0
2908
depredictedtarget0 embpstate0
2909
empintrp0 emppc0 emis_alu_exception0
2910
emis_taken_branch0 emtargetpc0
2911
emarg20 emresult0 emdest0
2912
emisreturnfromexception0
2913
emmispredictedtaken0
2914
emmispredictednottaken0 emregwrite0
2915
emmemwrite0 emmemtoreg0 dmem0 epc0
2916
isexception0 mmbpstate0 mmpintrp0
2917
mmisreturnfromexception0
2918
mmis_alu_exception0 mmppc0 mmval0
2919
mmdest0 mmregwrite0 mwbpstate0
2920
mwpintrp0 mwisreturnfromexception0
2921
mwis_alu_exception0 mwppc0 mwval0
2923
(g 'prf (g 'impl st15))
2924
(g 'pdmemhist_2 (g 'impl st15))))
2925
(st17 (simulate_a st16 nil nil nil pc0 intrp0
2926
nil pc0 bpstate0 intrp0 pc0
2927
alu_exception_handler intrp0
2928
bpstate0 ffbpstate0 ffpintrp0
2929
ffpredicteddirection0
2930
ffpredictedtarget0 ffinst0 ffppc0
2931
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2932
fdpredicteddirection0
2933
fdpredictedtarget0 debpstate0
2934
depintrp0 deppc0 desrc10 desrc20 a1
2935
a2 dedest0 deop0 deimm0 deuseimm0
2936
deisreturnfromexception0 deregwrite0
2937
dememwrite0 dememtoreg0 deisbranch0
2938
depredicteddirection0
2939
depredictedtarget0 embpstate0
2940
empintrp0 emppc0 emis_alu_exception0
2941
emis_taken_branch0 emtargetpc0
2942
emarg20 emresult0 emdest0
2943
emisreturnfromexception0
2944
emmispredictedtaken0
2945
emmispredictednottaken0 emregwrite0
2946
emmemwrite0 emmemtoreg0 dmem0 epc0
2947
isexception0 mmbpstate0 mmpintrp0
2948
mmisreturnfromexception0
2949
mmis_alu_exception0 mmppc0 mmval0
2950
mmdest0 mmregwrite0 mwbpstate0
2951
mwpintrp0 mwisreturnfromexception0
2952
mwis_alu_exception0 mwppc0 mwval0
2954
(g 'prf (g 'impl st16))
2955
(g 'pdmemhist_2 (g 'impl st16))))
2956
(st18 (simulate_a st17 nil nil nil pc0 intrp0
2957
nil pc0 bpstate0 intrp0 pc0
2958
alu_exception_handler intrp0
2959
bpstate0 ffbpstate0 ffpintrp0
2960
ffpredicteddirection0
2961
ffpredictedtarget0 ffinst0 ffppc0
2962
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2963
fdpredicteddirection0
2964
fdpredictedtarget0 debpstate0
2965
depintrp0 deppc0 desrc10 desrc20 a1
2966
a2 dedest0 deop0 deimm0 deuseimm0
2967
deisreturnfromexception0 deregwrite0
2968
dememwrite0 dememtoreg0 deisbranch0
2969
depredicteddirection0
2970
depredictedtarget0 embpstate0
2971
empintrp0 emppc0 emis_alu_exception0
2972
emis_taken_branch0 emtargetpc0
2973
emarg20 emresult0 emdest0
2974
emisreturnfromexception0
2975
emmispredictedtaken0
2976
emmispredictednottaken0 emregwrite0
2977
emmemwrite0 emmemtoreg0 dmem0 epc0
2978
isexception0 mmbpstate0 mmpintrp0
2979
mmisreturnfromexception0
2980
mmis_alu_exception0 mmppc0 mmval0
2981
mmdest0 mmregwrite0 mwbpstate0
2982
mwpintrp0 mwisreturnfromexception0
2983
mwis_alu_exception0 mwppc0 mwval0
2985
(g 'prf (g 'impl st17))
2986
(g 'pdmemhist_2 (g 'impl st17))))
2987
(st19 (simulate_a st18 nil nil nil pc0 intrp0
2988
nil pc0 bpstate0 intrp0 pc0
2989
alu_exception_handler intrp0
2990
bpstate0 ffbpstate0 ffpintrp0
2991
ffpredicteddirection0
2992
ffpredictedtarget0 ffinst0 ffppc0
2993
fdpintrp0 fdbpstate0 fdppc0 fdinst0
2994
fdpredicteddirection0
2995
fdpredictedtarget0 debpstate0
2996
depintrp0 deppc0 desrc10 desrc20 a1
2997
a2 dedest0 deop0 deimm0 deuseimm0
2998
deisreturnfromexception0 deregwrite0
2999
dememwrite0 dememtoreg0 deisbranch0
3000
depredicteddirection0
3001
depredictedtarget0 embpstate0
3002
empintrp0 emppc0 emis_alu_exception0
3003
emis_taken_branch0 emtargetpc0
3004
emarg20 emresult0 emdest0
3005
emisreturnfromexception0
3006
emmispredictedtaken0
3007
emmispredictednottaken0 emregwrite0
3008
emmemwrite0 emmemtoreg0 dmem0 epc0
3009
isexception0 mmbpstate0 mmpintrp0
3010
mmisreturnfromexception0
3011
mmis_alu_exception0 mmppc0 mmval0
3012
mmdest0 mmregwrite0 mwbpstate0
3013
mwpintrp0 mwisreturnfromexception0
3014
mwis_alu_exception0 mwppc0 mwval0
3016
(g 'prf (g 'impl st18))
3017
(g 'pdmemhist_2 (g 'impl st18))))
3018
(st20 (simulate_a st19 nil nil nil pc0 intrp0
3019
nil pc0 bpstate0 intrp0 pc0
3020
alu_exception_handler intrp0
3021
bpstate0 ffbpstate0 ffpintrp0
3022
ffpredicteddirection0
3023
ffpredictedtarget0 ffinst0 ffppc0
3024
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3025
fdpredicteddirection0
3026
fdpredictedtarget0 debpstate0
3027
depintrp0 deppc0 desrc10 desrc20 a1
3028
a2 dedest0 deop0 deimm0 deuseimm0
3029
deisreturnfromexception0 deregwrite0
3030
dememwrite0 dememtoreg0 deisbranch0
3031
depredicteddirection0
3032
depredictedtarget0 embpstate0
3033
empintrp0 emppc0 emis_alu_exception0
3034
emis_taken_branch0 emtargetpc0
3035
emarg20 emresult0 emdest0
3036
emisreturnfromexception0
3037
emmispredictedtaken0
3038
emmispredictednottaken0 emregwrite0
3039
emmemwrite0 emmemtoreg0 dmem0 epc0
3040
isexception0 mmbpstate0 mmpintrp0
3041
mmisreturnfromexception0
3042
mmis_alu_exception0 mmppc0 mmval0
3043
mmdest0 mmregwrite0 mwbpstate0
3044
mwpintrp0 mwisreturnfromexception0
3045
mwis_alu_exception0 mwppc0 mwval0
3047
(g 'prf (g 'impl st19))
3048
(g 'pdmemhist_2 (g 'impl st19))))
3049
(st21 (simulate_a st20 nil nil nil pc0 intrp0
3050
nil pc0 bpstate0 intrp0 pc0
3051
alu_exception_handler intrp0
3052
bpstate0 ffbpstate0 ffpintrp0
3053
ffpredicteddirection0
3054
ffpredictedtarget0 ffinst0 ffppc0
3055
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3056
fdpredicteddirection0
3057
fdpredictedtarget0 debpstate0
3058
depintrp0 deppc0 desrc10 desrc20 a1
3059
a2 dedest0 deop0 deimm0 deuseimm0
3060
deisreturnfromexception0 deregwrite0
3061
dememwrite0 dememtoreg0 deisbranch0
3062
depredicteddirection0
3063
depredictedtarget0 embpstate0
3064
empintrp0 emppc0 emis_alu_exception0
3065
emis_taken_branch0 emtargetpc0
3066
emarg20 emresult0 emdest0
3067
emisreturnfromexception0
3068
emmispredictedtaken0
3069
emmispredictednottaken0 emregwrite0
3070
emmemwrite0 emmemtoreg0 dmem0 epc0
3071
isexception0 mmbpstate0 mmpintrp0
3072
mmisreturnfromexception0
3073
mmis_alu_exception0 mmppc0 mmval0
3074
mmdest0 mmregwrite0 mwbpstate0
3075
mwpintrp0 mwisreturnfromexception0
3076
mwis_alu_exception0 mwppc0 mwval0
3078
(g 'prf (g 'impl st20))
3079
(g 'pdmemhist_2 (g 'impl st20))))
3080
(i_pc0 (committedpc (g 'mwwrt (g 'impl st21))
3081
(g 'mwppc (g 'impl st21))
3082
(g 'mmwrt (g 'impl st21))
3083
(g 'mmppc (g 'impl st21))
3084
(g 'emwrt (g 'impl st21))
3085
(g 'emppc (g 'impl st21))
3086
(g 'dewrt (g 'impl st21))
3087
(g 'deppc (g 'impl st21))
3088
(g 'fdwrt (g 'impl st21))
3089
(g 'fdppc (g 'impl st21))
3090
(g 'ffwrt (g 'impl st21))
3091
(g 'ffppc (g 'impl st21))
3092
(g 'ppc (g 'impl st21))))
3093
(i_rf0 (g 'prf (g 'impl st21)))
3094
(i_dmem0 (g 'pdmemhist_2 (g 'impl st21)))
3095
(i_epc0 (g 'pepchist_2 (g 'impl st21)))
3097
(g 'pisexceptionhist_2 (g 'impl st21)))
3098
(rank_w (rank (g 'mwwrt (g 'impl st21)) zero
3099
(g 'mmwrt (g 'impl st21))
3100
(g 'emwrt (g 'impl st21))
3101
(g 'dewrt (g 'impl st21))
3102
(g 'fdwrt (g 'impl st21))
3103
(g 'ffwrt (g 'impl st21))))
3104
(st22 (simulate_a st21 nil nil t i_pc0
3105
committedintrp nil pc0 bpstate0
3106
intrp0 pc0 alu_exception_handler
3107
intrp0 bpstate0 ffbpstate0 ffpintrp0
3108
ffpredicteddirection0
3109
ffpredictedtarget0 ffinst0 ffppc0
3110
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3111
fdpredicteddirection0
3112
fdpredictedtarget0 debpstate0
3113
depintrp0 deppc0 desrc10 desrc20 a1
3114
a2 dedest0 deop0 deimm0 deuseimm0
3115
deisreturnfromexception0 deregwrite0
3116
dememwrite0 dememtoreg0 deisbranch0
3117
depredicteddirection0
3118
depredictedtarget0 embpstate0
3119
empintrp0 emppc0 emis_alu_exception0
3120
emis_taken_branch0 emtargetpc0
3121
emarg20 emresult0 emdest0
3122
emisreturnfromexception0
3123
emmispredictedtaken0
3124
emmispredictednottaken0 emregwrite0
3125
emmemwrite0 emmemtoreg0 dmem0 epc0
3126
isexception0 mmbpstate0 mmpintrp0
3127
mmisreturnfromexception0
3128
mmis_alu_exception0 mmppc0 mmval0
3129
mmdest0 mmregwrite0 mwbpstate0
3130
mwpintrp0 mwisreturnfromexception0
3131
mwis_alu_exception0 mwppc0 mwval0
3133
(g 'prf (g 'impl st21))
3134
(g 'pdmemhist_2 (g 'impl st21))))
3135
(s_pc0 (g 'spc (g 'spec st22)))
3136
(s_rf0 (g 'srf (g 'spec st22)))
3137
(s_dmem0 (g 'sdmem (g 'spec st22)))
3138
(s_epc0 (g 'sepc (g 'spec st22)))
3140
(g 'sisexception (g 'spec st22)))
3141
(i_pc (committedpc (g 'mwwrt (g 'impl st22))
3142
(g 'mwppc (g 'impl st22))
3143
(g 'mmwrt (g 'impl st22))
3144
(g 'mmppc (g 'impl st22))
3145
(g 'emwrt (g 'impl st22))
3146
(g 'emppc (g 'impl st22))
3147
(g 'dewrt (g 'impl st22))
3148
(g 'deppc (g 'impl st22))
3149
(g 'fdwrt (g 'impl st22))
3150
(g 'fdppc (g 'impl st22))
3151
(g 'ffwrt (g 'impl st22))
3152
(g 'ffppc (g 'impl st22))
3153
(g 'ppc (g 'impl st22))))
3154
(i_rf (g 'prf (g 'impl st22)))
3155
(i_dmem (g 'pdmemhist_2 (g 'impl st22)))
3156
(i_epc (g 'pepchist_2 (g 'impl st22)))
3158
(g 'pisexceptionhist_2 (g 'impl st22)))
3159
(rank_v (rank (g 'mwwrt (g 'impl st22)) zero
3160
(g 'mmwrt (g 'impl st22))
3161
(g 'emwrt (g 'impl st22))
3162
(g 'dewrt (g 'impl st22))
3163
(g 'fdwrt (g 'impl st22))
3164
(g 'ffwrt (g 'impl st22))))
3165
(st23 (simulate_a st22 nil t nil pc0 intrp0
3166
nil pc0 bpstate0 intrp0 pc0
3167
alu_exception_handler intrp0
3168
bpstate0 ffbpstate0 ffpintrp0
3169
ffpredicteddirection0
3170
ffpredictedtarget0 ffinst0 ffppc0
3171
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3172
fdpredicteddirection0
3173
fdpredictedtarget0 debpstate0
3174
depintrp0 deppc0 desrc10 desrc20 a1
3175
a2 dedest0 deop0 deimm0 deuseimm0
3176
deisreturnfromexception0 deregwrite0
3177
dememwrite0 dememtoreg0 deisbranch0
3178
depredicteddirection0
3179
depredictedtarget0 embpstate0
3180
empintrp0 emppc0 emis_alu_exception0
3181
emis_taken_branch0 emtargetpc0
3182
emarg20 emresult0 emdest0
3183
emisreturnfromexception0
3184
emmispredictedtaken0
3185
emmispredictednottaken0 emregwrite0
3186
emmemwrite0 emmemtoreg0 dmem0 epc0
3187
isexception0 mmbpstate0 mmpintrp0
3188
mmisreturnfromexception0
3189
mmis_alu_exception0 mmppc0 mmval0
3190
mmdest0 mmregwrite0 mwbpstate0
3191
mwpintrp0 mwisreturnfromexception0
3192
mwis_alu_exception0 mwppc0 mwval0
3194
(g 'prf (g 'impl st22))
3195
(g 'pdmemhist_2 (g 'impl st22))))
3196
(s_pc1 (g 'spc (g 'spec st23)))
3197
(s_rf1 (g 'srf (g 'spec st23)))
3198
(s_dmem1 (g 'sdmem (g 'spec st23)))
3199
(s_epc1 (g 'sepc (g 'spec st23)))
3201
(g 'sisexception (g 'spec st23)))
3202
(st24 (simulate_a st23 t nil nil pc0 intrp0
3203
nil pc0 bpstate0 intrp0 pc0
3204
alu_exception_handler intrp0
3205
bpstate0 ffbpstate0 ffpintrp0
3206
ffpredicteddirection0
3207
ffpredictedtarget0 ffinst0 ffppc0
3208
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3209
fdpredicteddirection0
3210
fdpredictedtarget0 debpstate0
3211
depintrp0 deppc0 desrc10 desrc20 a1
3212
a2 dedest0 deop0 deimm0 deuseimm0
3213
deisreturnfromexception0 deregwrite0
3214
dememwrite0 dememtoreg0 deisbranch0
3215
depredicteddirection0
3216
depredictedtarget0 embpstate0
3217
empintrp0 emppc0 emis_alu_exception0
3218
emis_taken_branch0 emtargetpc0
3219
emarg20 emresult0 emdest0
3220
emisreturnfromexception0
3221
emmispredictedtaken0
3222
emmispredictednottaken0 emregwrite0
3223
emmemwrite0 emmemtoreg0 dmem0 epc0
3224
isexception0 mmbpstate0 mmpintrp0
3225
mmisreturnfromexception0
3226
mmis_alu_exception0 mmppc0 mmval0
3227
mmdest0 mmregwrite0 mwbpstate0
3228
mwpintrp0 mwisreturnfromexception0
3229
mwis_alu_exception0 mwppc0 mwval0
3231
(g 'prf (g 'impl st23))
3232
(g 'pdmemhist_2 (g 'impl st23))))
3233
(st25 (simulate_a st24 nil nil nil pc0 intrp0
3234
nil pc0 bpstate0 intrp0 pc0
3235
alu_exception_handler intrp0
3236
bpstate0 ffbpstate0 ffpintrp0
3237
ffpredicteddirection0
3238
ffpredictedtarget0 ffinst0 ffppc0
3239
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3240
fdpredicteddirection0
3241
fdpredictedtarget0 debpstate0
3242
depintrp0 deppc0 desrc10 desrc20 a1
3243
a2 dedest0 deop0 deimm0 deuseimm0
3244
deisreturnfromexception0 deregwrite0
3245
dememwrite0 dememtoreg0 deisbranch0
3246
depredicteddirection0
3247
depredictedtarget0 embpstate0
3248
empintrp0 emppc0 emis_alu_exception0
3249
emis_taken_branch0 emtargetpc0
3250
emarg20 emresult0 emdest0
3251
emisreturnfromexception0
3252
emmispredictedtaken0
3253
emmispredictednottaken0 emregwrite0
3254
emmemwrite0 emmemtoreg0 dmem0 epc0
3255
isexception0 mmbpstate0 mmpintrp0
3256
mmisreturnfromexception0
3257
mmis_alu_exception0 mmppc0 mmval0
3258
mmdest0 mmregwrite0 mwbpstate0
3259
mwpintrp0 mwisreturnfromexception0
3260
mwis_alu_exception0 mwppc0 mwval0
3262
(g 'prf (g 'impl st24))
3263
(g 'pdmemhist_2 (g 'impl st24))))
3264
(st26 (simulate_a st25 nil nil nil pc0 intrp0
3265
nil pc0 bpstate0 intrp0 pc0
3266
alu_exception_handler intrp0
3267
bpstate0 ffbpstate0 ffpintrp0
3268
ffpredicteddirection0
3269
ffpredictedtarget0 ffinst0 ffppc0
3270
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3271
fdpredicteddirection0
3272
fdpredictedtarget0 debpstate0
3273
depintrp0 deppc0 desrc10 desrc20 a1
3274
a2 dedest0 deop0 deimm0 deuseimm0
3275
deisreturnfromexception0 deregwrite0
3276
dememwrite0 dememtoreg0 deisbranch0
3277
depredicteddirection0
3278
depredictedtarget0 embpstate0
3279
empintrp0 emppc0 emis_alu_exception0
3280
emis_taken_branch0 emtargetpc0
3281
emarg20 emresult0 emdest0
3282
emisreturnfromexception0
3283
emmispredictedtaken0
3284
emmispredictednottaken0 emregwrite0
3285
emmemwrite0 emmemtoreg0 dmem0 epc0
3286
isexception0 mmbpstate0 mmpintrp0
3287
mmisreturnfromexception0
3288
mmis_alu_exception0 mmppc0 mmval0
3289
mmdest0 mmregwrite0 mwbpstate0
3290
mwpintrp0 mwisreturnfromexception0
3291
mwis_alu_exception0 mwppc0 mwval0
3293
(g 'prf (g 'impl st25))
3294
(g 'pdmemhist_2 (g 'impl st25))))
3295
(st27 (simulate_a st26 nil nil nil pc0 intrp0
3296
nil pc0 bpstate0 intrp0 pc0
3297
alu_exception_handler intrp0
3298
bpstate0 ffbpstate0 ffpintrp0
3299
ffpredicteddirection0
3300
ffpredictedtarget0 ffinst0 ffppc0
3301
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3302
fdpredicteddirection0
3303
fdpredictedtarget0 debpstate0
3304
depintrp0 deppc0 desrc10 desrc20 a1
3305
a2 dedest0 deop0 deimm0 deuseimm0
3306
deisreturnfromexception0 deregwrite0
3307
dememwrite0 dememtoreg0 deisbranch0
3308
depredicteddirection0
3309
depredictedtarget0 embpstate0
3310
empintrp0 emppc0 emis_alu_exception0
3311
emis_taken_branch0 emtargetpc0
3312
emarg20 emresult0 emdest0
3313
emisreturnfromexception0
3314
emmispredictedtaken0
3315
emmispredictednottaken0 emregwrite0
3316
emmemwrite0 emmemtoreg0 dmem0 epc0
3317
isexception0 mmbpstate0 mmpintrp0
3318
mmisreturnfromexception0
3319
mmis_alu_exception0 mmppc0 mmval0
3320
mmdest0 mmregwrite0 mwbpstate0
3321
mwpintrp0 mwisreturnfromexception0
3322
mwis_alu_exception0 mwppc0 mwval0
3324
(g 'prf (g 'impl st26))
3325
(g 'pdmemhist_2 (g 'impl st26))))
3326
(st28 (simulate_a st27 nil nil nil pc0 intrp0
3327
nil pc0 bpstate0 intrp0 pc0
3328
alu_exception_handler intrp0
3329
bpstate0 ffbpstate0 ffpintrp0
3330
ffpredicteddirection0
3331
ffpredictedtarget0 ffinst0 ffppc0
3332
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3333
fdpredicteddirection0
3334
fdpredictedtarget0 debpstate0
3335
depintrp0 deppc0 desrc10 desrc20 a1
3336
a2 dedest0 deop0 deimm0 deuseimm0
3337
deisreturnfromexception0 deregwrite0
3338
dememwrite0 dememtoreg0 deisbranch0
3339
depredicteddirection0
3340
depredictedtarget0 embpstate0
3341
empintrp0 emppc0 emis_alu_exception0
3342
emis_taken_branch0 emtargetpc0
3343
emarg20 emresult0 emdest0
3344
emisreturnfromexception0
3345
emmispredictedtaken0
3346
emmispredictednottaken0 emregwrite0
3347
emmemwrite0 emmemtoreg0 dmem0 epc0
3348
isexception0 mmbpstate0 mmpintrp0
3349
mmisreturnfromexception0
3350
mmis_alu_exception0 mmppc0 mmval0
3351
mmdest0 mmregwrite0 mwbpstate0
3352
mwpintrp0 mwisreturnfromexception0
3353
mwis_alu_exception0 mwppc0 mwval0
3355
(g 'prf (g 'impl st27))
3356
(g 'pdmemhist_2 (g 'impl st27))))
3357
(st29 (simulate_a st28 nil nil nil pc0 intrp0
3358
nil pc0 bpstate0 intrp0 pc0
3359
alu_exception_handler intrp0
3360
bpstate0 ffbpstate0 ffpintrp0
3361
ffpredicteddirection0
3362
ffpredictedtarget0 ffinst0 ffppc0
3363
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3364
fdpredicteddirection0
3365
fdpredictedtarget0 debpstate0
3366
depintrp0 deppc0 desrc10 desrc20 a1
3367
a2 dedest0 deop0 deimm0 deuseimm0
3368
deisreturnfromexception0 deregwrite0
3369
dememwrite0 dememtoreg0 deisbranch0
3370
depredicteddirection0
3371
depredictedtarget0 embpstate0
3372
empintrp0 emppc0 emis_alu_exception0
3373
emis_taken_branch0 emtargetpc0
3374
emarg20 emresult0 emdest0
3375
emisreturnfromexception0
3376
emmispredictedtaken0
3377
emmispredictednottaken0 emregwrite0
3378
emmemwrite0 emmemtoreg0 dmem0 epc0
3379
isexception0 mmbpstate0 mmpintrp0
3380
mmisreturnfromexception0
3381
mmis_alu_exception0 mmppc0 mmval0
3382
mmdest0 mmregwrite0 mwbpstate0
3383
mwpintrp0 mwisreturnfromexception0
3384
mwis_alu_exception0 mwppc0 mwval0
3386
(g 'prf (g 'impl st28))
3387
(g 'pdmemhist_2 (g 'impl st28))))
3388
(i_pc0_2 (committedpc
3389
(g 'mwwrt (g 'impl st29))
3390
(g 'mwppc (g 'impl st29))
3391
(g 'mmwrt (g 'impl st29))
3392
(g 'mmppc (g 'impl st29))
3393
(g 'emwrt (g 'impl st29))
3394
(g 'emppc (g 'impl st29))
3395
(g 'dewrt (g 'impl st29))
3396
(g 'deppc (g 'impl st29))
3397
(g 'fdwrt (g 'impl st29))
3398
(g 'fdppc (g 'impl st29))
3399
(g 'ffwrt (g 'impl st29))
3400
(g 'ffppc (g 'impl st29))
3401
(g 'ppc (g 'impl st29))))
3402
(i_rf0_2 (g 'prf (g 'impl st29)))
3403
(i_dmem0_2 (g 'pdmemhist_2 (g 'impl st29)))
3404
(i_epc0_2 (g 'pepchist_2 (g 'impl st29)))
3406
(g 'pisexceptionhist_2 (g 'impl st29)))
3408
(rank (g 'mwwrt (g 'impl st29)) zero
3409
(g 'mmwrt (g 'impl st29))
3410
(g 'emwrt (g 'impl st29))
3411
(g 'dewrt (g 'impl st29))
3412
(g 'fdwrt (g 'impl st29))
3413
(g 'ffwrt (g 'impl st29))))
3414
(st30 (simulate_a st29 nil nil t i_pc0_2
3415
committedintrp nil pc0 bpstate0
3416
intrp0 pc0 alu_exception_handler
3417
intrp0 bpstate0 ffbpstate0 ffpintrp0
3418
ffpredicteddirection0
3419
ffpredictedtarget0 ffinst0 ffppc0
3420
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3421
fdpredicteddirection0
3422
fdpredictedtarget0 debpstate0
3423
depintrp0 deppc0 desrc10 desrc20 a1
3424
a2 dedest0 deop0 deimm0 deuseimm0
3425
deisreturnfromexception0 deregwrite0
3426
dememwrite0 dememtoreg0 deisbranch0
3427
depredicteddirection0
3428
depredictedtarget0 embpstate0
3429
empintrp0 emppc0 emis_alu_exception0
3430
emis_taken_branch0 emtargetpc0
3431
emarg20 emresult0 emdest0
3432
emisreturnfromexception0
3433
emmispredictedtaken0
3434
emmispredictednottaken0 emregwrite0
3435
emmemwrite0 emmemtoreg0 dmem0 epc0
3436
isexception0 mmbpstate0 mmpintrp0
3437
mmisreturnfromexception0
3438
mmis_alu_exception0 mmppc0 mmval0
3439
mmdest0 mmregwrite0 mwbpstate0
3440
mwpintrp0 mwisreturnfromexception0
3441
mwis_alu_exception0 mwppc0 mwval0
3443
(g 'prf (g 'impl st29))
3444
(g 'pdmemhist_2 (g 'impl st29))))
3445
(s_pc0_2 (g 'spc (g 'spec st30)))
3446
(s_rf0_2 (g 'srf (g 'spec st30)))
3447
(s_dmem0_2 (g 'sdmem (g 'spec st30)))
3448
(s_epc0_2 (g 'sepc (g 'spec st30)))
3450
(g 'sisexception (g 'spec st30)))
3451
(i_pc_2 (committedpc (g 'mwwrt (g 'impl st30))
3452
(g 'mwppc (g 'impl st30))
3453
(g 'mmwrt (g 'impl st30))
3454
(g 'mmppc (g 'impl st30))
3455
(g 'emwrt (g 'impl st30))
3456
(g 'emppc (g 'impl st30))
3457
(g 'dewrt (g 'impl st30))
3458
(g 'deppc (g 'impl st30))
3459
(g 'fdwrt (g 'impl st30))
3460
(g 'fdppc (g 'impl st30))
3461
(g 'ffwrt (g 'impl st30))
3462
(g 'ffppc (g 'impl st30))
3463
(g 'ppc (g 'impl st30))))
3464
(i_rf_2 (g 'prf (g 'impl st30)))
3465
(i_dmem_2 (g 'pdmemhist_2 (g 'impl st30)))
3466
(i_epc_2 (g 'pepchist_2 (g 'impl st30)))
3468
(g 'pisexceptionhist_2 (g 'impl st30)))
3470
(rank (g 'mwwrt (g 'impl st30)) zero
3471
(g 'mmwrt (g 'impl st30))
3472
(g 'emwrt (g 'impl st30))
3473
(g 'dewrt (g 'impl st30))
3474
(g 'fdwrt (g 'impl st30))
3475
(g 'ffwrt (g 'impl st30))))
3476
(st31 (simulate_a st30 nil t nil pc0 intrp0
3477
nil pc0 bpstate0 intrp0 pc0
3478
alu_exception_handler intrp0
3479
bpstate0 ffbpstate0 ffpintrp0
3480
ffpredicteddirection0
3481
ffpredictedtarget0 ffinst0 ffppc0
3482
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3483
fdpredicteddirection0
3484
fdpredictedtarget0 debpstate0
3485
depintrp0 deppc0 desrc10 desrc20 a1
3486
a2 dedest0 deop0 deimm0 deuseimm0
3487
deisreturnfromexception0 deregwrite0
3488
dememwrite0 dememtoreg0 deisbranch0
3489
depredicteddirection0
3490
depredictedtarget0 embpstate0
3491
empintrp0 emppc0 emis_alu_exception0
3492
emis_taken_branch0 emtargetpc0
3493
emarg20 emresult0 emdest0
3494
emisreturnfromexception0
3495
emmispredictedtaken0
3496
emmispredictednottaken0 emregwrite0
3497
emmemwrite0 emmemtoreg0 dmem0 epc0
3498
isexception0 mmbpstate0 mmpintrp0
3499
mmisreturnfromexception0
3500
mmis_alu_exception0 mmppc0 mmval0
3501
mmdest0 mmregwrite0 mwbpstate0
3502
mwpintrp0 mwisreturnfromexception0
3503
mwis_alu_exception0 mwppc0 mwval0
3505
(g 'prf (g 'impl st30))
3506
(g 'pdmemhist_2 (g 'impl st30))))
3507
(s_pc1_2 (g 'spc (g 'spec st31)))
3508
(s_rf1_2 (g 'srf (g 'spec st31)))
3509
(s_dmem1_2 (g 'sdmem (g 'spec st31)))
3510
(s_epc1_2 (g 'sepc (g 'spec st31)))
3512
(g 'sisexception (g 'spec st31)))
3513
(st32 (simulate_a st31 t nil nil pc0 intrp0
3514
nil pc0 bpstate0 intrp0 pc0
3515
alu_exception_handler intrp0
3516
bpstate0 ffbpstate0 ffpintrp0
3517
ffpredicteddirection0
3518
ffpredictedtarget0 ffinst0 ffppc0
3519
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3520
fdpredicteddirection0
3521
fdpredictedtarget0 debpstate0
3522
depintrp0 deppc0 desrc10 desrc20 a1
3523
a2 dedest0 deop0 deimm0 deuseimm0
3524
deisreturnfromexception0 deregwrite0
3525
dememwrite0 dememtoreg0 deisbranch0
3526
depredicteddirection0
3527
depredictedtarget0 embpstate0
3528
empintrp0 emppc0 emis_alu_exception0
3529
emis_taken_branch0 emtargetpc0
3530
emarg20 emresult0 emdest0
3531
emisreturnfromexception0
3532
emmispredictedtaken0
3533
emmispredictednottaken0 emregwrite0
3534
emmemwrite0 emmemtoreg0 dmem0 epc0
3535
isexception0 mmbpstate0 mmpintrp0
3536
mmisreturnfromexception0
3537
mmis_alu_exception0 mmppc0 mmval0
3538
mmdest0 mmregwrite0 mwbpstate0
3539
mwpintrp0 mwisreturnfromexception0
3540
mwis_alu_exception0 mwppc0 mwval0
3542
(g 'prf (g 'impl st31))
3543
(g 'pdmemhist_2 (g 'impl st31))))
3544
(st33 (simulate_a st32 nil nil nil pc0 intrp0
3545
nil pc0 bpstate0 intrp0 pc0
3546
alu_exception_handler intrp0
3547
bpstate0 ffbpstate0 ffpintrp0
3548
ffpredicteddirection0
3549
ffpredictedtarget0 ffinst0 ffppc0
3550
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3551
fdpredicteddirection0
3552
fdpredictedtarget0 debpstate0
3553
depintrp0 deppc0 desrc10 desrc20 a1
3554
a2 dedest0 deop0 deimm0 deuseimm0
3555
deisreturnfromexception0 deregwrite0
3556
dememwrite0 dememtoreg0 deisbranch0
3557
depredicteddirection0
3558
depredictedtarget0 embpstate0
3559
empintrp0 emppc0 emis_alu_exception0
3560
emis_taken_branch0 emtargetpc0
3561
emarg20 emresult0 emdest0
3562
emisreturnfromexception0
3563
emmispredictedtaken0
3564
emmispredictednottaken0 emregwrite0
3565
emmemwrite0 emmemtoreg0 dmem0 epc0
3566
isexception0 mmbpstate0 mmpintrp0
3567
mmisreturnfromexception0
3568
mmis_alu_exception0 mmppc0 mmval0
3569
mmdest0 mmregwrite0 mwbpstate0
3570
mwpintrp0 mwisreturnfromexception0
3571
mwis_alu_exception0 mwppc0 mwval0
3573
(g 'prf (g 'impl st32))
3574
(g 'pdmemhist_2 (g 'impl st32))))
3575
(st34 (simulate_a st33 nil nil nil pc0 intrp0
3576
nil pc0 bpstate0 intrp0 pc0
3577
alu_exception_handler intrp0
3578
bpstate0 ffbpstate0 ffpintrp0
3579
ffpredicteddirection0
3580
ffpredictedtarget0 ffinst0 ffppc0
3581
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3582
fdpredicteddirection0
3583
fdpredictedtarget0 debpstate0
3584
depintrp0 deppc0 desrc10 desrc20 a1
3585
a2 dedest0 deop0 deimm0 deuseimm0
3586
deisreturnfromexception0 deregwrite0
3587
dememwrite0 dememtoreg0 deisbranch0
3588
depredicteddirection0
3589
depredictedtarget0 embpstate0
3590
empintrp0 emppc0 emis_alu_exception0
3591
emis_taken_branch0 emtargetpc0
3592
emarg20 emresult0 emdest0
3593
emisreturnfromexception0
3594
emmispredictedtaken0
3595
emmispredictednottaken0 emregwrite0
3596
emmemwrite0 emmemtoreg0 dmem0 epc0
3597
isexception0 mmbpstate0 mmpintrp0
3598
mmisreturnfromexception0
3599
mmis_alu_exception0 mmppc0 mmval0
3600
mmdest0 mmregwrite0 mwbpstate0
3601
mwpintrp0 mwisreturnfromexception0
3602
mwis_alu_exception0 mwppc0 mwval0
3604
(g 'prf (g 'impl st33))
3605
(g 'pdmemhist_2 (g 'impl st33))))
3606
(st35 (simulate_a st34 nil nil nil pc0 intrp0
3607
nil pc0 bpstate0 intrp0 pc0
3608
alu_exception_handler intrp0
3609
bpstate0 ffbpstate0 ffpintrp0
3610
ffpredicteddirection0
3611
ffpredictedtarget0 ffinst0 ffppc0
3612
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3613
fdpredicteddirection0
3614
fdpredictedtarget0 debpstate0
3615
depintrp0 deppc0 desrc10 desrc20 a1
3616
a2 dedest0 deop0 deimm0 deuseimm0
3617
deisreturnfromexception0 deregwrite0
3618
dememwrite0 dememtoreg0 deisbranch0
3619
depredicteddirection0
3620
depredictedtarget0 embpstate0
3621
empintrp0 emppc0 emis_alu_exception0
3622
emis_taken_branch0 emtargetpc0
3623
emarg20 emresult0 emdest0
3624
emisreturnfromexception0
3625
emmispredictedtaken0
3626
emmispredictednottaken0 emregwrite0
3627
emmemwrite0 emmemtoreg0 dmem0 epc0
3628
isexception0 mmbpstate0 mmpintrp0
3629
mmisreturnfromexception0
3630
mmis_alu_exception0 mmppc0 mmval0
3631
mmdest0 mmregwrite0 mwbpstate0
3632
mwpintrp0 mwisreturnfromexception0
3633
mwis_alu_exception0 mwppc0 mwval0
3635
(g 'prf (g 'impl st34))
3636
(g 'pdmemhist_2 (g 'impl st34))))
3637
(st36 (simulate_a st35 nil nil nil pc0 intrp0
3638
nil pc0 bpstate0 intrp0 pc0
3639
alu_exception_handler intrp0
3640
bpstate0 ffbpstate0 ffpintrp0
3641
ffpredicteddirection0
3642
ffpredictedtarget0 ffinst0 ffppc0
3643
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3644
fdpredicteddirection0
3645
fdpredictedtarget0 debpstate0
3646
depintrp0 deppc0 desrc10 desrc20 a1
3647
a2 dedest0 deop0 deimm0 deuseimm0
3648
deisreturnfromexception0 deregwrite0
3649
dememwrite0 dememtoreg0 deisbranch0
3650
depredicteddirection0
3651
depredictedtarget0 embpstate0
3652
empintrp0 emppc0 emis_alu_exception0
3653
emis_taken_branch0 emtargetpc0
3654
emarg20 emresult0 emdest0
3655
emisreturnfromexception0
3656
emmispredictedtaken0
3657
emmispredictednottaken0 emregwrite0
3658
emmemwrite0 emmemtoreg0 dmem0 epc0
3659
isexception0 mmbpstate0 mmpintrp0
3660
mmisreturnfromexception0
3661
mmis_alu_exception0 mmppc0 mmval0
3662
mmdest0 mmregwrite0 mwbpstate0
3663
mwpintrp0 mwisreturnfromexception0
3664
mwis_alu_exception0 mwppc0 mwval0
3666
(g 'prf (g 'impl st35))
3667
(g 'pdmemhist_2 (g 'impl st35))))
3668
(i_pc0_3 (committedpc
3669
(g 'mwwrt (g 'impl st36))
3670
(g 'mwppc (g 'impl st36))
3671
(g 'mmwrt (g 'impl st36))
3672
(g 'mmppc (g 'impl st36))
3673
(g 'emwrt (g 'impl st36))
3674
(g 'emppc (g 'impl st36))
3675
(g 'dewrt (g 'impl st36))
3676
(g 'deppc (g 'impl st36))
3677
(g 'fdwrt (g 'impl st36))
3678
(g 'fdppc (g 'impl st36))
3679
(g 'ffwrt (g 'impl st36))
3680
(g 'ffppc (g 'impl st36))
3681
(g 'ppc (g 'impl st36))))
3682
(i_rf0_3 (g 'prf (g 'impl st36)))
3683
(i_dmem0_3 (g 'pdmemhist_2 (g 'impl st36)))
3684
(i_epc0_3 (g 'pepchist_2 (g 'impl st36)))
3686
(g 'pisexceptionhist_2 (g 'impl st36)))
3688
(rank (g 'mwwrt (g 'impl st36)) zero
3689
(g 'mmwrt (g 'impl st36))
3690
(g 'emwrt (g 'impl st36))
3691
(g 'dewrt (g 'impl st36))
3692
(g 'fdwrt (g 'impl st36))
3693
(g 'ffwrt (g 'impl st36))))
3694
(st37 (simulate_a st36 nil nil t i_pc0_3
3695
committedintrp nil pc0 bpstate0
3696
intrp0 pc0 alu_exception_handler
3697
intrp0 bpstate0 ffbpstate0 ffpintrp0
3698
ffpredicteddirection0
3699
ffpredictedtarget0 ffinst0 ffppc0
3700
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3701
fdpredicteddirection0
3702
fdpredictedtarget0 debpstate0
3703
depintrp0 deppc0 desrc10 desrc20 a1
3704
a2 dedest0 deop0 deimm0 deuseimm0
3705
deisreturnfromexception0 deregwrite0
3706
dememwrite0 dememtoreg0 deisbranch0
3707
depredicteddirection0
3708
depredictedtarget0 embpstate0
3709
empintrp0 emppc0 emis_alu_exception0
3710
emis_taken_branch0 emtargetpc0
3711
emarg20 emresult0 emdest0
3712
emisreturnfromexception0
3713
emmispredictedtaken0
3714
emmispredictednottaken0 emregwrite0
3715
emmemwrite0 emmemtoreg0 dmem0 epc0
3716
isexception0 mmbpstate0 mmpintrp0
3717
mmisreturnfromexception0
3718
mmis_alu_exception0 mmppc0 mmval0
3719
mmdest0 mmregwrite0 mwbpstate0
3720
mwpintrp0 mwisreturnfromexception0
3721
mwis_alu_exception0 mwppc0 mwval0
3723
(g 'prf (g 'impl st36))
3724
(g 'pdmemhist_2 (g 'impl st36))))
3725
(s_pc0_3 (g 'spc (g 'spec st37)))
3726
(s_rf0_3 (g 'srf (g 'spec st37)))
3727
(s_dmem0_3 (g 'sdmem (g 'spec st37)))
3728
(s_epc0_3 (g 'sepc (g 'spec st37)))
3730
(g 'sisexception (g 'spec st37)))
3731
(i_pc_3 (committedpc (g 'mwwrt (g 'impl st37))
3732
(g 'mwppc (g 'impl st37))
3733
(g 'mmwrt (g 'impl st37))
3734
(g 'mmppc (g 'impl st37))
3735
(g 'emwrt (g 'impl st37))
3736
(g 'emppc (g 'impl st37))
3737
(g 'dewrt (g 'impl st37))
3738
(g 'deppc (g 'impl st37))
3739
(g 'fdwrt (g 'impl st37))
3740
(g 'fdppc (g 'impl st37))
3741
(g 'ffwrt (g 'impl st37))
3742
(g 'ffppc (g 'impl st37))
3743
(g 'ppc (g 'impl st37))))
3744
(i_rf_3 (g 'prf (g 'impl st37)))
3745
(i_dmem_3 (g 'pdmemhist_2 (g 'impl st37)))
3746
(i_epc_3 (g 'pepchist_2 (g 'impl st37)))
3748
(g 'pisexceptionhist_2 (g 'impl st37)))
3750
(rank (g 'mwwrt (g 'impl st37)) zero
3751
(g 'mmwrt (g 'impl st37))
3752
(g 'emwrt (g 'impl st37))
3753
(g 'dewrt (g 'impl st37))
3754
(g 'fdwrt (g 'impl st37))
3755
(g 'ffwrt (g 'impl st37))))
3756
(st38 (simulate_a st37 nil t nil pc0 intrp0
3757
nil pc0 bpstate0 intrp0 pc0
3758
alu_exception_handler intrp0
3759
bpstate0 ffbpstate0 ffpintrp0
3760
ffpredicteddirection0
3761
ffpredictedtarget0 ffinst0 ffppc0
3762
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3763
fdpredicteddirection0
3764
fdpredictedtarget0 debpstate0
3765
depintrp0 deppc0 desrc10 desrc20 a1
3766
a2 dedest0 deop0 deimm0 deuseimm0
3767
deisreturnfromexception0 deregwrite0
3768
dememwrite0 dememtoreg0 deisbranch0
3769
depredicteddirection0
3770
depredictedtarget0 embpstate0
3771
empintrp0 emppc0 emis_alu_exception0
3772
emis_taken_branch0 emtargetpc0
3773
emarg20 emresult0 emdest0
3774
emisreturnfromexception0
3775
emmispredictedtaken0
3776
emmispredictednottaken0 emregwrite0
3777
emmemwrite0 emmemtoreg0 dmem0 epc0
3778
isexception0 mmbpstate0 mmpintrp0
3779
mmisreturnfromexception0
3780
mmis_alu_exception0 mmppc0 mmval0
3781
mmdest0 mmregwrite0 mwbpstate0
3782
mwpintrp0 mwisreturnfromexception0
3783
mwis_alu_exception0 mwppc0 mwval0
3785
(g 'prf (g 'impl st37))
3786
(g 'pdmemhist_2 (g 'impl st37))))
3787
(s_pc1_3 (g 'spc (g 'spec st38)))
3788
(s_rf1_3 (g 'srf (g 'spec st38)))
3789
(s_dmem1_3 (g 'sdmem (g 'spec st38)))
3790
(s_epc1_3 (g 'sepc (g 'spec st38)))
3792
(g 'sisexception (g 'spec st38)))
3793
(st39 (simulate_a st38 t nil nil pc0 intrp0
3794
nil pc0 bpstate0 intrp0 pc0
3795
alu_exception_handler intrp0
3796
bpstate0 ffbpstate0 ffpintrp0
3797
ffpredicteddirection0
3798
ffpredictedtarget0 ffinst0 ffppc0
3799
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3800
fdpredicteddirection0
3801
fdpredictedtarget0 debpstate0
3802
depintrp0 deppc0 desrc10 desrc20 a1
3803
a2 dedest0 deop0 deimm0 deuseimm0
3804
deisreturnfromexception0 deregwrite0
3805
dememwrite0 dememtoreg0 deisbranch0
3806
depredicteddirection0
3807
depredictedtarget0 embpstate0
3808
empintrp0 emppc0 emis_alu_exception0
3809
emis_taken_branch0 emtargetpc0
3810
emarg20 emresult0 emdest0
3811
emisreturnfromexception0
3812
emmispredictedtaken0
3813
emmispredictednottaken0 emregwrite0
3814
emmemwrite0 emmemtoreg0 dmem0 epc0
3815
isexception0 mmbpstate0 mmpintrp0
3816
mmisreturnfromexception0
3817
mmis_alu_exception0 mmppc0 mmval0
3818
mmdest0 mmregwrite0 mwbpstate0
3819
mwpintrp0 mwisreturnfromexception0
3820
mwis_alu_exception0 mwppc0 mwval0
3822
(g 'prf (g 'impl st38))
3823
(g 'pdmemhist_2 (g 'impl st38))))
3824
(st40 (simulate_a st39 nil nil nil pc0 intrp0
3825
nil pc0 bpstate0 intrp0 pc0
3826
alu_exception_handler intrp0
3827
bpstate0 ffbpstate0 ffpintrp0
3828
ffpredicteddirection0
3829
ffpredictedtarget0 ffinst0 ffppc0
3830
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3831
fdpredicteddirection0
3832
fdpredictedtarget0 debpstate0
3833
depintrp0 deppc0 desrc10 desrc20 a1
3834
a2 dedest0 deop0 deimm0 deuseimm0
3835
deisreturnfromexception0 deregwrite0
3836
dememwrite0 dememtoreg0 deisbranch0
3837
depredicteddirection0
3838
depredictedtarget0 embpstate0
3839
empintrp0 emppc0 emis_alu_exception0
3840
emis_taken_branch0 emtargetpc0
3841
emarg20 emresult0 emdest0
3842
emisreturnfromexception0
3843
emmispredictedtaken0
3844
emmispredictednottaken0 emregwrite0
3845
emmemwrite0 emmemtoreg0 dmem0 epc0
3846
isexception0 mmbpstate0 mmpintrp0
3847
mmisreturnfromexception0
3848
mmis_alu_exception0 mmppc0 mmval0
3849
mmdest0 mmregwrite0 mwbpstate0
3850
mwpintrp0 mwisreturnfromexception0
3851
mwis_alu_exception0 mwppc0 mwval0
3853
(g 'prf (g 'impl st39))
3854
(g 'pdmemhist_2 (g 'impl st39))))
3855
(st41 (simulate_a st40 nil nil nil pc0 intrp0
3856
nil pc0 bpstate0 intrp0 pc0
3857
alu_exception_handler intrp0
3858
bpstate0 ffbpstate0 ffpintrp0
3859
ffpredicteddirection0
3860
ffpredictedtarget0 ffinst0 ffppc0
3861
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3862
fdpredicteddirection0
3863
fdpredictedtarget0 debpstate0
3864
depintrp0 deppc0 desrc10 desrc20 a1
3865
a2 dedest0 deop0 deimm0 deuseimm0
3866
deisreturnfromexception0 deregwrite0
3867
dememwrite0 dememtoreg0 deisbranch0
3868
depredicteddirection0
3869
depredictedtarget0 embpstate0
3870
empintrp0 emppc0 emis_alu_exception0
3871
emis_taken_branch0 emtargetpc0
3872
emarg20 emresult0 emdest0
3873
emisreturnfromexception0
3874
emmispredictedtaken0
3875
emmispredictednottaken0 emregwrite0
3876
emmemwrite0 emmemtoreg0 dmem0 epc0
3877
isexception0 mmbpstate0 mmpintrp0
3878
mmisreturnfromexception0
3879
mmis_alu_exception0 mmppc0 mmval0
3880
mmdest0 mmregwrite0 mwbpstate0
3881
mwpintrp0 mwisreturnfromexception0
3882
mwis_alu_exception0 mwppc0 mwval0
3884
(g 'prf (g 'impl st40))
3885
(g 'pdmemhist_2 (g 'impl st40))))
3886
(st42 (simulate_a st41 nil nil nil pc0 intrp0
3887
nil pc0 bpstate0 intrp0 pc0
3888
alu_exception_handler intrp0
3889
bpstate0 ffbpstate0 ffpintrp0
3890
ffpredicteddirection0
3891
ffpredictedtarget0 ffinst0 ffppc0
3892
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3893
fdpredicteddirection0
3894
fdpredictedtarget0 debpstate0
3895
depintrp0 deppc0 desrc10 desrc20 a1
3896
a2 dedest0 deop0 deimm0 deuseimm0
3897
deisreturnfromexception0 deregwrite0
3898
dememwrite0 dememtoreg0 deisbranch0
3899
depredicteddirection0
3900
depredictedtarget0 embpstate0
3901
empintrp0 emppc0 emis_alu_exception0
3902
emis_taken_branch0 emtargetpc0
3903
emarg20 emresult0 emdest0
3904
emisreturnfromexception0
3905
emmispredictedtaken0
3906
emmispredictednottaken0 emregwrite0
3907
emmemwrite0 emmemtoreg0 dmem0 epc0
3908
isexception0 mmbpstate0 mmpintrp0
3909
mmisreturnfromexception0
3910
mmis_alu_exception0 mmppc0 mmval0
3911
mmdest0 mmregwrite0 mwbpstate0
3912
mwpintrp0 mwisreturnfromexception0
3913
mwis_alu_exception0 mwppc0 mwval0
3915
(g 'prf (g 'impl st41))
3916
(g 'pdmemhist_2 (g 'impl st41))))
3917
(i_pc0_4 (committedpc
3918
(g 'mwwrt (g 'impl st42))
3919
(g 'mwppc (g 'impl st42))
3920
(g 'mmwrt (g 'impl st42))
3921
(g 'mmppc (g 'impl st42))
3922
(g 'emwrt (g 'impl st42))
3923
(g 'emppc (g 'impl st42))
3924
(g 'dewrt (g 'impl st42))
3925
(g 'deppc (g 'impl st42))
3926
(g 'fdwrt (g 'impl st42))
3927
(g 'fdppc (g 'impl st42))
3928
(g 'ffwrt (g 'impl st42))
3929
(g 'ffppc (g 'impl st42))
3930
(g 'ppc (g 'impl st42))))
3931
(i_rf0_4 (g 'prf (g 'impl st42)))
3932
(i_dmem0_4 (g 'pdmemhist_2 (g 'impl st42)))
3933
(i_epc0_4 (g 'pepchist_2 (g 'impl st42)))
3935
(g 'pisexceptionhist_2 (g 'impl st42)))
3937
(rank (g 'mwwrt (g 'impl st42)) zero
3938
(g 'mmwrt (g 'impl st42))
3939
(g 'emwrt (g 'impl st42))
3940
(g 'dewrt (g 'impl st42))
3941
(g 'fdwrt (g 'impl st42))
3942
(g 'ffwrt (g 'impl st42))))
3943
(st43 (simulate_a st42 nil nil t i_pc0_4
3944
committedintrp nil pc0 bpstate0
3945
intrp0 pc0 alu_exception_handler
3946
intrp0 bpstate0 ffbpstate0 ffpintrp0
3947
ffpredicteddirection0
3948
ffpredictedtarget0 ffinst0 ffppc0
3949
fdpintrp0 fdbpstate0 fdppc0 fdinst0
3950
fdpredicteddirection0
3951
fdpredictedtarget0 debpstate0
3952
depintrp0 deppc0 desrc10 desrc20 a1
3953
a2 dedest0 deop0 deimm0 deuseimm0
3954
deisreturnfromexception0 deregwrite0
3955
dememwrite0 dememtoreg0 deisbranch0
3956
depredicteddirection0
3957
depredictedtarget0 embpstate0
3958
empintrp0 emppc0 emis_alu_exception0
3959
emis_taken_branch0 emtargetpc0
3960
emarg20 emresult0 emdest0
3961
emisreturnfromexception0
3962
emmispredictedtaken0
3963
emmispredictednottaken0 emregwrite0
3964
emmemwrite0 emmemtoreg0 dmem0 epc0
3965
isexception0 mmbpstate0 mmpintrp0
3966
mmisreturnfromexception0
3967
mmis_alu_exception0 mmppc0 mmval0
3968
mmdest0 mmregwrite0 mwbpstate0
3969
mwpintrp0 mwisreturnfromexception0
3970
mwis_alu_exception0 mwppc0 mwval0
3972
(g 'prf (g 'impl st42))
3973
(g 'pdmemhist_2 (g 'impl st42))))
3974
(s_pc0_4 (g 'spc (g 'spec st43)))
3975
(s_rf0_4 (g 'srf (g 'spec st43)))
3976
(s_dmem0_4 (g 'sdmem (g 'spec st43)))
3977
(s_epc0_4 (g 'sepc (g 'spec st43)))
3979
(g 'sisexception (g 'spec st43)))
3980
(i_pc_4 (committedpc (g 'mwwrt (g 'impl st43))
3981
(g 'mwppc (g 'impl st43))
3982
(g 'mmwrt (g 'impl st43))
3983
(g 'mmppc (g 'impl st43))
3984
(g 'emwrt (g 'impl st43))
3985
(g 'emppc (g 'impl st43))
3986
(g 'dewrt (g 'impl st43))
3987
(g 'deppc (g 'impl st43))
3988
(g 'fdwrt (g 'impl st43))
3989
(g 'fdppc (g 'impl st43))
3990
(g 'ffwrt (g 'impl st43))
3991
(g 'ffppc (g 'impl st43))
3992
(g 'ppc (g 'impl st43))))
3993
(i_rf_4 (g 'prf (g 'impl st43)))
3994
(i_dmem_4 (g 'pdmemhist_2 (g 'impl st43)))
3995
(i_epc_4 (g 'pepchist_2 (g 'impl st43)))
3997
(g 'pisexceptionhist_2 (g 'impl st43)))
3999
(rank (g 'mwwrt (g 'impl st43)) zero
4000
(g 'mmwrt (g 'impl st43))
4001
(g 'emwrt (g 'impl st43))
4002
(g 'dewrt (g 'impl st43))
4003
(g 'fdwrt (g 'impl st43))
4004
(g 'ffwrt (g 'impl st43))))
4005
(st44 (simulate_a st43 nil t nil pc0 intrp0
4006
nil pc0 bpstate0 intrp0 pc0
4007
alu_exception_handler intrp0
4008
bpstate0 ffbpstate0 ffpintrp0
4009
ffpredicteddirection0
4010
ffpredictedtarget0 ffinst0 ffppc0
4011
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4012
fdpredicteddirection0
4013
fdpredictedtarget0 debpstate0
4014
depintrp0 deppc0 desrc10 desrc20 a1
4015
a2 dedest0 deop0 deimm0 deuseimm0
4016
deisreturnfromexception0 deregwrite0
4017
dememwrite0 dememtoreg0 deisbranch0
4018
depredicteddirection0
4019
depredictedtarget0 embpstate0
4020
empintrp0 emppc0 emis_alu_exception0
4021
emis_taken_branch0 emtargetpc0
4022
emarg20 emresult0 emdest0
4023
emisreturnfromexception0
4024
emmispredictedtaken0
4025
emmispredictednottaken0 emregwrite0
4026
emmemwrite0 emmemtoreg0 dmem0 epc0
4027
isexception0 mmbpstate0 mmpintrp0
4028
mmisreturnfromexception0
4029
mmis_alu_exception0 mmppc0 mmval0
4030
mmdest0 mmregwrite0 mwbpstate0
4031
mwpintrp0 mwisreturnfromexception0
4032
mwis_alu_exception0 mwppc0 mwval0
4034
(g 'prf (g 'impl st43))
4035
(g 'pdmemhist_2 (g 'impl st43))))
4036
(s_pc1_4 (g 'spc (g 'spec st44)))
4037
(s_rf1_4 (g 'srf (g 'spec st44)))
4038
(s_dmem1_4 (g 'sdmem (g 'spec st44)))
4039
(s_epc1_4 (g 'sepc (g 'spec st44)))
4041
(g 'sisexception (g 'spec st44)))
4042
(st45 (simulate_a st44 t nil nil pc0 intrp0
4043
nil pc0 bpstate0 intrp0 pc0
4044
alu_exception_handler intrp0
4045
bpstate0 ffbpstate0 ffpintrp0
4046
ffpredicteddirection0
4047
ffpredictedtarget0 ffinst0 ffppc0
4048
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4049
fdpredicteddirection0
4050
fdpredictedtarget0 debpstate0
4051
depintrp0 deppc0 desrc10 desrc20 a1
4052
a2 dedest0 deop0 deimm0 deuseimm0
4053
deisreturnfromexception0 deregwrite0
4054
dememwrite0 dememtoreg0 deisbranch0
4055
depredicteddirection0
4056
depredictedtarget0 embpstate0
4057
empintrp0 emppc0 emis_alu_exception0
4058
emis_taken_branch0 emtargetpc0
4059
emarg20 emresult0 emdest0
4060
emisreturnfromexception0
4061
emmispredictedtaken0
4062
emmispredictednottaken0 emregwrite0
4063
emmemwrite0 emmemtoreg0 dmem0 epc0
4064
isexception0 mmbpstate0 mmpintrp0
4065
mmisreturnfromexception0
4066
mmis_alu_exception0 mmppc0 mmval0
4067
mmdest0 mmregwrite0 mwbpstate0
4068
mwpintrp0 mwisreturnfromexception0
4069
mwis_alu_exception0 mwppc0 mwval0
4071
(g 'prf (g 'impl st44))
4072
(g 'pdmemhist_2 (g 'impl st44))))
4073
(st46 (simulate_a st45 nil nil nil pc0 intrp0
4074
nil pc0 bpstate0 intrp0 pc0
4075
alu_exception_handler intrp0
4076
bpstate0 ffbpstate0 ffpintrp0
4077
ffpredicteddirection0
4078
ffpredictedtarget0 ffinst0 ffppc0
4079
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4080
fdpredicteddirection0
4081
fdpredictedtarget0 debpstate0
4082
depintrp0 deppc0 desrc10 desrc20 a1
4083
a2 dedest0 deop0 deimm0 deuseimm0
4084
deisreturnfromexception0 deregwrite0
4085
dememwrite0 dememtoreg0 deisbranch0
4086
depredicteddirection0
4087
depredictedtarget0 embpstate0
4088
empintrp0 emppc0 emis_alu_exception0
4089
emis_taken_branch0 emtargetpc0
4090
emarg20 emresult0 emdest0
4091
emisreturnfromexception0
4092
emmispredictedtaken0
4093
emmispredictednottaken0 emregwrite0
4094
emmemwrite0 emmemtoreg0 dmem0 epc0
4095
isexception0 mmbpstate0 mmpintrp0
4096
mmisreturnfromexception0
4097
mmis_alu_exception0 mmppc0 mmval0
4098
mmdest0 mmregwrite0 mwbpstate0
4099
mwpintrp0 mwisreturnfromexception0
4100
mwis_alu_exception0 mwppc0 mwval0
4102
(g 'prf (g 'impl st45))
4103
(g 'pdmemhist_2 (g 'impl st45))))
4104
(st47 (simulate_a st46 nil nil nil pc0 intrp0
4105
nil pc0 bpstate0 intrp0 pc0
4106
alu_exception_handler intrp0
4107
bpstate0 ffbpstate0 ffpintrp0
4108
ffpredicteddirection0
4109
ffpredictedtarget0 ffinst0 ffppc0
4110
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4111
fdpredicteddirection0
4112
fdpredictedtarget0 debpstate0
4113
depintrp0 deppc0 desrc10 desrc20 a1
4114
a2 dedest0 deop0 deimm0 deuseimm0
4115
deisreturnfromexception0 deregwrite0
4116
dememwrite0 dememtoreg0 deisbranch0
4117
depredicteddirection0
4118
depredictedtarget0 embpstate0
4119
empintrp0 emppc0 emis_alu_exception0
4120
emis_taken_branch0 emtargetpc0
4121
emarg20 emresult0 emdest0
4122
emisreturnfromexception0
4123
emmispredictedtaken0
4124
emmispredictednottaken0 emregwrite0
4125
emmemwrite0 emmemtoreg0 dmem0 epc0
4126
isexception0 mmbpstate0 mmpintrp0
4127
mmisreturnfromexception0
4128
mmis_alu_exception0 mmppc0 mmval0
4129
mmdest0 mmregwrite0 mwbpstate0
4130
mwpintrp0 mwisreturnfromexception0
4131
mwis_alu_exception0 mwppc0 mwval0
4133
(g 'prf (g 'impl st46))
4134
(g 'pdmemhist_2 (g 'impl st46))))
4135
(i_pc0_5 (committedpc
4136
(g 'mwwrt (g 'impl st47))
4137
(g 'mwppc (g 'impl st47))
4138
(g 'mmwrt (g 'impl st47))
4139
(g 'mmppc (g 'impl st47))
4140
(g 'emwrt (g 'impl st47))
4141
(g 'emppc (g 'impl st47))
4142
(g 'dewrt (g 'impl st47))
4143
(g 'deppc (g 'impl st47))
4144
(g 'fdwrt (g 'impl st47))
4145
(g 'fdppc (g 'impl st47))
4146
(g 'ffwrt (g 'impl st47))
4147
(g 'ffppc (g 'impl st47))
4148
(g 'ppc (g 'impl st47))))
4149
(i_rf0_5 (g 'prf (g 'impl st47)))
4150
(i_dmem0_5 (g 'pdmemhist_2 (g 'impl st47)))
4151
(i_epc0_5 (g 'pepchist_2 (g 'impl st47)))
4153
(g 'pisexceptionhist_2 (g 'impl st47)))
4155
(rank (g 'mwwrt (g 'impl st47)) zero
4156
(g 'mmwrt (g 'impl st47))
4157
(g 'emwrt (g 'impl st47))
4158
(g 'dewrt (g 'impl st47))
4159
(g 'fdwrt (g 'impl st47))
4160
(g 'ffwrt (g 'impl st47))))
4161
(st48 (simulate_a st47 nil nil t i_pc0_5
4162
committedintrp nil pc0 bpstate0
4163
intrp0 pc0 alu_exception_handler
4164
intrp0 bpstate0 ffbpstate0 ffpintrp0
4165
ffpredicteddirection0
4166
ffpredictedtarget0 ffinst0 ffppc0
4167
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4168
fdpredicteddirection0
4169
fdpredictedtarget0 debpstate0
4170
depintrp0 deppc0 desrc10 desrc20 a1
4171
a2 dedest0 deop0 deimm0 deuseimm0
4172
deisreturnfromexception0 deregwrite0
4173
dememwrite0 dememtoreg0 deisbranch0
4174
depredicteddirection0
4175
depredictedtarget0 embpstate0
4176
empintrp0 emppc0 emis_alu_exception0
4177
emis_taken_branch0 emtargetpc0
4178
emarg20 emresult0 emdest0
4179
emisreturnfromexception0
4180
emmispredictedtaken0
4181
emmispredictednottaken0 emregwrite0
4182
emmemwrite0 emmemtoreg0 dmem0 epc0
4183
isexception0 mmbpstate0 mmpintrp0
4184
mmisreturnfromexception0
4185
mmis_alu_exception0 mmppc0 mmval0
4186
mmdest0 mmregwrite0 mwbpstate0
4187
mwpintrp0 mwisreturnfromexception0
4188
mwis_alu_exception0 mwppc0 mwval0
4190
(g 'prf (g 'impl st47))
4191
(g 'pdmemhist_2 (g 'impl st47))))
4192
(s_pc0_5 (g 'spc (g 'spec st48)))
4193
(s_rf0_5 (g 'srf (g 'spec st48)))
4194
(s_dmem0_5 (g 'sdmem (g 'spec st48)))
4195
(s_epc0_5 (g 'sepc (g 'spec st48)))
4197
(g 'sisexception (g 'spec st48)))
4198
(i_pc_5 (committedpc (g 'mwwrt (g 'impl st48))
4199
(g 'mwppc (g 'impl st48))
4200
(g 'mmwrt (g 'impl st48))
4201
(g 'mmppc (g 'impl st48))
4202
(g 'emwrt (g 'impl st48))
4203
(g 'emppc (g 'impl st48))
4204
(g 'dewrt (g 'impl st48))
4205
(g 'deppc (g 'impl st48))
4206
(g 'fdwrt (g 'impl st48))
4207
(g 'fdppc (g 'impl st48))
4208
(g 'ffwrt (g 'impl st48))
4209
(g 'ffppc (g 'impl st48))
4210
(g 'ppc (g 'impl st48))))
4211
(i_rf_5 (g 'prf (g 'impl st48)))
4212
(i_dmem_5 (g 'pdmemhist_2 (g 'impl st48)))
4213
(i_epc_5 (g 'pepchist_2 (g 'impl st48)))
4215
(g 'pisexceptionhist_2 (g 'impl st48)))
4217
(rank (g 'mwwrt (g 'impl st48)) zero
4218
(g 'mmwrt (g 'impl st48))
4219
(g 'emwrt (g 'impl st48))
4220
(g 'dewrt (g 'impl st48))
4221
(g 'fdwrt (g 'impl st48))
4222
(g 'ffwrt (g 'impl st48))))
4223
(st49 (simulate_a st48 nil t nil pc0 intrp0
4224
nil pc0 bpstate0 intrp0 pc0
4225
alu_exception_handler intrp0
4226
bpstate0 ffbpstate0 ffpintrp0
4227
ffpredicteddirection0
4228
ffpredictedtarget0 ffinst0 ffppc0
4229
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4230
fdpredicteddirection0
4231
fdpredictedtarget0 debpstate0
4232
depintrp0 deppc0 desrc10 desrc20 a1
4233
a2 dedest0 deop0 deimm0 deuseimm0
4234
deisreturnfromexception0 deregwrite0
4235
dememwrite0 dememtoreg0 deisbranch0
4236
depredicteddirection0
4237
depredictedtarget0 embpstate0
4238
empintrp0 emppc0 emis_alu_exception0
4239
emis_taken_branch0 emtargetpc0
4240
emarg20 emresult0 emdest0
4241
emisreturnfromexception0
4242
emmispredictedtaken0
4243
emmispredictednottaken0 emregwrite0
4244
emmemwrite0 emmemtoreg0 dmem0 epc0
4245
isexception0 mmbpstate0 mmpintrp0
4246
mmisreturnfromexception0
4247
mmis_alu_exception0 mmppc0 mmval0
4248
mmdest0 mmregwrite0 mwbpstate0
4249
mwpintrp0 mwisreturnfromexception0
4250
mwis_alu_exception0 mwppc0 mwval0
4252
(g 'prf (g 'impl st48))
4253
(g 'pdmemhist_2 (g 'impl st48))))
4254
(s_pc1_5 (g 'spc (g 'spec st49)))
4255
(s_rf1_5 (g 'srf (g 'spec st49)))
4256
(s_dmem1_5 (g 'sdmem (g 'spec st49)))
4257
(s_epc1_5 (g 'sepc (g 'spec st49)))
4259
(g 'sisexception (g 'spec st49)))
4260
(st50 (simulate_a st49 t nil nil pc0 intrp0
4261
nil pc0 bpstate0 intrp0 pc0
4262
alu_exception_handler intrp0
4263
bpstate0 ffbpstate0 ffpintrp0
4264
ffpredicteddirection0
4265
ffpredictedtarget0 ffinst0 ffppc0
4266
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4267
fdpredicteddirection0
4268
fdpredictedtarget0 debpstate0
4269
depintrp0 deppc0 desrc10 desrc20 a1
4270
a2 dedest0 deop0 deimm0 deuseimm0
4271
deisreturnfromexception0 deregwrite0
4272
dememwrite0 dememtoreg0 deisbranch0
4273
depredicteddirection0
4274
depredictedtarget0 embpstate0
4275
empintrp0 emppc0 emis_alu_exception0
4276
emis_taken_branch0 emtargetpc0
4277
emarg20 emresult0 emdest0
4278
emisreturnfromexception0
4279
emmispredictedtaken0
4280
emmispredictednottaken0 emregwrite0
4281
emmemwrite0 emmemtoreg0 dmem0 epc0
4282
isexception0 mmbpstate0 mmpintrp0
4283
mmisreturnfromexception0
4284
mmis_alu_exception0 mmppc0 mmval0
4285
mmdest0 mmregwrite0 mwbpstate0
4286
mwpintrp0 mwisreturnfromexception0
4287
mwis_alu_exception0 mwppc0 mwval0
4289
(g 'prf (g 'impl st49))
4290
(g 'pdmemhist_2 (g 'impl st49))))
4291
(st51 (simulate_a st50 nil nil nil pc0 intrp0
4292
nil pc0 bpstate0 intrp0 pc0
4293
alu_exception_handler intrp0
4294
bpstate0 ffbpstate0 ffpintrp0
4295
ffpredicteddirection0
4296
ffpredictedtarget0 ffinst0 ffppc0
4297
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4298
fdpredicteddirection0
4299
fdpredictedtarget0 debpstate0
4300
depintrp0 deppc0 desrc10 desrc20 a1
4301
a2 dedest0 deop0 deimm0 deuseimm0
4302
deisreturnfromexception0 deregwrite0
4303
dememwrite0 dememtoreg0 deisbranch0
4304
depredicteddirection0
4305
depredictedtarget0 embpstate0
4306
empintrp0 emppc0 emis_alu_exception0
4307
emis_taken_branch0 emtargetpc0
4308
emarg20 emresult0 emdest0
4309
emisreturnfromexception0
4310
emmispredictedtaken0
4311
emmispredictednottaken0 emregwrite0
4312
emmemwrite0 emmemtoreg0 dmem0 epc0
4313
isexception0 mmbpstate0 mmpintrp0
4314
mmisreturnfromexception0
4315
mmis_alu_exception0 mmppc0 mmval0
4316
mmdest0 mmregwrite0 mwbpstate0
4317
mwpintrp0 mwisreturnfromexception0
4318
mwis_alu_exception0 mwppc0 mwval0
4320
(g 'prf (g 'impl st50))
4321
(g 'pdmemhist_2 (g 'impl st50))))
4322
(i_pc0_6 (committedpc
4323
(g 'mwwrt (g 'impl st51))
4324
(g 'mwppc (g 'impl st51))
4325
(g 'mmwrt (g 'impl st51))
4326
(g 'mmppc (g 'impl st51))
4327
(g 'emwrt (g 'impl st51))
4328
(g 'emppc (g 'impl st51))
4329
(g 'dewrt (g 'impl st51))
4330
(g 'deppc (g 'impl st51))
4331
(g 'fdwrt (g 'impl st51))
4332
(g 'fdppc (g 'impl st51))
4333
(g 'ffwrt (g 'impl st51))
4334
(g 'ffppc (g 'impl st51))
4335
(g 'ppc (g 'impl st51))))
4336
(i_rf0_6 (g 'prf (g 'impl st51)))
4337
(i_dmem0_6 (g 'pdmemhist_2 (g 'impl st51)))
4338
(i_epc0_6 (g 'pepchist_2 (g 'impl st51)))
4340
(g 'pisexceptionhist_2 (g 'impl st51)))
4342
(rank (g 'mwwrt (g 'impl st51)) zero
4343
(g 'mmwrt (g 'impl st51))
4344
(g 'emwrt (g 'impl st51))
4345
(g 'dewrt (g 'impl st51))
4346
(g 'fdwrt (g 'impl st51))
4347
(g 'ffwrt (g 'impl st51))))
4348
(st52 (simulate_a st51 nil nil t i_pc0_6
4349
committedintrp nil pc0 bpstate0
4350
intrp0 pc0 alu_exception_handler
4351
intrp0 bpstate0 ffbpstate0 ffpintrp0
4352
ffpredicteddirection0
4353
ffpredictedtarget0 ffinst0 ffppc0
4354
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4355
fdpredicteddirection0
4356
fdpredictedtarget0 debpstate0
4357
depintrp0 deppc0 desrc10 desrc20 a1
4358
a2 dedest0 deop0 deimm0 deuseimm0
4359
deisreturnfromexception0 deregwrite0
4360
dememwrite0 dememtoreg0 deisbranch0
4361
depredicteddirection0
4362
depredictedtarget0 embpstate0
4363
empintrp0 emppc0 emis_alu_exception0
4364
emis_taken_branch0 emtargetpc0
4365
emarg20 emresult0 emdest0
4366
emisreturnfromexception0
4367
emmispredictedtaken0
4368
emmispredictednottaken0 emregwrite0
4369
emmemwrite0 emmemtoreg0 dmem0 epc0
4370
isexception0 mmbpstate0 mmpintrp0
4371
mmisreturnfromexception0
4372
mmis_alu_exception0 mmppc0 mmval0
4373
mmdest0 mmregwrite0 mwbpstate0
4374
mwpintrp0 mwisreturnfromexception0
4375
mwis_alu_exception0 mwppc0 mwval0
4377
(g 'prf (g 'impl st51))
4378
(g 'pdmemhist_2 (g 'impl st51))))
4379
(s_pc0_6 (g 'spc (g 'spec st52)))
4380
(s_rf0_6 (g 'srf (g 'spec st52)))
4381
(s_dmem0_6 (g 'sdmem (g 'spec st52)))
4382
(s_epc0_6 (g 'sepc (g 'spec st52)))
4384
(g 'sisexception (g 'spec st52)))
4385
(i_pc_6 (committedpc (g 'mwwrt (g 'impl st52))
4386
(g 'mwppc (g 'impl st52))
4387
(g 'mmwrt (g 'impl st52))
4388
(g 'mmppc (g 'impl st52))
4389
(g 'emwrt (g 'impl st52))
4390
(g 'emppc (g 'impl st52))
4391
(g 'dewrt (g 'impl st52))
4392
(g 'deppc (g 'impl st52))
4393
(g 'fdwrt (g 'impl st52))
4394
(g 'fdppc (g 'impl st52))
4395
(g 'ffwrt (g 'impl st52))
4396
(g 'ffppc (g 'impl st52))
4397
(g 'ppc (g 'impl st52))))
4398
(i_rf_6 (g 'prf (g 'impl st52)))
4399
(i_dmem_6 (g 'pdmemhist_2 (g 'impl st52)))
4400
(i_epc_6 (g 'pepchist_2 (g 'impl st52)))
4402
(g 'pisexceptionhist_2 (g 'impl st52)))
4404
(rank (g 'mwwrt (g 'impl st52)) zero
4405
(g 'mmwrt (g 'impl st52))
4406
(g 'emwrt (g 'impl st52))
4407
(g 'dewrt (g 'impl st52))
4408
(g 'fdwrt (g 'impl st52))
4409
(g 'ffwrt (g 'impl st52))))
4410
(st53 (simulate_a st52 nil t nil pc0 intrp0
4411
nil pc0 bpstate0 intrp0 pc0
4412
alu_exception_handler intrp0
4413
bpstate0 ffbpstate0 ffpintrp0
4414
ffpredicteddirection0
4415
ffpredictedtarget0 ffinst0 ffppc0
4416
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4417
fdpredicteddirection0
4418
fdpredictedtarget0 debpstate0
4419
depintrp0 deppc0 desrc10 desrc20 a1
4420
a2 dedest0 deop0 deimm0 deuseimm0
4421
deisreturnfromexception0 deregwrite0
4422
dememwrite0 dememtoreg0 deisbranch0
4423
depredicteddirection0
4424
depredictedtarget0 embpstate0
4425
empintrp0 emppc0 emis_alu_exception0
4426
emis_taken_branch0 emtargetpc0
4427
emarg20 emresult0 emdest0
4428
emisreturnfromexception0
4429
emmispredictedtaken0
4430
emmispredictednottaken0 emregwrite0
4431
emmemwrite0 emmemtoreg0 dmem0 epc0
4432
isexception0 mmbpstate0 mmpintrp0
4433
mmisreturnfromexception0
4434
mmis_alu_exception0 mmppc0 mmval0
4435
mmdest0 mmregwrite0 mwbpstate0
4436
mwpintrp0 mwisreturnfromexception0
4437
mwis_alu_exception0 mwppc0 mwval0
4439
(g 'prf (g 'impl st52))
4440
(g 'pdmemhist_2 (g 'impl st52))))
4441
(s_pc1_6 (g 'spc (g 'spec st53)))
4442
(s_rf1_6 (g 'srf (g 'spec st53)))
4443
(s_dmem1_6 (g 'sdmem (g 'spec st53)))
4444
(s_epc1_6 (g 'sepc (g 'spec st53)))
4446
(g 'sisexception (g 'spec st53)))
4447
(st54 (simulate_a st53 t nil nil pc0 intrp0
4448
nil pc0 bpstate0 intrp0 pc0
4449
alu_exception_handler intrp0
4450
bpstate0 ffbpstate0 ffpintrp0
4451
ffpredicteddirection0
4452
ffpredictedtarget0 ffinst0 ffppc0
4453
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4454
fdpredicteddirection0
4455
fdpredictedtarget0 debpstate0
4456
depintrp0 deppc0 desrc10 desrc20 a1
4457
a2 dedest0 deop0 deimm0 deuseimm0
4458
deisreturnfromexception0 deregwrite0
4459
dememwrite0 dememtoreg0 deisbranch0
4460
depredicteddirection0
4461
depredictedtarget0 embpstate0
4462
empintrp0 emppc0 emis_alu_exception0
4463
emis_taken_branch0 emtargetpc0
4464
emarg20 emresult0 emdest0
4465
emisreturnfromexception0
4466
emmispredictedtaken0
4467
emmispredictednottaken0 emregwrite0
4468
emmemwrite0 emmemtoreg0 dmem0 epc0
4469
isexception0 mmbpstate0 mmpintrp0
4470
mmisreturnfromexception0
4471
mmis_alu_exception0 mmppc0 mmval0
4472
mmdest0 mmregwrite0 mwbpstate0
4473
mwpintrp0 mwisreturnfromexception0
4474
mwis_alu_exception0 mwppc0 mwval0
4476
(g 'prf (g 'impl st53))
4477
(g 'pdmemhist_2 (g 'impl st53))))
4478
(i_pc0_7 (committedpc
4479
(g 'mwwrt (g 'impl st54))
4480
(g 'mwppc (g 'impl st54))
4481
(g 'mmwrt (g 'impl st54))
4482
(g 'mmppc (g 'impl st54))
4483
(g 'emwrt (g 'impl st54))
4484
(g 'emppc (g 'impl st54))
4485
(g 'dewrt (g 'impl st54))
4486
(g 'deppc (g 'impl st54))
4487
(g 'fdwrt (g 'impl st54))
4488
(g 'fdppc (g 'impl st54))
4489
(g 'ffwrt (g 'impl st54))
4490
(g 'ffppc (g 'impl st54))
4491
(g 'ppc (g 'impl st54))))
4492
(i_rf0_7 (g 'prf (g 'impl st54)))
4493
(i_dmem0_7 (g 'pdmemhist_2 (g 'impl st54)))
4494
(i_epc0_7 (g 'pepchist_2 (g 'impl st54)))
4496
(g 'pisexceptionhist_2 (g 'impl st54)))
4498
(rank (g 'mwwrt (g 'impl st54)) zero
4499
(g 'mmwrt (g 'impl st54))
4500
(g 'emwrt (g 'impl st54))
4501
(g 'dewrt (g 'impl st54))
4502
(g 'fdwrt (g 'impl st54))
4503
(g 'ffwrt (g 'impl st54))))
4504
(st55 (simulate_a st54 nil nil t i_pc0_7
4505
committedintrp nil pc0 bpstate0
4506
intrp0 pc0 alu_exception_handler
4507
intrp0 bpstate0 ffbpstate0 ffpintrp0
4508
ffpredicteddirection0
4509
ffpredictedtarget0 ffinst0 ffppc0
4510
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4511
fdpredicteddirection0
4512
fdpredictedtarget0 debpstate0
4513
depintrp0 deppc0 desrc10 desrc20 a1
4514
a2 dedest0 deop0 deimm0 deuseimm0
4515
deisreturnfromexception0 deregwrite0
4516
dememwrite0 dememtoreg0 deisbranch0
4517
depredicteddirection0
4518
depredictedtarget0 embpstate0
4519
empintrp0 emppc0 emis_alu_exception0
4520
emis_taken_branch0 emtargetpc0
4521
emarg20 emresult0 emdest0
4522
emisreturnfromexception0
4523
emmispredictedtaken0
4524
emmispredictednottaken0 emregwrite0
4525
emmemwrite0 emmemtoreg0 dmem0 epc0
4526
isexception0 mmbpstate0 mmpintrp0
4527
mmisreturnfromexception0
4528
mmis_alu_exception0 mmppc0 mmval0
4529
mmdest0 mmregwrite0 mwbpstate0
4530
mwpintrp0 mwisreturnfromexception0
4531
mwis_alu_exception0 mwppc0 mwval0
4533
(g 'prf (g 'impl st54))
4534
(g 'pdmemhist_2 (g 'impl st54))))
4535
(s_pc0_7 (g 'spc (g 'spec st55)))
4536
(s_rf0_7 (g 'srf (g 'spec st55)))
4537
(s_dmem0_7 (g 'sdmem (g 'spec st55)))
4538
(s_epc0_7 (g 'sepc (g 'spec st55)))
4540
(g 'sisexception (g 'spec st55)))
4541
(i_pc_7 (committedpc (g 'mwwrt (g 'impl st55))
4542
(g 'mwppc (g 'impl st55))
4543
(g 'mmwrt (g 'impl st55))
4544
(g 'mmppc (g 'impl st55))
4545
(g 'emwrt (g 'impl st55))
4546
(g 'emppc (g 'impl st55))
4547
(g 'dewrt (g 'impl st55))
4548
(g 'deppc (g 'impl st55))
4549
(g 'fdwrt (g 'impl st55))
4550
(g 'fdppc (g 'impl st55))
4551
(g 'ffwrt (g 'impl st55))
4552
(g 'ffppc (g 'impl st55))
4553
(g 'ppc (g 'impl st55))))
4554
(i_rf_7 (g 'prf (g 'impl st55)))
4555
(i_dmem_7 (g 'pdmemhist_2 (g 'impl st55)))
4556
(i_epc_7 (g 'pepchist_2 (g 'impl st55)))
4558
(g 'pisexceptionhist_2 (g 'impl st55)))
4560
(rank (g 'mwwrt (g 'impl st55)) zero
4561
(g 'mmwrt (g 'impl st55))
4562
(g 'emwrt (g 'impl st55))
4563
(g 'dewrt (g 'impl st55))
4564
(g 'fdwrt (g 'impl st55))
4565
(g 'ffwrt (g 'impl st55))))
4566
(st56 (simulate_a st55 nil t nil pc0 intrp0
4567
nil pc0 bpstate0 intrp0 pc0
4568
alu_exception_handler intrp0
4569
bpstate0 ffbpstate0 ffpintrp0
4570
ffpredicteddirection0
4571
ffpredictedtarget0 ffinst0 ffppc0
4572
fdpintrp0 fdbpstate0 fdppc0 fdinst0
4573
fdpredicteddirection0
4574
fdpredictedtarget0 debpstate0
4575
depintrp0 deppc0 desrc10 desrc20 a1
4576
a2 dedest0 deop0 deimm0 deuseimm0
4577
deisreturnfromexception0 deregwrite0
4578
dememwrite0 dememtoreg0 deisbranch0
4579
depredicteddirection0
4580
depredictedtarget0 embpstate0
4581
empintrp0 emppc0 emis_alu_exception0
4582
emis_taken_branch0 emtargetpc0
4583
emarg20 emresult0 emdest0
4584
emisreturnfromexception0
4585
emmispredictedtaken0
4586
emmispredictednottaken0 emregwrite0
4587
emmemwrite0 emmemtoreg0 dmem0 epc0
4588
isexception0 mmbpstate0 mmpintrp0
4589
mmisreturnfromexception0
4590
mmis_alu_exception0 mmppc0 mmval0
4591
mmdest0 mmregwrite0 mwbpstate0
4592
mwpintrp0 mwisreturnfromexception0
4593
mwis_alu_exception0 mwppc0 mwval0
4595
(g 'prf (g 'impl st55))
4596
(g 'pdmemhist_2 (g 'impl st55))))
4597
(s_pc1_7 (g 'spc (g 'spec st56)))
4598
(s_rf1_7 (g 'srf (g 'spec st56)))
4599
(s_dmem1_7 (g 'sdmem (g 'spec st56)))
4600
(s_epc1_7 (g 'sepc (g 'spec st56)))
4602
(g 'sisexception (g 'spec st56))))
4613
(and (equal s_pc0 i_pc0)
4615
(read-srf_a a1 s_rf0)
4616
(read-prf_a a1 i_rf0)))
4617
(equal s_dmem0 i_dmem0))
4618
(equal s_epc0 i_epc0))
4619
(equalb s_isexception0
4624
(and (equal s_pc1 i_pc)
4626
(read-srf_a a1 s_rf1)
4627
(read-prf_a a1 i_rf)))
4628
(equal s_dmem1 i_dmem))
4629
(equal s_epc1 i_epc))
4630
(equalb s_isexception1
4636
(and (equal s_pc0 i_pc)
4638
(read-srf_a a1 s_rf0)
4639
(read-prf_a a1 i_rf)))
4640
(equal s_dmem0 i_dmem))
4641
(equal s_epc0 i_epc))
4642
(equalb s_isexception0
4644
(< rank_v rank_w))))
4652
(equal s_pc0_2 i_pc0_2)
4654
(read-srf_a a1 s_rf0_2)
4655
(read-prf_a a1 i_rf0_2)))
4656
(equal s_dmem0_2 i_dmem0_2))
4657
(equal s_epc0_2 i_epc0_2))
4658
(equalb s_isexception0_2
4663
(and (equal s_pc1_2 i_pc_2)
4665
(read-srf_a a1 s_rf1_2)
4666
(read-prf_a a1 i_rf_2)))
4667
(equal s_dmem1_2 i_dmem_2))
4668
(equal s_epc1_2 i_epc_2))
4669
(equalb s_isexception1_2
4675
(and (equal s_pc0_2 i_pc_2)
4677
(read-srf_a a1 s_rf0_2)
4678
(read-prf_a a1 i_rf_2)))
4679
(equal s_dmem0_2 i_dmem_2))
4680
(equal s_epc0_2 i_epc_2))
4681
(equalb s_isexception0_2
4683
(< rank_v_2 rank_w_2))))
4690
(and (equal s_pc0_3 i_pc0_3)
4692
(read-srf_a a1 s_rf0_3)
4693
(read-prf_a a1 i_rf0_3)))
4694
(equal s_dmem0_3 i_dmem0_3))
4695
(equal s_epc0_3 i_epc0_3))
4696
(equalb s_isexception0_3
4701
(and (equal s_pc1_3 i_pc_3)
4703
(read-srf_a a1 s_rf1_3)
4704
(read-prf_a a1 i_rf_3)))
4705
(equal s_dmem1_3 i_dmem_3))
4706
(equal s_epc1_3 i_epc_3))
4707
(equalb s_isexception1_3
4713
(and (equal s_pc0_3 i_pc_3)
4715
(read-srf_a a1 s_rf0_3)
4716
(read-prf_a a1 i_rf_3)))
4717
(equal s_dmem0_3 i_dmem_3))
4718
(equal s_epc0_3 i_epc_3))
4719
(equalb s_isexception0_3
4721
(< rank_v_3 rank_w_3))))
4728
(and (equal s_pc0_4 i_pc0_4)
4730
(read-srf_a a1 s_rf0_4)
4731
(read-prf_a a1 i_rf0_4)))
4732
(equal s_dmem0_4 i_dmem0_4))
4733
(equal s_epc0_4 i_epc0_4))
4734
(equalb s_isexception0_4
4739
(and (equal s_pc1_4 i_pc_4)
4741
(read-srf_a a1 s_rf1_4)
4742
(read-prf_a a1 i_rf_4)))
4743
(equal s_dmem1_4 i_dmem_4))
4744
(equal s_epc1_4 i_epc_4))
4745
(equalb s_isexception1_4
4751
(and (equal s_pc0_4 i_pc_4)
4753
(read-srf_a a1 s_rf0_4)
4754
(read-prf_a a1 i_rf_4)))
4755
(equal s_dmem0_4 i_dmem_4))
4756
(equal s_epc0_4 i_epc_4))
4757
(equalb s_isexception0_4
4759
(< rank_v_4 rank_w_4))))
4766
(and (equal s_pc0_5 i_pc0_5)
4768
(read-srf_a a1 s_rf0_5)
4769
(read-prf_a a1 i_rf0_5)))
4770
(equal s_dmem0_5 i_dmem0_5))
4771
(equal s_epc0_5 i_epc0_5))
4772
(equalb s_isexception0_5
4777
(and (equal s_pc1_5 i_pc_5)
4778
(equal (read-srf_a a1 s_rf1_5)
4779
(read-prf_a a1 i_rf_5)))
4780
(equal s_dmem1_5 i_dmem_5))
4781
(equal s_epc1_5 i_epc_5))
4782
(equalb s_isexception1_5
4788
(and (equal s_pc0_5 i_pc_5)
4789
(equal (read-srf_a a1 s_rf0_5)
4790
(read-prf_a a1 i_rf_5)))
4791
(equal s_dmem0_5 i_dmem_5))
4792
(equal s_epc0_5 i_epc_5))
4793
(equalb s_isexception0_5
4795
(< rank_v_5 rank_w_5))))
4800
(and (equal s_pc0_6 i_pc0_6)
4802
(read-srf_a a1 s_rf0_6)
4803
(read-prf_a a1 i_rf0_6)))
4804
(equal s_dmem0_6 i_dmem0_6))
4805
(equal s_epc0_6 i_epc0_6))
4806
(equalb s_isexception0_6
4811
(and (equal s_pc1_6 i_pc_6)
4813
(read-srf_a a1 s_rf1_6)
4814
(read-prf_a a1 i_rf_6)))
4815
(equal s_dmem1_6 i_dmem_6))
4816
(equal s_epc1_6 i_epc_6))
4817
(equalb s_isexception1_6
4822
(and (equal s_pc0_6 i_pc_6)
4824
(read-srf_a a1 s_rf0_6)
4825
(read-prf_a a1 i_rf_6)))
4826
(equal s_dmem0_6 i_dmem_6))
4827
(equal s_epc0_6 i_epc_6))
4828
(equalb s_isexception0_6
4830
(< rank_v_6 rank_w_6))))
4834
(and (equal s_pc0_7 i_pc0_7)
4836
(read-srf_a a1 s_rf0_7)
4837
(read-prf_a a1 i_rf0_7)))
4838
(equal s_dmem0_7 i_dmem0_7))
4839
(equal s_epc0_7 i_epc0_7))
4840
(equalb s_isexception0_7
4844
(and (equal s_pc1_7 i_pc_7)
4845
(equal (read-srf_a a1 s_rf1_7)
4846
(read-prf_a a1 i_rf_7)))
4847
(equal s_dmem1_7 i_dmem_7))
4848
(equal s_epc1_7 i_epc_7))
4849
(equalb s_isexception1_7
4853
(and (equal s_pc0_7 i_pc_7)
4855
(read-srf_a a1 s_rf0_7)
4856
(read-prf_a a1 i_rf_7)))
4857
(equal s_dmem0_7 i_dmem_7))
4858
(equal s_epc0_7 i_epc_7))
4859
(equalb s_isexception0_7
4861
(< rank_v_7 rank_w_7))))))
added
removed
books/workshops/2004/manolios-srinivasan/support/Benchmark-Problems/cxs-bp-ex-inp.lisp
