Chapter 6. Characteristics of Formal Equivalency Verification

6.1 RTL Combinational Model Equivalency

A critical SoC project checkpoint at multiple phases of the development schedule is to prove functional equivalency between the RTL and gate netlist implementation model throughout the SoC model hierarchy. An RTL logic synthesis flow is expected to remain equivalent through the various stages of logic reduction, factoring, repowering, technology library mapping, and clock/ test insertion algorithms. Yet for gate netlists that are manually captured or, especially, for ECOs applied directly to the netlist, model equivalency between RTL and netlist must be proven. Functional validation testbenches applied to both RTL and netlist is a possible ...

Get VLSI Design Methodology Development, First Edition now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.