Research Projects

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

Sanjit A. Seshia and Bryan Brady

Semiconductor Research Corporation 1355.001

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.

Background information can be found in references [1,2].

[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]

R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, and B. Brady, "An Abstraction-Based Decision Procedure for Bit-Vector Arithmetic," International Journal on Software Tools for Technology Transfer, 2008, to appear.

More information: http://uclid.eecs.berkeley.edu/v2ucl/