Title :
Improved SAT-based bounded reachability analysis
Author :
Ganai, Malay K. ; Aziz, Adnan
Author_Institution :
C&C Res. Labs., NEC, Princeton, NJ, USA
Abstract :
Symbolic simulation is widely used in logic verification. Previous approaches based on BDDs suffer from space outs, while SAT-based approaches have been found fairly robust. We propose a SAT-based symbolic simulation algorithm using a noncanonical two-input AND/INVERTER graph representation and on-the-fly reduction algorithm on such a graph representation. Unlike previous approaches where circuit is explicitly unrolled, we propagate the symbolic values represented using the simplified AND/INVERTER graph across the time frames. This simplification have significant impact on the performance of SAT-solver. Experimental results on large examples show the effectiveness of the proposed technique over previous approaches. Specifically we were able to find real bugs in pieces of the designs from IBM Gigahertz Processor Project which were previously remained undetected. Moreover, previous heuristics used in BDD-based symbolic simulation can still be applied to this algorithm
Keywords :
formal verification; logic simulation; reachability analysis; symbol manipulation; SAT; bounded reachability analysis; logic verification; noncanonical two-input AND/INVERTER graph representation; on-the-fly reduction algorithm; symbolic simulation; Reachability analysis;
Conference_Titel :
Design Automation Conference, 2002. Proceedings of ASP-DAC 2002. 7th Asia and South Pacific and the 15th International Conference on VLSI Design. Proceedings.
Conference_Location :
Bangalore
Print_ISBN :
0-7695-1441-3
DOI :
10.1109/ASPDAC.2002.995020