Welcome to the homepage of BAT, the Bit-level Analysis Tool. BAT is a tool for deciding bounded model checking and k-induction queries for a powerful hardware description language that is strongly typed (with type inference), includes bit vectors, memories, and the standard operations on these data types, allows for user defined functions, functions which return multiple values, etc.
BAT was first released in 2006, and can be thought of as an SMT solver (decision procedure) for the quantifier-free fragment of first-order logic that includes the extensional theory of bit-vector arrays (memories) and fixed-size bit-vectors. BAT is an eager solver that uses term-rewriting as a preprocessing step and then uses various techniques to generate SAT instances. These techniques include:
- A powerful technique for greatly reducing memories.
- Subformula hashing.
- The integration of term-rewriting techniques into the translation algorithm.
- A new CNF generation algorithm.
Key features of the BAT language are:
- Strongly typed, with type inference.
- Essentially equivalent to synthesizable subsets of HDLs such as Verilog.
- User-defined functions.
- Constant definitons for easily creating parameterized models.
- Memories are treated as first-class objects. This means they can be passed to functions and compared for (in)equality.
The result is a tool that can solve problems that cannot be handled by any other decision procedure we have tried (circa 2010). For example, BAT can prove that a 32-bit 5 stage pipelined machine model refines its ISA in approximately 2 minutes. We know of no other tools that can solve even much simpler pipeline machine examples. See the benchmarks page for this and other benchmarks.
To find out more about BAT or to use it yourself, see the links along the left side of this website. On October 2014, we released a new version of BAT along with sources.
Contact us if you have any questions or want to collaborate on interesting applications.
The original authors were Pete Manolios (Advisor, Architect, Lead), Sudarshan Srinivasan (Applications, Benchmarks), and Daron Vroon (Developer, Algorithms). Significant contributions were made by Ben Chambers (CNF generation for V2). Eugene Goldberg and Vasilis Papavasileiou helped with integration and distribution for V2.