From ad8f251ba2db3b36a67809a6dc02d9bac45eafd0 Mon Sep 17 00:00:00 2001
From: Luke Wren <wren6991@gmail.com>
Date: Sat, 29 May 2021 23:24:02 +0100
Subject: [PATCH] RVFI wrapper: use proper bus assumptions. RVFI monitor: don't
 mark instruction which is aligned with IRQ as invalid, because the IRQ entry
 is notionally behind it

---
 hdl/hazard3_rvfi_monitor.vh |  6 +--
 hdl/hazard3_rvfi_wrapper.v  | 74 +++++++++++++++++++++++--------------
 2 files changed, 48 insertions(+), 32 deletions(-)

diff --git a/hdl/hazard3_rvfi_monitor.vh b/hdl/hazard3_rvfi_monitor.vh
index 16df2f7..22a0328 100644
--- a/hdl/hazard3_rvfi_monitor.vh
+++ b/hdl/hazard3_rvfi_monitor.vh
@@ -47,9 +47,7 @@ always @ (posedge clk or negedge rst_n) begin
 		end else if (!m_stall) begin
 			rvfm_m_valid <= 1'b0;
 		end
-		// Squash instructions where an IRQ is taken (but keep instructions which
-		// cause an exception... which is really what the rvfi_trap signal refers to)
-		rvfi_valid_r <= rvfm_m_valid && !m_stall && !(m_trap_enter_vld && !rvfm_m_trap);
+		rvfi_valid_r <= rvfm_m_valid && !m_stall;
 		rvfi_insn_r <= rvfm_m_instr;
 		rvfi_trap_r <= rvfm_m_trap;
 
@@ -111,7 +109,7 @@ assign rvfi_pc_wdata = rvfi_pc_wdata_r;
 always @ (posedge clk) begin
 	if (!m_stall) begin
 		rvfi_pc_rdata_r <= rvfm_xm_pc;
-		rvfi_pc_wdata_r <= rvfm_xm_pc_next;
+		rvfi_pc_wdata_r <= m_trap_enter_vld && m_trap_enter_rdy ? m_trap_addr : rvfm_xm_pc_next;
 	end
 end
 
diff --git a/hdl/hazard3_rvfi_wrapper.v b/hdl/hazard3_rvfi_wrapper.v
index 25be6c5..fd2e6fa 100644
--- a/hdl/hazard3_rvfi_wrapper.v
+++ b/hdl/hazard3_rvfi_wrapper.v
@@ -33,38 +33,56 @@ module rvfi_wrapper (
 (* keep *) `rvformal_rand_reg [31:0]  d_hrdata;
 
 
-// AHB-lite requires: data phase of IDLE has no wait states
-always @ (posedge clock) begin
-	if ($past(i_htrans) == 2'b00 && $past(i_hready))
-		assume(i_hready);
-	if ($past(d_htrans) == 2'b00 && $past(d_hready))
-		assume(d_hready);
-end
+
 
 `ifdef RISCV_FORMAL_FAIRNESS
-
-reg [7:0] i_bus_fairness_ctr;
-reg [7:0] d_bus_fairness_ctr;
-localparam MAX_STALL_LENGTH = 8;
-
-always @ (posedge clock) begin
-	if (reset) begin
-		i_bus_fairness_ctr <= 8'h0;
-		d_bus_fairness_ctr <= 8'h0;
-	end else begin
-		i_bus_fairness_ctr <= i_bus_fairness_ctr + ~&i_bus_fairness_ctr;
-		d_bus_fairness_ctr <= d_bus_fairness_ctr + ~&d_bus_fairness_ctr;
-		if (i_hready)
-			i_bus_fairness_ctr <= 8'h0;
-		if (d_hready)
-			d_bus_fairness_ctr <= 8'h0;
-	end
-	assume(i_bus_fairness_ctr <= MAX_STALL_LENGTH);
-	assume(d_bus_fairness_ctr <= MAX_STALL_LENGTH);
-end
-
+localparam MAX_BUS_STALL = 8;
+`else
+localparam MAX_BUS_STALL = -1;
 `endif
 
+ahbl_slave_assumptions #(
+	.MAX_BUS_STALL (MAX_BUS_STALL)
+) i_slave_assumptions (
+	.clk             (clock),
+	.rst_n           (!reset),
+
+	.dst_hready_resp (i_hready),
+	.dst_hready      (i_hready),
+	.dst_hresp       (i_hresp),
+	.dst_haddr       (i_haddr),
+	.dst_hwrite      (i_hwrite),
+	.dst_htrans      (i_htrans),
+	.dst_hsize       (i_hsize),
+	.dst_hburst      (i_hburst),
+	.dst_hprot       (i_hprot),
+	.dst_hmastlock   (i_hmastlock),
+	.dst_hwdata      (i_hwdata),
+	.dst_hrdata      (i_hrdata)
+);
+
+
+ahbl_slave_assumptions #(
+	.MAX_BUS_STALL (MAX_BUS_STALL)
+) d_slave_assumptions (
+	.clk             (clock),
+	.rst_n           (!reset),
+
+	.dst_hready_resp (d_hready),
+	.dst_hready      (d_hready),
+	.dst_hresp       (d_hresp),
+	.dst_haddr       (d_haddr),
+	.dst_hwrite      (d_hwrite),
+	.dst_htrans      (d_htrans),
+	.dst_hsize       (d_hsize),
+	.dst_hburst      (d_hburst),
+	.dst_hprot       (d_hprot),
+	.dst_hmastlock   (d_hmastlock),
+	.dst_hwdata      (d_hwdata),
+	.dst_hrdata      (d_hrdata)
+);
+
+
 // ----------------------------------------------------------------------------
 // Device Under Test
 // ----------------------------------------------------------------------------