Comparing layouts with HDL models: a formal verification technique

The authors discuss a formal verification technique using binary decision diagrams (BDDs) for comparing the functionality of a transistor netlist extracted from a layout with a design description in a hardware description language (HDL). A state machine is first abstracted from a transistor netlist, given information relating to clock signals and clock models. The resulting state machine behavior is then compared with another that is derived from the HDL description. The basic ingredients of the technique used can be directly applied (or, in other cases, extended) to various related contexts of interest