ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
reduce.c
Go to the documentation of this file.
1/*
2 * Revision Control Information
3 *
4 * $Source$
5 * $Author$
6 * $Revision$
7 * $Date$
8 *
9 */
10/*
11 module: reduce.c
12 purpose: Perform the Espresso-II reduction step
13
14 Reduction is a technique used to explore larger regions of the
15 optimization space. We replace each cube of F with a smaller
16 cube while still maintaining a cover of the same logic function.
17*/
18
19#include "espresso.h"
20
22
23
24static bool toggle = TRUE;
25
26
27/*
28 reduce -- replace each cube in F with its reduction
29
30 The reduction of a cube is the smallest cube contained in the cube
31 which can replace the cube in the original cover without changing
32 the cover. This is equivalent to the super cube of all of the
33 essential points in the cube. This can be computed directly.
34
35 The problem is that the order in which the cubes are reduced can
36 greatly affect the final result. We alternate between two ordering
37 strategies:
38
39 (1) Order the cubes in ascending order of distance from the
40 largest cube breaking ties by ordering cubes of equal distance
41 in descending order of size (sort_reduce)
42
43 (2) Order the cubes in descending order of the inner-product of
44 the cube and the column sums (mini_sort)
45
46 The real workhorse of this section is the routine SCCC which is
47 used to find the Smallest Cube Containing the Complement of a cover.
48 Reduction as proposed by Espresso-II takes a cube and computes its
49 maximal reduction as the intersection between the cube and the
50 smallest cube containing the complement of (F u D - {c}) cofactored
51 against c.
52
53 As usual, the unate-recursive paradigm is used to compute SCCC.
54 The SCCC of a unate cover is trivial to compute, and thus we perform
55 Shannon Cofactor expansion attempting to drive the cover to be unate
56 as fast as possible.
57*/
58
61IN pcover D;
62{
63 register pcube last, p, cunder, *FD;
64
65 /* Order the cubes */
67 F = random_order(F);
68 else {
69 F = toggle ? sort_reduce(F) : mini_sort(F, descend);
70 toggle = ! toggle;
71 }
72
73 /* Try to reduce each cube */
74 FD = cube2list(F, D);
75 foreach_set(F, last, p) {
76 cunder = reduce_cube(FD, p); /* reduce the cube */
77 if (setp_equal(cunder, p)) { /* see if it actually did */
78 SET(p, ACTIVE); /* cube remains active */
79 SET(p, PRIME); /* cube remains prime ? */
80 } else {
81 if (debug & REDUCE) {
82 printf("REDUCE: %s to %s %s\n",
83 pc1(p), pc2(cunder), print_time(ptime()));
84 }
85 set_copy(p, cunder); /* save reduced version */
86 RESET(p, PRIME); /* cube is no longer prime */
87 if (setp_empty(cunder))
88 RESET(p, ACTIVE); /* if null, kill the cube */
89 else
90 SET(p, ACTIVE); /* cube is active */
91 }
92 free_cube(cunder);
93 }
94 free_cubelist(FD);
95
96 /* Delete any cubes of F which reduced to the empty cube */
97 return sf_inactive(F);
98}
99
100/* reduce_cube -- find the maximal reduction of a cube */
102IN pcube *FD, p;
103{
104 pcube cunder;
105
106 cunder = sccc(cofactor(FD, p));
107 return set_and(cunder, cunder, p);
108}
109
110
111/* sccc -- find Smallest Cube Containing the Complement of a cover */
113INOUT pcube *T; /* T will be disposed of */
114{
115 pcube r;
116 register pcube cl, cr;
117 register int best;
118 static int sccc_level = 0;
119
120 if (debug & REDUCE1) {
121 debug_print(T, "SCCC", sccc_level++);
122 }
123
124 if (sccc_special_cases(T, &r) == MAYBE) {
125 cl = new_cube();
126 cr = new_cube();
127 best = binate_split_select(T, cl, cr, REDUCE1);
128 r = sccc_merge(sccc(scofactor(T, cl, best)),
129 sccc(scofactor(T, cr, best)), cl, cr);
130 free_cubelist(T);
131 }
132
133 if (debug & REDUCE1)
134 printf("SCCC[%d]: result is %s\n", --sccc_level, pc1(r));
135 return r;
136}
137
138
139pcube sccc_merge(left, right, cl, cr)
140INOUT register pcube left, right; /* will be disposed of ... */
141INOUT register pcube cl, cr; /* will be disposed of ... */
142{
143 INLINEset_and(left, left, cl);
144 INLINEset_and(right, right, cr);
145 INLINEset_or(left, left, right);
146 free_cube(right);
147 free_cube(cl);
148 free_cube(cr);
149 return left;
150}
151
152
153/*
154 sccc_cube -- find the smallest cube containing the complement of a cube
155
156 By DeMorgan's law and the fact that the smallest cube containing a
157 cover is the "or" of the positional cubes, it is simple to see that
158 the SCCC is the universe if the cube has more than two active
159 variables. If there is only a single active variable, then the
160 SCCC is merely the bitwise complement of the cube in that
161 variable. A last special case is no active variables, in which
162 case the SCCC is empty.
163
164 This is "anded" with the incoming cube result.
165*/
167register pcube result, p;
168{
169 register pcube temp=cube.temp[0], mask;
170 int var;
171
172 if ((var = cactive(p)) >= 0) {
173 mask = cube.var_mask[var];
174 INLINEset_xor(temp, p, mask);
175 INLINEset_and(result, result, temp);
176 }
177 return result;
178}
179
180/*
181 * sccc_special_cases -- check the special cases for sccc
182 */
183
184bool sccc_special_cases(T, result)
185INOUT pcube *T; /* will be disposed if answer is determined */
186OUT pcube *result; /* returned only if answer determined */
187{
188 register pcube *T1, p, temp = cube.temp[1], ceil, cof = T[0];
189 pcube *A, *B;
190
191 /* empty cover => complement is universe => SCCC is universe */
192 if (T[2] == NULL) {
193 *result = set_save(cube.fullset);
194 free_cubelist(T);
195 return TRUE;
196 }
197
198 /* row of 1's => complement is empty => SCCC is empty */
199 for(T1 = T+2; (p = *T1++) != NULL; ) {
200 if (full_row(p, cof)) {
201 *result = new_cube();
202 free_cubelist(T);
203 return TRUE;
204 }
205 }
206
207 /* Collect column counts, determine unate variables, etc. */
208 massive_count(T);
209
210 /* If cover is unate (or single cube), apply simple rules to find SCCCU */
211 if (cdata.vars_unate == cdata.vars_active || T[3] == NULL) {
212 *result = set_save(cube.fullset);
213 for(T1 = T+2; (p = *T1++) != NULL; ) {
214 (void) sccc_cube(*result, set_or(temp, p, cof));
215 }
216 free_cubelist(T);
217 return TRUE;
218 }
219
220 /* Check for column of 0's (which can be easily factored( */
221 ceil = set_save(cof);
222 for(T1 = T+2; (p = *T1++) != NULL; ) {
223 INLINEset_or(ceil, ceil, p);
224 }
225 if (! setp_equal(ceil, cube.fullset)) {
226 *result = sccc_cube(set_save(cube.fullset), ceil);
227 if (setp_equal(*result, cube.fullset)) {
228 free_cube(ceil);
229 } else {
230 *result = sccc_merge(sccc(cofactor(T,ceil)),
231 set_save(cube.fullset), ceil, *result);
232 }
233 free_cubelist(T);
234 return TRUE;
235 }
236 free_cube(ceil);
237
238 /* Single active column at this point => tautology => SCCC is empty */
239 if (cdata.vars_active == 1) {
240 *result = new_cube();
241 free_cubelist(T);
242 return TRUE;
243 }
244
245 /* Check for components */
246 if (cdata.var_zeros[cdata.best] < CUBELISTSIZE(T)/2) {
247 if (cubelist_partition(T, &A, &B, debug & REDUCE1) == 0) {
248 return MAYBE;
249 } else {
250 free_cubelist(T);
251 *result = sccc(A);
252 ceil = sccc(B);
253 (void) set_and(*result, *result, ceil);
254 set_free(ceil);
255 return TRUE;
256 }
257 }
258
259 /* Not much we can do about it */
260 return MAYBE;
261}
263
#define TRUE
Definition abcBm.c:38
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define pcover
Definition espresso.h:264
#define new_cube()
Definition espresso.h:262
bool full_row()
char * pc1()
#define set_save(r)
Definition espresso.h:166
#define INLINEset_or(r, a, b)
Definition espresso.h:205
#define REDUCE1
Definition espresso.h:358
pset_family sf_inactive()
pcube * scofactor()
pcube sccc()
#define set_free(r)
Definition espresso.h:167
#define INLINEset_xor(r, a, b)
Definition espresso.h:218
#define ACTIVE
Definition espresso.h:129
pset set_and()
bool sccc_special_cases()
#define print_time(t)
Definition espresso.h:22
pcover random_order()
pcube * cube2list()
void debug_print()
pcover mini_sort()
void massive_count()
#define INOUT
Definition espresso.h:334
pcube sccc_merge()
pcover sort_reduce()
#define pcube
Definition espresso.h:261
ABC_NAMESPACE_HEADER_END int binate_split_select()
#define REDUCE
Definition espresso.h:357
#define free_cube(r)
Definition espresso.h:263
char * pc2()
pcover reduce()
#define foreach_set(R, last, p)
Definition espresso.h:135
pcube * cofactor()
unsigned int debug
Definition globals.c:19
#define SET(set, flag)
Definition espresso.h:122
pcube reduce_cube()
bool setp_empty()
#define INLINEset_and(r, a, b)
Definition espresso.h:202
#define IN
Definition espresso.h:332
#define RESET(set, flag)
Definition espresso.h:123
#define PRIME
Definition espresso.h:127
int cubelist_partition()
bool use_random_order
Definition globals.c:38
pset set_or()
bool setp_equal()
pcube sccc_cube()
pset set_copy()
#define free_cubelist(T)
Definition espresso.h:267
#define OUT
Definition espresso.h:333
#define CUBELISTSIZE(T)
Definition espresso.h:329
int cactive()
#define MAYBE
Definition espresso.h:257
Cube * p
Definition exorList.c:222
Definition exor.h:123
#define ptime()
Definition util_old.h:283