Equivalence Checking · synthesis

Part 7 · Verification, ECO and Handoff · Intermediate

5topics
5lessons

Formal equivalence checking proves the synthesized netlist behaves the same as the RTL. It matches registers and black boxes, then compares the combinational logic between them.

Term	Meaning
Miter	A circuit that instantiates both designs and flags any input where their outputs differ.
Key point	A matched comparison point: a primary output, a register output, or a black-box boundary.
Counterexample	One input vector on which the two designs disagree, with the differing output named.
Black box	A block excluded from comparison and treated as an ideal boundary with fixed ports.

Miter joining RTL and netlist with a single verdict.

The miter joins RTL and netlist; the solver returns equality or one distinguishing vector.

Lesson	What it covers
Combinational equivalence	Matched registers, cones between key points, and a miter proof on a small design.
Key points and black boxes	Primary outputs, flop boundaries and black boxes as the comparison points.
Retiming and recoding	Moved registers and recoded states, and why the correspondence must be rebuilt.
Reading a failure	Counterexamples, localisation, and a mutated netlist proven different.
Constants and brute force	Tied inputs, unreachable cases, and exhaustive brute force on three inputs.

Check yourself The miter reports equal on every key point. What does that prove, and what does it leave open?

It proves the netlist matches the RTL at those points on all inputs. It leaves open anything excluded as a black box and any intent the RTL itself got wrong.

Up nextCombinational Equivalence of RTL and Netlist

Practice this lesson Report an error

Term

Meaning

Miter

A circuit that instantiates both designs and flags any input where their outputs differ.

Key point

A matched comparison point: a primary output, a register output, or a black-box boundary.

Counterexample

One input vector on which the two designs disagree, with the differing output named.

Black box

A block excluded from comparison and treated as an ideal boundary with fixed ports.

Lesson

What it covers

Combinational equivalence

Matched registers, cones between key points, and a miter proof on a small design.

Key points and black boxes

Primary outputs, flop boundaries and black boxes as the comparison points.

Retiming and recoding

Moved registers and recoded states, and why the correspondence must be rebuilt.

Reading a failure

Counterexamples, localisation, and a mutated netlist proven different.

Constants and brute force

Tied inputs, unreachable cases, and exhaustive brute force on three inputs.