Welcome to the homepage of BAT, the Bit-level Analysis Tool. BAT implements a state-of-the-art decision procedure for solving quantifier-free formulas over the extensional theory of fixed-size bit-vectors and fixed-size bit-vector arrays (memories). Such problems often appear in hardware, software, and security domains. BAT uses innovative techniques for efficiently translating from the high-level BAT language into tractable SAT problems. 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. 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.
Contact us if you have any questions or want to collaborate on interesting applications.