From 5193dfe47719f8240b337875a5051b8aeb138db8 Mon Sep 17 00:00:00 2001 From: Luke Wren Date: Sat, 25 Jun 2022 20:08:35 +0100 Subject: [PATCH] Add separate define HAZARD3_ASSERTIONS for enabling internal assertions, and enable it only on the bus compliance model checks. Trying to make the solver's life easier in instruction_fetch_match. --- hdl/arith/hazard3_alu.v | 2 +- hdl/arith/hazard3_muldiv_seq.v | 2 +- hdl/arith/hazard3_shift_barrel.v | 2 +- hdl/hazard3_core.v | 18 +++++++++--------- hdl/hazard3_csr.v | 2 +- hdl/hazard3_decode.v | 11 ----------- hdl/hazard3_frontend.v | 10 +++++----- test/formal/bus_compliance_1port/Makefile | 3 +++ test/formal/bus_compliance_2port/Makefile | 3 +++ 9 files changed, 24 insertions(+), 29 deletions(-) diff --git a/hdl/arith/hazard3_alu.v b/hdl/arith/hazard3_alu.v index 7e7bd59..1143230 100644 --- a/hdl/arith/hazard3_alu.v +++ b/hdl/arith/hazard3_alu.v @@ -212,7 +212,7 @@ end // ---------------------------------------------------------------------------- // Properties for base-ISA instructions -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS `ifndef RISCV_FORMAL // Really we're just interested in the shifts and comparisons, as these are // the nontrivial ones. However, easier to test everything! diff --git a/hdl/arith/hazard3_muldiv_seq.v b/hdl/arith/hazard3_muldiv_seq.v index 1c6128b..30482e9 100644 --- a/hdl/arith/hazard3_muldiv_seq.v +++ b/hdl/arith/hazard3_muldiv_seq.v @@ -259,7 +259,7 @@ assign result_l = // ---------------------------------------------------------------------------- // Interface properties -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS always @ (posedge clk) if (rst_n && $past(rst_n)) begin: properties integer i; diff --git a/hdl/arith/hazard3_shift_barrel.v b/hdl/arith/hazard3_shift_barrel.v index b7060e2..74f8b86 100644 --- a/hdl/arith/hazard3_shift_barrel.v +++ b/hdl/arith/hazard3_shift_barrel.v @@ -47,7 +47,7 @@ always @ (*) begin: shift dout[i] = right_nleft ? shift_accum[W_DATA - 1 - i] : shift_accum[i]; end -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS always @ (*) begin if (right_nleft && arith && !rotate) begin: asr assert($signed(dout) == $signed(din) >>> $signed(shamt)); diff --git a/hdl/hazard3_core.v b/hdl/hazard3_core.v index 2829d79..e88fed2 100644 --- a/hdl/hazard3_core.v +++ b/hdl/hazard3_core.v @@ -396,7 +396,7 @@ always @ (posedge clk or negedge rst_n) begin end end -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS always @ (posedge clk) if (rst_n && !x_stall) begin // If stage 2 sees a reg operand, it must have been correctly predecoded too. if (|d_rs1) @@ -499,7 +499,7 @@ always @ (posedge clk or negedge rst_n) begin if (m_trap_enter_vld) begin // Bail out, squash the in-progress AMO. x_amo_phase <= 3'h0; -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS // Should only happen during an address phase, *or* the fault phase. assert(x_amo_phase == 3'h0 || x_amo_phase == 3'h2 || x_amo_phase == 3'h4); // The fault phase only holds when we have a misaligned AMO directly behind @@ -512,14 +512,14 @@ always @ (posedge clk or negedge rst_n) begin // First address phase stalled due to address dependency on // previous load/mul/etc. Shouldn't be possible in later phases. x_amo_phase <= 3'h0; -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS assert(x_amo_phase == 3'h0); `endif end else if (x_amo_phase == 3'h4) begin // Clear fault phase once it goes through to stage 3 and excepts if (!x_stall) x_amo_phase <= 3'h0; -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS // This should only happen when we are stalled on an older load/store etc assert(!(x_stall && !m_stall)); `endif @@ -542,7 +542,7 @@ always @ (posedge clk or negedge rst_n) begin end end -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS always @ (posedge clk) if (rst_n) begin // Other states should be unreachable assert(x_amo_phase <= 3'h4); @@ -691,7 +691,7 @@ if (EXTENSION_M) begin: has_muldiv end -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS always @ (posedge clk) if (d_aluop != ALUOP_MULDIV) assert(!x_stall_muldiv); `endif @@ -957,7 +957,7 @@ always @ (posedge clk or negedge rst_n) begin // First phase of 2-phase AHBL error response. Pass the exception along on // this cycle, and on the next cycle the trap entry will be asserted, // suppressing any load/store that may currently be in stage X. -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS assert(xm_memop != MEMOP_NONE); `endif xm_except <= @@ -968,7 +968,7 @@ always @ (posedge clk or negedge rst_n) begin end end -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS always @ (posedge clk) if (rst_n) begin // D bus errors must always squash younger load/stores if ($past(bus_dph_err_d && !bus_dph_ready_d)) @@ -1124,7 +1124,7 @@ always @ (posedge clk) begin end `endif -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS // We borrow mw_result during an AMO to capture rdata and feed back through // the ALU, since it already has the right paths. Make sure this is safe. // (Whatever instruction is in M ahead of AMO should have passed through by diff --git a/hdl/hazard3_csr.v b/hdl/hazard3_csr.v index 15742a1..1e61e1a 100644 --- a/hdl/hazard3_csr.v +++ b/hdl/hazard3_csr.v @@ -1198,7 +1198,7 @@ assign m_mode_loadstore = !U_MODE || debug_mode || ( // FIXME how does this inte // ---------------------------------------------------------------------------- // Properties -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS // Keep track of whether we are in a trap (only for formal property purposes) reg in_trap; diff --git a/hdl/hazard3_decode.v b/hdl/hazard3_decode.v index 8fe249f..567a5ed 100644 --- a/hdl/hazard3_decode.v +++ b/hdl/hazard3_decode.v @@ -150,17 +150,6 @@ always @ (posedge clk or negedge rst_n) begin // prediction target instead of the sequentially next PC pc <= predicted_branch ? d_btb_target_addr : pc_seq_next; end - // If the current instruction is marked as being a predicted-taken - // branch, it *must* be a valid branch instruction, because executing - // the branch is how we recover from misprediction -`ifdef FORMAL - // This can be defeated if you branch backward halfway into a 32-bit - // instruction that immediately precedes the branch. - // if (predicted_branch && !d_starved && !debug_mode && !d_except_instr_bus_fault) begin - // assert(!d_invalid); - // assert(d_branchcond == BCOND_ZERO || d_branchcond == BCOND_NZERO); - // end -`endif end end diff --git a/hdl/hazard3_frontend.v b/hdl/hazard3_frontend.v index 10d97c8..6ea9424 100644 --- a/hdl/hazard3_frontend.v +++ b/hdl/hazard3_frontend.v @@ -162,7 +162,7 @@ always @ (posedge clk or negedge rst_n) begin: fifo_update fifo_predbranch[0] <= 2'b00; fifo_valid_hw[0] <= 2'b11; end -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS // FIFO validity must be compact, so we can always consume from the end if (!fifo_valid[0]) begin assert(!fifo_valid[1]); @@ -270,7 +270,7 @@ always @ (posedge clk or negedge rst_n) begin // This should be impossible, but assert to be sure, because it *will* // change the fetch address (and we shouldn't check it in hardware if // we can prove it doesn't happen) -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS assert(!(jump_target_vld && reset_holdoff)); `endif end @@ -338,7 +338,7 @@ always @ (posedge clk or negedge rst_n) begin pending_fetches <= 2'h0; ctr_flush_pending <= 2'h0; end else begin -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS assert(ctr_flush_pending <= pending_fetches); assert(pending_fetches < 2'd3); assert(!(mem_data_vld && !pending_fetches)); @@ -485,7 +485,7 @@ always @ (posedge clk or negedge rst_n) begin cir_bus_err <= 3'h0; cir_predbranch_reg <= 3'h0; end else begin -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS assert(cir_vld <= 2); assert(cir_use <= cir_vld); if (!jump_now) @@ -499,7 +499,7 @@ always @ (posedge clk or negedge rst_n) begin end end -`ifdef FORMAL +`ifdef HAZARD3_ASSERTIONS reg [1:0] property_past_buf_level; // Workaround for weird non-constant $past reset issue always @ (posedge clk or negedge rst_n) begin if (!rst_n) begin diff --git a/test/formal/bus_compliance_1port/Makefile b/test/formal/bus_compliance_1port/Makefile index 29d7a87..146c9ce 100644 --- a/test/formal/bus_compliance_1port/Makefile +++ b/test/formal/bus_compliance_1port/Makefile @@ -3,6 +3,9 @@ TOP=tb YOSYS_SMT_SOLVER=z3 DEPTH=25 +# Also check internal properties +DEFINES=HAZARD3_ASSERTIONS + all: bmc include $(SCRIPTS)/formal.mk diff --git a/test/formal/bus_compliance_2port/Makefile b/test/formal/bus_compliance_2port/Makefile index 29d7a87..146c9ce 100644 --- a/test/formal/bus_compliance_2port/Makefile +++ b/test/formal/bus_compliance_2port/Makefile @@ -3,6 +3,9 @@ TOP=tb YOSYS_SMT_SOLVER=z3 DEPTH=25 +# Also check internal properties +DEFINES=HAZARD3_ASSERTIONS + all: bmc include $(SCRIPTS)/formal.mk