vyges physical formal — CLI reference

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

vyges formal — a formal property campaign on an IP's RTL, to one report

usage:
  vyges formal run    MANIFEST [--out DIR] [--jobs N] [--only ID,ID] [--no-mutants] [--json]
  vyges formal replay MANIFEST ID --out DIR [--show SIGNAL,SIGNAL]
  vyges formal report MANIFEST --out DIR

commands:
  run      bind the manifest's monitors into the RTL, synthesize, prove every property and cover
           with vyges-lec, replay every counterexample in Verilator, re-prove every mutant, and
           write DIR/report.md and DIR/report.json
  replay   replay one counterexample of a finished run, printing the claim and any --show signals
           (flattened names, e.g. u_core.state_q) cycle by cycle
  report   re-render a finished run's report after editing the manifest's expectations or text
           (no proof is re-run; refused if the RTL has moved to another commit since the run)

flags:
  --out DIR        the run's directory (run: default ./formal-<ip name>)
  --jobs N         proofs in parallel (default: half the cores)
  --only ID,ID     run only these properties/covers
  --no-mutants     skip the mutants
  --json           run: print a JSON summary on stdout when done
  --lec P · --yosys P · --verilator P · --sv2v P · --liberty FILE
                   the programs and the Liberty (default: the manifest, then
                   VYGES_FORMAL_LEC / _YOSYS / _VERILATOR / _SV2V / _LIBERTY, then PATH);
                   sv2v only for [rtl] frontend = "sv2v" (SystemVerilog packages, imports)
  --describe       print a machine-readable JSON description of every command
  -h, --help · -V, --version

The manifest (TOML) names the RTL ([rtl] repo, files, top, clock, params), the monitors and the
module each binds into ([[bind]]), and every [[assumption]], [[property]], [[cover]] and [[mutant]].
A monitor defines vf_p_<id> (1 = property violated), vf_c_<id> (1 = cover hit) and vf_a_<id>
(0 = assumption broken) from the nets of the module it binds into.

exit: 0 every result as expected · 2 something unexpected, or usage · 1 tool error

Contract

Generated from vyges physical formal --describe.

formal

a formal property campaign on an IP’s RTL: monitors bound into the design, every property and cover proved or refuted, counterexamples replayed in simulation, mutants to measure the property set, one report

Maturity: structured

run {manifest} --json

Consumes: rtl, liberty

Artifacts: formal_report (report_path)

Assertion: all-as-expected — passes when all_as_expected is true

Threads

• Option: --jobs
• Default: half the cores

Proofs run as child processes, –jobs at a time (default half the cores); lower it to share the machine with other runs.

Provenance limitations

• Every result belongs to the RTL commit recorded in the report; a dirty working tree is flagged, not refused.
• Proofs start from the all-zero register state (the prover’s model); a register without reset is listed in the report’s lint, and its zero start is an assumption, not a proof.
• Inputs are free except for the manifest’s assumptions; memory read data is free unless the monitors model it.
• A bounded result (holds_within N) says nothing past cycle N; a timeout is undecided, never a pass.
• Needs yosys and Verilator on PATH and vyges-lec (installed with the physical engines); without Verilator, counterexamples are reported unreplayed.

formal.replay

replay one counterexample of a finished run in simulation, cycle by cycle

replay {manifest} {id} --out {out}

formal.report

re-render a finished run’s report from its report.json (no proof re-run)

report {manifest} --out {out}