Kestrel-3

Artifact 6a73cad59a4fe513994e22f93c3d777144c2c9193c2e0c3f4c9e86e49b876838:

• File cores/cpu/MStatus_formal.v — part of check-in [6074d7325c] at 2019-04-08 00:29:02 on branch trunk — Convert MSTATUS and MIE to use MemCSR (user: kc5tja size: 1251)

`default_nettype none


module MStatus_formal();
   wire [11:0] i_adr;
   wire [1:0]  i_priv;
   wire        i_ree;
   wire        i_we;
   wire [63:0] i_dat;
   wire [63:0] o_dat;
   wire        o_valid;
   wire        rst, clk;


   reg 	       z_past_valid = 0;
   always @(posedge clk)
     z_past_valid <= 1;


   MStatus dut(.i_adr(i_adr),
	       .i_priv(i_priv),
	       .i_ree(i_ree),
	       .i_we(i_we),
	       .i_dat(i_dat),
	       .o_dat(o_dat),
	       .o_valid(o_valid),
	       .rst(rst),
	       .clk(clk));


   always @(*)
     if(i_adr !== 12'h300) assert(!o_valid);

   always @(*)
     if(i_priv !== 2'h3) assert(!o_valid);

   always @(posedge clk)
     if($past(i_we) && $past(o_valid) && !$past(rst) && z_past_valid) begin
	assert(o_dat[1:0] == 2'b00);
	assert(o_dat[3:2] == $past(i_dat[3:2]));
	assert(o_dat[5:4] == 2'b00);
	assert(o_dat[7:6] == $past(i_dat[7:6]));
	assert(o_dat[8] == 1'b0);
	assert(o_dat[12:9] == $past(i_dat[12:9]));
	assert(o_dat[16:13] == 4'b0000);
	assert(o_dat[17] == $past(i_dat[17]));
	assert(o_dat[22:18] == 5'b00000);
	assert(o_dat[31:23] == $past(i_dat[31:23]));
	assert(o_dat[35:32] == 4'b0000);
	assert(o_dat[62:36] == $past(i_dat[62:36]));
	assert(o_dat[63] == 1'b0);
     end
   
endmodule