Automatic abstraction and verification of verilog models

ABSTRACT

Abstraction plays a critical role in verifying complex sys-tems. A number of languages have been proposed to model hardware systems by, primarily, abstracting away their wide datapaths while keeping the low-level details of their control logic. This leads to a significant reduction in the size of the state space and makes it possible to verify intricate control interactions formally. These languages, however, require that the abstraction be done manually, a tedious and error-prone process. In this paper we describe Vapor, a tool that auto-matically abstracts behavioral RTL Verilog to the CLU lan-guage used by the UCLID system. Vapor performs a sound abstraction with emphasis on minimizing false errors. Our method is fast, systematic, and complements UCLID by serving as a back-end for dealing with UCLID counterexamples. Preliminary results show the feasibility of automatic abstraction and its utility in formal verification.

REFERENCES

• 1: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 2: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, Validity Checking for Combinations of Theories with Equality, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.187-201, November 06-08, 1996
• 3: Randal E. Bryant , Shuvendu K. Lahiri , Sanjit A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proceedings of the 14th International Conference on Computer Aided Verification, p.78-92, July 27-31, 2002
• 4: Randal E. Bryant , Steven German , Miroslav N. Velev, Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.93-134, Jan. 2001 [doi>10.1145/371282.371364]
• 5: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 6: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 7: Ramin Hojati , Robert K. Brayton, Automatic Datapath Abstraction In Hardware Systems, Proceedings of the 7th International Conference on Computer Aided Verification, p.98-113, July 03-05, 1995
• 8: Matt Kaufmann , J. S. Moore, An Industrial Strength Theorem Prover for a Logic Based on Common Lisp, IEEE Transactions on Software Engineering, v.23 n.4, p.203-213, April 1997 [doi>10.1109/32.588534]
• 9: Shuvendu K. Lahiri , Sanjit A. Seshia , Randal E. Bryant, Modeling and Verification of Out-of-Order Microprocessors in UCLID, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.142-159, November 06-08, 2002
• 10: Maher Mneimneh , Fadi Aloul , Chris Weaver , Saugata Chatterjee , Karem Sakallah , Todd Austin, Scalable hybrid verification of complex microprocessors, Proceedings of the 38th conference on Design automation, p.41-46, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378265]
• 11: Sanjit A. Seshia, Shuvendue K. Lahiri, Randal E. Bryant. "A User's Guide to UCLID version 0.1".
• 12: Donald E. Thomas , Philip R. Moorby, The VERILOG Hardware Description Language, Kluwer Academic Publishers, Norwell, MA, 1991
• 13: "IEEE Std 1364-1995, IEEE Standard Hardware Description Language Based on the Verilog® Hardware Description Language" IEEE, Incs.
• 14: Dong Wang , Pei-Hsin Jiang , James Kukula , Yunshan Zhu , Tony Ma , Robert Damiano, Formal property verification by abstraction refinement with formal, simulation and hybrid engines, Proceedings of the 38th conference on Design automation, p.35-40, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378260]
• 15: Digital Equipment corporation, "The Alpha Architecture Handbook". 1992.
• 16: www.cs.utexas.edu/users/moore/acl2/
• 17: www.icarus.com/eda/verilog/
• 18: www-2.cs.cmu.edu/~uclid
• 19: vlsi.colorado.edu/~vis

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Verification

Keywords:
UCLID, abstraction, logic of counter arithmetic with lambda expressions and uninter-preted functions (CLU), register transfer level (RTL), verilog