Add (currently failing) trap entry property. Fails when an IRQ arrives during a load/store data phase which subsequently excepts.

hdl/hazard3_csr.v

@@ -1052,8 +1052,9 @@ assign mcause_irq_next = !exception_req_any;
 assign mcause_code_next = exception_req_any ? {2'h0, except} : mcause_irq_num;
 
 // ----------------------------------------------------------------------------
+// Properties
 
-`ifdef RISCV_FORMAL
+`ifdef FORMAL
 
 // Keep track of whether we are in a trap (only for formal property purposes)
 reg in_trap;
@@ -1066,31 +1067,47 @@ always @ (posedge clk or negedge rst_n)
 			&& !(trap_enter_vld && trap_enter_rdy && except == EXCEPT_MRET);
 
 always @ (posedge clk) begin
+`ifdef RISCV_FORMAL
 	// Assume there are no nested exceptions, to stop riscv-formal from doing
 	// annoying things like stopping instructions from retiring by repeatedly
 	// feeding in invalid instructions
-
 	if (in_trap)
-		assume(except == EXCEPT_NONE);
+		assume(except == EXCEPT_NONE || except == EXCEPT_MRET);
 
 	// Assume IRQs are not deasserted on cycles where exception entry does not
 	// take place
-
 	if (!trap_enter_rdy)
 		assume(~|(irq_r & ~irq));
+`endif
 
 	// Make sure CSR accesses are flushed
 	if (trap_enter_vld && trap_enter_rdy)
 		assert(!(wen || ren));
-	// Something is screwed up if this happens
+
+	// Writing to CSR on cycle after trap entry -- should be impossible, a CSR
+	// access instruction should have been flushed or moved down to stage 3, and
+	// no fetch could have arrived by now
 	if ($past(trap_enter_vld && trap_enter_rdy))
 		assert(!wen);
-	// Should be impossible to get into the trap and exit it so quickly:
+
+	// Should be impossible to get into the trap and exit immediately:
 	if (in_trap && !$past(in_trap))
 		assert(except != EXCEPT_MRET);
-	// Should be impossible to get to another mret so soon after exiting:
-	assert(!(except == EXCEPT_MRET && $past(except == EXCEPT_MRET)));
 
+	// Should be impossible to get to another mret so soon after exiting:
+	if ($past(except == EXCEPT_MRET && trap_enter_vld && trap_enter_rdy))
+		assert(except != EXCEPT_MRET);
+
+	// Must be impossible to enter two traps on consecutive cycles. Most importantly:
+	//
+	// - IRQ -> Except: no new instruction could have been fetched by this point,
+	//   and an exception by e.g. a left-behind store data phase would sample the
+	//   wrong PC.
+	//
+	// - Except -> IRQ: would need to re-set mstatus.mie first
+
+	if ($past(trap_enter_vld && trap_enter_rdy))
+		assert(!(trap_enter_vld && trap_enter_rdy));
 end
 
 `endif

test/formal/bus_compliance_2port/tb.v

@@ -30,8 +30,10 @@ always @ (posedge clk)
 (* keep *) wire [2:0]   d_hburst;
 (* keep *) wire [3:0]   d_hprot;
 (* keep *) wire         d_hmastlock;
+(* keep *) wire         d_hexcl;
 (* keep *) wire         d_hready;
 (* keep *) wire         d_hresp;
+(* keep *) wire         d_hexokay;
 (* keep *) wire [31:0]  d_hwdata;
 (* keep *) wire [31:0]  d_hrdata;
 
@@ -60,8 +62,10 @@ hazard3_cpu_2port dut (
 	.d_hburst     (d_hburst),
 	.d_hprot      (d_hprot),
 	.d_hmastlock  (d_hmastlock),
+	.d_hexcl      (d_hexcl),
 	.d_hready     (d_hready),
 	.d_hresp      (d_hresp),
+	.d_hexokay    (d_hexokay),
 	.d_hwdata     (d_hwdata),
 	.d_hrdata     (d_hrdata),
 
@@ -83,6 +87,7 @@ ahbl_slave_assumptions #(
 	.dst_hready_resp (i_hready),
 	.dst_hready      (i_hready),
 	.dst_hresp       (i_hresp),
+	.dst_hexokay     (1'b0),
 	.dst_haddr       (i_haddr),
 	.dst_hwrite      (i_hwrite),
 	.dst_htrans      (i_htrans),
@@ -90,6 +95,7 @@ ahbl_slave_assumptions #(
 	.dst_hburst      (i_hburst),
 	.dst_hprot       (i_hprot),
 	.dst_hmastlock   (i_hmastlock),
+	.dst_hexcl       (1'b0),
 	.dst_hwdata      (i_hwdata),
 	.dst_hrdata      (i_hrdata)
 );
@@ -103,6 +109,7 @@ ahbl_slave_assumptions #(
 	.dst_hready_resp (d_hready),
 	.dst_hready      (d_hready),
 	.dst_hresp       (d_hresp),
+	.dst_hexokay     (d_hexokay),
 	.dst_haddr       (d_haddr),
 	.dst_hwrite      (d_hwrite),
 	.dst_htrans      (d_htrans),
@@ -110,6 +117,7 @@ ahbl_slave_assumptions #(
 	.dst_hburst      (d_hburst),
 	.dst_hprot       (d_hprot),
 	.dst_hmastlock   (d_hmastlock),
+	.dst_hexcl       (d_hexcl),
 	.dst_hwdata      (d_hwdata),
 	.dst_hrdata      (d_hrdata)
 );
@@ -120,6 +128,7 @@ ahbl_master_assertions i_assertions (
 
 	.src_hready      (i_hready),
 	.src_hresp       (i_hresp),
+	.src_hexokay     (1'b0),
 	.src_haddr       (i_haddr),
 	.src_hwrite      (i_hwrite),
 	.src_htrans      (i_htrans),
@@ -127,6 +136,7 @@ ahbl_master_assertions i_assertions (
 	.src_hburst      (i_hburst),
 	.src_hprot       (i_hprot),
 	.src_hmastlock   (i_hmastlock),
+	.src_hexcl       (1'b0),
 	.src_hwdata      (i_hwdata),
 	.src_hrdata      (i_hrdata)
 );
@@ -138,6 +148,7 @@ ahbl_master_assertions d_assertions (
 
 	.src_hready      (d_hready),
 	.src_hresp       (d_hresp),
+	.src_hexokay     (d_hexokay),
 	.src_haddr       (d_haddr),
 	.src_hwrite      (d_hwrite),
 	.src_htrans      (d_htrans),
@@ -145,6 +156,7 @@ ahbl_master_assertions d_assertions (
 	.src_hburst      (d_hburst),
 	.src_hprot       (d_hprot),
 	.src_hmastlock   (d_hmastlock),
+	.src_hexcl       (d_hexcl),
 	.src_hwdata      (d_hwdata),
 	.src_hrdata      (d_hrdata)
 );

test/formal/common/ahbl_master_assertions.v

@@ -26,6 +26,7 @@ module ahbl_master_assertions #(
 
 	input wire               src_hready,
 	input wire               src_hresp,
+	input wire               src_hexokay,
 	input wire [W_ADDR-1:0]  src_haddr,
 	input wire               src_hwrite,
 	input wire [1:0]         src_htrans,
@@ -33,6 +34,7 @@ module ahbl_master_assertions #(
 	input wire [2:0]         src_hburst,
 	input wire [3:0]         src_hprot,
 	input wire               src_hmastlock,
+	input wire               src_hexcl,
 	input wire [W_DATA-1:0]  src_hwdata,
 	input wire [W_DATA-1:0]  src_hrdata
 );

test/formal/common/ahbl_slave_assumptions.v

@@ -28,6 +28,7 @@ module ahbl_slave_assumptions #(
 	input wire               dst_hready_resp,
 	input wire               dst_hready,
 	input wire               dst_hresp,
+	input wire               dst_hexokay,
 	input wire [W_ADDR-1:0]  dst_haddr,
 	input wire               dst_hwrite,
 	input wire [1:0]         dst_htrans,
@@ -35,6 +36,7 @@ module ahbl_slave_assumptions #(
 	input wire [2:0]         dst_hburst,
 	input wire [3:0]         dst_hprot,
 	input wire               dst_hmastlock,
+	input wire               dst_hexcl,
 	input wire [W_DATA-1:0]  dst_hwdata,
 	input wire [W_DATA-1:0]  dst_hrdata
 );