skip to main content
10.1145/1228784.1228879acmconferencesArticle/Chapter ViewAbstractPublication PagesglsvlsiConference Proceedingsconference-collections
Article

Reducing verification overhead with RTL slicing

Published: 11 March 2007 Publication History

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]
J. A. Abraham, V. M. Vedula, and D. G. Saab. Verifying properties using sequential atpg. In Proc. Intl. Test Conf., pages 194--202, 2002.
[2]
S. Bates and S. Horwitz. Incremental program testing using program dependence graphs. In Twentieth ACM Symposium on Principles of Programming Languages, pages 384--396, 1993.
[3]
A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using sat procedures instead of bdds. In Proc. DAC, pages 317--320, 1999.
[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]
S. A. Cook. The complexity of theorem proving procedures. In The 3rd Annual ACM Symposium on the Theory of Computation, pages 151--158, 1971.
[6]
Intel Corporation. Usb 2.0 transceiver microcell interface specification. In Intel, 2001.
[7]
K. B. Gallagher and J. R. Lyle. Using program slicing in software maintenance. IEEE Transactions on Software Engineering, pages 751--761, Aug. 1991.
[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]
N. K. Jha and S. Gupta. Testing of Digital Systems. Cambridge Univ. Press, 2003.
[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]
M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient sat solver. In Proc. DAC, pages 530--535, June 2001.
[14]
G. Parthasarathy, C.-Y. Huang, and K.-T. Cheng. An analysis of atpg and sat algorithms for formal verification. In Proc. 6th IEEE Intl. HLDVT Workshop, pages 177--182, November 2001.
[15]
Q. Qiang, C.-L. Chang, D. G. Saab, and J. A. Abraham. Case study of atpg-based bounded model checking: Verifying usb2.0 ip core. In Proc. of ICCD, 2005.
[16]
Q. Qiang, D. G. Saab, and J. A. Abraham. Checking nested properties using bounded model checking and sequential atpg. In Proc. 19th Intl. Conf.on VLSI Design, 2006.
[17]
D. G. Saab, J. A. Abraham, and V. M. Vedula. Formal verification using bounded model checking: Sat versus sequential atpg engines. In Proc. 16th Intl. Conf. on VLSI Design, 2003.
[18]
A. Silburt. Functional verification of silicon intensive system. In On-Chip System Design Conf., 1998.
[19]
J. M. Silva and K. A. Sakallah. Grasp-a new search algorithm for satis ability. In ICCAD, pages 220--227, November 1996.
[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 and J. A. Abraham. A novel methodology for hierarchical test generation using functional constraint composition. In Proc. of the 5th Int. workshop on High Level Design Validation and Test, pages 9--14, 2000.
[23]
V. M. Vedula, J. A. Abraham, and J. Bhadra. Program slicing for hierarchical test generation. In Proc. of the 20th IEEE VTS, pages 237--246, 2002.
[24]
V. M. Vedula, W. J. Townsend, and J. A. Abraham. Program slicing for atpg-based property checking. In Proc. of the 17th Int. Conf. on VLSI Design, 2004.
[25]
M. Weise. Program slicing. IEEE Transactions on Software Engineering, pages 352--357, 1984.
[26]
M. Weiser. Programmers use slices when debugging. CACM, 25(7):446--452, 1982.
[27]
H. Zhang. Sato: An efficient propositional prover. In Intl. Conf. on Automated Deduction, pages 272--275, 1997.

Cited By

View all
  • (2021)Learning semantic representations to verify hardware designsProceedings of the 35th International Conference on Neural Information Processing Systems10.5555/3540261.3542060(23491-23504)Online publication date: 6-Dec-2021

Index Terms

  1. Reducing verification overhead with RTL slicing

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    GLSVLSI '07: Proceedings of the 17th ACM Great Lakes symposium on VLSI
    March 2007
    626 pages
    ISBN:9781595936059
    DOI:10.1145/1228784
    Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

    Sponsors

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 11 March 2007

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. CAD
    2. test
    3. verification

    Qualifiers

    • Article

    Conference

    GLSVLSI07
    Sponsor:
    GLSVLSI07: Great Lakes Symposium on VLSI 2007
    March 11 - 13, 2007
    Stresa-Lago Maggiore, Italy

    Acceptance Rates

    Overall Acceptance Rate 312 of 1,156 submissions, 27%

    Upcoming Conference

    GLSVLSI '25
    Great Lakes Symposium on VLSI 2025
    June 30 - July 2, 2025
    New Orleans , LA , USA

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)6
    • Downloads (Last 6 weeks)1
    Reflects downloads up to 28 Jan 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2021)Learning semantic representations to verify hardware designsProceedings of the 35th International Conference on Neural Information Processing Systems10.5555/3540261.3542060(23491-23504)Online publication date: 6-Dec-2021

    View Options

    Login options

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Figures

    Tables

    Media

    Share

    Share

    Share this Publication link

    Share on social media