vyges physical lec — CLI reference

Generated from vyges physical lec --help — this page is the tool’s own output, verbatim.

vyges physical lec — logic equivalence (combinational, sequential) and property checking

usage:
  vyges physical lec check GOLDEN.v REVISED.v --lib L.lib [--engine E] [-o OUT] [--json] [--fail-on-diff]
  vyges physical lec sec   GOLDEN.v REVISED.v --lib L.lib [-o OUT] [--json] [--fail-on-diff]
  vyges physical lec prove DESIGN.v --lib L.lib --never NET [--never NET ...] [--bound N]
                          [-o OUT] [--json] [--fail-on-diff]

commands:
  check            combinational: registers cut and matched by instance name
  sec              sequential: registers kept as state, primary outputs compared on every
                   input sequence from the all-zero register state (one clock; needs --features abc)
  prove            property: each --never NET stays 0 on every input sequence from the all-zero
                   register state; --bound N checks cycles 0..N only (needs --features abc)

flags:
  --lib FILE       Liberty (pin directions + comb/seq split) — required
  --engine E       abc: SAT-based (ABC), scales to real netlists, names the first differing
                        endpoint (the default in a build with --features abc, as released)
                   bdd: exact BDDs, lists every differing endpoint (the default without it)
                   both: run both and fail if they disagree; reports the bdd result
  -o FILE          write the report to FILE (default: stdout)
  --json           machine-readable JSON instead of text
  --fail-on-diff   exit 3 if the designs are not equivalent (prove: a net can be 1),
                   4 if undecided (CI gate); without it a verdict exits 0
  --describe       print a machine-readable JSON description of every command
  -h, --help · -V, --version

Contract

Generated from vyges physical lec --describe.

lec

formal checks on gate-level netlists: combinational and sequential equivalence, and property checking, with counter-examples

Maturity: structured

check {golden} {revised} --lib {lib}

Consumes: netlist, liberty

Artifacts: equivalence_report (report_path)

Assertion: logic-equivalent — passes when equivalent is true

Threads

Runs on one thread; there is no thread option. Several jobs can run side by side, one core each.

Provenance limitations

• input_hash covers the argument vector, not the content of the netlists or the Liberty it names.
• Liberty include files are not enumerated.
• check is COMBINATIONAL: registers are cut (an output a free input, a data pin an endpoint) and matched by instance name, so two designs that differ only in register naming or retiming are reported as differing.
• check’s default engine is ABC’s SAT-based prover in the released build (built with the ABC engine), which names the FIRST differing endpoint; –engine bdd lists every differing endpoint but its BDDs can grow past what a real core allows; –engine both runs the two and is an error if they disagree. A build without the ABC engine has only bdd, and sec and prove exit 2.
• sec and prove share one sequential model: registers are their Liberty ff groups, all starting at 0, on ONE rising-edge clock traced back through buffers to a primary input. Asynchronous clear and preset are modelled synchronously. Latches, register banks, inverted or gated clocks and a second clock are refused with an error rather than approximated.
• Every counter-example sec or prove reports is replayed on the model before it is reported; one that does not replay is an error, never a verdict.
• Any command can be UNDECIDED when ABC gives up within its limits; it is reported as undecided (exit 4 with –fail-on-diff), never as a pass.
• prove –bound N checks cycles 0 to N only: no failure there is holds_within, which is not a proof.

lec.sec

sequential equivalence: registers kept as state, primary outputs compared on every input sequence from the all-zero register state

sec {golden} {revised} --lib {lib}

Assertion: sequentially-equivalent — passes when equivalent is true

lec.prove

property check: each named net stays 0 on every input sequence from the all-zero register state

prove {design} --lib {lib}

Assertion: property-holds — passes when verdict is one of holds, holds_within