v1.0.0 to v1.0.0

---

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.

## 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

---

## 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