Libraries related to representing and processing Boolean functions, geared toward large-scale automatic reasoning, e.g., via SAT solving and AIG or BDD packages.
Introduction
Boolean functions
are widely useful throughout mathematical logic, computer science, and computer engineering. In formal verification, they are especially interesting because many high-capacity, fully automatic techniques are known for analyzing, comparing, and simplifying them; for instance, see binary decision diagrams (bdds), SAT solvers, and-inverter graphs (aigs), model checking, equivalence checking, and so forth.
Libraries for Boolean Functions
We have developed some libraries for working with Boolean functions, for instance:
- satlink provides a representation of conjunctive normal form formulas and a way to call SAT solvers from ACL2 and trust their results.
- Libraries like aig and ubdds provide hons-based AIG and BDD packages.
- aignet provides a more efficient, stobj-based AIG representation similar to that used by ABC.
These libraries are important groundwork for the gl framework for bit-blasting ACL2 theorems, and may be of interest to anyone who is trying to develop new, automatic tools or proof techniques.
Libraries for Four-Valued Logic
Being able to process large-scale Boolean functions is especially important in hardware-verification. But actually, here, to model certain circuits and to implement certain algorithms, it can be useful to go beyond Boolean functions and consider a richer logic.
You might call Boolean functions or Boolean logic a two-valued logic, since there are just two values (true and false) that any variable can take. It is often useful to add a third value, usually called X, to represent an "unknown" value. In some systems, a fourth value, Z, is added to represent an undriven wire. For more on this, see why-4v-logic.
We have developed two libraries to support working in four-valued logic. Of these, the 4v library is somewhat higher level and is generally simpler and more convenient to work with. It serves as the basis of the esim hardware simulator. Meanwhile, the faig library is a bit lower-level and does not enjoy the very nice 4v-monotonicity property of 4v-sexprs. On the other hand, faigs are closer to aigs, and can be useful for loading expressions into aignet or satlink.
Related Papers
Besides the documentation here, you may find the following papers useful:
Jared Davis and Sol Swords. Verified AIG Algorithms in ACL2. In ACL2 Workshop 2013. May, 2013. EPTCS 114. Pages 95-110.
Sol Swords and Jared Davis. Bit-Blasting ACL2 Theorems. In ACL2 Workshop 2011. November, 2011. EPTCS 70. Pages 84-102.
Sol Swords and Warren A Hunt, Jr. A Mechanically Verified AIG to BDD Conversion Algorithm. In ITP 2010,LNCS 6172, Springer. Pages 435-449.
Subtopics 
- 4v
- An hons-based, s-expression representation of monotonic, four-valued functions.
- Aig
- A hons-based And-Inverter Graph (AIG) library for representing and manipulating Boolean functions.
- Aignet
- An efficient, stobj-based And-Inverter Graph (AIG) representation for Boolean functions and finite-state machines.
- Bdd
- Ordered binary decision diagrams with rewriting
- Bed
- A Hons-based implementation of Boolean Expression Diagrams, described by Anderson and Hulgaard.
- Faig
- A hons-based representation of four-valued functions as pairs of aigs.
- Ipasir
- ACL2 bindings for the ipasir incremental SAT solving interface
- Satlink
- A simple representation for Boolean formulas in conjunctive normal form, and a mechanism for calling SAT solvers from within ACL2 and trusting what they say. (CCL Only)
- Truth
- Library for reasoning about and computing with integer-encoded truth tables.
- Ubdds
- A hons-based, unlabeled Binary Decision Diagram (bdd) representation of Boolean functions.
0 comments:
Post a Comment