(*--------------------------------------------------------

----------------------------------------------------------
Model of an out-of-order processor
Author : Shuvendu Lahiri (shuvendu@ece.cmu.edu)
----------------------------------------------------------


- This files checks some properties of the rob using bounded
- property checking used for the thesis
- Start state is a reset state
- Check if the impl and isa reg-files are the same after k steps


Added features :

a)
- this model gets rid of the rob.write

b)
-- While retiring, the check is_rob_empty() is put
-- before incrementing head, previously caused the
-- head to go past the tail


c)
-- when an instruction is dispatched, it looks up the reg_valid
-- field. 
-- if thats valid, it grabs the data and sets the srcvalid  to true. 
-- if not, it looks at the reg_tag(tag) entry at rob. if the valid bit 
     set, then it grabs the rob_value at that location.
-- else grabs the tag, and sets srcvalid to false


d) 2/13/02
-- added a fielf rob_active for rob entries, such that this 
-- field is true iff the instruction is currently between 
-- the current rob_head and rob_tail

-- NOTE : no < in the model now !!!! because of rob_active



* An xsmv description of the out-of-order processor description
* The model depicts the one described by Randy Bryant

-- System can alternate between three types of operations:
--   Dispatch: Read instruction and create entry in reorder buffer
--   Execute(i): Attempt to execute operation at position i in reorder buffer
--   Retire: Attempt to retire operation at head of reorder buffer
--
--     	     Flush
--	       |
--             v
--    +-----------------------+
--    |      Controller       |
--    |                       | No-Op/Dispatch/Operate/Retire
--    |        	              |------->
--    |          	      | Decoded instruction
--    |          	      |------->
--    |                       | Execution ID
--    |                       |------->
--    +-----------------------+
--
--
--    +-------------------------+     +----------------------------------+
--    |   Register/Rename       |     |  	  Reorder Buffer       	 |
--    |		 	        |     |				         |
--    |    +=======+======+     |     |   +=+=+=+=+==============+=+=+   |
--    |	   | valid | val  |     |     |   | | | | |        	 | | |   |
--    | +->|       |------|     |     |   | | | | |   . . .      | | |   |
--    | |  |       | tag  |     |     |   | | | | |              | | |   |
--    | |  +=======+======+     |     |   +=+=+=+=+==============+=+=+   |
--    | Register ID	        |     |	   ^                          ^  |
--    +-------------------------+     |    |     	       	      |  |
--				      |    +-- Head            Tail --+  |
--				      +----------------------------------+



---- Reorder Buffer Entries.  
--   All indexed by reorder buffer position
--
--   +------------+
--   |  Write     |   Should the result of this operation be written back?
--   +------------+
--   |  Valid	  |   Has this operation been executed?
--   +------------+
--   |  Dest 	  |   Destination register ID
--   +------------+
--   |  value	  |   Write Back Value
--   +------------+
--   |  Opcode	  |   Opcode for operation
--   +------------+
--   |  src1valid |   Is src1 ready?
--   +------------+
--   |  src1val   |   src1 value  
--   +------------+
--   |  src1tag   |   src1 tag
--   +------------+
--   |  src2valid |   Is src2 ready?
--   +------------+
--   |  src2val   |   src2 value 
--   +------------+
--   |  src2tag   |   src2 tag
--   +------------+




* An Auxiliary ISA has been added to check the correctness of the Impl machine.

- Shuvendu Lahiri & Sanjit Seshia
	under guidance of Prof. Randy Bryant


--------------------------------------------------------*)


MODEL OOO

MODULE OOO


	
INPUT
	(* the list of external variables to drive the simulation *)

	flush 		 : TRUTH ; (* controls the flush  *)
	isa   		 : TRUTH ; (* denotes isa mode *)
	control_dispatch : TRUTH ; (* controls the dispatch *)


VAR



	(* the ISA visible state vars *)
	instr : TERM; (* the instr mem *)
	

	(* the controller variables *)
	oper_0 	    : TRUTH ;(* 0th bit of operation *)
	oper_1 	    : TRUTH ;(* 1st bit of operation *)
	ex_id       : TERM  ;(* the id of the instr to execute *)
	n_oper_0    : TERM  ;
	n_oper_1    : TERM  ;
		

	(* the auxiliary ISA module *)
	isa_rf 		: FUNC[1];
	isa_src1	: FUNC[1];
	isa_src2	: FUNC[1];
	isa_src1val 	: FUNC[1];
	isa_src2val 	: FUNC[1];
	isa_value 	: FUNC[1];
	isa_src1tag     : FUNC[1];
	isa_src2tag     : FUNC[1];

	(* temporary variables for #defines *)
	isa_rf_0 		: FUNC[1];
	isa_src1val_0		: FUNC[1];	
	isa_src2val_0	 	: FUNC[1];
	isa_value_0		: FUNC[1];
	isa_src1tag_0 		: FUNC[1];
	isa_src2tag_0 		: FUNC[1];
	
	rob_valid_0 		: PRED[1];
	

	(* the register file *)	
	reg_valid  : PRED[1]; (* if the reg has valid data *)
	reg_val    : FUNC[1]; 	
	reg_tag    : FUNC[1];

	(* reoder buffer variables *)
	rob_head :  TERM ; (* Oldest entry *)
 	rob_tail :  TERM ; (* Where next entry should go *)

	(* each rob entry  *)
  	rob_valid 	:  PRED[1] ; 
	rob_active 	:  PRED[1] ; (* new on 2/13/02, for removing < on rob_head *)
  	rob_write 	:  PRED[1] ;
  	rob_dest	:  FUNC[1] ; 
  	rob_value	:  FUNC[1] ;
  	rob_opcode	:  FUNC[1] ;
  	rob_src1valid	:  PRED[1] ;
  	rob_src1val	:  FUNC[1] ;
	rob_src1tag	:  FUNC[1] ;
	rob_src2valid	:  PRED[1] ;
  	rob_src2val	:  FUNC[1] ;
  	rob_src2tag	:  FUNC[1] ;

	(* the #define declarations variable *)
	dest 	: TERM ;
	opcode  : TERM ;
	src1    : TERM ;
	src2    : TERM ;

	nop      : TRUTH ;
	dispatch : TRUTH ;
	execute  : TRUTH ;
	retire   : TRUTH ;

	reg_val1 : TERM ;
	reg_val2 : TERM ;

	alu_result_isa : TERM ;
	alu_result_ooo : TERM ;

	retire_match : PRED[1] ; 
	rob_instr_ready : PRED[1] ;  
	ex_src1match    : PRED[1] ;  
	ex_src2match    : PRED[1] ; 


	is_rob_full  : TRUTH ;

	(* list of predicates and truth vars for invariants *)
	Inv_A    : PRED[1];
	Inv_A1   : PRED[1];
	Inv_B1   : PRED[1];
	Inv_B2   : PRED[1];
	Inv_D    : PRED[1];
	Inv_C    : PRED[1];
	Inv_E    : PRED[1];
	Inv_F    : PRED[1];
	Inv_G    : PRED[1];
	Inv_G1   : PRED[1];
	Inv_H1   : PRED[1];
	Inv_H2   : PRED[1];
	Inv_H3   : PRED[1];
	Inv_K    : PRED[1];
	Inv_L    : PRED[1];
	Inv_Z    : PRED[1];
	Inv_range : PRED[1];

	Inv_B1_weak : PRED[1];
	Inv_B2_weak : PRED[1];
	Inv_D_weak  : PRED[1];

	Inv_1 : TRUTH ;
	Inv_2 : TRUTH ;
	Inv_3 : TRUTH ;
	Inv_4 : TRUTH ;
	Inv_5 : TRUTH ;

	Inv_new_instr_regs : TRUTH;
	Inv_delta          : TRUTH ;

	Inv : TRUTH ;


	(* some next state invariants without instantiation *)
	Inv_A_next  : PRED[1];
	Inv_A1_next : PRED[1];
	Inv_B1_next : PRED[1];
	Inv_B2_next : PRED[1];
	Inv_C_next  : PRED[1];
	Inv_D_next  : PRED[1];
	Inv_E_next  : PRED[1];
	Inv_F_next  : PRED[1];
	Inv_G_next  : PRED[1];
	Inv_G1_next  : PRED[1];
	Inv_H1_next  : PRED[1];
	Inv_H2_next  : PRED[1];
	Inv_H3_next  : PRED[1];
	Inv_K_next  : PRED[1];
	Inv_L_next  : PRED[1];


	Inv_Z_next  : PRED[1];

CONST
	(* to check the effect of interpreting succ *)
	uif_succ : FUNC[1];


	(* special init value for the don't care terms *)
	init_null_term : TERM;
	init_null_tag : TERM;
	init_null_val : TERM;
	init_null_reg : TERM;
	init_null_opcode : TERM ;
	

	(* the list of uninterpreted functions *)
	Decode_dest : FUNC[1];  
	Decode_opcode : FUNC[1];  
	Decode_src1 : FUNC[1];  
	Decode_src2 : FUNC[1];  
	New_instr : FUNC[1]; 
	New_ex_id : FUNC[1];
	Alu       : FUNC[3];

	(* to generate non-deterministic choice *)
	New_oper_0 : PRED[1];
	New_oper_1 : PRED[1];
	New_var : FUNC[1];

	(* list of uninterpreted functions for initializing *)
	init_op_0 : TRUTH ;
	init_op_1 : TRUTH ;
	init_instr : TERM ; (* initial value of instr *)
	init_ex_id : TERM ; (* initial value of ex_id *)

	
	(* for the auxiliary module *)
	init_isa_rf 		: FUNC[1];
	init_isa_src1		: FUNC[1];
	init_isa_src2		: FUNC[1];
	init_isa_src1val	: FUNC[1];	
	init_isa_src2val	: FUNC[1];
	init_isa_value		: FUNC[1];




	(* for the register file *)
	init_reg_valid : PRED[1]; 
	init_reg_val    : FUNC[1];
	init_reg_tag    : FUNC[1];

	(* for the rob module *)
	init_rob_head : TERM;
	init_rob_tail : TERM;
	init_rob_valid 	:  PRED[1] ; 

  	init_rob_write 	:  PRED[1] ;
  	init_rob_dest	:  FUNC[1] ; 
  	init_rob_value	: FUNC[1]   ;
  	init_rob_opcode	: FUNC[1]   ;
  	init_rob_src1val : FUNC[1]   ;
  	init_rob_src1tag : FUNC[1]   ;
  	init_rob_src1valid : PRED[1]   ;
  	init_rob_src2val : FUNC[1]   ;
  	init_rob_src2tag : FUNC[1]   ;
  	init_rob_src2valid : PRED[1]   ;


	init_n_oper_0 : TERM ;
	init_n_oper_1 : TERM ;


	(*argument variables for the lambda terms *)
	regid : TERM ;
	tag   : TERM ;
	i     : TERM ;
	j     : TERM ;
	r     : TERM ;
	v     : TERM ;

	addr  : TERM ;
	indx  : TERM ;
	rid   : TERM ;
	t     : TERM ;
DEFINE




	(* decode the instr *)
	dest 	:= Decode_dest(instr);
	opcode  := Decode_opcode(instr); 
	src1    := Decode_src1(instr);
	src2    := Decode_src2(instr);


	
	(* length = 3 *)
	(*is_rob_full  := (rob_tail = succ^3(rob_head));*)


	(* length = infinity *)
	is_rob_full := 0 ;


	(* decode controller output
	 * modify the controller output so that
	 * the operations can be controlled by
	 * additional variables "flush" and 
	 * "control_dispatch", and the predicate
	 * "is_rob_full()"
	 *)

	nop      := ((~oper_1) & (~oper_0)) & ~control_dispatch ;
	dispatch := (((~oper_1) & ( oper_0)) | control_dispatch) & ~is_rob_full;
	execute  := (( oper_1) & (~oper_0)) & ~control_dispatch ;
	retire   := (( oper_1) & ( oper_0)) & ~control_dispatch ;



	(* a more controlled operations *)
	(* NOT USED NOW
	op_nop 	    := (~oper_1) & (~oper_0);
	op_dispatch := (~oper_1) & ( oper_0);
	op_execute  := ( oper_1) & (~oper_0);
	op_retire   := ( oper_1) & ( oper_0);

	dispatch :=  ~is_rob_full & (op_dispatch | control_dispatch);
	execute  :=  ~dispatch & (op_execute | control_execute);
	retire   :=  ~dispatch & ~execute  & (op_retire | control_retire);
	nop      :=  ~dispatch & ~execute  & ~retire & op_nop ;	
	
	*)


	
	(* register values *)
	reg_val1 := reg_val(src1);
	reg_val2 := reg_val(src2);
	
	(* results of alu *)
	alu_result_isa := Alu(opcode, reg_val1, reg_val2);
	alu_result_ooo := Alu(rob_opcode(ex_id), rob_src1val(ex_id), rob_src2val(ex_id)); 

	
	(* rob_write is just a macro now *)
	rob_write := Lambda (tag). (reg_tag(rob_dest(tag)) = tag);


	(* retiring instr write to reg file *)
	(* check that the instr has executed *)
	retire_match := Lambda (regid). (retire & rob_valid(rob_head) & (rob_dest(rob_head) = regid));


	(* check to see if the instr is ready , note that the execute is not idempotent if we start 
	 * from an arbitrary state
	 *)
	 (* previous definition : changed on 2/13/02 by shuvendu 
	rob_instr_ready := Lambda (tag). rob_src1valid(tag) & rob_src2valid(tag) &  ~rob_valid(tag) &
		(rob_head <= tag) & (tag < rob_tail);
	*)

        rob_instr_ready := Lambda (tag). rob_src1valid(tag) & rob_src2valid(tag) &  ~rob_valid(tag) &
		 (rob_active(tag));
	

	(* check to see if the currently exec instr has matching dest *)
	(* previous definition : changed on 2/13/02 by shuvendu 
	ex_src1match    := Lambda (tag). ~(rob_src1valid(tag)) & (rob_src1tag(tag) = ex_id )
			 & rob_instr_ready(ex_id) & (rob_head <= ex_id) & (ex_id < rob_tail);
	ex_src2match    := Lambda (tag). ~(rob_src2valid(tag)) & (rob_src2tag(tag) = ex_id )
			 & rob_instr_ready(ex_id) & (rob_head <= ex_id) & (ex_id < rob_tail);
         *)
	ex_src1match    := Lambda (tag). ~(rob_src1valid(tag)) & (rob_src1tag(tag) = ex_id )
			 & rob_instr_ready(ex_id);
	ex_src2match    := Lambda (tag). ~(rob_src2valid(tag)) & (rob_src2tag(tag) = ex_id )
			 & rob_instr_ready(ex_id);



	(*----- variables to store the initial states of impl-----------*)

	rob_valid_0 := Lambda (tag). (tag < init_rob_tail) & init_rob_valid(tag);



	(*----- variables to store the initial states of isa-----------*)



	isa_src1val_0 :=  Lambda (tag).   
	case
		init_rob_src1valid(tag) : init_rob_src1val(tag);
		default : init_isa_src1val(tag);
	esac ;
	
	
	isa_src2val_0 := Lambda (tag). 
	case
		
		init_rob_src2valid(tag) : init_rob_src2val(tag);
		default : init_isa_src2val(tag);
	esac;
	

	isa_value_0 :=  Lambda (tag). 
	case
		init_rob_valid(tag) :  init_rob_value(tag);
		default : Alu(init_rob_opcode(tag), isa_src1val_0(tag), isa_src2val_0(tag));
	esac;

	isa_rf_0  := Lambda (regid). 
	case 	
		init_reg_valid(regid) : init_reg_val(regid);

		~init_reg_valid(regid) & (init_rob_valid(init_reg_tag(regid))) &( init_rob_dest(init_reg_tag(regid)) = regid ) : init_rob_value(init_reg_tag(regid));


		~init_reg_valid(regid) & ~init_rob_valid(init_reg_tag(regid)) & (init_rob_dest(init_reg_tag(regid)) = regid) : Alu(init_rob_opcode(init_reg_tag(regid)), isa_src1val_0(init_reg_tag(regid)), isa_src2val_0(init_reg_tag(regid)));


		default : init_isa_rf(regid);
	esac ;


	(*
	((((((((((((((((((((((((((((((((((((((((((((((((((((
		 INVARIANT DEFINITIONS 
	((((((((((((((((((((((((((((((((((((((((((((((((((((
	*)	

	(**************************************************)
	(* list of invariants needed  for the impl m/c    *)
	(**************************************************)



ASSIGN

	
	(*###################################*)		
	(*------CONTROLLER -----------------*)
	(*###################################*)		
	
	(* 
	 * The controller outputs the tuple 
	 * <operation, ex_id, instr> 
	 * where 
	 * (a) operation :is the next operation
	 *     {nop, dispatch, execute, retire}
	 * (b) ex_id : is the id of the instr in rob
	 *     which is next executed, constrained to 
	 *     be less than rob_tail.
	 * (c) instr : the next instruction	
	 *)
	
	(* the operation is coded by 2 bits <oper_1, oper_0>
	 * nop 		= 00
	 * dispatch 	= 01 
	 * execute      = 10
	 * retire       = 11
	 *)

	(* NOTE : now the control logic has been modified 
	 * for testing if the rob is full
	 * if the rob is full, the dispatch signal is disabled
	 *) 










	(**************IMPORTANT*****************)
	(* force the operation to alternate between
	 * execute and retire to complete all the 
	 * instructions in the rob when flush is 
	 * asserted
	 *)


	(* n_oper_0, n_oper_1 are arbitrary vars
	 * they are used to generate a new bool 
	 * value every cycle, since {1,0} is not
	 * supported for defaults
	 *)
	
	
	(*------operation : bit 0---------------*)
	init[oper_0] := 0 ; 
	next[oper_0] := case 
		flush & execute  : 1; (* retire *)
		flush & ~execute : 0; (* execute *)
		default : New_oper_0(n_oper_0);

	esac;

	(* arbitrary value generaator *)
	init[n_oper_0] := init_n_oper_0;
	next[n_oper_0] := New_var(n_oper_0);

	
	(*------operation : bit 1---------------*)
	init[oper_1] := 0 ; 
	next[oper_1] := case 
		flush & execute  : 1;(* retire *)
		flush & ~execute : 1;(* execute *)
		default : New_oper_1(n_oper_1);


	esac;	
	

	(* arbitrary value generaator *)
	init[n_oper_1] := init_n_oper_1;
	next[n_oper_1] := New_var(n_oper_1);


	(*-------- ex_id ------------------*)
	init[ex_id] := init_ex_id;
	next[ex_id] := case 
		flush : next[rob_head]; (* always execute the oldest instr  in flush mode*)
		default : New_ex_id(n_oper_0);
	esac;

	
	(*------ instruction  ----------*)
	init[instr] := init_instr;
	next[instr] := case 

		(* ISA part *)
		isa  : New_instr(instr);

		(* OOO part *)
		~isa & dispatch : New_instr(instr);

		default : instr;
	esac;






	(*###################################*)		
	(*-------REGISTER FILE -------------*)
	(*###################################*)		

	(* 
	 *  Register file also includes renaming information
 	 *  Entries indexed by register ID
	 *  valid : Is the entry data or tag?
  	 *  val	  : Value  for each register id
	 *  tag   : Tag    for each register id
	 *)



	(* --- valid bit of register file ---------*)
	(* the invariant related to reg_valid is encoded
	 * into the initial state *)	

	init[reg_valid] := Lambda(regid). 1 ; (* all valid initially *)
	next[reg_valid] := Lambda(regid).
	case 
		
		(* OOO part *)

		(*  Set to invalid if regid is destination of instruction 
		 *  being dispatched *)
		~isa & dispatch & (dest = regid) : 0;


		(* Set to valid if regid is destination of instruction 
		 * being retired, and the tag is the one stored in reg_tag(regid) 
		 *)
		~isa & retire_match(regid) & (reg_tag(regid) = rob_head) : 1;

		(* else stays the same *)
		default : reg_valid(regid);

	esac;


	(* ---- value of the register file --------*)
	init[reg_val] := Lambda(regid). (* init_reg_val(regid); *) init_null_val;
	next[reg_val] := Lambda(regid).
	case 
		(*   ISA part *)
 		isa & (regid = dest) : alu_result_isa;
		
		(* OOO part  *)
		(* Set to computed value if regid is destination of 
		 * retiring instruction,  
		 * need to check for rob_head = rob_tail, as the next 
		 * instruction in the empty rob might write into the RF
		 *)
		~isa & retire_match(regid) & ~(rob_head = rob_tail): rob_value (rob_head);
			
		
		(* else stays the same *)
		default : reg_val(regid);
	esac;
		
	(* ---- tag of the register file --------*)
	init[reg_tag] := Lambda(regid). (* init_null_tag *) 
	  init_rob_head (* repl null tag with init_rob_hd *); (* does not matter *)
	next[reg_tag] := Lambda(regid).
	case 
		(* OOO part  *)
		(* Set to tail if regid is destination of instruction 
		 * being dispatched *)
		~isa & dispatch & (dest = regid) : rob_tail;
		
		
		(* else stays the same *)
		default : reg_tag(regid);
	esac;



	(*###################################*)		
	(*----------REORDER BUFFER-----------*)
	(*###################################*)		
	

	(* diagram and fields provided at the start *)	
	(*----- head of the rob ---------*)
	init[rob_head] := init_rob_head;
	next[rob_head] := case	
		(* increment while retiring instr *)
		retire & rob_valid(rob_head) & ~(rob_head = rob_tail): succ(rob_head);

		default : rob_head;
	esac;


	(*----- tail of the rob ---------*)
	init[rob_tail] := init_rob_head; 
	next[rob_tail] := case 
		(* increment while dispatch instr *)
		 dispatch  : succ(rob_tail);

		default   : rob_tail;
	esac;

	
	(*----- valid bit of each entry--------*)	
	init[rob_valid] := Lambda (tag). 0; (* all are invalid *)
	next[rob_valid] := Lambda (tag).
	case 

		(* set when the instr is executed *)
		(* note the special constr on tag *)
		execute & (ex_id = tag) & rob_instr_ready(tag) : 1;


		(* else remain the same *)
		default : rob_valid (tag);
	esac;

	(*------ active bit : an instruction is present --------*)
	init[rob_active] := Lambda (tag). 0;
        next[rob_active] := Lambda(tag).
	case
	        (* set when an instruction is decoded *)
                 dispatch & (tag = rob_tail) : 1;
		 retire   & (tag = rob_head) & ~(rob_head = rob_tail) : 0 ;
                 default : rob_active(tag);
        esac;

	(*----- value field of each entry--------*)	
	init[rob_value] := Lambda (tag). init_null_val ; (* does not matter *)
	next[rob_value] := Lambda (tag).
	case 
		(* set when the instr is executed *)
		execute & (ex_id = tag) & rob_instr_ready(tag) : 
			Alu(rob_opcode(ex_id), rob_src1val(ex_id), rob_src2val(ex_id));

		(* else remains the same *)
		default : rob_value (tag);
	esac;	

	
	(*----- opcode field of each entry-------*)	
	init[rob_opcode] := Lambda (tag). init_null_opcode ; (* does not matter *)
	next[rob_opcode] := Lambda (tag).
	case 
		(* set when dispatch *)
		dispatch & (tag = rob_tail) : opcode ;

		(* else remain teh same *)
		default : rob_opcode (tag);
	esac;



	(*----- dest   field of each entry-------*)	
	init[rob_dest] := Lambda (tag). init_null_reg ; 
	next[rob_dest] := Lambda (tag).
	case 
		(* set when dispatch *)
		dispatch & (tag = rob_tail) : dest ;

		(* else remain teh same *)
		default : rob_dest (tag);
	esac;



 
	(*----- src1valid bit of each entry-------*)
	init[rob_src1valid] := Lambda (tag). 0;
	next[rob_src1valid] := Lambda (tag).
	case

		(* while dispatch, check the status of src1 reg in reg_vt *)
		dispatch & (tag = rob_tail) : (reg_valid(src1) | rob_valid(reg_tag(src1)));

		(* currently exec instr has matching dest *)
		execute & ex_src1match(tag) : 1 ;

	
		default : rob_src1valid (tag);
	esac;


	(*----- src2valid bit of each entry-------*)
	init[rob_src2valid] := Lambda (tag). 0;
	next[rob_src2valid] := Lambda (tag).
	case

		(* while dispatch, check the status of src2 reg in reg_vt *)
		dispatch & (tag = rob_tail) : (reg_valid(src2) | rob_valid(reg_tag(src2)));

		(* currently exec instr has matching dest *)
		execute & ex_src2match(tag) : 1 ;

	
		default : rob_src2valid (tag);
	esac;



	
	(*----- src1val field of each entry-------*)	
	init[rob_src1val] := Lambda (tag) . init_null_val ;
	next[rob_src1val] := Lambda (tag) .
	case
		(* dispatch instr: get entry from reg file *) 
		dispatch  & (tag = rob_tail) & reg_valid(src1) : reg_val(src1);
	

		(* dispatch and the producer is valid *)
		dispatch & (tag = rob_tail) & rob_valid(reg_tag(src1)) : rob_value(reg_tag(src1));

		(* currently exec instr has matching dest *)
		execute & ex_src1match(tag) : alu_result_ooo;

	
		default : rob_src1val(tag);
	esac;


	(*----- src1tag field of each entry-------*)	
	init[rob_src1tag] := Lambda (tag) . (* init_null_tag *) 
	  init_rob_head (* repl null tag with init_rob_hd *);
	next[rob_src1tag] := Lambda (tag) .
	case
	
		(* dispatch instr: get entry from reg file *)
		dispatch & (tag = rob_tail) : reg_tag(src1);


		default : rob_src1tag(tag);
	esac;



	(*----- src2val field of each entry-------*)	
	init[rob_src2val] := Lambda (tag) . init_null_val;
	next[rob_src2val] := Lambda (tag) .
	case
		(* dispatch instr: get entry from reg file *)
		dispatch & (tag = rob_tail) & reg_valid(src2) : reg_val(src2);	

		(* dispatch and the producer is valid *)
		dispatch & (tag = rob_tail) & rob_valid(reg_tag(src2)) : rob_value(reg_tag(src2));

	
		(* currently exec instr has matching dest *)
		execute & ex_src2match(tag) : alu_result_ooo;

		default : rob_src2val(tag);
	      esac;


	(*----- src2tag field of each entry-------*)	
        init[rob_src2tag] := Lambda (tag) . (* init_null_tag *) 
            init_rob_head (* repl null tag with init_rob_hd *);
	next[rob_src2tag] := Lambda (tag) .
	case
	
		(* dispatch instr: get entry from reg file *)
		dispatch & (tag = rob_tail) : reg_tag(src2); 

		default : rob_src2tag(tag);
	esac;



	(*###################################*)		
	(*-------ISA  MODULE -------------*)
	(*###################################*)		

	(* 
	 * This module helps to preserve the correctness
	 * between the Impl and ISA module. It contains
   	 * a RF, and an rob like list indexed by the same
	 * tag that indexes into rob
	 *)

	(* whenever an instr is dispatched in the impl m/c
	 * the isa module keeps a note of the correct values
	 *)

	(* the isa register  file   *)
	init[isa_rf] := Lambda (regid). (* init_reg_val(regid);*) init_null_val;
	next[isa_rf] := Lambda (regid). 
	case
		dispatch & (regid = dest) : Alu(opcode, isa_rf(src1), isa_rf(src2));
		default : isa_rf(regid);
	esac;



	(* src1val *)
	init[isa_src1val] := Lambda (tag). init_null_val;
	(* 
	case
		(* Invariant E*)
		init_rob_src1valid(tag) : init_rob_src1val(tag);
		default : init_isa_src1val(tag);
	esac ;
	*)
	next[isa_src1val] := Lambda (tag).
	case
		dispatch & (tag = rob_tail) : isa_rf(src1);
		default : isa_src1val(tag);
	esac ;	


	(* src2val *)
	init[isa_src2val] := Lambda (tag). init_null_val;
	(* 
	case
		(* Invariant F *)
		init_rob_src2valid(tag) : init_rob_src2val(tag);
		default : init_isa_src2val(tag);
	esac;
	*)				
	next[isa_src2val] := Lambda (tag).
	case
		dispatch & (tag = rob_tail) : isa_rf(src2);
		default : isa_src2val(tag);
	esac ;	

	(* value *)
	init[isa_value] := Lambda (tag). init_null_val;
	(*
	case
		(* Invariant G *)
		init_rob_valid(tag) :  init_rob_value(tag);

		(* Invariant G1 *)
		default : Alu(init_rob_opcode(tag), isa_src1val_0(tag), isa_src2val_0(tag));
		
	esac;
	*)
	next[isa_value] := Lambda (tag).
	case
		dispatch & (tag = rob_tail) : Alu(opcode, isa_rf(src1), isa_rf(src2));
		default : isa_value(tag);
	esac ;	



	

SPEC


CONTROL

EXTVAR

flush : TRUTH := 0  ;
isa   : TRUTH := 0  ;
control_dispatch : TRUTH := 0 ;


STOREVAR

(* store the register files *)
rf_I1 : FUNC[1];
rf_S0 : FUNC[1];
rf_S1 : FUNC[1];

rob_tail_I0 : TERM;
rob_tail_I1 : TERM;

VAR 
Inv_unique_reg_tags : PRED[2];
Inv_correct_value : TRUTH;

InvA : PRED[1];
InvD : PRED[1];

CONST
t : TERM ;
addr : TERM;
r   : TERM;
r1   : TERM;
r2   : TERM;

DEFINE

(* invariant A in fmcad paper *)
InvA := Lambda(t). (OOO.rob_valid(t) => OOO.rob_src1valid(t));

(* invariant D *)
InvD := Lambda(r). (~OOO.reg_valid(r) => OOO.rob_dest(OOO.reg_tag(r)) = r) ;

(* define the invariant about uniqueness of reg-tags *)
Inv_unique_reg_tags := Lambda (r1, r2) . ( ~(r1 = r2) & ~OOO.reg_valid(r1) & ~OOO.reg_valid(r2)) => ~( OOO.reg_tag(r1) = OOO.reg_tag(r2));

(* check to see if the value retired is the value to be  *)
(* computed in that cycle                                *)

Inv_correct_value := 
  (OOO.retire & (OOO.rob_head < OOO.rob_tail) & OOO.rob_valid(OOO.rob_head)) =>
  (OOO.rob_value(OOO.rob_head) = OOO.isa_value(OOO.rob_head));
 


EXEC



(******** plain old invariant checking **********)


simulate(12);

(* results are present in the thesis  *)
decide(OOO.reg_valid(addr) => (OOO.reg_val(addr) = OOO.isa_rf(addr)));