Subscribe

Issue No.07 - July (2010 vol.59)

pp: 981-994

Andreas Veneris , University of Toronto, Toronto

Hratch Mangassarian , University of Toronto, Toronto

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2010.74

ABSTRACT

Formal CAD tools operate on mathematical models describing the sequential behavior of a VLSI design. With the growing size and state-space of modern digital hardware designs, the conciseness of this mathematical model is of paramount importance in extending the scalability of those tools, provided that the compression does not come at the cost of reduced performance. Quantified Boolean Formula satisfiability (QBF) is a powerful generalization of Boolean satisfiability (SAT). It also belongs to the same complexity class as many CAD problems dealing with sequential circuits, which makes it a natural candidate for encoding such problems. This work proposes a succinct QBF encoding for modeling sequential circuit behavior. The encoding is parametrized and further compression is achieved using time-frame windowing. Comprehensive hardware constructions are used to illustrate the proposed encodings. Three notable CAD problems, namely bounded model checking, design debugging and sequential test pattern generation, are encoded as QBF instances to demonstrate the robustness and practicality of the proposed approach. Extensive experiments on OpenCore circuits show memory reductions in the order of 90 percent and demonstrate competitive runtimes compared to state-of-the-art SAT techniques. Furthermore, the number of solved instances is increased by 16 percent. Admittedly, this work encourages further research in the use of QBF in CAD for VLSI.

INDEX TERMS

SAT, QBF, BMC, k-induction, design debugging, sequential ATPG.

CITATION

Andreas Veneris, Hratch Mangassarian, "Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test",

*IEEE Transactions on Computers*, vol.59, no. 7, pp. 981-994, July 2010, doi:10.1109/TC.2010.74REFERENCES

- [1] T. Sasao,
Logic Synthesis and Optimization. Kluwer Academic Publisher, 1993.- [2] C. Sechen,
VLSI Placement and Global Routing Using Simulated Annealing. Kluwer Academic Publisher, 1988.- [3] R. Drechsler,
Formal Verification of Circuits. Kluwer Academic Publisher, 2000.- [4] M. Abramovici, M. Breuer, and A. Friedman,
Digital Systems Testing and Testable Design. Computer Science Press, 1990.- [5] A. Sistla and E. Clarke, "The Complexity of Propositional Linear Temporal Logics,"
J. ACM, vol. 32, no. 3, pp. 733-749, 1985.- [6] J. Jiang and R. Brayton, "Retiming and Resynthesis: A Complexity Perspective,"
IEEE Trans. Computer-Aided Design (CAD), vol. 25, no. 12, pp. 2674-2686, Dec. 2006.- [7] J. Baumgartner, H. Mony, V. Paruthi, R. Kanzelman, and G. Janssen, "Scalable Sequential Equivalence Checking across Arbitrary Design Transformations,"
Proc. Int'l Conf. Computer Design, 2006.- [8] A. Freitas, H. Neto, and A. Oliveira, "On the Complexity of Power Estimation Problems,"
Proc. Int'l Workshop Logic and Synthesis, pp. 239-244, 2000.- [9]
Int'l Technology Roadmap for Semiconductors, 2007.- [10] M. Ganai and A. Gupta,
SAT-Based Scalable Formal Verification Solutions. Springer-Verlag, 2007.- [11] E. Clarke, O. Grumberg, and D. Peled,
Model Checking. The MIT Press, 2000.- [12] R. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation,"
IEEE Trans. Computers, vol. 35, no. 8, pp. 667-691, Aug. 1986.- [13] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, "Symbolic Model Checking without BDDs,"
Proc. Tools and Algorithms for the Construction and Analysis of Systems, pp. 193-207, 1999.- [14] J. Marques-Silva and K. Sakallah, "GRASP: A Search Algorithm for Propositional Satisfiability,"
IEEE Trans. Computers, vol. 48, no. 5, pp. 506-521, May 1999.- [15] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engineering an Efficient SAT Solver,"
Proc. Design Automation Conf., pp. 530-535, 2001.- [16] N. Eén and N. Sörensson, "An Extensible SAT-Solver,"
Proc. Int'l Conf. Theory and Applications of Satisfiability Testing, pp. 502-518, 2003.- [17] A. Mishchenko, M. Case, R. Brayton, and S. Jang, "Scalable and Scalably-Verifiable Sequential Synthesis,"
Proc. Int'l Workshop Logic and Synthesis, 2008.- [18] A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu, "Bounded Model Checking," Advances in Computers, no. 60, 2003.
- [19] N. Amla, X. Du, A. Kuehlmann, R. Kurshan, and K. McMillan, "An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment,"
Proc. Conf. Historical Analysis and Research in Marketing (CHARME), pp. 254-268, 2005.- [20] H. Konuk and T. Larrabee, "Explorations of Sequential ATPG Using Boolean Satisfiability,"
Proc. IEEE VLSI Test Symp., pp. 85-90, 1993.- [21] A. Smith, A. Veneris, M. Ali, and A. Viglas, "Fault Diagnosis and Logic Debugging Using Boolean Satisfiability,"
IEEE Trans. Computer-Aided Design, vol. 24, no. 10, pp. 1606-1621, Oct. 2005.- [22] F. Lu and S. Malik, "Conflict Driven Learning in a Quantified Boolean Satisfiability Solver,"
Proc. Int'l Conf. Computer-Aided Design (CAD), pp. 442-449, 2002.- [23] A. Biere, "Resolve and Expand,"
Proc. Int'l Conf. Theory and Applications of Satisfiability Testing, pp. 238-246, 2004.- [24] M. Benedetti, "sKizzo: A Suite to Evaluate and Certify QBFs,"
Proc. Int'l Conf. Automated Deduction, pp. 369-376, 2005.- [25] H. Samulowitz and F. Bacchus, "Using SAT in QBF,"
Proc. Int'l Conf. Principles and Practive of Constraint Programming, pp. 578-592, 2005.- [26] N. Dershowitz, Z. Hanna, and J. Katz, "Bounded Model Checking with QBF,"
Proc. Int'l Conf. Theory and Applications of Satisfiability Testing, pp. 408-414, 2005.- [27] T. Jussila and A. Biere, "Compressing BMC Encodings with QBF,"
Proc. Int'l Workshop Bounded Model Checking, pp. 1-14, 2006.- [28] H. Mangassarian, A. Veneris, S. Safarpour, M. Benedetti, and D. Smith, "A Performance-Driven QBF-Based Iterative Logic Array Representation with Applications to Verification, Debug and Test,"
Proc. Int'l Conf. CAD, pp. 240-245, 2007.- [29] G. Tseitin, "On the Complexity of Derivations in the Propositional Calculus,"
Proc. Studies in Constructive Math. and Math. Logic, pp. 115-125, 1968.- [30] M. Davis, G. Logemann, and D. Loveland, "A Machine Program for Theorem Proving,"
Comm. ACM, vol. 5, pp. 394-397, 1962.- [31] M. Sheeran, S. Singh, and G. Stålmarck, "Checking Safety Properties Using Induction and a SAT-Solver,"
Proc. Formal Methods in Computer-Aided Design, pp. 127-144, 2000.- [32] M. Ali, S. Safarpour, A. Veneris, M. Abadir, and R. Drechsler, "Post-Verification Debugging of Hierarchical Designs,"
Proc. Int'l Conf. CAD, pp. 871-876, 2005.- [33] OpenCores.org, http:/www.opencores.org, 2006.
- [34] C. Sinz and E. Dieringer, "DPvis-A Tool to Visualize Structured SAT Instances,"
Proc. Int'l Conf. Theory and Applications of Satisfiability Testing, 2005. |