From 3703b1fc4c3b15d12926e0132b66522abe4506f0 Mon Sep 17 00:00:00 2001
From: Luke Wren <wren6991@gmail.com>
Date: Mon, 13 Jun 2022 20:36:15 +0100
Subject: [PATCH] Allow use of cir_flush_behind in frontend_match formal tb

---
 hdl/hazard3_frontend.v                |  2 +-
 test/formal/frontend_fetch_match/tb.v | 33 +++++++++++++++++++++++++--
 2 files changed, 32 insertions(+), 3 deletions(-)

diff --git a/hdl/hazard3_frontend.v b/hdl/hazard3_frontend.v
index ec18ad0..34f9c0f 100644
--- a/hdl/hazard3_frontend.v
+++ b/hdl/hazard3_frontend.v
@@ -74,7 +74,7 @@ module hazard3_frontend #(
 
 `include "rv_opcodes.vh"
 
-localparam W_BUNDLE = W_DATA / 2;
+localparam W_BUNDLE = 16;
 // This is the minimum for full throughput (enough to avoid dropping data when
 // decode stalls) and there is no significant advantage to going larger.
 localparam FIFO_DEPTH = 2;
diff --git a/test/formal/frontend_fetch_match/tb.v b/test/formal/frontend_fetch_match/tb.v
index cbfc9d2..5762ad7 100644
--- a/test/formal/frontend_fetch_match/tb.v
+++ b/test/formal/frontend_fetch_match/tb.v
@@ -120,14 +120,38 @@ always @ (posedge clk or negedge rst_n) begin
 	end
 end
 
-assign cir_flush_behind = 1'b0; // TODO
 assign debug_mode = 1'b0;
 assign dbg_instr_data_vld = 1'b0;
 
+// Don't consume nonexistent data
 always assume(cir_use <= cir_vld);
+// Consume an amount consistent with the instruction size (as the frontend
+// also considers instruction size when a cir_flush_behind occurs)
+always assume(cir_use == 0 || cir_use == (cir[1:0] == 2'b11 ? 2'd2 : 2'd1));
 
 assign jump_target[0] = 1'b0;
 
+// flush_behind is always due to an instruction in D, so should only happen
+// when the CIR is fully valid.
+assign cir_flush_behind = jump_target_vld && jump_target_rdy && ~|cir_use &&
+	cir_vld >= (cir[1:0] == 2'b11 ? 2'd2 : 2'd1);
+
+reg cir_locked;
+reg [31:0] jump_target_prev;
+always @ (posedge clk or negedge rst_n) begin
+	if (!rst_n) begin
+		cir_locked <= 1'b0;
+		jump_target_prev <= 32'h0;
+	end else begin
+		cir_locked <= (cir_locked || cir_flush_behind) && ~|cir_use;
+		jump_target_prev <= jump_target;
+		if (cir_locked) begin
+			assume(jump_target == jump_target_prev);
+			assume(!jump_target_vld);
+		end
+	end
+end
+
 // Jump should not be asserted on the first cycle after reset, as this *will*
 // change the fetch address and screw things up. We don't check this in
 // hardware (as it's assumed to be impossible in the real processor), just
@@ -145,6 +169,8 @@ always @ (posedge clk or negedge rst_n) begin
 	if (!rst_n) begin
 		pc <= RESET_VECTOR;
 	end else if (jump_target_vld && jump_target_rdy) begin
+		pc <= cir_flush_behind ? pc : jump_target;
+	end else if (cir_locked && |cir_use) begin
 		pc <= jump_target;
 	end else begin
 		pc <= pc + {cir_use, 1'b0};
@@ -159,7 +185,10 @@ always @ (posedge clk) if (rst_n) begin
 	if (cir_vld >= 2'd1) begin
 		assert(cir[15:0] == pc[16:1]);
 	end
-	if (cir_vld >= 2'd2) begin
+	// Note that following a flush_behind the upper half of the CIR may be
+	// nonsequential with the lower half, if and only if the lower half
+	// contains a 16-bit instruction.
+	if (cir_vld >= 2'd2 && cir[1:0] == 2'b11) begin
 		assert(cir[31:16] == pc[16:1] + 16'd1);
 	end
 end