| | This Article | |
| |
| |
| | Share | |
| |
| |
| | Bibliographic References | |
| |
| |
| | Add to: | |
| |
 Digg
 Furl
 Spurl
 Blink
 Simpy
 Google
 Del.icio.us
 Y!MyWeb
| |
| | Search | |
| |
| |
| | |
A New Simulation-Based Property Checking Algorithm Based on Partitioned Alternative Search Space Traversal
November 2006 (vol. 55 no. 11)
pp. 1325-1334
We present a new logic-simulation-based algorithm on verifying safety properties of large sequential hardware designs. This algorithm explores the search space defined by partitioned internal circuit nodes. Two powerful features are proposed to increase the effectiveness during search space exploration and counterexample generation for verifying safety properties. These include 1) new search space constituted by internal nodes instead of state variables and 2) static learning on multiple nodes to further enlarge the target. These two features are integrated with the following techniques during our simulation: incorporation of a BCP (Boolean Constraint Propagation) engine for multiple nodes implication and multiple-time-frame GA (Genetic Algorithm) search. Because only logic simulation is needed in our algorithm, the computational effort is low. Experimental results on large benchmark circuits have shown that this logic-simulation-based verifier achieves significantly better results compared with existing formal verification tools and simulation-based methods.
[1] 1325 J. Jain, A. Narayan, M. Fujita, and A. Sangiovanni-Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuit,” Proc. Int'l Conf. Computer Design (ICCD), pp. 445-454, 1997.[2] L. Lamport, “Proving the Correctness of Multiprocess Programs,” IEEE Trans. Software Eng., vol. 3, no. 2, pp. 124-142, Mar. 1977.[3] C. Kern and M. Greenstreet, “Formal Verification in Hardware Design: A Survey,” ACM Trans. Design Automation of Electronic Systems, vol. 4, no. 2, pp. 123-193, Apr. 1999.[4] “${\rm Mur}\phi$ Description Language and Verifier,” http://sprout. stanford.edu/dillmurphi.html , 2006.[5] K.L. McMillan, Symbolic Model Checking. Boston: Kluwer Academic, 1993.[6] “The SMV System,” http://www-2.cs.cmu.edu/~modelchecksmv.html , 2006.[7] H. Iwashita and T. Nakata, “Forward Model Checking Techniques Oriented to Buggy Designs,” Proc. Int'l Conf. Computer-Aided Design (ICCAD), pp. 400-404, Nov. 1997.[8] V. Boppana, S.P. Rajan, K. Takayama, and M. Fujita, “Model Checking Based on Sequential ATPG,” Proc. Computer-Aided Verification Conf. (CAV), pp. 418-430, 1999.[9] C.-Y. Huang and K.-T. Cheng, “Assertion Checking by Combined Word-Level ATPG and Modular Arithmetic Constraint-Solving Techniques,” Proc. Design Automation Conf., pp. 118-123, June 2000.[10] M.K. Ganai, A. Aziz, and A. Kuehlmann, “Enhancing Simulation with BDDs and ATPG,” Proc. Design Automation Conf. (DAC), pp.385-390, 1999.[11] G. Parthasarathy, C.-Y. Huang, and K.-T. Cheng, “An Analysis of ATPG and SAT Algorithms for Formal Verification,” Proc. High-Level Design Validation and Test Workshop, pp. 177-182, Nov. 2001.[12] J.A. Abraham, V.M. Vedula, and D.G. Saab, “Verifying Properties Using Sequential ATPG,” Proc. Int'l Test Conf., pp. 194-202, 2002.[13] M. Hsiao and J. Jain, “Practical Use of Sequential ATPG for Model Checking: Going the Extra Mile Does Pay Off,” Proc. High-Level Design Validation and Test Workshop, pp. 39-44, Nov. 2001.[14] S. Sheng, K. Takayama, and M.S. Hsiao, “Effective Safety Property Checking Using Simulation-Based Sequential ATPG,” Proc. Design Automation Conf. (DAC), pp. 813-818, 2002.[15] A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures instead of BDDs,” Proc. Design Automation Conf., pp. 317-320, 1999.[16] J.P. Marques-Silva and K.A. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Trans. Computers, vol. 48, no. 5, pp. 506-521, May 1999.[17] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an Efficient SAT Solver,” Proc. Design Automation Conf., pp. 530-535, 2001.[18] Q. Wu and M.S. Hsiao, “Efficient Sequential ATPG Based on Partitioned Finite-State-Machine Traversal,” Proc. Int'l Test Conf., pp. 281-289, 2003.[19] Q. Wu and M.S. Hsiao, “Efficient ATPG for Design Validation Based on Partitioned State Exploration Histories,” Proc. VLSI Test Symp., pp. 389-394, 2004.[20] Q. Wu and M.S. Hsiao, “State Variable Extraction to Reduce Problem Complexity for ATPG and Design Validation,” Proc. Int'l Test Conf., pp. 820-829, 2004.[21] A. Pnueli, “The Temporal Semantics of Concurrent Programs,” Proc. Int'l Symp. Semantics of Computer Science, pp. 1-20, 1979.[22] E. Clarke, E.A. Emerson, and A. Sistla, “Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications,” ACM Trans. Programming Languages and Systems, vol. 1, no. 2, pp. 244-263, 1986.[23] J.P. Hayes, Introduction to Digital Logic Design. Reading, Mass.: Addison-Wesley, 1993.[24] J.W. Freeman, “Improvements to Propositional Satisfiability Search Algorithms,” PhD dissertation, Dept. of Computer and Information Science, Univ. of Pennsylvania, May 1995.[25] R. Zabih and D.A. McAllester, “A Rearrangement Search Strategy for Determining Propositional Satisfiability,” Proc. Nat'l Conf. Artificial Intelligence, pp. 155-160, 1988.[26] M. Davis and H. Putnam, “A Computing Procedure for Quantification Theory,” J. ACM, vol. 7, pp. 201-215, 1960.[27] “Genetic Algorithm Tutorial Home Page,” http://www.estec. esa.nl/outreach/gatutor Default.htm, 2005.[28] D.E. Goldberg, Genetic Algorithms in Search, Optimization & Machine Learning. Reading, Mass.: Addison-Wesley, 1989.[29] J.-K. Zhao, E.M. Rudnick, and J.H. Patel, “Static Logic Implication with Application to Fast Redundancy Identification,” Proc. VLSI Test Symp., pp. 288-293, 1997.[30] F. Brglez, D. Bryan, and K. Kozminski, “Combinational Profiles of Sequential Benchmark Circuits,” Proc. Int'l Symp. Circuits and Systems, pp. 1929-1934, 1989.[31] S. Davidson, M. Niermann, and J.H. Patel, “HITEC: A Test Generation Package for Sequential Circuits,” Proc. European Design Automation Conf., pp. 214-218, 1991.[32] M.S. Hsiao, E.M. Rudnick, and J.H. Patel, “Sequential Circuit Test Generation Using Dynamic State Traversal,” Proc. European Design and Test Conf., pp. 22-28, 1997.
Index Terms:
Automatic test pattern generation (ATPG), verification, logic-simulation, satisfiability.
Citation:
Qingwei Wu, Michael S. Hsiao, "A New Simulation-Based Property Checking Algorithm Based on Partitioned Alternative Search Space Traversal," IEEE Transactions on Computers, vol. 55, no. 11, pp. 1325-1334, Nov. 2006, doi:10.1109/TC.2006.170
