Bat: The bit-level analysis tool

Abstract. While effective methods for bit-level verification of low-level proper-ties exist, system-level properties that entail reasoning about a significant part of the design pose a major verification challenge. We present the Bit-level Analy-sis Tool (BAT), a state-of-the-art decision procedure for bit-level reasoning that implements a novel collection of techniques targeted towards enabling the ver-ification of system-level properties. Key features of the BAT system are an ex-pressive 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.