%
% Tomasulo Transition Function: Decoding the Instruction Word
%
% (C) 2000-2001 Daniel Kroening
%

tomdecode: THEORY
BEGIN

  IMPORTING dlxtomtypes;
  dlxif: LIBRARY = "../dlxif";
  lib  : LIBRARY = "../lib";
  IMPORTING dlxif@isa, dlxif@dlxspr, lib@lib;

  tomID(Iw: registert):IDt=
    (#
      fpu    :=I_fpu(Iw),
      alu    :=I_is_alu(Iw),
      load   :=I_load(Iw),
      store  :=I_store(Iw),
      fload  :=I_fload(Iw),
      fstore :=I_fstore(Iw),
      rfe    :=I_rfe(Iw),
      movi2s :=I_movi2s(Iw),
      movs2i :=I_movs2i(Iw),
      trap   :=I_trap(Iw),
      mem    :=I_mem(Iw),
      faddsub:=I_faddsub(Iw),
      fmuldiv:=I_fmuldiv(Iw),
      fnegabs:=I_fnegabs(Iw),
      fsqrt  :=I_fsqrt(Iw),
      frem   :=I_frem(Iw),
      fmov   :=I_fmov(Iw),
      fcvt   :=I_fcvt(Iw),
      fcond  :=I_fcond(Iw),
      mi2f   :=I_mi2f(Iw),
      mf2i   :=I_mf2i(Iw),
      branch :=I_branch(Iw),
      link   :=I_link(Iw),
      jr     :=I_jr(Iw),
      jump   :=I_j(Iw),
      branch_fcc:=I_branch_fcc(Iw),
      ALU    :=I_ALU(Iw),
      shift  :=I_shift(Iw),
      illegal:=I_illegal(Iw),
      immediate:=I_immediate(Iw),
      double_dest:=fdouble_dest(Iw),
      double_src:=fdouble_src(Iw),
      Iw     :=Iw
    #);

  spr_used(A: registerindext): bool =  % valid SPR address?
    (NOT A(3) AND NOT A(4)) OR (NOT A(0) AND NOT A(1) AND NOT A(2) AND A(3) AND NOT A(4));
 
  spr_used_correct: LEMMA
    FORALL (A: registerindext):
    spr_used(A) IFF bv2nat(A)<=nspr_LAST;

  tomop(ID: IDt):
    [# op1_RS1, op1_FS1, op1_RS2, op1_FCC, op1_SA, op1_ESR,
       op2_RS2, op2_FS2, op3_RM, op4_SR,
       dest_RD, dest_FD, dest_FCC, dest_R31, dest_SA, dest_SR:bool #]=
    (#
      op1_RS1 :=ID`alu OR ID`mem OR (ID`branch AND NOT ID`branch_fcc) OR
                ID`jr OR ID`movi2s,
      op1_FS1 :=ID`fpu OR ID`mf2i OR ID`fcond,
      op1_RS2 :=ID`mi2f,
      op1_FCC :=ID`branch AND ID`branch_fcc,
      op1_SA  :=ID`movs2i,
      op1_ESR :=ID`rfe,
      op2_RS2 :=ID`ALU OR ID`shift OR ID`store,
      op2_FS2 :=ID`faddsub OR ID`fmuldiv OR ID`fcond OR ID`fstore,
      op3_RM  :=ID`fpu, %ID`faddsub OR ID`fmuldiv,
      op4_SR  :=ID`fpu OR ID`fcond, %ID`faddsub OR ID`fmuldiv OR ID`fcond,
      dest_RD :=ID`alu OR (ID`mem AND ID`load) OR ID`movs2i OR ID`mf2i,
      dest_FD :=ID`fload OR ID`fpu OR ID`mi2f,
      dest_FCC:=ID`fcond,
      dest_R31:=(ID`jump OR ID`jr) AND ID`link,
      dest_SA :=ID`movi2s,
      dest_SR :=ID`rfe
    #);

  tomIA(ID: IDt):IAt=
    LET op=tomop(ID) IN
    (#
      sop:=LAMBDA (x: below(6)):
        COND
          x=0 ->
            (# A:=IF op`op1_RS2 THEN
                    I_RS2(ID`Iw)
                  ELSIF op`op1_SA THEN
                    ID`immediate^(4,0)
                  ELSIF op`op1_FCC THEN
                    SPR_FCC
                  ELSIF op`op1_ESR THEN
                    SPR_ESR
                  ELSE
                    I_RS1(ID`Iw)
                  ENDIF,

               fprl:=op`op1_FS1 AND     (ID`double_src OR NOT I_RS1(ID`Iw)(0)),
               fprh:=op`op1_FS1 AND NOT (ID`double_src OR NOT I_RS1(ID`Iw)(0)),
               spr:=op`op1_SA AND spr_used(ID`immediate^(4,0)) OR op`op1_FCC OR op`op1_ESR,
               gpr:=op`op1_RS1 OR op`op1_RS2 #),

          x=1 ->
            (# A:=IF op`op1_RS2 THEN
                    I_RS2(ID`Iw)
                  ELSE
                    I_RS1(ID`Iw)
                  ENDIF,
               fprl:=op`op1_FS1 AND NOT (ID`double_src OR I_RS1(ID`Iw)(0)),
               fprh:=op`op1_FS1 AND     (ID`double_src OR I_RS1(ID`Iw)(0)),
               spr:=FALSE,
               gpr:=op`op1_RS1 OR op`op1_RS2 #),

          x=2 ->
            (# A:=I_RS2(ID`Iw),
               fprl:=op`op2_FS2 AND     (ID`double_src OR NOT I_RS2(ID`Iw)(0)),
               fprh:=op`op2_FS2 AND NOT (ID`double_src OR NOT I_RS2(ID`Iw)(0)),
               spr:=FALSE,
               gpr:=op`op2_RS2 #),

          x=3 ->
            (# A:=I_RS2(ID`Iw),
               fprl:=op`op2_FS2 AND NOT (ID`double_src OR I_RS2(ID`Iw)(0)),
               fprh:=op`op2_FS2 AND     (ID`double_src OR I_RS2(ID`Iw)(0)),
               spr:=FALSE,
               gpr:=FALSE #),

          x=4 ->
            (# A:=SPR_RM,
               fprl:=FALSE,
               fprh:=FALSE,
               spr:=op`op3_RM,
               gpr:=FALSE #),

          x=5 ->
            (# A:=SPR_SR,
               fprl:=FALSE,
               fprh:=FALSE,
               spr:=op`op4_SR,
               gpr:=FALSE #)
        ENDCOND,

      dest:=
        LET address=I_RD(ID`Iw) IN
        (# A   :=IF op`dest_R31 THEN
                   index31
                 ELSIF op`dest_SR THEN
                   SPR_SR
                 ELSIF op`dest_FCC THEN
                   SPR_FCC
                 ELSIF op`dest_SA THEN
                   I_immediate(ID`Iw)^(4,0)
                 ELSE
                   address
                 ENDIF,
           fprl:=op`dest_FD AND (ID`double_dest OR NOT address(0)),
           fprh:=op`dest_FD AND (ID`double_dest OR address(0)),
           spr :=(op`dest_SA AND spr_used(ID`immediate^(4,0))) OR op`dest_FCC OR op`dest_SR,
           gpr :=op`dest_R31 OR (op`dest_RD AND (address(0) OR address(1) OR
				 address(2) OR address(3) OR address(4))) #)
    #);

  dest_addr_not_mixed: LEMMA
    FORALL (Iw: registert):
    LET dest=tomIA(tomID(Iw))`dest IN
    (dest`fprl=>NOT dest`spr AND NOT dest`gpr) AND
    (dest`fprh=>NOT dest`spr AND NOT dest`gpr) AND
    (dest`spr =>NOT dest`fprl AND NOT dest`fprh AND NOT dest`gpr) AND
    (dest`gpr =>NOT dest`fprl AND NOT dest`fprh AND NOT dest`spr);

  no_dest_r0: LEMMA
    FORALL (Iw: registert):
    LET dest=tomIA(tomID(Iw))`dest IN
    NOT (dest`gpr AND bv2nat(dest`A)=0);

  source_addr_not_mixed: LEMMA
    FORALL (Iw: registert, x: below(6)):
    LET src=tomIA(tomID(Iw))`sop(x) IN
    (src`fprl=>                 NOT src`fprh AND NOT src`gpr AND NOT src`spr) AND
    (src`fprh=>NOT src`fprl                  AND NOT src`gpr AND NOT src`spr) AND
    (src`gpr =>NOT src`fprl AND NOT src`fprh                 AND NOT src`spr) AND
    (src`spr =>NOT src`fprl AND NOT src`fprh AND NOT src`gpr);

  spr_is_used : LEMMA
    FORALL (Iw: registert, x: below(6)):
    LET src=tomIA(tomID(Iw))`sop(x) IN
      src`spr IMPLIES bv2nat(src`A)<=nspr_LAST;

  spr_is_used_dest : LEMMA
    FORALL (Iw: registert):
    LET dest=tomIA(tomID(Iw))`dest IN
      dest`spr IMPLIES bv2nat(dest`A)<=nspr_LAST;

  fpr_helper : LEMMA
    FORALL (Iw:registert, x: below(6)):
    LET src=tomIA(tomID(Iw))`sop(x) IN
      (src`fprh OR src`fprl) IMPLIES 
	x<4 AND 
	tomIA(tomID(Iw))`sop(0)`A=tomIA(tomID(Iw))`sop(1)`A AND
	tomIA(tomID(Iw))`sop(2)`A=tomIA(tomID(Iw))`sop(3)`A;

  gpr_helper : LEMMA
    FORALL (Iw:registert, x: below(6)):
    LET src=tomIA(tomID(Iw))`sop(x) IN
      src`gpr IMPLIES x<3 AND 
	(x/=1 OR tomIA(tomID(Iw))`sop(0)`A=tomIA(tomID(Iw))`sop(1)`A);

  spr_helper : LEMMA
    FORALL (Iw:registert, x: below(6)):
    LET src=tomIA(tomID(Iw))`sop(x) IN
      tomIA(tomID(Iw))`sop(4)`A=SPR_RM AND
      tomIA(tomID(Iw))`sop(5)`A=SPR_SR AND
      (src`spr IMPLIES x/=1 AND x/=2 AND x/=3);

END tomdecode