Abstract
Reducing run times and the amount of memory needed for computations is one requirement in order to match today's sizes of real world designs in formal hardware verification. Designs are usually given as Register-Transfer-Level (RTL) specifications, but most of today's hardware verification tools are based on bit-level methods. However, designs, like for example ALUs or bus interfaces, often have very regular structures that can be described easily on a higher level of abstraction. This information is lost on bit-level and thus cannot be utilized by verification tools, if verification procedures operate on the basis of bit-level descriptions. Recently, several approaches to formal circuit verification have been proposed that make use of such regularities. These approaches are based on word-level descriptions as they are available on the RTL. We introduce the main concepts of formal verification on the RTL and give a brief overview of existing techniques. Recent developments are outlined, and based on real world examples we show the advantages of the use of word-level information for equivalence checking and property checking.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
REFERENCES
Barrett, C.W., Dill, D.L, and Levitt, J.R., A Decision Procedure for Bit-Vector Arithmetic, Design Autom. Conf., 1998, pp. 522–527.
Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., and Zhu, Y., Symbolic Model Checking using SAT Procedures Instead of BDDs, Design Autom. Conf., 1999, pp. 317–320.
Brinkmann, R. and Drechsler, R., RTL-datapath Verification using Integer Linear Programming, ASP Design Autom. Conf., 2002, pp. 741–746.
Bryant, R.E. and Chen, Y.-A., Verification of Arithmetic Functions with Binary Moment Diagrams, Technical report, 1994, CMU-CS-94-160.
Clarke, E., Emerson, E., Jha, S., and Sistla, A., Symmetry Reduction in Model Checking, in Computer Aided Verification, 1998, vol. 1447 of LNCS, pp. 147–158.
Clarke, E., Grumberg, O., and Long, D., Model Checking and Abstraction, Symp. on Principles of Programming Languages, 1992, pp. 342–354.
Clarke, E.M., Fujita, M., and Zhao, X., Hybrid Decision Diagrams—Overcoming the Limitations of MTBDDs and BMDs, Int. Conf. on CAD, 1995, pp. 159–163.
Cyrluk, D., Möller, O., and Rueß, H., An Efficient Decision Procedure for the Theory of Fixed-sized Bitvectors, in Computer Aided Verification, 1997, vol. 1254 of LNCS, pp. 60–71.
Dershowitz, N. and Jouannaud, J., Handbook of Theoretical Computer Science, Formal Methods and Semantics, New York: Elsevier, 1990.
Drechsler, R., Formal Verification of Circuits, New York: Kluwer, 2000.
Drechsler, R., Becker, B., and Ruppertz, S., K*BMDs: A New Data Structure for Verification, Eur. Design ℰ Test Conf., 1996, pp. 2–8.
Drechsler, R. and Höreth, S., Manipulation of *BMDs, ASP Design Autom. Conf., 1998, pp. 433–438.
Drechsler, R. and Höreth, S., Gatecomp: Equivalence Checking of Digital Circuits in an Industrial Environment, Int. Workshop on Boolean Problems, 2002, pp. 195–200.
Emerson, E. and Trefler, R., From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking, CHARME, 1999, pp. 142–156.
Fallah, F., Coverage Directed Validation of Hardware Models, PhD Dissertation, MIT, 1999.
Fallah, F., Devadas, S., and Keutzer, K., Functional Vector Generation for HDL Models using Linear Programming and 3-satisfiability, Design Autom. Conf., 1998, pp. 528–533.
Höreth, S., Implementation of a Multiple-Domain Decision Diagram Package, in CHARME, New York: Chapman &; Hall, 1997, pp. 185–202.
Höreth, S., A Word-level Graph Manipulation Package, Software Tools Tech. Transfer, 2001, no. 3(2).
Höreth, S. and Drechsler, R., Formal Verification of Word-level Specifications, Design, Automation and Test in Europe, 1999, pp. 52–58.
Huang, C.-Y. and Cheng, K.-T., Assertion Checking by Combined Word-level ATPG and Modular Arithmetic Constraint-solving Techniques, Design Autom. Conf., 2000, pp. 118–123.
Johannsen, P. and Drechsler, R., Formal Verification on Register Transfer Level—Utilizing High-level Information for Hardware Verification, IFIP Int. Conf. on VLSI, 2001, pp. 127–132.
Kuehlmann, A., Ganai, M., and Paruthi, V., Circuit-based Boolean Reasoning, Design Autom. Conf., 2001, pp. 232–237.
Möller, M. and Rueß, H., Solving Bit-Vector Equations, Int. Conf. on Formal Methods in CAD, 1998, pp. 36–48.
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., and Malik, S., Chaff: Engineering an Efficient SAT Solver, Design Autom. Conf., 2001, pp. 530–535.
Pugh, W., The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis, Proc. ACM, 1992, no. 8, pp. 102–114.
Scholl, C., Becker, B., and Weis, T.M., Word-level Decision Diagrams, WLCDs and Division, Int. Conf. on CAD, 1998, pp. 672–677.
Silva, J., Search Algorithms for Satisfiability Problems in Combinational Switching Circuits, PhD Dissertation, Univ. of Michigan, 1995.
Thathachar, J.S., On the Limitations of Ordered Representations of Functions, Computer Aided Verifi-cation, 1998, vol. 1427, pp. 232–243.
Velev, M. and Bryant, R., Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors, Design Autom. Conf., 2001, pp. 226–231.
Zeng, Z., Kalla, P., and Ciesielski, M., LPSAT: A Unified Approach to RTL Satisfiability, Design, Autom. and Test in Eur., 2001, pp. 398–402.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Drechsler, R. Using Word-Level Information in Formal Hardware Verification. Automation and Remote Control 65, 963–977 (2004). https://doi.org/10.1023/B:AURC.0000030907.28679.82
Issue Date:
DOI: https://doi.org/10.1023/B:AURC.0000030907.28679.82