
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Hratch Mangassarian, Andreas Veneris, Marco Benedetti, "Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test," IEEE Transactions on Computers, vol. 59, no. 7, pp. 981994, July, 2010.  
BibTex  x  
@article{ 10.1109/TC.2010.74, author = {Hratch Mangassarian and Andreas Veneris and Marco Benedetti}, title = {Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test}, journal ={IEEE Transactions on Computers}, volume = {59}, number = {7}, issn = {00189340}, year = {2010}, pages = {981994}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2010.74}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test IS  7 SN  00189340 SP981 EP994 EPD  981994 A1  Hratch Mangassarian, A1  Andreas Veneris, A1  Marco Benedetti, PY  2010 KW  SAT KW  QBF KW  BMC KW  kinduction KW  design debugging KW  sequential ATPG. VL  59 JA  IEEE Transactions on Computers ER   
[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. 733749, 1985.
[6] J. Jiang and R. Brayton, "Retiming and Resynthesis: A Complexity Perspective," IEEE Trans. ComputerAided Design (CAD), vol. 25, no. 12, pp. 26742686, 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. 239244, 2000.
[9] Int'l Technology Roadmap for Semiconductors, 2007.
[10] M. Ganai and A. Gupta, SATBased Scalable Formal Verification Solutions. SpringerVerlag, 2007.
[11] E. Clarke, O. Grumberg, and D. Peled, Model Checking. The MIT Press, 2000.
[12] R. Bryant, "GraphBased Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, vol. 35, no. 8, pp. 667691, 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. 193207, 1999.
[14] J. MarquesSilva and K. Sakallah, "GRASP: A Search Algorithm for Propositional Satisfiability," IEEE Trans. Computers, vol. 48, no. 5, pp. 506521, 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. 530535, 2001.
[16] N. Eén and N. Sörensson, "An Extensible SATSolver," Proc. Int'l Conf. Theory and Applications of Satisfiability Testing, pp. 502518, 2003.
[17] A. Mishchenko, M. Case, R. Brayton, and S. Jang, "Scalable and ScalablyVerifiable 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 SATBased Model Checking Techniques in an Industrial Environment," Proc. Conf. Historical Analysis and Research in Marketing (CHARME), pp. 254268, 2005.
[20] H. Konuk and T. Larrabee, "Explorations of Sequential ATPG Using Boolean Satisfiability," Proc. IEEE VLSI Test Symp., pp. 8590, 1993.
[21] A. Smith, A. Veneris, M. Ali, and A. Viglas, "Fault Diagnosis and Logic Debugging Using Boolean Satisfiability," IEEE Trans. ComputerAided Design, vol. 24, no. 10, pp. 16061621, Oct. 2005.
[22] F. Lu and S. Malik, "Conflict Driven Learning in a Quantified Boolean Satisfiability Solver," Proc. Int'l Conf. ComputerAided Design (CAD), pp. 442449, 2002.
[23] A. Biere, "Resolve and Expand," Proc. Int'l Conf. Theory and Applications of Satisfiability Testing, pp. 238246, 2004.
[24] M. Benedetti, "sKizzo: A Suite to Evaluate and Certify QBFs," Proc. Int'l Conf. Automated Deduction, pp. 369376, 2005.
[25] H. Samulowitz and F. Bacchus, "Using SAT in QBF," Proc. Int'l Conf. Principles and Practive of Constraint Programming, pp. 578592, 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. 408414, 2005.
[27] T. Jussila and A. Biere, "Compressing BMC Encodings with QBF," Proc. Int'l Workshop Bounded Model Checking, pp. 114, 2006.
[28] H. Mangassarian, A. Veneris, S. Safarpour, M. Benedetti, and D. Smith, "A PerformanceDriven QBFBased Iterative Logic Array Representation with Applications to Verification, Debug and Test," Proc. Int'l Conf. CAD, pp. 240245, 2007.
[29] G. Tseitin, "On the Complexity of Derivations in the Propositional Calculus," Proc. Studies in Constructive Math. and Math. Logic, pp. 115125, 1968.
[30] M. Davis, G. Logemann, and D. Loveland, "A Machine Program for Theorem Proving," Comm. ACM, vol. 5, pp. 394397, 1962.
[31] M. Sheeran, S. Singh, and G. Stålmarck, "Checking Safety Properties Using Induction and a SATSolver," Proc. Formal Methods in ComputerAided Design, pp. 127144, 2000.
[32] M. Ali, S. Safarpour, A. Veneris, M. Abadir, and R. Drechsler, "PostVerification Debugging of Hierarchical Designs," Proc. Int'l Conf. CAD, pp. 871876, 2005.
[33] OpenCores.org, http:/www.opencores.org, 2006.
[34] C. Sinz and E. Dieringer, "DPvisA Tool to Visualize Structured SAT Instances," Proc. Int'l Conf. Theory and Applications of Satisfiability Testing, 2005.