Lesson 8.3 · Formal Equivalence Verification

RTL-to-netlist and netlist-to-netlist

Every transformation between RTL and the final layout can introduce bugs: synthesis tool errors, manual engineering change orders (ECOs), scan insertion, timing fixes. FEV is run after each step.

FEV between each consecutive pair of models keeps the final netlist provably equal to the RTL.

Constraints you will meet

Scan / test mode: after scan insertion the netlist has extra muxes. Constrain scan_enable = 0 (functional mode) to compare against RTL that has no scan.
Clock gating: inserted clock gates change how flops are enabled; tools understand standard gating cells, but may need hints.
Black boxes: memories, analog blocks and hard macros are black-boxed in both models. Their outputs become free inputs and their inputs become compare points.