Terms are listed alphabetically. Each definition fixes the vocabulary the lessons use; the lesson in the last column teaches the idea. Numbers quoted here belong to the running designs of the course and are teaching values, not figures for any real product or process.
Term | Meaning | Taught in |
|---|---|---|
Abstraction refinement | Proving on a simplified model, then adding back detail only where a spurious failure demands it. | |
Antecedent | The trigger of an implication: the check starts in every cycle it holds, so a level antecedent starts one attempt per cycle. | |
Assertion | A check on an output or internal state: the engine asks whether any behaviour of the model can violate it, and answers proven, counterexample or inconclusive. | |
Assume-guarantee | A sound split of a proof: block A proved under X about its inputs, block B proved to guarantee X, with no circular dependence. | |
Assumption | A constraint on the model's inputs or environment, with an owner, a discharge target and a lifetime, recorded beside every result that uses it. | |
Assumption influence | Which assumptions a proof actually relied on, and how much of the legal behaviour each one removes. | |
Base case | The first induction obligation: the property holds in the first k states reached from reset. | |
BDD | A stored set of states as a decision diagram; its size depends sharply on variable order. | |
Black box | A removed block whose outputs are free: passing proofs stay valid and failures may be spurious until a contract constrains it. | |
BMC (bounded model checking) | The engine that unrolls the transition relation k times and asks whether a violation is reachable within them. | |
Bound justification | The recorded argument that a depth suffices: reset plus trigger plus worst-case latency plus one, a diameter argument, or an inductive proof. | |
Bounded response | A safety property of the form response within N cycles, written with a counter and a stated N. | |
Bounded to N | How a bounded pass is written: no counterexample within N cycles. A sound, stated result, reported under inconclusive until the depth is justified. It is not a proof. | |
Case split | Proving a property once per case of a mode or value, with a separate lemma showing the cases cover everything. | |
COI (cone of influence) | The transitive fan-in a property can depend on. Reducing to it is exact and never over-constrains. | |
Consequent | The response of an implication: what must hold in the same cycle for the overlapped form or the next cycle for the non-overlapped form. | |
Contract | The table of assumptions between blocks with owners and the assertions that discharge each row. | |
Counterexample (CEX) | A concrete trace from reset that breaks a property, read down to the earliest failing cycle. | |
Counterexample to induction (CTI) | A failing induction step that may start in an unreachable state, so it may be spurious. | |
Cover | A directive that asks whether a witness trace is reachable: for an antecedent, for ordinary activity, for a scenario. | |
Cut invariant | The relation between the internal registers of two retimed designs that lets the proof of equal outputs pass. | |
Cut point | A signal replaced by a free value to cut logic, sound only with a contract the neighbour proves. | |
Data independence | The justification for proving data handling once: control never branches on data values. | |
Depth | How many steps a bounded check unrolls. It is derived from reset, trigger and latency, never guessed. | |
Diameter | The largest number of steps needed to reach any reachable state from reset. A bound at or beyond it has seen every reachable state, which is what justifies a bounded result. | |
Disable iff | The clause that switches a property off while reset is active, including its polarity and the first enabled cycle. | |
Engine | The algorithm behind a run: bounded check, induction, IC3, interpolation, each with what it can prove or refute. | |
Fairness (weak, strong) | A constraint on environment choices only. Weak: an action that stays enabled for ever is taken infinitely often. Strong: an action enabled infinitely often is taken infinitely often. | |
Harness | The wrapper around a design for a formal run: parameters, free inputs, one reset sequence, assumptions, assertions and covers. | |
Helper invariant (helper assertion) | An invariant proved beside a property to exclude unreachable states and make the induction step pass. Every helper is itself proved. | |
History register | A register that holds earlier values of a signal so a check can look back N cycles: the runnable replacement for a sequence local variable and for a windowed $past. | |
IC3 (also called PDR) | The engine that builds frames of over-approximated reachable states, blocking counterexamples to induction until a fixed point. | |
Inconclusive | The outcome when a run exhausts time, depth or strength undecided. It is never evidence. | |
Induction step | The second induction obligation: any k consecutive states satisfying the property imply it in the next state. | |
Interpolation | An over-approximation of the image that still excludes bad states, letting some runs decide without a hand-written helper. | |
Invariant | A condition true in every reachable state. A safety property is an invariant. | |
k-induction | Induction over windows of k states: base case plus step, both to the same k. | |
Key point | A compared state element in an equivalence run, found by name, structure or function. Unmapped points need classification. | |
Lasso | An infinite trace shaped as a prefix plus a loop. It is the shape of every liveness violation. | |
Latency alignment | Comparing two implementations only after the defined point where their outputs correspond, with the latency asserted separately. | |
Latency window | The number of cycles within which a change on one side must appear on the other, stated as a bounded response. | |
LEC | Combinational equivalence under one-to-one state correspondence, scan off, and consistent constants and black boxes. | |
Liveness | A property only an infinite trace can refute: something good eventually happens. | |
Miter | Two combinational blocks fed shared inputs with their outputs compared: equivalence as one safety property. | |
Mode condition | The setting under which a connection or behaviour is claimed, so the proof asserts the row only inside its mode. | |
Mutant | A design or property with one injected fault, used to test whether the property set can fail. | |
Mutation | The coverage method that requires some property to fail for every injected fault. | |
Over-approximation | A set of states that contains every reachable state and possibly more. A property proved on it holds on the real design; a failure on it may be spurious. | |
Over-constraint | Assumptions that exclude legal behaviour, making proofs pass and covers stay unreached. Exposed by activity covers, never by assertions. | |
Past ($past) | The sampled value of an expression n cycles ago. Its third argument is a gating expression, never a window. | |
Product machine | Two state machines run side by side on shared inputs, with a comparison of their outputs; equivalence becomes a safety property of the pair. | |
Proof core | What the proof actually used, against the cone of what it could have used. Coverage is the union over proven properties. | |
Proof status ledger (signoff ledger) | One row per property: status, bound with justification, assumptions used, covers, mutants, source hash. | |
Property | A requirement written as a checkable statement with a trigger, a response, a window and a scope. | |
Proven | A run outcome: the property holds for the stated model under the stated assumptions. Only this outcome is a proof. | |
Reachability | Whether a state or a witness can be reached from reset. Safety is unreachability of the bad state. | |
Reset determinism | That the state after the reset sequence does not depend on free initial values, proved with two copies of the design. | |
Restrict | A tool-level constraint that deletes the input behaviours it excludes, like an assumption, but a simulator ignores it instead of checking it. Shown as a concept only. | |
Retiming | Moving registers across logic: states differ while outputs agree, needing sequential equivalence and a cut invariant. | |
Safety | A property a finite bad prefix can refute: something bad never happens. | |
Sampled value | What an assertion sees: signal values sampled at the clock edge, not the values driven after it. | |
SAT | The solver question behind one unrolled step: is there an assignment that violates the property. | |
SAT sweeping | Merging candidate-equivalent nodes in a miter after simulation signatures propose them and the solver confirms them. | |
SEC (sequential equivalence checking) | Equivalence of two state machines from reset on shared inputs, needing a state-correspondence invariant. | |
Simple-path constraint | The uniqueness condition that states along an induction window are pairwise different. | |
SMT | Satisfiability over theories such as bit-vectors and arithmetic, the solver behind datapath-heavy checks. | |
Source hash | The revision stamp tying each result to the exact sources proved. A change reruns the proof. | |
Spurious failure | A counterexample the real design cannot produce: from an unreachable start, a free cut point, or an over-free black box. Replayed against the real design to prove it spurious. | |
Strong and weak operators | How an unbounded obligation treats a finite prefix: a weak obligation never fails while it is still open, on a finite prefix or on a loop; a strong one fails it. Vacuity is a different thing. | |
Structural hashing | Merging identical sub-structures in a miter so the solver sees each one once. | |
Stutter tolerance | A comparison that ignores idle cycles in which both sides hold state, so a finite stretch of no change cannot break it. | |
Symbolic constant | A free value the tool picks once and keeps, held fixed by an equality with its registered copy; it names the tracked slot, tag or shadow data. | |
Task | A named unit of formal work: design, properties, engine choice, depth and time limit. | |
Tautological assertion | An assertion that cannot fail whatever the design does, such as a bound the signal can never exceed. A mutant it cannot catch exposes it. | |
Time limit | The effort budget of a run. Expiry reports inconclusive, never a pass. | |
Tracked item | One entry followed through a queue by a symbolic slot and shadow value, standing for all data. | |
Two-state model | The default formal model with no unknown value, in which an unknown-check proves nothing. | |
Unreachable state | A state that no input sequence from reset can reach. An induction step may start there, which is how a spurious counterexample arises. | |
Vacuity | A pass whose trigger never fires. It is exposed by an antecedent cover, not by the assertion. | |
Waiver | A recorded acceptance of an inconclusive property with evidence, an owner and an expiry. | |
Witness | A trace reaching a cover: proof that a trigger, activity or scenario can happen. | |
X propagation | Unknown values spreading from unreset or unpowered sources, answered by reset-determinism proofs and dedicated analysis. |
Pair | The difference |
|---|---|
Proven, bounded to N and inconclusive | Proven: decided true for the stated model and assumptions. Inconclusive: undecided for lack of time, depth or strength. Bounded to N is the form an inconclusive bounded pass takes: no counterexample within N, undecided beyond. Only proven is a proof. |
Counterexample and counterexample to induction | A counterexample starts at reset and breaks the property: a real bug unless the model is wrong. A CTI starts anywhere and breaks only the induction step: maybe spurious, answered by a stronger invariant. |
Safety and liveness | Safety is refuted by a finite bad prefix. Liveness needs an infinite trace, drawn as a lasso. Within N cycles is safety, eventually is liveness. |
Assumption and assertion | An assumption constrains inputs and belongs to the environment side. An assertion asks about outputs and belongs to the block that owes the behaviour. |
Cone and proof core | The cone is what the property could depend on. The proof core is what the proof used. Coverage needs both, plus the depth behind them. |
Vacuity and a weak obligation | Vacuity: the trigger never fires, so the property never really checks. A weak unbounded obligation: it cannot fail while it is still open, finite or looping, by its semantics. Different causes, different fixes. |
Fairness on the environment and on the design | Fairness may constrain environment choices such as stalls. Put it on a design output and the proof is true by assumption. |
LEC and SEC | LEC compares combinational blocks under one-to-one state correspondence. SEC compares state machines whose states differ, with an invariant relating them. |
Deadlock, livelock and starvation | Deadlock: no progress is possible, a cycle of waits. Livelock: activity without completion. Starvation: one requester never served while others are. |
Mutation and vacuity | Mutation asks whether the property can fail when the design is broken. Vacuity asks whether it ever really checked. A property needs both answers. |
A counterexample to induction. Strengthen with a helper invariant that excludes the unreachable region, prove the helper, and rerun the step.