2008 Research Summary

Word-Level Verification of Hardware Designs Using Selective Term-Level Abstraction

View Current Project Information

Sanjit A. Seshia and Bryan Brady

The goal of this research is to verify the correctness of RTL descriptions of digital hardware. UCLID is a system for term-level verification, meaning that finite-precision datatypes are abstracted into arbitrary-precision integers, and functional units are abstracted into uninterpreted functions. The benefit of term-level representations is that irrelevant information can be abstracted away, leading to a more efficiently verifiable model. On the other hand, this introduces imprecision into the model which can lead to both false positives and negatives.

In this project, we investigate combining term-level representations and reasoning with more precise word-level techniques. The problems include automatic abstraction of RTL into a combined representation and efficient SAT-based decision procedures for a combination of bit-vector and term-level problems. Our proposed solution combines type inference, counterexample-guided abstraction refinement, and a bit-vector decision procedure based on proof-based abstraction refinement.

Refer to [1-4] for background information.

[1]

R. E. Bryant, S. K. Lahiri, and S. A. Seshia, "Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions," Proc. Computer-Aided Verification, LNCS 2404, Copenhagen, Denmark, July 2002.

[2]

D. Kroening, J. Ouaknine, S. A. Seshia, and O. Strichman, "Abstraction-Based Satisfiability Solving of Presburger Arithmetic," Proc. Int. Conf. Computer-Aided Verification, LNCS 3114, July 2004, pp. 308-320.

[3]

S. K. Lahiri and S. A. Seshia, "The UCLID Decision Procedure," Proc. Int. Conf. Computer-Aided Verification, LNCS 3114, July 2004, pp. 475-478.

[4]

R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, and B. Brady, "Deciding Bit-Vector Arithmetic with Abstraction," 13th Int. Conf. on Tools and Algorithms for the Construction of Systems (TACAS), March 2007, pp. 358-372.