%
% Tomasulo Common Data Bus (CDB)
%
% (C) 2000-2001 Daniel Kroening
%

cdb: THEORY
BEGIN

  IMPORTING tom_conft, tomconst;

  % valid bits stored in the producers

  P_valid(S3: S3conft): bvec[no_fu]=
    LAMBDA (i: funot[no_reg, no_rs, no_fu]): S3`P(i)`valid;

  IMPORTING arbiter_impl;

  % producer for completion

  tomcompl_p(S3: S3conft): bvec[no_fu]=
    arbiter_impl[no_fu](S3`CDB_arbiter, P_valid(S3));

  compl_p_unique: LEMMA
    FORALL (S3: S3conft):
    unique?(LAMBDA (fu: funot): tomcompl_p(S3)(fu));

  compl_p_correct : LEMMA
    FORALL (S3: S3conft):
    (empty?(tomcompl_p(S3)) OR singleton?(tomcompl_p(S3))) AND
    FORALL (fu:funot):
    tomcompl_p(S3)(fu) IMPLIES S3`P(fu)`valid;

  tomCDB(S3: S3conft, compl_p: bvec[no_fu]):cdbt=
    IF compl_p(0) THEN
      S3`P(0)
    ELSIF compl_p(1) THEN
      S3`P(1)
    ELSIF compl_p(2) THEN
      S3`P(2)
    ELSIF compl_p(3) THEN
      S3`P(3)
    ELSIF compl_p(4) THEN
      S3`P(4)
    ELSE
      (#
        tag:=tag0,
        valid:=FALSE,
        data:=LAMBDA (x: below(2)): r0,
        CA:=r0,
        EData:=r0
      #)
    ENDIF;

  tomCDB_correct : LEMMA
  FORALL (S3: S3conft):
  LET compl_p=tomcompl_p(S3) IN
  tomCDB(S3,compl_p)=
    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;

  tomCDB_correct2 : LEMMA
  FORALL (S3: S3conft):
  LET compl_p=tomcompl_p(S3) IN
  tomCDB(S3,compl_p)`valid = NOT empty?(compl_p);

  CDB_select_correct: LEMMA
    FORALL (S3: S3conft, compl_p: bvec[no_fu], fu: funot):
    unique?(LAMBDA (f: funot): compl_p(f)) AND compl_p(fu)
    => (tomCDB(S3, compl_p)=S3`P(fu));

  tomCDB_valid_correct: LEMMA
    FORALL (S3: S3conft):
    tomCDB(S3, tomcompl_p(S3))`valid<=>(EXISTS (fu: funot): tomcompl_p(S3)(fu));

  % stall signals for function units

  tomFU_stall_in(S3: S3conft, compl_p: bvec[no_fu]):bvec[no_fu]=
    LAMBDA (i: below(no_fu)): P_valid(S3)(i) AND NOT compl_p(i);

END cdb