vyges-formal — property campaigns on RTL
Installed with the physical engines. Install it with
vyges install physical, then runvyges formal(orvyges physical formal). It is also a standalonevyges-formalbinary on your PATH (the integration contract for flow authors). Source: vyges-tools/formal.
Simulation shows a design does the right thing on the tests someone wrote. A property campaign
asks the stronger question early, while the RTL is still changing: does the design keep its
promises on every input sequence? vyges-formal runs one from a manifest and writes one report,
with every result tied to the git commit of the RTL it was run on.
| command | does |
|---|---|
run | binds the monitors into the RTL, synthesizes, proves every property and cover with vyges-lec, replays every counterexample in Verilator, re-proves every mutant, and writes report.md and report.json |
replay | one counterexample of a finished run, cycle by cycle, with any internal signals named by --show |
report | re-renders a finished run after the manifest’s expectations or text change (refused if the RTL moved to another commit) |
Run it
vyges install physical # one-time
vyges formal run manifest.toml --out formal-out # prove, replay, mutate, report
vyges formal replay manifest.toml c4_write_addr_in_range --out formal-out --show u_core.state_q
vyges formal report manifest.toml --out formal-out
A campaign also needs Yosys and
Verilator on PATH (sv2v too for
SystemVerilog with packages or interfaces, frontend = "sv2v"), and a Liberty for the proof model
(--liberty FILE, or [synth] liberty in the manifest). Exit status: 0 when every result is as
expected, 2 when anything is not, 1 on a tool error.
The manifest and the monitors
The manifest (TOML) names the RTL (a git repository, its files, the top, the clock, parameters), the monitors and the module each binds into, and every assumption, property, cover and mutant. A monitor is plain Verilog spliced into the module it watches, so it reads that module’s nets by name, and it names its claims by convention:
| net | meaning |
|---|---|
vf_p_<id> | 1 when property <id> is violated |
vf_c_<id> | 1 when cover <id> is hit |
vf_a_<id> | 0 when assumption <id> is broken |
A claim counts only once reset has been asserted and released, and only while every assumption it names has held. The full manifest format is in the vyges-formal README.
What the report says
- Proved properties hold on every input sequence from reset, under the stated assumptions.
- A failing property comes with a counterexample, replayed in Verilator as a second witness.
- A cover shows the assumptions still allow a behaviour; an unreachable cover is dead logic or an assumption that is too strong.
- A mutant that no property catches is a gap in the property set.
- A finding is a failure recorded against the specification, tracked commit to commit until the RTL is fixed.
Proofs start from the all-zero register state; registers without reset are listed, because their zero start is an assumption. Memory read data is free unless a monitor models the memory.