vyges-lec — combinational logic equivalence

Part of the Vyges Loom suite. Install once with vyges install loom, then run vyges loom lec. It’s also a standalone vyges-lec binary on your PATH (the integration contract for flow authors).

vyges-lec answers: do two gate-level netlists compute the same function? It is the formal sibling of simulation — a simulator shows two designs agree on the vectors you ran; LEC proves they agree on all of them, or hands you the input where they don’t. It builds a canonical ROBDD for every endpoint of both designs over one shared variable order; equal functions share a node, so the check is exact, and a mismatch’s miter walks straight to a counter-example.

Run it

vyges install loom                                                   # one-time
vyges loom lec check golden.v revised.v --lib cells.lib               # -> verdict
vyges loom lec check golden.v revised.v --lib cells.lib --fail-on-diff # exit 3 if differ

vyges-lec — NOT EQUIVALENT ✗  (1 compared, 1 differ)
  differ at `f`   when a=1 b=0

Sequential designs are cut at the registers — flop Q nets are free inputs, flop D nets are endpoints — so it proves the combinational logic between registers (registers matched by name).

See the full CLI reference (generated from --help).

Where it sits

Golden + revised netlists + Liberty → an equivalence verdict (text or --json, with a CI exit code). It guards every synthesis, ECO, and hand-edit. Gate functions come from a standard-cell primitive map (an unknown cell is a hard error, never a silent wrong answer); the Liberty function-attribute path and an AIG+SAT scaling path are the depth passes.