8779bcd1db
Provide a process to create a single Verilog source of Ibex for riscv-formal. Option to enable writeback stage. |
||
|---|---|---|
| .. | ||
| .gitignore | ||
| Makefile | ||
| README.md | ||
Formal
Unsupported Verilog source creation for RISC-V Formal Verification.
The Verilog source created here is used by riscv-formal.
Riscv-formal uses Yosys, but the SystemVerilog front-end of Yosys does not support all the language features used by Ibex.
The Makefile provided here uses sv2v and Yosys to create a single Verilog source of Ibex.
This flow has some similarities to syn, but uses only a simplified subset.
In order to make it easier to use with riscv-formal, the conversion is done with a simple Makefile.
Prerequisites
Install the following, if not used with the container flow described in riscv-formal.
- sv2v, best option is to use the latest version, but packed arrays is required
- Yosys
Limitations
The "M" extension is currently disabled.
Usage
It should not be necessary to create the Verilog source manually as it is used by the riscv-formal Ibex build system.
Run the following command from the top level directory of Ibex to create the Verilog source.
make -C formal
This will create a directory formal/build which contains an equivalent Verilog file for each SystemVerilog source. The single output file formal/ibex.v contains the complete Ibex source, which can then be imported by riscv-formal.