core-v-verif
core-v-verif copied to clipboard
openhwgroup
User-mode Asserts
SVAs for checking user-mode, according to the vplan https://github.com/openhwgroup/core-v-verif/issues/1256.
Note, rtl is not ready to pass everything yet, and rvfi updates are needed. (But our test stimuli doesn't exercise user-mode yet so it is still expected that these asserts will not cause failures in simulation.)
Note, the vplan review is not done, so these asserts might see future updates. (Which would not be unlikely otherwise anyway.)
This does not pass ci_check yet, because the core hash was updated and this necessitates iss-related updates. Hence, the pr is a "draft". After a separate pull request has fixed the core-updating issue, then I will merge from 40s/dev into this pr branch, make sure ci_check passes, and remove the "draft" status.
Great stuff @silabs-robin. General question: are these assertions intented to be used for both formal and simulation? If so, which set of assumptions are required to use formal?
are these assertions intented to be used for both formal and simulation? If so, which set of assumptions are required to use formal?
No additional assumptions should be needed for these user-mode asserts. For all the assertion files we have, only general assumes are required (obi protocol, no "scan_cg_en", no Xes from blackboxed multiplier, input addresses stable after "fetch_enable").
Just a small update on this: It was pending on some fixes in "cv32e40s/dev" which are now in, but also the vplan review meeting led to some vplan fixes that will be incorporated in the assertions as well, and it is also pending on some rvfi fixes, etc. So this is on halt for a while longer.
I am back on this branch. Will close and re-open when ready, in case people are "subscribed" to this PR.