|
|
|---|
|
|
|
|---|
Libraries related to representing and processing Boolean functions, geared toward large-scale automatic reasoning, e.g., via SAT solving and AIG or BDD packages.
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.
We have developed some libraries for working with Boolean functions, for instance:
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.
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.
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.