hdl-tools/digital-chip-design-agents/formal-verification

Skill: Formal Verification (FPV + LEC)

Invocation

When this skill is loaded and a user presents a formal verification task, do not execute stages directly. Immediately spawn the digital-chip-design-agents:formal-orchestrator agent and pass the full user request and any available context to it. The orchestrator enforces the stage sequence, loop-back rules, and sign-off criteria defined below.

Use the domain rules in this file only when the orchestrator reads this skill mid-flow for stage-specific guidance, or when the user asks a targeted reference question rather than requesting a full flow execution.

Pre-run Context

Before executing or advising on any stage, read the following files if they exist:

1. memory/formal/knowledge.md — known failure patterns, successful tool flags, PDK/tool quirks.

Incorporate its guidance into every stage decision. If absent, proceed without it.

1. memory/formal/run_state.md — current run identity (run_id, design_name, tool,

last_stage). Use this to resume correctly after interruption. If absent, a new run is starting; the orchestrator will create this file before the first stage.

This pre-run read applies whether this skill is loaded by a user or called by the orchestrator mid-flow. It ensures the fix database is consulted before any diagnosis step.

Purpose

Exhaustively prove design properties and equivalence using formal methods. Complements simulation-based verification for correctness proofs, protocol compliance, and equivalence checking between RTL and gate-level netlists.

Supported EDA Tools

Open-Source

• SymbiYosys (sby) — formal property verification front-end for open-source solvers
• Yosys (yosys) — synthesis and equivalence checking back-end
• Boolector — SMT solver for bit-vector arithmetic
• Z3 — general-purpose SMT solver from Microsoft Research
• ABC — logic synthesis and verification framework (sequential equivalence)
• Tabby CAD Suite — commercial bundle of sby + solvers (from YosysHQ)

Proprietary

• Cadence JasperGold (jg, dialect cadence) — industry-standard FPV, CDC, DFT formal
• Synopsys VC Formal (vcf, dialect synopsys) — property checking and equivalence verification
• Siemens Questa Formal (qformal, dialect siemens) — FPV and coverage closure
• Synopsys Formality (fm_shell, dialect synopsys) — RTL↔netlist and netlist↔netlist

equivalence (LEC); wrapper wrap-fm.sh

• Cadence Conformal LEC (lec, dialect cadence) — RTL↔netlist and netlist↔netlist

equivalence (LEC); wrapper wrap-lec.sh

Stage: property_planning

Property Categories

1. Safety: "something bad never happens"

assert property (@(posedge clk) !(error && valid));

1. Liveness: "something good eventually happens" (always bound the interval)

assert property (@(posedge clk) req |-> ##[1:MAX] ack);

1. Stability: "output is stable while condition holds"

assert property (@(posedge clk) valid |-> $stable(data));

1. Reachability: "a state is reachable" (use cover, not assert)

cover property (@(posedge clk) state == DONE);

Domain Rules

1. Every spec feature: at least one property or cover point
2. All properties: include descriptive name and failure message
3. Liveness properties: always bound with ##[1:BOUND]
4. Use $past(), $rose(), $fell() over manual delay logic
5. disable iff: use for reset gating
6. Take the RTL hand-off as an input: every entry in design_state.rtl.unverified[] (claims

the RTL flow concluded without a tool run) gets a property, a cover, or a written reason it is not formally tractable and who checks it instead. If rtl.unverified is absent the RTL flow did not report — say so in the property plan and derive the targets below from the RTL yourself; do not read "absent" as "nothing to prove"

1. Prove at boundary parameter values, not only the default: a proof holds for one

parameterisation. Re-run at WIDTH=1, DEPTH=1 and 2, N=1, and any non-power-of-two value the module accepts. A guarded initial/$fatal parameter assertion in the RTL sits inside synthesis translate_off and may be invisible to the formal front-end, so restate the legal parameter range in the environment

Property Targets Lint Cannot Prove

A clean lint run says nothing about these. Each applies wherever the structure exists:

QoR Metrics to Evaluate

• All spec features mapped to property or cover
• Every rtl.unverified[] entry mapped to a property, a cover, or a stated reason
• Cover points: key states are reachable

Output Required

• Property plan (feature → property mapping)
• SVA property file (.sva)
• SVA assumption file

Stage: environment_setup

Domain Rules

1. Constrain all primary inputs to legal values only
2. Protocol assumptions: model upstream block behaviour
3. Reset assumption: force correct reset sequence at time 0
4. Over-constraining → vacuous proof (nothing can be proven wrong) — always run vacuity check
5. Under-constraining → false CEX (environment bug, not DUT) — check all CEX carefully
6. Vacuity check: disable each assume — property should NOT hold without it
7. Document every assumption with justification

Common Assumption Templates

// Reset sequence
assume property (@(posedge clk) $rose(rst_n) |-> ##[1:5] rst_n);
 
// AXI valid stability
assume property (@(posedge clk)
  (s_axi_awvalid && !s_axi_awready) |=> $stable(s_axi_awaddr));

QoR Metrics to Evaluate

• Vacuity check: PASS for all properties
• No over-constraining: formal tool reports reasonable state space
• Environment signed off by verification lead

Output Required

• Formal environment file (constraints/assumptions)
• Vacuity check report
• Environment review record

Stage: fpv_run

Result Classifications

Strategies for Inconclusive

1. Increase BMC bound (k-induction)
2. Apply abstractions (data abstraction, counter abstraction)
3. Decompose: prove sub-properties; compose to main property
4. If intractable, record the property as UNVERIFIED with the bound reached and the

justification. A bounded proof is not PROVEN and an assumed-correct property is not a result — neither counts toward the PROVEN total, and a P0 property left UNVERIFIED blocks sign-off

QoR Metrics to Evaluate

• Target: 100% PROVEN or UNREACHABLE (no unanalysed CEX)
• All INCONCLUSIVE: documented with justification and bound used

Output Required

• FPV run report (per property: result, CEX trace if applicable)
• CEX waveform descriptions for failures

Stage: cex_analysis

Domain Rules

1. Every CEX: determine if it is a real DUT bug or an assumption/environment bug
2. Real DUT bug: do not edit the RTL from this flow. Write a fix_request entry to

design_state.fix_requests[] (failure_class=formal_cex, CEX trace path, the property that failed) and stop; the RTL flow applies the fix under its own lint rules and FPV is re-run on the result. Counts as an RTL bug, not a formal bug

1. Assumption bug: tighten assumption → re-run vacuity check
2. False CEX from under-constraining: document clearly before adding assumption
3. Never waive a CEX without root cause
4. A CEX must not be cleared by narrowing the environment. Before adding or tightening an

assumption, confirm the excluded behaviour is illegal per the spec or the upstream block's contract; an assumption that removes legal stimulus hides the bug instead of fixing it. Likewise never weaken or delete the failing property to get a pass

1. State what located the bug: set suspected_rtl.basis to traced when the CEX trace shows

the faulty signal and cycle, hypothesis when the location is inferred

Output Required

• CEX analysis report (bug or false alarm, root cause, fix applied)

Stage: lec_run

LEC Flow

1. Read golden: RTL or pre-ECO netlist
2. Read revised: post-synthesis netlist or post-ECO netlist
3. Map points: match sequential/combinational key points
4. Verify all points: compare cone-of-influence
5. Report: EQUIVALENT / UNMATCHED / ABORTED

Tool outline (standard commands only; measured notes pending):

• Formality (fm_shell -f lec.tcl, through wrap-fm.sh): read_db the libraries,

read_sverilog -r / read_verilog -r + set_top r:/WORK/<top> for the reference, read_verilog -i + set_top i:/WORK/<top> for the implementation, an SVF from the synthesis run (set_svf) when there is one, then match and verify. The verdict is Verification SUCCEEDED; FAILED and INCONCLUSIVE are not equivalence

• Conformal (lec -xl -nogui -dofile lec.do, through wrap-lec.sh): read library,

read design -golden and read design -revised, set system mode lec, add compare point -all, compare, report verification. Read the compare summary: any Non-equivalent or Abort point is not equivalence

• Yosys (equiv_make / equiv_simple / equiv_induct, or a miter + SAT) for the open

flow

Domain Rules

1. Use same SDC for both golden and revised
2. Scan mode: flatten scan chains or use scan-unaware mode
3. Black boxes: handle consistently in both netlists
4. Unmatched points: must be root-caused — not waived without RTL team approval
5. Post-ECO: run LEC after every ECO, not just at sign-off
6. Negative control before trusting EQUIVALENT. Run the same script once on a deliberately

mutated revised netlist (invert one gate output, swap two inputs of an AND/OR, or tie one flop's D) and require the tool to report it non-equivalent. A setup that cannot catch the mutant — black-boxed modules, a wrong set_top, constant-propagated cones, an SVF that explains the mutation away — proves nothing on the real netlist. Record the mutant and the verdict next to the real result

1. Unmatched or unread design objects (black boxes, unlinked cells, unread .db) are listed

by name; an EQUIVALENT verdict over a black-boxed module covers nothing inside it

Common LEC Failures