pipe_rec[addr, data, opcodes: NONEMPTY_TYPE]: THEORY

BEGIN
 
  IMPORTING time, signal

     t: VAR time   

     somedata: data
     somefile: [addr -> data]
     someaddr : addr
     somebool : bool
     someopcode : opcodes

   % Input wires: decoded instruction fields

     opcode: signal[opcodes]
     src1, src2: signal[addr]
     dstn: signal[addr]

   % Controller-generated pipeline abort signal to handle control hazards
     stall: signal[bool]

   % ALU 
     aluop: [opcodes, data, data -> data]

   % The state
       state : TYPE+ = 
           [# dstnd : addr,
              dstndd : addr,
              stalld : bool,
              stalldd : bool,
              wbreg : data,
              regfile : [addr->data],
              opreg1 : data,            
              opreg2 : data,
              opcoded : opcodes 
            #]

     beh(t) : RECURSIVE state = 
              IF t=0 THEN
              (#
               dstnd := someaddr,
               dstndd := someaddr,
               stalld := somebool,
               stalldd := somebool,
               wbreg := somedata,
               regfile := somefile,
               opreg1 := somedata,
               opreg2 :=somedata,
               opcoded := someopcode
              #)    
              ELSE
               LET dstnd  = dstn(t-1) IN
               LET dstndd = beh(t-1)`dstnd IN
               LET stalld = stall(t-1) IN
               LET stalldd = beh(t-1)`stalld(t-1) IN
               LET aluout =  aluop(beh(t-1)`opcoded, beh(t-1)`opreg1, beh(t-1)`opreg2) IN
               LET wbreg = aluout IN
               LET opcoded = opcode(t-1) IN
               LET opreg1  =     
                             IF src1(t-1) = beh(t-1)`dstnd & NOT beh(t-1)`stalld
                                THEN aluout
                             ELSIF src1(t-1) = beh(t-1)`dstndd & NOT beh(t-1)`stalldd
                                THEN beh(t-1)`wbreg
                             ELSE beh(t-1)`regfile(src1(t-1)) ENDIF IN
               LET opreg2 : data =     
                             IF src2(t-1) = beh(t-1)`dstnd & NOT beh(t-1)`stalld
                                THEN aluout
                             ELSIF src2(t-1) = beh(t-1)`dstndd & NOT beh(t-1)`stalldd
                                THEN beh(t-1)`wbreg
                             ELSE beh(t-1)`regfile(src2(t-1)) ENDIF IN
               LET regfile = IF beh(t-1)`stalldd THEN beh(t-1)`regfile
                            ELSE beh(t-1)`regfile WITH [(beh(t-1)`dstndd) := beh(t-1)`wbreg]
                            ENDIF IN
	(# 
               dstnd := dstnd,
               dstndd :=dstndd,
               stalld := stalld,
               stalldd := stalldd,
               wbreg := wbreg,
               regfile:=regfile,
               opreg1 := opreg1,
               opreg2 := opreg2,
               opcoded := opcoded
            #)
       ENDIF    
       MEASURE t

    correctness: THEOREM
     FORALL t: 
        NOT(stall(t)) 
         IMPLIES
            beh(t+3)`regfile(dstn(t)) =
            aluop(opcode(t), beh(t+2)`regfile(src1(t)), beh(t+2)`regfile(src2(t)))

% The following proves the theorem
%
% (auto-rewrite-theories "pipe_rec")
% (grind)

% (REPEAT (LIFT-IF :UPDATES? NIL))
% (ASSERT))

END pipe_rec