190
H. Riener et al.
Table 8.1 Synthesis of ESOP forms for LUT mapping
Fixed-size
Downward search
Upward search
Terms R
C
k
T
R
C
k
T
R
C
k
T
8
3735 266 5.19 49.65 s 3854 147 3.60 300.44 s 3857 3854 3.60 248.07 s
16
3806 195 7.10 50.56 s 3965 36 3.82 695.08 s 3965
36 3.82 338.72 s
32
3966 35 8.45 42.67s 4001
0 3.94 1430.41s 4001
0 3.94 355.49 s
0
1
2
3
4
5
6
7
8
9
1 0
1 1
1 2
1 3
1 4
1 5
1 6
10
1
10
2
10
3
10
4
10
5
Fig. 8.5 SAT-solver results for different k for 0xF550311031100000
parts. The first part (fixed-size) is dedicated to synthesis of an ESOP form for
the given term limit (without minimizing the number of terms). In this case, the
SAT-solver’s heuristics decides whether unnecessary terms are canceled or kept.
The second part (downward search) is dedicated to a synthesis procedure that
iteratively synthesizes ESOP forms starting from the upper term limit and decreases
the number of terms until the constraint system becomes unsatisfiable (as described
in Algorithm 4). The satisfying assignment with the smallest number of terms
is used for deriving an ESOP form. The last part (upward search) is similar to
the second part, but starts with 1 term and increases the number if the constraint
system is unsatisfiable. The satisfying assignment with the largest number of terms
is used to derive an ESOP form. For each part, we list the number of Boolean
functions successfully realized (R), the number of Boolean functions that could
not be synthesized because the SAT-solver’s conflict limit (C) was exceeded, the
average number of terms (k) for all realizable Boolean functions, and the total
runtime (T) for synthesizing all Boolean functions. The runtime includes the time
for synthesizing the realizable Boolean function and the time spent in unsuccessful
synthesis attempts.
Example 8.2 We illustrate the effect of the conflict limit on upward and downward
search with a simple example. Consider the completely specified Boolean function
0xF550311031100000. We attempt to synthesize an ESOP form of minimal
size with at most 16 terms and a conflict limit of 10,000 using the upward and
downward search procedures, respectively. Figure 8.5 shows the number of conflicts
explored by the SAT-solver in logarithmic scale parameterized by the number of
H. Riener et al.
Table 8.1 Synthesis of ESOP forms for LUT mapping
Fixed-size
Downward search
Upward search
Terms R
C
k
T
R
C
k
T
R
C
k
T
8
3735 266 5.19 49.65 s 3854 147 3.60 300.44 s 3857 3854 3.60 248.07 s
16
3806 195 7.10 50.56 s 3965 36 3.82 695.08 s 3965
36 3.82 338.72 s
32
3966 35 8.45 42.67s 4001
0 3.94 1430.41s 4001
0 3.94 355.49 s
0
1
2
3
4
5
6
7
8
9
1 0
1 1
1 2
1 3
1 4
1 5
1 6
10
1
10
2
10
3
10
4
10
5
Fig. 8.5 SAT-solver results for different k for 0xF550311031100000
parts. The first part (fixed-size) is dedicated to synthesis of an ESOP form for
the given term limit (without minimizing the number of terms). In this case, the
SAT-solver’s heuristics decides whether unnecessary terms are canceled or kept.
The second part (downward search) is dedicated to a synthesis procedure that
iteratively synthesizes ESOP forms starting from the upper term limit and decreases
the number of terms until the constraint system becomes unsatisfiable (as described
in Algorithm 4). The satisfying assignment with the smallest number of terms
is used for deriving an ESOP form. The last part (upward search) is similar to
the second part, but starts with 1 term and increases the number if the constraint
system is unsatisfiable. The satisfying assignment with the largest number of terms
is used to derive an ESOP form. For each part, we list the number of Boolean
functions successfully realized (R), the number of Boolean functions that could
not be synthesized because the SAT-solver’s conflict limit (C) was exceeded, the
average number of terms (k) for all realizable Boolean functions, and the total
runtime (T) for synthesizing all Boolean functions. The runtime includes the time
for synthesizing the realizable Boolean function and the time spent in unsuccessful
synthesis attempts.
Example 8.2 We illustrate the effect of the conflict limit on upward and downward
search with a simple example. Consider the completely specified Boolean function
0xF550311031100000. We attempt to synthesize an ESOP form of minimal
size with at most 16 terms and a conflict limit of 10,000 using the upward and
downward search procedures, respectively. Figure 8.5 shows the number of conflicts
explored by the SAT-solver in logarithmic scale parameterized by the number of