diff --git a/.gitignore b/.gitignore index c8e53dd..6d69192 100644 --- a/.gitignore +++ b/.gitignore @@ -21,4 +21,9 @@ __pycache__ #cocotb build files *.log sim_build*/ -build/ \ No newline at end of file +build/ + +# formal verification artifacts +formal/instructions/verify_instructions*/ +formal/*/verify_*/ +formal/verification_report.json diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..aceae0c --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "riscv-formal"] + path = riscv-formal + url = https://github.com/YosysHQ/riscv-formal.git diff --git a/README.md b/README.md index ffe8df1..64706a6 100644 --- a/README.md +++ b/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/) diff --git a/formal/instructions/instruction_list.txt b/formal/instructions/instruction_list.txt new file mode 100644 index 0000000..12a7e11 --- /dev/null +++ b/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 diff --git a/formal/instructions/verify_instructions.sby b/formal/instructions/verify_instructions.sby new file mode 100644 index 0000000..ca8d4df --- /dev/null +++ b/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-- diff --git a/formal/integration/verify_cover.sby b/formal/integration/verify_cover.sby new file mode 100644 index 0000000..76a4a43 --- /dev/null +++ b/formal/integration/verify_cover.sby @@ -0,0 +1,129 @@ +[options] +mode prove +expect pass +depth 50 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Complete ISA verification for COVER --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# Complete ISA verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 insn_c*.v + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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/insns/insn_c_add.v +../../riscv-formal/insns/insn_c_addi.v +../../riscv-formal/insns/insn_c_addi16sp.v +../../riscv-formal/insns/insn_c_addi4spn.v +../../riscv-formal/insns/insn_c_addiw.v +../../riscv-formal/insns/insn_c_addw.v +../../riscv-formal/insns/insn_c_and.v +../../riscv-formal/insns/insn_c_andi.v +../../riscv-formal/insns/insn_c_beqz.v +../../riscv-formal/insns/insn_c_bnez.v +../../riscv-formal/insns/insn_c_j.v +../../riscv-formal/insns/insn_c_jal.v +../../riscv-formal/insns/insn_c_jalr.v +../../riscv-formal/insns/insn_c_jr.v +../../riscv-formal/insns/insn_c_ld.v +../../riscv-formal/insns/insn_c_ldsp.v +../../riscv-formal/insns/insn_c_li.v +../../riscv-formal/insns/insn_c_lui.v +../../riscv-formal/insns/insn_c_lw.v +../../riscv-formal/insns/insn_c_lwsp.v +../../riscv-formal/insns/insn_c_mv.v +../../riscv-formal/insns/insn_c_or.v +../../riscv-formal/insns/insn_c_sd.v +../../riscv-formal/insns/insn_c_sdsp.v +../../riscv-formal/insns/insn_c_slli.v +../../riscv-formal/insns/insn_c_srai.v +../../riscv-formal/insns/insn_c_srli.v +../../riscv-formal/insns/insn_c_sub.v +../../riscv-formal/insns/insn_c_subw.v +../../riscv-formal/insns/insn_c_sw.v +../../riscv-formal/insns/insn_c_swsp.v +../../riscv-formal/insns/insn_c_xor.v +../../riscv-formal/insns/insn_clmul.v +../../riscv-formal/insns/insn_clmulh.v +../../riscv-formal/insns/insn_clmulr.v +../../riscv-formal/insns/insn_clz.v +../../riscv-formal/insns/insn_clzw.v +../../riscv-formal/insns/insn_cpop.v +../../riscv-formal/insns/insn_cpopw.v +../../riscv-formal/insns/insn_ctz.v +../../riscv-formal/insns/insn_ctzw.v diff --git a/formal/integration/verify_fault.sby b/formal/integration/verify_fault.sby new file mode 100644 index 0000000..20cd270 --- /dev/null +++ b/formal/integration/verify_fault.sby @@ -0,0 +1,89 @@ +[options] +mode prove +expect pass +depth 50 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Complete ISA verification for FAULT --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# Complete ISA verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_rv32i_insn.v + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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/tests/coverage/riscv_rv32i_insn.v diff --git a/formal/integration/verify_rv32i.sby b/formal/integration/verify_rv32i.sby new file mode 100644 index 0000000..83a7c3b --- /dev/null +++ b/formal/integration/verify_rv32i.sby @@ -0,0 +1,91 @@ +[options] +mode prove +expect pass +depth 50 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Complete ISA verification for RV32I --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# Complete ISA verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 isa_rv32i.v +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 isa_rv32iZbkx.v + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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/insns/isa_rv32i.v +../../riscv-formal/insns/isa_rv32iZbkx.v diff --git a/formal/integration/verify_rv32mi.sby b/formal/integration/verify_rv32mi.sby new file mode 100644 index 0000000..6042435 --- /dev/null +++ b/formal/integration/verify_rv32mi.sby @@ -0,0 +1,89 @@ +[options] +mode prove +expect pass +depth 50 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Complete ISA verification for RV32IM --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# Complete ISA verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 isa_rv32im.v + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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/insns/isa_rv32im.v diff --git a/formal/riscv_formal.sby b/formal/riscv_formal.sby new file mode 100644 index 0000000..f27259c --- /dev/null +++ b/formal/riscv_formal.sby @@ -0,0 +1,94 @@ +[options] +mode prove +expect pass +wait on + +[engines] +smtbmc boolector + +[script] +# --- Design files --- +read_verilog -DFORMAL top.v +read_verilog -DFORMAL riscv_cpu.v +read_verilog -DFORMAL data_mem.v +read_verilog -DFORMAL execution_unit.v +read_verilog -DFORMAL instr_mem.v +read_verilog -DFORMAL memory_unit.v +read_verilog -DFORMAL seven_seg.v +read_verilog -DFORMAL writeback.v + +# Core modules +read_verilog -DFORMAL alu.v +read_verilog -DFORMAL csr_exec.v +read_verilog -DFORMAL csr_file.v +read_verilog -DFORMAL decoder.v +read_verilog -DFORMAL interrupt_controller.v +read_verilog -DFORMAL pc.v +read_verilog -DFORMAL registerfile.v +read_verilog -DFORMAL timer.v +read_verilog -DFORMAL uart.v + +# Pipeline stages +read_verilog -DFORMAL EX_MEM.v +read_verilog -DFORMAL forwarding_unit.v +read_verilog -DFORMAL ID_EX.v +read_verilog -DFORMAL IF_ID.v +read_verilog -DFORMAL load_use_detector.v +read_verilog -DFORMAL MEM_WB.v +read_verilog -DFORMAL store_load_detector.v +read_verilog -DFORMAL store_load_forward.v + +# Includes +read_verilog -DFORMAL instr_defines.vh +read_verilog -DFORMAL memory_map.vh + +# riscv-formal checks +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_INSN_MODEL=rvfi_insn_model -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_INSN_MODEL=rvfi_insn_model -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_insn_check.sv +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_INSN_MODEL=rvfi_insn_model -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_reg_check.sv +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_INSN_MODEL=rvfi_insn_model -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_pc_fwd_check.sv +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_INSN_MODEL=rvfi_insn_model -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_pc_bwd_check.sv + +# --- Ordered passes (fixes "run proc first", keeps big RAM abstract) --- +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../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_insn_check.sv +../riscv-formal/checks/rvfi_reg_check.sv +../riscv-formal/checks/rvfi_pc_fwd_check.sv +../riscv-formal/checks/rvfi_pc_bwd_check.sv +../riscv-formal/checks/rvfi_macros.vh diff --git a/formal/run_verification_suite.py b/formal/run_verification_suite.py new file mode 100644 index 0000000..41be34b --- /dev/null +++ b/formal/run_verification_suite.py @@ -0,0 +1,418 @@ +#!/usr/bin/env python3 +""" +RISC-V CPU Formal Verification Suite Runner +Runs comprehensive verification tests with parallel execution and reporting. +""" + +import os +import sys +import time +import subprocess +import multiprocessing +import shutil +from pathlib import Path +from concurrent.futures import ThreadPoolExecutor, as_completed +from dataclasses import dataclass +from typing import List, Optional, Tuple +import json +import argparse + +@dataclass +class TestResult: + """Data class to store test results.""" + test_name: str + category: str + status: str # "PASS", "FAIL", "TIMEOUT", "ERROR" + duration: float + log_file: Optional[str] = None + error_message: Optional[str] = None + +class VerificationSuiteRunner: + """Main class for running the verification suite.""" + + def __init__(self, max_workers: int = None, timeout: int = 300): + # Cap parallelism to 8 to avoid overwhelming solvers/CPU memory usage on + # larger SBY jobs; this proved a stable default for typical workstation setups. + self.max_workers = max_workers or min(multiprocessing.cpu_count(), 8) + self.timeout = timeout + self.results: List[TestResult] = [] + self.start_time = None + + def load_instruction_list(self, list_file: Path) -> List[str]: + """Load instruction names from a list file.""" + if not list_file.exists(): + return [] + + instructions = [] + with open(list_file) as f: + for line in f: + name = line.strip() + if not name or name.startswith("#"): + continue + instructions.append(name) + return instructions + + def find_test_files(self, test_dir: Path) -> List[Tuple[Path, Optional[str]]]: + """Find all .sby test files (and associated tasks) in a directory.""" + if not test_dir.exists(): + return [] + test_entries: List[Tuple[Path, Optional[str]]] = [] + + for test_file in sorted(test_dir.glob("*.sby")): + if test_file.name == "verify_instructions.sby": + instruction_list = self.load_instruction_list(test_dir / "instruction_list.txt") + if instruction_list: + for insn in instruction_list: + test_entries.append((test_file, insn)) + continue + test_entries.append((test_file, None)) + + return test_entries + + def format_test_name(self, test_file: Path, task: Optional[str]) -> str: + """Create a human-readable test name.""" + if task: + return f"{task}" + return test_file.stem + + def run_single_test(self, test_file: Path, task: Optional[str], category: str) -> TestResult: + """Run a single SBY test and return the result.""" + test_name = self.format_test_name(test_file, task) + start_time = time.time() + + try: + # Create command + cmd = ["sby", "-f", str(test_file)] + if task: + cmd.append(task) + + # Run the test with timeout + process = subprocess.run( + cmd, + cwd=test_file.parent, + capture_output=True, + text=True, + timeout=self.timeout + ) + + duration = time.time() - start_time + + # Determine status based on return code + if process.returncode == 0: + status = "PASS" + error_message = None + else: + status = "FAIL" + error_message = process.stderr or process.stdout + + # Find log file if it exists + job_dir_name = f"{test_file.stem}_{task}" if task else test_file.stem + log_dir = test_file.parent / job_dir_name + log_file = None + if log_dir.exists(): + log_files = list(log_dir.glob("**/*.log")) + if log_files: + log_file = str(log_files[0]) + + return TestResult( + test_name=test_name, + category=category, + status=status, + duration=duration, + log_file=log_file, + error_message=error_message + ) + + except subprocess.TimeoutExpired: + duration = time.time() - start_time + return TestResult( + test_name=test_name, + category=category, + status="TIMEOUT", + duration=duration, + error_message=f"Test timed out after {self.timeout} seconds" + ) + + except Exception as e: + duration = time.time() - start_time + return TestResult( + test_name=test_name, + category=category, + status="ERROR", + duration=duration, + error_message=str(e) + ) + + def run_tests_parallel(self, test_files: List[Tuple[Path, Optional[str], str]]) -> List[TestResult]: + """Run tests in parallel using ThreadPoolExecutor.""" + results = [] + + with ThreadPoolExecutor(max_workers=self.max_workers) as executor: + # Submit all tests + future_to_test = { + executor.submit(self.run_single_test, test_file, task, category): (self.format_test_name(test_file, task), category) + for test_file, task, category in test_files + } + + # Collect results as they complete + for future in as_completed(future_to_test): + test_name, category = future_to_test[future] + try: + result = future.result() + results.append(result) + + # Print progress + status_symbol = { + "PASS": "[PASS]", + "FAIL": "[FAIL]", + "TIMEOUT": "[TIMEOUT]", + "ERROR": "[ERROR]" + }.get(result.status, "[UNKNOWN]") + + print(f"{status_symbol} [{category:12}] {result.test_name:20} - {result.status:8} ({result.duration:.2f}s)") + + except Exception as e: + print(f"[ERROR] [{category:12}] {test_name:20} - Exception: {e}") + + return results + + def generate_summary_report(self) -> str: + """Generate a comprehensive summary report.""" + if not self.results: + return "No test results available." + + # Count results by category and status + category_stats = {} + status_counts = {"PASS": 0, "FAIL": 0, "TIMEOUT": 0, "ERROR": 0} + + for result in self.results: + # Update overall status counts + status_counts[result.status] += 1 + + # Update category stats + if result.category not in category_stats: + category_stats[result.category] = {"PASS": 0, "FAIL": 0, "TIMEOUT": 0, "ERROR": 0} + category_stats[result.category][result.status] += 1 + + # Calculate durations + total_duration = sum(r.duration for r in self.results) + wall_time = time.time() - self.start_time if self.start_time else 0 + + # Build report + report = [] + report.append("RISC-V CPU Formal Verification Summary Report") + report.append("=" * 60) + report.append(f"Total Tests: {len(self.results)}") + report.append(f"Wall Time: {wall_time:.2f} seconds") + report.append(f"CPU Time: {total_duration:.2f} seconds") + report.append(f"Speedup: {total_duration/wall_time:.2f}x" if wall_time > 0 else "Speedup: N/A") + report.append("") + + # Overall status summary + report.append("Overall Results:") + for status, count in status_counts.items(): + percentage = (count / len(self.results)) * 100 + symbol = {"PASS": "[PASS]", "FAIL": "[FAIL]", "TIMEOUT": "[TIMEOUT]", "ERROR": "[ERROR]"}[status] + report.append(f" {symbol} {status:8}: {count:3} tests ({percentage:5.1f}%)") + report.append("") + + # Category breakdown + report.append("Results by Category:") + for category, stats in category_stats.items(): + total_cat = sum(stats.values()) + pass_rate = (stats["PASS"] / total_cat) * 100 if total_cat > 0 else 0 + report.append(f" {category:15}: {stats['PASS']:2}/{total_cat:2} passed ({pass_rate:5.1f}%)") + report.append("") + + # Failed tests details + failed_tests = [r for r in self.results if r.status != "PASS"] + if failed_tests: + report.append("Failed Tests:") + for result in failed_tests: + report.append(f" [{result.category:12}] {result.test_name:20} - {result.status}") + if result.error_message: + # Truncate long error messages + error = result.error_message[:100] + "..." if len(result.error_message) > 100 else result.error_message + report.append(f" Error: {error}") + report.append("") + + # Performance stats + fastest = min(self.results, key=lambda r: r.duration) + slowest = max(self.results, key=lambda r: r.duration) + avg_duration = total_duration / len(self.results) + + report.append("Performance Statistics:") + report.append(f" Fastest: {fastest.test_name:20} ({fastest.duration:.2f}s)") + report.append(f" Slowest: {slowest.test_name:20} ({slowest.duration:.2f}s)") + report.append(f" Average: {avg_duration:.2f}s per test") + + return "\n".join(report) + + def save_detailed_report(self, output_file: Path): + """Save detailed test results to JSON file.""" + report_data = { + "summary": { + "total_tests": len(self.results), + "wall_time": time.time() - self.start_time if self.start_time else 0, + "cpu_time": sum(r.duration for r in self.results), + "timestamp": time.strftime("%Y-%m-%d %H:%M:%S") + }, + "results": [ + { + "test_name": r.test_name, + "category": r.category, + "status": r.status, + "duration": r.duration, + "log_file": r.log_file, + "error_message": r.error_message + } + for r in self.results + ] + } + + with open(output_file, 'w') as f: + json.dump(report_data, f, indent=2) + + def run_verification_suite(self, formal_dir: Path, categories: List[str] = None) -> bool: + """Run the complete verification suite.""" + self.start_time = time.time() + + print("Starting RISC-V CPU Formal Verification Suite") + print("=" * 60) + print(f"Working directory: {formal_dir}") + print(f"Max parallel workers: {self.max_workers}") + print(f"Timeout per test: {self.timeout}s") + print("") + + # Define test categories and their directories + test_categories = { + "instructions": "instructions", + "system": "system_checks", + "integration": "integration" + } + + # Filter categories if specified + if categories: + test_categories = {k: v for k, v in test_categories.items() if k in categories} + + # Collect all test files + all_test_files: List[Tuple[Path, Optional[str], str]] = [] + for category, subdir in test_categories.items(): + test_dir = formal_dir / subdir + test_files = self.find_test_files(test_dir) + all_test_files.extend([(f, task, category) for f, task in test_files]) + + if not all_test_files: + print("[ERROR] No test files found!") + return False + + print(f"Found {len(all_test_files)} test cases across {len(test_categories)} categories") + for category, subdir in test_categories.items(): + test_dir = formal_dir / subdir + count = len(self.find_test_files(test_dir)) + print(f" {category:12}: {count:3} tests") + print("") + + # Run tests + print("Running verification tests...") + print("-" * 60) + self.results = self.run_tests_parallel(all_test_files) + + # Generate and display summary + print("\n" + "=" * 60) + summary = self.generate_summary_report() + print(summary) + + # Save detailed report + report_file = formal_dir / "verification_report.json" + self.save_detailed_report(report_file) + print(f"\nDetailed report saved to: {report_file}") + + # Return success if all tests passed + passed_tests = len([r for r in self.results if r.status == "PASS"]) + return passed_tests == len(self.results) + + +def validate_prerequisites(formal_dir: Path) -> bool: + """Validate external tools and riscv-formal assets before running tests.""" + errors: List[str] = [] + + if shutil.which("sby") is None: + errors.append("Missing 'sby' executable in PATH.") + + repo_root = formal_dir.parent + required_riscv_formal_files = [ + repo_root / "riscv-formal" / "checks" / "rvfi_macros.vh", + repo_root / "riscv-formal" / "checks" / "rvfi_insn_check.sv", + repo_root / "riscv-formal" / "checks" / "rvfi_reg_check.sv", + repo_root / "riscv-formal" / "checks" / "rvfi_pc_fwd_check.sv", + repo_root / "riscv-formal" / "checks" / "rvfi_pc_bwd_check.sv", + repo_root / "riscv-formal" / "insns" / "isa_rv32i.v", + repo_root / "riscv-formal" / "insns" / "isa_rv32im.v", + ] + + missing_files = [path for path in required_riscv_formal_files if not path.exists()] + if missing_files: + errors.append("Missing riscv-formal assets:") + errors.extend([f" - {path}" for path in missing_files]) + errors.append("Hint: run `git submodule update --init --recursive` from repository root.") + + if errors: + print("[ERROR] Formal verification prerequisites are not satisfied.") + for err in errors: + print(err) + return False + + return True + +def main(): + """Main entry point.""" + parser = argparse.ArgumentParser(description="Run RISC-V CPU formal verification suite") + parser.add_argument("--formal-dir", type=Path, default=Path(__file__).parent, + help="Path to formal verification directory") + parser.add_argument("--categories", nargs="+", choices=["instructions", "system", "integration"], + help="Categories to test (default: all)") + parser.add_argument("--workers", type=int, + help="Number of parallel workers") + parser.add_argument("--timeout", type=int, default=300, + help="Timeout per test in seconds") + parser.add_argument("--generate-only", action="store_true", + help="Only generate test configs, don't run tests") + + args = parser.parse_args() + + # Change to formal directory + formal_dir = args.formal_dir.resolve() + if not formal_dir.exists(): + print(f"[ERROR] Formal directory not found: {formal_dir}") + return 1 + + instructions_dir = formal_dir / "instructions" + list_file = instructions_dir / "instruction_list.txt" + sby_file = instructions_dir / "verify_instructions.sby" + + if args.generate_only: + print("Instruction test configurations are static and do not require generation.") + return 0 + + if not instructions_dir.exists() or not list_file.exists() or not sby_file.exists(): + print("[ERROR] Instruction verification assets are missing.") + print(f" Expected: {list_file}") + print(f" Expected: {sby_file}") + return 1 + + if not validate_prerequisites(formal_dir): + return 1 + + # Run verification suite + runner = VerificationSuiteRunner( + max_workers=args.workers, + timeout=args.timeout + ) + + success = runner.run_verification_suite(formal_dir, args.categories) + + return 0 if success else 1 + +if __name__ == "__main__": + sys.exit(main()) diff --git a/formal/system_checks/verify_causal.sby b/formal/system_checks/verify_causal.sby new file mode 100644 index 0000000..9b4fe3a --- /dev/null +++ b/formal/system_checks/verify_causal.sby @@ -0,0 +1,89 @@ +[options] +mode prove +expect pass +depth 30 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Design files for CAUSAL verification --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# riscv-formal checks for CAUSAL verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_causal_check.sv + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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_causal_check.sv diff --git a/formal/system_checks/verify_dmem.sby b/formal/system_checks/verify_dmem.sby new file mode 100644 index 0000000..a8f164d --- /dev/null +++ b/formal/system_checks/verify_dmem.sby @@ -0,0 +1,89 @@ +[options] +mode prove +expect pass +depth 30 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Design files for DMEM verification --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# riscv-formal checks for DMEM verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_dmem_check.sv + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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_dmem_check.sv diff --git a/formal/system_checks/verify_hang.sby b/formal/system_checks/verify_hang.sby new file mode 100644 index 0000000..2210831 --- /dev/null +++ b/formal/system_checks/verify_hang.sby @@ -0,0 +1,89 @@ +[options] +mode prove +expect pass +depth 30 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Design files for HANG verification --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# riscv-formal checks for HANG verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_hang_check.sv + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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_hang_check.sv diff --git a/formal/system_checks/verify_ill.sby b/formal/system_checks/verify_ill.sby new file mode 100644 index 0000000..2af100a --- /dev/null +++ b/formal/system_checks/verify_ill.sby @@ -0,0 +1,89 @@ +[options] +mode prove +expect pass +depth 30 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Design files for ILL verification --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# riscv-formal checks for ILL verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_ill_check.sv + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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_ill_check.sv diff --git a/formal/system_checks/verify_imem.sby b/formal/system_checks/verify_imem.sby new file mode 100644 index 0000000..1e4ef78 --- /dev/null +++ b/formal/system_checks/verify_imem.sby @@ -0,0 +1,89 @@ +[options] +mode prove +expect pass +depth 30 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Design files for IMEM verification --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# riscv-formal checks for IMEM verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_imem_check.sv + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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_imem_check.sv diff --git a/formal/system_checks/verify_liveness.sby b/formal/system_checks/verify_liveness.sby new file mode 100644 index 0000000..7ab669a --- /dev/null +++ b/formal/system_checks/verify_liveness.sby @@ -0,0 +1,89 @@ +[options] +mode prove +expect pass +depth 30 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Design files for LIVENESS verification --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# riscv-formal checks for LIVENESS verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_liveness_check.sv + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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_liveness_check.sv diff --git a/formal/system_checks/verify_pc_bwd.sby b/formal/system_checks/verify_pc_bwd.sby new file mode 100644 index 0000000..39ff04c --- /dev/null +++ b/formal/system_checks/verify_pc_bwd.sby @@ -0,0 +1,89 @@ +[options] +mode prove +expect pass +depth 30 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Design files for PC_BWD verification --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# riscv-formal checks for PC_BWD verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_pc_bwd_check.sv + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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_pc_bwd_check.sv diff --git a/formal/system_checks/verify_pc_fwd.sby b/formal/system_checks/verify_pc_fwd.sby new file mode 100644 index 0000000..7d7464e --- /dev/null +++ b/formal/system_checks/verify_pc_fwd.sby @@ -0,0 +1,89 @@ +[options] +mode prove +expect pass +depth 30 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Design files for PC_FWD verification --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# riscv-formal checks for PC_FWD verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_pc_fwd_check.sv + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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_pc_fwd_check.sv diff --git a/formal/system_checks/verify_reg.sby b/formal/system_checks/verify_reg.sby new file mode 100644 index 0000000..d4222aa --- /dev/null +++ b/formal/system_checks/verify_reg.sby @@ -0,0 +1,89 @@ +[options] +mode prove +expect pass +depth 30 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Design files for REG verification --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# riscv-formal checks for REG verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_reg_check.sv + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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_reg_check.sv diff --git a/formal/system_checks/verify_unique.sby b/formal/system_checks/verify_unique.sby new file mode 100644 index 0000000..318e60a --- /dev/null +++ b/formal/system_checks/verify_unique.sby @@ -0,0 +1,89 @@ +[options] +mode prove +expect pass +depth 30 +wait on + +[engines] +smtbmc boolector + +[script] +# --- Design files for UNIQUE verification --- +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 top.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 riscv_cpu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 data_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 execution_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_mem.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 seven_seg.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 writeback.v + +# Core modules +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 alu.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_exec.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 csr_file.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 decoder.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 interrupt_controller.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 pc.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 registerfile.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 timer.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 uart.v + +# Pipeline stages +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 EX_MEM.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 forwarding_unit.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 ID_EX.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 IF_ID.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 load_use_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 MEM_WB.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_detector.v +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 store_load_forward.v + +# Include files +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 instr_defines.vh +read_verilog -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 memory_map.vh + +# riscv-formal checks for UNIQUE verification +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_macros.vh +read_verilog -sv -formal -DFORMAL -DRISCV_FORMAL_NRET=1 -DRISCV_FORMAL_ILEN=32 -DRISCV_FORMAL_XLEN=32 -DRISCV_FORMAL_CHANNEL_IDX=0 rvfi_unique_check.sv + +# Synthesis passes +hierarchy -top top +proc +opt +memory -nomap +flatten +setundef -undriven -anyseq +check +stat + +[files] +../../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_unique_check.sv diff --git a/riscv-formal b/riscv-formal new file mode 160000 index 0000000..cde5616 --- /dev/null +++ b/riscv-formal @@ -0,0 +1 @@ +Subproject commit cde56160d48adecdf76d9046bb3b05bb2885d3e2 diff --git a/rtl/core_modules/alu.v b/rtl/core_modules/alu.v index 3ca2717..b3d1fa0 100644 --- a/rtl/core_modules/alu.v +++ b/rtl/core_modules/alu.v @@ -9,6 +9,7 @@ module alu ( output reg [31:0] ALUoutput ); + // Keep ALU semantics identical across simulation, synthesis, and formal always @(*) begin case (instr_id) INSTR_ADD: ALUoutput = $signed(rs1) + $signed(rs2); // Addition diff --git a/rtl/core_modules/csr_file.v b/rtl/core_modules/csr_file.v index 89a37d7..201cfb9 100644 --- a/rtl/core_modules/csr_file.v +++ b/rtl/core_modules/csr_file.v @@ -21,7 +21,14 @@ module csr_file ( // Timer interrupt input input wire timer_interrupt, input wire software_interrupt, - input wire external_interrupt + input wire external_interrupt, + + // Expose key CSR registers for other modules + output reg [31:0] mstatus, + output reg [31:0] mie, + output reg [31:0] mip, + output reg [31:0] mtvec, + output reg [31:0] mepc ); // Common CSR addresses @@ -38,15 +45,10 @@ module csr_file ( localparam CSR_CYCLEH = 12'hC80; // CSR registers - reg [31:0] mstatus; reg [31:0] misa; - reg [31:0] mie; - reg [31:0] mtvec; reg [31:0] mscratch; - reg [31:0] mepc; reg [31:0] mcause; reg [31:0] mtval; - reg [31:0] mip; reg [63:0] cycle_counter; // Check if CSR address is valid @@ -148,4 +150,4 @@ module csr_file ( end end -endmodule \ No newline at end of file +endmodule diff --git a/rtl/core_modules/uart.v b/rtl/core_modules/uart.v index 23ff331..0b9336b 100644 --- a/rtl/core_modules/uart.v +++ b/rtl/core_modules/uart.v @@ -2,194 +2,140 @@ `include "memory_map.vh" module uart ( - input wire clk, - input wire rst, - + input wire clk, + input wire rst, + // Memory interface - input wire [31:0] addr, - input wire [31:0] write_data, - input wire write_enable, - input wire read_enable, - output reg [31:0] read_data, - output wire uart_valid, - + input wire [31:0] addr, + input wire [31:0] write_data, + input wire write_enable, + input wire read_enable, + output reg [31:0] read_data, + output wire uart_valid, + // UART output - output wire tx + output wire tx ); - // Registers - reg [7:0] tx_data; // Data to transmit - reg [15:0] baud_div; // Baud rate divisor - reg [15:0] baud_counter; // Baud rate counter - reg tx_busy; // Transmission in progress - reg tx_enable; // Enable transmission - reg tx_start_pending; // Start transmission flag that persists - reg baud_reload; // Flag to reload baud counter - - // Status bits - reg tx_fifo_full; - reg tx_fifo_empty; - - // UART control state machine - reg [3:0] tx_state; - reg [3:0] tx_bit_count; - reg tx_out; - - // Constants - localparam TX_IDLE = 4'd0; - localparam TX_START = 4'd1; - localparam TX_DATA = 4'd2; - localparam TX_STOP = 4'd3; - - // Address validation - assign uart_valid = (addr == `UART_DATA) || - (addr == `UART_STATUS) || - (addr == `UART_CONTROL) || - (addr == `UART_BAUD); - - // UART TX output + // Transmit state + reg [9:0] tx_shift_reg; // {stop, data[7:0], start} + reg [7:0] tx_last_data; // Readback register for UART_DATA + reg [15:0] baud_divider; // Configured baud divisor + reg [15:0] baud_counter; // Baud counter + reg [3:0] tx_bit_index; // Counts transmitted bits (start + data + stop) + reg tx_busy; // Indicates transmission in progress + reg tx_enable; // Global transmitter enable + reg tx_fifo_full; // Indicates write while busy + reg tx_fifo_empty; // Indicates transmitter idle + reg tx_out; // Serialized TX output + + localparam [15:0] DEFAULT_BAUD_DIV = 16'd434; // 115200 @ 50 MHz + + // Address decode + assign uart_valid = (addr == `UART_DATA) || + (addr == `UART_STATUS) || + (addr == `UART_CONTROL)|| + (addr == `UART_BAUD); + assign tx = tx_out; - - // Default baud rate (115200 @ 50MHz clock) - localparam DEFAULT_BAUD_DIVISOR = 16'd434; - - // Initialize registers - initial begin - tx_data = 8'h00; - baud_div = DEFAULT_BAUD_DIVISOR; - tx_busy = 1'b0; - tx_enable = 1'b1; - tx_out = 1'b1; // Idle state is high - tx_state = TX_IDLE; - tx_bit_count = 4'b0; - tx_fifo_full = 1'b0; - tx_fifo_empty = 1'b1; - baud_counter = 16'b1; // Start at 1 so first baud tick happens quickly - tx_start_pending = 1'b0; - baud_reload = 1'b0; - end - - // Handle register writes (only updates registers, no counter manipulation) + + // Ensure the baud counter never reaches zero, which would stall transmission or + // produce an undefined baud period. Divisors of 0 or 1 are coerced to 1. + function [15:0] baud_reload_value; + input [15:0] raw_value; + begin + baud_reload_value = (raw_value <= 16'd1) ? 16'd1 : raw_value; + end + endfunction + always @(posedge clk or posedge rst) begin if (rst) begin - tx_data <= 8'h00; - baud_div <= DEFAULT_BAUD_DIVISOR; - tx_enable <= 1'b1; - tx_start_pending <= 1'b0; - tx_busy <= 1'b0; - baud_reload <= 1'b1; // Force reload after reset + tx_shift_reg <= 10'h3FF; + tx_last_data <= 8'h00; + baud_divider <= DEFAULT_BAUD_DIV; + baud_counter <= DEFAULT_BAUD_DIV; + tx_bit_index <= 4'd0; + tx_busy <= 1'b0; + tx_enable <= 1'b1; + tx_fifo_full <= 1'b0; + tx_fifo_empty <= 1'b1; + tx_out <= 1'b1; // idle high end else begin - // Clear baud_reload flag after one cycle - baud_reload <= 1'b0; - + // Default idle status + if (!tx_busy) begin + tx_fifo_empty <= 1'b1; + tx_fifo_full <= 1'b0; + end + if (write_enable && uart_valid) begin case (addr) + `UART_CONTROL: begin + tx_enable <= write_data[0]; + if (!write_data[0]) begin + tx_busy <= 1'b0; + tx_fifo_empty <= 1'b1; + tx_fifo_full <= 1'b0; + tx_out <= 1'b1; + end + end + + `UART_BAUD: begin + baud_divider <= baud_reload_value(write_data[15:0]); + if (!tx_busy) begin + baud_counter <= baud_reload_value(write_data[15:0]); + end + end + `UART_DATA: begin - // Single-byte transmit buffer: if busy, set tx_fifo_full but do not buffer additional bytes. - if (!tx_busy && tx_enable) begin - tx_data <= write_data[7:0]; - tx_start_pending <= 1'b1; // Set pending flag - tx_busy <= 1'b1; // Set busy immediately + if (tx_enable && !tx_busy) begin + tx_shift_reg <= {1'b1, write_data[7:0], 1'b0}; + tx_last_data <= write_data[7:0]; + tx_bit_index <= 4'd0; + tx_busy <= 1'b1; tx_fifo_empty <= 1'b0; + tx_out <= 1'b0; // start bit + baud_counter <= baud_reload_value(baud_divider); end else begin tx_fifo_full <= 1'b1; end end - `UART_CONTROL: begin - tx_enable <= write_data[0]; - end - `UART_BAUD: begin - baud_div <= write_data[15:0]; - baud_reload <= 1'b1; // Signal to reload counter - end - default: ; // Do nothing + + default: ; endcase end + + if (tx_enable && tx_busy) begin + if (baud_counter == 16'd0) begin + if (tx_bit_index < 4'd9) begin + tx_out <= tx_shift_reg[1]; + tx_shift_reg <= {1'b1, tx_shift_reg[9:1]}; + tx_bit_index <= tx_bit_index + 4'd1; + baud_counter <= baud_reload_value(baud_divider); + end else begin + tx_busy <= 1'b0; + tx_out <= 1'b1; + tx_fifo_empty <= 1'b1; + tx_fifo_full <= 1'b0; + end + end else begin + baud_counter <= baud_counter - 16'd1; + end + end end end - - // Handle register reads + always @(*) begin if (read_enable && uart_valid) begin case (addr) - `UART_DATA: read_data = {24'b0, tx_data}; - `UART_STATUS: read_data = {29'b0, tx_busy, tx_fifo_empty, tx_fifo_full}; + `UART_DATA: read_data = {24'b0, tx_last_data}; + `UART_STATUS: read_data = {29'b0, tx_busy, tx_fifo_empty, tx_fifo_full}; `UART_CONTROL: read_data = {31'b0, tx_enable}; - `UART_BAUD: read_data = {16'b0, baud_div}; - default: read_data = 32'h0; + `UART_BAUD: read_data = {16'b0, baud_divider}; + default: read_data = 32'h0; endcase end else begin read_data = 32'h0; end end - - // UART transmitter state machine and baud counter - always @(posedge clk or posedge rst) begin - if (rst) begin - tx_state <= TX_IDLE; - tx_out <= 1'b1; - tx_bit_count <= 4'b0; - baud_counter <= 16'b1; // Start at 1 - tx_fifo_empty <= 1'b1; - tx_fifo_full <= 1'b0; - end else begin - // Handle baud counter reload - if (baud_reload) begin - baud_counter <= baud_div; - end else begin - // Normal baud rate counter logic - if (baud_counter > 0) begin - baud_counter <= baud_counter - 1'b1; - end else begin - // Baud tick occurred - reload counter and process state machine - baud_counter <= baud_div; - - case (tx_state) - TX_IDLE: begin - if (tx_enable && tx_start_pending) begin - tx_state <= TX_START; - tx_out <= 1'b0; // Start bit - tx_bit_count <= 4'b0; - tx_start_pending <= 1'b0; // Clear pending flag - end else begin - tx_out <= 1'b1; // Idle state - // Only clear busy when truly idle (no pending transmission) - if (!tx_start_pending) begin - tx_busy <= 1'b0; - tx_fifo_empty <= 1'b1; - tx_fifo_full <= 1'b0; - end - end - end - - TX_START: begin - tx_state <= TX_DATA; - tx_out <= tx_data[0]; // First data bit (LSB first) - tx_bit_count <= 4'b1; - end - - TX_DATA: begin - if (tx_bit_count < 8) begin - tx_out <= tx_data[tx_bit_count[2:0]]; - tx_bit_count <= tx_bit_count + 1'b1; - end else begin - tx_state <= TX_STOP; - tx_out <= 1'b1; // Stop bit - end - end - - TX_STOP: begin - tx_state <= TX_IDLE; - tx_busy <= 1'b0; - tx_fifo_empty <= 1'b1; - tx_fifo_full <= 1'b0; - end - - default: tx_state <= TX_IDLE; - endcase - end - end - end - end -endmodule \ No newline at end of file +endmodule diff --git a/rtl/data_mem.v b/rtl/data_mem.v index e8b3d4b..fcc7297 100644 --- a/rtl/data_mem.v +++ b/rtl/data_mem.v @@ -3,23 +3,25 @@ // data_mem.v - byte-addressable data memory for RISC-V CPU -module data_mem #(parameter DATA_WIDTH = 32, ADDR_WIDTH = 32, MEM_SIZE = 1048576) ( // 1MB = 1024*1024 bytes - input wire clk, +module data_mem #(parameter DATA_WIDTH = 32, ADDR_WIDTH = 32, MEM_SIZE = 64) ( // default 64 bytes for formal build; functional size set by top-level + input wire clk, input wire wr_en, input wire rd_en, input wire [3:0] write_byte_enable, // Write byte enables input wire [2:0] load_type, // Load type encoding - input wire [ADDR_WIDTH-1:0] addr, + input wire [ADDR_WIDTH-1:0] addr, input wire [DATA_WIDTH-1:0] wr_data, output wire [DATA_WIDTH-1:0] rd_data_out ); - // Array of 1MB bytes + // Array of MEM_SIZE bytes reg [7:0] data_ram [0:MEM_SIZE-1]; + // Declare loop variable for initialization + integer i; + // Initialize memory to zeros initial begin - integer i; for (i = 0; i < MEM_SIZE; i = i + 1) begin data_ram[i] = 8'h00; end @@ -40,16 +42,16 @@ module data_mem #(parameter DATA_WIDTH = 32, ADDR_WIDTH = 32, MEM_SIZE = 1048576 wire [7:0] byte_data; wire [15:0] halfword_data; wire [31:0] word_data; - + // Read individual bytes directly assign byte_data = (addr < MEM_SIZE) ? data_ram[addr] : 8'h00; - + // Read halfwords (little-endian: low byte first) - assign halfword_data = (addr < MEM_SIZE-1) ? + assign halfword_data = (addr < MEM_SIZE-1) ? {data_ram[addr+1], data_ram[addr]} : 16'h0000; - + // Read words (little-endian: low byte first) - assign word_data = (addr < MEM_SIZE-3) ? + assign word_data = (addr < MEM_SIZE-3) ? {data_ram[addr+3], data_ram[addr+2], data_ram[addr+1], data_ram[addr]} : 32'h00000000; // Format read data based on load type - much simpler logic @@ -83,4 +85,4 @@ module data_mem #(parameter DATA_WIDTH = 32, ADDR_WIDTH = 32, MEM_SIZE = 1048576 end end -endmodule \ No newline at end of file +endmodule diff --git a/rtl/execution_unit.v b/rtl/execution_unit.v index 8a41704..c23066e 100644 --- a/rtl/execution_unit.v +++ b/rtl/execution_unit.v @@ -32,8 +32,8 @@ module execution_unit( output reg jump_signal, output reg [31:0] jump_addr, output reg [31:0] mem_addr, - output reg [31:0] rs1_value_out, - output reg [31:0] rs2_value_out, + output wire [31:0] rs1_value_out, + output wire [31:0] rs2_value_out, output reg flush_pipeline, // Add interrupt/exception inputs @@ -100,13 +100,14 @@ always @(*) begin endcase end +wire [31:0] alu_output_wire; alu alu_inst( .rs1(rs1_value), .rs2(rs2_value), .imm(imm), .instr_id(instr_id), .pc_input(jump_addr), - .ALUoutput() + .ALUoutput(alu_output_wire) ); // For all R-type instructions, the exec_output is the output of the ALU @@ -138,10 +139,10 @@ always @(*) begin end else begin case (opcode) 7'b0110011: begin // R-type instructions - exec_output = alu_inst.ALUoutput; + exec_output = alu_output_wire; end 7'b0010011: begin // I-type instructions - exec_output = alu_inst.ALUoutput; + exec_output = alu_output_wire; end 7'b0000011: begin // Load instructions mem_addr = rs1_value + imm; diff --git a/rtl/instr_mem.v b/rtl/instr_mem.v index 005ee09..a14786f 100644 --- a/rtl/instr_mem.v +++ b/rtl/instr_mem.v @@ -16,6 +16,14 @@ module instr_mem #( // Array of 32-bit words (keeps $readmemh compatibility) reg [DATA_WIDTH-1:0] instr_ram [0:MEM_SIZE-1]; +// Local variables for always blocks +reg [ADDR_WIDTH-3:0] word_addr; +reg [1:0] byte_offset; +reg [31:0] word_data; +reg [31:0] next_word_data; +reg [7:0] byte_data; +reg [15:0] halfword_data; + `ifdef COCOTB_SIM initial begin `ifdef INSTR_HEX_FILE @@ -31,9 +39,9 @@ initial begin // $display(" [0x08]: 0x%08h", instr_ram[2]); end `else +integer i; initial begin // Initialize instruction memory with NOPs - integer i; for (i = 0; i < MEM_SIZE; i = i + 1) begin instr_ram[i] = 32'h00000013; // Default to NOP instruction end @@ -49,15 +57,8 @@ always @(*) begin end end -// Port 2: Data access with byte/halfword/word support always @(*) begin // Extract word address and byte offset - reg [ADDR_WIDTH-3:0] word_addr; - reg [1:0] byte_offset; - reg [31:0] word_data; - reg [7:0] byte_data; - reg [15:0] halfword_data; - word_addr = instr_addr_p2[ADDR_WIDTH-1:2]; byte_offset = instr_addr_p2[1:0]; @@ -86,7 +87,6 @@ always @(*) begin // Handle cross-word boundary access for halfwords and words if (byte_offset == 2'b11 && (load_type == 3'b001 || load_type == 3'b101)) begin // Halfword access that crosses word boundary - reg [31:0] next_word_data; if (word_addr + 1 < MEM_SIZE) begin next_word_data = instr_ram[word_addr + 1]; end else begin @@ -97,7 +97,6 @@ always @(*) begin if (byte_offset != 2'b00 && load_type == 3'b010) begin // Word access that crosses word boundary - need to combine two words - reg [31:0] next_word_data; if (word_addr + 1 < MEM_SIZE) begin next_word_data = instr_ram[word_addr + 1]; end else begin diff --git a/rtl/pipeline_stages/EX_MEM.v b/rtl/pipeline_stages/EX_MEM.v index aa31242..d353fcf 100644 --- a/rtl/pipeline_stages/EX_MEM.v +++ b/rtl/pipeline_stages/EX_MEM.v @@ -13,6 +13,16 @@ module EX_MEM ( input wire [31:0] jump_addr_in, input wire [5:0] instr_id_in, input wire rd_valid_in, + input wire [31:0] instruction_in, + input wire [11:0] csr_addr_in, + input wire csr_read_enable_in, + input wire csr_write_enable_in, + input wire [31:0] csr_write_data_in, + input wire [31:0] csr_read_data_in, + input wire interrupt_taken_in, + input wire mret_instruction_in, + input wire ecall_exception_in, + input wire ebreak_exception_in, output reg [4:0] rs1_addr_out, output reg [4:0] rs2_addr_out, output reg [4:0] rd_addr_out, @@ -24,7 +34,17 @@ module EX_MEM ( output reg jump_signal_out, output reg [31:0] jump_addr_out, output reg [5:0] instr_id_out, - output reg rd_valid_out + output reg rd_valid_out, + output reg [31:0] instruction_out, + output reg [11:0] csr_addr_out, + output reg csr_read_enable_out, + output reg csr_write_enable_out, + output reg [31:0] csr_write_data_out, + output reg [31:0] csr_read_data_out, + output reg interrupt_taken_out, + output reg mret_instruction_out, + output reg ecall_exception_out, + output reg ebreak_exception_out ); always @(posedge clk or posedge rst) begin @@ -41,6 +61,16 @@ module EX_MEM ( jump_addr_out <= 32'b0; instr_id_out <= 6'b0; rd_valid_out <= 1'b0; + instruction_out <= 32'b0; + csr_addr_out <= 12'b0; + csr_read_enable_out <= 1'b0; + csr_write_enable_out <= 1'b0; + csr_write_data_out <= 32'b0; + csr_read_data_out <= 32'b0; + interrupt_taken_out <= 1'b0; + mret_instruction_out <= 1'b0; + ecall_exception_out <= 1'b0; + ebreak_exception_out <= 1'b0; end else begin rs1_addr_out <= rs1_addr_in; rs2_addr_out <= rs2_addr_in; @@ -53,8 +83,18 @@ module EX_MEM ( jump_signal_out <= jump_signal_in; jump_addr_out <= jump_addr_in; instr_id_out <= instr_id_in; - rd_valid_out <= rd_valid_in; + rd_valid_out <= rd_valid_in; + instruction_out <= instruction_in; + csr_addr_out <= csr_addr_in; + csr_read_enable_out <= csr_read_enable_in; + csr_write_enable_out <= csr_write_enable_in; + csr_write_data_out <= csr_write_data_in; + csr_read_data_out <= csr_read_data_in; + interrupt_taken_out <= interrupt_taken_in; + mret_instruction_out <= mret_instruction_in; + ecall_exception_out <= ecall_exception_in; + ebreak_exception_out <= ebreak_exception_in; end end -endmodule \ No newline at end of file +endmodule diff --git a/rtl/pipeline_stages/ID_EX.v b/rtl/pipeline_stages/ID_EX.v index f310b40..dbc9d0f 100644 --- a/rtl/pipeline_stages/ID_EX.v +++ b/rtl/pipeline_stages/ID_EX.v @@ -10,6 +10,7 @@ module ID_EX( input wire [4:0] rd_addr_in, input wire [6:0] opcode_in, input wire [5:0] instr_id_in, + input wire [31:0] instruction_in, input wire [31:0] pc_in, input wire [31:0] rs1_value_in, input wire [31:0] rs2_value_in, @@ -23,6 +24,7 @@ module ID_EX( output reg [4:0] rd_addr_out, output reg [6:0] opcode_out, output reg [5:0] instr_id_out, + output reg [31:0] instruction_out, output reg [31:0] pc_out, output reg [31:0] rs1_value_out, output reg [31:0] rs2_value_out @@ -38,6 +40,7 @@ module ID_EX( rd_addr_out <= 5'b0; opcode_out <= 7'b0; instr_id_out <= 6'b0; + instruction_out <= 32'b0; pc_out <= 32'b0; rs1_value_out <= 32'b0; rs2_value_out <= 32'b0; @@ -52,6 +55,7 @@ module ID_EX( rd_addr_out <= 5'b0; opcode_out <= 7'b0; instr_id_out <= 6'b0; + instruction_out <= 32'b0; pc_out <= pc_in; // Keep PC for correct program flow rs1_value_out <= 32'b0; rs2_value_out <= 32'b0; @@ -65,9 +69,10 @@ module ID_EX( rd_addr_out <= rd_addr_in; opcode_out <= opcode_in; instr_id_out <= instr_id_in; + instruction_out <= instruction_in; pc_out <= pc_in; rs1_value_out <= rs1_value_in; rs2_value_out <= rs2_value_in; end end -endmodule \ No newline at end of file +endmodule diff --git a/rtl/pipeline_stages/MEM_WB.v b/rtl/pipeline_stages/MEM_WB.v index 5653556..9f4e3ef 100644 --- a/rtl/pipeline_stages/MEM_WB.v +++ b/rtl/pipeline_stages/MEM_WB.v @@ -17,6 +17,21 @@ module MEM_WB ( input wire [5:0] instr_id_in, input wire rd_valid_in, input wire [31:0] mem_data_in, // Data from memory + input wire [31:0] mem_wr_data_in, + input wire [31:0] instruction_in, + input wire [11:0] csr_addr_in, + input wire csr_read_enable_in, + input wire csr_write_enable_in, + input wire [31:0] csr_write_data_in, + input wire [31:0] csr_read_data_in, + input wire interrupt_taken_in, + input wire mret_instruction_in, + input wire ecall_exception_in, + input wire ebreak_exception_in, + input wire mem_read_enable_in, + input wire mem_write_enable_in, + input wire [3:0] write_byte_enable_in, + input wire [2:0] load_type_in, // Store-load forwarding inputs input wire store_load_hazard, // Signal indicating a store-load hazard @@ -35,7 +50,22 @@ module MEM_WB ( output reg [31:0] jump_addr_out, output reg [5:0] instr_id_out, output reg rd_valid_out, - output reg [31:0] mem_data_out // Data going to the writeback stage + output reg [31:0] mem_data_out, // Data going to the writeback stage + output reg [31:0] mem_wr_data_out, + output reg [31:0] instruction_out, + output reg [11:0] csr_addr_out, + output reg csr_read_enable_out, + output reg csr_write_enable_out, + output reg [31:0] csr_write_data_out, + output reg [31:0] csr_read_data_out, + output reg interrupt_taken_out, + output reg mret_instruction_out, + output reg ecall_exception_out, + output reg ebreak_exception_out, + output reg mem_read_enable_out, + output reg mem_write_enable_out, + output reg [3:0] write_byte_enable_out, + output reg [2:0] load_type_out ); always @(posedge clk or posedge rst) begin @@ -54,6 +84,21 @@ module MEM_WB ( instr_id_out <= 6'b0; rd_valid_out <= 1'b0; mem_data_out <= 32'b0; + mem_wr_data_out <= 32'b0; + instruction_out <= 32'b0; + csr_addr_out <= 12'b0; + csr_read_enable_out <= 1'b0; + csr_write_enable_out <= 1'b0; + csr_write_data_out <= 32'b0; + csr_read_data_out <= 32'b0; + interrupt_taken_out <= 1'b0; + mret_instruction_out <= 1'b0; + ecall_exception_out <= 1'b0; + ebreak_exception_out <= 1'b0; + mem_read_enable_out <= 1'b0; + mem_write_enable_out <= 1'b0; + write_byte_enable_out <= 4'b0; + load_type_out <= 3'b0; end else begin // Transfer all register values @@ -72,6 +117,21 @@ module MEM_WB ( // If there's a store-load hazard, forward store data instead of memory data mem_data_out <= store_load_hazard ? store_data : mem_data_in; + mem_wr_data_out <= mem_wr_data_in; + instruction_out <= instruction_in; + csr_addr_out <= csr_addr_in; + csr_read_enable_out <= csr_read_enable_in; + csr_write_enable_out <= csr_write_enable_in; + csr_write_data_out <= csr_write_data_in; + csr_read_data_out <= csr_read_data_in; + interrupt_taken_out <= interrupt_taken_in; + mret_instruction_out <= mret_instruction_in; + ecall_exception_out <= ecall_exception_in; + ebreak_exception_out <= ebreak_exception_in; + mem_read_enable_out <= mem_read_enable_in; + mem_write_enable_out <= mem_write_enable_in; + write_byte_enable_out <= write_byte_enable_in; + load_type_out <= load_type_in; end end -endmodule \ No newline at end of file +endmodule diff --git a/rtl/riscv_cpu.v b/rtl/riscv_cpu.v index 7acba91..5c52748 100644 --- a/rtl/riscv_cpu.v +++ b/rtl/riscv_cpu.v @@ -1,4 +1,3 @@ -`default_nettype none module riscv_cpu ( input wire clk, input wire rst, @@ -16,9 +15,83 @@ module riscv_cpu ( // Interrupt inputs input wire timer_interrupt, input wire software_interrupt, - input wire external_interrupt + input wire external_interrupt, + + // RVFI interface outputs for formal verification + output wire rvfi_valid, + output wire [63:0] rvfi_order, + output wire [31:0] rvfi_insn, + output wire rvfi_trap, + output wire rvfi_halt, + output wire rvfi_intr, + output wire [1:0] rvfi_mode, + output wire [1:0] rvfi_ixl, + output wire [4:0] rvfi_rs1_addr, + output wire [4:0] rvfi_rs2_addr, + output wire [31:0] rvfi_rs1_rdata, + output wire [31:0] rvfi_rs2_rdata, + output wire [4:0] rvfi_rd_addr, + output wire [31:0] rvfi_rd_wdata, + output wire [31:0] rvfi_pc_rdata, + output wire [31:0] rvfi_pc_wdata, + output wire [31:0] rvfi_mem_addr, + output wire [3:0] rvfi_mem_rmask, + output wire [31:0] rvfi_mem_rdata, + output wire [31:0] rvfi_mem_wdata, + output wire [3:0] rvfi_mem_wmask, + + // CSR RVFI channels + output wire [31:0] rvfi_csr_mstatus_rmask, + output wire [31:0] rvfi_csr_mstatus_wmask, + output wire [31:0] rvfi_csr_mstatus_rdata, + output wire [31:0] rvfi_csr_mstatus_wdata, + output wire [31:0] rvfi_csr_misa_rmask, + output wire [31:0] rvfi_csr_misa_wmask, + output wire [31:0] rvfi_csr_misa_rdata, + output wire [31:0] rvfi_csr_misa_wdata, + output wire [31:0] rvfi_csr_mie_rmask, + output wire [31:0] rvfi_csr_mie_wmask, + output wire [31:0] rvfi_csr_mie_rdata, + output wire [31:0] rvfi_csr_mie_wdata, + output wire [31:0] rvfi_csr_mtvec_rmask, + output wire [31:0] rvfi_csr_mtvec_wmask, + output wire [31:0] rvfi_csr_mtvec_rdata, + output wire [31:0] rvfi_csr_mtvec_wdata, + output wire [31:0] rvfi_csr_mscratch_rmask, + output wire [31:0] rvfi_csr_mscratch_wmask, + output wire [31:0] rvfi_csr_mscratch_rdata, + output wire [31:0] rvfi_csr_mscratch_wdata, + output wire [31:0] rvfi_csr_mepc_rmask, + output wire [31:0] rvfi_csr_mepc_wmask, + output wire [31:0] rvfi_csr_mepc_rdata, + output wire [31:0] rvfi_csr_mepc_wdata, + output wire [31:0] rvfi_csr_mcause_rmask, + output wire [31:0] rvfi_csr_mcause_wmask, + output wire [31:0] rvfi_csr_mcause_rdata, + output wire [31:0] rvfi_csr_mcause_wdata, + output wire [31:0] rvfi_csr_mtval_rmask, + output wire [31:0] rvfi_csr_mtval_wmask, + output wire [31:0] rvfi_csr_mtval_rdata, + output wire [31:0] rvfi_csr_mtval_wdata, + output wire [31:0] rvfi_csr_mip_rmask, + output wire [31:0] rvfi_csr_mip_wmask, + output wire [31:0] rvfi_csr_mip_rdata, + output wire [31:0] rvfi_csr_mip_wdata ); + // Instruction and CSR identifiers used for RVFI bookkeeping + localparam [5:0] INSTR_INVALID = 6'h00; + + localparam [11:0] CSR_MSTATUS = 12'h300; + localparam [11:0] CSR_MISA = 12'h301; + localparam [11:0] CSR_MIE = 12'h304; + localparam [11:0] CSR_MTVEC = 12'h305; + localparam [11:0] CSR_MSCRATCH = 12'h340; + localparam [11:0] CSR_MEPC = 12'h341; + localparam [11:0] CSR_MCAUSE = 12'h342; + localparam [11:0] CSR_MTVAL = 12'h343; + localparam [11:0] CSR_MIP = 12'h344; + // Instantiate PC wire [31:0] pc_inst0_out; wire pc_inst0_j_signal; @@ -125,6 +198,7 @@ module riscv_cpu ( wire [6:0] id_ex_inst0_opcode_out; wire [5:0] id_ex_inst0_instr_id_out; wire [31:0] id_ex_inst0_pc_out; + wire [31:0] id_ex_inst0_instruction_out; wire [31:0] id_ex_inst0_rs1_value_out; wire [31:0] id_ex_inst0_rs2_value_out; @@ -147,6 +221,7 @@ module riscv_cpu ( .rd_addr_in(decoder_inst0_rd_out), .opcode_in(decoder_inst0_opcode_out), .instr_id_in(decoder_inst0_instr_id_out), + .instruction_in(if_id_instr_out), .pc_in(if_id_pc_out), .rs1_value_in(rf_inst0_rs1_value_out), .rs2_value_in(rf_inst0_rs2_value_out), @@ -160,6 +235,7 @@ module riscv_cpu ( .rd_addr_out(id_ex_inst0_rd_addr_out), .opcode_out(id_ex_inst0_opcode_out), .instr_id_out(id_ex_inst0_instr_id_out), + .instruction_out(id_ex_inst0_instruction_out), .pc_out(id_ex_inst0_pc_out), .rs1_value_out(id_ex_inst0_rs1_value_out), .rs2_value_out(id_ex_inst0_rs2_value_out) @@ -210,6 +286,13 @@ module riscv_cpu ( wire ecall_exception; wire ebreak_exception; + // CSR outputs + wire [31:0] csr_mstatus; + wire [31:0] csr_mie; + wire [31:0] csr_mip; + wire [31:0] csr_mtvec; + wire [31:0] csr_mepc; + // Instantiate interrupt controller interrupt_controller int_ctrl_inst ( .clk(clk), @@ -217,9 +300,9 @@ module riscv_cpu ( .timer_interrupt(timer_interrupt), .software_interrupt(software_interrupt), .external_interrupt(external_interrupt), - .mstatus(csr_file_inst.mstatus), - .mie(csr_file_inst.mie), - .mip(csr_file_inst.mip), + .mstatus(csr_mstatus), + .mie(csr_mie), + .mip(csr_mip), .interrupt_pending(interrupt_pending), .interrupt_cause(interrupt_cause), .interrupt_taken(interrupt_taken), @@ -246,7 +329,12 @@ module riscv_cpu ( .ebreak_exception(ebreak_exception), .timer_interrupt(timer_interrupt), .software_interrupt(software_interrupt), - .external_interrupt(external_interrupt) + .external_interrupt(external_interrupt), + .mstatus(csr_mstatus), + .mie(csr_mie), + .mip(csr_mip), + .mtvec(csr_mtvec), + .mepc(csr_mepc) ); execution_unit ex_unit_inst0 ( @@ -284,8 +372,8 @@ module riscv_cpu ( // Interrupt connections .interrupt_pending(interrupt_pending), .interrupt_cause(interrupt_cause), - .mtvec(csr_file_inst.mtvec), - .mepc(csr_file_inst.mepc), + .mtvec(csr_mtvec), + .mepc(csr_mepc), .interrupt_taken(interrupt_taken), .mret_instruction(mret_instruction), .ecall_exception(ecall_exception), @@ -307,6 +395,16 @@ module riscv_cpu ( wire [31:0] ex_mem_inst0_jump_addr_out; wire [5:0] ex_mem_inst0_instr_id_out; wire ex_mem_inst0_rd_valid_out; + wire [31:0] ex_mem_inst0_instruction_out; + wire [11:0] ex_mem_inst0_csr_addr_out; + wire ex_mem_inst0_csr_read_enable_out; + wire ex_mem_inst0_csr_write_enable_out; + wire [31:0] ex_mem_inst0_csr_write_data_out; + wire [31:0] ex_mem_inst0_csr_read_data_out; + wire ex_mem_inst0_interrupt_taken_out; + wire ex_mem_inst0_mret_instruction_out; + wire ex_mem_inst0_ecall_exception_out; + wire ex_mem_inst0_ebreak_exception_out; EX_MEM ex_mem_inst0 ( .clk(clk), @@ -323,6 +421,16 @@ module riscv_cpu ( .jump_addr_in(ex_inst0_jump_addr_out), .instr_id_in(id_ex_inst0_instr_id_out), .rd_valid_in(id_ex_inst0_rd_valid_out), + .instruction_in(id_ex_inst0_instruction_out), + .csr_addr_in(csr_addr), + .csr_read_enable_in(csr_read_enable), + .csr_write_enable_in(csr_write_enable), + .csr_write_data_in(csr_write_data), + .csr_read_data_in(csr_read_data), + .interrupt_taken_in(interrupt_taken), + .mret_instruction_in(mret_instruction), + .ecall_exception_in(ecall_exception), + .ebreak_exception_in(ebreak_exception), .rs1_addr_out(ex_mem_inst0_rs1_addr_out), .rs2_addr_out(ex_mem_inst0_rs2_addr_out), .rd_addr_out(ex_mem_inst0_rd_addr_out), @@ -334,7 +442,17 @@ module riscv_cpu ( .jump_signal_out(ex_mem_inst0_jump_signal_out), .jump_addr_out(ex_mem_inst0_jump_addr_out), .instr_id_out(ex_mem_inst0_instr_id_out), - .rd_valid_out(ex_mem_inst0_rd_valid_out) + .rd_valid_out(ex_mem_inst0_rd_valid_out), + .instruction_out(ex_mem_inst0_instruction_out), + .csr_addr_out(ex_mem_inst0_csr_addr_out), + .csr_read_enable_out(ex_mem_inst0_csr_read_enable_out), + .csr_write_enable_out(ex_mem_inst0_csr_write_enable_out), + .csr_write_data_out(ex_mem_inst0_csr_write_data_out), + .csr_read_data_out(ex_mem_inst0_csr_read_data_out), + .interrupt_taken_out(ex_mem_inst0_interrupt_taken_out), + .mret_instruction_out(ex_mem_inst0_mret_instruction_out), + .ecall_exception_out(ex_mem_inst0_ecall_exception_out), + .ebreak_exception_out(ex_mem_inst0_ebreak_exception_out) ); // Instantiate Memory Unit @@ -381,6 +499,21 @@ module riscv_cpu ( wire [5:0] mem_wb_inst0_instr_id_out; wire mem_wb_inst0_rd_valid_out; wire [31:0] mem_wb_inst0_mem_data_out; + wire [31:0] mem_wb_inst0_instruction_out; + wire [11:0] mem_wb_inst0_csr_addr_out; + wire mem_wb_inst0_csr_read_enable_out; + wire mem_wb_inst0_csr_write_enable_out; + wire [31:0] mem_wb_inst0_csr_write_data_out; + wire [31:0] mem_wb_inst0_csr_read_data_out; + wire mem_wb_inst0_interrupt_taken_out; + wire mem_wb_inst0_mret_instruction_out; + wire mem_wb_inst0_ecall_exception_out; + wire mem_wb_inst0_ebreak_exception_out; + wire mem_wb_inst0_mem_read_enable_out; + wire mem_wb_inst0_mem_write_enable_out; + wire [3:0] mem_wb_inst0_write_byte_enable_out; + wire [2:0] mem_wb_inst0_load_type_out; + wire [31:0] mem_wb_inst0_mem_wr_data_out; // Add wires for store-load forwarding wire store_load_hazard; @@ -413,6 +546,21 @@ module riscv_cpu ( .instr_id_in(ex_mem_inst0_instr_id_out), .rd_valid_in(ex_mem_inst0_rd_valid_out), .mem_data_in(module_read_data_in), // Connect memory data + .mem_wr_data_in(mem_unit_inst0_wr_data_out), + .instruction_in(ex_mem_inst0_instruction_out), + .csr_addr_in(ex_mem_inst0_csr_addr_out), + .csr_read_enable_in(ex_mem_inst0_csr_read_enable_out), + .csr_write_enable_in(ex_mem_inst0_csr_write_enable_out), + .csr_write_data_in(ex_mem_inst0_csr_write_data_out), + .csr_read_data_in(ex_mem_inst0_csr_read_data_out), + .interrupt_taken_in(ex_mem_inst0_interrupt_taken_out), + .mret_instruction_in(ex_mem_inst0_mret_instruction_out), + .ecall_exception_in(ex_mem_inst0_ecall_exception_out), + .ebreak_exception_in(ex_mem_inst0_ebreak_exception_out), + .mem_read_enable_in(mem_unit_inst0_read_enable_out), + .mem_write_enable_in(mem_unit_inst0_wr_enable_out), + .write_byte_enable_in(mem_unit_inst0_write_byte_enable_out), + .load_type_in(mem_unit_inst0_load_type_out), // Store-load forwarding connections .store_load_hazard(store_load_hazard), @@ -431,7 +579,22 @@ module riscv_cpu ( .jump_addr_out(mem_wb_inst0_jump_addr_out), .instr_id_out(mem_wb_inst0_instr_id_out), .rd_valid_out(mem_wb_inst0_rd_valid_out), - .mem_data_out(mem_wb_inst0_mem_data_out) // Output to WB stage + .mem_data_out(mem_wb_inst0_mem_data_out), // Output to WB stage + .mem_wr_data_out(mem_wb_inst0_mem_wr_data_out), + .instruction_out(mem_wb_inst0_instruction_out), + .csr_addr_out(mem_wb_inst0_csr_addr_out), + .csr_read_enable_out(mem_wb_inst0_csr_read_enable_out), + .csr_write_enable_out(mem_wb_inst0_csr_write_enable_out), + .csr_write_data_out(mem_wb_inst0_csr_write_data_out), + .csr_read_data_out(mem_wb_inst0_csr_read_data_out), + .interrupt_taken_out(mem_wb_inst0_interrupt_taken_out), + .mret_instruction_out(mem_wb_inst0_mret_instruction_out), + .ecall_exception_out(mem_wb_inst0_ecall_exception_out), + .ebreak_exception_out(mem_wb_inst0_ebreak_exception_out), + .mem_read_enable_out(mem_wb_inst0_mem_read_enable_out), + .mem_write_enable_out(mem_wb_inst0_mem_write_enable_out), + .write_byte_enable_out(mem_wb_inst0_write_byte_enable_out), + .load_type_out(mem_wb_inst0_load_type_out) ); // Instantiate Write Back Stage @@ -456,4 +619,122 @@ module riscv_cpu ( // Write Back Stage + // RVFI (RISC-V Formal Interface) implementation for formal verification + reg [63:0] rvfi_order_reg; + + wire rvfi_commit_valid = (mem_wb_inst0_instr_id_out != INSTR_INVALID); + + // Update order counter on valid instructions + always @(posedge clk) begin + if (rst) begin + rvfi_order_reg <= 64'b0; + end else if (rvfi_commit_valid) begin + rvfi_order_reg <= rvfi_order_reg + 1; + end + end + + // RVFI base channel outputs + assign rvfi_valid = rvfi_commit_valid; + assign rvfi_order = rvfi_order_reg; + assign rvfi_insn = mem_wb_inst0_instruction_out; + assign rvfi_trap = mem_wb_inst0_ecall_exception_out || mem_wb_inst0_ebreak_exception_out; + assign rvfi_halt = 1'b0; + assign rvfi_intr = mem_wb_inst0_interrupt_taken_out; + + assign rvfi_mode = 2'b11; // Machine mode + assign rvfi_ixl = 2'b01; // RV32 + + assign rvfi_rs1_addr = mem_wb_inst0_rs1_addr_out; + assign rvfi_rs2_addr = mem_wb_inst0_rs2_addr_out; + assign rvfi_rs1_rdata = mem_wb_inst0_rs1_value_out; + assign rvfi_rs2_rdata = mem_wb_inst0_rs2_value_out; + assign rvfi_rd_addr = wb_inst0_rd_addr_out; + assign rvfi_rd_wdata = wb_inst0_wr_en_out ? wb_inst0_rd_value_out : 32'b0; + + assign rvfi_pc_rdata = mem_wb_inst0_pc_out; + assign rvfi_pc_wdata = mem_wb_inst0_jump_signal_out ? mem_wb_inst0_jump_addr_out + : mem_wb_inst0_pc_out + 32'd4; + + wire rvfi_mem_is_load = rvfi_commit_valid && mem_wb_inst0_mem_read_enable_out; + wire rvfi_mem_is_store = rvfi_commit_valid && mem_wb_inst0_mem_write_enable_out; + + function automatic [3:0] rvfi_load_mask(input [2:0] load_type, input [1:0] addr); + begin + case (load_type) + 3'b000, 3'b100: rvfi_load_mask = 4'b0001 << addr; + 3'b001, 3'b101: rvfi_load_mask = (addr[0] == 1'b0) ? (4'b0011 << addr[1:0]) : 4'b0000; + 3'b010: rvfi_load_mask = 4'b1111; + default: rvfi_load_mask = 4'b0000; + endcase + end + endfunction + + wire [3:0] rvfi_mem_rmask_value = rvfi_load_mask(mem_wb_inst0_load_type_out, + mem_wb_inst0_mem_addr_out[1:0]); + + assign rvfi_mem_addr = (rvfi_mem_is_load || rvfi_mem_is_store) ? mem_wb_inst0_mem_addr_out : 32'b0; + assign rvfi_mem_rmask = rvfi_mem_is_load ? rvfi_mem_rmask_value : 4'b0000; + assign rvfi_mem_rdata = rvfi_mem_is_load ? mem_wb_inst0_mem_data_out : 32'b0; + assign rvfi_mem_wmask = rvfi_mem_is_store ? mem_wb_inst0_write_byte_enable_out : 4'b0000; + assign rvfi_mem_wdata = rvfi_mem_is_store ? mem_wb_inst0_mem_wr_data_out : 32'b0; + + // CSR RVFI channels + wire csr_commit_read = rvfi_commit_valid && mem_wb_inst0_csr_read_enable_out; + wire csr_commit_write = rvfi_commit_valid && mem_wb_inst0_csr_write_enable_out; + wire [11:0] csr_addr_commit = mem_wb_inst0_csr_addr_out; + wire [31:0] csr_rdata_commit = mem_wb_inst0_csr_read_data_out; + wire [31:0] csr_wdata_commit = mem_wb_inst0_csr_write_data_out; + + function automatic [31:0] csr_mask; + input cond; + begin + csr_mask = cond ? 32'hFFFF_FFFF : 32'h0000_0000; + end + endfunction + + assign rvfi_csr_mstatus_rmask = csr_mask(csr_commit_read && (csr_addr_commit == CSR_MSTATUS)); + assign rvfi_csr_mstatus_rdata = (csr_commit_read && (csr_addr_commit == CSR_MSTATUS)) ? csr_rdata_commit : 32'b0; + assign rvfi_csr_mstatus_wmask = csr_mask(csr_commit_write && (csr_addr_commit == CSR_MSTATUS)); + assign rvfi_csr_mstatus_wdata = (csr_commit_write && (csr_addr_commit == CSR_MSTATUS)) ? csr_wdata_commit : 32'b0; + + assign rvfi_csr_misa_rmask = csr_mask(csr_commit_read && (csr_addr_commit == CSR_MISA)); + assign rvfi_csr_misa_rdata = (csr_commit_read && (csr_addr_commit == CSR_MISA)) ? csr_rdata_commit : 32'b0; + assign rvfi_csr_misa_wmask = csr_mask(csr_commit_write && (csr_addr_commit == CSR_MISA)); + assign rvfi_csr_misa_wdata = (csr_commit_write && (csr_addr_commit == CSR_MISA)) ? csr_wdata_commit : 32'b0; + + assign rvfi_csr_mie_rmask = csr_mask(csr_commit_read && (csr_addr_commit == CSR_MIE)); + assign rvfi_csr_mie_rdata = (csr_commit_read && (csr_addr_commit == CSR_MIE)) ? csr_rdata_commit : 32'b0; + assign rvfi_csr_mie_wmask = csr_mask(csr_commit_write && (csr_addr_commit == CSR_MIE)); + assign rvfi_csr_mie_wdata = (csr_commit_write && (csr_addr_commit == CSR_MIE)) ? csr_wdata_commit : 32'b0; + + assign rvfi_csr_mtvec_rmask = csr_mask(csr_commit_read && (csr_addr_commit == CSR_MTVEC)); + assign rvfi_csr_mtvec_rdata = (csr_commit_read && (csr_addr_commit == CSR_MTVEC)) ? csr_rdata_commit : 32'b0; + assign rvfi_csr_mtvec_wmask = csr_mask(csr_commit_write && (csr_addr_commit == CSR_MTVEC)); + assign rvfi_csr_mtvec_wdata = (csr_commit_write && (csr_addr_commit == CSR_MTVEC)) ? csr_wdata_commit : 32'b0; + + assign rvfi_csr_mscratch_rmask = csr_mask(csr_commit_read && (csr_addr_commit == CSR_MSCRATCH)); + assign rvfi_csr_mscratch_rdata = (csr_commit_read && (csr_addr_commit == CSR_MSCRATCH)) ? csr_rdata_commit : 32'b0; + assign rvfi_csr_mscratch_wmask = csr_mask(csr_commit_write && (csr_addr_commit == CSR_MSCRATCH)); + assign rvfi_csr_mscratch_wdata = (csr_commit_write && (csr_addr_commit == CSR_MSCRATCH)) ? csr_wdata_commit : 32'b0; + + assign rvfi_csr_mepc_rmask = csr_mask(csr_commit_read && (csr_addr_commit == CSR_MEPC)); + assign rvfi_csr_mepc_rdata = (csr_commit_read && (csr_addr_commit == CSR_MEPC)) ? csr_rdata_commit : 32'b0; + assign rvfi_csr_mepc_wmask = csr_mask(csr_commit_write && (csr_addr_commit == CSR_MEPC)); + assign rvfi_csr_mepc_wdata = (csr_commit_write && (csr_addr_commit == CSR_MEPC)) ? csr_wdata_commit : 32'b0; + + assign rvfi_csr_mcause_rmask = csr_mask(csr_commit_read && (csr_addr_commit == CSR_MCAUSE)); + assign rvfi_csr_mcause_rdata = (csr_commit_read && (csr_addr_commit == CSR_MCAUSE)) ? csr_rdata_commit : 32'b0; + assign rvfi_csr_mcause_wmask = csr_mask(csr_commit_write && (csr_addr_commit == CSR_MCAUSE)); + assign rvfi_csr_mcause_wdata = (csr_commit_write && (csr_addr_commit == CSR_MCAUSE)) ? csr_wdata_commit : 32'b0; + + assign rvfi_csr_mtval_rmask = csr_mask(csr_commit_read && (csr_addr_commit == CSR_MTVAL)); + assign rvfi_csr_mtval_rdata = (csr_commit_read && (csr_addr_commit == CSR_MTVAL)) ? csr_rdata_commit : 32'b0; + assign rvfi_csr_mtval_wmask = csr_mask(csr_commit_write && (csr_addr_commit == CSR_MTVAL)); + assign rvfi_csr_mtval_wdata = (csr_commit_write && (csr_addr_commit == CSR_MTVAL)) ? csr_wdata_commit : 32'b0; + + assign rvfi_csr_mip_rmask = csr_mask(csr_commit_read && (csr_addr_commit == CSR_MIP)); + assign rvfi_csr_mip_rdata = (csr_commit_read && (csr_addr_commit == CSR_MIP)) ? csr_rdata_commit : 32'b0; + assign rvfi_csr_mip_wmask = csr_mask(csr_commit_write && (csr_addr_commit == CSR_MIP)); + assign rvfi_csr_mip_wdata = (csr_commit_write && (csr_addr_commit == CSR_MIP)) ? csr_wdata_commit : 32'b0; + endmodule diff --git a/rtl/top.v b/rtl/top.v index c856620..ea82d3a 100644 --- a/rtl/top.v +++ b/rtl/top.v @@ -4,19 +4,87 @@ module top ( input wire clk, input wire rst, - + // External interrupt inputs input wire software_interrupt, input wire external_interrupt, - + // UART output output wire uart_tx, - + // Optional debug outputs output wire [31:0] pc_debug, - output wire [31:0] instr_debug + output wire [31:0] instr_debug, + + // RVFI interface for formal verification + output wire rvfi_valid, + output wire [63:0] rvfi_order, + output wire [31:0] rvfi_insn, + output wire rvfi_trap, + output wire rvfi_halt, + output wire rvfi_intr, + output wire [1:0] rvfi_mode, + output wire [1:0] rvfi_ixl, + output wire [4:0] rvfi_rs1_addr, + output wire [4:0] rvfi_rs2_addr, + output wire [31:0] rvfi_rs1_rdata, + output wire [31:0] rvfi_rs2_rdata, + output wire [4:0] rvfi_rd_addr, + output wire [31:0] rvfi_rd_wdata, + output wire [31:0] rvfi_pc_rdata, + output wire [31:0] rvfi_pc_wdata, + output wire [31:0] rvfi_mem_addr, + output wire [3:0] rvfi_mem_rmask, + output wire [31:0] rvfi_mem_rdata, + output wire [31:0] rvfi_mem_wdata, + output wire [3:0] rvfi_mem_wmask, + output wire [31:0] rvfi_csr_mstatus_rmask, + output wire [31:0] rvfi_csr_mstatus_wmask, + output wire [31:0] rvfi_csr_mstatus_rdata, + output wire [31:0] rvfi_csr_mstatus_wdata, + output wire [31:0] rvfi_csr_misa_rmask, + output wire [31:0] rvfi_csr_misa_wmask, + output wire [31:0] rvfi_csr_misa_rdata, + output wire [31:0] rvfi_csr_misa_wdata, + output wire [31:0] rvfi_csr_mie_rmask, + output wire [31:0] rvfi_csr_mie_wmask, + output wire [31:0] rvfi_csr_mie_rdata, + output wire [31:0] rvfi_csr_mie_wdata, + output wire [31:0] rvfi_csr_mtvec_rmask, + output wire [31:0] rvfi_csr_mtvec_wmask, + output wire [31:0] rvfi_csr_mtvec_rdata, + output wire [31:0] rvfi_csr_mtvec_wdata, + output wire [31:0] rvfi_csr_mscratch_rmask, + output wire [31:0] rvfi_csr_mscratch_wmask, + output wire [31:0] rvfi_csr_mscratch_rdata, + output wire [31:0] rvfi_csr_mscratch_wdata, + output wire [31:0] rvfi_csr_mepc_rmask, + output wire [31:0] rvfi_csr_mepc_wmask, + output wire [31:0] rvfi_csr_mepc_rdata, + output wire [31:0] rvfi_csr_mepc_wdata, + output wire [31:0] rvfi_csr_mcause_rmask, + output wire [31:0] rvfi_csr_mcause_wmask, + output wire [31:0] rvfi_csr_mcause_rdata, + output wire [31:0] rvfi_csr_mcause_wdata, + output wire [31:0] rvfi_csr_mtval_rmask, + output wire [31:0] rvfi_csr_mtval_wmask, + output wire [31:0] rvfi_csr_mtval_rdata, + output wire [31:0] rvfi_csr_mtval_wdata, + output wire [31:0] rvfi_csr_mip_rmask, + output wire [31:0] rvfi_csr_mip_wmask, + output wire [31:0] rvfi_csr_mip_rdata, + output wire [31:0] rvfi_csr_mip_wdata ); + // Size memories differently for formal vs functional builds +`ifdef FORMAL + localparam integer INSTR_MEM_WORDS = 32; + localparam integer DATA_MEM_BYTES = 64; +`else + localparam integer INSTR_MEM_WORDS = 4096; // 16KB instruction space + localparam integer DATA_MEM_BYTES = 4096; // 4KB data space +`endif + // Wires to connect CPU and memories wire [31:0] cpu_pc_out; wire [31:0] instr_to_cpu; @@ -30,41 +98,41 @@ module top ( wire [3:0] cpu_write_byte_enable; // Write byte enables wire [2:0] cpu_load_type; // Load type wire [31:0] instr_read_data; - + // Timer module wires wire [31:0] timer_read_data; wire timer_valid; wire timer_interrupt; - + // UART module wires wire [31:0] uart_read_data; wire uart_valid; wire uart_access; - + // Memory address decoding using memory map wire data_mem_access; wire timer_access; wire instr_mem_access; - + // Use memory map macros for clean address decoding assign data_mem_access = `IS_DATA_MEM(data_mem_addr); assign timer_access = `IS_TIMER_MEM(data_mem_addr); assign uart_access = `IS_UART_MEM(data_mem_addr); assign instr_mem_access = `IS_INSTR_MEM(data_mem_addr); - + // Select the appropriate address for memory access assign data_mem_addr = cpu_mem_write_en ? cpu_mem_write_addr : cpu_mem_read_addr; - + // Multiplex read data based on address - assign mem_read_data = timer_access ? timer_read_data : + assign mem_read_data = timer_access ? timer_read_data : data_mem_access ? data_mem_read_data : uart_access ? uart_read_data : instr_mem_access ? instr_read_data : 32'h00000000; - + // Debug outputs assign pc_debug = cpu_pc_out; assign instr_debug = instr_to_cpu; - + // Data memory read data (separate wire for clarity) wire [31:0] data_mem_read_data; @@ -84,14 +152,73 @@ module top ( .module_read_addr(cpu_mem_read_addr), .module_write_addr(cpu_mem_write_addr), .module_write_byte_enable(cpu_write_byte_enable), - .module_load_type(cpu_load_type) + .module_load_type(cpu_load_type), + + // RVFI interface connections + .rvfi_valid(rvfi_valid), + .rvfi_order(rvfi_order), + .rvfi_insn(rvfi_insn), + .rvfi_trap(rvfi_trap), + .rvfi_halt(rvfi_halt), + .rvfi_intr(rvfi_intr), + .rvfi_mode(rvfi_mode), + .rvfi_ixl(rvfi_ixl), + .rvfi_rs1_addr(rvfi_rs1_addr), + .rvfi_rs2_addr(rvfi_rs2_addr), + .rvfi_rs1_rdata(rvfi_rs1_rdata), + .rvfi_rs2_rdata(rvfi_rs2_rdata), + .rvfi_rd_addr(rvfi_rd_addr), + .rvfi_rd_wdata(rvfi_rd_wdata), + .rvfi_pc_rdata(rvfi_pc_rdata), + .rvfi_pc_wdata(rvfi_pc_wdata), + .rvfi_mem_addr(rvfi_mem_addr), + .rvfi_mem_rmask(rvfi_mem_rmask), + .rvfi_mem_rdata(rvfi_mem_rdata), + .rvfi_mem_wdata(rvfi_mem_wdata), + .rvfi_mem_wmask(rvfi_mem_wmask), + .rvfi_csr_mstatus_rmask(rvfi_csr_mstatus_rmask), + .rvfi_csr_mstatus_wmask(rvfi_csr_mstatus_wmask), + .rvfi_csr_mstatus_rdata(rvfi_csr_mstatus_rdata), + .rvfi_csr_mstatus_wdata(rvfi_csr_mstatus_wdata), + .rvfi_csr_misa_rmask(rvfi_csr_misa_rmask), + .rvfi_csr_misa_wmask(rvfi_csr_misa_wmask), + .rvfi_csr_misa_rdata(rvfi_csr_misa_rdata), + .rvfi_csr_misa_wdata(rvfi_csr_misa_wdata), + .rvfi_csr_mie_rmask(rvfi_csr_mie_rmask), + .rvfi_csr_mie_wmask(rvfi_csr_mie_wmask), + .rvfi_csr_mie_rdata(rvfi_csr_mie_rdata), + .rvfi_csr_mie_wdata(rvfi_csr_mie_wdata), + .rvfi_csr_mtvec_rmask(rvfi_csr_mtvec_rmask), + .rvfi_csr_mtvec_wmask(rvfi_csr_mtvec_wmask), + .rvfi_csr_mtvec_rdata(rvfi_csr_mtvec_rdata), + .rvfi_csr_mtvec_wdata(rvfi_csr_mtvec_wdata), + .rvfi_csr_mscratch_rmask(rvfi_csr_mscratch_rmask), + .rvfi_csr_mscratch_wmask(rvfi_csr_mscratch_wmask), + .rvfi_csr_mscratch_rdata(rvfi_csr_mscratch_rdata), + .rvfi_csr_mscratch_wdata(rvfi_csr_mscratch_wdata), + .rvfi_csr_mepc_rmask(rvfi_csr_mepc_rmask), + .rvfi_csr_mepc_wmask(rvfi_csr_mepc_wmask), + .rvfi_csr_mepc_rdata(rvfi_csr_mepc_rdata), + .rvfi_csr_mepc_wdata(rvfi_csr_mepc_wdata), + .rvfi_csr_mcause_rmask(rvfi_csr_mcause_rmask), + .rvfi_csr_mcause_wmask(rvfi_csr_mcause_wmask), + .rvfi_csr_mcause_rdata(rvfi_csr_mcause_rdata), + .rvfi_csr_mcause_wdata(rvfi_csr_mcause_wdata), + .rvfi_csr_mtval_rmask(rvfi_csr_mtval_rmask), + .rvfi_csr_mtval_wmask(rvfi_csr_mtval_wmask), + .rvfi_csr_mtval_rdata(rvfi_csr_mtval_rdata), + .rvfi_csr_mtval_wdata(rvfi_csr_mtval_wdata), + .rvfi_csr_mip_rmask(rvfi_csr_mip_rmask), + .rvfi_csr_mip_wmask(rvfi_csr_mip_wmask), + .rvfi_csr_mip_rdata(rvfi_csr_mip_rdata), + .rvfi_csr_mip_wdata(rvfi_csr_mip_wdata) ); // Instantiate instruction memory instr_mem #( .DATA_WIDTH(32), .ADDR_WIDTH(32), - .MEM_SIZE(131072) // 512KB / 4 bytes = 128K words + .MEM_SIZE(INSTR_MEM_WORDS) ) instr_mem_inst ( .instr_addr(cpu_pc_out), .instr_addr_p2(data_mem_addr), @@ -100,11 +227,11 @@ module top ( .instr_p2(instr_read_data) ); - // Instantiate data memory + // Instantiate data memory data_mem #( .DATA_WIDTH(32), .ADDR_WIDTH(32), - .MEM_SIZE(1048576) // 1MB in bytes + .MEM_SIZE(DATA_MEM_BYTES) ) data_mem_inst ( .clk(clk), .wr_en(cpu_mem_write_en && data_mem_access), @@ -115,7 +242,7 @@ module top ( .wr_data(cpu_mem_write_data), .rd_data_out(data_mem_read_data) ); - + // Instantiate timer module timer timer_inst ( .clk(clk), @@ -145,14 +272,14 @@ module top ( `ifdef COCOTB_SIM // Add parameter to control FST file path reg [1023:0] dumpfile_path = "riscv_cpu.fst"; // Default path - + initial begin // Check for custom dump file name from plusargs if (!$value$plusargs("dumpfile=%s", dumpfile_path)) begin // Use default if not specified dumpfile_path = "riscv_cpu.fst"; end - + // Set up wave dumping $dumpfile(dumpfile_path); $dumpvars(0, top); @@ -160,4 +287,4 @@ module top ( end `endif -endmodule \ No newline at end of file +endmodule diff --git a/tests/unit_tests/test_alu.py b/tests/unit_tests/test_alu.py index bc2940c..0470e1c 100644 --- a/tests/unit_tests/test_alu.py +++ b/tests/unit_tests/test_alu.py @@ -2,7 +2,29 @@ from cocotb.triggers import Timer import random import os -from pathlib import Path +import sys +from contextlib import contextmanager + + +@contextmanager +def prepend_to_path(*path_entries: str): + """Temporarily prepend directories to PATH for simulator subprocesses.""" + entries = [entry for entry in path_entries if entry] + if not entries: + yield + return + + original_path = os.environ.get("PATH") + prefix = os.pathsep.join(entries) + new_path = prefix if not original_path else f"{prefix}{os.pathsep}{original_path}" + os.environ["PATH"] = new_path + try: + yield + finally: + if original_path is None: + os.environ.pop("PATH", None) + else: + os.environ["PATH"] = original_path # Helper function to verify ALU operation async def verify_alu_operation(dut, rs1, rs2, imm, instruction, pc_input, expected_output, operation_name): @@ -226,10 +248,14 @@ def runCocotbTests(): incl_dir = os.path.join(rtl_dir, "include") verilog_file = os.path.join(rtl_dir, "core_modules", "alu.v") - run( - verilog_sources=[verilog_file], - toplevel="alu", - module="test_alu", - simulator="verilator", - includes=[incl_dir] - ) + tools_dir = os.path.join(root_dir, "tests", "tools") + python_dir = os.path.dirname(sys.executable) + with prepend_to_path(tools_dir, python_dir): + run( + verilog_sources=[verilog_file], + toplevel="alu", + module="test_alu", + simulator="verilator", + includes=[incl_dir], + extra_env={"PYTHON3": sys.executable}, + ) diff --git a/tests/unit_tests/test_decoder_gcc.py b/tests/unit_tests/test_decoder_gcc.py index c5ca1d1..4227d70 100644 --- a/tests/unit_tests/test_decoder_gcc.py +++ b/tests/unit_tests/test_decoder_gcc.py @@ -2,6 +2,29 @@ from cocotb.triggers import Timer import subprocess import os +import sys +from contextlib import contextmanager + + +@contextmanager +def prepend_to_path(*path_entries: str): + """Temporarily prepend directories to PATH for simulator subprocesses.""" + entries = [entry for entry in path_entries if entry] + if not entries: + yield + return + + original_path = os.environ.get("PATH") + prefix = os.pathsep.join(entries) + new_path = prefix if not original_path else f"{prefix}{os.pathsep}{original_path}" + os.environ["PATH"] = new_path + try: + yield + finally: + if original_path is None: + os.environ.pop("PATH", None) + else: + os.environ["PATH"] = original_path def assemble_riscv_instruction(assembly_code, bin_file="temp.bin"): with open("temp.s", "w") as f: @@ -129,12 +152,16 @@ def runCocotbTests(): instr_defines_file = os.path.join(rtl_dir, "instr_defines.vh") decoder_file = os.path.join(rtl_dir, "core_modules", "decoder.v") - run( - verilog_sources=[ - decoder_file - ], - toplevel="decoder", - module="test_decoder_gcc", - simulator="verilator", - includes=[str(incl_dir)], - ) \ No newline at end of file + tools_dir = os.path.join(root_dir, "tests", "tools") + python_dir = os.path.dirname(sys.executable) + with prepend_to_path(tools_dir, python_dir): + run( + verilog_sources=[ + decoder_file + ], + toplevel="decoder", + module="test_decoder_gcc", + simulator="verilator", + includes=[str(incl_dir)], + extra_env={"PYTHON3": sys.executable}, + )