184
H. Riener et al.
Algorithm 4 SAT-based exact synthesis guided by counterexamples
input : a (possibly incompletely-specified) Boolean function f
output: a minimal ESOP r functionally equivalent to f
r ← ;
k ← 1;
ϕ(p, q, z) ← true;
while m ← NotEquivalent(f ,r) do
ϕ ← AddConstraints(ϕ,m);
if ˆ
p, ˆ
q |= SAT(∃z : ϕ(p, q, z)) then
r ← MakeESOP( ˆ
p, ˆ
q);
else
r ← ;
k ← k + 1;
ϕ(p, q, z) ← true;
end
end
return r;
assignment to the intermediate Boolean variables z is for the construction of no
further interest and not returned. Finally, the function MakeESOP constructs an
ESOP form from the assignment ˆ
p and ˆ
q according to the rules described in (8.11).
Note that Algorithm 3 always terminates, but may run out of resources (memory or
time) if the minimal ESOP requires many product terms. Thus in practice usually
an additional termination criterion in form of an upper bound for the size parameter
k or maximum number of conflicts examined by the SAT-solver is provided.
Counterexample-Guided Abstraction-Refinement Algorithm 3 synthesizes
an ESOP form in one step. Alternatively, counterexample-guided abstractionrefinement can be employed as shown in Algorithm 4. The idea of the
abstraction-refinement loop is to iteratively update a candidate ESOP form r
(starting from the empty ESOP form ) until it eventually becomes semantically
equivalent to the Boolean function f to be synthesized. In each iteration, the
constraints of one assignment x = x 1 · · · x n for which r and f evaluate differently
(r(x) = f (x)) are added (AddConstraints) to the constraint satisfaction
problem and r is resynthesized. If ϕ becomes unsatisfiable, then the constraints
cannot be solved within the current restriction to k product terms and k needs to be
relaxed. If f and r are equivalent, i.e., no counterexample x = x 1 · · · x n is found
by NotEquivalent, then r is returned as an ESOP form semantically equivalent
to f . The main advantage of Algorithms 4 over 3 lies in its ability to abstract
from unnecessary constraints which keeps the constraint satisfaction problem as
small as possible. The algorithm is fast mainly because modern backtrack searchbased SAT-solvers support incremental solving [7] and are able to maintain learned
information when new constraints are added to a satisfiability problem. The oracle
NotEquivalent has to be capable of verifying whether a candidate ESOP form
r is functionally equivalent to the Boolean function f . For Boolean functions with
up to 16 Boolean variables, simulation using explicit representations such as truth
H. Riener et al.
Algorithm 4 SAT-based exact synthesis guided by counterexamples
input : a (possibly incompletely-specified) Boolean function f
output: a minimal ESOP r functionally equivalent to f
r ← ;
k ← 1;
ϕ(p, q, z) ← true;
while m ← NotEquivalent(f ,r) do
ϕ ← AddConstraints(ϕ,m);
if ˆ
p, ˆ
q |= SAT(∃z : ϕ(p, q, z)) then
r ← MakeESOP( ˆ
p, ˆ
q);
else
r ← ;
k ← k + 1;
ϕ(p, q, z) ← true;
end
end
return r;
assignment to the intermediate Boolean variables z is for the construction of no
further interest and not returned. Finally, the function MakeESOP constructs an
ESOP form from the assignment ˆ
p and ˆ
q according to the rules described in (8.11).
Note that Algorithm 3 always terminates, but may run out of resources (memory or
time) if the minimal ESOP requires many product terms. Thus in practice usually
an additional termination criterion in form of an upper bound for the size parameter
k or maximum number of conflicts examined by the SAT-solver is provided.
Counterexample-Guided Abstraction-Refinement Algorithm 3 synthesizes
an ESOP form in one step. Alternatively, counterexample-guided abstractionrefinement can be employed as shown in Algorithm 4. The idea of the
abstraction-refinement loop is to iteratively update a candidate ESOP form r
(starting from the empty ESOP form ) until it eventually becomes semantically
equivalent to the Boolean function f to be synthesized. In each iteration, the
constraints of one assignment x = x 1 · · · x n for which r and f evaluate differently
(r(x) = f (x)) are added (AddConstraints) to the constraint satisfaction
problem and r is resynthesized. If ϕ becomes unsatisfiable, then the constraints
cannot be solved within the current restriction to k product terms and k needs to be
relaxed. If f and r are equivalent, i.e., no counterexample x = x 1 · · · x n is found
by NotEquivalent, then r is returned as an ESOP form semantically equivalent
to f . The main advantage of Algorithms 4 over 3 lies in its ability to abstract
from unnecessary constraints which keeps the constraint satisfaction problem as
small as possible. The algorithm is fast mainly because modern backtrack searchbased SAT-solvers support incremental solving [7] and are able to maintain learned
information when new constraints are added to a satisfiability problem. The oracle
NotEquivalent has to be capable of verifying whether a candidate ESOP form
r is functionally equivalent to the Boolean function f . For Boolean functions with
up to 16 Boolean variables, simulation using explicit representations such as truth