BAT
Bit-level Analysis Tool, version 2

Papers



Automatic Memory Reductions for RTL-Level Verification.

Panagiotis Manolios, Sudarshan K. Srinivasan, and Daron Vroon.
International Conference on Computer Aided Design (ICCAD-2006), 2006. © ACM

Abstract

We present several techniques for automatically reducing memories in RTL designs. This includes a new memory abstraction algorithm that allows us to greatly reduce the size of memories and a technique based on-term rewriting that further improves the abstraction. In contrast to previously proposed methods for abstracting memories of RTL designs, our methods are general---e.g., they allow us to arbitrarily and directly compare memories---and they are sound and complete---e.g., there are no false positives or negatives. In addition, the combination of our techniques allows us to automatically verify RTL pipelined machine designs beyond the reach of current state-of-the-art methods, as our experimental results show.

Paper
Presentation

Efficient Circuit to CNF Conversion

Panagiotis Manolios and Daron Vroon.
SAT 2007, The Tenth International Conference on Theory and Applications of Satisfiability Testing, 200. © Springer

Abstract

Modern SAT solvers are proficient at solving Boolean satisfiability problems in Conjunctive Normal Form (CNF). However, these problems mostly arise from general Boolean circuits that are then translated to CNF. We outline a simple and expressive data structure for describing arbitrary circuits, as well as an algorithm for converting circuits to CNF. Our experimental results over a large benchmark suite show that the CNF problems we generate are consistently smaller and more quickly solved by modern SAT solvers than the CNF problems generated by current CNF generation methods.

Paper

BAT: The Bit-Level Analysis Tool.

 Panagiotis Manolios, Sudarshan K. Srinivasan, and Daron Vroon.
CAV 2007, Nineteenth International on Computer Aided Verification, 2007. © Springer

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.

Paper

Faster SAT Solving with Better CNF Generation.

Benjamin Chambers, Panagiotis Manolios, and Daron Vroon.
DATE: Design, Automation, and Test, Europe, 2009. © ACM

Abstract

Boolean satisfiability (SAT) solving has become an enabling technology with wide-ranging applications in numerous disciplines. These applications tend to be most naturally encoded using arbitrary Boolean expressions, but to use modern SAT solvers, one has to generate expressions in Conjunctive Normal Form (CNF). This process can significantly affect SAT solving times. In this paper, we introduce a new linear-time CNF generation algorithm. We have implemented our algorithm and have conducted extensive experiments, which show that our algorithm leads to faster SAT solving times and smaller CNF than existing approaches.

Paper