tom_impl_spec[(IMPORTING fpu_impl_ui_types,cache_mem_impl_types)
	    TOMadd : add_circuit_t,
	    TOMmd  : md_circuit_t,
	    TOMfpm : fpm_circuit_t,
	    mif_next:mif_next_t,
	    fpu_spec_op : fpu_spec_op_t]: THEORY
BEGIN

%% tom_impl_spec is an "abstract" VAMP implementation,
%% i.e., all execution units are replaced by their specification
%% and all basic circuits also
%% This is ONLY for complexity reasons, i.e., importing tom_impl_spec
%% in PVS takes about 15% of the time it would take to import the
%% actual implementation AND the correctness proofs of all the parts.

  dlxif : LIBRARY = "../dlxif";
  dlxalu: LIBRARY = "../dlxalu";

%% NOTE: The VAMP configuration, decode, and producers are shared
%% between the abstract implememtation and the actual implementation
%% since they do not contain basic circuits anyway.

  IMPORTING fpu_impl_ui[TOMadd,TOMmd,TOMfpm,fpu_spec_op], %% fpu spec
	    cache_mem_impl_ui[mif_next],                  %% memory unit spec
	    dlxif@dlxifspec[fpu_spec],                    %% programmer's model
	    tom_conft, 					  %% VAMP configuration
	    tomdecode, 					  %% VAMP decode
	    dlxalu@dlxalu_spec, 			  %% alu spec
	    producer;					  %% VAMP producers

%% the different parts of the "abstract" VAMP next state function
%% the names are formed from the actual implementation names plus "_spec"

    tomalu_step_spec(alu: alu_reg, clear, stall_in: bool, inputs: fu_rs_regt):
      [#
        reg: alu_reg,
        out: cdbt
      #]=
      (#
        reg:=(# dummy:=FALSE #),
        out:=
          LET op1=inputs`op(0),
              op2=IF I_ALUi(inputs`f) OR I_shifti(inputs`f) THEN
                    I_immediate(inputs`f)
                  ELSE
                    inputs`op(2)
                  ENDIF,
              ALU_out=ALUf_spec(op1, op2, ALUfunction(inputs`f)) IN
          (#
            tag:=inputs`tag,       % just pass through
            valid:=inputs`valid,   % just pass through
            data:=LAMBDA (x: below(2)): ALU_out`result, % easy embedding
            CA:=LAMBDA (i: below(32)):
              IF i=6 THEN
                ALU_out`ovf        % ovf exception
              ELSE
                FALSE
              ENDIF,
            EData:=r0              % no exception data
          #)
      #);

    SPR_next_spec(SPR:[upto(nspr_LAST)->registert], reset, writeback, JISR, repeat:bool,
             wbROBe: robet, MCA: registert):
      [upto(nspr_LAST)->registert]=
      LET SPRu= LAMBDA (r: upto(nspr_LAST)):
		  IF writeback THEN
		    IF wbROBe`dest`spr AND bv2nat(wbROBe`dest`A)=r THEN
          	      wbROBe`data(0)
		    ELSE IF r=nspr_IEEEf THEN	% accumulate causes according to IEEE-standard
          	      	SPR(r)^(31,5) o (SPR(r)^(4,0) OR wbROBe`CA^(11,7))
		      ELSE
	  	      	SPR(r)
		      ENDIF
		    ENDIF
      		  ELSE
        	    SPR(r)
      		  ENDIF IN
      IF reset THEN % initialization
        LAMBDA (r: upto(nspr_LAST)): IF r=nspr_ECA THEN r1 ELSE r0 ENDIF
      ELSIF JISR THEN % interrupt
        LAMBDA (r: upto(nspr_LAST)):
        COND
          r=nspr_SR   ->r0,
          r=nspr_ESR  ->IF repeat THEN
                          SPR(nspr_SR)
                        ELSE
                          SPRu(nspr_SR)
                        ENDIF,
          r=nspr_ECA  ->MCA,
          r=nspr_EPC  ->IF repeat THEN
                          wbROBe`oPCp
                        ELSE
                          wbROBe`nextPCp
                        ENDIF,
          r=nspr_EDPC ->IF repeat THEN
                          wbROBe`oDPC
                        ELSE
                          wbROBe`nextDPC
                        ENDIF,
          r=nspr_EData->wbROBe`EData,
          ELSE -> SPRu(r)
        ENDCOND
      ELSE
        SPRu
      ENDIF;

  signals4_spec(S4: S4conft, SR : registert, reset: bool):signals4t=
    LET wbROBe   = S4`rob(bv2nat(S4`ROBhead)),
	ROBempty = bv2nat(S4`ROBcount)=0,
	ROBfull  = bv2nat(S4`ROBcount)=rob_entries,
	retire   = wbROBe`valid AND NOT ROBempty AND NOT reset,
	MCA      = LAMBDA (i:below(32)):
        	     IF i>=6 AND i/=12 THEN 
          	       	wbROBe`CA(i) AND SR(i)
		     ELSE 
          		wbROBe`CA(i)
        	     ENDIF,
	JISR     = retire AND EXISTS (i:below(32)):MCA(i),
	repeat   = MCA(0) OR MCA(1) OR MCA(2) OR MCA(3) OR MCA(4),
	rollback = JISR IN
    (#
      wbROBe   :=wbROBe,
      ROBempty :=ROBempty,
      ROBfull  :=ROBfull,
      retire   :=retire,
      MCA      :=MCA,
      JISR     :=JISR,
      repeat   :=repeat,
      writeback:=retire AND NOT (JISR AND repeat),
      rollback :=rollback,
      clear    :=(reset OR rollback)
     #);

  rob_step_spec(complete_rob: robt, issue, issue_with_result: bool,
           CDB: cdbt, ID: IDt,
           IA: IAt, issue_CA, issue_EData: registert,
           nextPCp, nextDPC: registert,
           oPCp, oDPC : registert,
           ROBtail : tagt,
           issue_opA: registert):robt=
    LAMBDA (r: below(rob_entries)):
    LET rob=complete_rob(r),
	issue_A=bv2nat(ROBtail)=r AND issue,
	compl_A=bv2nat(CDB`tag)=r AND CDB`valid IN
    (#
      valid:=IF issue_A THEN
               issue_with_result
             ELSIF compl_A THEN
               TRUE
             ELSE
               rob`valid
             ENDIF,

      data :=IF issue_A AND issue_with_result THEN
               LAMBDA (x: below(2)):
               IF x=0 THEN 
                 IF (ID`jump OR ID`jr) AND ID`link THEN
                   oPCp+r4
                 ELSE
                   issue_opA
                 ENDIF
               ELSE 
                 r0 
               ENDIF
             ELSIF compl_A THEN
                 CDB`data
             ELSE
               rob`data
             ENDIF,

      CA   :=IF issue_A AND issue_with_result THEN
               issue_CA
             ELSIF compl_A THEN
               CDB`CA
             ELSE
               rob`CA
             ENDIF,

      EData:=IF issue_A AND issue_with_result THEN
               issue_EData
             ELSIF compl_A THEN
               CDB`EData
             ELSE
               rob`EData
             ENDIF,

      dest :=IF issue_A THEN
               IA`dest
             ELSE
               rob`dest
             ENDIF,

      oPCp :=IF issue_A THEN
               oPCp
             ELSE
               rob`oPCp
             ENDIF,

      oDPC :=IF issue_A THEN
               oDPC
             ELSE
               rob`oDPC
             ENDIF,

      nextPCp:=IF issue_A THEN
                 nextPCp
               ELSE
                 rob`nextPCp
               ENDIF,

      nextDPC:=IF issue_A THEN
                 nextDPC
               ELSE
                 rob`nextDPC
               ENDIF
    #);

  prod_step5_spec(prod: prod_reg[5],
    	  clear: bool,
    	  A_issue, A_wb: bvec[5],
    	  we_issue, we_wb: bool,
    	  tag_issue, tag_wb: tagt):prod_reg[5]=
    LAMBDA (i: below(exp2(5))):
      IF clear THEN
        (#
          valid:=TRUE,
          tag:=tag0
        #)
      ELSE
	IF bv2nat[5](A_issue)=i AND we_issue THEN
          (#
            valid:=FALSE,
            tag:=tag_issue
          #)
        ELSIF bv2nat(A_wb)=i AND we_wb AND
	      tag_wb=prod(bv2nat(A_wb))`tag THEN
          prod(i) WITH [valid:=TRUE]
        ELSE
          prod(i)
        ENDIF
      ENDIF;

  prod_step4_spec(prod: prod_reg[4],
    	  clear: bool,
    	  A_issue, A_wb: bvec[4],
    	  we_issue, we_wb: bool,
    	  tag_issue, tag_wb: tagt):prod_reg[4]=
    LAMBDA (i: below(exp2(4))):
      IF clear THEN
        (#
          valid:=TRUE,
          tag:=tag0
        #)
      ELSE
	IF bv2nat[4](A_issue)=i AND we_issue THEN
          (#
            valid:=FALSE,
            tag:=tag_issue
          #)
        ELSIF bv2nat(A_wb)=i AND we_wb AND
	      tag_wb=prod(bv2nat(A_wb))`tag THEN
          prod(i) WITH [valid:=TRUE]
        ELSE
          prod(i)
        ENDIF
      ENDIF;

  tomrf_spec(S5: S5conft, writeback:bool, wbROBe: robet, IA: IAt):tomrft=
      LET A  = IA`sop(0)`A,
	  Af = IA`sop(0)`A^(4,1),
	  Afh= IA`sop(1)`A^(4,1),
	  B  = IA`sop(2)`A,
	  Bf = IA`sop(2)`A^(4,1),
	  Bfh= IA`sop(3)`A^(4,1),
	  C  = wbROBe`dest`A,
          Cf = wbROBe`dest`A^(4,1) IN
      (#
        nextGPR :=IF writeback AND wbROBe`dest`gpr THEN
		    S5`GPR WITH [(C):=wbROBe`data(0)]
		  ELSE
		    S5`GPR
		  ENDIF,
        nextFPRl:=IF writeback AND wbROBe`dest`fprl THEN
		    S5`FPRl WITH [(Cf):=wbROBe`data(0)]
		  ELSE
		    S5`FPRl
		  ENDIF,
        nextFPRh:=IF writeback AND wbROBe`dest`fprh THEN
		    S5`FPRh WITH [(Cf):=wbROBe`data(1)]
		  ELSE
		    S5`FPRh
		  ENDIF,
        rfdata  :=LAMBDA (x: below(6)):
          COND
            x=0->IF IA`sop(x)`gpr THEN
                   S5`GPR(A)
                 ELSIF IA`sop(x)`spr THEN
		   IF bv2nat(A)<=nspr_LAST THEN
        	     S5`SPR(bv2nat(A))
		   ELSE
		     r0
		   ENDIF
                 ELSIF IA`sop(x)`fprl THEN
                   S5`FPRl(Af)
                 ELSE
                   S5`FPRh(Afh)
                 ENDIF,
            x=1->IF IA`sop(x)`fprl THEN
                   S5`FPRl(Af)
                 ELSIF IA`sop(x)`fprh THEN
                   S5`FPRh(Afh)
		 ELSE 
                   S5`GPR(A)
                 ENDIF,
            x=2->IF IA`sop(x)`gpr THEN
                   S5`GPR(B)
                 ELSIF IA`sop(x)`fprl THEN
                   S5`FPRl(Bf)
                 ELSE
                   S5`FPRh(Bfh)
                 ENDIF,
            x=3->IF IA`sop(x)`fprl THEN
                   S5`FPRl(Bf)
                 ELSE
                   S5`FPRh(Bfh)
                 ENDIF,
            x=4->S5`SPR(nspr_RM),
            x=5->S5`SPR(nspr_SR)
          ENDCOND
	#);

  tomsourceops_spec(S5: S5conft, complete_rob: robt, IA: IAt, CDB: cdbt, 
	       rfdata: [below(6)->registert]): tomsourceopst=
    LAMBDA (x: below(6)): 
      LET addr  =IA`sop(x), 
	  rfdata=rfdata(x),
  	  rf = IF addr`gpr THEN
      	    	 IF bv2nat(addr`A)=0 THEN
             	 (# valid:=TRUE,
              	    tag  :=tag0,
           	    data :=r0 #)
      	    	 ELSE
              	   LET prod=S5`GPRp(bv2nat(addr`A)) IN
        	   (# valid:=prod`valid,
           	      tag  :=prod`tag,
           	      data :=rfdata #)
      	       	 ENDIF
    	       ELSIF addr`fprl THEN
      		 LET prod=S5`FPRlp(bv2nat(addr`A^(4,1))) IN
      		 (# valid:=prod`valid,
         	    tag  :=prod`tag,
         	    data :=rfdata #)
    	       ELSIF addr`fprh THEN
      	         LET prod=S5`FPRhp(bv2nat(addr`A^(4,1))) IN
      		 (# valid:=prod`valid,
         	    tag  :=prod`tag,
         	    data :=rfdata #)
    	       ELSIF addr`spr THEN
      		 IF bv2nat(addr`A)<=nspr_LAST THEN
        	   LET prod=S5`SPRp(bv2nat(addr`A)) IN
        	   (# valid:=prod`valid,
           	      tag  :=prod`tag,
           	      data :=rfdata #)
      		 ELSE
        	 (# valid:=TRUE,
           	    tag  :=tag0, % anyvalue
          	    data :=r0 #)        
      		 ENDIF
    	       ELSE % none
      	       (# valid:=TRUE,
         	  tag:=tag0,  % anyvalue
         	  data:=r0 #)
    	       ENDIF,
  	  rob = complete_rob(bv2nat(rf`tag)) IN
    IF rf`valid THEN
      rf
    ELSIF CDB`valid AND CDB`tag=rf`tag THEN
      (# valid:=TRUE,
         tag:=rf`tag, % anyvalue
         data:=IF addr`fprh THEN
		 CDB`data(1)
	       ELSE
		 CDB`data(0)
	       ENDIF #)
    ELSE % ROB + no valid
      (# valid:=rob`valid,
         tag:=rf`tag,
         data:=IF addr`fprh THEN
		 rob`data(1)
	       ELSE
		 rob`data(0)
	       ENDIF #)
    ENDIF;

  signals3_spec(S3: S3conft):signals3t=
    LET compl_p=arbiter_impl_spec[no_fu](S3`CDB_arbiter, 
				   LAMBDA (i: funot[no_reg, no_rs, no_fu]): S3`P(i)`valid),
        CDB=IF empty?(compl_p) THEN
	      (#
	        tag:=tag0,
	        valid:=FALSE,
	        data:=LAMBDA (x: below(2)): r0,
	        CA:=r0,
	        EData:=r0
	      #)
	    ELSE
	      S3`P(the(compl_p))
	    ENDIF,
        FU_stall_in=LAMBDA (i: below(no_fu)):
		      S3`P(i)`valid AND NOT compl_p(i) IN
    (#
      compl_p  :=compl_p,
      CDB      :=CDB,
      FU_stall_in:=FU_stall_in
    #);

  signals2_spec(S3: S3conft, S2:S2conft, reset: bool, 
		s3: signals3t, clear:bit):signals2t=
    LET fu_stall_out=LAMBDA (fu: below(no_fu)):
    		      COND
      			fu=0 -> s3`FU_stall_in(fu),
      			fu=1 -> tomfpu1_stallout_ui(S3`fpu1, s3`FU_stall_in(fu)),
      			fu=2 -> tomfpu2_stallout_ui(S3`fpu2, s3`FU_stall_in(fu)),
      			fu=3 -> tomfpu3_stallout_ui(S3`fpu3, s3`FU_stall_in(fu)),
      			fu=4 -> tommem_stallout (S3`mem,  s3`FU_stall_in(fu))
    		      ENDCOND,
        dispatch_rs = LET RS_valid=LAMBDA (i: below(no_rs)):
                   	S2`RS(i)`valid AND
                        FORALL (x: below(6)): S2`RS(i)`op(x)`valid IN
                      LAMBDA (i: below(no_rs)):
     			COND
			  i<=3 -> arbiter_impl_spec[4](S2`alurs_arbiter, RS_valid^(3, 0))(i)
              		     	  AND NOT fu_stall_out(0),
      			  i=4  -> RS_valid(4) AND NOT fu_stall_out(1),
      			  i=5  -> RS_valid(5) AND NOT fu_stall_out(2),
      			  i=6  -> RS_valid(6) AND NOT fu_stall_out(3),
      			  i=7  -> RS_valid(7) AND NOT fu_stall_out(4)
    			ENDCOND,
        fu_inputs = LAMBDA (fu: funot[no_reg, no_rs, no_fu]):fu_rs_map(
      		      COND
        		fu=0->IF empty?(dispatch_rs^(3,0)) THEN
                		S2`RS(0) WITH [valid:=FALSE]
	      		      ELSE
                		S2`RS(the(dispatch_rs^(3,0)))
              		      ENDIF,
        		fu=1->S2`RS(rs_fpu1) WITH [valid:=dispatch_rs(4)],
        		fu=2->S2`RS(rs_fpu2) WITH [valid:=dispatch_rs(5)],
        		fu=3->S2`RS(rs_fpu3) WITH [valid:=dispatch_rs(6)],
        		fu=4->S2`RS(rs_mem)  WITH [valid:=dispatch_rs(7)]
      		      ENDCOND) IN
    (#
      fu_stall_out:=fu_stall_out,
      dispatch_rs:=dispatch_rs,
      fu_inputs:=fu_inputs,

      alu_step :=tomalu_step_spec(S3`alu,  clear, s3`FU_stall_in(0), fu_inputs(0)),
      fpu1_step:=tomfpu1_step_ui (S3`fpu1, clear, s3`FU_stall_in(1), fu_inputs(1)),
      fpu2_step:=tomfpu2_step_ui (S3`fpu2, clear, s3`FU_stall_in(2), fu_inputs(2)),
      fpu3_step:=tomfpu3_step_ui (S3`fpu3, clear, s3`FU_stall_in(3), fu_inputs(3))
    #);

  signals1_spec(S1: S1conft, S2: S2conft, S4: S4conft, 
		S5: S5conft, reset: bool, 
	   	s3: signals3t, s4: signals4t):signals1t=
    LET ID=tomID(S1`IR),
        IA=tomIA(ID),
	rf=tomrf_spec(S5, s4`writeback, s4`wbROBe, IA),
	sourceops=tomsourceops_spec(S5, S4`rob, IA, s3`CDB, rf`rfdata),
	issue_exception=S1`CAipf OR S1`CAimal,
	issue_CA=LAMBDA (i: below(32)):
    		   COND
      		     i=1  -> ID`illegal,
      		     i=2  -> S1`CAimal,
      		     i=3  -> S1`CAipf,
      		     i=5  -> ID`trap,
      		     ELSE -> FALSE
    		   ENDCOND,
	issue_EData=IF S1`CAimal OR S1`CAipf THEN
		      S2`DPC
		    ELSIF ID`trap THEN
		      ID`immediate
		    ELSE
		      r0
		    ENDIF,
	nextPCp=dlxispec_nextpc(S1`IR, sourceops(0)`data, S2`PCp, S5`SPR(nspr_EPC)),
        nextDPC=IF ID`rfe THEN
                  S5`SPR(nspr_EDPC)
                ELSE
                  S2`PCp
                ENDIF,
	issue_fu=IF issue_exception THEN
      		   LAMBDA (fu: funot[no_reg, no_rs, no_fu]): FALSE
    		 ELSE
      		   LAMBDA (fu: funot[no_reg, no_rs, no_fu]):
        	     COND
          	       fu=fu_alu -> ID`alu,
          	       fu=fu_fpu1-> ID`faddsub,
          	       fu=fu_fpu2-> ID`fmuldiv,
          	       fu=fu_fpu3-> ID`fnegabs OR ID`fsqrt OR ID`frem OR
                       		ID`fmov OR ID`fcvt OR ID`mi2f OR
                       		ID`mf2i OR ID`fcond,
          	       fu=fu_mem -> ID`mem
        	     ENDCOND
		 ENDIF,
	issue_with_result=(S1`CAipf OR S1`CAimal OR I_illegal(S1`IR) OR I_trap(S1`IR) OR 
    			I_branch(S1`IR) OR I_j(S1`IR) OR I_jr(S1`IR) OR I_rfe(S1`IR) OR 
    			I_movs2i(S1`IR) OR I_movi2s(S1`IR)),
	issue_rs=LET x=LAMBDA (i: below(4)): NOT S2`RS(i)`valid,
		     alu_ffo=LAMBDA (n:below(4)):
		       	       IF empty?(x) THEN
				 FALSE
			       ELSE
				 n=min[below(4)](x)
			       ENDIF IN
    			LAMBDA (rs: below(no_rs)):
    			  COND
      			    rs<rs_alu+4->alu_ffo(rs) AND issue_fu(fu_alu),
      			    rs=rs_fpu1 ->NOT S2`RS(rs)`valid AND issue_fu(fu_fpu1),
      			    rs=rs_fpu2 ->NOT S2`RS(rs)`valid AND issue_fu(fu_fpu2),
      			    rs=rs_fpu3 ->NOT S2`RS(rs)`valid AND issue_fu(fu_fpu3),
      			    rs=rs_mem  ->NOT S2`RS(rs)`valid AND issue_fu(fu_mem)
    			  ENDCOND,
	full_1=S1`full,
        stall_1=(s4`ROBfull AND NOT s4`writeback OR
    		  (NOT issue_with_result AND FORALL (rs: rsnot):NOT issue_rs(rs))  OR
    		  ID`movs2i AND bv2nat(IA`sop(0)`A)=nspr_IEEEf AND NOT s4`ROBempty OR
    		  (ID`branch OR ID`jr OR ID`movi2s OR ID`movs2i OR ID`rfe) AND NOT sourceops(0)`valid OR
    		  ID`rfe AND (NOT S5`SPRp(nspr_EPC)`valid OR NOT S5`SPRp(nspr_EDPC)`valid)) AND
                full_1,
        ue_1=(NOT s4`rollback) AND full_1 AND (NOT stall_1) IN
    (#
      ID:=ID,
      IA:=IA,
      rf:=rf,
      sourceops:=sourceops,

      issue_exception:=issue_exception,
      issue_CA:=issue_CA,
      issue_EData:=issue_EData,
      nextPCp:=nextPCp,
      nextDPC:=nextDPC,

      issue_fu:=issue_fu,
      issue_with_result:=issue_with_result,
      issue_rs:=issue_rs,
      full_1 :=full_1,
      stall_1:=stall_1,
      ue_1   :=ue_1,
      issue  :=ue_1
    #);

  signals0_spec(DPC : registert, mem:mem_reg, ROBhead: tagt,
	   	ext_in    : data_outputt[29,2^3],
  	   	ext_reset : bit,
	   	bp_in     : memory_outputt[29,2,2^3],
	   	reset: bool, s1: signals1t, s2: signals2t, s3: signals3t, s4: signals4t):signals0t=
    LET g_0DPC=IF s1`full_1 THEN s1`nextDPC ELSE DPC ENDIF IN

    LET mem_input=(# clear    := s4`clear, 
		     stall_in := s3`FU_stall_in(fu_mem),
                     inputs   := s2`fu_inputs(fu_mem), 
		     PC       := g_0DPC, 
		     ROBtail  := ROBhead,
		     bp_in    := bp_in,
                     ext_in   := ext_in,
                     ext_reset:= ext_reset #) IN
    LET mem_step=tommem_step_ui(mem, mem_input) IN

    LET full_0=TRUE,
        stall_0=(s1`stall_1 OR mem_step`imem_busy) AND full_0 IN
    (#
      g_0DPC :=g_0DPC,
      full_0 :=full_0,
      stall_0:=stall_0,
      ue_0   :=(NOT s4`rollback) AND full_0 AND (NOT stall_0),
      mem_step:=mem_step,

      fuout  :=LAMBDA (fu: funot[no_reg, no_rs, no_fu]):
        COND
          fu=0 -> s2`alu_step`out,
          fu=1 -> s2`fpu1_step`out,
          fu=2 -> s2`fpu2_step`out,
          fu=3 -> s2`fpu3_step`out,
          fu=4 -> mem_step`out
        ENDCOND
    #);

  rs_step_spec(rs_reg: rs_regt, IA: IAt,
    clear, fill, dispatch: bit,
    CDB: cdbt, Din: rs_Dint):rs_regt=
    (#
      tag  :=IF fill THEN Din`tag ELSE rs_reg`tag ENDIF,
      f    :=IF fill THEN Din`f ELSE rs_reg`f ENDIF,
      valid:=IF clear THEN FALSE ELSIF fill THEN TRUE ELSIF dispatch THEN FALSE ELSE rs_reg`valid ENDIF,
      op   :=LAMBDA (x: below(6)):
               IF clear THEN 
      		 rs_reg`op(x) WITH [valid:=FALSE]
    	       ELSIF fill THEN
      		 Din`op(x)
    	       ELSIF rs_reg`op(x)`tag=CDB`tag AND NOT rs_reg`op(x)`valid AND 
			CDB`valid AND rs_reg`valid THEN
      		 (#
        	   valid:=TRUE,
        	   tag:=rs_reg`op(x)`tag,
        	   data:=IF rs_reg`fprh(x) THEN
		   	   CDB`data(1)
			 ELSE
			   CDB`data(0)
			 ENDIF
      		 #)
    	       ELSE
      		 rs_reg`op(x)
    	       ENDIF,
	 fprh:= IF fill THEN 
		  LAMBDA (x:below(6)):
	            IA`sop(x)`fprh
		ELSE
		  rs_reg`fprh
		ENDIF
    #);


  tom_step_spec(conf: tom_conft, reset: bool,
	   	ext_in    : data_outputt[29,2^3],
	   	ext_reset : bit,
	   	bp_in     : memory_outputt[29,2,2^3]): 
    [# conf    : tom_conft,
       ext_out : data_inputt[29,2^3],
       bp_out  : memory_inputt[29,2,2^3] #]=

    LET s4=signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),reset),
        s3=signals3_spec(conf`S3),
        s2=signals2_spec(conf`S3, conf`S2,              	       reset,         s3, s4`clear),
        s1=signals1_spec(conf`S1, conf`S2, conf`S4, conf`S5,	       reset,         s3, s4),
        s0=signals0_spec(conf`S2`DPC, conf`S3`mem, conf`S4`ROBhead, 
 		    ext_in, ext_reset, bp_in,		       reset, s1, s2, s3, s4) IN

    % Transition Function
    (# conf :=
    (#
      S1:=(#
         full:=(s0`ue_0 OR s1`stall_1) AND NOT s4`rollback AND NOT reset,
         IR    :=IF s0`ue_0 THEN s0`mem_step`imem_out ELSE conf`S1`IR     ENDIF,
         CAipf :=IF s0`ue_0 THEN s0`mem_step`ipf      ELSE conf`S1`CAipf  ENDIF,
         CAimal:=IF s0`ue_0 THEN s0`mem_step`imal     ELSE conf`S1`CAimal ENDIF
       #),

      S2:=(#
         PCp:=IF reset OR s4`JISR THEN
                SISRnext
              ELSIF s1`ue_1 THEN
                s1`nextPCp
              ELSE
                conf`S2`PCp
              ENDIF,

         DPC:=IF reset OR s4`JISR THEN
                SISR
              ELSIF s1`ue_1 THEN
                s1`nextDPC
              ELSE
                conf`S2`DPC
              ENDIF,

         RS:=LET Din=
      	     (#
              	op:=s1`sourceops,
        	tag:=conf`S4`ROBtail,
        	f:=conf`S1`IR
      	     #) IN
      	     LAMBDA (rs: below(no_rs)):
               rs_step_spec(conf`S2`RS(rs), s1`IA, s4`clear, s1`issue_rs(rs) AND s1`issue, 
			 	s2`dispatch_rs(rs), s3`CDB, Din), 
         alurs_arbiter:=arbiter_step_spec[4](conf`S2`alurs_arbiter,NOT s2`fu_stall_out(fu_alu),s4`clear)
        #),

      S3:=(#
         alu  :=s2`alu_step`reg,
         fpu1 :=s2`fpu1_step`reg,
         fpu2 :=s2`fpu2_step`reg,
         fpu3 :=s2`fpu3_step`reg,
         mem  :=s0`mem_step`reg,
         P:=LAMBDA (fu: funot[no_reg, no_rs, no_fu]):
           P_step(conf`S3`P(fu), s4`clear, s3`compl_p(fu), s0`fuout(fu)),
         CDB_arbiter:=arbiter_step_spec[no_fu](conf`S3`CDB_arbiter, TRUE, s4`clear)
        #),

      S4:=(#
         rob:=rob_step_spec(conf`S4`rob, s1`issue, s1`issue_with_result, s3`CDB,
                       s1`ID, s1`IA, s1`issue_CA, s1`issue_EData,
                       s1`nextPCp, s1`nextDPC, 
		       conf`S2`PCp, conf`S2`DPC, conf`S4`ROBtail, s1`sourceops(0)`data),
         ROBhead:=IF s4`clear THEN
                    tag0
		  ELSIF s4`writeback THEN
                    conf`S4`ROBhead+1
		  ELSE
                    conf`S4`ROBhead
		  ENDIF,
         ROBtail:=IF s4`clear THEN
                    tag0
		  ELSIF s1`issue THEN
                    conf`S4`ROBtail+1
		  ELSE
                    conf`S4`ROBtail
		  ENDIF,
         ROBcount:=IF s4`clear THEN
                     LAMBDA (i: below(tag_width+1)): FALSE
		   ELSIF s1`issue AND s4`writeback OR NOT s1`issue AND NOT s4`writeback THEN
      		     conf`S4`ROBcount
    		   ELSIF s1`issue AND NOT s4`writeback THEN
      		     conf`S4`ROBcount+1
    		   ELSE
      		     conf`S4`ROBcount-1
    		   ENDIF
        #),

      S5:=(#
         GPR  :=s1`rf`nextGPR,
         SPR  :=SPR_next_spec(conf`S5`SPR, reset, s4`writeback, s4`JISR,
                         s4`repeat, s4`wbROBe, s4`MCA),
         FPRl :=s1`rf`nextFPRl,
         FPRh :=s1`rf`nextFPRh,
         GPRp :=prod_step5_spec(conf`S5`GPRp,  s4`clear, s1`IA`dest`A, s4`wbROBe`dest`A,
			      	s1`issue AND s1`IA`dest`gpr, 
			      	s4`writeback AND s4`wbROBe`dest`gpr,
		       		conf`S4`ROBtail, conf`S4`ROBhead),
         SPRp :=prod_step5_spec(conf`S5`SPRp,  s4`clear, s1`IA`dest`A, s4`wbROBe`dest`A,
			      	s1`issue AND s1`IA`dest`spr, 
			      	s4`writeback AND s4`wbROBe`dest`spr,
			       conf`S4`ROBtail, conf`S4`ROBhead),
         FPRlp:=prod_step4_spec(conf`S5`FPRlp, s4`clear, s1`IA`dest`A^(4,1), s4`wbROBe`dest`A^(4,1),
			      	s1`issue AND s1`IA`dest`fprl, 
			      	s4`writeback AND s4`wbROBe`dest`fprl,
			       conf`S4`ROBtail, conf`S4`ROBhead),
         FPRhp:=prod_step4_spec(conf`S5`FPRhp, s4`clear, s1`IA`dest`A^(4,1), s4`wbROBe`dest`A^(4,1),
			      	s1`issue AND s1`IA`dest`fprh, 
			      	s4`writeback AND s4`wbROBe`dest`fprh,
			       conf`S4`ROBtail, conf`S4`ROBhead)
        #)
    #),
    ext_out := s0`mem_step`ext_out,
    bp_out  := s0`mem_step`bp_out
    #);
    
    arbitrary_conf : tom_conft;

%% The recursive definition of the configuration for reasoning in the proofs

    tom_impl_conf(init_conf: tom_conft, input:tom_impl_input_funct,n:nat):RECURSIVE tom_conft=
      IF n=0 THEN
	init_conf
      ELSE
	tom_step_spec(tom_impl_conf(init_conf,input,n-1),
		      input(n-1)`reset,
		      input(n-1)`ext_in,
		      input(n-1)`ext_reset,
		      input(n-1)`bp_in)`conf
      ENDIF
      MEASURE n;

%% the output function

  tom_impl_out(init_conf: tom_conft, input:tom_impl_input_funct)(n:nat):tom_impl_outputt=
    LET next=tom_step_spec(tom_impl_conf(init_conf,input,n),
		      input(n)`reset,
		      input(n)`ext_in,
		      input(n)`ext_reset,
		      input(n)`bp_in) IN
	(# ext_out := next`ext_out,
	   bp_out  := next`bp_out #);

%% Assumption is all the correctness proofs:
%% * no ext_reset during VAMP runtime
%% * no write access on external memory access port
%% * external access port is kept stable if externel busy is asserted
%% NOTE: external reset is later on asusmed initially
%% and external writes are allowed as long es the VAMP is kept in the reset state
%% in order to allow for uploading of programs into the VAMP memory

  good_tom_impl_input_func?(T:nat,init_conf:initial_conft)(input:tom_impl_input_funct):bool =
    (FORALL (Tp:upto(T)): NOT input(Tp)`ext_reset) AND
    (FORALL (Tp:upto(T)): NOT input(Tp)`ext_in`mw) AND
    (FORALL (Tp:below(T)): input(Tp)`ext_in`mr AND 
			 tom_impl_out(init_conf,input)(Tp)`ext_out`busy IMPLIES
			input(Tp+1)`ext_in=input(Tp)`ext_in);

END tom_impl_spec