Yosys formal verification guide

This project contains a cookbook for formal verification methods

App 1: Logic equivalence check

• Synthesize a simple design under test (DUT) down to Yosys' generic ($-)cells
• Run Yosys Logic Equivalence check (LEC) to prove functional equivalence of both circuits

Resources

• Yosys docs
• Yosys synthesis suite toolset

Usage

The flow defaults to the counter design; override it with design=<name> (available designs: counter, lfsr).

• Running synthesis: make dosyn (writes gen/<design>_mapped.v)
• Running LEC: make dolec (re-synthesizes the netlist first if it is stale)
• Running LEC for every design: make test
• Picking a design: make dolec design=lfsr
• Listing targets: make help

The generated netlists in gen/ are build artifacts (git-ignored). Because the netlist is built from Yosys' internal ($-)cells, the SAT engine already knows their semantics -- no behavioral cell models are needed to prove equivalence.