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

@@ -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!

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;

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));

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

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;

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
 

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

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

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