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