Property and Equivalence Checking

Formal Verification Introduction covered the mathematics; this page covers the two genuinely distinct problems formal tools are actually pointed at in a real flow. They share the exhaustive-proof mechanism underneath, but answer completely different questions.

Property checking: proving an assertion, not just running it

SystemVerilog's concurrent assertions already covered writing a property like this:

property req_gets_ack;
  @(posedge clk) req |-> ##[1:3] ack;
endproperty
assert property (req_gets_ack);

In simulation, this assertion only ever gets checked against whatever traces the test suite happens to generate — it can run clean for the entire regression and still be violatable by a sequence nobody happened to simulate. A formal property checking (FPV) tool treats the same property as a proof target instead: it exhaustively searches every reachable state for any legal input sequence that violates it, and returns one of three outcomes, not just pass/fail:

• Proven — no legal trace violates the property, for any reachable state, full stop.
• Falsified — a counterexample exists, and the tool reports the exact trace:

Property: req |-> ##[1:3] ack (once req rises, ack must arrive within 1–3 cycles)

Counterexample trace the formal tool found — no simulation run ever generated this exact sequence:

req rises; ack doesn't arrive until 4 cycles later — one cycle outside the property's ##[1:3] window. Property violated.

• Inconclusive — the tool ran out of time or resources before reaching a bounded or unbounded proof; a real, common outcome on a large enough cone of logic, not a failure of the technique itself.

"Bounded" and "unbounded" name two genuinely different strengths of "proven," worth telling apart: a bounded proof confirms no counterexample exists within some explored depth of cycles (e.g. 50 clock cycles from reset) — real evidence, but not a guarantee that cycle 51 is safe. An unbounded proof (commonly reached via a technique called k-induction) establishes the property holds for every reachable state, no matter how many cycles out — the actual, full "proven" result the bullet above describes. A tool reporting a bounded result honestly should never be read as equivalent to the unbounded case, even though both can look like "no counterexample found yet" from the outside.

A "proven" result can still be meaningless: vacuity

A property can technically report "proven" for a hollow reason — if its trigger condition (req rising, above) is never actually reachable in the design at all, the implication is trivially true simply because its left-hand side never fires. This is called a vacuous proof, and it's a genuine, well-documented gotcha: the property passed, but was never meaningfully exercised even once during the proof. Formal tools run a separate vacuity check specifically to catch this — a "proven" result worth trusting has to also be non-vacuous.

assert, assume, and cover: three different jobs for the same syntax

The property syntax above is written once, but which directive wraps it changes what a formal tool actually does with it — and confusing them is a common, real mistake:

• assert property (...) — the property must always hold; the tool searches for any legal trace that violates it, exactly as described above.
• assume property (...) — not a check at all, but a constraint on the input space: "treat this as a given about how the environment behaves," and only explore traces consistent with it. Critically, this directive behaves completely differently in the two contexts it can appear in: in ordinary simulation, an assume has no effect whatsoever — it's silently ignored; in formal, it's a hard constraint that actively prunes which states the tool is even allowed to consider.
• cover property (...) — the opposite obligation from assert: the property must be true at least once, not always, confirming a scenario is actually reachable rather than forbidding one.

This connects directly to the vacuity gotcha above. An assume that's more restrictive than the real environment can accidentally rule out the exact traces that would have exposed a bug — the formal tool isn't lying when it reports "proven," it has genuinely searched every trace it was allowed to consider, but an overly tight assume shrank that search space until the bug-triggering scenario was never a candidate at all. A non-vacuous "proven" result is only as trustworthy as the assumes that shaped the search behind it.

Equivalence checking: proving two representations compute the same thing

A completely different question: not "does this design satisfy a property," but "do these two designs compute exactly the same function." Two distinct techniques answer it, for two different situations:

• Combinational equivalence checking (CEC) — the most mature formal technique in the EDA industry, and, for RTL-versus-post-synthesis-netlist comparison specifically, considered a hard requirement at most companies doing chip design, not an optional extra check. CEC works when the two designs are state-matched — every flip-flop in the RTL corresponds to a specific flip-flop in the netlist — reducing the problem to proving the combinational logic between corresponding state elements computes identically.
• Sequential equivalence checking (SEC) — needed when the two designs are not state-matched: a retimed pipeline (registers moved across combinational logic to improve timing, changing latency without changing the eventual result), a different number of cycles to produce the same output, or a different internal scheduling of the same computation. Genuinely harder than CEC, since it can't rely on a one-to-one register correspondence to anchor the proof.

The concrete, practical use case that makes this real rather than theoretical: a bug found late — after synthesis, close to tapeout — sometimes gets fixed with a manual, targeted netlist edit (an ECO, engineering change order) rather than a full re-synthesis, because a full re-synthesis risks reopening timing closure work that's already finished. Equivalence checking is what proves that hand-edit didn't accidentally change the design's function anywhere else — a small, manual change verified with the same exhaustive rigor as the original RTL-to-netlist comparison, without re-running the entire simulation regression against the new netlist.

What's next

Formal verification — the mathematics, property proofs, and equivalence checking — is now covered end to end. Section D turns to a set of specialized verification domains a real front-end flow includes beyond ordinary functional simulation and formal proofs of behavior: clock and reset domain crossing, linting, gate-level simulation, power-aware verification, and timing verification.