%
% Tomasulo Transition Function
%
% (C) 2000-2001 Daniel Kroening
%

tom_implementation: THEORY
BEGIN

  dlxif: LIBRARY = "../dlxif";

  IMPORTING dlxif@dlxifinit, tom_signals, producer;

%% this is the *concrete* VAMP implementation in contrast to the
%% abstract implementation from tom_impl_spec
%% this is next state function that is actually synthesized to Verilog HDL
%% (together with all the files it imports)

  tom_step(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(conf`S4, conf`S5`SPR(nspr_SR), 	       reset),
        s3=signals3(conf`S3),
        s2=signals2(conf`S3, conf`S2,              	       reset,         s3, s4`clear),
        s1=signals1(conf`S1, conf`S2, conf`S4, conf`S5,	       reset,         s3, s4),
        s0=signals0(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:=all_RS_step(conf`S2`RS, s1`IA, s4`clear, s1`issue, s1`issue_rs, s2`dispatch_rs,
                         s3`CDB, s1`sourceops, conf`S4`ROBtail, conf`S1`IR), 

         alurs_arbiter:=arbiter_step[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[5](conf`S3`CDB_arbiter, TRUE, s4`clear)
        #),

      S4:=(#
         rob:=rob_step(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:=ROBhead_step(conf`S4`ROBhead, s4`clear, s4`writeback),
         ROBtail:=ROBtail_step(conf`S4`ROBtail, s4`clear, s1`issue),
         ROBcount:=ROBcount_step(conf`S4`ROBcount, s4`clear, s1`issue, s4`writeback)
        #),

      S5:=(#
         GPR  :=s1`rf`nextGPR,
         SPR  :=SPR_next(conf`S5`SPR, reset, s4`writeback, s4`JISR,
                         s4`repeat, s4`wbROBe, s4`MCA),
         FPRl :=s1`rf`nextFPRl,
         FPRh :=s1`rf`nextFPRh,
         GPRp :=gpr_prod_step (conf`S5`GPRp,  s4`clear, s1`IA, s4`wbROBe, s1`issue, s4`writeback,
			       conf`S4`ROBtail, conf`S4`ROBhead),
         SPRp :=spr_prod_step (conf`S5`SPRp,  s4`clear, s1`IA, s4`wbROBe, s1`issue, s4`writeback,
			       conf`S4`ROBtail, conf`S4`ROBhead),
         FPRlp:=fprl_prod_step(conf`S5`FPRlp, s4`clear, s1`IA, s4`wbROBe, s1`issue, s4`writeback,
			       conf`S4`ROBtail, conf`S4`ROBhead),
         FPRhp:=fprh_prod_step(conf`S5`FPRhp, s4`clear, s1`IA, s4`wbROBe, s1`issue, s4`writeback,
			       conf`S4`ROBtail, conf`S4`ROBhead)
        #)
    #),
    ext_out := s0`mem_step`ext_out,
    bp_out  := s0`mem_step`bp_out
    #);

END tom_implementation