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.
2. 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

Stage: property_planning

Property Categories

1. Safety: "something bad never happens" assert property (@(posedge clk) !(error && valid));
2. Liveness: "something good eventually happens" (always bound the interval) assert property (@(posedge clk) req |-> ##[1:MAX] ack);
3. Stability: "output is stable while condition holds" assert property (@(posedge clk) valid |-> $stable(data));
4. 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"
7. 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