tom_correct2a[(IMPORTING tom_conft,fpu_impl_ui_types)
	       initial_vamp:initial_conft,
	       fpu_spec_op : fpu_spec_op_t,
	       (IMPORTING fpu_impl_ui_ok_types[fpu_spec_op])
	       add_spec:add_spec_t,
	       md_spec :md_spec_t,
	       fpm_spec:fpm_spec_t,
	       TOMadd : add_circuit_t,
	       TOMmd  : md_circuit_t,
	       TOMfpm : fpm_circuit_t,
	       mif_next:mif_next_t,
	       initial_vamp_mem:mem_state]: THEORY
BEGIN

  tomasulo: LIBRARY = "../tomasulo";

  IMPORTING tom_impl_spec[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op],
	    fpu_impl_ui_ok[fpu_spec_op,add_spec,md_spec,fpm_spec];

%% step 2: showing equivalence between VAMP implementation (tom_conf) and
%% Tomasulo implementation (cI)
%% sub-step a: defining cI

% after defining cS, we will define cI, Daniels Tomasulo implementation
% that is a live refinement of cS
% cI contains a reorder buffer, producers, and reservation stations
% apart from the register file inherited from cS

% inputs to cI are functions that define for any cycle T whether
% an instruction is issued, dispatched, completed, .. and so on

% with these functions and cS, Daniel defines a Tomasulo implementation cI
% WITHOUT instruction fetch, memory, interrupts and implementation registers
% (e.g. buffering of instuction destination register in Rob or opcode in RS)

% for Daniels proof to be valid, these functions have to satisfy a set of assumptions
% i.e. an issue does not overwrite valid data in a reservation station
% these assumptions naturally are on the cI configurations that are derived from the functions

% ideally, the input functions should be derived from the VAMP, and
% then, the equality of VAMP and cI is shown.
% however, since the functions have to satisfy assumptions on the cI derived from the functions,
% this circular approach becomes extremely messy if feasible at all

% therefore, we introduce an additional intermediate layer.
% we first define the input functions for cI as functions on cI configurations
% and some further configuration parts derived from the VAMP (PC,...)
% we then define our own cI and scheduling functions in 'my' based on these input functions
% we then define Daniel's real input functions with the n-th 'my' configuration 
% and the configuration input functions
% and finally, we show the 'obvious' again: 'my' equals Daniel's definition...

% thx to Daniel for this unnecessary detour

% in order to apply the correctness proofs, we derive the initial specification configuration
% from the initial VAMP
% the derivation is the obvious one: copy all the visible registers
  init_conf : dlx_conft =
  (# GPR  := initial_vamp`S5`GPR,
     FPRh := initial_vamp`S5`FPRh,
     FPRl := initial_vamp`S5`FPRl,
     SPR  := LAMBDA(reg:bvec[5]):IF bv2nat(reg)<=nspr_LAST THEN
				   initial_vamp`S5`SPR(bv2nat(reg))
				 ELSE
				   r0
				 ENDIF,
     PCp  := initial_vamp`S2`PCp,
     DPC  := initial_vamp`S2`DPC,
     mem  := LET inst           =initial_vamp`S3`mem`inst,
		 EA:below(2^29) =bv2nat(inst`EA^(31,3)) IN
	     IF inst`rollback AND inst`I_s THEN
	       initial_vamp_mem WITH [(EA):=
		 LAMBDA (j:below(64)):
              	   IF inst`mwb(div(j,8)) THEN
                     inst`data(j)
               	   ELSE
                     initial_vamp_mem(EA)(j)
                   ENDIF ]
	     ELSE
	       initial_vamp_mem 
	     ENDIF #);

  IMPORTING tom_correct[fpu_spec_op,TOMadd,TOMmd,TOMfpm,mif_next,init_conf], 
		tomasulo@tomimplspec[no_reg, no_rs, no_fu],
		tomasulo@tomfusi, tomasulo@tagtheory;

  T: VAR nat;
  i: VAR nat;

% a helper lemma for the mysterious embedding function from the last theory
% we need a register 'fprh' in the RS in order to compute the cSspec'e
  embedding_helper : LEMMA
    FORALL (IR:registert,x:below(6)):
    cSspec`e(cSS(IR,x))=IF x<4 AND tomIA(tomID(IR))`sop(x)`fprh THEN
		       	  1
		     	ELSE
			  0
		     	ENDIF;

% we map VAMP configurations to cI configurations	
  map_cIt(conf:tom_conft):cIt=
    (#
       	R  := LAMBDA (r:regnot):
    	     	LET t=conf`S5 IN
    	      	COND
    		  r<32           -> LET x=nat2bv[5](r)    IN 
				(# data:=t`GPR(x),  valid:=t`GPRp(r)`valid,  tag:=t`GPRp(r)`tag  #),
    		  r>=32 AND r<48 -> LET x=nat2bv[4](r-32) IN 
				(# data:=t`FPRl(x), valid:=t`FPRlp(r-32)`valid, tag:=t`FPRlp(r-32)`tag #),
    		  r>=48 AND r<64 -> LET x=nat2bv[4](r-48) IN 
				(# data:=t`FPRh(x), valid:=t`FPRhp(r-48)`valid, tag:=t`FPRhp(r-48)`tag #),
    		  ELSE           -> 
				(# data:=t`SPR(r-64),  valid:=t`SPRp(r-64)`valid,  tag:=t`SPRp(r-64)`tag  #)
    	        ENDCOND,
	RS := LAMBDA (rs:rsnot):
      		LET RS = conf`S2`RS(rs) IN
    		(# 
       		  op    := RS`op,
       		  valid := RS`valid,
       		  tag   := RS`tag
    		#),
	ROB:= LAMBDA (tag:tagt):
      		LET i   = bv2nat(tag),
          	    ROB = conf`S4`rob(i) IN
    		(# 
      		  valid  := ROB`valid,
      		  result := LAMBDA (d:dt):
			      COND d<2 -> ROB`data(d),
				   d=2 -> ROB`CA,
				   d=3 -> ROB`EData
			      ENDCOND
		#),
	P  := LAMBDA (fu:funot):
      		LET P = conf`S3`P(fu) IN
    		(#
      		  valid  := P`valid,
      		  tag    := P`tag,
      		  result := LAMBDA (d:dt):
			      COND d<2 -> P`data(d),
				   d=2 -> P`CA,
				   d=3 -> P`EData
			      ENDCOND
    		#)
    #);

% the initial cI is defined in the obvious way...
  cIinitial: cIt=
    map_cIt(initial_vamp);

%% and now the dozens of helper functions needed in order to
%% define "my", our own version of cI

% MCA from VAMP translated to extended cI
  MCA(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1]):registert =
    LET CA=cI`ROB(ROBhead)`result(2),
	SR=cI`R(64)`data IN
      LAMBDA (i:below(32)):
        IF i>=6 AND i/=12 THEN
          CA(i) AND SR(i)
        ELSE
          CA(i)
        ENDIF;

% JISR from VAMP translated to extended cI
  JISR(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1]):bool =
    cI`ROB(ROBhead)`valid AND NOT bv2nat(ROBcount)=0 AND 
      NOT empty?(MCA(cI,ROBhead,ROBtail,ROBcount));

% repeat from VAMP translated to extended cI
  repeat(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1]):bool =
      NOT empty?(MCA(cI,ROBhead,ROBtail,ROBcount)^(4,0));

% configuration versions of input to Daniel's cI
  cIissue_with_result(S1:S1conft):bool=
    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);

  cIwriteback(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1]):bool=
    LET wbROBe   = cI`ROB(ROBhead),
	ROBempty = bv2nat(ROBcount)=0 IN
       wbROBe`valid AND NOT ROBempty;
    
  cIissue_rs(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1], S1:S1conft, rs:rsnot):bool=
    LET	issue_exception=S1`CAipf OR S1`CAimal,
	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 -> I_is_alu(S1`IR),
          	       fu=fu_fpu1-> I_faddsub(S1`IR),
          	       fu=fu_fpu2-> I_fmuldiv(S1`IR),
          	       fu=fu_fpu3-> I_fnegabs(S1`IR) OR I_fsqrt(S1`IR) OR 
					I_frem(S1`IR) OR I_fmov(S1`IR) OR 
					I_fcvt(S1`IR) OR I_mi2f(S1`IR) OR
                       			I_mf2i(S1`IR) OR I_fcond(S1`IR),
          	       fu=fu_mem -> I_mem(S1`IR)
        	     ENDCOND
		 ENDIF,
	x=LAMBDA (i: below(4)): NOT cI`RS(i)`valid,
	alu_ffo=LAMBDA (n:below(4)):
		  IF empty?(x) THEN
		    FALSE
		  ELSE
		    n=min[below(4)](x)
		  ENDIF IN
	S1`full AND NOT (bv2nat(ROBcount)=rob_entries AND NOT 
	  cIwriteback(cI, ROBhead, ROBtail, ROBcount)) AND
  	COND
      	    rs<rs_alu+4->alu_ffo(rs) AND issue_fu(fu_alu),
      	    rs=rs_fpu1 ->NOT cI`RS(rs)`valid AND issue_fu(fu_fpu1),
      	    rs=rs_fpu2 ->NOT cI`RS(rs)`valid AND issue_fu(fu_fpu2),
      	    rs=rs_fpu3 ->NOT cI`RS(rs)`valid AND issue_fu(fu_fpu3),
      	    rs=rs_mem  ->NOT cI`RS(rs)`valid AND issue_fu(fu_mem)
    	ENDCOND;

  cIcompletion(cI:cIt):bool=
    NOT empty?(LAMBDA (i: funot[no_reg, no_rs, no_fu]): cI`P(i)`valid);

  cIcompl_p(cI:cIt,CDB_arbiter:arbiter_conft[no_fu]):funot=
    LET compl_p=arbiter_impl_spec[no_fu](CDB_arbiter, 
				   LAMBDA (i: funot[no_reg, no_rs, no_fu]): cI`P(i)`valid) IN
    IF empty?(compl_p) THEN
      0
    ELSE
      the(compl_p)
    ENDIF;

% a few shortcut functions in order to reduce size of 'my' definition
  fu_stall_in(cI:cIt,CDB_arbiter:arbiter_conft[no_fu])(fu:funot):bool=
    cI`P(fu)`valid AND NOT (cIcompletion(cI) AND cIcompl_p(cI,CDB_arbiter)=fu);

  fu_conft : TYPE = [#  mem: mem_reg,
    			fpu1: fpu1_reg,
    			fpu2: fpu2_reg,
    			fpu3: fpu3_reg,
    			alu: alu_reg #];
		        
  fu_stall_out(cI:cIt, CDB_arbiter:arbiter_conft[no_fu], fu_conf:fu_conft)(fu: funot):bool=
      COND
	fu=0 -> fu_stall_in(cI,CDB_arbiter)(fu),
	fu=1 -> tomfpu1_stallout_ui(fu_conf`fpu1, fu_stall_in(cI,CDB_arbiter)(fu)),
	fu=2 -> tomfpu2_stallout_ui(fu_conf`fpu2, fu_stall_in(cI,CDB_arbiter)(fu)),
	fu=3 -> tomfpu3_stallout_ui(fu_conf`fpu3, fu_stall_in(cI,CDB_arbiter)(fu)),
	fu=4 -> tommem_stallout (fu_conf`mem,  fu_stall_in(cI,CDB_arbiter)(fu))
      ENDCOND;

  CDB(cI:cIt, CDB_arbiter:arbiter_conft[no_fu]):CDBt= 
	LET completion=cIcompletion(cI),
	    compl_p   =cIcompl_p(cI,CDB_arbiter) IN
	(# valid := completion,
   	   tag   := IF completion THEN
	       	      cI`P(compl_p)`tag
	    	    ELSE
	       	      tag0
	    	    ENDIF,
   	   result:= IF completion THEN
	       	      cI`P(compl_p)`result
	    	    ELSE
	       	      LAMBDA (d: dt): r0
	    	    ENDIF #);

  issue_op(cI:cIt, CDB_arbiter:arbiter_conft[no_fu], r:regnot):tomt=
    LET tag=cI`R(r)`tag,
	CDB=CDB(cI, CDB_arbiter) IN
    IF r=0 THEN
      (#
        valid:=TRUE,
        tag:=tag0,
        data:=r0
      #)
    ELSIF cI`R(r)`valid THEN % Register File
      cI`R(r)
    ELSIF CDB`valid AND CDB`tag=tag THEN % CDB
      (#
        valid:=TRUE,
        tag:=tag,
        data:=CDB`result(cSspec`e(r))
      #)
    ELSE % ROB + no data in one case
      (#
        valid:=cI`ROB(tag)`valid,
        tag:=tag,
        data:=cI`ROB(tag)`result(cSspec`e(r))
      #)
    ENDIF;
	
  stall_1(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1], 
	  S1:S1conft, CDB_arbiter:arbiter_conft[no_fu]):bool=
	(bv2nat(ROBcount)=rob_entries AND NOT 
	  cIwriteback(cI, ROBhead, ROBtail, ROBcount) OR
	  NOT cIissue_with_result(S1) AND (FORALL (rs:rsnot):
	  NOT cIissue_rs(cI, ROBhead, ROBtail, ROBcount, S1, rs)) OR
	  I_movs2i(S1`IR) AND cSS(S1`IR,0)=64+nspr_IEEEf AND NOT bv2nat(ROBcount)=0 OR 
	  (I_branch(S1`IR) OR I_jr(S1`IR) OR I_movi2s(S1`IR) OR I_movs2i(S1`IR) OR 
	   I_rfe(S1`IR)) AND NOT issue_op(cI, CDB_arbiter, cSS(S1`IR,0))`valid OR
	  I_rfe(S1`IR) AND (NOT cI`R(64+nspr_EPC)`valid OR NOT cI`R(64+nspr_EDPC)`valid)) AND
	  S1`full;

% and the next input functions for Daniel in config-version
  cIissue(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1], 
	  S1:S1conft, CDB_arbiter:arbiter_conft[no_fu]):bool=
	S1`full AND NOT stall_1(cI, ROBhead, ROBtail, ROBcount, S1, CDB_arbiter);

  cIdispatch_rs(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1], 
		alurs_arbiter:arbiter_conft[4], CDB_arbiter:arbiter_conft[no_fu],
		fu_conf:fu_conft, rs:rsnot):bool=
    LET fu_stall_out=LAMBDA (fu:funot):fu_stall_out(cI,CDB_arbiter,fu_conf)(fu),
	RS_valid=LAMBDA (i: below(no_rs)):
                   cI`RS(i)`valid AND
                   FORALL (x: below(6)): cI`RS(i)`op(x)`valid IN
	COND
	  rs<=3 -> arbiter_impl_spec[4](alurs_arbiter, RS_valid^(3, 0))(rs) AND
			 NOT fu_stall_out(0),
	  rs=4  -> RS_valid(4) AND NOT fu_stall_out(1),
	  rs=5  -> RS_valid(5) AND NOT fu_stall_out(2),
	  rs=6  -> RS_valid(6) AND NOT fu_stall_out(3),
	  rs=7  -> RS_valid(7) AND NOT fu_stall_out(4)
	ENDCOND;

  cIdispatch_fu(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1], 
		alurs_arbiter:arbiter_conft[4], CDB_arbiter:arbiter_conft[no_fu],
		fu_conf:fu_conft, fu:funot):rsnot=
    LET alu_disp=LAMBDA(rs:below(4)):
		   cIdispatch_rs(cI,ROBhead,ROBtail,ROBcount,
				alurs_arbiter,CDB_arbiter,fu_conf,rs) IN
      IF fu=0 THEN
	IF NOT empty?(alu_disp) THEN
	  the(alu_disp)
	ELSE
	  0
	ENDIF
      ELSE
	3+fu
      ENDIF;

% once again shortcuts
  cI_fu_rs_map(rs:RSt, f:registert):fu_rs_regt=
    (# valid := rs`valid,
       tag   := rs`tag,
       op    := LAMBDA (x:below(6)):rs`op(x)`data,
       f     := f
    #);

  fu_inputs(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1], 
	    alurs_arbiter:arbiter_conft[4], CDB_arbiter:arbiter_conft[no_fu],
	    fu_conf:fu_conft, sI_RS:[rsnot->upfrom(-1)])(fu:funot): fu_rs_regt= 
    LET rs=cIdispatch_fu(cI,ROBhead,ROBtail,ROBcount,alurs_arbiter,CDB_arbiter,fu_conf,fu) IN
      cI_fu_rs_map(cI`RS(rs) WITH
	           [valid := cIdispatch_rs(cI,ROBhead,ROBtail,ROBcount,alurs_arbiter,CDB_arbiter,fu_conf,rs)],
      IF sI_RS(rs)>=0 THEN
	Iw(dlx_conf_without_interrupt_IEEEf(init_conf,sI_RS(rs)))
      ELSE
        initial_vamp`S2`RS(rs)`f
      ENDIF);

  next_DPC(cI:cIt,S1:S1conft,PCp:registert):registert=
	IF I_rfe(S1`IR) THEN
       	  cI`R(64+nspr_EDPC)`data
        ELSE
          PCp
	ENDIF;

  mem_input(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1], 
	    alurs_arbiter:arbiter_conft[4], CDB_arbiter:arbiter_conft[no_fu],
	    fu_conf:fu_conft, sI_RS:[rsnot->upfrom(-1)],
	    input:tom_impl_inputt,S1:S1conft,PCp,DPC:registert):tommem_inputt = 
      (# clear    := FALSE, 
         stall_in := fu_stall_in(cI,CDB_arbiter)(fu_mem),
	 inputs   := fu_inputs(cI,ROBhead,ROBtail,ROBcount,alurs_arbiter,CDB_arbiter,fu_conf,sI_RS)(fu_mem), 
	 PC       := IF S1`full THEN
		       next_DPC(cI,S1,PCp)
		     ELSE
		       DPC
		     ENDIF, 
	 ROBtail  := ROBhead,
	 bp_in    := input`bp_in,
	 ext_in   := input`ext_in,
	 ext_reset:= FALSE #);

  fu_out(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1], 
	    alurs_arbiter:arbiter_conft[4], CDB_arbiter:arbiter_conft[no_fu],
	    fu_conf:fu_conft, sI_RS:[rsnot->upfrom(-1)],
	    input:tom_impl_inputt,S1:S1conft,PCp,DPC:registert)(fu:funot):cdbt=
    COND
      fu=fu_alu  -> tomalu_step_spec(fu_conf`alu, FALSE,fu_stall_in(cI,CDB_arbiter)(fu_alu),
			fu_inputs(cI,ROBhead,ROBtail,ROBcount,alurs_arbiter,CDB_arbiter,fu_conf,sI_RS)(fu_alu))`out,
      fu=fu_fpu1 -> tomfpu1_step_ui(fu_conf`fpu1, FALSE,fu_stall_in(cI,CDB_arbiter)(fu_fpu1),
			fu_inputs(cI,ROBhead,ROBtail,ROBcount,alurs_arbiter,CDB_arbiter,fu_conf,sI_RS)(fu_fpu1))`out,
      fu=fu_fpu2 -> tomfpu2_step_ui(fu_conf`fpu2, FALSE,fu_stall_in(cI,CDB_arbiter)(fu_fpu2),
			fu_inputs(cI,ROBhead,ROBtail,ROBcount,alurs_arbiter,CDB_arbiter,fu_conf,sI_RS)(fu_fpu2))`out,
      fu=fu_fpu3 -> tomfpu3_step_ui(fu_conf`fpu3, FALSE,fu_stall_in(cI,CDB_arbiter)(fu_fpu3),
			fu_inputs(cI,ROBhead,ROBtail,ROBcount,alurs_arbiter,CDB_arbiter,fu_conf,sI_RS)(fu_fpu3))`out,
      fu=fu_mem  -> tommem_step_ui(fu_conf`mem,mem_input(cI,ROBhead,ROBtail,ROBcount,alurs_arbiter,CDB_arbiter,fu_conf,sI_RS,
				  input,S1,PCp,DPC))`out
    ENDCOND;

% and the last input for Daniel
  fuspec(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1], 
	    alurs_arbiter:arbiter_conft[4], CDB_arbiter:arbiter_conft[no_fu],
	    fu_conf:fu_conft, sI_RS:[rsnot->upfrom(-1)],
	    input:tom_impl_inputt,S1:S1conft,PCp,DPC:registert,fu:funot,sI:nat): [# valid, stall : bit, sI : nat #]=
      (# valid := fu_out(cI,ROBhead,ROBtail,ROBcount,alurs_arbiter,CDB_arbiter,
		    	 fu_conf,sI_RS,input,S1,PCp,DPC)(fu)`valid,
         stall := fu_stall_out(cI,CDB_arbiter,fu_conf)(fu),
         sI    := sI #);	

% the final shortcuts
  writeback_f(cI:cIt,ROBhead:tagt,writeback:bit,sI_writeback:nat):cIt=
    IF writeback THEN
      cI WITH [R := LAMBDA (r:regnot):
	IF instr_has_dest(sI_writeback,r) THEN
	(# valid := IF cI`R(r)`tag=ROBhead THEN
			TRUE
		    ELSE
			cI`R(r)`valid
		    ENDIF,
	   tag   := cI`R(r)`tag,
	   data  := cI`ROB(ROBhead)`result(cSspec`e(r)) #)
	ELSIF r=idx_ieeef THEN
	  (# valid := cI`R(idx_ieeef)`valid,
	     tag   := cI`R(idx_ieeef)`tag,
	     data  := f_ieeef(cI`R(idx_ieeef)`data,
			      cI`ROB(ROBhead)`result) #)
	ELSE
	  cI`R(r)
	ENDIF]
    ELSE
      cI
    ENDIF;

  snoop_f(wb,cI:cIt,CDB:CDBt,sI_RS:[rsnot->upfrom(-1)]):cIt=
    wb WITH [ RS := LAMBDA (rs:rsnot):
  	IF cI`RS(rs)`valid AND sI_RS(rs)>=0 THEN
    	  wb`RS(rs) WITH [ op := LAMBDA (x:st):
	    IF NOT cI`RS(rs)`op(x)`valid AND CDB`valid AND
		CDB`tag=cI`RS(rs)`op(x)`tag THEN
	    (# valid := TRUE,
	       tag   := CDB`tag,
	       data  := CDB`result(cSspec`e(S(sI_RS(rs),x)))
	    #)
	    ELSE
	      wb`RS(rs)`op(x)
	    ENDIF]
  	ELSE
    	  wb`RS(rs)
  	ENDIF];

  completion_f(snoop_p,cI:cIt,CDB:CDBt,completion:bit,compl_p:funot,
		fuout:[funot->[# valid, stall : bit, sI: nat #]]):cIt= 
    IF CDB`valid THEN
      snoop_p WITH [`ROB(CDB`tag) := 
        (# valid  := TRUE,
	   result := CDB`result #)]
    ELSE snoop_p 
    ENDIF WITH [P := LAMBDA (fu:funot):
      IF fuout(fu)`valid THEN
	  (# valid  := TRUE,
	     result := result(fuout(fu)`sI),
	     tag    := I_tag(fuout(fu)`sI)
	  #)
      ELSIF completion AND fu=compl_p THEN
        snoop_p`P(fu) WITH [valid := FALSE]
      ELSE
        snoop_p`P(fu)
      ENDIF ];

% additional sIS1 schedulind function for stage 1
  cIS1(cI:cIt, ROBhead, ROBtail:tagt, ROBcount:bvec[tag_width+1],
       S1:S1conft, CDB_arbiter:arbiter_conft[no_fu], imem_busy:bit):bool=
	NOT (stall_1(cI, ROBhead, ROBtail, ROBcount, S1, CDB_arbiter) OR imem_busy);

END tom_correct2a