diff --git a/hdl/hazard3_csr.v b/hdl/hazard3_csr.v index f7a92b2..56b459d 100644 --- a/hdl/hazard3_csr.v +++ b/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 diff --git a/test/formal/bus_compliance_2port/tb.v b/test/formal/bus_compliance_2port/tb.v index 63654fd..2addfff 100644 --- a/test/formal/bus_compliance_2port/tb.v +++ b/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) ); diff --git a/test/formal/common/ahbl_master_assertions.v b/test/formal/common/ahbl_master_assertions.v index c2c2c1b..b9a30fe 100644 --- a/test/formal/common/ahbl_master_assertions.v +++ b/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 ); diff --git a/test/formal/common/ahbl_slave_assumptions.v b/test/formal/common/ahbl_slave_assumptions.v index 9a44cb5..52023d1 100644 --- a/test/formal/common/ahbl_slave_assumptions.v +++ b/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 );