colin
/
Hazard3
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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

This commit is contained in:
Luke Wren 2021-05-29 23:24:02 +01:00
parent ea5db61582
commit ad8f251ba2
2 changed files with 48 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
hdl/hazard3_rvfi_monitor.vh
View File

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

74
hdl/hazard3_rvfi_wrapper.v
View File

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