Add Formal Verification Flow Using Yosys's riscv-formal#16
Open
5iri wants to merge 9 commits intoSRA-VJTI:mainfrom
Open
Add Formal Verification Flow Using Yosys's riscv-formal#165iri wants to merge 9 commits intoSRA-VJTI:mainfrom
5iri wants to merge 9 commits intoSRA-VJTI:mainfrom
Conversation
Member
|
Is this ready for review? |
Member
Author
|
yes @SuperChamp234 |
Member
Author
|
@SuperChamp234 can you review now? I have reduced the line size by a lot now :) |
Contributor
There was a problem hiding this comment.
Pull Request Overview
This PR introduces formal verification infrastructure for the Synapse-32 CPU core using Yosys's riscv-formal framework and SymbiYosys. The changes include:
- RVFI (RISC-V Formal Interface) implementation in the CPU and top-level modules
- Formal verification scripts and configuration files for instruction-level and system-level checks
- Test infrastructure with parallel execution support
- Documentation updates explaining the verification workflow
Reviewed Changes
Copilot reviewed 35 out of 35 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| rtl/riscv_cpu.v | Added RVFI output ports and logic to track instruction execution for formal verification |
| rtl/top.v | Added RVFI interface ports and conditional memory sizing for formal vs functional builds |
| rtl/core_modules/alu.v | Added simplified ALU implementation for formal verification mode |
| rtl/execution_unit.v | Fixed ALU output connections from hierarchical to wire-based references |
| rtl/data_mem.v | Moved loop variable declarations outside initial blocks for synthesis compatibility |
| rtl/instr_mem.v | Moved local variables outside always blocks to module scope |
| rtl/core_modules/uart.v | Complete rewrite to single always_comb block with next-state logic pattern |
| rtl/core_modules/csr_file.v | Exposed CSR registers as module outputs for external access |
| rtl/pipeline_stages/*.v | Added RVFI-related signals propagation through pipeline stages |
| formal/ | Added comprehensive verification infrastructure with scripts, configs, and test suites |
| tests/unit_tests/*.py | Added PATH manipulation for tool discovery in test environments |
| README.md | Added formal verification documentation section |
| .gitmodules | Added riscv-formal submodule reference |
Comments suppressed due to low confidence (1)
rtl/riscv_cpu.v:1
- Inconsistent indentation: these two lines should align with the indentation of surrounding port connections (lines 375-376 have different indentation than line 337).
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Contributor
There was a problem hiding this comment.
Pull Request Overview
Copilot reviewed 34 out of 35 changed files in this pull request and generated 3 comments.
Comments suppressed due to low confidence (3)
rtl/riscv_cpu.v:1
- Removed the
default_nettype nonedirective without explanation. This directive helps catch typos by requiring explicit wire declarations. Consider documenting why it was removed or restoring it if there's no technical reason for its removal.
rtl/riscv_cpu.v:1 - The load mask calculation for halfword loads (line 665) shifts by addr[1:0], which can be 0, 1, 2, or 3. However, when addr[0] is 1 (misaligned), it returns 0, but when addr[0] is 0, it shifts 4'b0011 by addr[1:0]. If addr[1:0] is 2, this shifts to 4'b1100, which is correct. But the shift amount should only use addr[1] since halfwords are 2-byte aligned. Use
4'b0011 << {addr[1], 1'b0}instead.
tests/unit_tests/test_alu.py:1 - The unused import of
Pathwas removed, but the newprepend_to_pathcontext manager (lines 9-27) is duplicated across both test files (test_alu.py and test_decoder_gcc.py). Consider moving this to a shared utility module to avoid duplication.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Contributor
There was a problem hiding this comment.
Pull Request Overview
Copilot reviewed 34 out of 35 changed files in this pull request and generated 3 comments.
Comments suppressed due to low confidence (2)
rtl/riscv_cpu.v:1
- These magic numbers (2'b11 for Machine mode, 2'b01 for RV32) should be defined as named constants or documented with references to the RISC-V specification sections that define these values.
rtl/execution_unit.v:1 - [nitpick] Inconsistent indentation: these lines are not aligned with other port connections in the same instantiation (line 375-376 vs surrounding lines).
`default_nettype none
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Member
Author
|
@SuperChamp234 this pr is ready for review now, please check! |
Member
Author
|
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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 PR adds documentation and configuration for formal verification of the Synapse-32 CPU core using Yosys's riscv-formal and SymbiYosys.
The README is updated to explain the verification flow, including how to run SBY tasks, what is checked, and how to interpret results.
Changes