%
% Tomasulo Dispatch Control
%
% (C) 2000-2001 Daniel Kroening
%

dispatch: THEORY
BEGIN

  IMPORTING cdb, tomconst;

  % valid bits stored in the reservation stations

 tomRS_valid(S2: S2conft): bvec[no_rs]=
    LAMBDA (i: below(no_rs)):
    S2`RS(i)`valid AND
    equalitytester_impl[6]
      (LAMBDA (x: below(6)): S2`RS(i)`op(x)`valid, fill[6](TRUE));

 tomRS_valid_correct : LEMMA
 FORALL (S2: S2conft): 
 tomRS_valid(S2)=
    LAMBDA (i: below(no_rs)):
    S2`RS(i)`valid AND
    FORALL (x: below(6)): S2`RS(i)`op(x)`valid;

  IMPORTING arbiter_impl;

  % RS for dispatch

  tomdispatch_rs(S2: S2conft, fu_stall: bvec[no_fu]): bvec[no_rs]=
    LET RS_valid=tomRS_valid(S2) IN
    LAMBDA (i: below(no_rs)):
    COND
      i<=3 -> arbiter_impl[4](S2`alurs_arbiter, RS_valid^(3, 0))(i)
              AND NOT fu_stall(0),
      i=4  -> RS_valid(4) AND NOT fu_stall(1),
      i=5  -> RS_valid(5) AND NOT fu_stall(2),
      i=6  -> RS_valid(6) AND NOT fu_stall(3),
      i=7  -> RS_valid(7) AND NOT fu_stall(4)
    ENDCOND;

  tomdispatch_rs_correct : LEMMA
  FORALL (S2       : S2conft, 
	  fu_stall : bvec[no_fu]):
  (empty?(tomdispatch_rs(S2,fu_stall)^(3,0)) OR 
    singleton?(tomdispatch_rs(S2,fu_stall)^(3,0))) AND
  tomdispatch_rs(S2,fu_stall)=
    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[4](S2`alurs_arbiter, RS_valid^(3, 0))(i)
              AND NOT fu_stall(0),
      i=4  -> RS_valid(4) AND NOT fu_stall(1),
      i=5  -> RS_valid(5) AND NOT fu_stall(2),
      i=6  -> RS_valid(6) AND NOT fu_stall(3),
      i=7  -> RS_valid(7) AND NOT fu_stall(4)
    ENDCOND;

  tomdispatch_rs_is_valid: LEMMA
    FORALL (S2: S2conft, fu_stall: bvec[no_fu], rs: rsnot):
    tomdispatch_rs(S2, fu_stall)(rs)
    => tomRS_valid(S2)(rs);

  tom_fu_inputs(S2: S2conft, dispatch_rs: bvec[no_rs]):[funot[no_reg, no_rs, no_fu]->fu_rs_regt]=
    LAMBDA (fu: funot[no_reg, no_rs, no_fu]):
      fu_rs_map(COND
        fu=0->IF dispatch_rs(0) THEN
            S2`RS(0)
          ELSIF dispatch_rs(1) THEN
            S2`RS(1)
          ELSIF dispatch_rs(2) THEN
            S2`RS(2)
          ELSIF dispatch_rs(3) THEN
            S2`RS(3)
          ELSE
            S2`RS(0) WITH [valid:=FALSE]
          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);

  tom_fu_inputs_correct : LEMMA
  FORALL (S2: S2conft, fu_stall: bvec[no_fu]):
  LET dispatch_rs=tomdispatch_rs(S2,fu_stall) IN
  tom_fu_inputs(S2,dispatch_rs)=
    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);

END dispatch