Skip to content

Commit

Permalink
Added rvfi_wu and rvfi_sleep signals to rvfi, fixed issue with rvfi_c…
Browse files Browse the repository at this point in the history
…sr_mip_rdata signal

Signed-off-by: Halfdan Bechmann <[email protected]>
  • Loading branch information
halfdan-dolva committed Mar 24, 2022
1 parent 243bb9c commit 4ec718b
Show file tree
Hide file tree
Showing 5 changed files with 114 additions and 6 deletions.
53 changes: 49 additions & 4 deletions bhv/cv32e40x_rvfi.sv
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,7 @@ module cv32e40x_rvfi
input logic wb_valid_i,
input logic ebreak_in_wb_i,
input logic [31:0] instr_rdata_wb_i,
input logic csr_en_wb_i,
// Register writes
input logic rf_we_wb_i,
input logic [4:0] rf_addr_wb_i,
Expand All @@ -85,12 +86,20 @@ module cv32e40x_rvfi

input privlvl_t priv_lvl_i,

// Controller FSM probe
// Controller FSM probes
input ctrl_fsm_t ctrl_fsm_i,
input ctrl_state_e ctrl_fsm_cs_i,
input ctrl_state_e ctrl_fsm_ns_i,
input logic pending_single_step_i,
input logic single_step_allowed_i,
input logic nmi_pending_i,
input logic nmi_is_store_i,
input logic pending_debug_i,
input logic debug_mode_q_i,

// Interrupt Controller probes
input logic irq_wu_ctrl_i,
input logic [4:0] irq_id_ctrl_i,

//// CSR Probes ////
input jvt_t csr_jvt_n_i,
Expand Down Expand Up @@ -223,6 +232,9 @@ module cv32e40x_rvfi
output logic [ 2:0] rvfi_dbg,
output logic [ 0:0] rvfi_dbg_mode,

output rvfi_wu_t rvfi_wu,
output logic [ 0:0] rvfi_sleep,

output logic [ 4:0] rvfi_rd_addr,
output logic [31:0] rvfi_rd_wdata,
output logic [ 4:0] rvfi_rs1_addr,
Expand Down Expand Up @@ -514,8 +526,6 @@ module cv32e40x_rvfi
logic [31:0] mhpmcounter_h_during_wb;




logic [63:0] data_wdata_ror; // Intermediate rotate signal, as direct part-select not supported in all tools

logic pc_mux_debug;
Expand Down Expand Up @@ -571,6 +581,34 @@ module cv32e40x_rvfi
assign in_trap_clr = wb_valid_i && in_trap[STAGE_WB].intr;


// Store information about wakeup until fist instruction is retired
// This information needs to be stored at the wakeup because other interrupts
// can be triggered between wakeup and the first instruction executed after wakeup
rvfi_wu_t rvfi_wu_next;
logic store_irq_wu_cause;

assign rvfi_wu_next.wu = rvfi_sleep; // If sleep is still set, it is the firs instruction after wakeup
always_ff @(posedge clk_i or negedge rst_ni) begin
if (!rst_ni) begin
store_irq_wu_cause <= 1'b0;
rvfi_wu_next.interrupt <= 1'b0;
rvfi_wu_next.debug <= 1'b0;
rvfi_wu_next.cause <= '0;
end else begin
// Store wake-up sources when core exits sleep
if ((ctrl_fsm_cs_i == SLEEP) && (ctrl_fsm_ns_i != SLEEP)) begin
rvfi_wu_next.interrupt <= irq_wu_ctrl_i;
store_irq_wu_cause <= irq_wu_ctrl_i;
rvfi_wu_next.debug <= pending_debug_i || debug_mode_q_i;
end
// IRQ cause is flopped and is therefore one cycle behind wakeup triggers
if (store_irq_wu_cause) begin
store_irq_wu_cause <= 1'b0;
rvfi_wu_next.cause <= {'0, irq_id_ctrl_i}; // NMIs will not wake up the core
end
end
end

// Set rvfi_trap for instructions causing exception or debug entry.
rvfi_trap_t rvfi_trap_next;

Expand Down Expand Up @@ -645,6 +683,8 @@ module cv32e40x_rvfi
ex_csr_rdata <= '0;
rvfi_dbg <= '0;
rvfi_dbg_mode <= '0;
rvfi_wu <= '0;
rvfi_sleep <= 1'b0;
rvfi_valid <= 1'b0;
rvfi_order <= '0;
rvfi_insn <= '0;
Expand Down Expand Up @@ -817,11 +857,16 @@ module cv32e40x_rvfi
rvfi_dbg <= debug_cause[STAGE_WB];
rvfi_dbg_mode <= debug_mode [STAGE_WB];

rvfi_sleep <= (ctrl_fsm_ns_i == SLEEP);
rvfi_wu <= rvfi_wu_next;

// Set expected next PC, half-word aligned
// Predict synchronous exceptions and synchronous debug entry in WB to include all causes
rvfi_pc_wdata <= (pc_mux_debug || pc_mux_exception) ? branch_addr_n_i & ~32'b1 :
(pc_mux_dret) ? csr_dpc_q_i :
pc_wdata[STAGE_WB] & ~32'b1;
end else begin // if (wb_valid_i)
rvfi_sleep <= rvfi_sleep; // Keep sleep signal asserted until next valid WB
end

end
Expand Down Expand Up @@ -965,7 +1010,7 @@ module cv32e40x_rvfi
assign rvfi_csr_wmask_d.mtval = '0;

assign ex_csr_rdata_d.mip = csr_mip_q_i;
assign rvfi_csr_rdata_d.mip = ex_csr_rdata.mip;
assign rvfi_csr_rdata_d.mip = csr_en_wb_i ? ex_csr_rdata.mip : csr_mip_q_i;
assign rvfi_csr_wdata_d.mip = csr_mip_n_i;
assign rvfi_csr_wmask_d.mip = csr_mip_we_i ? '1 : '0;

Expand Down
10 changes: 9 additions & 1 deletion bhv/cv32e40x_wrapper.sv
Original file line number Diff line number Diff line change
Expand Up @@ -254,7 +254,7 @@ module cv32e40x_wrapper
.branch_taken_in_ex (core_i.controller_i.controller_fsm_i.branch_taken_ex),
.exc_cause (core_i.controller_i.controller_fsm_i.exc_cause),
// probed controller signals
.ctrl_fsm_ns (core_i.controller_i.controller_fsm_i.ctrl_fsm_ns),
.ctrl_fsm_ns (core_i.controller_i.controller_fsm_i.ctrl_fsm_ns),
.ctrl_debug_mode_n (core_i.controller_i.controller_fsm_i.debug_mode_n),
.ctrl_pending_debug (core_i.controller_i.controller_fsm_i.pending_debug),
.ctrl_debug_allowed (core_i.controller_i.controller_fsm_i.debug_allowed),
Expand Down Expand Up @@ -339,6 +339,7 @@ module cv32e40x_wrapper
.dbg_ack(core_i.dbg_ack),
.ebreak_in_wb_i(core_i.controller_i.controller_fsm_i.ebreak_in_wb),
.nmi_addr_i(core_i.nmi_addr_i),
.core_sleep_i(core_i.core_sleep_o),
.*);

`endif // `ifndef COREV_ASSERT_OFF
Expand All @@ -365,6 +366,7 @@ module cv32e40x_wrapper
.wb_valid_i ( core_i.wb_stage_i.wb_valid_o ),
.wb_ready_i ( core_i.wb_stage_i.wb_ready_o ),
.instr_rdata_wb_i ( core_i.wb_stage_i.ex_wb_pipe_i.instr.bus_resp.rdata ),
.csr_en_wb_i ( core_i.wb_stage_i.ex_wb_pipe_i.csr_en ),
.ebreak_in_wb_i ( core_i.controller_i.controller_fsm_i.ebreak_in_wb ),

.rs1_addr_id_i ( core_i.register_file_wrapper_i.raddr_i[0] ),
Expand Down Expand Up @@ -414,10 +416,16 @@ module cv32e40x_wrapper

.priv_lvl_i ( PRIV_LVL_M /* Not implemented in cv32e40x */ ),
.ctrl_fsm_i ( core_i.ctrl_fsm ),
.ctrl_fsm_cs_i ( core_i.controller_i.controller_fsm_i.ctrl_fsm_cs ),
.ctrl_fsm_ns_i ( core_i.controller_i.controller_fsm_i.ctrl_fsm_ns ),
.pending_single_step_i ( core_i.controller_i.controller_fsm_i.pending_single_step ),
.single_step_allowed_i ( core_i.controller_i.controller_fsm_i.single_step_allowed ),
.nmi_pending_i ( core_i.controller_i.controller_fsm_i.nmi_pending_q ),
.nmi_is_store_i ( core_i.controller_i.controller_fsm_i.nmi_is_store_q ),
.pending_debug_i ( core_i.controller_i.controller_fsm_i.pending_debug ),
.debug_mode_q_i ( core_i.controller_i.controller_fsm_i.debug_mode_q ),
.irq_wu_ctrl_i ( core_i.irq_wu_ctrl ),
.irq_id_ctrl_i ( core_i.irq_id_ctrl ),
// CSRs
.csr_jvt_n_i ( core_i.cs_registers_i.jvt_n ),
.csr_jvt_q_i ( core_i.cs_registers_i.jvt_q ),
Expand Down
7 changes: 7 additions & 0 deletions bhv/include/cv32e40x_rvfi_pkg.sv
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,13 @@ package cv32e40x_rvfi_pkg;

} rvfi_csr_map_t;

typedef struct packed {
logic [10:0] cause;
logic debug;
logic interrupt;
logic wu;
} rvfi_wu_t;

typedef struct packed {
logic [10:0] cause;
logic interrupt;
Expand Down
3 changes: 3 additions & 0 deletions bhv/include/cv32e40x_wrapper.vh
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,9 @@
.rvfi_dbg(),\
.rvfi_dbg_mode(),\
\
.rvfi_wu(),\
.rvfi_sleep(),\
\
.rvfi_rd_addr(),\
.rvfi_rd_wdata(),\
.rvfi_rs1_addr(),\
Expand Down
47 changes: 46 additions & 1 deletion sva/cv32e40x_rvfi_sva.sv
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,11 @@ module cv32e40x_rvfi_sva
input rvfi_trap_t rvfi_trap,
input logic [2:0] rvfi_dbg,

input ctrl_fsm_t ctrl_fsm_i,
input rvfi_wu_t rvfi_wu,
input logic rvfi_sleep,

input logic core_sleep_i,
input ctrl_fsm_t ctrl_fsm_i,
input logic [31:0] rvfi_csr_dcsr_rdata,
input logic [31:0] rvfi_csr_mcause_rdata,
input logic [31:0] rvfi_pc_rdata,
Expand Down Expand Up @@ -168,6 +172,47 @@ module cv32e40x_rvfi_sva
((rvfi_csr_mcause_rdata[7:0] == INT_CAUSE_LSU_LOAD_FAULT) || (rvfi_csr_mcause_rdata[7:0] == INT_CAUSE_LSU_STORE_FAULT)))
else `uvm_error("rvfi", "dcsr.nmip not followed by rvfi_intr and NMI handler")


// Check that rvfi_sleep is always followed by rvfi_wu
a_always_rvfi_wu_after_rvfi_sleep:
assert property (@(posedge clk_i) disable iff (!rst_ni)
s_goto_next_rvfi_valid(rvfi_sleep) |-> rvfi_wu.wu)
else `uvm_error("rvfi", "rvfi_sleep asserted without being followed by rvfi_wu")


logic previous_instruction_was_sleep;
always_ff @(posedge clk_i or negedge rst_ni) begin
if (!rst_ni) begin
previous_instruction_was_sleep <= 1'b0;
end else begin
if ( rvfi_valid ) begin
// Store sleep signal from previous valid instruction
previous_instruction_was_sleep <= rvfi_sleep;
end
end
end

// Check that rvfi_wu is only asserted after fist having signalled rvfi_sleep
a_always_rvfi_sleep_before_rvfi_wu:
assert property (@(posedge clk_i) disable iff (!rst_ni)
(rvfi_wu.wu && rvfi_valid) |-> previous_instruction_was_sleep)
else `uvm_error("rvfi", "rvfi_wu asserted without a previous rvfi_sleep")

// Check that the last instruction before core_sleep_o had rvfi_sleep set
a_always_core_sleep_always_preceeded_by_instr_with_rvfi_sleep:
assert property (@(posedge clk_i) disable iff (!rst_ni)
core_sleep_i |-> previous_instruction_was_sleep)
else `uvm_error("rvfi", "The instruction before asserted core_sleep_o did not have rvfi_sleep set")

// Check that rvfi_sleep is always set when the core is sleeping
// This assertion is stricter than needed (behavior only specified for valid insructions)
// but is added as a sanity check for this implementation
a_always_rvfi_sleep_when_core_sleep:
assert property (@(posedge clk_i) disable iff (!rst_ni)
core_sleep_i |-> rvfi_sleep)
else `uvm_error("rvfi", "rvfi_sleep not asserted even though core_sleep_o was set")


endmodule : cv32e40x_rvfi_sva


0 comments on commit 4ec718b

Please sign in to comment.