Skip to content

Commit

Permalink
Merge pull request #2265 from silabs-hfegran/dev_hf_fixed_pmp_assertion
Browse files Browse the repository at this point in the history
Fixed pmp-assertion
  • Loading branch information
silabs-robin authored Oct 31, 2023
2 parents a616908 + 6f8db81 commit 7741619
Showing 1 changed file with 13 additions and 8 deletions.
21 changes: 13 additions & 8 deletions cv32e40s/tb/uvmt/uvmt_cv32e40s_pmp_assert.sv
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,6 @@ module uvmt_cv32e40s_pmp_assert
.*
);


// Extra covers and asserts to comprehensively match the spec

// Cover the helper-RTL internals
Expand Down Expand Up @@ -318,14 +317,20 @@ module uvmt_cv32e40s_pmp_assert
// such pmpcfg writes are ignored, leaving pmpcfg unchanged. This restriction can be temporarily lifted
// e.g. during the boot process, by setting mseccfg.RLB.
// (vplan:ExecIgnored)

property p_mmode_only_or_shared_executable_ignore;
logic [3:0] lrwx;
csr_pmp_i.mseccfg.mml === 1'b1 &&
csr_pmp_i.mseccfg.rlb === 1'b0 ##1
($changed(csr_pmp_i.cfg[region]),
lrwx = { csr_pmp_i.cfg[region].lock, csr_pmp_i.cfg[region].read, csr_pmp_i.cfg[region].write, csr_pmp_i.cfg[region].exec }
)
|->
!(lrwx inside { 4'b1?01, 4'b101? });
endproperty : p_mmode_only_or_shared_executable_ignore

a_mmode_only_or_shared_executable_ignore: assert property (
csr_pmp_i.mseccfg.mml === 1'b1 && csr_pmp_i.mseccfg.rlb === 1'b0 |=>
$stable(csr_pmp_i.cfg[region])
or
not ($changed(csr_pmp_i.cfg[region]) ##0
csr_pmp_i.cfg[region].lock === 1'b1 ##0
csr_pmp_i.cfg[region].read === 1'b0 ##0
csr_pmp_i.cfg[region].write || csr_pmp_i.cfg[region].exec)
p_mmode_only_or_shared_executable_ignore
) else `uvm_error(info_tag, "certain rules can't be added");

cov_mmode_only_or_shared_executable: cover property (
Expand Down

0 comments on commit 7741619

Please sign in to comment.