← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2000/manolios/pipeline/trivial/sawada-model/model.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2000/manolios/pipeline/trivial/sawada-model/model.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(include-book "basic-def")
 
4
 
 
5
(deflabel begin-model)
 
6
 
 
7
; Basic Pipeline Design
 
8
; Our example machine is very simple.  It consists of a program counter, 
 
9
; a register file, the memory, pipeline latches latch1 and latch2.
 
10
; The programmer visible components are the program counter, the register
 
11
; file and the memory.  It can execute two types of instructions, ADD
 
12
; and SUB.  The format of an instruction is as shown here:
 
13
;           --------------------------------
 
14
;          | op    |  RC   |  RA   |   RB  |
 
15
;           --------------------------------
 
16
;           15    12 11    8 7     4 3     0 
 
17
;
 
18
; where RC, RA and RB are operand register specifiers.  There are only
 
19
; two valid opcodes 0 (ADD) and 1 (SUB).  An instruction without a
 
20
; valid opcode is considered as a NOP.  The ADD instruction reads
 
21
; registers specified by RA and RB, adds the values and writes the
 
22
; result back into the register specified by RC.  The SUB subtracts RB
 
23
; from RA.  Every machine cycle the program counter is incremented by
 
24
; 1.  No exceptions and no interrupts occur.  There is one external
 
25
; input to the machine.  If this input signal is on, the machine may
 
26
; fetch a new instruction from the memory.  Pipeline flushing can be
 
27
; done by running the machine with 0's as its inputs. 
 
28
; 
 
29
; We define this machine at two levels: instruction-set architecture
 
30
; and micro-architecture.
 
31
 
 
32
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
 
33
; ISA Definition
 
34
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
35
; Description of ISA
 
36
; The ISA state consists of only programmer visible states, that is,
 
37
; the program counter, register file and the memory. 
 
38
; ISA behavior is specified by ISA-step.  Depending on the operand, 
 
39
; it executes ADD or SUB operation.
 
40
 
 
41
; Definition of the ISA state.
 
42
; 
 
43
; Note: For the detail of the definition with defstructure, please
 
44
; refer to the public ACL2 book data-structures/structures.lisp.
 
45
; Briefly speaking, an expression (ISA-state PC REGS MEM) returns
 
46
; an ISA state whose program counter, register file and memory are PC,
 
47
; REGS and MEM, respectively.  The pc value of an ISA state, ISA, can
 
48
; be obtained by (ISA-pc ISA). 
 
49
(defstructure ISA-state
 
50
  (pc   (:assert (addr-p pc)   :rewrite))
 
51
  (regs (:assert (regs-p regs) :rewrite))
 
52
  (mem  (:assert (mem-p mem)   :rewrite))
 
53
  (:options :guards  (:conc-name ISA-)))
 
54
 
 
55
(deflabel begin-ISA-def)
 
56
 
 
57
; Definition of the effect of an ADD instruction.
 
58
(defun ISA-add (rc ra rb ISA)
 
59
  (declare (xargs :guard (and (rname-p rc) (rname-p ra) (rname-p rb)
 
60
                              (ISA-state-p ISA))))
 
61
  (ISA-state (addr (1+ (ISA-pc ISA)))
 
62
             (write-reg (word (+ (read-reg ra (ISA-regs ISA))
 
63
                                 (read-reg rb (ISA-regs ISA))))
 
64
                        rc (ISA-regs ISA))
 
65
             (ISA-mem ISA)))
 
66
 
 
67
; Definition of the effect of an SUB instruction.
 
68
(defun ISA-sub (rc ra rb ISA)
 
69
  (declare (xargs :guard (and (rname-p rc) (rname-p ra) (rname-p rb)
 
70
                              (ISA-state-p ISA))))
 
71
  (ISA-state (addr (1+ (ISA-pc ISA)))
 
72
             (write-reg (word (- (read-reg ra (ISA-regs ISA))
 
73
                                 (read-reg rb (ISA-regs ISA))))
 
74
                        rc (ISA-regs ISA))
 
75
             (ISA-mem ISA)))
 
76
                  
 
77
; Definition of NOP. It only increments the program counter. 
 
78
(defun ISA-default (ISA)
 
79
  (declare (xargs :guard (ISA-state-p ISA)))
 
80
  (ISA-state (addr (1+ (ISA-pc ISA)))
 
81
             (ISA-regs ISA)
 
82
             (ISA-mem ISA)))
 
83
 
 
84
; Next ISA state function.  It takes the current ISA state and returns 
 
85
; the ISA state after executing one instruction.  This function is a
 
86
; simple dispatcher of corresponding functions depending on the
 
87
; instruction type.
 
88
(defun ISA-step (ISA)
 
89
  (declare (xargs :guard (ISA-state-p ISA)))
 
90
  (let ((inst (read-mem (ISA-pc ISA) (ISA-mem ISA))))
 
91
    (let ((op (op-field inst))
 
92
          (rc (rc-field inst))
 
93
          (ra (ra-field inst))
 
94
          (rb (rb-field inst)))
 
95
      (case op
 
96
        (0 (ISA-add rc ra rb ISA)) ; add
 
97
        (1 (ISA-sub rc ra rb ISA)) ; sub
 
98
        (otherwise (ISA-default ISA))))))
 
99
 
 
100
; N step ISA function.  It returns the ISA state after executing n
 
101
; instructions from the initial state, ISA.  
 
102
(defun ISA-stepn (ISA n)
 
103
  (declare (xargs :guard (and (ISA-state-p ISA) (integerp n) (<= 0 n))))
 
104
  (if (zp n) ISA (ISA-stepn (ISA-step ISA) (1- n))))
 
105
 
 
106
(deflabel end-ISA-def)
 
107
 
 
108
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
 
109
; MA Definition
 
110
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
111
; Definition of MA states
 
112
;
 
113
; Definition of pipeline latch latch1. 
 
114
(defstructure latch1
 
115
  (valid? (:assert (bitp valid?) :rewrite))
 
116
  (op     (:assert (opcd-p op)   :rewrite))
 
117
  (rc     (:assert (rname-p rc)  :rewrite))
 
118
  (ra     (:assert (rname-p ra)  :rewrite))
 
119
  (rb     (:assert (rname-p rb)  :rewrite))
 
120
  (:options :guards))
 
121
 
 
122
; Definition of pipeline latch latch2.
 
123
(defstructure latch2
 
124
  (valid?  (:assert (bitp valid?)   :rewrite))
 
125
  (op      (:assert (opcd-p op)     :rewrite))
 
126
  (rc      (:assert (rname-p rc)    :rewrite))
 
127
  (ra-val  (:assert (word-p ra-val) :rewrite))
 
128
  (rb-val  (:assert (word-p rb-val) :rewrite))
 
129
  (:options :guards))
 
130
 
 
131
; Definition of pipelined micro-architecture. 
 
132
(defstructure MA-state
 
133
  (pc     (:assert (addr-p pc)       :rewrite (:rewrite (acl2-numberp pc))))
 
134
  (regs   (:assert (regs-p regs)     :rewrite))
 
135
  (mem    (:assert (mem-p mem)       :rewrite))
 
136
  (latch1 (:assert (latch1-p latch1) :rewrite))
 
137
  (latch2 (:assert (latch2-p latch2) :rewrite))
 
138
  (:options :guards  (:conc-name MA-)))
 
139
 
 
140
; Defines the signal supplied to the micro-architectural behavioral
 
141
; function.  We assume that the micro-architecture takes one bit
 
142
; input, which turn on and off instruction fetching.
 
143
(defun MA-sig-p (sig)
 
144
  (declare (xargs :guard t))
 
145
  (bitp sig))
 
146
 
 
147
; List of sig
 
148
(deflist MA-sig-listp (l)
 
149
  (declare (xargs :guard t))
 
150
  MA-sig-p)
 
151
 
 
152
(deflabel begin-MA-def)
 
153
; The definition of ALU.  The ALU takes opcode and two operands, 
 
154
; and outputs the result. 
 
155
(defun ALU-output (op val1 val2)
 
156
  (declare (xargs :guard (and (opcd-p op) (word-p val1) (word-p val2))))
 
157
  (cond ((equal op 0) (word (+ val1 val2)))
 
158
        ((equal op 1) (word (- val1 val2)))
 
159
        (t 0)))
 
160
 
 
161
; The behavior of the register file.  If the latch2 contains an ADD or
 
162
; SUB instruction, the register specified by latch2-rc is updated by
 
163
; the output from the ALU.  Otherwise, the register file is unchanged.
 
164
(defun step-regs (MA)
 
165
  (declare (xargs :guard (MA-state-p MA)))
 
166
  (let ((latch2 (MA-latch2 MA)))
 
167
    (b-if (b-and (latch2-valid? latch2)
 
168
                 (b-ior (bv-eqv *opcode-size* (latch2-op latch2) 0)
 
169
                        (bv-eqv *opcode-size* (latch2-op latch2) 1)))
 
170
          (write-reg (ALU-output (latch2-op latch2)
 
171
                                 (latch2-ra-val latch2)
 
172
                                 (latch2-rb-val latch2))
 
173
                     (latch2-rc latch2)
 
174
                     (MA-regs MA))
 
175
          (MA-regs MA))))
 
176
 
 
177
; The dependency check.  If there is a true (RAW) dependency
 
178
; between the instructions at latch1 and latch2, the instruction at
 
179
; latch1 should stall until the instruction at latch2 completes.  We
 
180
; check whether the destination register of the instruction at latch2
 
181
; is one of the source registers of the instruction at latch1. 
 
182
(defun dependency? (MA)
 
183
  (declare (xargs :guard (MA-state-p MA)))
 
184
  (let ((latch1 (MA-latch1 MA))
 
185
        (latch2 (MA-latch2 MA)))
 
186
    (b-ior (bv-eqv *rname-size* (latch1-ra latch1) (latch2-rc latch2))
 
187
           (bv-eqv *rname-size* (latch1-rb latch1) (latch2-rc latch2)))))
 
188
 
 
189
(defthm bitp-dependency
 
190
    (bitp (dependency? MA)))
 
191
 
 
192
; The stall condition.  If both latch1 and latch2 contain valid
 
193
; instructions, and there are dependencies between the two
 
194
; instructions, the instruction at latch1 is stalled.  
 
195
(defun stall-cond? (MA)
 
196
  (declare (xargs :guard (MA-state-p MA)))
 
197
  (b-and (latch1-valid? (MA-latch1 MA))
 
198
         (b-and (latch2-valid? (MA-latch2 MA))
 
199
                (dependency? MA))))
 
200
 
 
201
(defthm bitp-stall-cond
 
202
    (bitp (stall-cond? MA)))
 
203
 
 
204
; Next state function for pipeline latch latch2.  The instruction at
 
205
; latch1 advances to latch2, only if stall-cond? is off.  Note that
 
206
; the rest of the fields of latch2 are updated anyway. Is it okay?
 
207
; The answer is yes.  The instruction at latch2 always complete, and
 
208
; the instruction at latch1 may or may not advance to latch2.  If
 
209
; instruction at latch1 stalls, latch2 will hold a bubble in the next
 
210
; cycle.  In this case, we don't care the values the fields of latch2
 
211
; except for latch2-valid?, which indicates whether the content of
 
212
; latch2 is a bubble or not.
 
213
(defun step-latch2 (MA)
 
214
  (declare (xargs :guard (MA-state-p MA)))
 
215
  (let ((latch1 (MA-latch1 MA))
 
216
        (latch2 (MA-latch2 MA)))
 
217
    (latch2 (b-and (latch1-valid? latch1)
 
218
                   (b-nand (dependency? MA) (latch2-valid? latch2)))
 
219
            (latch1-op latch1)
 
220
            (latch1-rc latch1)
 
221
            (read-reg (latch1-ra latch1) (MA-regs MA))
 
222
            (read-reg (latch1-rb latch1) (MA-regs MA)))))
 
223
 
 
224
 
 
225
; This function defines how latch1 is updated. If the stall condition
 
226
; is true, latch1 is not updated.  If latch1 is currently empty or the
 
227
; stall condition is false, and if the given sig is true, we fetch an
 
228
; instruction.  Sig is an external input that directs the processor to
 
229
; fetch a new instruction.
 
230
(defun step-latch1 (MA sig)
 
231
  (declare (xargs :guard (and (MA-state-p MA) (MA-sig-p sig))))
 
232
  (let ((latch1 (MA-latch1 MA))
 
233
        (inst (read-mem (MA-pc MA) (MA-mem MA))))
 
234
    (latch1 (b-ior sig (stall-cond? MA))
 
235
            (b-if (stall-cond? MA) (latch1-op latch1) (op-field inst))
 
236
            (b-if (stall-cond? MA) (latch1-rc latch1) (rc-field inst))
 
237
            (b-if (stall-cond? MA) (latch1-ra latch1) (ra-field inst))
 
238
            (b-if (stall-cond? MA) (latch1-rb latch1) (rb-field inst)))))
 
239
 
 
240
 
 
241
; The condition whether a new instruction is fetched. 
 
242
(defun fetch-inst? (MA sig)
 
243
  (declare (xargs :guard (and (MA-state-p MA) (MA-sig-p sig))))
 
244
  (b-and sig
 
245
         (b-nand (latch1-valid? (MA-latch1 MA))
 
246
                 (b-and (latch2-valid? (MA-latch2 MA))
 
247
                        (dependency? MA)))))
 
248
 
 
249
(defthm bitp-fetch-inst?
 
250
    (bitp (fetch-inst? MA sig)))
 
251
 
 
252
; Function step-pc defines how the program counter is updated. 
 
253
(defun step-pc (MA sig)
 
254
  (declare (xargs :guard (and (MA-state-p MA) (MA-sig-p sig))))
 
255
  (b-if (fetch-inst? MA sig)
 
256
        (addr (1+ (MA-pc MA)))
 
257
        (MA-pc MA)))
 
258
                        
 
259
; MA-step defines how the MA state is updated every clock cycle.  The
 
260
; memory does not change in our model.  The behavior of other
 
261
; components is specified by the corresponding step functions.
 
262
(defun MA-step (MA sig)
 
263
  (declare (xargs :guard (and (MA-state-p MA) (MA-sig-p sig))))
 
264
  (MA-state (step-pc MA sig)
 
265
            (step-regs MA)
 
266
            (MA-mem MA)
 
267
            (step-latch1 MA sig)
 
268
            (step-latch2 MA)))      
 
269
 
 
270
; MA-stepn returns the MA state after n clock cycles of MA execution.
 
271
; The argument MA is the initial state, and sig-list specifies the
 
272
; series of inputs.
 
273
(defun MA-stepn (MA sig-list n)
 
274
  (declare (xargs :guard (and (MA-state-p MA) (MA-sig-listp sig-list)
 
275
                              (integerp n) (<= 0 n)
 
276
                              (<= n (len sig-list)))))
 
277
  (if (zp n)
 
278
      MA
 
279
      (MA-stepn (MA-step MA (car sig-list)) (cdr sig-list) (1- n))))
 
280
 
 
281
(deflabel end-MA-def)
 
282
 
 
283
(deftheory ISA-def
 
284
    (set-difference-theories
 
285
     (set-difference-theories (function-theory 'end-ISA-def)
 
286
                              (function-theory 'begin-ISA-def))
 
287
     '(ISA-stepn)))
 
288
 
 
289
(deftheory MA-def
 
290
    (set-difference-theories
 
291
     (set-difference-theories (function-theory 'end-MA-def)
 
292
                              (function-theory 'begin-MA-def))
 
293
     '(MA-stepn)))
 
294
 
 
295
(in-theory (disable ISA-def MA-def MA-sig-p))
 
296
 
 
297
;;;;;;;; Type proofs ;;;;;;;;
 
298
(defthm ISA-state-p-ISA-step
 
299
    (implies (ISA-state-p ISA) (ISA-state-p (ISA-step ISA)))
 
300
  :hints (("Goal" :in-theory (enable ISA-step ISA-add ISA-sub ISA-default))))
 
301
 
 
302
(defthm ISA-state-p-ISA-stepn
 
303
    (implies (ISA-state-p ISA) (ISA-state-p (ISA-stepn ISA n))))
 
304
 
 
305
(defthm addr-p-step-pc
 
306
    (implies (MA-state-p MA) (addr-p (step-pc MA sig)))
 
307
  :hints (("Goal" :in-theory (enable step-pc))))
 
308
 
 
309
(defthm word-p-ALU-output
 
310
    (implies (and (opcd-p op) (word-p val1) (word-p val2))
 
311
             (word-p (ALU-output op val1 val2)))
 
312
  :hints (("Goal" :in-theory (enable ALU-output))))
 
313
 
 
314
(defthm regs-p-step-regs
 
315
    (implies (MA-state-p MA) (regs-p (step-regs MA)))
 
316
  :hints (("Goal" :in-theory (enable step-regs))))
 
317
 
 
318
(defthm latch1-p-step-latch1
 
319
    (implies (and (MA-state-p MA) (MA-sig-p sig))
 
320
             (latch1-p (step-latch1 MA sig)))
 
321
  :hints (("Goal" :in-theory (enable step-latch1 MA-sig-p))))
 
322
 
 
323
(defthm latch1-p-step-latch2
 
324
    (implies (and (MA-state-p MA) (MA-sig-p sig))
 
325
             (latch2-p (step-latch2 MA)))
 
326
  :hints (("Goal" :in-theory (enable step-latch2 MA-sig-p))))
 
327
 
 
328
(defthm MA-state-p-MA-step
 
329
    (implies (and (MA-state-p MA) (MA-sig-p sig))
 
330
             (MA-state-p (MA-step MA sig)))
 
331
  :hints (("Goal" :in-theory (enable MA-step))))
 
332
 
 
333
(defthm MA-state-p-MA-stepn
 
334
    (implies (and (MA-state-p MA) (MA-sig-listp sig-list)
 
335
                  (<= n (len sig-list)))
 
336
             (MA-state-p (MA-stepn MA sig-list n))))
 
337
 
 
338
;;;  Predicates for correctness
 
339
 
 
340
; The projection function from an MA state to the corresponding ISA
 
341
; state. Function proj strips off pipeline latches from the MA state.
 
342
(defun proj (MA)
 
343
  (declare (xargs :guard (MA-state-p MA)))
 
344
  (ISA-state (MA-pc MA) (MA-regs MA) (MA-mem MA)))
 
345
 
 
346
; (flushed? MA) is true if the pipeline of MA is flushed.
 
347
(defun flushed? (MA)
 
348
  (b-nor (latch1-valid? (MA-latch1 MA))
 
349
         (latch2-valid? (MA-latch2 MA))))
 
350
 
 
351
 
 
352
#|
 
353
We will prove a following lemma for operational correctness:
 
354
(defthm correctness
 
355
    (implies (and (MA-state-p MA)
 
356
                  (MA-sig-listp sig-list)
 
357
                  (<= n (len sig-list))
 
358
                  (b1p (flushed? MA))
 
359
                  (b1p (flushed? (MA-stepn MA sig-list n))))
 
360
             (equal (proj (MA-stepn MA sig-list n))
 
361
                    (ISA-stepn (proj MA)
 
362
                               (num-insts MA sig-list n)))))
 
363
 
 
364
where num-insts calculates the nunber of instructions executed in the
 
365
n cycles of MA execution.  We also prove the liveness property with:
 
366
 
 
367
(defthm liveness
 
368
    (implies (MA-state-p MA)
 
369
             (b1p (flushed? (MA-stepn MA
 
370
                                      (zeros (flush-cycles MA))
 
371
                                      (flush-cycles MA)))))).
 
372
 
 
373
Function flush-cycles calculates the number of cycles to flush the pipeline. 
 
374
|#