You are here

Boolean Functions: From Logical Circuits To Prime Ideals Via Decision Diagrams

Team and supervisors
Department / Team: 
Team Web Site: 
https://team.inria.fr/hycomes/
PhD Director
Benoit Caillaud
Co-director(s), co-supervisor(s)
Khalil Ghorbal
Contact(s)
NameEmail address
Khalil Ghorbal
khalil.ghorbal@inria.fr
PhD subject
Abstract

1. *Context*

Boolean functions (or systems of them) are a central object of study in different, seemingly unrelated, fields.
In computer science, their encoding motivated a very versatile data structure known as Binary Decision Diagrams (BDD). BDD are ubiquitous and their use extended far beyond computer science. It suffices perhaps to say that Bryant’s original paper [2], introducing the first canonical decision diagram, has over 11000 citations (and counting).
In hardware design, the synthesis and optimization of electronic circuits (chips) largely rely on their logical counterparts, so called logical circuits (net- works of logic gates), which can be regarded as systems of Boolean functions. Interestingly, the underlying data structure commonly used to represent logical circuits is AND-Invert Graph [5], which is also, per its name, also a graph-based structure. It has numerous advantages pertaining to its simplicity. Firstly, it uses the AND operator as the main binary operator, and secondly, it doesn’t require any particular ordering on the variables. This sharply contrasts with BDD, which uses the Shannon operator and requires that all paths of the graph respect the same variable ordering. The conversion of a circuit to an AIG scales very well while avoiding unpredictable size increase. It also permits an efficient local manipulations which makes it very suitable for circuit optimization and synthesis. Conjunctive Normal Forms (CNF) are yet another normal form often used to canonically represent systems of Boolean functions. The recent advances of CNF-based SAT solvers, especially with the advent of clause learning, was a game changer to find concrete counter examples falsifying the equivalence of memory-less (or combinatorial) circuits, before and after the optimization pro- cess, at a very large scale. Despite those outstanding advances, the need for a proof (or certificate) of equivalence, as well as the verification of circuits with memory (introducing quantifiers) still a serious challenge both theoretically and practically. An important effort (time and money) are today invested by micro- electronics’ companies to test (in the classical sense) whether the final optimized circuits satisfy their original specification.
Now putting the hat of a mathematician, following Galois’ insights, studying the relations between roots of systems of equations has proved to be a fertile point of view that has lead to uncover deep connections between geometry and algebra. As such, a system of Boolean functions is an algebraic encoding for a discrete geometric object. Several theories have been developed and successfully used to check for the existence of solutions or counting their numbers. Let us for instance mention that Gr ̈obner bases [3], implemented in most computer algebra systems, serve primarily to effectively check for the emptiness of the set of solutions of a system of polynomial equations exhibiting in a finite number of steps a certificate in case of emptiness.
To summarize, this leaves us with one central object, a system of Boolean functions, and (at least) three different ways to tackle it, from rather different angles and using, at a first sight at least, quite different toolboxes.

2. *Thesis*

The thesis ambitions to uncover potential bridges between:
• Binary Decision Diagrams, the several existing variants and their related reduction rules,
• AND-Invert Graphs and their various highly efficient local optimization heuristics,
• Radical ideals (or prime ideal decomposition) over finite fields, and their underlying algebraic structure.
Our hope is to benefit from the different angles at which the same object has been treated. For instance, we already observed that a (global) invariant in its usual algebraic sense can be captured by a (local) reduction rule in the sense of BDD. How to translate the invariant to the rule or vice versa remains however not really well understood.
The first step will consist in better understanding two particular canoni- cal variants of BDD, namely, the original one introduced by Bryant (together with its negation output variant), and Minato’s Zero Suppressed Decision Dia- gram [6], (ZDD), which is more suitable for sparse Boolean functions. Currently, one cannot merge easily both variants. For instance, the negation output can- not be added to ZDD without decompressing and compressing back the entire structure. This is not only time and memory consuming, the uncompressed structure might not preserve the same sparsity structure that benefited the non negated one. We believe, at the right level of abstraction, one can actually define an abstract data structure that is both suitable for dense and sparse functions. Ideally, we would like our abstract representation to fuse on one hand the Disjoint Support Decomposition (DSD) representation [1], while, on the other hand, capturing all linear invariants (PNP-Invariants) following [4].
The second step will consist in better understanding the optimization heuris- tics used in hardware design in order to attempt to build a parallel (if any) with reducing the abstract BDD we mentioned in the first step or to transfer such transformation in the BDD world.

Along the road, we hope to tackle the variable ordering problem. This problem, common to BDD and to radical ideals computation, consists in finding an adequate ordering for the size of the BDD and the intermediate computations, respectively, to remain tractable.
Symbolic computations, despite their numerous advantages and usefulness in a variety of domains suffer greatly from their computational cost. They are often traded fro less accurate, yet very fast, numerical approximations which benefit from a well adapted hardware design. Our ultimate goal is to design both the data structures and the underlying hardware to make symbolic computations as affordable and effective as the their numerical counter parts.

Bibliography

[1] Valeria Maria Bertacco. Achieving Scalable Hardware Verification with Sym- bolic Simulation. PhD thesis, Stanford University, Stanford, CA, USA, 2003.

[2] Randal E. Bryant. Graph-based algorithms for boolean function manipula- tion. IEEE Trans. Comput., 35(8):677–691, August 1986.

[3] Bruno Buchberger. Bruno buchberger’s PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Journal of Symbolic Computation, 41(3-4):475–511, mar 2006.

[4] Jerry R. Burch and David E. Long. Efficient boolean function matching. In
Proceedings of the 1992 IEEE/ACM International Conference on Computer- aided Design, ICCAD ’92, pages 408–411, Los Alamitos, CA, USA, 1992. IEEE Computer Society Press.

[5] Leo Hellerman. A catalog of three-variable or-invert and and-invert logical circuits. IEEE Transactions on Electronic Computers, EC-12(3):198–223, jun 1963.

[6] Shin-ichi Minato. Zero-suppressed BDDs for Set Manipulation in Combina- torial Problems. In Proceedings of the 30th International Design Automation Conference, DAC ’93, pages 272–277, New York, NY, USA, 1993. ACM.

Work start date: 
Septembre 2019
Keywords: 
Boolean Functions, Decision diagrams, Logical circuits, Prime ideals, Finite fields
Place: 
IRISA - Campus universitaire de Beaulieu, Rennes