Reducing verification overhead with RTL slicing

ABSTRACT

Design complexity is increasing with every technology generation, causing verification tools to require large amounts of resources. In this paper, we develop a technique to reduce the complexity of verifying digital designs described in a Hardware Description Language (HDL). For a given property to be verified, we derive an HDL executable design slice that is behaviorally equivalent to the original design. The slice is less complex than the original design and requires fewer resources for analysis by a verification tool. The slicer is implemented as a pre-processor to SMV, a SAT-based verification tool, and Formal, an ATPG-based verification tool. Experimental results on the USB2.0 IP core show that RTL slicing reduces both CPU and memory overhead for both SMV and Formal. This reduction allows the verification tools to effectively deal with complex designs.

REFERENCES

• 1: Jacob A. Abraham , Vivekananda M. Vedula , Daniel G. Saab, Verifying Properties Using Sequential ATPG, Proceedings of the 2002 IEEE International Test Conference, p.194, October 07-10, 2002
• 2: Samuel Bates , Susan Horwitz, Incremental program testing using program dependence graphs, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.384-396, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158694]
• 3: 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]
• 4: E. M. Clarke, M. Fujita, S. P. Rajan, T. W. Reps, S. Shankar, and T. Teitelbaum. Program slicing of hardware description languages. In Technical Report CMU-CS99-103, 1999.
• 5: Stephen A. Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing, p.151-158, May 03-05, 1971, Shaker Heights, Ohio, United States [doi>10.1145/800157.805047]
• 6: Intel Corporation. Usb 2.0 transceiver microcell interface specification. In Intel, 2001.
• 7: Keith Brian Gallagher , James R. Lyle, Using Program Slicing in Software Maintenance, IEEE Transactions on Software Engineering, v.17 n.8, p.751-761, August 1991 [doi>10.1109/32.83912]
• 8: P. Goel. An implicit enumeration algorithm to generate tests for combinational logic circuits. IEEE Trans. on Computers, 30(3):215--222, March 1981.
• 9: M. Iwaihara, M. Nomura, S. Ichinose, and H. Yasuura. Program slicing on vhdl descriptions and its applications. In Proc. of Asian Pacific Conf. on Hardware Description Languages, pages 132--139, 1996.
• 10: Niraj K. Jha , Sandeep Gupta, Testing of Digital Systems, Cambridge University Press, New York, NY, 2002
• 11: T. Li, Yang G., and S. Li. An automatic circuit extractor for rtl verification. In Proc. of the 12th Asian Test Symposium, 2003.
• 12: M. A. Breuer M. Abramovici and and A. D. Friedman. Digital Systems Testing and Testable Design. IEEE Press, 1990.
• 13: 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]
• 14: G. Parthasarathy , Kwang-Ting Cheng , Chung-Yang Huang, An Analysis of ATPG and SAT algorithms for Formal Verification, Proceedings of the Sixth IEEE International High-Level Design Validation and Test Workshop (HLDVT'01), p.177, December 07-09, 2001
• 15: Qiang Qiang , Qiang, Chia-Lun Chang , Daniel G. Saab , Jacob A. Abraham, Case Study of ATPG-based Bounded Model Checking: Verifying USB2.0 IP Core, Proceedings of the 2005 International Conference on Computer Design, p.461-463, October 02-05, 2005 [doi>10.1109/ICCD.2005.36]
• 16: Qiang Qiang , Daniel G. Saab , Jacob A. Abraham, Checking Nested Properties Using Bounded Model Checking and Sequential ATPG, Proceedings of the 19th International Conference on VLSI Design held jointly with 5th International Conference on Embedded Systems Design, p.225-230, January 03-07, 2006 [doi>10.1109/VLSID.2006.58]
• 17: Daniel G. Saab , Jacob A. Abraham , Vivekananda M. Vedula, Formal Verification Using Bounded Model Checking: SAT versus Sequential ATPG Engines, Proceedings of the 16th International Conference on VLSI Design, p.243, January 04-08, 2003
• 18: A. Silburt. Functional verification of silicon intensive system. In On-Chip System Design Conf., 1998.
• 19: 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
• 20: SMV. Candence smv. In http://www-cad.eecs.berkeley.edu/. Candence Berkeley Lab., 2003.
• 21: R. Usselmann. Usb function ip core. In http://www.opencores.org, 2002.
• 22: V. M. Vedula , J. A. Abraham, A novel methodology for hierarchical test generation using functional constraint composition, Proceedings of the IEEE International High-Level Validation and Test Workshop (HLDVT'00), p.9, November 08-10, 2000
• 23: Vivekananda M. Vedula , Jacob A. Abraham , Jayanta Bhadra, Program Slicing for Hierarchical Test Generation, Proceedings of the 20th IEEE VLSI Test Symposium, p.237, April 28-May 02, 2002
• 24: Vivekananda M. Vedula , Whitney J. Townsend , Jacob A. Abraham, Program Slicing for ATPG-Based Property Checking, Proceedings of the 17th International Conference on VLSI Design, p.591, January 05-09, 2004
• 25: M. Weise. Program slicing. IEEE Transactions on Software Engineering, pages 352--357, 1984.
• 26: Mark Weiser, Programmers use slices when debugging, Communications of the ACM, v.25 n.7, p.446-452, July 1982 [doi>10.1145/358557.358577]
• 27: Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids

General Terms:
Algorithms, Design, Experimentation

Keywords:
CAD, test, verification