%
% Specification of a DLX with
%  - floating point unit
%  - generic memory interface that allows for virtual memory
%
% (C) 2000-2001 Daniel Kroening
%

dlxifspec[(IMPORTING fpu_spec)fpu_spec:fpu_spec_t]: THEORY
  BEGIN

    pipetheory: LIBRARY = "../pipetheory";
    dlxalu    : LIBRARY = "../dlxalu";

    IMPORTING dlxif_conft, isa,
              nextpc_spec, dlxifinit,
              pipetheory@mathmtimet,dlxalu@dlxalu_spec;

    %
    % external signals
    %

%  sbeyer: external interrupts as a function of the configuration are rubbish
%
%    ex_t: TYPE = bvec[19];
%    ex_0: ex_t = LAMBDA (i: below(19)): FALSE;
%
%    ex: [dlx_conft->ex_t];
 
    %
    % internal signals
    %

    imal(dlx_conf: dlx_conft):bool=
      imem_spec_imal(dlx_conf`mem, dlx_conf`DPC);

    ipf(dlx_conf: dlx_conft):bool=
      imem_spec_ipf(dlx_conf`mem, dlx_conf`DPC);

    %
    % Shorthands
    % 

    % Instruction word of an instruction

    Iw(dlx_conf: dlx_conft):registert=
      IF imal(dlx_conf) OR ipf(dlx_conf) THEN
       	r0
      ELSE
        imem_spec_load(dlx_conf`mem, dlx_conf`DPC)
      ENDIF;

    % integer operands

    op1(dlx_conf: dlx_conft):registert=
      LET Iw=Iw(dlx_conf) IN
      IF I_RS1(Iw)=index0 THEN r0 ELSE dlx_conf`GPR(I_RS1(Iw)) ENDIF;

    op2(dlx_conf: dlx_conft):registert=
      LET Iw=Iw(dlx_conf) IN
        LET a=IF I_store(Iw) THEN I_RD(Iw) ELSE I_RS2(Iw)
              ENDIF IN
        IF a=index0 THEN r0 ELSE dlx_conf`GPR(a) ENDIF;

    % ALU result

    ALU(dlx_conf: dlx_conft):[# result: registert, ovf: bool #]=
      LET Iw=Iw(dlx_conf),
          op1=op1(dlx_conf), 
          op2=IF I_ALU(Iw) OR I_shift(Iw) THEN
                op2(dlx_conf)
              ELSE
                I_immediate(Iw)
              ENDIF
          IN ALUf_spec(op1, op2, ALUfunction(Iw));
 
    % data memory exceptions

    dmal(dlx_conf: dlx_conft):bool=
      LET Iw=Iw(dlx_conf) IN
      I_mem(Iw) AND dmem_spec_dmal(dlx_conf`mem, op1(dlx_conf), Iw);

    dpf(dlx_conf: dlx_conft):bool=
      LET Iw=Iw(dlx_conf) IN
      I_mem(Iw) AND dmem_spec_dpf(dlx_conf`mem, op1(dlx_conf), Iw);

    % floating point operand with address a, embedding with zeros

    fop(dlx_conf: dlx_conft, a: registerindext):double=
      LET Iw=Iw(dlx_conf) IN
      IF fdouble_src(Iw) THEN
        dlx_conf`FPRh(a^(4,1)) o
        dlx_conf`FPRl(a^(4,1))
      ELSE
        IF a(0) THEN
          dlx_conf`FPRh(a^(4,1)) o dlx_conf`FPRh(a^(4,1))
        ELSE
          dlx_conf`FPRl(a^(4,1)) o dlx_conf`FPRl(a^(4,1))
        ENDIF
      ENDIF;

    % first floating point operand
      
    fop1(dlx_conf: dlx_conft):double=
      LET Iw=Iw(dlx_conf) IN
      IF I_mi2f(Iw) THEN % operand from GPR?
        op1(dlx_conf) o op1(dlx_conf)
      ELSE
        fop(dlx_conf, I_RS1(Iw))
      ENDIF;

    % second floating point operand

    fop2(dlx_conf: dlx_conft):double=
      LET Iw=Iw(dlx_conf) IN
      fop(dlx_conf, I_RS2(Iw));

    % FPU result

    FPU(dlx_conf: dlx_conft):
      [# result: double, exceptions: registert #]=
      LET Iw  =Iw(dlx_conf),
	  fop1=IF I_mi2f(Iw) THEN
		 op2(dlx_conf) o op2(dlx_conf)
	       ELSE
		 fop1(dlx_conf)
	       ENDIF,
          x=fpu_spec(fop1, fop2(dlx_conf),
               		dlx_conf`SPR(SPR_RM)^(1,0),
               		dlx_conf`SPR(SPR_SR)^(12,7),
               		Iw) IN
    % sbeyer 12.11: FPU result embedding would NOT REALLY HURT...
    % (ok, in fact its actually buggy without result embedding)
	(# result     := IF x`double THEN 
			   x`result
			 ELSE
			   x`result^(63,32) o x`result^(63,32)
			 ENDIF,
	   exceptions := map_CA(x`exceptions) #);

    % cause register

    CA(dlx_conf: dlx_conft):registert=
      LET Iw=Iw(dlx_conf),
          op1=op1(dlx_conf), 
          op2=op2(dlx_conf) IN
      LAMBDA (i:below(32)):
        COND
          i=0  -> FALSE,
          i=1  -> I_illegal(Iw),
          i=2  -> imal(dlx_conf) OR dmal(dlx_conf), 
          i=3  -> ipf(dlx_conf),
          i=4  -> dpf(dlx_conf),
          i=5  -> I_trap(Iw),
       	% sbeyer: on ipf or imal, Iw is forced to r0=I_shifti=I_is_alu
	%	   which should not produce an additional interrupt
          i=6  -> NOT imal(dlx_conf) AND NOT ipf(dlx_conf) AND 
		  I_is_alu(Iw) AND ALU(dlx_conf)`ovf,
          i>=7 AND i<=12 -> (I_fpu(Iw) OR I_fcond(Iw) OR I_mf2i(Iw) OR I_mi2f(Iw)) AND 
				FPU(dlx_conf)`exceptions(i),
          ELSE -> FALSE %ex(dlx_conf)(i-13)
        ENDCOND;

    % masked cause register

    MCA(dlx_conf: dlx_conft):registert=
      LAMBDA (i:below(32)):
        LET CA=CA(dlx_conf) IN
          IF i>=6 AND i/=12 THEN
            CA(i) AND dlx_conf`SPR(SPR_SR)(i)
          ELSE 
            CA(i) 
          ENDIF;

    % JISR - interrupt?

    JISR(dlx_conf: dlx_conft):bool=
      EXISTS (i:below(32)): MCA(dlx_conf)(i);

    % EData in case of an interrupt

    EData(dlx_conf: dlx_conft):registert=
      LET Iw=Iw(dlx_conf),
          op1=op1(dlx_conf) IN
% sbeyer: EData in case of /JISR does not hurt, but eases proof
%      IF JISR(dlx_conf) THEN
        IF imal(dlx_conf) OR ipf(dlx_conf) THEN
          dlx_conf`DPC
        ELSIF I_trap(Iw) THEN
          I_immediate(Iw)
        ELSIF I_mem(Iw) THEN
          dmem_spec_EA(dlx_conf`mem, op1, Iw)
        ELSIF I_fpu(Iw) OR I_fcond(Iw) OR I_mf2i(Iw) OR I_mi2f(Iw) THEN
	  FPU(dlx_conf)`result^(63,32)
	ELSE
          r0
        ENDIF;
 %     ELSE
 %       r0
 %     ENDIF;

    % interrupt level

    il(dlx_conf: dlx_conft):below(32)=
      IF JISR(dlx_conf) THEN
        min(MCA(dlx_conf))
      ELSE
        0
      ENDIF;

    % interrupt of type repeat?

    repeat(dlx_conf: dlx_conft):bool=
      il(dlx_conf)<5;

    % new value for SPR registers without exception

    SPRu(dlx_conf: dlx_conft):registerfilet=
      LET Iw=Iw(dlx_conf) IN
      LAMBDA (r: registerindext):
      IF I_rfe(Iw) AND r=SPR_SR THEN
        dlx_conf`SPR(SPR_ESR)
      ELSIF I_movi2s(Iw) AND 
            r=I_immediate(Iw)^(4,0) AND
            bv2nat(r)<=nspr_LAST THEN
        op1(dlx_conf)
      ELSIF I_fcond(Iw) AND r=SPR_FCC THEN
        FPU(dlx_conf)`result^(31,0)
      ELSE
        dlx_conf`SPR(r)
      ENDIF;

    % new value for DPC/PCp without exception

    nextDPCu(dlx_conf: dlx_conft):registert=
      LET Iw=Iw(dlx_conf) IN  % shorthands
      IF I_rfe(Iw) THEN 
        dlx_conf`SPR(SPR_EDPC)
      ELSE
        dlx_conf`PCp
      ENDIF;

    nextPCpu(dlx_conf: dlx_conft):registert=
      LET Iw=Iw(dlx_conf),    % shorthands
          op=IF I_branch(Iw) AND I_branch_fcc(Iw) THEN
               dlx_conf`SPR(SPR_FCC)
             ELSE
               op1(dlx_conf) % from GPR
             ENDIF IN
      dlxispec_nextpc(Iw, op, dlx_conf`PCp, dlx_conf`SPR(SPR_EPC));
 
    % transition function

    dlx_step(dlx_conf: dlx_conft): dlx_conft = 
      LET Iw =Iw(dlx_conf),    % shorthands
          op1=op1(dlx_conf), 
          op2=op2(dlx_conf) IN
      (#
        DPC:=IF JISR(dlx_conf) THEN SISR     ELSE nextDPCu(dlx_conf) ENDIF,
        PCp:=IF JISR(dlx_conf) THEN SISRnext ELSE nextPCpu(dlx_conf) ENDIF,

        GPR:=
	  % sbeyer 08.10:
          % do nothing for repeat interrupt!!!
	  % 
	  IF JISR(dlx_conf) AND repeat(dlx_conf) THEN
	    dlx_conf`GPR
          %
          % jump instructions
          %
	  ELSIF (I_j(Iw) OR I_jr(Iw)) AND I_link(Iw) THEN
            dlx_conf`GPR WITH [(index31):=dlx_conf`PCp+r4]
          %
          % ALU instructions
          %
          ELSIF I_is_alu(Iw) AND (I_RD(Iw)/=index0) THEN
            dlx_conf`GPR WITH [(I_RD(Iw)):=ALU(dlx_conf)`result]
          %
          % movs2i
          %
          ELSIF I_movs2i(Iw) AND (I_RD(Iw)/=index0) THEN
            dlx_conf`GPR WITH [(I_RD(Iw)):=
            LET SA=I_immediate(Iw)^(4,0) IN
            IF bv2nat(SA)<=nspr_LAST THEN
              dlx_conf`SPR(SA)
            ELSE
              r0
            ENDIF]
          %
          % Memory instructions
          %
          ELSIF I_mem(Iw) AND I_load(Iw) AND (I_RD(Iw)/=index0) THEN
            dlx_conf`GPR WITH [(I_RD(Iw)):=
              dmem_spec_load(dlx_conf`mem, op1, Iw)^(31,0)] 
          %
          % move float -> GPR
          %
          ELSIF I_mf2i(Iw) AND (I_RD(Iw)/=index0) THEN
            dlx_conf`GPR WITH [(I_RD(Iw)):=FPU(dlx_conf)`result^(31,0)]
          %
          % anyting other
          %
          ELSE
            dlx_conf`GPR
          ENDIF,
        %
        mem:=IF I_mem(Iw) AND I_store(Iw) AND
                NOT (JISR(dlx_conf) AND repeat(dlx_conf)) THEN
               mem_spec_trans(dlx_conf`mem, op1, Iw,
                              zero_extend(64)(op2(dlx_conf)))
             ELSIF I_mem(Iw) AND I_fstore(Iw) AND
                NOT (JISR(dlx_conf) AND repeat(dlx_conf)) THEN
               mem_spec_trans(dlx_conf`mem, op1, Iw, fop2(dlx_conf))
             ELSE
               dlx_conf`mem
             ENDIF,

        SPR:=
          LET SPRu=SPRu(dlx_conf) IN
          IF JISR(dlx_conf) THEN  % SPR transition in case of an interrupt
            LAMBDA (r: registerindext):
            COND
              r=SPR_SR   ->r0,
              r=SPR_ESR  ->IF repeat(dlx_conf) THEN dlx_conf`SPR(SPR_SR) ELSE SPRu(SPR_SR) ENDIF,
              r=SPR_ECA  ->MCA(dlx_conf),
              r=SPR_EPC  ->IF repeat(dlx_conf) THEN dlx_conf`PCp ELSE nextPCpu(dlx_conf) ENDIF,
              r=SPR_EDPC ->IF repeat(dlx_conf) THEN dlx_conf`DPC ELSE nextDPCu(dlx_conf) ENDIF,
              r=SPR_EData->EData(dlx_conf),
              ELSE -> IF repeat(dlx_conf) THEN 
			dlx_conf`SPR(r)
		      ELSE
			SPRu(r)
		      ENDIF
            ENDCOND
          ELSE
            SPRu % SPR transition without interrupt
          ENDIF,

        FPRl:=
	  % sbeyer 08.10:
          % do nothing for repeat interrupt!!!
	  % 
	  IF JISR(dlx_conf) AND repeat(dlx_conf) THEN
	    dlx_conf`FPRl
	  ELSIF I_fpu(Iw) OR I_mi2f(Iw) OR I_fload(Iw)  THEN
            LET result=IF I_fload(Iw) THEN
                         dmem_spec_load(dlx_conf`mem, op1, Iw)
                       ELSE
                         FPU(dlx_conf)`result
                       ENDIF IN
            IF fdouble_dest(Iw) OR NOT I_RD(Iw)(0) THEN
              dlx_conf`FPRl WITH [(I_RD(Iw)^(4,1)):=result^(31,0)]
            ELSE
              dlx_conf`FPRl
            ENDIF
          ELSE
            dlx_conf`FPRl
          ENDIF,

        FPRh:=
	  % sbeyer 08.10:
          % do nothing for repeat interrupt!!!
	  % 
	  IF JISR(dlx_conf) AND repeat(dlx_conf) THEN
	    dlx_conf`FPRh
	  ELSIF I_fpu(Iw) OR I_mi2f(Iw) OR I_fload(Iw) THEN
            LET result=IF I_fload(Iw) THEN
                         dmem_spec_load(dlx_conf`mem, op1, Iw)
                       ELSE
                         FPU(dlx_conf)`result
                       ENDIF IN
            IF fdouble_dest(Iw) OR I_RD(Iw)(0) THEN
              dlx_conf`FPRh WITH [(I_RD(Iw)^(4,1)):=result^(63,32)]
            ELSE
              dlx_conf`FPRh
            ENDIF
          ELSE
            dlx_conf`FPRh
          ENDIF
      #);

    dlx_step_without_interrupt(dlx_conf: dlx_conft): dlx_conft = 
      LET Iw =Iw(dlx_conf),    % shorthands
          op1=op1(dlx_conf), 
          op2=op2(dlx_conf) IN
      (#
        DPC:=nextDPCu(dlx_conf),
        PCp:=nextPCpu(dlx_conf),

        GPR:=
          %
          % jump instructions
          %
          IF (I_j(Iw) OR I_jr(Iw)) AND I_link(Iw) THEN
            dlx_conf`GPR WITH [(index31):=dlx_conf`PCp+r4]
          %
          % ALU instructions
          %
          ELSIF I_is_alu(Iw) AND (I_RD(Iw)/=index0) THEN
            dlx_conf`GPR WITH [(I_RD(Iw)):=ALU(dlx_conf)`result]
          %
          % movs2i
          %
          ELSIF I_movs2i(Iw) AND (I_RD(Iw)/=index0) THEN
            dlx_conf`GPR WITH [(I_RD(Iw)):=
            LET SA=I_immediate(Iw)^(4,0) IN
            IF bv2nat(SA)<=nspr_LAST THEN
              dlx_conf`SPR(SA)
            ELSE
              r0
            ENDIF]
          %
          % Memory instructions
          %
          ELSIF I_mem(Iw) AND I_load(Iw) AND (I_RD(Iw)/=index0) THEN
            dlx_conf`GPR WITH [(I_RD(Iw)):=
              dmem_spec_load(dlx_conf`mem, op1, Iw)^(31,0)] 
          %
          % move float -> GPR
          %
          ELSIF I_mf2i(Iw) AND (I_RD(Iw)/=index0) THEN
            dlx_conf`GPR WITH [(I_RD(Iw)):=FPU(dlx_conf)`result^(31,0)]
          %
          % anyting other
          %
          ELSE
            dlx_conf`GPR
          ENDIF,
        %
        mem:=IF I_mem(Iw) AND I_store(Iw) THEN
               mem_spec_trans(dlx_conf`mem, op1, Iw,
                              zero_extend(64)(op2(dlx_conf)))
             ELSIF I_mem(Iw) AND I_fstore(Iw) THEN
               mem_spec_trans(dlx_conf`mem, op1, Iw, fop2(dlx_conf))
             ELSE
               dlx_conf`mem
             ENDIF,

        SPR:=SPRu(dlx_conf),

        FPRl:=IF I_fpu(Iw) OR I_mi2f(Iw) OR I_fload(Iw) THEN
                LET result=IF I_fload(Iw) THEN
                             dmem_spec_load(dlx_conf`mem, op1, Iw)
                           ELSE
                             FPU(dlx_conf)`result
                           ENDIF IN
                IF fdouble_dest(Iw) OR NOT I_RD(Iw)(0) THEN
                  dlx_conf`FPRl WITH [(I_RD(Iw)^(4,1)):=result^(31,0)]
                ELSE
                  dlx_conf`FPRl
                ENDIF
              ELSE
                dlx_conf`FPRl
              ENDIF,

        FPRh:=IF I_fpu(Iw) OR I_mi2f(Iw) OR I_fload(Iw) THEN
                LET result=IF I_fload(Iw) THEN
                             dmem_spec_load(dlx_conf`mem, op1, Iw)
                           ELSE
                             FPU(dlx_conf)`result
                           ENDIF IN
                IF fdouble_dest(Iw) OR I_RD(Iw)(0) THEN
                  dlx_conf`FPRh WITH [(I_RD(Iw)^(4,1)):=result^(63,32)]
                ELSE
                  dlx_conf`FPRh
                ENDIF
              ELSE
                dlx_conf`FPRh
              ENDIF
      #);

    dlx_step_without_interrupt_IEEEf(dlx_conf: dlx_conft): dlx_conft = 
      LET dlx_step=dlx_step_without_interrupt(dlx_conf) IN
	IF I_fpu(Iw(dlx_conf)) OR I_fcond(Iw(dlx_conf)) OR 
	    I_mf2i(Iw(dlx_conf)) OR I_mi2f(Iw(dlx_conf)) THEN
	  dlx_step WITH [(SPR):=       
	    LAMBDA (r: registerindext):
              IF r=SPR_IEEEf  THEN
		dlx_step`SPR(r)^(31,5) o
        	(dlx_step`SPR(r)^(4,0) OR FPU(dlx_conf)`exceptions^(11,7))
	      ELSE
		dlx_step`SPR(r)
	      ENDIF]
	ELSE
	  dlx_step
	ENDIF;

    initial_conf?(dlx_conf: dlx_conft):bool =
      dlx_conf`DPC=SISR AND
      dlx_conf`PCp=SISRnext AND
      dlx_conf`SPR=initialSPR;

    dlx_step_IEEEf(dlx_conf: dlx_conft): dlx_conft = 
      LET dlx_step=dlx_step(dlx_conf) IN
	IF (I_fpu(Iw(dlx_conf)) OR I_fcond(Iw(dlx_conf)) OR 
	    I_mf2i(Iw(dlx_conf)) OR I_mi2f(Iw(dlx_conf))) AND NOT (JISR(dlx_conf) AND repeat(dlx_conf)) THEN
	  dlx_step WITH [(SPR):=       
	    LAMBDA (r: registerindext):
              IF r=SPR_IEEEf  THEN
		dlx_step`SPR(r)^(31,5) o
        	(dlx_step`SPR(r)^(4,0) OR FPU(dlx_conf)`exceptions^(11,7))
	      ELSE
		dlx_step`SPR(r)
	      ENDIF]
	ELSE
	  dlx_step
	ENDIF;

    dlx_step_without_interrupt_correct : LEMMA
    FORALL (dlx_conf: dlx_conft):
      NOT JISR(dlx_conf) IMPLIES
	dlx_step_IEEEf(dlx_conf)=dlx_step_without_interrupt_IEEEf(dlx_conf);

    dlx_conf(init_conf:dlx_conft, T: mathmtimet): RECURSIVE dlx_conft =
      IF T=0 THEN
        init_conf
      ELSE 
        dlx_step(dlx_conf(init_conf,T-1))
      ENDIF
      MEASURE T;

    dlx_conf_without_interrupt(init_conf:dlx_conft, T: mathmtimet): RECURSIVE dlx_conft =
      IF T=0 THEN
        init_conf
      ELSE 
        dlx_step_without_interrupt(dlx_conf_without_interrupt(init_conf,T-1))
      ENDIF
      MEASURE T;

    dlx_conf_without_interrupt_IEEEf(init_conf:dlx_conft,T: mathmtimet): RECURSIVE dlx_conft =
      IF T=0 THEN
        init_conf
      ELSE 
        dlx_step_without_interrupt_IEEEf(dlx_conf_without_interrupt_IEEEf(init_conf,T-1))
      ENDIF
      MEASURE T;

    dlx_conf_IEEEf(init_conf:dlx_conft,T: mathmtimet): RECURSIVE dlx_conft =
      IF T=0 THEN
        init_conf
      ELSE 
        dlx_step_IEEEf(dlx_conf_IEEEf(init_conf,T-1))
      ENDIF
      MEASURE T;

    dlx_conf_without_interrupt_correct : LEMMA
    FORALL (init_conf: dlx_conft,
	    T        : nat):
      (FORALL (Tp:below(T)): NOT JISR(dlx_conf_without_interrupt_IEEEf(init_conf,Tp))) IMPLIES
	dlx_conf_IEEEf(init_conf,T)=dlx_conf_without_interrupt_IEEEf(init_conf,T);

    dlx_conf_equal : LEMMA
      FORALL (T:nat, init_conf:dlx_conft):
	FORALL (Tp:upfrom(T)):
	  dlx_conf_IEEEf(init_conf,Tp)=
	  dlx_conf_IEEEf(dlx_conf_IEEEf(init_conf,T),Tp-T);

    dlx_conf_spr_helper : LEMMA
      FORALL (T:nat, init_conf:dlx_conft):
	dlx_conf_IEEEf(init_conf,T)`SPR=
	LAMBDA (x:bvec[5]):IF bv2nat(x)<=nspr_LAST THEN
				dlx_conf_IEEEf(init_conf,T)`SPR(x)
			   ELSE
				init_conf`SPR(x)
			   ENDIF;

    predicates : LIBRARY = "../predicates";

% now for the self-modifying businwess..
    IMPORTING predicates@predicates;

% is_write_to_adr denotes that a dlx configuration writes an address adr
    is_write_to_adr?(adr: registert)(dlx_conf: dlx_conft): bool=
	LET Iw=Iw(dlx_conf) IN
	  (I_store(Iw) OR I_fstore(Iw)) AND
	  dmem_spec_EA(dlx_conf`mem,op1(dlx_conf),Iw)^(31,3)=adr^(31,3);

% we want any fetch that was preceded by a write to the fetched address
% to be preceeded by a sync instruction (after last write, of course...)
    synced_code?(init_conf : dlx_conft,
		 state_func:[nat->dlx_conft]): bool=
      FORALL (T:nat):
	LET adr=state_func(T)`DPC IN
	exists_last_pred?[dlx_conft,is_write_to_adr?(adr)](state_func)(T) IMPLIES
	  LET last=last_pred_before[dlx_conft,is_write_to_adr?(adr)](state_func)(T) IN
	  EXISTS (Tp:subrange(last+1,T-1)):
	    I_sync(Iw(state_func(Tp)));

% for a machine with interrupts, we don't need any sync instrucion
% over a jump to the ISR, i.e.,
% we only need synced code without interrupt, but from all starting
% configurations reached by the next state function with interrupts
%
% later on, one wants to have a separate predicate for the ISR,
% but this will do for now
    synced_code_with_interrupt?(init_conf : dlx_conft): bool=
      FORALL (T:nat):
	LET conf=dlx_conf_IEEEf(init_conf,T) IN
	synced_code?(conf, LAMBDA(n:nat):dlx_conf_without_interrupt_IEEEf(conf,n));

  END dlxifspec