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.
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.
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.
sby) — formal property verification front-end for open-source solversyosys) — synthesis and equivalence checking back-endjg) — industry-standard FPV, CDC, DFT formalvcf) — property checking and equivalence verificationqformal) — FPV and coverage closureassert property (@(posedge clk) !(error && valid));assert property (@(posedge clk) req |-> ##[1:MAX] ack);assert property (@(posedge clk) valid |-> $stable(data));cover property (@(posedge clk) state == DONE);$past(), $rose(), $fell() over manual delay logicdisable iff: use for reset gating// 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));
| 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 |
| 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 |
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_<YYYYMMDD>_<HHMMSS> (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.