BAT: The Bit-Level Analysis Tool

---

Panagiotis Manolios, Sudarshan K. Srinivasan, and Daron Vroon.
Computer Aided Verification (CAV-2007), 2007. © Springer-Verlag

Abstract

While effective methods for bit-level verification of low-level properties exist, system-level properties that entail reasoning about a significant part of the design pose a major verification challenge. We present the Bit-level Analysis Tool (BAT), a state-of-the-art decision procedure for bit-level reasoning that implements a novel collection of techniques targeted towards enabling the verification of system-level properties. Key features of the BAT system are an expressive strongly-typed modeling and specification language, a fully automatic and efficient memory abstraction algorithm for extensional arrays, and a novel CNF generation algorithm. The BAT system can be used to automatically solve system-level RTL verification problems that were previously intractable, such as refinement-based verification of RTL-level pipelined machines.

PDF (35K) © Springer-Verlag