ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cofactor.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#include "espresso.h"
11
13
14
15/*
16 The cofactor of a cover against a cube "c" is a cover formed by the
17 cofactor of each cube in the cover against c. The cofactor of two
18 cubes is null if they are distance 1 or more apart. If they are
19 distance zero apart, the cofactor is the restriction of the cube
20 to the minterms of c.
21
22 The cube list contains the following information:
23
24 T[0] = pointer to a cube identifying the variables that have
25 been cofactored against
26 T[1] = pointer to just beyond the sentinel (i.e., T[n] in this case)
27 T[2]
28 .
29 . = pointers to cubes
30 .
31 T[n-2]
32 T[n-1] = NULL pointer (sentinel)
33
34
35 Cofactoring involves repeated application of "cdist0" to check if a
36 cube of the cover intersects the cofactored cube. This can be
37 slow, especially for the recursive descent of the espresso
38 routines. Therefore, a special cofactor routine "scofactor" is
39 provided which assumes the cofactor is only in a single variable.
40*/
41
42
43/* cofactor -- compute the cofactor of a cover with respect to a cube */
45IN pcube *T;
46IN register pcube c;
47{
48 pcube temp = cube.temp[0], *Tc_save, *Tc, *T1;
49 register pcube p;
50 int listlen;
51
52 listlen = CUBELISTSIZE(T) + 5;
53
54 /* Allocate a new list of cube pointers (max size is previous size) */
55 Tc_save = Tc = ALLOC(pcube, listlen);
56
57 /* pass on which variables have been cofactored against */
58 *Tc++ = set_or(new_cube(), T[0], set_diff(temp, cube.fullset, c));
59 Tc++;
60
61 /* Loop for each cube in the list, determine suitability, and save */
62 for(T1 = T+2; (p = *T1++) != NULL; ) {
63 if (p != c) {
64
65#ifdef NO_INLINE
66 if (! cdist0(p, c)) goto false;
67#else
68 {register int w,last;register unsigned int x;if((last=cube.inword)!=-1)
69 {x=p[last]&c[last];if(~(x|x>>1)&cube.inmask)goto false;for(w=1;w<last;w++)
70 {x=p[w]&c[w];if(~(x|x>>1)&DISJOINT)goto false;}}}{register int w,var,last;
71 register pcube mask;for(var=cube.num_binary_vars;var<cube.num_vars;var++){
72 mask=cube.var_mask[var];last=cube.last_word[var];for(w=cube.first_word[var
73 ];w<=last;w++)if(p[w]&c[w]&mask[w])goto nextvar;goto false;nextvar:;}}
74#endif
75
76 *Tc++ = p;
77 false: ;
78 }
79 }
80
81 *Tc++ = (pcube) NULL; /* sentinel */
82 Tc_save[1] = (pcube) Tc; /* save pointer to last */
83 return Tc_save;
84}
85
86/*
87 scofactor -- compute the cofactor of a cover with respect to a cube,
88 where the cube is "active" in only a single variable.
89
90 This routine has been optimized for speed.
91*/
92
93pcube *scofactor(T, c, var)
94IN pcube *T, c;
95IN int var;
96{
97 pcube *Tc, *Tc_save;
98 register pcube p, mask = cube.temp[1], *T1;
99 register int first = cube.first_word[var], last = cube.last_word[var];
100 int listlen;
101
102 listlen = CUBELISTSIZE(T) + 5;
103
104 /* Allocate a new list of cube pointers (max size is previous size) */
105 Tc_save = Tc = ALLOC(pcube, listlen);
106
107 /* pass on which variables have been cofactored against */
108 *Tc++ = set_or(new_cube(), T[0], set_diff(mask, cube.fullset, c));
109 Tc++;
110
111 /* Setup for the quick distance check */
112 (void) set_and(mask, cube.var_mask[var], c);
113
114 /* Loop for each cube in the list, determine suitability, and save */
115 for(T1 = T+2; (p = *T1++) != NULL; )
116 if (p != c) {
117 register int i = first;
118 do
119 if (p[i] & mask[i]) {
120 *Tc++ = p;
121 break;
122 }
123 while (++i <= last);
124 }
125
126 *Tc++ = (pcube) NULL; /* sentinel */
127 Tc_save[1] = (pcube) Tc; /* save pointer to last */
128 return Tc_save;
129}
130
132IN pcube *T;
133{
134 int *count = cdata.part_zeros;
135 pcube *T1;
136
137 /* Clear the column counts (count of # zeros in each column) */
138 { register int i;
139 for(i = cube.size - 1; i >= 0; i--)
140 count[i] = 0;
141 }
142
143 /* Count the number of zeros in each column */
144 { register int i, *cnt;
145 register unsigned int val;
146 register pcube p, cof = T[0], full = cube.fullset;
147 for(T1 = T+2; (p = *T1++) != NULL; )
148 for(i = LOOP(p); i > 0; i--)
149 if ((val = full[i] & ~ (p[i] | cof[i]))) {
150 cnt = count + ((i-1) << LOGBPI);
151#if BPI == 32
152 if (val & 0xFF000000) {
153 if (val & 0x80000000) cnt[31]++;
154 if (val & 0x40000000) cnt[30]++;
155 if (val & 0x20000000) cnt[29]++;
156 if (val & 0x10000000) cnt[28]++;
157 if (val & 0x08000000) cnt[27]++;
158 if (val & 0x04000000) cnt[26]++;
159 if (val & 0x02000000) cnt[25]++;
160 if (val & 0x01000000) cnt[24]++;
161 }
162 if (val & 0x00FF0000) {
163 if (val & 0x00800000) cnt[23]++;
164 if (val & 0x00400000) cnt[22]++;
165 if (val & 0x00200000) cnt[21]++;
166 if (val & 0x00100000) cnt[20]++;
167 if (val & 0x00080000) cnt[19]++;
168 if (val & 0x00040000) cnt[18]++;
169 if (val & 0x00020000) cnt[17]++;
170 if (val & 0x00010000) cnt[16]++;
171 }
172#endif
173 if (val & 0xFF00) {
174 if (val & 0x8000) cnt[15]++;
175 if (val & 0x4000) cnt[14]++;
176 if (val & 0x2000) cnt[13]++;
177 if (val & 0x1000) cnt[12]++;
178 if (val & 0x0800) cnt[11]++;
179 if (val & 0x0400) cnt[10]++;
180 if (val & 0x0200) cnt[ 9]++;
181 if (val & 0x0100) cnt[ 8]++;
182 }
183 if (val & 0x00FF) {
184 if (val & 0x0080) cnt[ 7]++;
185 if (val & 0x0040) cnt[ 6]++;
186 if (val & 0x0020) cnt[ 5]++;
187 if (val & 0x0010) cnt[ 4]++;
188 if (val & 0x0008) cnt[ 3]++;
189 if (val & 0x0004) cnt[ 2]++;
190 if (val & 0x0002) cnt[ 1]++;
191 if (val & 0x0001) cnt[ 0]++;
192 }
193 }
194 }
195
196 /*
197 * Perform counts for each variable:
198 * cdata.var_zeros[var] = number of zeros in the variable
199 * cdata.parts_active[var] = number of active parts for each variable
200 * cdata.vars_active = number of variables which are active
201 * cdata.vars_unate = number of variables which are active and unate
202 *
203 * best -- the variable which is best for splitting based on:
204 * mostactive -- most # active parts in any variable
205 * mostzero -- most # zeros in any variable
206 * mostbalanced -- minimum over the maximum # zeros / part / variable
207 */
208
209 { register int var, i, lastbit, active, maxactive;
210 int best = -1, mostactive = 0, mostzero = 0, mostbalanced = 32000;
211 cdata.vars_unate = cdata.vars_active = 0;
212
213 for(var = 0; var < cube.num_vars; var++) {
214 if (var < cube.num_binary_vars) { /* special hack for binary vars */
215 i = count[var*2];
216 lastbit = count[var*2 + 1];
217 active = (i > 0) + (lastbit > 0);
218 cdata.var_zeros[var] = i + lastbit;
219 maxactive = MAX(i, lastbit);
220 } else {
221 maxactive = active = cdata.var_zeros[var] = 0;
222 lastbit = cube.last_part[var];
223 for(i = cube.first_part[var]; i <= lastbit; i++) {
224 cdata.var_zeros[var] += count[i];
225 active += (count[i] > 0);
226 if (active > maxactive) maxactive = active;
227 }
228 }
229
230 /* first priority is to maximize the number of active parts */
231 /* for binary case, this will usually select the output first */
232 if (active > mostactive)
233 best = var, mostactive = active, mostzero = cdata.var_zeros[best],
234 mostbalanced = maxactive;
235 else if (active == mostactive)
236 {
237 /* secondary condition is to maximize the number zeros */
238 /* for binary variables, this is the same as minimum # of 2's */
239 if (cdata.var_zeros[var] > mostzero)
240 best = var, mostzero = cdata.var_zeros[best],
241 mostbalanced = maxactive;
242 else if (cdata.var_zeros[var] == mostzero)
243 /* third condition is to pick a balanced variable */
244 /* for binary vars, this means roughly equal # 0's and 1's */
245 if (maxactive < mostbalanced)
246 best = var, mostbalanced = maxactive;
247 }
248
249 cdata.parts_active[var] = active;
250 cdata.is_unate[var] = (active == 1);
251 cdata.vars_active += (active > 0);
252 cdata.vars_unate += (active == 1);
253 }
254 cdata.best = best;
255 }
256}
257
258int binate_split_select(T, cleft, cright, debug_flag)
259IN pcube *T;
260IN register pcube cleft, cright;
261IN int debug_flag;
262{
263 int best = cdata.best;
264 register int i, lastbit = cube.last_part[best], halfbit = 0;
265 register pcube cof=T[0];
266
267 /* Create the cubes to cofactor against */
268 (void) set_diff(cleft, cube.fullset, cube.var_mask[best]);
269 (void) set_diff(cright, cube.fullset, cube.var_mask[best]);
270 for(i = cube.first_part[best]; i <= lastbit; i++)
271 if (! is_in_set(cof,i))
272 halfbit++;
273 for(i = cube.first_part[best], halfbit = halfbit/2; halfbit > 0; i++)
274 if (! is_in_set(cof,i))
275 halfbit--, set_insert(cleft, i);
276 for(; i <= lastbit; i++)
277 if (! is_in_set(cof,i))
278 set_insert(cright, i);
279
280 if (debug & debug_flag) {
281 (void) printf("BINATE_SPLIT_SELECT: split against %d\n", best);
282 if (verbose_debug)
283 (void) printf("cl=%s\ncr=%s\n", pc1(cleft), pc2(cright));
284 }
285 return best;
286}
287
288
290pcover A;
291{
292 register pcube last, p, *plist, *list;
293
294 list = plist = ALLOC(pcube, A->count + 3);
295 *plist++ = new_cube();
296 plist++;
297 foreach_set(A, last, p) {
298 *plist++ = p;
299 }
300 *plist++ = NULL; /* sentinel */
301 list[1] = (pcube) plist;
302 return list;
303}
304
305
307pcover A, B;
308{
309 register pcube last, p, *plist, *list;
310
311 list = plist = ALLOC(pcube, A->count + B->count + 3);
312 *plist++ = new_cube();
313 plist++;
314 foreach_set(A, last, p) {
315 *plist++ = p;
316 }
317 foreach_set(B, last, p) {
318 *plist++ = p;
319 }
320 *plist++ = NULL;
321 list[1] = (pcube) plist;
322 return list;
323}
324
325
327pcover A, B, C;
328{
329 register pcube last, p, *plist, *list;
330
331 plist = ALLOC(pcube, A->count + B->count + C->count + 3);
332 list = plist;
333 *plist++ = new_cube();
334 plist++;
335 foreach_set(A, last, p) {
336 *plist++ = p;
337 }
338 foreach_set(B, last, p) {
339 *plist++ = p;
340 }
341 foreach_set(C, last, p) {
342 *plist++ = p;
343 }
344 *plist++ = NULL;
345 list[1] = (pcube) plist;
346 return list;
347}
348
349
351pcube *A1;
352{
353 register int i;
354 register pcube p, pdest, cof = A1[0];
355 register pcover A;
356
357 A = new_cover(CUBELISTSIZE(A1));
358 for(i = 2; (p = A1[i]) != NULL; i++) {
359 pdest = GETSET(A, i-2);
360 INLINEset_or(pdest, p, cof);
361 }
362 A->count = CUBELISTSIZE(A1);
363 return A;
364}
365
367pcube *T;
368{
369 register pcube *Tdest;
370 register int i, ncubes;
371
372 (void) set_copy(cube.temp[0], T[0]); /* retrieve cofactor */
373
374 ncubes = CUBELISTSIZE(T);
375 qsort((char *) (T+2), (size_t)ncubes, sizeof(pset), (int (*)()) d1_order);
376
377 Tdest = T+2;
378 /* *Tdest++ = T[2]; */
379 for(i = 3; i < ncubes; i++) {
380 if (d1_order(&T[i-1], &T[i]) != 0) {
381 *Tdest++ = T[i];
382 }
383 }
384
385 *Tdest++ = NULL; /* sentinel */
386 Tdest[1] = (pcube) Tdest; /* save pointer to last */
387}
389
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define ALLOC(type, num)
Definition avl.h:27
#define MAX(a, b)
Definition avl.h:23
void simplify_cubelist(pcube *T)
Definition cofactor.c:366
#define pcover
Definition espresso.h:264
#define new_cube()
Definition espresso.h:262
char * pc1()
#define DISJOINT
Definition espresso.h:514
#define INLINEset_or(r, a, b)
Definition espresso.h:205
pcube * scofactor()
int d1_order()
#define is_in_set(set, e)
Definition espresso.h:170
#define set_insert(set, e)
Definition espresso.h:172
pset set_and()
pcube * cube2list()
pcover cubeunlist()
void massive_count()
#define pcube
Definition espresso.h:261
ABC_NAMESPACE_HEADER_END int binate_split_select()
#define LOOP(set)
Definition espresso.h:104
#define GETSET(family, index)
Definition espresso.h:161
pset set_diff()
#define LOGBPI
Definition espresso.h:69
char * pc2()
#define foreach_set(R, last, p)
Definition espresso.h:135
pcube * cofactor()
pcube * cube3list()
unsigned int debug
Definition globals.c:19
bool verbose_debug
Definition globals.c:20
#define IN
Definition espresso.h:332
unsigned int * pset
Definition espresso.h:73
pset set_or()
bool cdist0()
pset set_copy()
#define CUBELISTSIZE(T)
Definition espresso.h:329
pcube * cube1list()
#define new_cover(i)
Definition espresso.h:265
Cube * p
Definition exorList.c:222
Definition exor.h:123