Formal Verification That Ships Silicon: A Practitioner’s Playbook

Executive Summary

As SoCs scale in complexity and safety expectations rise, formal verification (FV) moves from “nice to have” to sign-off critical. This playbook shows exactly how we run formal—from property planning to proof closure, fault injection, and audit-ready reporting—so you can ship first-time-right silicon.

Who Should Read

ASIC/SoC Leads, DV Engineers, Safety Managers (ISO 26262), and CTOs prioritizing tapeout confidence.

Table of Contents

1. Scope: What Formal Is (and Isn’t)

2. Property Taxonomy That Works

3. Model Prep: Assumptions, Constraints, and Abstractions

4. Engines & Proof Strategies (BMC, Induction, IC3/PDR)

5. Safety & Security with Formal (FuSa, X-prop, Info-flow)

6. Fault Campaigns & Diagnostic Coverage

7. Closure Metrics, Sign-off, and Evidence

8. Code Snippets: SVA Patterns That Scale

1) Scope: What Formal Is (and Isn’t)

• Is: Exhaustive state-space exploration under constraints; ideal for corner cases, safety (never), liveness (eventually), connectivity, and micro-protocols.

• Isn’t: A full replacement for simulation; it complements UVM/GLS and reduces late surprises.

2) Property Taxonomy That Works

• Safety (invariants): “bad never happens.”

• Liveness (progress): “good eventually happens.”

• Connectivity/Equivalence: Net-to-net connectivity, RTL vs. ECO equivalence.

• Protocol/Timing Windows: Handshakes, FIFOs, arbiter fairness.

• X-Cleanliness/Reset Integrity.

Example — FIFO Safety/Liveness

// Safety: Read shall not occur when FIFO empty property p_no_read_on_empty; @(posedge clk) disable iff (!rst_n) (fifo_rd && fifo_empty) |-> $error("Read on empty"); endproperty assert property (p_no_read_on_empty); // Liveness: Every write eventually becomes readable property p_eventual_read; @(posedge clk) disable iff (!rst_n) fifo_wr |-> ##[1:$] fifo_rd; endproperty cover property (p_eventual_read);

3) Model Prep: Assumptions, Constraints, and Abstractions

• Assumptions shape legal environments (AXI/APB/ACE/TileLink).

• Abstraction (gray-box, scoreboards, memories) to keep state space tractable.

• Assume-Guarantee: split proofs per sub-block with contracts.

Reset/X Rules: Always add global reset stabilization and X-init guards. Constrain clocks/resets to realistic behaviors.

4) Engines & Proof Strategies

• BMC for shallow bugs and counterexamples.

• k-Induction for unbounded proofs of invariants.

• IC3/PDR for scalable safety properties.

• Cutpoints & Invariants to help convergence.

• Cone-of-Influence trimming + black-boxing of irrelevant datapaths.

5) Safety & Security with Formal

• FuSa: prove safety mechanisms (ECC, lockstep, watchdog) always react correctly; ensure fail-safe transitions.

• Information flow/security: assert isolation between secure/non-secure domains; non-interference on paths.

ECC Example (single-bit correction, double-bit detect)

property p_sbe_corrected; @(posedge clk) disable iff (!rst_n) (rd_valid && inject_single_bit_err) |-> (ecc_sbe && data_out == data_in); endproperty assert property (p_sbe_corrected); property p_dbe_detected; @(posedge clk) disable iff (!rst_n) (rd_valid && inject_double_bit_err) |-> (ecc_dbe && fault_irq); endproperty assert property (p_dbe_detected);

6) Fault Campaigns & Diagnostic Coverage

• Enumerate stuck-at, SEU/SET, and latent faults on safety-critical nets.

• Drive formal fault injection to measure detection times and diagnostic coverage against ASIL targets (SPFM/LFM).

• Export machine-readable results (CSV/JSON) into safety metrics dashboards.

7) Closure Metrics, Sign-off, and Evidence

• Proof status: Proven / Bounded / Falsified / Inconclusive (with rationale).

• Cover closure: Evidence of reachability for critical flows.

• Assumption review: Peer-review assumptions to avoid over-constraint.

• Audit bundle: Property specs, proof logs, fault coverage, and traceability to requirements (AS/RS IDs).

8) Reusable SVA Patterns

• Handshake (req→ack), FIFO bounds, counter ranges, state exclusivity, interrupt de-glitch, CSR access ordering—package these in a property library reused across IPs.

Call to Action:
Want an audit-ready formal sign-off? We’ll blueprint your property plan in one week and wire it into CI, so every RTL change is formally guarded.