8 Exact Synthesis of ESOP Forms
179
satisfiable if and only if an ESOP form with k (initially k = 1) product terms
that implements the specification exists. The problem is then solved utilizing a SATsolver and, if satisfiable, an ESOP form with k product terms is returned. Otherwise,
if unsatisfiable, k is increased and the synthesis process is restarted. The synthesis
approach is hardly affected by the number of Boolean variables and particularly fast
if the Boolean function can be expressed by using only a few product terms. We
argue that such a SAT-based exact synthesis procedure can be a backbone of a new
generation of heuristic ESOP optimization methods that, instead of relying on cube
transformations applied to a pair of product terms, are capable of optimizing small
subsets (windows) of product terms.
The proposed approach is the first ESOP synthesis technique based on Boolean
satisfiability. We further present a relaxation of the technique to compute ESOP
forms with size close to minimal leveraging the SAT-solver’s conflict limit. We
have implemented SAT-based exact synthesis for ESOPs and the relaxation of the
approach using an off-the-shelf SAT-solver and show in the experiments that SATbased ESOP synthesis can be readily used to synthesize ESOP forms with up to 8
Boolean variables and up to 100 terms. As benchmarks, we use completely specified
Boolean functions that are used as representatives of the NPN4 equivalence
classes [12] as well as completely specified Boolean functions that appeared in
technology mapping using look-up tables (LUTs) with at most 8 inputs (8-LUT
mapping). Moreover, we use a set of randomly generated incompletely specified
Boolean functions with up to 8 Boolean variables.
8.2 Background
Exclusive-or Sum-of-Products (ESOP) Let B = {0, 1} and B 3 = {0, 1, −} with
the third element “−” which denotes don’t care. An ESOP form in n Boolean
variables x 1 , . . . , x n is a Boolean expression
k
j =1
n
i=1
x
l i,j
i
,
(8.1)
where the operators ⊕ and ∧ denote standard addition (XOR) and multiplication
(AND) in the Galois field with two-elements, respectively, each l i,j ∈ B 3 is a
constant and each expression
x
l i,j
i =
⎧
⎪ ⎪ ⎨
⎪ ⎪ ⎩
¯
x i , if l i,j = 0
x i , if l i,j = 1
1, if l i,j = −
(8.2)
179
satisfiable if and only if an ESOP form with k (initially k = 1) product terms
that implements the specification exists. The problem is then solved utilizing a SATsolver and, if satisfiable, an ESOP form with k product terms is returned. Otherwise,
if unsatisfiable, k is increased and the synthesis process is restarted. The synthesis
approach is hardly affected by the number of Boolean variables and particularly fast
if the Boolean function can be expressed by using only a few product terms. We
argue that such a SAT-based exact synthesis procedure can be a backbone of a new
generation of heuristic ESOP optimization methods that, instead of relying on cube
transformations applied to a pair of product terms, are capable of optimizing small
subsets (windows) of product terms.
The proposed approach is the first ESOP synthesis technique based on Boolean
satisfiability. We further present a relaxation of the technique to compute ESOP
forms with size close to minimal leveraging the SAT-solver’s conflict limit. We
have implemented SAT-based exact synthesis for ESOPs and the relaxation of the
approach using an off-the-shelf SAT-solver and show in the experiments that SATbased ESOP synthesis can be readily used to synthesize ESOP forms with up to 8
Boolean variables and up to 100 terms. As benchmarks, we use completely specified
Boolean functions that are used as representatives of the NPN4 equivalence
classes [12] as well as completely specified Boolean functions that appeared in
technology mapping using look-up tables (LUTs) with at most 8 inputs (8-LUT
mapping). Moreover, we use a set of randomly generated incompletely specified
Boolean functions with up to 8 Boolean variables.
8.2 Background
Exclusive-or Sum-of-Products (ESOP) Let B = {0, 1} and B 3 = {0, 1, −} with
the third element “−” which denotes don’t care. An ESOP form in n Boolean
variables x 1 , . . . , x n is a Boolean expression
k
j =1
n
i=1
x
l i,j
i
,
(8.1)
where the operators ⊕ and ∧ denote standard addition (XOR) and multiplication
(AND) in the Galois field with two-elements, respectively, each l i,j ∈ B 3 is a
constant and each expression
x
l i,j
i =
⎧
⎪ ⎪ ⎨
⎪ ⎪ ⎩
¯
x i , if l i,j = 0
x i , if l i,j = 1
1, if l i,j = −
(8.2)