forked from tampler/yosys-formal
Formal verification with yosys
- Coq 86%
- Verilog 13.4%
- Makefile 0.6%
| gen | ||
| lec | ||
| rtl | ||
| syn | ||
| tech/osu035 | ||
| .gitignore | ||
| Makefile | ||
| README.md | ||
Yosys formal verification guide
This project contains a cookbook for formal verification methods
App 1: Logic equivalence check
- Synthesize and map a simple design under test (DUT) into the OSU 350nm technology
- Run Yosys Logic Equivalence check (LEC) to prove functional equivalence of both circuits
Resources
Usage
- Running synthesis:
make dosyn - Running LEC:
make dolec