Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques

ABSTRACT

We present a new approach to checking assertion properties for RTI, design verification. Our approach combines structural, word-level automatic test pattern generation (ATPG) and modular arithmetic constraint-solving techniques to solve the constraints imposed by the target assertion property. Our word-level ATPG and implication technique not only solves the constraints on the control logic, but also propagates the logic implications to the datapath. A novel arithmetic constraint solver based on modular number system is then employed to solve the remaining constraints in datapath. The advantages of the new method are threefold. First, the decision-making process of the word-level ATPG is confined to the selected control signals only. Therefore, the enumeration of enormous number of choices at the datapath signals is completely avoided. Second, our new implication translation techniques allow word-level logic implication being performed across the boundary of datapath and control logic, and therefore, efficiently cut down the ATPG search space. Third, our arithmetic constraint solver is based on modular instead of integral number system. It can thus avoid the false negative effect resulting from the bit-vector value modulation. A prototype system has been built which consists of an industrial front-end HDL parser, a property-to-constraint converter and the ATPG/arithmetic constraint-solving engine. The experimental results on some public benchmark and industrial circuits demonstrate the efficiency of our approach and its applicability to large industrial designs.

REFERENCES

• 1: Ranga Vemuri , Ravi Kalyanaraman, Generation of design verification tests from behavioral VHDL programs using path enumeration and constraint programming, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.3 n.2, p.201-214, June 1995 [doi>10.1109/92.386221]
• 2: Chian-Min Richard Ho, Validation tools for complex digital designs, Stanford University, Stanford, CA, 1997
• 3: Farzan Fallah , Srinivas Devadas , Kurt Keutzer, Functional vector generation for HDL models using linear programming and 3-satisfiability, Proceedings of the 35th annual conference on Design automation, p.528-533, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277187]
• 4: Kwang-Ting Cheng , A. S. Krishnakumar, Automatic generation of functional vectors using the extended finite state machine model, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.1 n.1, p.57-79, Jan. 1996 [doi>10.1145/225871.225880]
• 5: R. C-Y Huang, and K-T. Cheng, "A New Extended Finite State Machine (EFSM) Model for RTL Design Verification", Proc. IEEE International High Level Design Validation and Test Workshop, Nov. 1998, pp. 47-53.
• 6: E. M. Clarke and E. A. Emerson, "Synthesis of Synchronization Skeletons for Branching Time Temporal Logic", Lecture Notes in Comp. Science, Vol. 131, May, 1981, pp. 244-263.
• 7: "Murphi description language and verifier", http://verify.stanford.edu/cgi-bin/wrap/dill/Murphi.
• 8: In-Ho Moon , Jae-Young Jang , Gary D. Hachtel , Fabio Somenzi , Jun Yuan , Carl Pixley, Approximate reachability don't cares for CTL model checking, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.351-358, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289053]
• 9: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 10: "The SMV System", http://www.cs.cmu.edu/,--modelcheck/ smv.html.
• 11: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 12: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 13: A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309942]
• 14: A. Pnueli, "A Temporal Logic of Concurrent Programs", Theoretical Computer Science, 13:45-60, 1981.
• 15: Lawrence H. Goldstein , Evelyn L. Thigpen, SCOAP: Sandia controllability/observability analysis program, Proceedings of the 17th conference on Design automation, p.190-196, June 23-25, 1980, Minneapolis, Minnesota, United States [doi>10.1145/800139.804528]
• 16: F. Brglez, "On Testability Analysis of Combinational Networks", Proc. ISCAS, May 1984, pp. 221-225.
• 17: Allenby, "Rings, Fields, and Groups", Edward Arnold Ltd., 1983.
• 18: B.W. Jones, "Modular Arithmetic", Blaisdell Publishing Company, 1964.

INDEX TERMS

Primary Classification:
  J. Computer Applications

Additional Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids
          Subjects: Hardware description languages
  B.8 Performance and Reliability

General Terms:
Design, Experimentation, Languages, Measurement, Performance, Theory, Verification