formal-verification · diff
v1.0.0 to v1.0.0
41 added, 4 removed. Audit A to A.
---
name: formal-verification
description: >
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.
version: 1.0.0
author: chuanseng-ng
license: MIT
allowed-tools: Read, Write, Bash
---
# 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
+ 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:
+
+ | 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 |
+
### 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
```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 |
+ | 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 |
### 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
+ 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: fix RTL → re-run FPV (counts as RTL bug, not formal 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
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
+ 6. 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
+ 7. 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
### 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
+ - [ ] All INCONCLUSIVE: documented with justification and recorded as `UNVERIFIED`, not PROVEN
+ - [ ] Every `rtl.unverified[]` entry: proven, covered, or dispositioned with a reason
- [ ] 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_<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.
### 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_<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.
### 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.