Exact Synthesis of Majority-Inverter Graphs and Its Applications

We propose effective algorithms for exact synthesis of Boolean logic networks using satisfiability modulo theories (SMT) solvers. Since exact synthesis is a difficult problem, it can only be applied efficiently to very small functions, having up to 6 variables. Key in our approach is to use majority-inverter graphs as underlying logic representation as they are simple (homogeneous logic representation) and expressive (contain And/Or-inverter graphs) at the same time. This has a positive impact on the problem formulation: it simplifies the encoding as SMT constraints and also allows for various techniques to break symmetries in the search space due to the regular data structure. Our algorithm optimizes with respect to the MIG’s size or depth and uses different ways to encode the problem and several methods to improve solving time, with symmetry breaking techniques being the most effective ones. We discuss several applications of exact synthesis and motivate them by experiments on a set of large arithmetic benchmarks. Using the proposed techniques, we are able to improve both area and delay after LUT-based technology mapping beyond the current results achieved by state-of-the-art logic synthesis algorithms.

Published in:
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 36, 11, 1842-1855
Piscataway, Ieee-Inst Electrical Electronics Engineers Inc

Note: The status of this file is: EPFL only

 Record created 2017-01-10, last modified 2020-07-29

Download fulltext

Rate this document:

Rate this document:
(Not yet reviewed)