Structural search for RTL with predicate learning

We present an efficient search strategy for satisfiability checking on circuits represented at the register-transfer-level (RTL). We use the RTL circuit structure by extending concepts from classic automatic test-pattern generation (ATPG) algorithms and interval-arithmetic to guide the search process. We extend the idea of Boolean recursive learning on predicate logic in the RTL using Boolean and interval constraint propagation in the control and data-path of the circuit. This is used as a pre-processing step to derive relations between predicate logic signals that are used to augment the search. We demonstrate experimentally that these methods provide significant improvement over current techniques on sample benchmarks. Categories and Subject Descriptors: B.5 [Register Tranfer Level Implementation] ? verification, testing General Terms: Algorithms, Verification

• Type: Conference
• Year: 2005
• Where: DAC
• Authors: Ganapathy Parthasarathy, Madhu K. Iyer, Kwang-Ting Cheng, Forrest Brewer
• Keywords: Boolean Recursive Learning, DAC 2005, Design Automation, Predicate Logic Signals, RTL Circuit Structure