Skip to content

Commit

Permalink
Merge branch 'cv32e40s/dev' of github.com:openhwgroup/core-v-verif in…
Browse files Browse the repository at this point in the history
…to xdev2sdev_merge_2023-11-20

Signed-off-by: Robin Pedersen <[email protected]>
  • Loading branch information
silabs-robin committed Nov 28, 2023
2 parents a98a325 + 7261536 commit eabbfa2
Show file tree
Hide file tree
Showing 16 changed files with 1,334 additions and 1,114 deletions.
14 changes: 12 additions & 2 deletions bin/merge.sh
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,16 @@ usage() {
}


die() {

scriptname=$0
message=$1
echo "$scriptname: error: $message"
exit 1

}


merge_cv32e40s_into_cv32e40x-dv () {

echo $'\n======= Merge of cv32e40s into cv32e40x-dv: =======\n'
Expand Down Expand Up @@ -158,8 +168,8 @@ rejection_diff() {
branch_name_merge_normal=$(git branch | grep 'merge')
branch_name_merge_theirs=$(echo $branch_name_merge_normal | sed 's/merge/theirs/')

git checkout main
git checkout -B $branch_name_merge_theirs
git checkout main || die "can't checkout main"
git checkout -B $branch_name_merge_theirs || die "can't create branch"
git merge -X theirs $branch_name_40s_subtree

move_files_40s_into_40x
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ UM v0.3.0 Common,Constraints,Privilege Modes,CLIC interrupts only support machin
Assume on input for formal",Assertion Check,"ENV capability, not specific test",Functional Coverage,a_clic_mode_only
UM v0.3.0 Common,Constraints,NMI,"NMI address is located at the 15th entry in the machine trap vector table, located at mtvec. In other words, nmi_addr = { mtvec[31:7], 5'b0_1111, 2'b00 }","Assert that nmi addr = { mtvec[31:7], 5'b0_1111, 2'b00 }",Assertion Check,"ENV capability, not specific test",Functional Coverage,a_nmi_to_mtvec_offset
UM v0.3.0 Common,Constraints,Interrupts,Support up to a maximum of 1024 CLIC interrupts,Assert that SMCLIC_ID_WIDTH is inside { 1 .. 10 },Assertion Check,"ENV capability, not specific test",Functional Coverage,a_clic_valid_setting
UM v0.3.0 Common,Constraints,Interrupts,Interrupt levels inside { 0 .. 255 },Correct functionality of interrupts of all valid levels,Check against RM,Constrained-Random,Functional Coverage,"Missing covergroup, vc should use all interrupt levels"
UM v0.3.0 Common,Constraints,Interrupts,Interrupt levels inside { 0 .. 255 },Correct functionality of interrupts of all valid levels,Check against RM,Constrained-Random,Functional Coverage,clic_cg.cp_lvl
UM v0.3.0 Common,Constraints,Input ports,irq_i[31:0] tied to zero,Assert that non-clic irq[31:0] signals are tied to 0,Assertion Check,"ENV capability, not specific test",Functional Coverage,a_tieoff_zero_irq_i
Silabs Internal,Eventually taken,Interrupt taken,"An interrupt that is both pending and enabled shall be taken, unless if the core is in debug mode or is blocked by external interfaces (rvalid, fence_flush_ack, etc), and the taking happens within a fixed number of cycles","Check that when conditions are right, then the interrupt gets taken within expected time",Assertion Check,"ENV capability, not specific test",Functional Coverage,"Waived on top level verification due to lack of visibility and precise specification of what prevents interrupts from being taken, and there exist no definite bound.

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@
"Pass/Fail Criteria": "Check against RM",
"Test Type": "Constrained-Random",
"Coverage Method": "Functional Coverage",
"Link to Coverage": "Missing covergroup, vc should use all interrupt levels"
"Link to Coverage": "clic_cg.cp_lvl"
},
{
"Requirement Location": "UM v0.3.0 Common",
Expand Down
Binary file modified cv32e40s/docs/VerifPlans/Simulation/interrupts/CV32E40SX_CLIC.xlsx
Binary file not shown.
624 changes: 393 additions & 231 deletions cv32e40s/docs/VerifPlans/Simulation/privileged_spec/CV32E40S_PMP.csv

Large diffs are not rendered by default.

763 changes: 323 additions & 440 deletions cv32e40s/docs/VerifPlans/Simulation/privileged_spec/CV32E40S_PMP.json

Large diffs are not rendered by default.

Binary file not shown.
33 changes: 29 additions & 4 deletions cv32e40s/tb/assertions/uvmt_cv32e40s_pmp_assert.sv
Original file line number Diff line number Diff line change
Expand Up @@ -205,25 +205,25 @@ module uvmt_cv32e40s_pmp_assert
iff (csr_pmp_i.cfg[match_status.val_index].mode == PMP_MODE_NAPOT &&
match_status.is_matched == 1'b1 &&
match_status.is_access_allowed == 1'b1
);
);

cp_napot_min_8byte_disallowed: coverpoint { pmp_req_addr_i[2+PMP_GRANULARITY], csr_pmp_i.addr[match_status.val_index][2+PMP_GRANULARITY] }
iff (csr_pmp_i.cfg[match_status.val_index].mode == PMP_MODE_NAPOT &&
match_status.is_matched == 1'b1 &&
match_status.is_access_allowed == 1'b0
);
);

cp_napot_encoding: coverpoint ( pmp_req_addr_i[33:2+PMP_GRANULARITY] == csr_pmp_i.addr[match_status.val_index][33:2+PMP_GRANULARITY] )
iff (csr_pmp_i.cfg[match_status.val_index].mode == PMP_MODE_NAPOT &&
match_status.is_matched == 1'b1 &&
match_status.is_access_allowed == 1'b1
);
);

cp_napot_encoding_disallowed: coverpoint ( pmp_req_addr_i[33:2+PMP_GRANULARITY] == csr_pmp_i.addr[match_status.val_index][33:2+PMP_GRANULARITY] )
iff (csr_pmp_i.cfg[match_status.val_index].mode == PMP_MODE_NAPOT &&
match_status.is_matched == 1'b1 &&
match_status.is_access_allowed == 1'b0
);
);

endgroup
cg_internals_common cg_int = new();
Expand Down Expand Up @@ -306,6 +306,14 @@ module uvmt_cv32e40s_pmp_assert
$changed(csr_pmp_i.cfg[region].read)
);

if (region > 0) begin: gen_tor
cov_rlb_locked_rules_can_modify_tor : cover property (
csr_pmp_i.mseccfg.rlb === 1'b1 && csr_pmp_i.cfg[region].lock === 1'b1 &&
csr_pmp_i.cfg[region].mode === PMP_MODE_TOR ##1
$changed(csr_pmp_i.cfg[region-1])
);
end

cov_rlb_locked_rules_can_remove : cover property (
csr_pmp_i.mseccfg.rlb === 1'b1 &&
csr_pmp_i.cfg[region].lock == 1'b1 &&
Expand Down Expand Up @@ -538,6 +546,23 @@ module uvmt_cv32e40s_pmp_assert
end


// "mseccfg" has fields hardwired to 0 (vplan:ReservedZero)

a_reserved_zero_mseccfg_fields: assert property (
csr_pmp_i.mseccfg[31:3] == '0
) else `uvm_error(info_tag, "mseccfg fields not zero");


// "Unused" PMP CSRs read as zero (vplan:UnusedZero)

for (genvar i = PMP_NUM_REGIONS; i < 64; i++) begin: gen_unused_zero
a_unused_zero_pmp_csrs: assert property (
csr_pmp_i.cfg[i] == '0 &&
csr_pmp_i.addr[i] == '0
);
end


endmodule : uvmt_cv32e40s_pmp_assert


Expand Down
78 changes: 52 additions & 26 deletions cv32e40s/tb/assertions/uvmt_cv32e40s_pmprvfi_assert.sv
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,8 @@ module uvmt_cv32e40s_pmprvfi_assert
import uvma_rvfi_pkg::EXC_CAUSE_INSTR_INTEGRITY_FAULT;
import uvmt_cv32e40s_base_test_pkg::*;
#(
parameter int PMP_GRANULARITY = 0,
parameter int PMP_NUM_REGIONS = 0
parameter int PMP_GRANULARITY,
parameter int PMP_NUM_REGIONS
)(
// Clock and Reset
input wire clk_i,
Expand Down Expand Up @@ -84,14 +84,14 @@ module uvmt_cv32e40s_pmprvfi_assert

string info_tag = "CV32E40S_PMPRVFI_ASSERT";

localparam logic [1:0] MODE_U = 2'b 00;
localparam logic [1:0] MODE_M = 2'b 11;
localparam logic [2:0] DBG_TRIGGER = 3'd 2;
localparam int NUM_CFG_REGS = 16;
localparam int NUM_ADDR_REGS = 64;
localparam int CSRADDR_FIRST_PMPCFG = 12'h 3A0;
localparam int CSRADDR_FIRST_PMPADDR = 12'h 3B0;
localparam int CSRADDR_MSECCFG = 12'h 747;
localparam int NUM_ADDR_REGS = 64;
localparam int NUM_CFG_REGS = 16;
localparam logic [11:0] CSRADDR_FIRST_PMPADDR = 12'h 3B0;
localparam logic [11:0] CSRADDR_FIRST_PMPCFG = 12'h 3A0;
localparam logic [11:0] CSRADDR_MSECCFG = 12'h 747;
localparam logic [1:0] MODE_M = 2'b 11;
localparam logic [1:0] MODE_U = 2'b 00;
localparam logic [2:0] DBG_TRIGGER = 3'd 2;

typedef struct packed {
logic pc_lower;
Expand Down Expand Up @@ -222,6 +222,16 @@ module uvmt_cv32e40s_pmprvfi_assert
assign pmp_csr_rvfi_wdata.mseccfg = rvfi_csr_mseccfg_wdata;
assign pmp_csr_rvfi_wmask.mseccfg = rvfi_csr_mseccfg_wmask;

logic is_all_regions_off;
always_comb begin
is_all_regions_off = 1;
for (int i = 0; i < PMP_NUM_REGIONS; i++) begin
if (pmp_csr_rvfi_rdata.cfg[i].mode != '0) begin
is_all_regions_off = 0;
end
end
end


// Helper models

Expand Down Expand Up @@ -336,30 +346,22 @@ module uvmt_cv32e40s_pmprvfi_assert
.*
);

var [31:0] clk_cnt;
always @(posedge clk_i, negedge rst_ni) begin
if (rst_ni == 0) begin
clk_cnt <= 32'd 1;
end else if (clk_cnt != '1) begin
clk_cnt <= clk_cnt + 32'd 1;
end
end


// Assertions:


// PMP CSRs only accessible from M-mode (vplan:Csrs:MmodeOnly)
// PMP CSRs only accessible from M-mode (vplan:Csrs:MmodeOnly, vplan:MsecCfg:MmodeOnly)

sequence seq_csrs_mmode_only_ante;
sequence seq_pmp_csr_access(mode);
is_rvfi_csr_instr &&
(rvfi_mode == MODE_U) &&
(rvfi_mode == mode) &&
(rvfi_insn[31:20] inside {['h3A0 : 'h3EF], 'h747, 'h757}) //PMP regs
;
endsequence : seq_csrs_mmode_only_ante
endsequence

a_csrs_mmode_only: assert property (
seq_csrs_mmode_only_ante
seq_pmp_csr_access(MODE_U)
|->
is_rvfi_exc_ill_instr ||
is_rvfi_exc_instr_bus_fault ||
Expand All @@ -370,9 +372,16 @@ module uvmt_cv32e40s_pmprvfi_assert

cov_csrs_mmode_only: cover property (
// Want to see "the real cause" (ill exc) finishing this property
seq_csrs_mmode_only_ante ##0 is_rvfi_exc_ill_instr
seq_pmp_csr_access(MODE_U) ##0 is_rvfi_exc_ill_instr
);

// M-mode can always access the csrs (vplan:AlwaysAccessible)
a_always_accessible_mmode_csrs: assert property (
seq_pmp_csr_access(MODE_M)
|->
! is_rvfi_exc_ill_instr
) else `uvm_error(info_tag, "mmode couldn't access csr");


// NAPOT, some bits read as ones, depending on G (vplan:NapotOnes)

Expand Down Expand Up @@ -897,7 +906,7 @@ module uvmt_cv32e40s_pmprvfi_assert
csr_intended_wdata <=
rvfi_if.csr_intended_wdata(
({24'd 0, pmp_csr_rvfi_rdata.cfg[i]} << 8*(i%4)),
(CSRADDR_FIRST_PMPCFG + (i / 3'd4))
(CSRADDR_FIRST_PMPCFG + (i[11:0] / 3'd4))
);
end
wire pmpncfg_t cfg_attempt = csr_intended_wdata[32'd 8 * (i%4) +: 8];
Expand All @@ -906,7 +915,7 @@ module uvmt_cv32e40s_pmprvfi_assert
pmp_csr_rvfi_rdata.mseccfg.rlb &&
pmp_csr_rvfi_rdata.mseccfg.mml
##0
rvfi_if.is_csr_write(CSRADDR_FIRST_PMPCFG + (i / 3'd4)) &&
rvfi_if.is_csr_write(CSRADDR_FIRST_PMPCFG + (i[11:0] / 3'd4)) &&
!rvfi_trap &&
!(PMP_GRANULARITY > 0 && cfg_attempt.mode == PMP_MODE_NA4)
;
Expand All @@ -928,6 +937,23 @@ module uvmt_cv32e40s_pmprvfi_assert
);


// If all regions "OFF", U-mode fails (vplan:UmodeOff)

a_umode_off: assert property (
rvfi_if.is_umode &&
is_all_regions_off
|->
rvfi_if.rvfi_trap
);


// "mseccfgh" is just zero (vplan:MseccfghZero)

a_mseccfgh_zero: assert property (
rvfi_csr_mseccfgh_rdata == '0
) else `uvm_error(info_tag, "mseccfgh not zero");


// Translate write-attempts to legal values

function automatic pmpncfg_t rectify_cfg_write (pmpncfg_t cfg_pre, pmpncfg_t cfg_attempt);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -348,15 +348,23 @@ module uvmt_cv32e40s_rvfi_assert
) else `uvm_error(info_tag, "!store->!exce, exce->store");


// Disassembler

// Disassembler
a_unknowninstr_trap: assert property (
(rvfi_if.instr_asm.instr == UNKNOWN_INSTR) && rvfi_if.rvfi_valid
|->
rvfi_if.rvfi_trap.trap
) else `uvm_error(info_tag, "Unknown instruction is not trapped");


// Exception's don't update GPRs

a_exceptions_dont_update_gprs: assert property (
rvfi_valid && rvfi_trap.exception
|->
(rvfi_if.rvfi_rd1_addr == 0)
) else `uvm_error(info_tag, "exceptions shouldn't update gprs");


endmodule : uvmt_cv32e40s_rvfi_assert

Expand Down
File renamed without changes.
7 changes: 7 additions & 0 deletions cv32e40s/tb/uvmt/uvmt_cv32e40s_clic_interrupt_assert.sv
Original file line number Diff line number Diff line change
Expand Up @@ -780,6 +780,13 @@ module uvmt_cv32e40s_clic_interrupt_assert
end
end

covergroup cg_clic @(posedge clk_i);
option.per_instance = 1;
cp_lvl: coverpoint irq_level{ bins values[] = {[0:255]};}
endgroup

cg_clic clic_cg = new;


assign core_not_in_debug = debug_running;
assign core_in_debug = !core_not_in_debug;
Expand Down
4 changes: 2 additions & 2 deletions cv32e40s/tb/uvmt/uvmt_cv32e40s_tb_files.flist
Original file line number Diff line number Diff line change
Expand Up @@ -21,13 +21,13 @@ ${DV_UVMT_PATH}/uvmt_cv32e40s_tb.sv
${DV_UVMT_PATH}/../assertions/uvmt_cv32e40s_fencei_assert.sv
${DV_UVMT_PATH}/../assertions/uvmt_cv32e40s_pmp_assert.sv
${DV_UVMT_PATH}/../assertions/uvmt_cv32e40s_pmprvfi_assert.sv
${DV_UVMT_PATH}/../assertions/uvmt_cv32e40s_rvfi_assert.sv
${DV_UVMT_PATH}/../assertions/uvmt_cv32e40s_umode_assert.sv
${DV_UVMT_PATH}/uvmt_cv32e40s_clic_interrupt_assert.sv
${DV_UVMT_PATH}/uvmt_cv32e40s_debug_assert.sv
${DV_UVMT_PATH}/uvmt_cv32e40s_integration_assert.sv
${DV_UVMT_PATH}/uvmt_cv32e40s_interrupt_assert.sv
${DV_UVMT_PATH}/uvmt_cv32e40s_pma_assert.sv
${DV_UVMT_PATH}/uvmt_cv32e40s_rvfi_assert.sv
${DV_UVMT_PATH}/uvmt_cv32e40s_triggers_assert_cov.sv
${DV_UVMT_PATH}/uvmt_cv32e40s_xsecure_assert/uvmt_cv32e40s_xsecure_bus_protocol_hardening_assert.sv
${DV_UVMT_PATH}/uvmt_cv32e40s_xsecure_assert/uvmt_cv32e40s_xsecure_data_independent_timing_assert.sv
Expand All @@ -45,6 +45,7 @@ ${DV_UVMT_PATH}/uvmt_cv32e40s_zc_assert.sv

${DV_UVMT_PATH}/../assertions/uvmt_cv32e40s_pma_model.sv
${DV_UVMT_PATH}/../assertions/uvmt_cv32e40s_pmp_model.sv
${DV_UVMT_PATH}/../assertions/uvmt_cv32e40s_rvfi_cov.sv
${DV_UVMT_PATH}/../assertions/uvmt_cv32e40s_umode_cov.sv
${DV_UVMT_PATH}/support_logic/uvmt_cv32e40s_rchk_shim.sv
${DV_UVMT_PATH}/support_logic/uvmt_cv32e40s_sl_fifo.sv
Expand All @@ -53,4 +54,3 @@ ${DV_UVMT_PATH}/support_logic/uvmt_cv32e40s_sl_trigger_match.sv
${DV_UVMT_PATH}/support_logic/uvmt_cv32e40s_sl_trigger_match_mem.sv
${DV_UVMT_PATH}/support_logic/uvmt_cv32e40s_support_logic.sv
${DV_UVMT_PATH}/uvmt_cv32e40s_pma_cov.sv
${DV_UVMT_PATH}/uvmt_cv32e40s_rvfi_cov.sv
Loading

0 comments on commit eabbfa2

Please sign in to comment.