Self-adjusting constrained random stimulus generation using splitting evenness evaluation and XOR constraints

ABSTRACT

Constrained random stimulus generation plays significant roles in hardware verification nowadays, and the quality of the generated stimuli is key to the efficiency of the test process. In this work, we present a linear dynamic method to guide random stimulus generation by SAT solvers. A splitting simplified Min-Distance-Sum evaluation method and an XOR sampling strategy are integrated in the self-adjusting random stimulus generation framework. The evenness of the split groups is evaluated to find out some uneven parts. Then, random partial solutions for the uneven parts and random XOR constraints for the other inputs are added into constraints to get better distributed stimuli. Experimental results show that our method can evaluate the evenness as well as more complex formulae for stimulus generation, and also confirm that the self-adjusting method can improve the fault coverage ratio by more than 17% averagely with the same number of stimuli.

REFERENCES

• 1: Synopsys Inc., "Constrained-random test generation and functional coverage with Vera," Technical report, Feb. 2003.
• 2: L. Singh, L. Drucker, "Advanced Verification Techniques: A SystemC Based Approach for Successful Tapeout," Springer US, 2004.
• 3: SystemC Verification Working Group, "Systemc verification standard specification," OSCI website: http://www.systemc.org, May. 2003.
• 4: J. Yuan, A. Aziz, C. Pixley, K. Albin, "Simplifying Boolean constraint solving for random simulation-vector generation," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 23, No. 3, pp. 412--420, 2004.
• 5: Jun Yuan , Carl Pixley , Adnan Aziz, Constraint-Based Verification, Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 6: João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
• 7: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 8: N. Eén and N. Sörensson, "An extensible SAT solver," International Conference on Theory and Applications of Satisfiability Testing, pp. 502--518, 2003.
• 9: Nathan Kitchen , Andreas Kuehlmann, Stimulus generation for constrained random simulation, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
• 10: C. P. Gomes, A. Sabharwal, B. Selman, "Near-Uniform Sampling of Combinatorial Spaces Using XOR Constraints," the 20th Annual Conference on Neural Information Processing Systems, pp. 481--488, Dec 2006.
• 11: C. P. Gomes, W. Hoeve, A. Sabharwal, B. Selman, "Counting CSP Solutions Using Generalized XOR Constraints," the 22nd Conference on Artificial Intelligence, pp. 204--209, July 2007.
• 12: Stephen M. Plaza , Igor L. Markov , Valeria Bertacco, Random stimulus generation using entropy and XOR constraints, Proceedings of the conference on Design, automation and test in Europe, March 10-14, 2008, Munich, Germany [doi>10.1145/1403375.1403538]
• 13: L G Valiant , V V Vazirani, NP is as easy as detecting unique solutions, Proceedings of the seventeenth annual ACM symposium on Theory of computing, p.458-463, May 06-08, 1985, Providence, Rhode Island, United States [doi>10.1145/22145.22196]
• 14: A. J. Compton, "An Algorithm for the Even Distribution of Entities in One Dimension," the Computer Journal, Vol. 28, No. 5, pp. 530--537, 1985.
• 15: H. K. Lee and D. S. Ha, "HOPE: An Efficient Parallel Fault Simulator for Synchronous Sequential Circuits," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 15, No. 9, pp. 1048--1058, 1996.
• 16: ISCAS89 Sequential Benchmark Circuits: http://www.ece.vt.edu/mhsiao/iscas89.html
• 17: Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001 [doi>10.1023/A:1011276507260]