- Panagiotis Manolios, Sudarshan K. Srinivasan, and Daron Vroon. Automatic Memory Reductions for RTL-Level Verification. ICCAD 2006, ACM-IEEE International Conference on Computer Aided Design, November 2006.
- Panagiotis Manolios and Daron Vroon. Efficient Circuit to CNF Conversion. SAT 2007, The Tenth International Conference on Theory and Applications of Satisfiability Testing, May 2007.
- Panagiotis Manolios, Sudarshan Srinivasan, and Daron Vroon. BAT: The Bit-Level Analysis Tool. CAV 2007, Nineteenth International on Computer Aided Verification, July 2007.
- Benjamin Chambers, Panagiotis Manolios, and Daron Vroon. Faster SAT Solving with Better CNF Generation. DATE 2009, Design Automation and Test in Europe, April 2009.
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
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.
Efficient Circuit to CNF ConversionPanagiotis Manolios and Daron Vroon.
SAT 2007, The Tenth International Conference on Theory and Applications of Satisfiability Testing, 200. © Springer
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.
BAT: The Bit-Level Analysis Tool.Panagiotis Manolios, Sudarshan K. Srinivasan, and Daron Vroon.
CAV 2007, Nineteenth International on Computer Aided Verification, 2007. © Springer
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.
Faster SAT Solving with Better CNF Generation.Benjamin Chambers, Panagiotis Manolios, and Daron Vroon.
DATE: Design, Automation, and Test, Europe, 2009. © ACM
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.