ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cofactor.c File Reference
#include "espresso.h"
Include dependency graph for cofactor.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START pcubecofactor (IN pcube *T, IN register pcube c)
 
pcubescofactor (IN pcube *T, IN pcube c, IN int var)
 
void massive_count (IN pcube *T)
 
int binate_split_select (IN pcube *T, IN register pcube cleft, IN register pcube cright, IN int debug_flag)
 
pcubecube1list (pcover A)
 
pcubecube2list (pcover A, pcover B)
 
pcubecube3list (pcover A, pcover B, pcover C)
 
pcover cubeunlist (pcube *A1)
 
void simplify_cubelist (pcube *T)
 

Function Documentation

◆ binate_split_select()

int binate_split_select ( IN pcube * T,
IN register pcube cleft,
IN register pcube cright,
IN int debug_flag )

Definition at line 258 of file cofactor.c.

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}
char * pc1()
#define is_in_set(set, e)
Definition espresso.h:170
#define set_insert(set, e)
Definition espresso.h:172
#define pcube
Definition espresso.h:261
pset set_diff()
char * pc2()
unsigned int debug
Definition globals.c:19
bool verbose_debug
Definition globals.c:20
Definition exor.h:123
Here is the call graph for this function:

◆ cofactor()

ABC_NAMESPACE_IMPL_START pcube * cofactor ( IN pcube * T,
IN register pcube c )

Definition at line 44 of file cofactor.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}
#define ALLOC(type, num)
Definition avl.h:27
#define new_cube()
Definition espresso.h:262
#define DISJOINT
Definition espresso.h:514
pset set_or()
bool cdist0()
#define CUBELISTSIZE(T)
Definition espresso.h:329
Cube * p
Definition exorList.c:222
unsigned short var
Definition giaNewBdd.h:35
Here is the call graph for this function:
Here is the caller graph for this function:

◆ cube1list()

pcube * cube1list ( pcover A)

Definition at line 289 of file cofactor.c.

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}
#define foreach_set(R, last, p)
Definition espresso.h:135

◆ cube2list()

pcube * cube2list ( pcover A,
pcover B )

Definition at line 306 of file cofactor.c.

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}

◆ cube3list()

pcube * cube3list ( pcover A,
pcover B,
pcover C )

Definition at line 326 of file cofactor.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}

◆ cubeunlist()

pcover cubeunlist ( pcube * A1)

Definition at line 350 of file cofactor.c.

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}
#define pcover
Definition espresso.h:264
#define INLINEset_or(r, a, b)
Definition espresso.h:205
#define GETSET(family, index)
Definition espresso.h:161
#define new_cover(i)
Definition espresso.h:265

◆ massive_count()

void massive_count ( IN pcube * T)

Definition at line 131 of file cofactor.c.

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}
#define MAX(a, b)
Definition avl.h:23
#define LOOP(set)
Definition espresso.h:104
#define LOGBPI
Definition espresso.h:69

◆ scofactor()

pcube * scofactor ( IN pcube * T,
IN pcube c,
IN int var )

Definition at line 93 of file cofactor.c.

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}
pset set_and()
Here is the call graph for this function:

◆ simplify_cubelist()

void simplify_cubelist ( pcube * T)

Definition at line 366 of file cofactor.c.

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}
int d1_order()
unsigned int * pset
Definition espresso.h:73
pset set_copy()
Here is the call graph for this function: