ivy/test/toma8_mc.ivy

#lang ivy1.7

type word_t
type reg_t 
type tag_t
type eu_t
type opcode = {op_alu,op_rd,op_wr,op_nop}

module st_opr = {
  var valid : bool
  var tag : tag_t
  var val : word_t
}


# an uninterpreted function to model the ALU

function f(X:word_t,Y:word_t) : word_t

object ref = {

    action step(opin : opcode,                           # opcode input
                srca:reg_t, srcb:reg_t, dst:reg_t,       # source and dest indices input
                din: word_t,                             # data input
                st_choice : tag_t,
                issue_choice : tag_t,
                issue_eu : eu_t,
                exe_valid : bool
                )

    returns (
      dout : word_t
    )

    var r(R:reg_t) : word_t        # the register file

    implement step {
        var opra : word_t;
        var oprb : word_t;
        var res : word_t;

        if opin = op_alu {
	    opra := r(srca);
	    oprb := r(srcb);
	    res := f(opra,oprb);
	    r(dst) := res;
	}
	else if opin = op_rd {
	    dout := r(srca);
	}
	else if opin = op_wr {
	    r(dst) := din;
	};

       # following doesn't belong here...

        # update the aux state (this is ghost, should not be here)

        if(opin = op_alu){
            toma.aux(st_choice).opra := opra;
            toma.aux(st_choice).oprb := oprb;
            toma.aux(st_choice).res  := res;
            toma.aux(st_choice).srca := srca;
            toma.aux(st_choice).srcb := srcb;
        }; 
        
        if (exe_valid) {
            toma.aux(issue_choice).eu := issue_eu;
        };


    }
}
  
object toma = {

   object ir(self:reg_t) = {
        var resvd : bool
        var tag : tag_t
        var val : word_t
    }
  
    object st(self:tag_t) = {
        var valid : bool
        instance opra : st_opr
        instance oprb : st_opr
        var dst : reg_t
        var issued : bool
    }

    object eu(self:eu_t) = {
        var valid : bool
        var ready : bool
        var res : word_t
        var tag : tag_t
    }


    # the auxiliary state 

    object aux(self:tag_t) = {
        var opra : word_t
        var oprb : word_t
        var res : word_t
        var srca : reg_t
        var srcb : reg_t
        var eu : eu_t
    }

    instance pout : st_opr

    after init {
        st(T).valid := false;
        ir(R).resvd := false;
        eu(E).valid := false;

        # initialize abstract model to match the implementation

        ref.r(R) := ir(R).val;
    }
    

    action step (
      opin : opcode,                           # opcode input
      srca:reg_t, srcb:reg_t, dst:reg_t,       # source and dest indices input
      din: word_t,
      st_choice : tag_t,
      issue_choice : tag_t,
      issue_eu : eu_t,
      complete_eu : eu_t
    )
    returns (
      stallout : bool,
      dout : word_t
    )
    =
    {

        var exe_rdy : bool;
        var exe_valid : bool;
        var exe_tag : tag_t;
        var exe_opra : word_t;
        var exe_oprb : word_t;

        # completion of operation in execution unit, result on pout

        pout.valid := eu(complete_eu).valid & eu(complete_eu).ready;
        pout.val := eu(complete_eu).res;
        pout.tag := eu(complete_eu).tag;
        if pout.valid {
            eu(complete_eu).valid := false
        };


        # TODO: these need to be proved

        assume pout.tag = I & pout.valid -> pout.val = aux(I).res;
        assume pout.valid -> complete_eu = aux(pout.tag).eu;

        # use pout to retire an instruction

        if(pout.valid){
            ir(R).resvd := ir(R).tag ~= pout.tag & ir(R).resvd;
            ir(R).val := (pout.val) if (ir(R).resvd & ir(R).tag = pout.tag) else (ir(R).val);

            st(T).opra.valid := st(T).opra.tag = pout.tag | st(T).opra.valid;
            st(T).opra.val := (pout.val) if ~st(T).opra.valid & st(T).opra.tag = pout.tag else st(T).opra.val;
            
            st(T).oprb.valid := st(T).oprb.tag = pout.tag | st(T).oprb.valid;
            st(T).oprb.val := (pout.val) if ~st(T).oprb.valid & st(T).oprb.tag = pout.tag else st(T).oprb.val;
            
            st(T).valid := st(T).issued & pout.tag ~= T & st(T).valid;
        };

        # stall if station is busy or read of reserved register

        stallout := opin = op_alu & st(st_choice).valid 
                    | opin = op_rd & ir(srca).resvd;

        # perform the incoming op

        if(~stallout) {
            if opin = op_alu {
	        
	        # store the instruction in an RS
	  
	        ir(dst).resvd := true;
	        ir(dst).tag := st_choice;
	        st(st_choice).valid := true;
	        st(st_choice).issued := false;
	  
	        # fetch the a operand (with bypass)
	  
	        if(pout.valid & ir(srca).resvd & pout.tag = ir(srca).tag) {
	            st(st_choice).opra.valid := true;
	            st(st_choice).opra.tag := ir(srca).tag;
	            st(st_choice).opra.val := pout.val;
	        } else {
	            st(st_choice).opra.valid := ~ir(srca).resvd;
	            st(st_choice).opra.tag := ir(srca).tag;
	            st(st_choice).opra.val := ir(srca).val;
	        };
	  
	        # fetch the b operand (with bypass) */
	  
	        if(pout.valid & ir(srcb).resvd & pout.tag = ir(srcb).tag){
	            st(st_choice).oprb.valid := true;
	            st(st_choice).oprb.tag := ir(srcb).tag;
	            st(st_choice).oprb.val := pout.val;
	        } else {
	            st(st_choice).oprb.valid := ~ir(srcb).resvd;
	            st(st_choice).oprb.tag := ir(srcb).tag;
	            st(st_choice).oprb.val := ir(srcb).val;
	        }
	    }
            else if opin = op_rd {
                dout := ir(srca).val;
            }
            else if opin = op_wr {
	        ir(dst).val := din;
	        ir(dst).resvd := false;
	    }
        };
    
        # instruction issue from station to eu

        exe_rdy := ~eu(issue_eu).valid;

        if(st(issue_choice).valid
        & st(issue_choice).opra.valid
        & st(issue_choice).oprb.valid
        & ~st(issue_choice).issued
        & exe_rdy)
        {
	    exe_valid := true;
	    st(issue_choice).issued := true;
        }
        else exe_valid := false;
        
        exe_tag  := issue_choice;
        exe_opra :=  st(issue_choice).opra.val;
        exe_oprb :=  st(issue_choice).oprb.val;
    
        # perform op in execution unit, store result

        if(~eu(issue_eu).valid){
            eu(issue_eu).valid := exe_valid;
            eu(issue_eu).res := f(exe_opra)(exe_oprb);
            eu(issue_eu).tag := exe_tag;
        };
        
        # commit the abstract operation here
        
        if ~stallout {
            var dout := ref.step(opin,srca,srcb,dst,din,st_choice,issue_choice,issue_eu,exe_valid) # ghost
        }

    }
   

    # the refinement maps 
    
    invariant st(K).valid & st(K).opra.valid -> st(K).opra.val = aux(K).opra
    proof let I = st(K).opra.tag, J = aux(K).srca, C = aux(K).opra

    invariant st(K).valid & st(K).oprb.valid -> st(K).oprb.val = aux(K).oprb
    proof let I = st(K).oprb.tag, J = aux(K).srcb, C = aux(K).oprb


    # invariant pout.tag = I & pout.valid -> pout.val = aux(I).res;
    # proof let A = aux(i).opra, B = aux(i).oprb, C = f(a,b), J = complete_eu
   
    # # noninterference lemma

    # invariant pout.valid -> complete_eu = aux(pout.tag).eu;
    # proof I = pout.tag, J = complete_eu


}

export toma.step

schema trans1 = {
    type t
    function x : t
    function z : t
    property x = X & z = X -> x = z
}

schema trans2 = {
    type t
    function x : t
    property Y = X  -> (x = X <-> x = Y)
}

schema cong1 = {
    type t
    type u
    function x : t
    function f1(X:t) : u
    property x = X -> f1(x) = f1(X)
}

schema cong2 = {
    type t1
    type t2
    type u
    function x1 : t1
    function x2 : t2
    function f1(X1:t1,X2:t2) : u
    property x1 = X1 & x2 = X2 -> f1(x1,x2) = f1(X1,X2)
}