Name		Name	Last commit message	Last commit date
parent directory ..
.gitignore		.gitignore
README.md		README.md
cexdata.sh		cexdata.sh
checks.cfg		checks.cfg
checks.gtkw		checks.gtkw
complete.sby		complete.sby
complete.sv		complete.sv
cover.sby		cover.sby
cover.sv		cover.sv
disasm.py		disasm.py
dmemcheck.sv		dmemcheck.sv
equiv.sh		equiv.sh
honest.sby		honest.sby
honest.sv		honest.sv
imemcheck.sv		imemcheck.sv
testbugs.sh		testbugs.sh
wrapper.sv		wrapper.sv

README.md

riscv-formal proofs for picorv32

Quickstart guide:

First install Yosys, SymbiYosys, and the solvers. See here for instructions. Then download the core, generate the formal checks and run them:

wget -O picorv32.v https://raw.githubusercontent.com/cliffordwolf/picorv32/master/picorv32.v
python3 ../../checks/genchecks.py
make -C checks -j$(nproc)