# Formal Verification > Formal property verification (FPV) and logical equivalence checking (LEC). Use when proving design properties exhaustively, checking RTL vs gate-level netlist equivalence, verifying CDC crossings formally, or closing verification coverage gaps that simulation cannot efficiently reach. - Skill: `hdl-tools/formal-verification` (Agent Skill) - Install (CLI): `npx skillmds@latest add hdl-tools/formal-verification` - Raw SKILL.md: https://api.skillmd.com/api/skills/hdl-tools/formal-verification/raw - Safety review: pending - Works with: Claude Code, Claude.ai, OpenAI Codex - Category: Coding & Dev Tools - License: MIT - Author: hdl-tools (https://skillmd.com/u/hdl-tools) - Updated: 2026-09-22 - Page: https://skillmd.com/skills/hdl-tools/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`) — industry-standard FPV, CDC, DFT formal - **Synopsys VC Formal** (`vcf`) — property checking and equivalence verification - **Siemens Questa Formal** (`qformal`) — 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 ### QoR Metrics to Evaluate - All spec features mapped to property or cover - 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 ```systemverilog // 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 | Result | Meaning | Action | |--------|---------|--------| | PROVEN | Holds for all reachable states | Log and continue | | CEX | Counterexample found | Analyse; fix RTL or assumption | | VACUOUS | Antecedent never fires | Fix assumption or property | | INCONCLUSIVE | Bound too small or state space too large | Increase bound / abstract | | UNREACHABLE | Cover never reachable | Verify or waive | ### 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. Document as "assumed correct" with justification if intractable ### 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: fix RTL → re-run FPV (counts as RTL bug, not formal bug) 3. Assumption bug: tighten assumption → re-run vacuity check 4. False CEX from under-constraining: document clearly before adding assumption 5. Never waive a CEX without root cause ### 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 ### 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 ### Common LEC Failures | Failure | Fix | |---------|-----| | Optimizer removed logic | Verify with report_removal; add set_dont_touch if needed | | SDC mismatch | Ensure same clock groupings in both netlists | | Scan chain reordering | Use scan-unaware LEC mode | | Black box mismatch | Align black box list in both netlists | ### QoR Metrics to Evaluate - All compare points: EQUIVALENT - 0 UNMATCHED points - 0 ABORTED points ### Output Required - LEC run report - Unmatched point analysis (if any) - EQUIVALENT sign-off record --- ## Stage: formal_signoff ### Sign-off Checklist - [ ] All P0 properties: PROVEN - [ ] No unanalysed CEX - [ ] No vacuous proofs - [ ] LEC: 100% EQUIVALENT - [ ] All INCONCLUSIVE: documented with justification - [ ] Additional coverage closed vs simulation baseline ### Output Required - Formal sign-off report - Final property status table - LEC clean record --- ## Constraint Validation See `plugins/meta/skills/pipeline-orchestration/SKILL.md` §Constraints Schema for the authoritative schema and stage-entry validation rule. **No required keys** for formal verification — all constraints in this domain are optional. There are no numeric coverage thresholds unique to formal; this domain shares coverage targets with the functional-verification domain (`coverage.*`) and timing targets with the STA domain (`timing.wns_ns_target`). When evaluating LEC equivalence or FPV property results, tag `constraint_ref` in history entries with the relevant dot-path key if a constraint value was consulted (e.g. `"coverage.functional_pct"` when reporting coverage contribution). --- ## Memory ### Write on stage completion After each stage completes (regardless of whether an orchestrator session is active), write or overwrite one JSON record in `memory/formal/experiences.jsonl` keyed by `run_id`. This ensures data is persisted even if the flow is interrupted or called without full orchestrator context. Use `run_id` = `formal__` (set once at flow start; reuse on each stage update). Every JSON record written must include a top-level `"run_id"` field whose value matches this key — stage writes must upsert/overwrite by matching this persisted `run_id`. Set `signoff_achieved: false` until the final sign-off stage completes. ### Run state (write before first stage, update after each stage) Write `memory/formal/run_state.md` as the **first action** before launching any tool: ```markdown run_id: formal__ design_name: tool: start_time: last_stage: null current_stage: ``` Update `current_stage` when a stage starts, and set `last_stage` to the completed stage name only after successful completion (then clear `current_stage`). This file lets wakeup-loop prompts and resumed sessions identify the correct run and distinguish completed vs in-flight work. Create the file and parent directories if they do not exist. ### Optional: claude-mem index If `mcp__plugin_ecc_memory__add_observations` is available in this session, emit each applied fix as an observation to entity `chip-design-formal-fixes` after writing to `experiences.jsonl`. Skip silently if the tool is absent — JSONL is the canonical record.