Sequential equivalence reduces to combinational checks between matched storage. Each RTL register is paired with its netlist counterpart by name or by hierarchy.
The pairing must be exact before any pass means anything. An unmatched or mispaired register voids the comparison of its cones.
RTL side | Netlist side | Match rule |
|---|---|---|
Primary input | Primary input | Same port name and width. |
Register output | Register output | Same hierarchical name after synthesis. |
Primary output | Primary output | Same port name and width. |
Between two key points sits a combinational cone: all gates that influence the endpoint. The check proves each cone pair equal on every input vector.
A three-input cone needs eight exhaustive vectors. The calc block states the count the proof below covers.
cone inputs: a, b, c (3 inputs)
exhaustive vectors = 2^3 = 8
vectors: 000, 001, 010, 011, 100, 101, 110, 111
the miter proof covers all 8 vectors, not a sampleThe script below synthesizes a small RTL block to generic gates, then builds a miter against the RTL. In Yosys the library cells carry no logic model for the SAT solver, so this lesson proves equivalence before mapping to the teaching library, and mapping is a separate later step.
read_verilog <<EOV
module t(input wire a, b, c, output wire y);
assign y = (a & b) | (~a & c);
endmodule
EOV
hierarchy -top t
proc
opt
design -save pre
synth -top t -flatten
rename t gate
design -stash netlist
design -load pre
rename t gold
design -copy-from netlist -as gate gate
miter -equiv -flatten -make_outputs gold gate m
hierarchy -top m
sat -prove trigger 0 -verify m
log PASS: synthesized netlist equals RTL on all input vectorsNo area number is asserted here. The asserted property is equality on all eight vectors.
No. Sampling can miss the one vector that differs. Only the solver proof over all vectors is equivalence.
Void. The cones were never aligned, so the pass compares the wrong logic.