Glossary

Short, plain-English definitions of the terms used across the course.

Abstraction

Replacing part of a design with a simpler model that keeps the behaviour a property needs, e.g. a free signal instead of a large counter.

Antecedent

The left-hand side of an implication (A in A |-> B). If it does not match, the implication passes vacuously.

Assertion

A property the design must satisfy. Formal tools try to find a trace that violates it.

Assume-guarantee

Decomposition technique where each block's assumptions are proven as assertions on the block that drives those signals.

Assumption

A property the tool treats as always true about the environment (usually inputs). It restricts the behaviours explored.

BDD

Binary decision diagram: a canonical graph representation of a Boolean function for a fixed variable order.

Black box

A module whose contents are removed for a formal run; its outputs become free inputs.

BMC

Bounded model checking: unroll the design k cycles and use SAT to search for a violation within k cycles of reset.

Bounded proof

A guarantee that no violation exists within N cycles of reset. Not a full proof.

CDCL

Conflict-driven clause learning: the algorithm family behind modern SAT solvers.

Cone of influence (COI)

All logic that can affect the signals in a property. Logic outside it is removed before proving.

Consequent

The right-hand side of an implication (B in A |-> B).

Counterexample (CEX)

A concrete trace from reset that violates an assertion.

Cover

A property the tool tries to reach. A reachable cover comes with a trace; an unreachable one may indicate over-constraint.

Cut point

An internal signal disconnected from its driver and treated as a free input (an over-approximation).

Deferred assertion

An immediate assertion (assert final / assert #0) evaluated only after values settle in a time step.

Design exploration

Using formal (mostly covers) to understand and sanity-check new RTL before a testbench exists.

disable iff

SVA clause that abandons property evaluation while its condition (typically reset) is true.

Equivalence checking (FEV)

Proving that two models of a design produce the same outputs, e.g. RTL and netlist.

False negative

A reported failure that is not a real design bug (wrong property or missing assumption).

False positive

A reported pass that hides a real bug or checks nothing (e.g. over-constraint, vacuity, wrong reset).

Fixed point

The point in reachability analysis where no new states are found; the reachable set is complete.

FPV

Formal property verification: proving SVA properties on RTL with a model checker.

Free input

An input the tool may drive with any value on any cycle, subject only to assumptions.

Helper assertion

An extra (proven) invariant that strengthens induction and speeds up harder proofs.

Immediate assertion

A procedural check of a Boolean condition at the moment it executes.

Implication

SVA operators |-> (same tick) and |=> (next tick) linking an antecedent to a consequent.

Inconclusive

The tool neither proved nor disproved a property within its resource limits.

Induction (k-induction)

Proof method: base case from reset plus an inductive step from any state satisfying the property for k cycles.

Invariant

A property that holds in every reachable state.

Key point

In FEV, a point used for mapping and comparison: inputs, outputs, flops, black-box pins.

Liveness

A property stating something good eventually happens. Violations are infinite traces, shown as loops.

Local variable (SVA)

A variable declared in a property or sequence that captures a value for later comparison.

Miter

A circuit that feeds two designs the same inputs and compares their outputs, turning equivalence into a single check.

Model checking

Automatic verification of temporal properties on a finite-state model by exploring its state space.

Mutation

A deliberate small change (bug) in RTL used to test whether the property set detects it.

Over-approximation

A model with more behaviours than the real design. Safety proofs on it carry over; failures may be spurious.

Over-constraint

Assumptions that exclude legal behaviour, possibly hiding bugs.

PDR / IC3

Property-directed reachability: a SAT-based unbounded proof engine that learns inductive invariants.

Proof-core coverage

The part of the design the engines actually needed to prove a set of properties.

Reachable state

A state that can occur after reset under some legal input sequence.

Safety

A property stating something bad never happens. Every violation has a finite counterexample.

Sampled value

The value a signal had just before the clock edge (Preponed region); used by concurrent assertions.

SAT

Boolean satisfiability: finding an assignment that makes a formula true. The workhorse of modern formal engines.

Sequence

An SVA pattern of Boolean expressions over clock ticks, built with delays (##) and repetitions ([*], [->], [=]).

Sequential equivalence

Equivalence of two designs' output sequences from reset, even when their state elements differ.

Signoff

The decision that verification of a block is complete according to agreed criteria.

State-space explosion

The exponential growth of possible states with the number of state bits.

SVA

SystemVerilog Assertions: the assertion language defined in IEEE 1800.

Tracked item

Technique where the tool picks one arbitrary data item to follow, proving a data property for all items.

Under-approximation

A model with fewer behaviours than the real design (e.g. extra assumptions). Can hide bugs.

Unreachable coverage elimination (UCE)

Using formal to prove simulation coverage items unreachable so they can be excluded.

Vacuity

An implication passing only because its antecedent never matches.

X-propagation

The spread of unknown (X) values through logic; formal X-prop apps check X cannot reach important outputs.