This paper discusses a formal verification technique for comparing the functionality of a transistor netlist extracted from a layout with a design description in a hardware description language (HDL). Using novel techniques based on binary decision diagrams (BDD's), 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. In particular, the abstracted machine(s) can be represented as BDD relations or as synchronous sequential networks, both of which are common starting points for sequential synthesis and verification tools.
展开▼
