detect pma load/store fault, use in assert #2332
Conversation
silabs-robin
force-pushed
the
pma_subsequents_fix
branch
from
ba42eb6
to
ecf2c83
Compare
Signed-off-by: Robin Pedersen <Robin.Pedersen@silabs.com>
silabs-robin
force-pushed
the
pma_subsequents_fix
branch
from
ecf2c83
to
6a1f2f7
Compare
| @@ -174,6 +182,16 @@ module uvmt_cv32e40s_pma_assert | |||
| ); | |||
|
|
|||
|
|
|||
| // PMA-deny on instr, no mem op (vplan: Not a vplan item. Inspo from a_failure_denies_subsequents.) | |||
|
|
|||
| a_failure_denies_memops: assert property ( | |||
There was a problem hiding this comment.
Here is the old assert, with a new name, because it was somewhat useful still.
There was a problem hiding this comment.
If this assertion is necessary shouldnt we add it to the vplan? Or is it somehow a support assert for another assert (listed in a vplan)?
There was a problem hiding this comment.
In principle it could be added to the vplan.
But since this is a very minor extra check, I don't think it is worth the effort.
| |-> | ||
| (rvfi_instr_if.rvfi_mem_wmask != rvfi_instr_if.rvfi_mem_wmask_intended) | ||
| || | ||
| (rvfi_instr_if.rvfi_mem_wmask == 'd 0) |
There was a problem hiding this comment.
Luckily, we had the rvfi_mem_wmask_intended signal from before. 🙇
There was a problem hiding this comment.
is || (rvfi_instr_if.rvfi_mem_wmask == 'd 0) necessary?
There was a problem hiding this comment.
This might be unnecessary, but not breaking, so we let it lie.
There was a problem hiding this comment.
is || (rvfi_instr_if.rvfi_mem_wmask == 'd 0) necessary?
It would look more sensible if it said:
|| (rvfi_instr_if.rvfi_mem_wmask_intended == 'd 0)
The point is:
Either "actual" is short of "intended", or nothing was intended at all.
Or, it might have been a better fit to have it as a constraint in the antecedent.
There was a problem hiding this comment.
It is not unnecessary. It was found by a CEX.
| @@ -146,12 +146,20 @@ module uvmt_cv32e40s_pma_assert | |||
|
|
|||
| // After PMA-deny, subsequent accesses are also suppressed (vplan:"Multi-memory operation instructions") | |||
|
|
|||
| a_failure_denies_subsequents: assert property ( | |||
| rvfi_instr_if.is_pma_instr_fault | |||
| a_failure_denies_subsequents_loads: assert property ( | |||
There was a problem hiding this comment.
I see you have changed the assertion name. Is this something that should be updated in link to coverage in a vplan?
There was a problem hiding this comment.
That kind of work is better suited for a machine than a human.
And we are in the process of revising the vplan system to facilitate more automation.
Can this be the first challenge for a new automated system to sort out?
Or is the benefit of doing it manually today so big that it is warranted?
(Note that the name's prefix is the same, so the linkage is not 100% broken.)
(Note also that no testing has been removed, so the vplan is not more lacking after this PR.)
| |-> | ||
| (rvfi_instr_if.rvfi_mem_wmask != rvfi_instr_if.rvfi_mem_wmask_intended) | ||
| || | ||
| (rvfi_instr_if.rvfi_mem_wmask == 'd 0) |
There was a problem hiding this comment.
This might be unnecessary, but not breaking, so we let it lie.
This PR fixes an erronous assert, and two TODOs within it.
Test status: