Formal Verification

1 — Simulation vs Formal: The Core Difference

Every verification engineer learns simulation first — write a testbench, apply stimulus, check outputs. Simulation is fast, highly scalable, and easy to debug. But it has an irreducible blind spot: it only checks the states you happen to reach with the stimuli you happen to write. Corner cases that no test covers remain invisible.

Formal verification attacks this from the opposite direction. Instead of running specific input sequences, a formal tool constructs a mathematical model of all possible state transitions the design can make, then uses SAT solvers, BDD engines, or SMT solvers to exhaustively explore every reachable state and prove whether a given property can be violated.

The table below compares the two methodologies across the dimensions that matter most in practice.

2 — Model Checking vs Theorem Proving

The term "formal verification" covers two fundamentally different techniques. Most RTL engineers encounter model checking because it operates directly on hardware models without requiring manual proofs. Theorem proving is more powerful but requires an expert human prover and is used primarily in processor verification and safety-critical software.

Model Checking

Model checking automatically explores the complete reachable state space of a finite-state machine and checks whether a temporal logic property holds in every state. For RTL, the design is compiled into a transition relation, and a SAT or SMT solver searches for any state sequence that violates the property. If none exists, the property is proven. If one does, the tool returns a concrete counterexample trace.

• Fully automatic — no user-supplied proof steps required
• Works on synthesizable RTL compiled to a Boolean formula
• Returns either a proof or a concrete bug trace
• State explosion limits scale — used on blocks, not full chips
• Algorithms: BDD-based (symbolic), SAT-based (BMC), IC3/PDR (Property Directed Reachability)

Theorem Proving

Theorem proving uses an interactive proof assistant (Coq, Isabelle, HOL4, ACL2) in which a human engineer writes formal proofs that a mathematical specification is equivalent to a model of the design. The tool checks each proof step for logical consistency.

• Handles unbounded state spaces that model checking cannot touch
• Requires significant manual effort and formal methods expertise
• Used by ARM, Intel, and AMD on processor pipelines and microarchitecture
• Not directly tied to RTL — operates on abstract models

3 — SVA assume / assert / cover in Formal Context

SystemVerilog Assertions use the same assume, assert, and cover keywords in both simulation and formal tools — but their roles differ fundamentally in a formal environment.

assert — the property being proven

In formal mode, assert property (P) instructs the solver to prove that P holds in every reachable state. The tool attempts to find any sequence of legal inputs that causes P to be false. If it finds one, it reports a counterexample. If it cannot, it reports PROVEN (bounded or unbounded depending on the algorithm).

assume — constraining the input space

In simulation, assume is used to guide a testbench generator. In formal, assume property (C) is a mathematical constraint that restricts which input sequences the solver is allowed to consider. The solver will only explore traces where C holds. This models the legal environment of a block — for example, assuming an AHB master never asserts HWRITE and HMASTLOCK simultaneously unless the bus is owned.

cover — reachability witnesses

cover property (C) in formal asks the solver to find at least one trace where C is true, starting from reset. It proves that a state is reachable. This is invaluable for verifying that your assume constraints do not accidentally prevent meaningful scenarios.

// -------------------------------------------------------
// Formal property module for an AXI-lite arbiter
// Bind into DUT: bind axi_arbiter axi_arbiter_props u_props(.*);
// -------------------------------------------------------
module axi_arbiter_props (
  input logic        clk, rst_n,
  input logic        req_a, req_b,
  input logic        gnt_a, gnt_b,
  input logic        busy
);

  // Default clocking for all properties in this module
  default clocking cb @(posedge clk); endclocking
  default disable iff (!rst_n);

  // --- ASSUME: model the legal environment ---
  // Grants are only driven by DUT; requester holds req until granted
  assume property (gnt_a |-> req_a);   // can't get grant without req
  assume property (gnt_b |-> req_b);
  // Requesters don't withdraw req mid-transaction
  assume property (req_a && !gnt_a |=> req_a);

  // --- ASSERT: prove correctness properties ---
  // Mutual exclusion: both grants never high simultaneously
  assert property (!(gnt_a && gnt_b))
    else $error("FORMAL FAIL: dual grant");

  // Liveness: if req_a high, grant arrives within 4 cycles
  assert property (req_a |-> ##[1:4] gnt_a)
    else $error("FORMAL FAIL: starvation A");

  // --- COVER: prove interesting states are reachable ---
  cover property (req_a && req_b && !gnt_a && !gnt_b);  // both waiting
  cover property (gnt_a ##1 gnt_b);                     // A then B

endmodule

4 — Bounded Model Checking (BMC)

Bounded Model Checking (BMC) is the most widely used formal algorithm in industry because it is fast, automatic, and excellent at bug hunting. The core idea is to unroll the design's transition relation for a fixed number of clock cycles k and encode the entire unrolled execution as a Boolean satisfiability (SAT) problem.

How BMC works

1. The design RTL is compiled to a Boolean transition relation T(s, i, s') — from state s with input i, the next state is s'.
2. The property assertion is negated: the tool looks for a trace where NOT-P holds.
3. The path is unrolled: Init(s0) ∧ T(s0,i0,s1) ∧ T(s1,i1,s2) ∧ ... ∧ ¬P(sk)
4. A SAT solver is invoked on this formula. A satisfying assignment is a counterexample.
5. If UNSAT, no violation exists within k steps. Increment k and retry.

BMC limitations and when to stop

BMC result "no violation in k steps" is not a proof of correctness — it is only a guarantee up to depth k. Depth k must be large enough to reach the state where a bug could manifest. For a FIFO of depth 16, any overflow bug will be reachable within 16 write cycles. For a complex protocol, the depth may need to be hundreds. If BMC passes at depth k and no guidance exists for k, use k-induction (Section 5) to escalate to an unbounded proof.

5 — k-Induction for Unbounded Proofs

k-induction extends BMC into a complete, unbounded proof. It is the primary algorithm behind IC3/PDR (Property Directed Reachability), the current state-of-the-art for hardware model checking, but the classical formulation is the easiest to reason about.

Base Case — identical to BMC

Prove that the property P holds for all paths of length k starting from the initial state. This is exactly BMC at depth k.

Inductive Step — the key addition

Assume P holds for k consecutive steps starting from some arbitrary state (not necessarily the initial state). Prove that P must also hold at step k+1. If both base case and inductive step pass, P is proven for all time by mathematical induction.

// Conceptual mapping: k-induction in SVA terms
// The tool handles the math; you write the property.

// Property: FIFO never goes above its depth parameter
parameter int DEPTH = 16;
logic [4:0] count; // 0..16

// Assert: count is always <= DEPTH (no overflow)
assert property @(posedge clk) disable iff (!rst_n)
  (count <= DEPTH);

// A helper invariant (strengthening lemma) to help the inductive step:
// count can only change by +1 or -1 per cycle
assert property @(posedge clk) disable iff (!rst_n)
  (count == $past(count) + push - pop);

Why the inductive step sometimes fails

The inductive step starts from an arbitrary state, not a guaranteed reachable state. The solver can construct a starting state that is actually unreachable from reset, but which leads to a property violation at step k+1. The fix is to add strengthening lemmas — auxiliary invariants about valid design states — as additional assert properties that constrain the starting state. This is the main engineering challenge in k-induction-based formal proofs.

6 — Counterexample (CEX) Reading and Interpretation

When a formal tool finds a property violation, it produces a counterexample (CEX) — a concrete sequence of states and input values that drives the design from reset to a state where the assertion fails. Reading a CEX correctly is a critical skill: it is your primary debug artifact in formal verification, equivalent to a failing waveform in simulation.

Structure of a CEX

• Length: Minimum number of cycles to reach the violation from reset
• Initial state: All state elements at cycle 0 (usually after reset deassertion)
• Input sequence: The exact primary input values each cycle that the solver applied
• State trace: All register and signal values at each cycle
• Violation point: The cycle where the asserted property evaluates to false

CEX reading workflow

1. Load the CEX in the waveform viewer (JasperGold opens GTKWave or its own viewer automatically)
2. Locate the assertion failure marker — the cycle where the assert fires
3. Trace backward: which signal drove the bad value? Which state was the machine in?
4. Trace forward from cycle 0: which input sequence enabled reaching that state?
5. Determine: is this a real design bug, or an invalid environment (missing assume constraint)?

CEX replay in simulation

JasperGold can export a CEX as a SystemVerilog testbench or Tcl-driven simulation. Running the CEX through your simulator lets you use all your existing debug infrastructure — waveforms, assertions, UVM report handlers — to understand the bug root cause faster than stepping through the formal GUI alone.

7 — Vacuity Checking

Vacuity is one of the most dangerous silent failures in formal verification. A property is vacuously true when its antecedent (the trigger condition) is never satisfied in any trace the tool considers, so the implication passes trivially — not because the design is correct but because the trigger never fires.

Classic vacuity example

// Intent: whenever req is asserted, ack must follow within 4 cycles
assert property @(posedge clk)
  (req |-> ##[1:4] ack);

// Hidden problem: this assume blocks req from EVER being asserted:
assume property @(posedge clk)
  (!req);  // too restrictive!

// The assert passes (PROVEN) but is 100% meaningless.
// req never fires, so the implication is vacuously satisfied.

How to detect vacuity

• JasperGold: Run check_vacuity after each prove run. The tool checks whether the antecedent of each implication was ever triggered in any valid trace.
• Cover witnesses: For every assert property (A |-> B), add a companion cover property (A). If the cover is UNREACHABLE, the assert is vacuous.
• Mutation: Temporarily negate the consequent — if the property still passes, it was vacuous.

// Best practice: pair every implication assert with a cover
assert property @(posedge clk) (req |-> ##[1:4] ack);

// Cover proves req CAN be asserted under current assumes
cover property  @(posedge clk) (req);

// In JasperGold Tcl:
// prove -property {assert_req_ack}
// check_vacuity -property {assert_req_ack}

8 — Typical Formal Verification Applications

Formal verification is not a replacement for simulation across all domains. It is most powerful for a defined set of high-value applications where exhaustive proof matters and the design scope fits within tool capacity.

Clock Domain Crossing (CDC)

CDC verification checks that every signal crossing a clock domain boundary is properly synchronized. A formal CDC tool builds a model of all possible metastability scenarios and proves that no data corruption can propagate to the receiving clock domain. Tools: Meridian CDC (Real Intent), SpyGlass (Synopsys). Formal CDC catches protocol-level bugs that structural CDC lint cannot — for example, multi-bit bus synchronization without gray encoding.

Datapath Equivalence Checking

After RTL optimization, retiming, or technology mapping, equivalence checking formally proves that two representations compute identical functions for all inputs. This is how synthesis tools are verified — proving the gate-level netlist is equivalent to the RTL. Cadence Conformal and Synopsys Formality are standard tools. No testbench needed; the proof is purely combinational (for combinational equivalence) or sequential.

Reachability Analysis

Proving that a design can never reach a specific "bad" state — a deadlock condition, a forbidden FSM state combination, an illegal address decode — is a direct application of model checking. The bad state is encoded as an assertion, and the tool proves it is unreachable from reset under all legal input sequences.

Protocol Property Verification

AXI, AHB, APB, PCIe, and USB all have formal VIP (Verification IP) available. The VIP provides assume constraints for the initiator side and assert properties for the target side (or vice versa). Running formal against your controller with VIP constraints gives exhaustive proof of protocol compliance — something thousands of simulation tests cannot match.

Safety and Liveness

• Safety: "Bad thing never happens" — mutual exclusion, no overflow, no metastability. Directly encoded as assert.
• Liveness: "Good thing eventually happens" — eventually granted, eventually acknowledged. Harder for model checkers; requires fair trace assumptions. JasperGold supports liveness via justice / compassion constraints.

9 — JasperGold Workflow

Cadence JasperGold is the industry-dominant formal verification platform. It wraps a multi-engine formal backend (SAT, BDD, IC3/PDR, abstract interpretation) behind a property-centric GUI and Tcl scripting interface. The typical project flow is:

1. Design elaboration: Compile the RTL and bind the property module
2. Environment setup: Define primary inputs, clocks, resets, assume constraints
3. Property specification: Load SVA file or inline property module
4. Prove: Run the formal engines on the assert targets
5. Analyze results: PROVEN, BOUNDED, CEX (failing), or VACUOUS
6. Debug: Inspect CEX in waveform viewer, fix RTL or assumes
7. Signoff: Achieve PROVEN status or documented BOUNDED depth for all targets

# -------------------------------------------------------
# JasperGold Tcl script: axi_arbiter_formal.tcl
# -------------------------------------------------------

# 1. Elaborate design
analyze -sv09 {
  src/axi_arbiter.sv
  props/axi_arbiter_props.sv
}
elaborate -top axi_arbiter -bbox_m {sram_macro}

# 2. Clock and reset
clock clk
reset -expression {!rst_n}

# 3. Assume environment constraints (beyond SVA file)
assume -name env_stable_req {req_a || req_b}  # at least one active

# 4. Prove all asserts
prove -all

# 5. Check vacuity on every proven property
check_vacuity -all

# 6. Dump result report
report -results -file jg_results.rpt -force

# 7. Save session for waveform debug
save_session -session axi_arbiter_session

JasperGold result codes

10 — SymbiYosys Open-Source Formal Flow

SymbiYosys (sby) is the open-source formal verification frontend maintained by YosysHQ. It wraps the Yosys synthesis framework and connects to open-source SAT/SMT solvers (Boolector, Yices2, Z3, ABC). It is fully capable of BMC, k-induction, and cover checking on synthesizable Verilog and SystemVerilog (via Verific or sv2v preprocessing).

sby configuration file

# arbiter_proof.sby
[options]
mode bmc       # or prove (k-induction), cover
depth 40       # unroll 40 cycles for BMC

[engines]
smtbmc boolector   # or: smtbmc yices; abc bmc3

[script]
read -formal src/axi_arbiter.sv
read -formal props/axi_arbiter_props.sv
prep -top axi_arbiter

[files]
src/axi_arbiter.sv
props/axi_arbiter_props.sv

# Run BMC then k-induction prove
$ sby -f arbiter_proof.sby

# For unbounded proof (k-induction):
# Change mode to "prove" in .sby file, then:
$ sby -f arbiter_prove.sby

# View counterexample if fail:
$ gtkwave arbiter_proof/engine_0/trace.vcd

Complete SVA property example with assume

// -------------------------------------------------------
// Formal properties for a synchronous FIFO
// Place in fifo_formal.sv, compile alongside fifo.sv
// -------------------------------------------------------
module fifo_formal #(
  parameter int DEPTH = 16,
  parameter int WIDTH = 8
) (
  input logic             clk, rst_n,
  input logic             push, pop,
  input logic [WIDTH-1:0] din,
  output logic[WIDTH-1:0] dout,
  input logic             full, empty,
  input logic [4:0]      count
);

  default clocking cb @(posedge clk); endclocking
  default disable iff (!rst_n);

  // ---- ASSUME: valid environment ----
  // Never push to a full FIFO (bus protocol guarantee)
  assume property (!full || !push);
  // Never pop from an empty FIFO
  assume property (!empty || !pop);

  // ---- ASSERT: correctness properties ----
  // Count never exceeds DEPTH
  assert property (count <= DEPTH)
    else $error("OVERFLOW: count=%0d > DEPTH", count);

  // Count never goes negative
  assert property (count != '1)   // unsigned never wraps below 0
    else $error("UNDERFLOW: count wrapped");

  // Full flag is consistent with count
  assert property (full == (count == DEPTH));
  assert property (empty == (count == 0));

  // After push (no simultaneous pop), count increments by 1
  assert property (push && !pop |=> count == $past(count) + 1);

  // ---- COVER: prove these states are reachable ----
  cover property (full);          // FIFO can fill
  cover property (empty ##1 full); // empty to full in one burst
  cover property (push && pop);   // simultaneous push-pop

endmodule

// Bind into DUT (add to testbench or elaboration script):
// bind sync_fifo fifo_formal #(.DEPTH(16),.WIDTH(8)) fml(.*);

FAQ