Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

vyges-lec — equivalence and property checking

Installed with the physical engines. Install it with vyges install physical (or vyges install lec), then run vyges physical lec. It is also a standalone vyges-lec binary on your PATH (the integration contract for flow authors).

vyges-lec proves things about gate-level netlists instead of sampling them. A simulator shows two designs agree on the vectors you ran; vyges-lec proves they agree on all of them, or hands you the input where they don’t.

Three questions

CommandQuestionOn failure
checkDo two netlists compute the same logic between registers? Registers are matched by instance name.the first differing endpoint (every one, with --engine bdd) and an input assignment that shows it
secDo two netlists give the same outputs on every input sequence, from the same register state? Registers need not line up.the output, the clock cycle, and the inputs of every cycle up to it
proveCan this net of one netlist ever be 1? An error flag, a “two grants at once” net.the net, the cycle, and the inputs of every cycle up to it

Run it

vyges install physical                                                    # one-time
vyges physical lec check golden.v revised.v --lib cells.lib                 # combinational (ABC)
vyges physical lec check golden.v revised.v --lib cells.lib --engine bdd    # exact BDDs, every endpoint
vyges physical lec sec   golden.v revised.v --lib cells.lib                 # sequential
vyges physical lec prove design.v --lib cells.lib --never err               # a proof
vyges physical lec prove design.v --lib cells.lib --never err --bound 20    # cycles 0..20

vyges-lec sec — NOT EQUIVALENT ✗  (1 output(s) compared; 1 vs 2 register(s))
  `y` differs in cycle 3 (cycle 0 is before the first clock edge), under:
    cycle 0: en=1
    cycle 1: en=1
    cycle 2: en=1
    cycle 3: en=0

Every command takes --json and -o FILE; --fail-on-diff makes a failure exit 3 and an undecided run exit 4, for CI.

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

How it models a netlist

  • A gate is its output pin’s Liberty function, so AOI/OAI, multi-output and tie cells are covered. A tied pin is its constant, a supply0/supply1 net its value; an unconnected input or an unknown cell in a compared cone is an error, never a silent answer.
  • check has two engines: ABC’s SAT-based prover (the default), which scales to real netlists, and an exact in-tree BDD engine (--engine bdd) that lists every differing endpoint on designs small enough for it. --engine both runs the two and fails if they disagree.
  • sec and prove keep the registers as state: each is its cell’s Liberty ff group, from 0, on one rising-edge clock reached through buffers. An asynchronous clear or preset acts at the clock edge. Inverted, gated or generated clocks, a second clock and latches are reported as errors rather than modelled approximately.
  • A sequential counterexample is replayed on the netlists before it is reported.

Where it sits

Netlists + Liberty in, a verdict out (text or --json, with a CI exit code). It guards every synthesis, ECO and hand edit: check and sec between any two stages of a flow, prove on the properties a design must never violate.