Vyges Loom
Logic equivalence check — did that synthesis, ECO or hand-edit keep the logic the same? Prove two netlists compute the same function across all inputs — or get the one input where they differ.
Used by: anyone who edits a netlist after synthesis — an ECO, a clock-gate insertion, a hand-fix — and needs to know the logic still means the same thing.
Every synthesis, ECO and hand-edit is a promise that the logic still means the same thing. Simulation can only spot-check that promise on the vectors you happened to run. vyges-lec proves it across all 2n inputs at once — or hands you the one input where the promise broke. It is the formal complement to simulation: it builds a canonical decision diagram for every output of both designs, so equal functions are provably equal, and a mismatch yields a concrete counter-example.
.lib ──► vyges-lec ──► EQUIVALENT ✓ / NOT ✗ (+ counter-example)
It builds a canonical, reduced, ordered BDD for every endpoint of both designs over one shared variable order — so two functions are equal iff they share a node, and the check is exact rather than a sampled run. When they differ, the miter walks straight to a satisfying input. Sequential designs are cut at the registers — the standard combinational equivalence model.
vyges-lec — NOT EQUIVALENT ✗ (1 compared, 1 differ) differ at `f` when a=1 b=0
A clean-room Rust engine with an in-tree decision-diagram core — no external solver dependency — runnable today on the same Liberty / Verilog the rest of Loom reads. See all the engines & the data spine →