Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix assert #2304

Merged
merged 3 commits into from
Nov 30, 2023
Merged

fix assert #2304

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
bc06068
fix rlb-write assert
silabs-krdosvik Nov 28, 2023
b5976e9
Merge branch 'cv32e40s/dev' of github.com:openhwgroup/core-v-verif in…
silabs-krdosvik Nov 28, 2023
d52afed
Remove unnecessary logic
silabs-krdosvik Nov 30, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
92 changes: 77 additions & 15 deletions cv32e40s/tb/assertions/uvmt_cv32e40s_pmprvfi_assert.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
module uvmt_cv32e40s_pmprvfi_assert
import cv32e40s_pkg::*;
import support_pkg::*;
import isa_decoder_pkg::*;
import uvm_pkg::*;
import uvma_rvfi_pkg::*;
import uvma_rvfi_pkg::EXC_CAUSE_INSTR_BUS_FAULT;
Expand All @@ -38,6 +39,7 @@ module uvmt_cv32e40s_pmprvfi_assert

//RVFI INSTR IF
uvma_rvfi_instr_if_t rvfi_if,
uvmt_cv32e40s_support_logic_module_o_if_t.slave_mp support_if,
// RVFI
input wire rvfi_valid,
input wire [31:0] rvfi_insn,
Expand Down Expand Up @@ -146,7 +148,7 @@ module uvmt_cv32e40s_pmprvfi_assert

wire is_rvfi_csr_write_instr =
is_rvfi_csr_instr &&
!((rvfi_insn[13:12] inside {2'b 10, 2'b 11}) && !rvfi_rs1_addr); // CSRRS/C[I] w/ rs1=x0/0
!((rvfi_insn[13:12] inside {2'b 01, 2'b 10, 2'b 11}) && !rvfi_rs1_addr); // CSRRW/S/C[I] w/ rs1=x0/0

wire [1:0] rvfi_effective_mode =
rvfi_csr_mstatus_rdata[17] ? // "mstatus.MPRV", modify privilege?
Expand Down Expand Up @@ -507,26 +509,86 @@ module uvmt_cv32e40s_pmprvfi_assert


// Stickiness isn't effectuated before triggered (vplan:LockingBypass:UntilReset)
logic first_MSECCFG_access;

always @(posedge clk_i, negedge rst_ni) begin
if (rst_ni == 0) begin
first_MSECCFG_access <= 1'b 1;
end else if (
rvfi_valid &&
!rvfi_trap &&
(support_if.asm_rvfi.instr == CSRRW ||
support_if.asm_rvfi.instr == CSRRS ||
support_if.asm_rvfi.instr == CSRRC ||
support_if.asm_rvfi.instr == CSRRWI ||
support_if.asm_rvfi.instr == CSRRSI ||
support_if.asm_rvfi.instr == CSRRCI)
) begin
first_MSECCFG_access <= 1'b 0;
end
end

property p_until_reset_notbefore(logic rlb);
$rose(rst_ni) ##0
(rvfi_valid [->1]) ##0 // First retire
(is_rvfi_csr_write_instr && (rvfi_insn[14:12] == 3'b 001)) ##0 // ..."csrrw"
(rvfi_insn[31:20] == CSRADDR_MSECCFG) ##0 // ...to mseccfg
!rvfi_trap ##0
(rvfi_rs1_rdata[2] == rlb) // (Write-attempt's data)
|->
pmp_csr_rvfi_wmask.mseccfg.rlb && // Must attempt
(pmp_csr_rvfi_wdata.mseccfg.rlb == rlb) // Must succeed
;
endproperty : p_until_reset_notbefore

a_until_reset_notbefore_0: assert property (
p_until_reset_notbefore(1'b 0)
$rose(rst_ni) ##0

// First write access to MSECCFG:
(rvfi_valid &&
first_MSECCFG_access &&

support_if.asm_rvfi.csr.address == MSECCFG &&
support_if.asm_rvfi.csr.valid &&

(support_if.asm_rvfi.instr == CSRRW ||
support_if.asm_rvfi.instr == CSRRC ||
support_if.asm_rvfi.instr == CSRRWI ||
support_if.asm_rvfi.instr == CSRRCI) &&

!rvfi_trap)[->1]
silabs-robin marked this conversation as resolved.
Show resolved Hide resolved

##0

// Set RLB bit to 0:
((support_if.asm_rvfi.instr == CSRRW && rvfi_rs1_rdata[2] == 1'b0) ||
(support_if.asm_rvfi.instr == CSRRC && rvfi_rs1_rdata[2] == 1'b1) ||
(support_if.asm_rvfi.instr == CSRRWI && support_if.asm_rvfi.imm.imm_value[2] == 1'b0) ||
(support_if.asm_rvfi.instr == CSRRCI && support_if.asm_rvfi.imm.imm_value[2] == 1'b1))

|->
pmp_csr_rvfi_wmask.mseccfg.rlb && // Must attempt
(pmp_csr_rvfi_wdata.mseccfg.rlb == 1'b0) // Must succeed
) else `uvm_error(info_tag, "RLB must be changeable after reset");


a_until_reset_notbefore_1: assert property (
silabs-robin marked this conversation as resolved.
Show resolved Hide resolved
p_until_reset_notbefore(1'b 1)
$rose(rst_ni) ##0

// First write access to MSECCFG:
(rvfi_valid &&
first_MSECCFG_access &&

support_if.asm_rvfi.csr.address == MSECCFG &&
support_if.asm_rvfi.csr.valid &&

(support_if.asm_rvfi.instr == CSRRW ||
support_if.asm_rvfi.instr == CSRRS ||
support_if.asm_rvfi.instr == CSRRWI ||
support_if.asm_rvfi.instr == CSRRSI) &&

!rvfi_trap)[->1]

##0

// Set RLB bit to 1:
((support_if.asm_rvfi.instr == CSRRW || support_if.asm_rvfi.instr == CSRRS) &&
rvfi_rs1_rdata[2] == 1'b1) ||

((support_if.asm_rvfi.instr == CSRRWI || support_if.asm_rvfi.instr == CSRRSI) &&
support_if.asm_rvfi.imm.imm_value[2])

|->
pmp_csr_rvfi_wmask.mseccfg.rlb && // Must attempt
(pmp_csr_rvfi_wdata.mseccfg.rlb == 1'b1) // Must succeed
) else `uvm_error(info_tag, "RLB must be changeable after reset");


Expand Down
1 change: 1 addition & 0 deletions cv32e40s/tb/uvmt/uvmt_cv32e40s_tb.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1526,6 +1526,7 @@ module uvmt_cv32e40s_tb;
.PMP_NUM_REGIONS (uvmt_cv32e40s_base_test_pkg::CORE_PARAM_PMP_NUM_REGIONS)
) pmprvfi_assert_i (
.rvfi_if (dut_wrap.cv32e40s_wrapper_i.rvfi_instr_if),
.support_if (support_logic_module_o_if.slave_mp),
.rvfi_mem_addr (rvfi_mem_addr [31:0]),
.rvfi_mem_wmask (rvfi_mem_wmask[ 3:0]),
.rvfi_mem_rmask (rvfi_mem_rmask[ 3:0]),
Expand Down
1 change: 1 addition & 0 deletions lib/isa_decoder/isa_typedefs_csr.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@
MSCRATCHCSW = 12'h348,
MSCRATCHCSWL = 12'h349,
MCLICBASE = 12'h34A,
MSECCFG = 12'h747,
TSELECT = 12'h7A0,
TDATA1 = 12'h7A1,
TDATA2 = 12'h7A2,
Expand Down