Add Formal Verification Flow Using Yosys's riscv-formal

.gitignore

@@ -21,4 +21,9 @@ __pycache__
 #cocotb build files
 *.log
 sim_build*/
-build/
+build/
+
+# formal verification artifacts
+formal/instructions/verify_instructions*/
+formal/*/verify_*/
+formal/verification_report.json

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "riscv-formal"]
+	path = riscv-formal
+	url = [email protected]:5iri/riscv-formal.git

README.md

@@ -122,6 +122,81 @@ The regression tests include:
 - [Chanchal Bahrani](https://github.com/Chanchal1010)
 - [Shri Vishakh Devanand](https://github.com/5iri)
 
+
+## Formal Verification
+
+Formal verification of the Synapse-32 CPU is performed using [Yosys's riscv-formal](https://github.com/cliffordwolf/riscv-formal) together with [SymbiYosys (SBY)](https://symbiyosys.readthedocs.io/en/latest/).
+
+### Prerequisites
+
+- [Yosys](https://yosyshq.net/yosys/)
+- [SymbiYosys (`sby`)](https://symbiyosys.readthedocs.io/en/latest/)
+- [Boolector](https://boolector.github.io/) (the `.sby` files are configured for `smtbmc boolector` by default) or another SMT solver supported by SymbiYosys
+- Python 3.8+
+
+Verify that these tools are in your `PATH`:
+
+```bash
+yosys -V
+sby --version
+boolector --version
+python3 --version
+```
+
+### Running the Suite
+
+The top-level driver lives in `formal/run_verification_suite.py` and automatically runs every integration, system, and per-instruction SymbiYosys job:
+
+```bash
+cd formal
+python3 run_verification_suite.py
+```
+
+Useful options:
+
+- `--workers N` limits the number of parallel jobs (defaults to the number of CPU cores, capped at 8).
+- `--timeout SECONDS` overrides the per-test timeout (default 300 s).
+- `--categories ...` narrows the run to any subset of `instructions`, `system`, `integration`.
+
+While the suite runs, live progress is printed, and a machine-readable summary is written to `formal/verification_report.json`. Individual job directories (e.g. `formal/instructions/verify_instructions_add/`) contain the SBY logs and traces for debugging failing proofs.
+
+### Cleaning Generated Artifacts
+
+The suite leaves only transient artifacts—handled by `.gitignore`—but you can wipe them manually when needed:
+
+```bash
+find formal/instructions -maxdepth 1 -type d -name 'verify_instructions*' -exec rm -rf {} +
+find formal -maxdepth 2 -type d -name 'verify_*' -exec rm -rf {} +
+rm -f formal/verification_report.json
+```
+
+### Verification Flow
+
+- Initialize the riscv-formal submodule (once per clone):
+  ```bash
+  git submodule update --init --recursive
+  ```
+- The verification environment is set up in the `formal/` directory, with integration tests and instruction-specific checks in subfolders.
+- SBY configuration files (e.g., `formal/integration/verify_rv32i.sby`) define the verification tasks, including the modules to check, properties to prove, and the engines to use. By default they use `smtbmc boolector`; to use another solver, edit the `[engines]` section accordingly.
+- The [riscv-formal](https://github.com/YosysHQ/riscv-formal) framework provides a set of formal properties for RISC-V cores, which are instantiated and checked against the Synapse-32 design.
+- To run a verification task, use:
+   ```bash
+   cd formal
+   python run_verification_suite.py
+   ```
+- The results and counterexamples (if any) are generated in the corresponding output folders.
+
+### What Is Verified
+
+- The CPU is checked for compliance with the RV32I instruction set and correct pipeline behavior.
+- Properties such as correct instruction execution, hazard handling, and control flow are formally proven using riscv-formal checkers.
+- Additional checks can be added for integration and fault scenarios.
+
+### Interpreting Results
+
+- If all properties are proven, the verification passes.
+- If a counterexample is found, the output folder will contain traces to help debug the issue.
+
 ### Acknowledgements and Resources
 
 - [SRA VJTI Eklavya 2023](https://sravjti.in/)

formal/instructions/instruction_list.txt

@@ -0,0 +1,45 @@
+add
+addi
+and
+andi
+auipc
+beq
+bge
+bgeu
+blt
+bltu
+bne
+div
+divu
+jal
+jalr
+lb
+lbu
+lh
+lhu
+lui
+lw
+mul
+mulh
+mulhsu
+mulhu
+or
+ori
+rem
+remu
+sb
+sh
+sll
+slli
+slt
+slti
+sltiu
+sltu
+sra
+srai
+srl
+srli
+sub
+sw
+xor
+xori

formal/instructions/verify_instructions.sby

@@ -0,0 +1,132 @@
+[tasks]
+--pycode-begin--
+with open("instruction_list.txt") as f:
+    for line in f:
+        name = line.strip()
+        if not name or name.startswith("#"):
+            continue
+        output(name)
+--pycode-end--
+
+[options]
+mode prove
+expect pass
+depth 20
+wait on
+
+[engines]
+smtbmc boolector
+
+[script]
+verilog_defines -D FORMAL
+verilog_defines -D RISCV_FORMAL_NRET=1
+verilog_defines -D RISCV_FORMAL_ILEN=32
+verilog_defines -D RISCV_FORMAL_XLEN=32
+verilog_defines -D RISCV_FORMAL_CHANNEL_IDX=0
+
+--pycode-begin--
+with open("instruction_list.txt") as f:
+    for line in f:
+        insn = line.strip()
+        if not insn or insn.startswith("#"):
+            continue
+        output(f"{insn}: verilog_defines -D RISCV_FORMAL_INSN_MODEL=rvfi_insn_{insn}")
+--pycode-end--
+
+--pycode-begin--
+design_sources = [
+    "top.v",
+    "riscv_cpu.v",
+    "data_mem.v",
+    "execution_unit.v",
+    "instr_mem.v",
+    "memory_unit.v",
+    "seven_seg.v",
+    "writeback.v",
+    "alu.v",
+    "csr_exec.v",
+    "csr_file.v",
+    "decoder.v",
+    "interrupt_controller.v",
+    "pc.v",
+    "registerfile.v",
+    "timer.v",
+    "uart.v",
+    "EX_MEM.v",
+    "forwarding_unit.v",
+    "ID_EX.v",
+    "IF_ID.v",
+    "load_use_detector.v",
+    "MEM_WB.v",
+    "store_load_detector.v",
+    "store_load_forward.v"
+]
+
+for src in design_sources:
+    output(f"read_verilog -formal {src}")
+--pycode-end--
+
+read_verilog -sv -formal instr_defines.vh
+read_verilog -sv -formal memory_map.vh
+read_verilog -sv -formal rvfi_macros.vh
+
+--pycode-begin--
+with open("instruction_list.txt") as f:
+    for line in f:
+        insn = line.strip()
+        if not insn or insn.startswith("#"):
+            continue
+        output(f"read_verilog -sv -formal insn_{insn}.v")
+--pycode-end--
+
+read_verilog -sv -formal rvfi_insn_check.sv
+
+hierarchy -top top
+proc
+opt
+memory -nomap
+flatten
+setundef -undriven -anyseq
+check
+stat
+
+[files]
+instruction_list.txt
+../../rtl/top.v
+../../rtl/riscv_cpu.v
+../../rtl/data_mem.v
+../../rtl/execution_unit.v
+../../rtl/instr_mem.v
+../../rtl/memory_unit.v
+../../rtl/seven_seg.v
+../../rtl/writeback.v
+../../rtl/core_modules/alu.v
+../../rtl/core_modules/csr_exec.v
+../../rtl/core_modules/csr_file.v
+../../rtl/core_modules/decoder.v
+../../rtl/core_modules/interrupt_controller.v
+../../rtl/core_modules/pc.v
+../../rtl/core_modules/registerfile.v
+../../rtl/core_modules/timer.v
+../../rtl/core_modules/uart.v
+../../rtl/pipeline_stages/EX_MEM.v
+../../rtl/pipeline_stages/forwarding_unit.v
+../../rtl/pipeline_stages/ID_EX.v
+../../rtl/pipeline_stages/IF_ID.v
+../../rtl/pipeline_stages/load_use_detector.v
+../../rtl/pipeline_stages/MEM_WB.v
+../../rtl/pipeline_stages/store_load_detector.v
+../../rtl/pipeline_stages/store_load_forward.v
+../../rtl/include/instr_defines.vh
+../../rtl/include/memory_map.vh
+../../riscv-formal/checks/rvfi_macros.vh
+../../riscv-formal/checks/rvfi_insn_check.sv
+
+--pycode-begin--
+with open("instruction_list.txt") as f:
+    for line in f:
+        insn = line.strip()
+        if not insn or insn.startswith("#"):
+            continue
+        output(f"../../riscv-formal/insns/insn_{insn}.v")
+--pycode-end--