formal-verificationFormal 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.
Independent GitHub snapshot · Automated classification · Original documentation governs
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.
Before executing or advising on any stage, read the following files if they exist:
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.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.
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, dialect cadence) — industry-standard FPV, CDC, DFT formalvcf, dialect synopsys) — property checking and equivalence verificationqformal, dialect siemens) — 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 gatingdesign_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"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 environmentA clean lint run says nothing about these. Each applies wherever the structure exists:
| Structure | Properties |
|---|---|
| Ready/valid interface | Transfer only on valid && ready; valid not retracted before acceptance; payload stable while valid && !ready; valid and ready low in reset |
| FSM | Every state reachable (cover); every state has an exit (bounded liveness); from any illegal encoding the machine reaches a legal state — mandatory for an FSM using unique case without default, where this assertion is the only recovery check |
| Arbiter | Grant is one-hot or zero; a continuously asserting requester is granted within N grants; rotation advances only on a consumed grant |
| FIFO | No write when full, no read when empty; empty is 1 and full is 0 out of reset; occupancy never exceeds depth |
| Arithmetic | Every +, -, * and accumulator stays within its result width, or wraps only where the spec says so |
| Reset | Every control flop has its specified value in the first cycle out of reset |
| Deadlock | No wait-for cycle: bounded liveness on every request/acknowledge and every credit return |
rtl.unverified[] entry mapped to a property, a cover, or a stated reason// 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 in cex_analysis; hand an RTL bug to the RTL flow, or fix the 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 |
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-offfix_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 bugsuspected_rtl.basis to traced when the CEX trace shows
the faulty signal and cycle, hypothesis when the location is inferred| 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 |
UNVERIFIED, not PROVENrtl.unverified[] entry: proven, covered, or dispositioned with a reasonSee 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).
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.
Write memory/formal/run_state.md as the first action before launching any tool:
run_id: formal_<YYYYMMDD>_<HHMMSS>
design_name: <design>
tool: <primary tool>
start_time: <ISO-8601>
last_stage: null
current_stage: <first stage name>
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.
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.