Combinational Verification based on High-Level Functional Specifications

We present a new combinational verification technique where the functional specification of a circuit under verification is utilized to simplify the verification task. The main idea is to assign to each primary input a general function, called a coordinate function, instead of a single variable function as in most BDD-based techniques. BDDs of intermediate nodes are then constructed based on these coordinate functionsin a topological order from primary inputs to primary outputs. Coordinate functions depend on primary input variables and extra variables. Therefore combinational verification is performed not over the set of primary input variables but over the extended set of variables. Coordinate functionsare chosen in such a way that inthe process of computing intermediate functionsthe dependency on the primary input variables is gradually replaced with that on the extra variables, thereby making boolean functions associated with primary outputs simple functions only in terms of the e...

• Type: Conference
• Year: 1998
• Where: DATE
• Authors: Evguenii I. Goldberg, Yuji Kukimoto, Robert K. Brayton
• Keywords: Coordinate Functions, DATE 1998, Hardware, Primary Input, Primary Input Variables