Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences


UC Berkeley


2009 Research Summary

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

View Current Project Information

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

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