# 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.