%
% Tomasulo Transition Function: Issuing an Instruction
%
% (C) 2000-2001 Daniel Kroening
%

tomissue: THEORY
BEGIN

  dlxif: LIBRARY = "../dlxif";
  IMPORTING dlxif@dlxspr;

  IMPORTING tomconst, dlxtombasics, tomdecode, tom_conft, find_first_one;

  % determine which FU gets an instuction

  fugen(ID: IDt, exception: bool): bvec[no_fu] =
    IF 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;

  % at most one functional unit gets the instruction

  fugen_unique: LEMMA
    FORALL (Iw: registert, exception: bool):
    unique?(LAMBDA (fu: funot): fugen(tomID(Iw), exception)(fu));

  % no functional unit?

  issue_with_result(fu: bvec[no_fu]):bool=
    zerotester_impl(fu);

  issue_with_result_correct : LEMMA
  FORALL (S1 : S1conft):
    LET ID=tomID(S1`IR),
        issue_exception=S1`CAipf OR S1`CAimal,
        issue_fu=fugen(ID, issue_exception) IN
    zerotester_impl[no_fu](issue_fu)=
    (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));
  
  % reservation station for issue

  tomissue_rs(S2: S2conft,
              issue_fu: bvec[no_fu]):bvec[no_rs]=
    LET alu_ffo=find_first_one_impl[4]
        (LAMBDA (x: below(4)): NOT S2`RS(x)`valid)`b 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;

  tomissue_rs_unique: LEMMA
    FORALL (S2: S2conft, issue_fu: bvec[no_fu]):
    unique?(LAMBDA (fu: funot): issue_fu(fu)) =>
    unique?(LAMBDA (rs: rsnot): tomissue_rs(S2, issue_fu)(rs));

  % exceptions available at issue time

  tomissue_CA(S1: S1conft, ID: IDt):registert=
    LAMBDA (i: below(32)):
    COND
      i=1  -> ID`illegal,
      i=2  -> S1`CAimal,
      i=3  -> S1`CAipf,
      i=5  -> ID`trap,
      ELSE -> FALSE
    ENDCOND;

  % stall signal for issue

  tomissue_stall(S5: S5conft,
                 ID: IDt, IA: IAt, issue_rs: bvec[no_rs],
                 issue_with_result, ROBfull, ROBempty: bool,
                 sourceops: tomsourceopst,
                 writeback:bool):bool=
    (ROBfull AND NOT writeback) OR
    (zerotester_impl[no_rs](issue_rs) AND NOT issue_with_result) OR
    (ID`movs2i AND equalitytester_impl[5](IA`sop(0)`A, SPR_IEEEf) AND NOT 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));

  tomissue_stall_correct : LEMMA
  FORALL (S5: S5conft,
          ID: IDt, IA: IAt, issue_rs: bvec[no_rs],
          issue_with_result, ROBfull, ROBempty: bool,
          sourceops: tomsourceopst,
          writeback:bool):
  tomissue_stall(S5, ID, IA, issue_rs, issue_with_result, 
		 ROBfull, ROBempty, sourceops, writeback)=
   (ROBfull AND NOT 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 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));

END tomissue