End-to-End Formal Verification of Ibex Trace Equivalence against the Sail Model #2245
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This comment was marked as outdated.
This comment was marked as outdated.
marnovandermaas
force-pushed
the
formal_cleanup
branch
from
98d948d to
d1ddec1
Compare
rswarbrick
reviewed
Jan 13, 2025
marnovandermaas
force-pushed
the
formal_cleanup
branch
2 times, most recently
from
7cd534d to
82bc8ad
Compare
rswarbrick
approved these changes
Jan 27, 2025
marnovandermaas
force-pushed
the
formal_cleanup
branch
from
82bc8ad to
9a5fdd5
Compare
|
I'm converting this back to draft because |
marnovandermaas
force-pushed
the
formal_cleanup
branch
from
9a5fdd5 to
d50fe25
Compare
nbdd0121
force-pushed
the
formal_cleanup
branch
from
d50fe25 to
fce84f6
Compare
|
I made a change to our fork of sail and updated the flake.lock which should address the |
nbdd0121
force-pushed
the
formal_cleanup
branch
from
fce84f6 to
4cc9061
Compare
Here's a high-level overview of what this commit does: - Compiles Sail into SystemVerilog including patchin compiler bugs - Create a TCL file that tells JasperGold what to prove and assume - Check memory operations modelling the LSU Most of these properties now prove without time-bound on the response from memory due to alternative LSUs - Check memory even with Smepmp errors: Continues on top of riscv/sail-riscv#196 - CSR verification - Checks for instruction types such as B-Type, I-Type, R-Type - Check illegal instructions and WFI instructions - Using psgen language for proof generation - Documentation on how to use the setup - Wrap around proof that proves instructions executed in a row still match the specification. - Liveness proof to guarantee instructions will retire within a upper bound of cycles. All of these proofs make heavy use of the concept of k-induction. All the different properties and steps are necessary to help the tool get the useful properties it needs to prove the next step. The instruction correctness, wrap-around and liveness all give us increased confidence that Ibex is trace-equivalent to Sail. Throughout this process an issue was found in Ibex where the pipeline was not flushing properly on changing PMP registers using clear: lowRISC#2193 Alternative LSUs: This makes all top level memory properties prove quickly and at a low proof effort (1 or 2-induction). Three 'alternative LSUs' representing three stages of memory instructions: 1. Before the first response is received, in the EX stage 2. After the first response is received, but not the second grant, also in the EX stage 3. Before the last response is received in the WB stage. In each case we ask 'if the response came now, would the result be correct?'. Similar is applied for CSRs/PC though less directly. This is particularly interesting (read: ugly) in the case of a PMP error wbexc_exists makes Wrap properties fast to prove. The bottleneck becomes SpecPastNoWbexcPC, which fails only due to a bug. See the comment in riscv.proof. Co-authored-by: Marno van der Maas <[email protected]> Signed-off-by: Louis-Emile Ploix <[email protected]>
This lets fusesoc do the heavy lifting in identify the correct files for us. Fusesoc is already extensively used for this purpose for synthesis and simulation. As part of this step, apply RTL patches that work around some current restrictions in the formal flow to the /build fileset copied by fusesoc. Co-authored-by: Gary Guo <[email protected]> Signed-off-by: Harry Callahan <[email protected]>
Adds a Nix environment which provides a development shell for the formal verification flow. All dependencies are fetched and built upon entering the shell (nix develop .#formal), except for the proprietary Cadence Jasper. The dev shell (nix develop .#formal-dev) is identical to the normal shell, but prints some information on how to swap out components. This is also documented in the README. Documentation on how to use this environment is added to the dv/formal/README.md The provided Makefile/.tcl scripts make assumptions about the environment they are run within which are provided by the Nix environment. Using Nix is the recommended way to run this flow, but if you cannot do this, you will need to duplicate the setup done by Nix in terms of environment variables and provided dependencies. Jasper Gold options: - allow_unsupported_OS is required on both the machines I use. - acquire_proj means that if JG is killed (which happens somewhat often) the next it runs it will still be able to take ownership of the project. Co-authored-by: Louis-Emile Ploix <[email protected]> Co-authored-by: Marno van der Maas <[email protected]> Co-authored-by: Gary Guo <[email protected]> Signed-off-by: Harry Callahan <[email protected]>
This includes renaming Jasper Gold to just Jasper Signed-off-by: Marno van der Maas <[email protected]>
M extension is not currently proven. This should be disabled rather than assumed as otherwise its property might be used to prove other properties in the same step (and thus not performing actual work). Signed-off-by: Gary Guo <[email protected]>
hcallahan-lowrisc
force-pushed
the
formal_cleanup
branch
from
4cc9061 to
9400123
Compare
hcallahan-lowrisc
approved these changes
Apr 27, 2025
There was a problem hiding this comment.
I've tidied up the commits and messages, including some final revisions to the documentation and build instructions. Everything looks good and clean to me, hence I think it is ready to go in. I'll remove the draft status.
@marnovandermaas I'll leave the final merge to you. But as it is now, LGTM. Really great work here.
hcallahan-lowrisc
changed the title
marnovandermaas
commented
Apr 28, 2025
FetchErrRoot is very slow to prove, and via SST I discovered that it was exploring the state space where ctrl FSM is in FIRST_FETCH, and there was a memory load instruction latched by IF, and it causes the stall logic to think there is a memory-induced stall. This is unreachable state because in FIRST_FETCH there can't be instructions latched, so add a helper property to aid the proof. Signed-off-by: Gary Guo <[email protected]>
These values were originally constants but now are parameters. Constrain them for formal. Signed-off-by: Gary Guo <[email protected]>
marnovandermaas
force-pushed
the
formal_cleanup
branch
from
9400123 to
2130ec5
Compare
|
This looks great, thanks for the updates everyone! I have a couple of small improvements coming hopefully today (removing the patches mostly) but after that I'm also happy for it to be merged. |
|
Ok, I've confirmed the proof is conclusive. I'll wait for @mndstrmr to add his fixes before merging. Feel free to add to this PR. |
|
Should all be good now, I'm happy for this to be merged if others are. |
|
Thanks @mndstrmr I just finished the proof and it is conclusive, so I am going to merge this. The |
The old patchfile disabled clock gating and set ResetAll = 1. We don't need either of these things any more with some minor invariant tweaks. This also improves the proof script, which should be faster now.
marnovandermaas
force-pushed
the
formal_cleanup
branch
from
54c44f4 to
deb67f4
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This adds an initial formal flow to the Ibex repository. It proves equivalence of the Ibex RTL and the Sail specification. For details and limitations please see the documentation.
A big thank you to @mndstrmr and @hcallahan-lowrisc for putting this work together.