Word-Level Verification of Hardware Designs Using Selective Term-Level Abstraction
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.
- 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.
- 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.
- S. K. Lahiri and S. A. Seshia, "The UCLID Decision Procedure," Proc. Int. Conf. Computer-Aided Verification, LNCS 3114, July 2004, pp. 475-478.
- 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.