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
10
(defun equalb (a b) (equal a b))
12
(defun nequal (a b) (not (equal a b))) (defun add-1 (a) (+ a 1))
14
(defun sub-1 (a) (- a 1))
16
(encapsulate ((nextdmem (x3 x2 x1) t))
17
(local (defun nextdmem (x3 x2 x1)
18
(declare (ignore x3) (ignore x2) (ignore x1))
20
(defthm nextdmem-type (integerp (nextdmem x3 x2 x1))))
22
(encapsulate ((dmem_read (x2 x1) t))
23
(local (defun dmem_read (x2 x1)
24
(declare (ignore x2) (ignore x1))
26
(defthm dmem_read-type (integerp (dmem_read x2 x1))))
28
(encapsulate ((rf0 (x1) t))
29
(local (defun rf0 (x1) (declare (ignore x1)) 1))
30
(defthm rf0-type (integerp (rf0 x1))))
32
(encapsulate ((imem0 (x1) t))
33
(local (defun imem0 (x1) (declare (ignore x1)) 1))
34
(defthm imem0-type (integerp (imem0 x1))))
36
(encapsulate ((src1 (x1) t))
37
(local (defun src1 (x1) (declare (ignore x1)) 1))
38
(defthm src1-type (integerp (src1 x1))))
40
(encapsulate ((src2 (x1) t))
41
(local (defun src2 (x1) (declare (ignore x1)) 1))
42
(defthm src2-type (integerp (src2 x1))))
44
(encapsulate ((opcode (x1) t))
45
(local (defun opcode (x1) (declare (ignore x1)) 1))
46
(defthm op-type (integerp (opcode x1))))
48
(encapsulate ((dest (x1) t))
49
(local (defun dest (x1) (declare (ignore x1)) 1))
50
(defthm dest-type (integerp (dest x1))))
52
(encapsulate ((alu (x3 x2 x1) t))
53
(local (defun alu (x3 x2 x1)
54
(declare (ignore x3) (ignore x2) (ignore x1))
56
(defthm alu-type (integerp (alu x3 x2 x1))))
58
(encapsulate ((getregwrite (x1) t))
59
(local (defun getregwrite (x1) (declare (ignore x1)) nil))
60
(defthm getregwrite-type (booleanp (getregwrite x1))))
62
(encapsulate ((getmemtoreg (x1) t))
63
(local (defun getmemtoreg (x1) (declare (ignore x1)) nil))
64
(defthm getmemtoreg-type (booleanp (getmemtoreg x1))))
66
(encapsulate ((getuseimm (x1) t))
67
(local (defun getuseimm (x1) (declare (ignore x1)) nil))
68
(defthm getuseimm-type (booleanp (getuseimm x1))))
70
(encapsulate ((getimm (x1) t))
71
(local (defun getimm (x1) (declare (ignore x1)) 1))
72
(defthm getimm-type (integerp (getimm x1))))
74
(encapsulate ((getmemwrite (x1) t))
75
(local (defun getmemwrite (x1) (declare (ignore x1)) nil))
76
(defthm getmemwrite-type (booleanp (getmemwrite x1))))
78
(encapsulate ((getisbranch (x1) t))
79
(local (defun getisbranch (x1) (declare (ignore x1)) nil))
80
(defthm getisbranch-type (booleanp (getisbranch x1))))
82
(encapsulate ((takebranch (x3 x2 x1) t))
83
(local (defun takebranch (x3 x2 x1)
84
(declare (ignore x3) (ignore x2) (ignore x1))
86
(defthm takebranch-type (booleanp (takebranch x3 x2 x1))))
88
(encapsulate ((selecttargetpc (x3 x2 x1) t))
89
(local (defun selecttargetpc (x3 x2 x1)
90
(declare (ignore x3) (ignore x2) (ignore x1))
92
(defthm selecttargetpc-type (integerp (selecttargetpc x3 x2 x1))))
94
(encapsulate ((nextbpstate (x1) t))
95
(local (defun nextbpstate (x1) (declare (ignore x1)) 1))
96
(defthm nextbpstate-type (integerp (nextbpstate x1))))
98
(encapsulate ((predictdirection (x1) t))
99
(local (defun predictdirection (x1) (declare (ignore x1)) nil))
100
(defthm predictdirection-type (booleanp (predictdirection x1))))
102
(encapsulate ((predicttarget (x1) t))
103
(local (defun predicttarget (x1) (declare (ignore x1)) 1))
104
(defthm predicttarget-type (integerp (predicttarget x1))))
106
(defun read-pimem_a (a pimem)
107
(declare (xargs :measure (acl2-count pimem)))
108
(if (endp pimem) (imem0 a)
109
(if (g 0 (car pimem)) (imem0 a) (read-pimem_a a (cdr pimem)))))
111
(defun read-prf_a (a prf)
112
(declare (xargs :measure (acl2-count prf)))
113
(if (endp prf) (rf0 a)
114
(if (g 0 (car prf)) (rf0 a)
116
((g 1 (car prf)) (rf0 a))
117
((and (and (g 2 (car prf)) (equal a (g 3 (car prf))))
120
(t (read-prf_a a (cdr prf)))))))
122
(defun read-simem_a (a simem)
123
(declare (xargs :measure (acl2-count simem)))
124
(if (endp simem) (imem0 a)
125
(if (g 0 (car simem)) (imem0 a)
127
((g 1 (car simem)) (imem0 a))
128
(t (read-simem_a a (cdr simem)))))))
130
(defun read-srf_a (a srf)
131
(declare (xargs :measure (acl2-count srf)))
132
(if (endp srf) (rf0 a)
133
(if (g 0 (car srf)) (rf0 a)
135
((g 1 (car srf)) (rf0 a))
136
((g 2 (car srf)) (read-prf_a a (g 3 (car srf))))
137
((and (and (g 4 (car srf))
138
(equal a (dest (g 5 (car srf)))))
141
(t (read-srf_a a (cdr srf)))))))
143
(defun u-state_a (impl spec) (seq nil 'impl impl 'spec spec))
146
(pimem ppc bpstate ffpredicteddirection ffpredictedtarget ffwrt
147
ffinst ffppc prf fdppc fdwrt fdinst fdpredicteddirection
148
fdpredictedtarget deppc desrc1 desrc2 dearg1 dearg2
149
dedest deop deimm deuseimm deregwrite dememwrite
150
dememtoreg deisbranch dewrt depredicteddirection
151
depredictedtarget emppc emis_taken_branch emtargetpc
152
emarg2 emresult emdest emwrt emmispredictedtaken
153
emmispredictednottaken emregwrite emmemwrite emmemtoreg
154
pdmemhist_2 pdmemhist_1 pdmem mmppc mmval mmdest mmwrt
155
mmregwrite mwppc mwval mwdest mwwrt mwregwrite)
156
(seq nil 'pimem pimem 'ppc ppc 'bpstate bpstate
157
'ffpredicteddirection ffpredicteddirection 'ffpredictedtarget
158
ffpredictedtarget 'ffwrt ffwrt 'ffinst ffinst 'ffppc ffppc 'prf
159
prf 'fdppc fdppc 'fdwrt fdwrt 'fdinst fdinst
160
'fdpredicteddirection fdpredicteddirection 'fdpredictedtarget
161
fdpredictedtarget 'deppc deppc 'desrc1 desrc1 'desrc2 desrc2
162
'dearg1 dearg1 'dearg2 dearg2 'dedest dedest 'deop deop 'deimm
163
deimm 'deuseimm deuseimm 'deregwrite deregwrite 'dememwrite
164
dememwrite 'dememtoreg dememtoreg 'deisbranch deisbranch 'dewrt
165
dewrt 'depredicteddirection depredicteddirection
166
'depredictedtarget depredictedtarget 'emppc emppc
167
'emis_taken_branch emis_taken_branch 'emtargetpc emtargetpc
168
'emarg2 emarg2 'emresult emresult 'emdest emdest 'emwrt emwrt
169
'emmispredictedtaken emmispredictedtaken
170
'emmispredictednottaken emmispredictednottaken 'emregwrite
171
emregwrite 'emmemwrite emmemwrite 'emmemtoreg emmemtoreg
172
'pdmemhist_2 pdmemhist_2 'pdmemhist_1 pdmemhist_1 'pdmem pdmem
173
'mmppc mmppc 'mmval mmval 'mmdest mmdest 'mmwrt mmwrt
174
'mmregwrite mmregwrite 'mwppc mwppc 'mwval mwval 'mwdest mwdest
175
'mwwrt mwwrt 'mwregwrite mwregwrite))
177
(defun initpimem_a (pimem) (cons (s 0 t (s 1 nil nil)) pimem))
179
(defun nextpimem_a (pimem) (cons (s 0 nil (s 1 nil nil)) pimem))
181
(defun initppc_a (pc0) pc0)
184
(initi pc0 mem1_mispredicted_taken emppc
185
mem1_mispredicted_nottaken emtargetpc stall flush ppc
186
if_predict_branch_taken predicted_target)
189
(mem1_mispredicted_taken emppc)
190
(mem1_mispredicted_nottaken emtargetpc)
191
((or stall flush) ppc)
192
(if_predict_branch_taken predicted_target)
195
(defun initbpstate_a (bpstate0) bpstate0)
197
(defun nextbpstate_a (initi bpstate0 stall bpstate)
198
(cond (initi bpstate0) (stall bpstate) (t (nextbpstate bpstate))))
200
(defun initffpredicteddirection_a (ffpredicteddirection0)
201
ffpredicteddirection0)
203
(defun nextffpredicteddirection_a
204
(initi ffpredicteddirection0 stall ffpredicteddirection
205
if_predict_branch_taken)
207
(initi ffpredicteddirection0)
208
(stall ffpredicteddirection)
209
(t if_predict_branch_taken)))
211
(defun initffpredictedtarget_a (ffpredictedtarget0)
214
(defun nextffpredictedtarget_a
215
(initi ffpredictedtarget0 stall ffpredictedtarget
218
(initi ffpredictedtarget0)
219
(stall ffpredictedtarget)
220
(t predicted_target)))
222
(defun initffwrt_a (ffwrt0) ffwrt0)
224
(defun nextffwrt_a (initi ffwrt0 squash stall ffwrt flush)
225
(cond (initi ffwrt0) (squash nil) (stall ffwrt) (flush nil) (t t)))
227
(defun initffinst_a (ffinst0) ffinst0)
229
(defun nextffinst_a (initi ffinst0 stall ffinst if_inst)
230
(cond (initi ffinst0) (stall ffinst) (t if_inst)))
232
(defun initffppc_a (ffppc0) ffppc0)
234
(defun nextffppc_a (initi ffppc0 stall ffppc ppc)
235
(cond (initi ffppc0) (stall ffppc) (t ppc)))
237
(defun initprf_a (prf) (cons (s 0 t (s 1 nil nil)) prf))
239
(defun nextprf_a (prf initi mwwrt mwdest mwregwrite mwval)
243
(s 3 mwdest (s 4 mwregwrite (s 5 mwval nil))))))
246
(defun initfdppc_a (fdppc0) fdppc0)
248
(defun nextfdppc_a (initi fdppc0 stall fdppc ffppc)
249
(cond (initi fdppc0) (stall fdppc) (t ffppc)))
251
(defun initfdwrt_a (fdwrt0) fdwrt0)
253
(defun nextfdwrt_a (initi fdwrt0 squash stall fdwrt ffwrt)
254
(cond (initi fdwrt0) (squash nil) (stall fdwrt) (t ffwrt)))
256
(defun initfdinst_a (fdinst0) fdinst0)
258
(defun nextfdinst_a (initi fdinst0 stall fdinst ffinst)
259
(cond (initi fdinst0) (stall fdinst) (t ffinst)))
261
(defun initfdpredicteddirection_a (fdpredicteddirection0)
262
fdpredicteddirection0)
264
(defun nextfdpredicteddirection_a
265
(initi fdpredicteddirection0 stall fdpredicteddirection
266
ffpredicteddirection)
268
(initi fdpredicteddirection0)
269
(stall fdpredicteddirection)
270
(t ffpredicteddirection)))
272
(defun initfdpredictedtarget_a (fdpredictedtarget0)
275
(defun nextfdpredictedtarget_a
276
(initi fdpredictedtarget0 stall fdpredictedtarget
279
(initi fdpredictedtarget0)
280
(stall fdpredictedtarget)
281
(t ffpredictedtarget)))
283
(defun initdeppc_a (deppc0) deppc0)
285
(defun nextdeppc_a (initi deppc0 fdppc)
286
(cond (initi deppc0) (t fdppc)))
288
(defun initdesrc1_a (desrc10) desrc10)
290
(defun nextdesrc1_a (initi desrc10 if_id_src1)
291
(cond (initi desrc10) (t if_id_src1)))
293
(defun initdesrc2_a (desrc20) desrc20)
295
(defun nextdesrc2_a (initi desrc20 if_id_src2)
296
(cond (initi desrc20) (t if_id_src2)))
298
(defun initdearg1_a (a1) a1)
301
(initi a1 if_id_src1 prf mwwrt mwdest mwregwrite mwval)
304
(t (read-prf_a if_id_src1
305
(nextprf_a prf initi mwwrt mwdest mwregwrite mwval)))))
307
(defun initdearg2_a (a2) a2)
310
(initi a2 if_id_src2 prf mwwrt mwdest mwregwrite mwval)
313
(t (read-prf_a if_id_src2
314
(nextprf_a prf initi mwwrt mwdest mwregwrite mwval)))))
316
(defun initdedest_a (dedest0) dedest0)
318
(defun nextdedest_a (initi dedest0 fdinst)
319
(cond (initi dedest0) (t (dest fdinst))))
321
(defun initdeop_a (deop0) deop0)
323
(defun nextdeop_a (initi deop0 fdinst)
324
(cond (initi deop0) (t (opcode fdinst))))
326
(defun initdeimm_a (deimm0) deimm0)
328
(defun nextdeimm_a (initi deimm0 fdinst)
329
(cond (initi deimm0) (t (getimm fdinst))))
331
(defun initdeuseimm_a (deuseimm0) deuseimm0)
333
(defun nextdeuseimm_a (initi deuseimm0 fdinst)
334
(cond (initi deuseimm0) (t (getuseimm fdinst))))
336
(defun initderegwrite_a (deregwrite0) deregwrite0)
338
(defun nextderegwrite_a (initi deregwrite0 id_regwrite)
339
(cond (initi deregwrite0) (t id_regwrite)))
341
(defun initdememwrite_a (dememwrite0) dememwrite0)
343
(defun nextdememwrite_a (initi dememwrite0 id_memwrite)
344
(cond (initi dememwrite0) (t id_memwrite)))
346
(defun initdememtoreg_a (dememtoreg0) dememtoreg0)
348
(defun nextdememtoreg_a (initi dememtoreg0 fdinst)
349
(cond (initi dememtoreg0) (t (getmemtoreg fdinst))))
351
(defun initdeisbranch_a (deisbranch0) deisbranch0)
353
(defun nextdeisbranch_a (initi deisbranch0 fdinst)
354
(cond (initi deisbranch0) (t (getisbranch fdinst))))
356
(defun initdewrt_a (dewrt0) dewrt0)
358
(defun nextdewrt_a (initi dewrt0 squash stall fdwrt)
359
(cond (initi dewrt0) (squash nil) (t (and (not stall) fdwrt))))
361
(defun initdepredicteddirection_a (depredicteddirection0)
362
depredicteddirection0)
364
(defun nextdepredicteddirection_a
365
(initi depredicteddirection0 stall depredicteddirection
366
fdpredicteddirection)
368
(initi depredicteddirection0)
369
(stall depredicteddirection)
370
(t fdpredicteddirection)))
372
(defun initdepredictedtarget_a (depredictedtarget0)
375
(defun nextdepredictedtarget_a
376
(initi depredictedtarget0 stall depredictedtarget
379
(initi depredictedtarget0)
380
(stall depredictedtarget)
381
(t fdpredictedtarget)))
383
(defun initemppc_a (emppc0) emppc0)
385
(defun nextemppc_a (initi emppc0 deppc)
386
(cond (initi emppc0) (t deppc)))
388
(defun initemis_taken_branch_a (emis_taken_branch0)
391
(defun nextemis_taken_branch_a
392
(initi emis_taken_branch0 ex_is_taken_branch)
393
(cond (initi emis_taken_branch0) (t ex_is_taken_branch)))
395
(defun initemtargetpc_a (emtargetpc0) emtargetpc0)
397
(defun nextemtargetpc_a (initi emtargetpc0 ex_targetpc)
398
(cond (initi emtargetpc0) (t ex_targetpc)))
400
(defun initemarg2_a (emarg20) emarg20)
402
(defun nextemarg2_a (initi emarg20 ex_fwd_src2)
403
(cond (initi emarg20) (t ex_fwd_src2)))
405
(defun initemresult_a (emresult0) emresult0)
407
(defun nextemresult_a (initi emresult0 ex_result)
408
(cond (initi emresult0) (t ex_result)))
410
(defun initemdest_a (emdest0) emdest0)
412
(defun nextemdest_a (initi emdest0 dedest)
413
(cond (initi emdest0) (t dedest)))
415
(defun initemwrt_a (emwrt0) emwrt0)
417
(defun nextemwrt_a (initi emwrt0 squash dewrt)
418
(cond (initi emwrt0) (squash nil) (t dewrt)))
420
(defun initemmispredictedtaken_a (emmispredictedtaken0)
421
emmispredictedtaken0)
423
(defun nextemmispredictedtaken_a
424
(initi emmispredictedtaken0 mispredicted_taken)
425
(cond (initi emmispredictedtaken0) (t mispredicted_taken)))
427
(defun initemmispredictednottaken_a (emmispredictednottaken0)
428
emmispredictednottaken0)
430
(defun nextemmispredictednottaken_a
431
(initi emmispredictednottaken0 mispredicted_nottaken)
432
(cond (initi emmispredictednottaken0) (t mispredicted_nottaken)))
434
(defun initemregwrite_a (emregwrite0) emregwrite0)
436
(defun nextemregwrite_a (initi emregwrite0 deregwrite)
437
(cond (initi emregwrite0) (t deregwrite)))
439
(defun initemmemwrite_a (emmemwrite0) emmemwrite0)
441
(defun nextemmemwrite_a (initi emmemwrite0 dememwrite)
442
(cond (initi emmemwrite0) (t dememwrite)))
444
(defun initemmemtoreg_a (emmemtoreg0) emmemtoreg0)
446
(defun nextemmemtoreg_a (initi emmemtoreg0 dememtoreg)
447
(cond (initi emmemtoreg0) (t dememtoreg)))
449
(defun initpdmemhist_2_a (dmem0) dmem0)
451
(defun nextpdmemhist_2_a (initi dmem0 pdmemhist_1)
452
(cond (initi dmem0) (t pdmemhist_1)))
454
(defun initpdmemhist_1_a (dmem0) dmem0)
456
(defun nextpdmemhist_1_a (initi dmem0 pdmem)
457
(cond (initi dmem0) (t pdmem)))
459
(defun initpdmem_a (dmem0) dmem0)
462
(initi dmem0 emwrt emmemwrite pdmem emresult emarg2)
465
((and emwrt emmemwrite) (nextdmem pdmem emresult emarg2))
468
(defun initmmppc_a (mmppc0) mmppc0)
470
(defun nextmmppc_a (initi mmppc0 emppc)
471
(cond (initi mmppc0) (t emppc)))
473
(defun initmmval_a (mmval0) mmval0)
475
(defun nextmmval_a (initi mmval0 emmemtoreg mem1_readdata emresult)
476
(cond (initi mmval0) (emmemtoreg mem1_readdata) (t emresult)))
478
(defun initmmdest_a (mmdest0) mmdest0)
480
(defun nextmmdest_a (initi mmdest0 emdest)
481
(cond (initi mmdest0) (t emdest)))
483
(defun initmmwrt_a (mmwrt0) mmwrt0)
485
(defun nextmmwrt_a (initi mmwrt0 emwrt)
486
(cond (initi mmwrt0) (t emwrt)))
488
(defun initmmregwrite_a (mmregwrite0) mmregwrite0)
490
(defun nextmmregwrite_a (initi mmregwrite0 emregwrite)
491
(cond (initi mmregwrite0) (t emregwrite)))
493
(defun initmwppc_a (mwppc0) mwppc0)
495
(defun nextmwppc_a (initi mwppc0 mmppc)
496
(cond (initi mwppc0) (t mmppc)))
498
(defun initmwval_a (mwval0) mwval0)
500
(defun nextmwval_a (initi mwval0 mmval)
501
(cond (initi mwval0) (t mmval)))
503
(defun initmwdest_a (mwdest0) mwdest0)
505
(defun nextmwdest_a (initi mwdest0 mmdest)
506
(cond (initi mwdest0) (t mmdest)))
508
(defun initmwwrt_a (mwwrt0) mwwrt0)
510
(defun nextmwwrt_a (initi mwwrt0 mmwrt)
511
(cond (initi mwwrt0) (t mmwrt)))
513
(defun initmwregwrite_a (mwregwrite0) mwregwrite0)
515
(defun nextmwregwrite_a (initi mwregwrite0 mmregwrite)
516
(cond (initi mwregwrite0) (t mmregwrite)))
518
(defun impl-simulate_a
519
(impl initi pc0 flush bpstate0 ffpredicteddirection0
520
ffpredictedtarget0 ffwrt0 ffinst0 ffppc0 fdppc0 fdwrt0
521
fdinst0 fdpredicteddirection0 fdpredictedtarget0 deppc0
522
desrc10 desrc20 a1 a2 dedest0 deop0 deimm0 deuseimm0
523
deregwrite0 dememwrite0 dememtoreg0 deisbranch0 dewrt0
524
depredicteddirection0 depredictedtarget0 emppc0
525
emis_taken_branch0 emtargetpc0 emarg20 emresult0 emdest0
526
emwrt0 emmispredictedtaken0 emmispredictednottaken0
527
emregwrite0 emmemwrite0 emmemtoreg0 dmem0 mmppc0 mmval0
528
mmdest0 mmwrt0 mmregwrite0 mwppc0 mwval0 mwdest0 mwwrt0
530
(let* ((pimem (g 'pimem impl)) (ppc (g 'ppc impl))
531
(bpstate (g 'bpstate impl))
532
(ffpredicteddirection (g 'ffpredicteddirection impl))
533
(ffpredictedtarget (g 'ffpredictedtarget impl))
534
(ffwrt (g 'ffwrt impl)) (ffinst (g 'ffinst impl))
535
(ffppc (g 'ffppc impl)) (prf (g 'prf impl))
536
(fdppc (g 'fdppc impl)) (fdwrt (g 'fdwrt impl))
537
(fdinst (g 'fdinst impl))
538
(fdpredicteddirection (g 'fdpredicteddirection impl))
539
(fdpredictedtarget (g 'fdpredictedtarget impl))
540
(deppc (g 'deppc impl)) (desrc1 (g 'desrc1 impl))
541
(desrc2 (g 'desrc2 impl)) (dearg1 (g 'dearg1 impl))
542
(dearg2 (g 'dearg2 impl)) (dedest (g 'dedest impl))
543
(deop (g 'deop impl)) (deimm (g 'deimm impl))
544
(deuseimm (g 'deuseimm impl))
545
(deregwrite (g 'deregwrite impl))
546
(dememwrite (g 'dememwrite impl))
547
(dememtoreg (g 'dememtoreg impl))
548
(deisbranch (g 'deisbranch impl)) (dewrt (g 'dewrt impl))
549
(depredicteddirection (g 'depredicteddirection impl))
550
(depredictedtarget (g 'depredictedtarget impl))
551
(emppc (g 'emppc impl))
552
(emis_taken_branch (g 'emis_taken_branch impl))
553
(emtargetpc (g 'emtargetpc impl)) (emarg2 (g 'emarg2 impl))
554
(emresult (g 'emresult impl)) (emdest (g 'emdest impl))
555
(emwrt (g 'emwrt impl))
556
(emmispredictedtaken (g 'emmispredictedtaken impl))
557
(emmispredictednottaken (g 'emmispredictednottaken impl))
558
(emregwrite (g 'emregwrite impl))
559
(emmemwrite (g 'emmemwrite impl))
560
(emmemtoreg (g 'emmemtoreg impl))
561
(pdmemhist_2 (g 'pdmemhist_2 impl))
562
(pdmemhist_1 (g 'pdmemhist_1 impl)) (pdmem (g 'pdmem impl))
563
(mmppc (g 'mmppc impl)) (mmval (g 'mmval impl))
564
(mmdest (g 'mmdest impl)) (mmwrt (g 'mmwrt impl))
565
(mmregwrite (g 'mmregwrite impl)) (mwppc (g 'mwppc impl))
566
(mwval (g 'mwval impl)) (mwdest (g 'mwdest impl))
567
(mwwrt (g 'mwwrt impl)) (mwregwrite (g 'mwregwrite impl)))
568
(let* ((if_inst (read-pimem_a ppc pimem))
569
(predicted_direction (predictdirection bpstate))
570
(predicted_target (predicttarget bpstate))
571
(if_predict_branch_taken
572
(and (getisbranch if_inst) predicted_direction))
573
(if_id_src1 (src1 fdinst)) (if_id_src2 (src2 fdinst))
574
(stall (and (and deregwrite dewrt)
575
(or (equal if_id_src1 dedest)
576
(equal if_id_src2 dedest))))
577
(id_regwrite (getregwrite fdinst))
578
(id_memwrite (getmemwrite fdinst))
580
(and (and mwwrt (equal desrc1 mwdest)) mwregwrite))
582
(and (and mwwrt (equal desrc2 mwdest)) mwregwrite))
584
(and (and mmwrt (equal desrc1 mmdest)) mmregwrite))
586
(and (and mmwrt (equal desrc2 mmdest)) mmregwrite))
589
(ex_mem2_equal_src1 mmval)
590
(ex_wb_equal_src1 mwval)
594
(ex_mem2_equal_src2 mmval)
595
(ex_wb_equal_src2 mwval)
597
(ex_data2 (cond (deuseimm deimm) (t ex_fwd_src2)))
598
(ex_result (alu deop ex_fwd_src1 ex_data2))
599
(ex_is_taken_branch_temp
600
(takebranch deop ex_fwd_src1 ex_fwd_src2))
602
(and (and ex_is_taken_branch_temp dewrt) deisbranch))
603
(ex_targetpc (selecttargetpc deop ex_fwd_src1 deppc))
604
(equal_targetpc (equal ex_targetpc depredictedtarget))
605
(equal_targetpc_bar (not equal_targetpc))
606
(ex_predicteddirection depredicteddirection)
607
(mispredicted_nottaken_case1
608
(and ex_is_taken_branch (not ex_predicteddirection)))
609
(mispredicted_nottaken_case2
610
(and ex_is_taken_branch equal_targetpc_bar))
611
(mispredicted_nottaken
612
(or mispredicted_nottaken_case1
613
mispredicted_nottaken_case2))
615
(and (and ex_predicteddirection deisbranch)
616
(not ex_is_taken_branch)))
617
(mem1_readdata (dmem_read pdmem emresult))
618
(mem1_is_taken_branch (and emwrt emis_taken_branch))
619
(mem1_mispredicted_taken (and emmispredictedtaken emwrt))
620
(mem1_mispredicted_nottaken
621
(and emmispredictednottaken emwrt))
623
(or mem1_mispredicted_nottaken mem1_mispredicted_taken))
624
(squash mem1_mispredicted))
625
(impl-state_a (nextpimem_a pimem)
626
(nextppc_a initi pc0 mem1_mispredicted_taken emppc
627
mem1_mispredicted_nottaken emtargetpc stall flush ppc
628
if_predict_branch_taken predicted_target)
629
(nextbpstate_a initi bpstate0 stall bpstate)
630
(nextffpredicteddirection_a initi ffpredicteddirection0
631
stall ffpredicteddirection if_predict_branch_taken)
632
(nextffpredictedtarget_a initi ffpredictedtarget0 stall
633
ffpredictedtarget predicted_target)
634
(nextffwrt_a initi ffwrt0 squash stall ffwrt flush)
635
(nextffinst_a initi ffinst0 stall ffinst if_inst)
636
(nextffppc_a initi ffppc0 stall ffppc ppc)
637
(nextprf_a prf initi mwwrt mwdest mwregwrite mwval)
638
(nextfdppc_a initi fdppc0 stall fdppc ffppc)
639
(nextfdwrt_a initi fdwrt0 squash stall fdwrt ffwrt)
640
(nextfdinst_a initi fdinst0 stall fdinst ffinst)
641
(nextfdpredicteddirection_a initi fdpredicteddirection0
642
stall fdpredicteddirection ffpredicteddirection)
643
(nextfdpredictedtarget_a initi fdpredictedtarget0 stall
644
fdpredictedtarget ffpredictedtarget)
645
(nextdeppc_a initi deppc0 fdppc)
646
(nextdesrc1_a initi desrc10 if_id_src1)
647
(nextdesrc2_a initi desrc20 if_id_src2)
648
(nextdearg1_a initi a1 if_id_src1 prf mwwrt mwdest
650
(nextdearg2_a initi a2 if_id_src2 prf mwwrt mwdest
652
(nextdedest_a initi dedest0 fdinst)
653
(nextdeop_a initi deop0 fdinst)
654
(nextdeimm_a initi deimm0 fdinst)
655
(nextdeuseimm_a initi deuseimm0 fdinst)
656
(nextderegwrite_a initi deregwrite0 id_regwrite)
657
(nextdememwrite_a initi dememwrite0 id_memwrite)
658
(nextdememtoreg_a initi dememtoreg0 fdinst)
659
(nextdeisbranch_a initi deisbranch0 fdinst)
660
(nextdewrt_a initi dewrt0 squash stall fdwrt)
661
(nextdepredicteddirection_a initi depredicteddirection0
662
stall depredicteddirection fdpredicteddirection)
663
(nextdepredictedtarget_a initi depredictedtarget0 stall
664
depredictedtarget fdpredictedtarget)
665
(nextemppc_a initi emppc0 deppc)
666
(nextemis_taken_branch_a initi emis_taken_branch0
668
(nextemtargetpc_a initi emtargetpc0 ex_targetpc)
669
(nextemarg2_a initi emarg20 ex_fwd_src2)
670
(nextemresult_a initi emresult0 ex_result)
671
(nextemdest_a initi emdest0 dedest)
672
(nextemwrt_a initi emwrt0 squash dewrt)
673
(nextemmispredictedtaken_a initi emmispredictedtaken0
675
(nextemmispredictednottaken_a initi emmispredictednottaken0
676
mispredicted_nottaken)
677
(nextemregwrite_a initi emregwrite0 deregwrite)
678
(nextemmemwrite_a initi emmemwrite0 dememwrite)
679
(nextemmemtoreg_a initi emmemtoreg0 dememtoreg)
680
(nextpdmemhist_2_a initi dmem0 pdmemhist_1)
681
(nextpdmemhist_1_a initi dmem0 pdmem)
682
(nextpdmem_a initi dmem0 emwrt emmemwrite pdmem emresult
684
(nextmmppc_a initi mmppc0 emppc)
685
(nextmmval_a initi mmval0 emmemtoreg mem1_readdata emresult)
686
(nextmmdest_a initi mmdest0 emdest)
687
(nextmmwrt_a initi mmwrt0 emwrt)
688
(nextmmregwrite_a initi mmregwrite0 emregwrite)
689
(nextmwppc_a initi mwppc0 mmppc)
690
(nextmwval_a initi mwval0 mmval)
691
(nextmwdest_a initi mwdest0 mmdest)
692
(nextmwwrt_a initi mwwrt0 mmwrt)
693
(nextmwregwrite_a initi mwregwrite0 mmregwrite)))))
695
(defun impl-initialize_a
696
(impl pc0 bpstate0 ffpredicteddirection0 ffpredictedtarget0
697
ffwrt0 ffinst0 ffppc0 fdppc0 fdwrt0 fdinst0
698
fdpredicteddirection0 fdpredictedtarget0 deppc0 desrc10
699
desrc20 a1 a2 dedest0 deop0 deimm0 deuseimm0 deregwrite0
700
dememwrite0 dememtoreg0 deisbranch0 dewrt0
701
depredicteddirection0 depredictedtarget0 emppc0
702
emis_taken_branch0 emtargetpc0 emarg20 emresult0 emdest0
703
emwrt0 emmispredictedtaken0 emmispredictednottaken0
704
emregwrite0 emmemwrite0 emmemtoreg0 dmem0 mmppc0 mmval0
705
mmdest0 mmwrt0 mmregwrite0 mwppc0 mwval0 mwdest0 mwwrt0
707
(let* ((pimem (g 'pimem impl)) (ppc (g 'ppc impl))
708
(bpstate (g 'bpstate impl))
709
(ffpredicteddirection (g 'ffpredicteddirection impl))
710
(ffpredictedtarget (g 'ffpredictedtarget impl))
711
(ffwrt (g 'ffwrt impl)) (ffinst (g 'ffinst impl))
712
(ffppc (g 'ffppc impl)) (prf (g 'prf impl))
713
(fdppc (g 'fdppc impl)) (fdwrt (g 'fdwrt impl))
714
(fdinst (g 'fdinst impl))
715
(fdpredicteddirection (g 'fdpredicteddirection impl))
716
(fdpredictedtarget (g 'fdpredictedtarget impl))
717
(deppc (g 'deppc impl)) (desrc1 (g 'desrc1 impl))
718
(desrc2 (g 'desrc2 impl)) (dearg1 (g 'dearg1 impl))
719
(dearg2 (g 'dearg2 impl)) (dedest (g 'dedest impl))
720
(deop (g 'deop impl)) (deimm (g 'deimm impl))
721
(deuseimm (g 'deuseimm impl))
722
(deregwrite (g 'deregwrite impl))
723
(dememwrite (g 'dememwrite impl))
724
(dememtoreg (g 'dememtoreg impl))
725
(deisbranch (g 'deisbranch impl)) (dewrt (g 'dewrt impl))
726
(depredicteddirection (g 'depredicteddirection impl))
727
(depredictedtarget (g 'depredictedtarget impl))
728
(emppc (g 'emppc impl))
729
(emis_taken_branch (g 'emis_taken_branch impl))
730
(emtargetpc (g 'emtargetpc impl)) (emarg2 (g 'emarg2 impl))
731
(emresult (g 'emresult impl)) (emdest (g 'emdest impl))
732
(emwrt (g 'emwrt impl))
733
(emmispredictedtaken (g 'emmispredictedtaken impl))
734
(emmispredictednottaken (g 'emmispredictednottaken impl))
735
(emregwrite (g 'emregwrite impl))
736
(emmemwrite (g 'emmemwrite impl))
737
(emmemtoreg (g 'emmemtoreg impl))
738
(pdmemhist_2 (g 'pdmemhist_2 impl))
739
(pdmemhist_1 (g 'pdmemhist_1 impl)) (pdmem (g 'pdmem impl))
740
(mmppc (g 'mmppc impl)) (mmval (g 'mmval impl))
741
(mmdest (g 'mmdest impl)) (mmwrt (g 'mmwrt impl))
742
(mmregwrite (g 'mmregwrite impl)) (mwppc (g 'mwppc impl))
743
(mwval (g 'mwval impl)) (mwdest (g 'mwdest impl))
744
(mwwrt (g 'mwwrt impl)) (mwregwrite (g 'mwregwrite impl)))
745
(let* ((if_inst (read-pimem_a ppc pimem))
746
(predicted_direction (predictdirection bpstate))
747
(predicted_target (predicttarget bpstate))
748
(if_predict_branch_taken
749
(and (getisbranch if_inst) predicted_direction))
750
(if_id_src1 (src1 fdinst)) (if_id_src2 (src2 fdinst))
751
(stall (and (and deregwrite dewrt)
752
(or (equal if_id_src1 dedest)
753
(equal if_id_src2 dedest))))
754
(id_regwrite (getregwrite fdinst))
755
(id_memwrite (getmemwrite fdinst))
757
(and (and mwwrt (equal desrc1 mwdest)) mwregwrite))
759
(and (and mwwrt (equal desrc2 mwdest)) mwregwrite))
761
(and (and mmwrt (equal desrc1 mmdest)) mmregwrite))
763
(and (and mmwrt (equal desrc2 mmdest)) mmregwrite))
766
(ex_mem2_equal_src1 mmval)
767
(ex_wb_equal_src1 mwval)
771
(ex_mem2_equal_src2 mmval)
772
(ex_wb_equal_src2 mwval)
774
(ex_data2 (cond (deuseimm deimm) (t ex_fwd_src2)))
775
(ex_result (alu deop ex_fwd_src1 ex_data2))
776
(ex_is_taken_branch_temp
777
(takebranch deop ex_fwd_src1 ex_fwd_src2))
779
(and (and ex_is_taken_branch_temp dewrt) deisbranch))
780
(ex_targetpc (selecttargetpc deop ex_fwd_src1 deppc))
781
(equal_targetpc (equal ex_targetpc depredictedtarget))
782
(equal_targetpc_bar (not equal_targetpc))
783
(ex_predicteddirection depredicteddirection)
784
(mispredicted_nottaken_case1
785
(and ex_is_taken_branch (not ex_predicteddirection)))
786
(mispredicted_nottaken_case2
787
(and ex_is_taken_branch equal_targetpc_bar))
788
(mispredicted_nottaken
789
(or mispredicted_nottaken_case1
790
mispredicted_nottaken_case2))
792
(and (and ex_predicteddirection deisbranch)
793
(not ex_is_taken_branch)))
794
(mem1_readdata (dmem_read pdmem emresult))
795
(mem1_is_taken_branch (and emwrt emis_taken_branch))
796
(mem1_mispredicted_taken (and emmispredictedtaken emwrt))
797
(mem1_mispredicted_nottaken
798
(and emmispredictednottaken emwrt))
800
(or mem1_mispredicted_nottaken mem1_mispredicted_taken))
801
(squash mem1_mispredicted))
802
(impl-state_a (initpimem_a pimem) (initppc_a pc0)
803
(initbpstate_a bpstate0)
804
(initffpredicteddirection_a ffpredicteddirection0)
805
(initffpredictedtarget_a ffpredictedtarget0)
806
(initffwrt_a ffwrt0) (initffinst_a ffinst0)
807
(initffppc_a ffppc0) (initprf_a prf) (initfdppc_a fdppc0)
808
(initfdwrt_a fdwrt0) (initfdinst_a fdinst0)
809
(initfdpredicteddirection_a fdpredicteddirection0)
810
(initfdpredictedtarget_a fdpredictedtarget0)
811
(initdeppc_a deppc0) (initdesrc1_a desrc10)
812
(initdesrc2_a desrc20) (initdearg1_a a1) (initdearg2_a a2)
813
(initdedest_a dedest0) (initdeop_a deop0)
814
(initdeimm_a deimm0) (initdeuseimm_a deuseimm0)
815
(initderegwrite_a deregwrite0)
816
(initdememwrite_a dememwrite0)
817
(initdememtoreg_a dememtoreg0)
818
(initdeisbranch_a deisbranch0) (initdewrt_a dewrt0)
819
(initdepredicteddirection_a depredicteddirection0)
820
(initdepredictedtarget_a depredictedtarget0)
822
(initemis_taken_branch_a emis_taken_branch0)
823
(initemtargetpc_a emtargetpc0) (initemarg2_a emarg20)
824
(initemresult_a emresult0) (initemdest_a emdest0)
826
(initemmispredictedtaken_a emmispredictedtaken0)
827
(initemmispredictednottaken_a emmispredictednottaken0)
828
(initemregwrite_a emregwrite0)
829
(initemmemwrite_a emmemwrite0)
830
(initemmemtoreg_a emmemtoreg0) (initpdmemhist_2_a dmem0)
831
(initpdmemhist_1_a dmem0) (initpdmem_a dmem0)
832
(initmmppc_a mmppc0) (initmmval_a mmval0)
833
(initmmdest_a mmdest0) (initmmwrt_a mmwrt0)
834
(initmmregwrite_a mmregwrite0) (initmwppc_a mwppc0)
835
(initmwval_a mwval0) (initmwdest_a mwdest0)
836
(initmwwrt_a mwwrt0) (initmwregwrite_a mwregwrite0)))))
838
(defun spec-state_a (simem spc srf sdmem)
839
(seq nil 'simem simem 'spc spc 'srf srf 'sdmem sdmem))
841
(defun initsimem_a (simem) (cons (s 0 t (s 1 nil nil)) simem))
843
(defun nextsimem_a (simem initi)
844
(cons (s 0 nil (s 1 initi nil)) simem))
846
(defun initspc_a (pc0) pc0)
849
(initi pc0 project_impl impl.ppc isa is_taken_branch targetpc
853
(project_impl impl.ppc)
854
((and isa is_taken_branch) targetpc)
858
(defun initsrf_a (srf) (cons (s 0 t (s 1 nil nil)) srf))
861
(srf initi project_impl impl.prf isa inst regwrite val)
866
(s 4 isa (s 5 inst (s 6 regwrite (s 7 val nil))))))))
869
(defun initsdmem_a (dmem0) dmem0)
872
(initi dmem0 project_impl impl.pdmem isa memwrite sdmem result
876
(project_impl impl.pdmem)
877
((and isa memwrite) (nextdmem sdmem result arg2_temp))
880
(defun spec-simulate_a
881
(spec initi pc0 project_impl impl.ppc isa impl.prf dmem0
883
(let* ((simem (g 'simem spec)) (spc (g 'spc spec))
884
(srf (g 'srf spec)) (sdmem (g 'sdmem spec)))
885
(let* ((inst (read-simem_a spc simem))
886
(regwrite (getregwrite inst)) (memtoreg (getmemtoreg inst))
887
(memwrite (getmemwrite inst)) (isbranch (getisbranch inst))
888
(useimm (getuseimm inst)) (imm (getimm inst))
889
(arg1 (read-srf_a (src1 inst) srf))
890
(arg2_temp (read-srf_a (src2 inst) srf))
891
(arg2 (cond (useimm imm) (t arg2_temp)))
892
(result (alu (opcode inst) arg1 arg2))
893
(is_taken_branch_temp
894
(takebranch (opcode inst) arg1 arg2_temp))
895
(is_taken_branch (and is_taken_branch_temp isbranch))
896
(targetpc (selecttargetpc (opcode inst) arg1 spc))
897
(readdata (dmem_read sdmem result))
898
(val (cond (memtoreg readdata) (t result))))
899
(spec-state_a (nextsimem_a simem initi)
900
(nextspc_a initi pc0 project_impl impl.ppc isa
901
is_taken_branch targetpc spc)
902
(nextsrf_a srf initi project_impl impl.prf isa inst regwrite
904
(nextsdmem_a initi dmem0 project_impl impl.pdmem isa
905
memwrite sdmem result arg2_temp)))))
907
(defun spec-initialize_a (spec pc0 dmem0)
908
(let* ((simem (g 'simem spec)) (spc (g 'spc spec))
909
(srf (g 'srf spec)) (sdmem (g 'sdmem spec)))
910
(let* ((inst (read-simem_a spc simem))
911
(regwrite (getregwrite inst)) (memtoreg (getmemtoreg inst))
912
(memwrite (getmemwrite inst)) (isbranch (getisbranch inst))
913
(useimm (getuseimm inst)) (imm (getimm inst))
914
(arg1 (read-srf_a (src1 inst) srf))
915
(arg2_temp (read-srf_a (src2 inst) srf))
916
(arg2 (cond (useimm imm) (t arg2_temp)))
917
(result (alu (opcode inst) arg1 arg2))
918
(is_taken_branch_temp
919
(takebranch (opcode inst) arg1 arg2_temp))
920
(is_taken_branch (and is_taken_branch_temp isbranch))
921
(targetpc (selecttargetpc (opcode inst) arg1 spc))
922
(readdata (dmem_read sdmem result))
923
(val (cond (memtoreg readdata) (t result))))
924
(spec-state_a (initsimem_a simem) (initspc_a pc0)
925
(initsrf_a srf) (initsdmem_a dmem0)))))
928
(st flush isa project_impl initi pc0 bpstate0
929
ffpredicteddirection0 ffpredictedtarget0 ffwrt0 ffinst0
930
ffppc0 fdppc0 fdwrt0 fdinst0 fdpredicteddirection0
931
fdpredictedtarget0 deppc0 desrc10 desrc20 a1 a2 dedest0
932
deop0 deimm0 deuseimm0 deregwrite0 dememwrite0 dememtoreg0
933
deisbranch0 dewrt0 depredicteddirection0 depredictedtarget0
934
emppc0 emis_taken_branch0 emtargetpc0 emarg20 emresult0
935
emdest0 emwrt0 emmispredictedtaken0 emmispredictednottaken0
936
emregwrite0 emmemwrite0 emmemtoreg0 dmem0 mmppc0 mmval0
937
mmdest0 mmwrt0 mmregwrite0 mwppc0 mwval0 mwdest0 mwwrt0
938
mwregwrite0 impl.ppc impl.prf impl.pdmem)
940
(impl-simulate_a (g 'impl st) initi pc0 flush bpstate0
941
ffpredicteddirection0 ffpredictedtarget0 ffwrt0 ffinst0
942
ffppc0 fdppc0 fdwrt0 fdinst0 fdpredicteddirection0
943
fdpredictedtarget0 deppc0 desrc10 desrc20 a1 a2 dedest0
944
deop0 deimm0 deuseimm0 deregwrite0 dememwrite0 dememtoreg0
945
deisbranch0 dewrt0 depredicteddirection0 depredictedtarget0
946
emppc0 emis_taken_branch0 emtargetpc0 emarg20 emresult0
947
emdest0 emwrt0 emmispredictedtaken0 emmispredictednottaken0
948
emregwrite0 emmemwrite0 emmemtoreg0 dmem0 mmppc0 mmval0
949
mmdest0 mmwrt0 mmregwrite0 mwppc0 mwval0 mwdest0 mwwrt0
951
(spec-simulate_a (g 'spec st) initi pc0 project_impl impl.ppc
952
isa impl.prf dmem0 impl.pdmem)))
955
(st flush isa project_impl initi pc0 bpstate0
956
ffpredicteddirection0 ffpredictedtarget0 ffwrt0 ffinst0
957
ffppc0 fdppc0 fdwrt0 fdinst0 fdpredicteddirection0
958
fdpredictedtarget0 deppc0 desrc10 desrc20 a1 a2 dedest0
959
deop0 deimm0 deuseimm0 deregwrite0 dememwrite0 dememtoreg0
960
deisbranch0 dewrt0 depredicteddirection0 depredictedtarget0
961
emppc0 emis_taken_branch0 emtargetpc0 emarg20 emresult0
962
emdest0 emwrt0 emmispredictedtaken0 emmispredictednottaken0
963
emregwrite0 emmemwrite0 emmemtoreg0 dmem0 mmppc0 mmval0
964
mmdest0 mmwrt0 mmregwrite0 mwppc0 mwval0 mwdest0 mwwrt0
967
(impl-initialize_a (g 'impl st) pc0 bpstate0
968
ffpredicteddirection0 ffpredictedtarget0 ffwrt0 ffinst0
969
ffppc0 fdppc0 fdwrt0 fdinst0 fdpredicteddirection0
970
fdpredictedtarget0 deppc0 desrc10 desrc20 a1 a2 dedest0
971
deop0 deimm0 deuseimm0 deregwrite0 dememwrite0 dememtoreg0
972
deisbranch0 dewrt0 depredicteddirection0 depredictedtarget0
973
emppc0 emis_taken_branch0 emtargetpc0 emarg20 emresult0
974
emdest0 emwrt0 emmispredictedtaken0 emmispredictednottaken0
975
emregwrite0 emmemwrite0 emmemtoreg0 dmem0 mmppc0 mmval0
976
mmdest0 mmwrt0 mmregwrite0 mwppc0 mwval0 mwdest0 mwwrt0
978
(spec-initialize_a (g 'spec st) pc0 dmem0)))
981
(implies (and (integerp pc0) (integerp dmem0)
982
(integerp bpstate0) (integerp a) (integerp zero)
983
(booleanp ffwrt0) (booleanp fdwrt0)
984
(booleanp dewrt0) (booleanp emwrt0)
985
(booleanp mmwrt0) (booleanp mwwrt0)
986
(integerp fdbpstate0)
987
(booleanp fdpredicteddirection0)
988
(integerp fdpredictedtarget0)
989
(booleanp emmispredictednottaken0)
990
(integerp debpstate0)
991
(booleanp depredicteddirection0)
992
(integerp depredictedtarget0)
993
(booleanp emmispredictedtaken0)
994
(integerp embpstate0) (integerp mmbpstate0)
995
(integerp mwbpstate0)
996
(integerp ffpredictedtarget0)
997
(integerp ffbpstate0)
998
(booleanp ffpredicteddirection0)
999
(integerp emppc0) (integerp mmppc0)
1000
(integerp mwppc0) (booleanp deisbranch0)
1001
(booleanp emis_taken_branch0)
1002
(integerp emtargetpc0) (integerp ffppc0)
1003
(integerp fdppc0) (integerp deppc0)
1004
(integerp mwval0) (integerp emresult0)
1005
(booleanp deregwrite0) (booleanp emregwrite0)
1006
(booleanp mwregwrite0) (integerp mwdest0)
1007
(integerp deop0) (integerp fddest0)
1008
(integerp dedest0) (integerp op0) (integerp s0)
1009
(integerp a1) (integerp a2) (integerp d0)
1010
(integerp d1) (integerp x0) (integerp fdop0)
1011
(booleanp w0) (booleanp w1) (integerp fdsrc10)
1012
(integerp fdsrc20) (integerp emdest0)
1013
(integerp emval0) (integerp desrc10)
1014
(integerp desrc20) (integerp fdinst0)
1015
(integerp deimm0) (booleanp deuseimm0)
1016
(booleanp dememtoreg0) (booleanp emmemtoreg0)
1017
(integerp emimm0) (booleanp emuseimm0)
1018
(booleanp dememwrite0) (booleanp emmemwrite0)
1019
(integerp emarg20) (integerp ffinst0)
1020
(integerp mmval0) (integerp mmdest0)
1021
(booleanp mmregwrite0) (integerp mmresult0)
1022
(booleanp mmmemwrite0) (integerp mmarg20))
1023
(let* ((st0 (initialize_a nil nil nil nil nil pc0
1024
bpstate0 ffpredicteddirection0
1025
ffpredictedtarget0 ffwrt0 ffinst0
1026
ffppc0 fdppc0 fdwrt0 fdinst0
1027
fdpredicteddirection0
1028
fdpredictedtarget0 deppc0 desrc10
1029
desrc20 a1 a2 dedest0 deop0 deimm0
1030
deuseimm0 deregwrite0 dememwrite0
1031
dememtoreg0 deisbranch0 dewrt0
1032
depredicteddirection0
1033
depredictedtarget0 emppc0
1034
emis_taken_branch0 emtargetpc0 emarg20
1035
emresult0 emdest0 emwrt0
1036
emmispredictedtaken0
1037
emmispredictednottaken0 emregwrite0
1038
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1039
mmval0 mmdest0 mmwrt0 mmregwrite0
1040
mwppc0 mwval0 mwdest0 mwwrt0
1042
(st1 (simulate_a st0 t nil nil nil pc0 bpstate0
1043
ffpredicteddirection0
1044
ffpredictedtarget0 ffwrt0 ffinst0
1045
ffppc0 fdppc0 fdwrt0 fdinst0
1046
fdpredicteddirection0
1047
fdpredictedtarget0 deppc0 desrc10
1048
desrc20 a1 a2 dedest0 deop0 deimm0
1049
deuseimm0 deregwrite0 dememwrite0
1050
dememtoreg0 deisbranch0 dewrt0
1051
depredicteddirection0
1052
depredictedtarget0 emppc0
1053
emis_taken_branch0 emtargetpc0 emarg20
1054
emresult0 emdest0 emwrt0
1055
emmispredictedtaken0
1056
emmispredictednottaken0 emregwrite0
1057
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1058
mmval0 mmdest0 mmwrt0 mmregwrite0
1059
mwppc0 mwval0 mwdest0 mwwrt0
1060
mwregwrite0 (g 'ppc (g 'impl st0))
1061
(g 'prf (g 'impl st0))
1062
(g 'pdmem (g 'impl st0))))
1063
(st2 (simulate_a st1 t nil nil nil pc0 bpstate0
1064
ffpredicteddirection0
1065
ffpredictedtarget0 ffwrt0 ffinst0
1066
ffppc0 fdppc0 fdwrt0 fdinst0
1067
fdpredicteddirection0
1068
fdpredictedtarget0 deppc0 desrc10
1069
desrc20 a1 a2 dedest0 deop0 deimm0
1070
deuseimm0 deregwrite0 dememwrite0
1071
dememtoreg0 deisbranch0 dewrt0
1072
depredicteddirection0
1073
depredictedtarget0 emppc0
1074
emis_taken_branch0 emtargetpc0 emarg20
1075
emresult0 emdest0 emwrt0
1076
emmispredictedtaken0
1077
emmispredictednottaken0 emregwrite0
1078
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1079
mmval0 mmdest0 mmwrt0 mmregwrite0
1080
mwppc0 mwval0 mwdest0 mwwrt0
1081
mwregwrite0 (g 'ppc (g 'impl st1))
1082
(g 'prf (g 'impl st1))
1083
(g 'pdmem (g 'impl st1))))
1084
(st3 (simulate_a st2 t nil nil nil pc0 bpstate0
1085
ffpredicteddirection0
1086
ffpredictedtarget0 ffwrt0 ffinst0
1087
ffppc0 fdppc0 fdwrt0 fdinst0
1088
fdpredicteddirection0
1089
fdpredictedtarget0 deppc0 desrc10
1090
desrc20 a1 a2 dedest0 deop0 deimm0
1091
deuseimm0 deregwrite0 dememwrite0
1092
dememtoreg0 deisbranch0 dewrt0
1093
depredicteddirection0
1094
depredictedtarget0 emppc0
1095
emis_taken_branch0 emtargetpc0 emarg20
1096
emresult0 emdest0 emwrt0
1097
emmispredictedtaken0
1098
emmispredictednottaken0 emregwrite0
1099
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1100
mmval0 mmdest0 mmwrt0 mmregwrite0
1101
mwppc0 mwval0 mwdest0 mwwrt0
1102
mwregwrite0 (g 'ppc (g 'impl st2))
1103
(g 'prf (g 'impl st2))
1104
(g 'pdmem (g 'impl st2))))
1105
(st4 (simulate_a st3 t nil nil nil pc0 bpstate0
1106
ffpredicteddirection0
1107
ffpredictedtarget0 ffwrt0 ffinst0
1108
ffppc0 fdppc0 fdwrt0 fdinst0
1109
fdpredicteddirection0
1110
fdpredictedtarget0 deppc0 desrc10
1111
desrc20 a1 a2 dedest0 deop0 deimm0
1112
deuseimm0 deregwrite0 dememwrite0
1113
dememtoreg0 deisbranch0 dewrt0
1114
depredicteddirection0
1115
depredictedtarget0 emppc0
1116
emis_taken_branch0 emtargetpc0 emarg20
1117
emresult0 emdest0 emwrt0
1118
emmispredictedtaken0
1119
emmispredictednottaken0 emregwrite0
1120
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1121
mmval0 mmdest0 mmwrt0 mmregwrite0
1122
mwppc0 mwval0 mwdest0 mwwrt0
1123
mwregwrite0 (g 'ppc (g 'impl st3))
1124
(g 'prf (g 'impl st3))
1125
(g 'pdmem (g 'impl st3))))
1126
(st5 (simulate_a st4 t nil nil nil pc0 bpstate0
1127
ffpredicteddirection0
1128
ffpredictedtarget0 ffwrt0 ffinst0
1129
ffppc0 fdppc0 fdwrt0 fdinst0
1130
fdpredicteddirection0
1131
fdpredictedtarget0 deppc0 desrc10
1132
desrc20 a1 a2 dedest0 deop0 deimm0
1133
deuseimm0 deregwrite0 dememwrite0
1134
dememtoreg0 deisbranch0 dewrt0
1135
depredicteddirection0
1136
depredictedtarget0 emppc0
1137
emis_taken_branch0 emtargetpc0 emarg20
1138
emresult0 emdest0 emwrt0
1139
emmispredictedtaken0
1140
emmispredictednottaken0 emregwrite0
1141
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1142
mmval0 mmdest0 mmwrt0 mmregwrite0
1143
mwppc0 mwval0 mwdest0 mwwrt0
1144
mwregwrite0 (g 'ppc (g 'impl st4))
1145
(g 'prf (g 'impl st4))
1146
(g 'pdmem (g 'impl st4))))
1147
(st6 (simulate_a st5 t nil nil nil pc0 bpstate0
1148
ffpredicteddirection0
1149
ffpredictedtarget0 ffwrt0 ffinst0
1150
ffppc0 fdppc0 fdwrt0 fdinst0
1151
fdpredicteddirection0
1152
fdpredictedtarget0 deppc0 desrc10
1153
desrc20 a1 a2 dedest0 deop0 deimm0
1154
deuseimm0 deregwrite0 dememwrite0
1155
dememtoreg0 deisbranch0 dewrt0
1156
depredicteddirection0
1157
depredictedtarget0 emppc0
1158
emis_taken_branch0 emtargetpc0 emarg20
1159
emresult0 emdest0 emwrt0
1160
emmispredictedtaken0
1161
emmispredictednottaken0 emregwrite0
1162
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1163
mmval0 mmdest0 mmwrt0 mmregwrite0
1164
mwppc0 mwval0 mwdest0 mwwrt0
1165
mwregwrite0 (g 'ppc (g 'impl st5))
1166
(g 'prf (g 'impl st5))
1167
(g 'pdmem (g 'impl st5))))
1171
(or (g 'ffwrt (g 'impl st6))
1172
(g 'fdwrt (g 'impl st6)))
1173
(g 'dewrt (g 'impl st6)))
1174
(g 'emwrt (g 'impl st6)))
1175
(g 'mmwrt (g 'impl st6)))
1176
(g 'mwwrt (g 'impl st6)))))
1177
(st7 (simulate_a st6 t nil nil nil pc0 bpstate0
1178
ffpredicteddirection0
1179
ffpredictedtarget0 ffwrt0 ffinst0
1180
ffppc0 fdppc0 fdwrt0 fdinst0
1181
fdpredicteddirection0
1182
fdpredictedtarget0 deppc0 desrc10
1183
desrc20 a1 a2 dedest0 deop0 deimm0
1184
deuseimm0 deregwrite0 dememwrite0
1185
dememtoreg0 deisbranch0 dewrt0
1186
depredicteddirection0
1187
depredictedtarget0 emppc0
1188
emis_taken_branch0 emtargetpc0 emarg20
1189
emresult0 emdest0 emwrt0
1190
emmispredictedtaken0
1191
emmispredictednottaken0 emregwrite0
1192
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1193
mmval0 mmdest0 mmwrt0 mmregwrite0
1194
mwppc0 mwval0 mwdest0 mwwrt0
1195
mwregwrite0 (g 'ppc (g 'impl st6))
1196
(g 'prf (g 'impl st6))
1197
(g 'pdmem (g 'impl st6))))
1201
(or (g 'ffwrt (g 'impl st7))
1202
(g 'fdwrt (g 'impl st7)))
1203
(g 'dewrt (g 'impl st7)))
1204
(g 'emwrt (g 'impl st7)))
1205
(g 'mmwrt (g 'impl st7)))
1206
(g 'mwwrt (g 'impl st7)))))
1207
(st8 (simulate_a st7 t nil nil nil pc0 bpstate0
1208
ffpredicteddirection0
1209
ffpredictedtarget0 ffwrt0 ffinst0
1210
ffppc0 fdppc0 fdwrt0 fdinst0
1211
fdpredicteddirection0
1212
fdpredictedtarget0 deppc0 desrc10
1213
desrc20 a1 a2 dedest0 deop0 deimm0
1214
deuseimm0 deregwrite0 dememwrite0
1215
dememtoreg0 deisbranch0 dewrt0
1216
depredicteddirection0
1217
depredictedtarget0 emppc0
1218
emis_taken_branch0 emtargetpc0 emarg20
1219
emresult0 emdest0 emwrt0
1220
emmispredictedtaken0
1221
emmispredictednottaken0 emregwrite0
1222
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1223
mmval0 mmdest0 mmwrt0 mmregwrite0
1224
mwppc0 mwval0 mwdest0 mwwrt0
1225
mwregwrite0 (g 'ppc (g 'impl st7))
1226
(g 'prf (g 'impl st7))
1227
(g 'pdmem (g 'impl st7))))
1231
(t (add-1 (add-1 zero)))))
1232
(st9 (simulate_a st8 nil nil t nil pc0 bpstate0
1233
ffpredicteddirection0
1234
ffpredictedtarget0 ffwrt0 ffinst0
1235
ffppc0 fdppc0 fdwrt0 fdinst0
1236
fdpredicteddirection0
1237
fdpredictedtarget0 deppc0 desrc10
1238
desrc20 a1 a2 dedest0 deop0 deimm0
1239
deuseimm0 deregwrite0 dememwrite0
1240
dememtoreg0 deisbranch0 dewrt0
1241
depredicteddirection0
1242
depredictedtarget0 emppc0
1243
emis_taken_branch0 emtargetpc0 emarg20
1244
emresult0 emdest0 emwrt0
1245
emmispredictedtaken0
1246
emmispredictednottaken0 emregwrite0
1247
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1248
mmval0 mmdest0 mmwrt0 mmregwrite0
1249
mwppc0 mwval0 mwdest0 mwwrt0
1250
mwregwrite0 (g 'ppc (g 'impl st8))
1251
(g 'prf (g 'impl st8))
1252
(g 'pdmem (g 'impl st8))))
1253
(s_pc0 (g 'spc (g 'spec st9)))
1254
(s_rf0 (g 'srf (g 'spec st9)))
1255
(s_dmem0 (g 'sdmem (g 'spec st9)))
1256
(st10 (simulate_a st9 nil t nil nil pc0
1257
bpstate0 ffpredicteddirection0
1258
ffpredictedtarget0 ffwrt0 ffinst0
1259
ffppc0 fdppc0 fdwrt0 fdinst0
1260
fdpredicteddirection0
1261
fdpredictedtarget0 deppc0 desrc10
1262
desrc20 a1 a2 dedest0 deop0 deimm0
1263
deuseimm0 deregwrite0 dememwrite0
1264
dememtoreg0 deisbranch0 dewrt0
1265
depredicteddirection0
1266
depredictedtarget0 emppc0
1267
emis_taken_branch0 emtargetpc0
1268
emarg20 emresult0 emdest0 emwrt0
1269
emmispredictedtaken0
1270
emmispredictednottaken0 emregwrite0
1271
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1272
mmval0 mmdest0 mmwrt0 mmregwrite0
1273
mwppc0 mwval0 mwdest0 mwwrt0
1274
mwregwrite0 (g 'ppc (g 'impl st9))
1275
(g 'prf (g 'impl st9))
1276
(g 'pdmem (g 'impl st9))))
1277
(s_pc1 (g 'spc (g 'spec st10)))
1278
(s_rf1 (g 'srf (g 'spec st10)))
1279
(s_dmem1 (g 'sdmem (g 'spec st10)))
1280
(st11 (simulate_a st10 nil nil nil t pc0
1281
bpstate0 ffpredicteddirection0
1282
ffpredictedtarget0 ffwrt0 ffinst0
1283
ffppc0 fdppc0 fdwrt0 fdinst0
1284
fdpredicteddirection0
1285
fdpredictedtarget0 deppc0 desrc10
1286
desrc20 a1 a2 dedest0 deop0 deimm0
1287
deuseimm0 deregwrite0 dememwrite0
1288
dememtoreg0 deisbranch0 dewrt0
1289
depredicteddirection0
1290
depredictedtarget0 emppc0
1291
emis_taken_branch0 emtargetpc0
1292
emarg20 emresult0 emdest0 emwrt0
1293
emmispredictedtaken0
1294
emmispredictednottaken0 emregwrite0
1295
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1296
mmval0 mmdest0 mmwrt0 mmregwrite0
1297
mwppc0 mwval0 mwdest0 mwwrt0
1298
mwregwrite0 (g 'ppc (g 'impl st10))
1299
(g 'prf (g 'impl st10))
1300
(g 'pdmem (g 'impl st10))))
1301
(st12 (simulate_a st11 nil nil nil nil pc0
1302
bpstate0 ffpredicteddirection0
1303
ffpredictedtarget0 ffwrt0 ffinst0
1304
ffppc0 fdppc0 fdwrt0 fdinst0
1305
fdpredicteddirection0
1306
fdpredictedtarget0 deppc0 desrc10
1307
desrc20 a1 a2 dedest0 deop0 deimm0
1308
deuseimm0 deregwrite0 dememwrite0
1309
dememtoreg0 deisbranch0 dewrt0
1310
depredicteddirection0
1311
depredictedtarget0 emppc0
1312
emis_taken_branch0 emtargetpc0
1313
emarg20 emresult0 emdest0 emwrt0
1314
emmispredictedtaken0
1315
emmispredictednottaken0 emregwrite0
1316
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1317
mmval0 mmdest0 mmwrt0 mmregwrite0
1318
mwppc0 mwval0 mwdest0 mwwrt0
1319
mwregwrite0 (g 'ppc (g 'impl st11))
1320
(g 'prf (g 'impl st11))
1321
(g 'pdmem (g 'impl st11))))
1322
(st13 (simulate_a st12 nil nil nil nil pc0
1323
bpstate0 ffpredicteddirection0
1324
ffpredictedtarget0 ffwrt0 ffinst0
1325
ffppc0 fdppc0 fdwrt0 fdinst0
1326
fdpredicteddirection0
1327
fdpredictedtarget0 deppc0 desrc10
1328
desrc20 a1 a2 dedest0 deop0 deimm0
1329
deuseimm0 deregwrite0 dememwrite0
1330
dememtoreg0 deisbranch0 dewrt0
1331
depredicteddirection0
1332
depredictedtarget0 emppc0
1333
emis_taken_branch0 emtargetpc0
1334
emarg20 emresult0 emdest0 emwrt0
1335
emmispredictedtaken0
1336
emmispredictednottaken0 emregwrite0
1337
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1338
mmval0 mmdest0 mmwrt0 mmregwrite0
1339
mwppc0 mwval0 mwdest0 mwwrt0
1340
mwregwrite0 (g 'ppc (g 'impl st12))
1341
(g 'prf (g 'impl st12))
1342
(g 'pdmem (g 'impl st12))))
1343
(st14 (simulate_a st13 nil nil nil nil pc0
1344
bpstate0 ffpredicteddirection0
1345
ffpredictedtarget0 ffwrt0 ffinst0
1346
ffppc0 fdppc0 fdwrt0 fdinst0
1347
fdpredicteddirection0
1348
fdpredictedtarget0 deppc0 desrc10
1349
desrc20 a1 a2 dedest0 deop0 deimm0
1350
deuseimm0 deregwrite0 dememwrite0
1351
dememtoreg0 deisbranch0 dewrt0
1352
depredicteddirection0
1353
depredictedtarget0 emppc0
1354
emis_taken_branch0 emtargetpc0
1355
emarg20 emresult0 emdest0 emwrt0
1356
emmispredictedtaken0
1357
emmispredictednottaken0 emregwrite0
1358
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1359
mmval0 mmdest0 mmwrt0 mmregwrite0
1360
mwppc0 mwval0 mwdest0 mwwrt0
1361
mwregwrite0 (g 'ppc (g 'impl st13))
1362
(g 'prf (g 'impl st13))
1363
(g 'pdmem (g 'impl st13))))
1364
(st15 (simulate_a st14 nil nil nil nil pc0
1365
bpstate0 ffpredicteddirection0
1366
ffpredictedtarget0 ffwrt0 ffinst0
1367
ffppc0 fdppc0 fdwrt0 fdinst0
1368
fdpredicteddirection0
1369
fdpredictedtarget0 deppc0 desrc10
1370
desrc20 a1 a2 dedest0 deop0 deimm0
1371
deuseimm0 deregwrite0 dememwrite0
1372
dememtoreg0 deisbranch0 dewrt0
1373
depredicteddirection0
1374
depredictedtarget0 emppc0
1375
emis_taken_branch0 emtargetpc0
1376
emarg20 emresult0 emdest0 emwrt0
1377
emmispredictedtaken0
1378
emmispredictednottaken0 emregwrite0
1379
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1380
mmval0 mmdest0 mmwrt0 mmregwrite0
1381
mwppc0 mwval0 mwdest0 mwwrt0
1382
mwregwrite0 (g 'ppc (g 'impl st14))
1383
(g 'prf (g 'impl st14))
1384
(g 'pdmem (g 'impl st14))))
1385
(st16 (simulate_a st15 nil nil nil nil pc0
1386
bpstate0 ffpredicteddirection0
1387
ffpredictedtarget0 ffwrt0 ffinst0
1388
ffppc0 fdppc0 fdwrt0 fdinst0
1389
fdpredicteddirection0
1390
fdpredictedtarget0 deppc0 desrc10
1391
desrc20 a1 a2 dedest0 deop0 deimm0
1392
deuseimm0 deregwrite0 dememwrite0
1393
dememtoreg0 deisbranch0 dewrt0
1394
depredicteddirection0
1395
depredictedtarget0 emppc0
1396
emis_taken_branch0 emtargetpc0
1397
emarg20 emresult0 emdest0 emwrt0
1398
emmispredictedtaken0
1399
emmispredictednottaken0 emregwrite0
1400
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1401
mmval0 mmdest0 mmwrt0 mmregwrite0
1402
mwppc0 mwval0 mwdest0 mwwrt0
1403
mwregwrite0 (g 'ppc (g 'impl st15))
1404
(g 'prf (g 'impl st15))
1405
(g 'pdmem (g 'impl st15))))
1406
(st17 (simulate_a st16 nil nil nil nil pc0
1407
bpstate0 ffpredicteddirection0
1408
ffpredictedtarget0 ffwrt0 ffinst0
1409
ffppc0 fdppc0 fdwrt0 fdinst0
1410
fdpredicteddirection0
1411
fdpredictedtarget0 deppc0 desrc10
1412
desrc20 a1 a2 dedest0 deop0 deimm0
1413
deuseimm0 deregwrite0 dememwrite0
1414
dememtoreg0 deisbranch0 dewrt0
1415
depredicteddirection0
1416
depredictedtarget0 emppc0
1417
emis_taken_branch0 emtargetpc0
1418
emarg20 emresult0 emdest0 emwrt0
1419
emmispredictedtaken0
1420
emmispredictednottaken0 emregwrite0
1421
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1422
mmval0 mmdest0 mmwrt0 mmregwrite0
1423
mwppc0 mwval0 mwdest0 mwwrt0
1424
mwregwrite0 (g 'ppc (g 'impl st16))
1425
(g 'prf (g 'impl st16))
1426
(g 'pdmem (g 'impl st16))))
1427
(t1 (g 'mwwrt (g 'impl st17)))
1428
(st18 (simulate_a st17 nil nil nil nil pc0
1429
bpstate0 ffpredicteddirection0
1430
ffpredictedtarget0 ffwrt0 ffinst0
1431
ffppc0 fdppc0 fdwrt0 fdinst0
1432
fdpredicteddirection0
1433
fdpredictedtarget0 deppc0 desrc10
1434
desrc20 a1 a2 dedest0 deop0 deimm0
1435
deuseimm0 deregwrite0 dememwrite0
1436
dememtoreg0 deisbranch0 dewrt0
1437
depredicteddirection0
1438
depredictedtarget0 emppc0
1439
emis_taken_branch0 emtargetpc0
1440
emarg20 emresult0 emdest0 emwrt0
1441
emmispredictedtaken0
1442
emmispredictednottaken0 emregwrite0
1443
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1444
mmval0 mmdest0 mmwrt0 mmregwrite0
1445
mwppc0 mwval0 mwdest0 mwwrt0
1446
mwregwrite0 (g 'ppc (g 'impl st17))
1447
(g 'prf (g 'impl st17))
1448
(g 'pdmem (g 'impl st17))))
1449
(t2 (g 'mwwrt (g 'impl st18)))
1450
(st19 (simulate_a st18 nil nil nil nil pc0
1451
bpstate0 ffpredicteddirection0
1452
ffpredictedtarget0 ffwrt0 ffinst0
1453
ffppc0 fdppc0 fdwrt0 fdinst0
1454
fdpredicteddirection0
1455
fdpredictedtarget0 deppc0 desrc10
1456
desrc20 a1 a2 dedest0 deop0 deimm0
1457
deuseimm0 deregwrite0 dememwrite0
1458
dememtoreg0 deisbranch0 dewrt0
1459
depredicteddirection0
1460
depredictedtarget0 emppc0
1461
emis_taken_branch0 emtargetpc0
1462
emarg20 emresult0 emdest0 emwrt0
1463
emmispredictedtaken0
1464
emmispredictednottaken0 emregwrite0
1465
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1466
mmval0 mmdest0 mmwrt0 mmregwrite0
1467
mwppc0 mwval0 mwdest0 mwwrt0
1468
mwregwrite0 (g 'ppc (g 'impl st18))
1469
(g 'prf (g 'impl st18))
1470
(g 'pdmem (g 'impl st18))))
1471
(t3 (g 'mwwrt (g 'impl st19)))
1472
(st20 (simulate_a st19 nil nil nil nil pc0
1473
bpstate0 ffpredicteddirection0
1474
ffpredictedtarget0 ffwrt0 ffinst0
1475
ffppc0 fdppc0 fdwrt0 fdinst0
1476
fdpredicteddirection0
1477
fdpredictedtarget0 deppc0 desrc10
1478
desrc20 a1 a2 dedest0 deop0 deimm0
1479
deuseimm0 deregwrite0 dememwrite0
1480
dememtoreg0 deisbranch0 dewrt0
1481
depredicteddirection0
1482
depredictedtarget0 emppc0
1483
emis_taken_branch0 emtargetpc0
1484
emarg20 emresult0 emdest0 emwrt0
1485
emmispredictedtaken0
1486
emmispredictednottaken0 emregwrite0
1487
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1488
mmval0 mmdest0 mmwrt0 mmregwrite0
1489
mwppc0 mwval0 mwdest0 mwwrt0
1490
mwregwrite0 (g 'ppc (g 'impl st19))
1491
(g 'prf (g 'impl st19))
1492
(g 'pdmem (g 'impl st19))))
1493
(t4 (g 'mwwrt (g 'impl st20)))
1494
(st21 (simulate_a st20 nil nil nil nil pc0
1495
bpstate0 ffpredicteddirection0
1496
ffpredictedtarget0 ffwrt0 ffinst0
1497
ffppc0 fdppc0 fdwrt0 fdinst0
1498
fdpredicteddirection0
1499
fdpredictedtarget0 deppc0 desrc10
1500
desrc20 a1 a2 dedest0 deop0 deimm0
1501
deuseimm0 deregwrite0 dememwrite0
1502
dememtoreg0 deisbranch0 dewrt0
1503
depredicteddirection0
1504
depredictedtarget0 emppc0
1505
emis_taken_branch0 emtargetpc0
1506
emarg20 emresult0 emdest0 emwrt0
1507
emmispredictedtaken0
1508
emmispredictednottaken0 emregwrite0
1509
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1510
mmval0 mmdest0 mmwrt0 mmregwrite0
1511
mwppc0 mwval0 mwdest0 mwwrt0
1512
mwregwrite0 (g 'ppc (g 'impl st20))
1513
(g 'prf (g 'impl st20))
1514
(g 'pdmem (g 'impl st20))))
1515
(t5 (g 'mwwrt (g 'impl st21)))
1516
(st22 (simulate_a st21 nil nil nil nil pc0
1517
bpstate0 ffpredicteddirection0
1518
ffpredictedtarget0 ffwrt0 ffinst0
1519
ffppc0 fdppc0 fdwrt0 fdinst0
1520
fdpredicteddirection0
1521
fdpredictedtarget0 deppc0 desrc10
1522
desrc20 a1 a2 dedest0 deop0 deimm0
1523
deuseimm0 deregwrite0 dememwrite0
1524
dememtoreg0 deisbranch0 dewrt0
1525
depredicteddirection0
1526
depredictedtarget0 emppc0
1527
emis_taken_branch0 emtargetpc0
1528
emarg20 emresult0 emdest0 emwrt0
1529
emmispredictedtaken0
1530
emmispredictednottaken0 emregwrite0
1531
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1532
mmval0 mmdest0 mmwrt0 mmregwrite0
1533
mwppc0 mwval0 mwdest0 mwwrt0
1534
mwregwrite0 (g 'ppc (g 'impl st21))
1535
(g 'prf (g 'impl st21))
1536
(g 'pdmem (g 'impl st21))))
1537
(t6 (g 'mwwrt (g 'impl st22)))
1539
((and (equal counter zero) t1)
1542
(or (equal counter zero)
1543
(equal counter (add-1 zero)))
1545
(add-1 (add-1 counter)))
1546
(t3 (add-1 (add-1 (add-1 counter))))
1548
(add-1 (add-1 (add-1 counter)))))
1551
(add-1 (add-1 (add-1 counter))))))
1556
(add-1 (add-1 counter)))))))
1562
(add-1 (add-1 counter))))))))))
1563
(st23 (simulate_a st22 nil nil nil t pc0
1564
bpstate0 ffpredicteddirection0
1565
ffpredictedtarget0 ffwrt0 ffinst0
1566
ffppc0 fdppc0 fdwrt0 fdinst0
1567
fdpredicteddirection0
1568
fdpredictedtarget0 deppc0 desrc10
1569
desrc20 a1 a2 dedest0 deop0 deimm0
1570
deuseimm0 deregwrite0 dememwrite0
1571
dememtoreg0 deisbranch0 dewrt0
1572
depredicteddirection0
1573
depredictedtarget0 emppc0
1574
emis_taken_branch0 emtargetpc0
1575
emarg20 emresult0 emdest0 emwrt0
1576
emmispredictedtaken0
1577
emmispredictednottaken0 emregwrite0
1578
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1579
mmval0 mmdest0 mmwrt0 mmregwrite0
1580
mwppc0 mwval0 mwdest0 mwwrt0
1581
mwregwrite0 (g 'ppc (g 'impl st22))
1582
(g 'prf (g 'impl st22))
1583
(g 'pdmem (g 'impl st22))))
1584
(st24 (simulate_a st23 nil nil nil nil pc0
1585
bpstate0 ffpredicteddirection0
1586
ffpredictedtarget0 ffwrt0 ffinst0
1587
ffppc0 fdppc0 fdwrt0 fdinst0
1588
fdpredicteddirection0
1589
fdpredictedtarget0 deppc0 desrc10
1590
desrc20 a1 a2 dedest0 deop0 deimm0
1591
deuseimm0 deregwrite0 dememwrite0
1592
dememtoreg0 deisbranch0 dewrt0
1593
depredicteddirection0
1594
depredictedtarget0 emppc0
1595
emis_taken_branch0 emtargetpc0
1596
emarg20 emresult0 emdest0 emwrt0
1597
emmispredictedtaken0
1598
emmispredictednottaken0 emregwrite0
1599
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1600
mmval0 mmdest0 mmwrt0 mmregwrite0
1601
mwppc0 mwval0 mwdest0 mwwrt0
1602
mwregwrite0 (g 'ppc (g 'impl st23))
1603
(g 'prf (g 'impl st23))
1604
(g 'pdmem (g 'impl st23))))
1605
(st25 (simulate_a st24 t nil nil nil pc0
1606
bpstate0 ffpredicteddirection0
1607
ffpredictedtarget0 ffwrt0 ffinst0
1608
ffppc0 fdppc0 fdwrt0 fdinst0
1609
fdpredicteddirection0
1610
fdpredictedtarget0 deppc0 desrc10
1611
desrc20 a1 a2 dedest0 deop0 deimm0
1612
deuseimm0 deregwrite0 dememwrite0
1613
dememtoreg0 deisbranch0 dewrt0
1614
depredicteddirection0
1615
depredictedtarget0 emppc0
1616
emis_taken_branch0 emtargetpc0
1617
emarg20 emresult0 emdest0 emwrt0
1618
emmispredictedtaken0
1619
emmispredictednottaken0 emregwrite0
1620
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1621
mmval0 mmdest0 mmwrt0 mmregwrite0
1622
mwppc0 mwval0 mwdest0 mwwrt0
1623
mwregwrite0 (g 'ppc (g 'impl st24))
1624
(g 'prf (g 'impl st24))
1625
(g 'pdmem (g 'impl st24))))
1626
(st26 (simulate_a st25 t nil nil nil pc0
1627
bpstate0 ffpredicteddirection0
1628
ffpredictedtarget0 ffwrt0 ffinst0
1629
ffppc0 fdppc0 fdwrt0 fdinst0
1630
fdpredicteddirection0
1631
fdpredictedtarget0 deppc0 desrc10
1632
desrc20 a1 a2 dedest0 deop0 deimm0
1633
deuseimm0 deregwrite0 dememwrite0
1634
dememtoreg0 deisbranch0 dewrt0
1635
depredicteddirection0
1636
depredictedtarget0 emppc0
1637
emis_taken_branch0 emtargetpc0
1638
emarg20 emresult0 emdest0 emwrt0
1639
emmispredictedtaken0
1640
emmispredictednottaken0 emregwrite0
1641
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1642
mmval0 mmdest0 mmwrt0 mmregwrite0
1643
mwppc0 mwval0 mwdest0 mwwrt0
1644
mwregwrite0 (g 'ppc (g 'impl st25))
1645
(g 'prf (g 'impl st25))
1646
(g 'pdmem (g 'impl st25))))
1647
(st27 (simulate_a st26 t nil nil nil pc0
1648
bpstate0 ffpredicteddirection0
1649
ffpredictedtarget0 ffwrt0 ffinst0
1650
ffppc0 fdppc0 fdwrt0 fdinst0
1651
fdpredicteddirection0
1652
fdpredictedtarget0 deppc0 desrc10
1653
desrc20 a1 a2 dedest0 deop0 deimm0
1654
deuseimm0 deregwrite0 dememwrite0
1655
dememtoreg0 deisbranch0 dewrt0
1656
depredicteddirection0
1657
depredictedtarget0 emppc0
1658
emis_taken_branch0 emtargetpc0
1659
emarg20 emresult0 emdest0 emwrt0
1660
emmispredictedtaken0
1661
emmispredictednottaken0 emregwrite0
1662
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1663
mmval0 mmdest0 mmwrt0 mmregwrite0
1664
mwppc0 mwval0 mwdest0 mwwrt0
1665
mwregwrite0 (g 'ppc (g 'impl st26))
1666
(g 'prf (g 'impl st26))
1667
(g 'pdmem (g 'impl st26))))
1668
(st28 (simulate_a st27 t nil nil nil pc0
1669
bpstate0 ffpredicteddirection0
1670
ffpredictedtarget0 ffwrt0 ffinst0
1671
ffppc0 fdppc0 fdwrt0 fdinst0
1672
fdpredicteddirection0
1673
fdpredictedtarget0 deppc0 desrc10
1674
desrc20 a1 a2 dedest0 deop0 deimm0
1675
deuseimm0 deregwrite0 dememwrite0
1676
dememtoreg0 deisbranch0 dewrt0
1677
depredicteddirection0
1678
depredictedtarget0 emppc0
1679
emis_taken_branch0 emtargetpc0
1680
emarg20 emresult0 emdest0 emwrt0
1681
emmispredictedtaken0
1682
emmispredictednottaken0 emregwrite0
1683
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1684
mmval0 mmdest0 mmwrt0 mmregwrite0
1685
mwppc0 mwval0 mwdest0 mwwrt0
1686
mwregwrite0 (g 'ppc (g 'impl st27))
1687
(g 'prf (g 'impl st27))
1688
(g 'pdmem (g 'impl st27))))
1689
(st29 (simulate_a st28 t nil nil nil pc0
1690
bpstate0 ffpredicteddirection0
1691
ffpredictedtarget0 ffwrt0 ffinst0
1692
ffppc0 fdppc0 fdwrt0 fdinst0
1693
fdpredicteddirection0
1694
fdpredictedtarget0 deppc0 desrc10
1695
desrc20 a1 a2 dedest0 deop0 deimm0
1696
deuseimm0 deregwrite0 dememwrite0
1697
dememtoreg0 deisbranch0 dewrt0
1698
depredicteddirection0
1699
depredictedtarget0 emppc0
1700
emis_taken_branch0 emtargetpc0
1701
emarg20 emresult0 emdest0 emwrt0
1702
emmispredictedtaken0
1703
emmispredictednottaken0 emregwrite0
1704
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1705
mmval0 mmdest0 mmwrt0 mmregwrite0
1706
mwppc0 mwval0 mwdest0 mwwrt0
1707
mwregwrite0 (g 'ppc (g 'impl st28))
1708
(g 'prf (g 'impl st28))
1709
(g 'pdmem (g 'impl st28))))
1710
(st30 (simulate_a st29 t nil nil nil pc0
1711
bpstate0 ffpredicteddirection0
1712
ffpredictedtarget0 ffwrt0 ffinst0
1713
ffppc0 fdppc0 fdwrt0 fdinst0
1714
fdpredicteddirection0
1715
fdpredictedtarget0 deppc0 desrc10
1716
desrc20 a1 a2 dedest0 deop0 deimm0
1717
deuseimm0 deregwrite0 dememwrite0
1718
dememtoreg0 deisbranch0 dewrt0
1719
depredicteddirection0
1720
depredictedtarget0 emppc0
1721
emis_taken_branch0 emtargetpc0
1722
emarg20 emresult0 emdest0 emwrt0
1723
emmispredictedtaken0
1724
emmispredictednottaken0 emregwrite0
1725
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1726
mmval0 mmdest0 mmwrt0 mmregwrite0
1727
mwppc0 mwval0 mwdest0 mwwrt0
1728
mwregwrite0 (g 'ppc (g 'impl st29))
1729
(g 'prf (g 'impl st29))
1730
(g 'pdmem (g 'impl st29))))
1734
(or (g 'ffwrt (g 'impl st30))
1735
(g 'fdwrt (g 'impl st30)))
1736
(g 'dewrt (g 'impl st30)))
1737
(g 'emwrt (g 'impl st30)))
1738
(g 'mmwrt (g 'impl st30)))
1739
(g 'mwwrt (g 'impl st30)))))
1740
(st31 (simulate_a st30 t nil nil nil pc0
1741
bpstate0 ffpredicteddirection0
1742
ffpredictedtarget0 ffwrt0 ffinst0
1743
ffppc0 fdppc0 fdwrt0 fdinst0
1744
fdpredicteddirection0
1745
fdpredictedtarget0 deppc0 desrc10
1746
desrc20 a1 a2 dedest0 deop0 deimm0
1747
deuseimm0 deregwrite0 dememwrite0
1748
dememtoreg0 deisbranch0 dewrt0
1749
depredicteddirection0
1750
depredictedtarget0 emppc0
1751
emis_taken_branch0 emtargetpc0
1752
emarg20 emresult0 emdest0 emwrt0
1753
emmispredictedtaken0
1754
emmispredictednottaken0 emregwrite0
1755
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1756
mmval0 mmdest0 mmwrt0 mmregwrite0
1757
mwppc0 mwval0 mwdest0 mwwrt0
1758
mwregwrite0 (g 'ppc (g 'impl st30))
1759
(g 'prf (g 'impl st30))
1760
(g 'pdmem (g 'impl st30))))
1764
(or (g 'ffwrt (g 'impl st31))
1765
(g 'fdwrt (g 'impl st31)))
1766
(g 'dewrt (g 'impl st31)))
1767
(g 'emwrt (g 'impl st31)))
1768
(g 'mmwrt (g 'impl st31)))
1769
(g 'mwwrt (g 'impl st31)))))
1770
(st32 (simulate_a st31 t nil nil nil pc0
1771
bpstate0 ffpredicteddirection0
1772
ffpredictedtarget0 ffwrt0 ffinst0
1773
ffppc0 fdppc0 fdwrt0 fdinst0
1774
fdpredicteddirection0
1775
fdpredictedtarget0 deppc0 desrc10
1776
desrc20 a1 a2 dedest0 deop0 deimm0
1777
deuseimm0 deregwrite0 dememwrite0
1778
dememtoreg0 deisbranch0 dewrt0
1779
depredicteddirection0
1780
depredictedtarget0 emppc0
1781
emis_taken_branch0 emtargetpc0
1782
emarg20 emresult0 emdest0 emwrt0
1783
emmispredictedtaken0
1784
emmispredictednottaken0 emregwrite0
1785
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1786
mmval0 mmdest0 mmwrt0 mmregwrite0
1787
mwppc0 mwval0 mwdest0 mwwrt0
1788
mwregwrite0 (g 'ppc (g 'impl st31))
1789
(g 'prf (g 'impl st31))
1790
(g 'pdmem (g 'impl st31))))
1794
(t (add-1 (add-1 zero)))))
1795
(i_pc (g 'ppc (g 'impl st32)))
1796
(i_rf (g 'prf (g 'impl st32)))
1797
(i_dmem (g 'pdmem (g 'impl st32)))
1798
(st33 (simulate_a st32 nil nil nil t pc0
1799
bpstate0 ffpredicteddirection0
1800
ffpredictedtarget0 ffwrt0 ffinst0
1801
ffppc0 fdppc0 fdwrt0 fdinst0
1802
fdpredicteddirection0
1803
fdpredictedtarget0 deppc0 desrc10
1804
desrc20 a1 a2 dedest0 deop0 deimm0
1805
deuseimm0 deregwrite0 dememwrite0
1806
dememtoreg0 deisbranch0 dewrt0
1807
depredicteddirection0
1808
depredictedtarget0 emppc0
1809
emis_taken_branch0 emtargetpc0
1810
emarg20 emresult0 emdest0 emwrt0
1811
emmispredictedtaken0
1812
emmispredictednottaken0 emregwrite0
1813
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1814
mmval0 mmdest0 mmwrt0 mmregwrite0
1815
mwppc0 mwval0 mwdest0 mwwrt0
1816
mwregwrite0 (g 'ppc (g 'impl st32))
1817
(g 'prf (g 'impl st32))
1818
(g 'pdmem (g 'impl st32))))
1819
(st34 (simulate_a st33 nil nil nil nil pc0
1820
bpstate0 ffpredicteddirection0
1821
ffpredictedtarget0 ffwrt0 ffinst0
1822
ffppc0 fdppc0 fdwrt0 fdinst0
1823
fdpredicteddirection0
1824
fdpredictedtarget0 deppc0 desrc10
1825
desrc20 a1 a2 dedest0 deop0 deimm0
1826
deuseimm0 deregwrite0 dememwrite0
1827
dememtoreg0 deisbranch0 dewrt0
1828
depredicteddirection0
1829
depredictedtarget0 emppc0
1830
emis_taken_branch0 emtargetpc0
1831
emarg20 emresult0 emdest0 emwrt0
1832
emmispredictedtaken0
1833
emmispredictednottaken0 emregwrite0
1834
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1835
mmval0 mmdest0 mmwrt0 mmregwrite0
1836
mwppc0 mwval0 mwdest0 mwwrt0
1837
mwregwrite0 (g 'ppc (g 'impl st33))
1838
(g 'prf (g 'impl st33))
1839
(g 'pdmem (g 'impl st33))))
1840
(st35 (simulate_a st34 nil nil nil nil pc0
1841
bpstate0 ffpredicteddirection0
1842
ffpredictedtarget0 ffwrt0 ffinst0
1843
ffppc0 fdppc0 fdwrt0 fdinst0
1844
fdpredicteddirection0
1845
fdpredictedtarget0 deppc0 desrc10
1846
desrc20 a1 a2 dedest0 deop0 deimm0
1847
deuseimm0 deregwrite0 dememwrite0
1848
dememtoreg0 deisbranch0 dewrt0
1849
depredicteddirection0
1850
depredictedtarget0 emppc0
1851
emis_taken_branch0 emtargetpc0
1852
emarg20 emresult0 emdest0 emwrt0
1853
emmispredictedtaken0
1854
emmispredictednottaken0 emregwrite0
1855
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1856
mmval0 mmdest0 mmwrt0 mmregwrite0
1857
mwppc0 mwval0 mwdest0 mwwrt0
1858
mwregwrite0 (g 'ppc (g 'impl st34))
1859
(g 'prf (g 'impl st34))
1860
(g 'pdmem (g 'impl st34))))
1861
(st36 (simulate_a st35 nil nil nil nil pc0
1862
bpstate0 ffpredicteddirection0
1863
ffpredictedtarget0 ffwrt0 ffinst0
1864
ffppc0 fdppc0 fdwrt0 fdinst0
1865
fdpredicteddirection0
1866
fdpredictedtarget0 deppc0 desrc10
1867
desrc20 a1 a2 dedest0 deop0 deimm0
1868
deuseimm0 deregwrite0 dememwrite0
1869
dememtoreg0 deisbranch0 dewrt0
1870
depredicteddirection0
1871
depredictedtarget0 emppc0
1872
emis_taken_branch0 emtargetpc0
1873
emarg20 emresult0 emdest0 emwrt0
1874
emmispredictedtaken0
1875
emmispredictednottaken0 emregwrite0
1876
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1877
mmval0 mmdest0 mmwrt0 mmregwrite0
1878
mwppc0 mwval0 mwdest0 mwwrt0
1879
mwregwrite0 (g 'ppc (g 'impl st35))
1880
(g 'prf (g 'impl st35))
1881
(g 'pdmem (g 'impl st35))))
1882
(st37 (simulate_a st36 nil nil nil nil pc0
1883
bpstate0 ffpredicteddirection0
1884
ffpredictedtarget0 ffwrt0 ffinst0
1885
ffppc0 fdppc0 fdwrt0 fdinst0
1886
fdpredicteddirection0
1887
fdpredictedtarget0 deppc0 desrc10
1888
desrc20 a1 a2 dedest0 deop0 deimm0
1889
deuseimm0 deregwrite0 dememwrite0
1890
dememtoreg0 deisbranch0 dewrt0
1891
depredicteddirection0
1892
depredictedtarget0 emppc0
1893
emis_taken_branch0 emtargetpc0
1894
emarg20 emresult0 emdest0 emwrt0
1895
emmispredictedtaken0
1896
emmispredictednottaken0 emregwrite0
1897
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1898
mmval0 mmdest0 mmwrt0 mmregwrite0
1899
mwppc0 mwval0 mwdest0 mwwrt0
1900
mwregwrite0 (g 'ppc (g 'impl st36))
1901
(g 'prf (g 'impl st36))
1902
(g 'pdmem (g 'impl st36))))
1903
(st38 (simulate_a st37 nil nil nil nil pc0
1904
bpstate0 ffpredicteddirection0
1905
ffpredictedtarget0 ffwrt0 ffinst0
1906
ffppc0 fdppc0 fdwrt0 fdinst0
1907
fdpredicteddirection0
1908
fdpredictedtarget0 deppc0 desrc10
1909
desrc20 a1 a2 dedest0 deop0 deimm0
1910
deuseimm0 deregwrite0 dememwrite0
1911
dememtoreg0 deisbranch0 dewrt0
1912
depredicteddirection0
1913
depredictedtarget0 emppc0
1914
emis_taken_branch0 emtargetpc0
1915
emarg20 emresult0 emdest0 emwrt0
1916
emmispredictedtaken0
1917
emmispredictednottaken0 emregwrite0
1918
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1919
mmval0 mmdest0 mmwrt0 mmregwrite0
1920
mwppc0 mwval0 mwdest0 mwwrt0
1921
mwregwrite0 (g 'ppc (g 'impl st37))
1922
(g 'prf (g 'impl st37))
1923
(g 'pdmem (g 'impl st37))))
1924
(st39 (simulate_a st38 nil nil nil nil pc0
1925
bpstate0 ffpredicteddirection0
1926
ffpredictedtarget0 ffwrt0 ffinst0
1927
ffppc0 fdppc0 fdwrt0 fdinst0
1928
fdpredicteddirection0
1929
fdpredictedtarget0 deppc0 desrc10
1930
desrc20 a1 a2 dedest0 deop0 deimm0
1931
deuseimm0 deregwrite0 dememwrite0
1932
dememtoreg0 deisbranch0 dewrt0
1933
depredicteddirection0
1934
depredictedtarget0 emppc0
1935
emis_taken_branch0 emtargetpc0
1936
emarg20 emresult0 emdest0 emwrt0
1937
emmispredictedtaken0
1938
emmispredictednottaken0 emregwrite0
1939
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1940
mmval0 mmdest0 mmwrt0 mmregwrite0
1941
mwppc0 mwval0 mwdest0 mwwrt0
1942
mwregwrite0 (g 'ppc (g 'impl st38))
1943
(g 'prf (g 'impl st38))
1944
(g 'pdmem (g 'impl st38))))
1945
(st40 (simulate_a st39 nil nil nil nil pc0
1946
bpstate0 ffpredicteddirection0
1947
ffpredictedtarget0 ffwrt0 ffinst0
1948
ffppc0 fdppc0 fdwrt0 fdinst0
1949
fdpredicteddirection0
1950
fdpredictedtarget0 deppc0 desrc10
1951
desrc20 a1 a2 dedest0 deop0 deimm0
1952
deuseimm0 deregwrite0 dememwrite0
1953
dememtoreg0 deisbranch0 dewrt0
1954
depredicteddirection0
1955
depredictedtarget0 emppc0
1956
emis_taken_branch0 emtargetpc0
1957
emarg20 emresult0 emdest0 emwrt0
1958
emmispredictedtaken0
1959
emmispredictednottaken0 emregwrite0
1960
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1961
mmval0 mmdest0 mmwrt0 mmregwrite0
1962
mwppc0 mwval0 mwdest0 mwwrt0
1963
mwregwrite0 (g 'ppc (g 'impl st39))
1964
(g 'prf (g 'impl st39))
1965
(g 'pdmem (g 'impl st39))))
1966
(t1 (g 'mwwrt (g 'impl st40)))
1967
(st41 (simulate_a st40 nil nil nil nil pc0
1968
bpstate0 ffpredicteddirection0
1969
ffpredictedtarget0 ffwrt0 ffinst0
1970
ffppc0 fdppc0 fdwrt0 fdinst0
1971
fdpredicteddirection0
1972
fdpredictedtarget0 deppc0 desrc10
1973
desrc20 a1 a2 dedest0 deop0 deimm0
1974
deuseimm0 deregwrite0 dememwrite0
1975
dememtoreg0 deisbranch0 dewrt0
1976
depredicteddirection0
1977
depredictedtarget0 emppc0
1978
emis_taken_branch0 emtargetpc0
1979
emarg20 emresult0 emdest0 emwrt0
1980
emmispredictedtaken0
1981
emmispredictednottaken0 emregwrite0
1982
emmemwrite0 emmemtoreg0 dmem0 mmppc0
1983
mmval0 mmdest0 mmwrt0 mmregwrite0
1984
mwppc0 mwval0 mwdest0 mwwrt0
1985
mwregwrite0 (g 'ppc (g 'impl st40))
1986
(g 'prf (g 'impl st40))
1987
(g 'pdmem (g 'impl st40))))
1988
(t2 (g 'mwwrt (g 'impl st41)))
1989
(st42 (simulate_a st41 nil nil nil nil pc0
1990
bpstate0 ffpredicteddirection0
1991
ffpredictedtarget0 ffwrt0 ffinst0
1992
ffppc0 fdppc0 fdwrt0 fdinst0
1993
fdpredicteddirection0
1994
fdpredictedtarget0 deppc0 desrc10
1995
desrc20 a1 a2 dedest0 deop0 deimm0
1996
deuseimm0 deregwrite0 dememwrite0
1997
dememtoreg0 deisbranch0 dewrt0
1998
depredicteddirection0
1999
depredictedtarget0 emppc0
2000
emis_taken_branch0 emtargetpc0
2001
emarg20 emresult0 emdest0 emwrt0
2002
emmispredictedtaken0
2003
emmispredictednottaken0 emregwrite0
2004
emmemwrite0 emmemtoreg0 dmem0 mmppc0
2005
mmval0 mmdest0 mmwrt0 mmregwrite0
2006
mwppc0 mwval0 mwdest0 mwwrt0
2007
mwregwrite0 (g 'ppc (g 'impl st41))
2008
(g 'prf (g 'impl st41))
2009
(g 'pdmem (g 'impl st41))))
2010
(t3 (g 'mwwrt (g 'impl st42)))
2011
(st43 (simulate_a st42 nil nil nil nil pc0
2012
bpstate0 ffpredicteddirection0
2013
ffpredictedtarget0 ffwrt0 ffinst0
2014
ffppc0 fdppc0 fdwrt0 fdinst0
2015
fdpredicteddirection0
2016
fdpredictedtarget0 deppc0 desrc10
2017
desrc20 a1 a2 dedest0 deop0 deimm0
2018
deuseimm0 deregwrite0 dememwrite0
2019
dememtoreg0 deisbranch0 dewrt0
2020
depredicteddirection0
2021
depredictedtarget0 emppc0
2022
emis_taken_branch0 emtargetpc0
2023
emarg20 emresult0 emdest0 emwrt0
2024
emmispredictedtaken0
2025
emmispredictednottaken0 emregwrite0
2026
emmemwrite0 emmemtoreg0 dmem0 mmppc0
2027
mmval0 mmdest0 mmwrt0 mmregwrite0
2028
mwppc0 mwval0 mwdest0 mwwrt0
2029
mwregwrite0 (g 'ppc (g 'impl st42))
2030
(g 'prf (g 'impl st42))
2031
(g 'pdmem (g 'impl st42))))
2032
(t4 (g 'mwwrt (g 'impl st43)))
2033
(st44 (simulate_a st43 nil nil nil nil pc0
2034
bpstate0 ffpredicteddirection0
2035
ffpredictedtarget0 ffwrt0 ffinst0
2036
ffppc0 fdppc0 fdwrt0 fdinst0
2037
fdpredicteddirection0
2038
fdpredictedtarget0 deppc0 desrc10
2039
desrc20 a1 a2 dedest0 deop0 deimm0
2040
deuseimm0 deregwrite0 dememwrite0
2041
dememtoreg0 deisbranch0 dewrt0
2042
depredicteddirection0
2043
depredictedtarget0 emppc0
2044
emis_taken_branch0 emtargetpc0
2045
emarg20 emresult0 emdest0 emwrt0
2046
emmispredictedtaken0
2047
emmispredictednottaken0 emregwrite0
2048
emmemwrite0 emmemtoreg0 dmem0 mmppc0
2049
mmval0 mmdest0 mmwrt0 mmregwrite0
2050
mwppc0 mwval0 mwdest0 mwwrt0
2051
mwregwrite0 (g 'ppc (g 'impl st43))
2052
(g 'prf (g 'impl st43))
2053
(g 'pdmem (g 'impl st43))))
2054
(t5 (g 'mwwrt (g 'impl st44)))
2055
(st45 (simulate_a st44 nil nil nil nil pc0
2056
bpstate0 ffpredicteddirection0
2057
ffpredictedtarget0 ffwrt0 ffinst0
2058
ffppc0 fdppc0 fdwrt0 fdinst0
2059
fdpredicteddirection0
2060
fdpredictedtarget0 deppc0 desrc10
2061
desrc20 a1 a2 dedest0 deop0 deimm0
2062
deuseimm0 deregwrite0 dememwrite0
2063
dememtoreg0 deisbranch0 dewrt0
2064
depredicteddirection0
2065
depredictedtarget0 emppc0
2066
emis_taken_branch0 emtargetpc0
2067
emarg20 emresult0 emdest0 emwrt0
2068
emmispredictedtaken0
2069
emmispredictednottaken0 emregwrite0
2070
emmemwrite0 emmemtoreg0 dmem0 mmppc0
2071
mmval0 mmdest0 mmwrt0 mmregwrite0
2072
mwppc0 mwval0 mwdest0 mwwrt0
2073
mwregwrite0 (g 'ppc (g 'impl st44))
2074
(g 'prf (g 'impl st44))
2075
(g 'pdmem (g 'impl st44))))
2076
(t6 (g 'mwwrt (g 'impl st45)))
2078
((and (equal counter zero) t1)
2081
(or (equal counter zero)
2082
(equal counter (add-1 zero)))
2084
(add-1 (add-1 counter)))
2085
(t3 (add-1 (add-1 (add-1 counter))))
2087
(add-1 (add-1 (add-1 counter)))))
2090
(add-1 (add-1 (add-1 counter))))))
2095
(add-1 (add-1 counter)))))))
2101
(add-1 (add-1 counter)))))))))))
2102
(or (and (and (equal s_pc1 i_pc)
2103
(equal (read-srf_a a1 s_rf1)
2104
(read-prf_a a1 i_rf)))
2105
(equal s_dmem1 i_dmem))
2106
(and (and (equal s_pc0 i_pc)
2107
(equal (read-srf_a a1 s_rf0)
2108
(read-prf_a a1 i_rf)))
2109
(equal s_dmem0 i_dmem)))))
added
removed
books/workshops/2004/manolios-srinivasan/support/Benchmark-Problems/fxs-bp-safety.lisp
