Formal cleanup #2245
Draft
Formal cleanup #2245
Conversation
This file contains 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
| @@ -5,6 +5,15 @@ Prerequisities (in your PATH): | |||
| - [psgen](https://github.com/mndstrmr/psgen) | |||
|
|
|||
| Build instructions: | |||
| - Clone this repository | |||
| - `cd dv/formal` | |||
| - `nix develop .#formal` | |||
There was a problem hiding this comment.
Hmm. I don't think I know where this flake gets defined. (Maybe just pull this line to the following commit?)
There was a problem hiding this comment.
This flake is at the root of the repo. Nix automatically searches up parent directories within the same repo.
There was a problem hiding this comment.
Sorry, that wasn't very clear of me. I think the "formal" flake is only defined in the next commit. To avoid a commit with inconsistent documentation, maybe it's worth moving this line to the next commit.
marnovandermaas
force-pushed
the
formal_cleanup
branch
2 times, most recently
from
7cd534d to
82bc8ad
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 <mvdmaas+git@lowrisc.org>
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. This also allows us to automatically patch the fusesoc-provided src files to work around some current restrictions in the formal flow, without modifying the main repository tree. Signed-off-by: Harry Callahan <hcallahan@lowrisc.org>
This includes Flake setup prove_no_liveness isn't great by any means, but it will prove everything orders of magnitude faster than prove -bg -all. 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. 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 <louis-emile.ploix@lowrisc.org> Co-authored-by: Marno van der Maas <mvdmaas+git@lowrisc.org> Signed-off-by: Harry Callahan <hcallahan@lowrisc.org>
This includes renaming Jasper Gold to just Jasper
Mostly line lengths and indexes. This commits also adds a Verible waiver file.
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 Ibex_FetchErrRoot is producing a counter-example. |
marnovandermaas
force-pushed
the
formal_cleanup
branch
from
9a5fdd5 to
d50fe25
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.