ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cvrm.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: cvrm.c
12 Purpose: miscellaneous cover manipulation
13 a) verify two covers are equal, check consistency of a cover
14 b) unravel a multiple-valued cover into minterms
15 c) sort covers
16*/
17
18#include "espresso.h"
19
21
22
23
24static void cb_unravel(c, start, end, startbase, B1)
25IN register pcube c;
26IN int start, end;
27IN pcube startbase;
28INOUT pcover B1;
29{
30 pcube base = cube.temp[0], p, last;
31 int expansion, place, skip, var, size, offset;
32 register int i, j, k, n;
33
34 /* Determine how many cubes it will blow up into, and create a mask
35 for those parts that have only a single coordinate
36 */
37 expansion = 1;
38 (void) set_copy(base, startbase);
39 for(var = start; var <= end; var++) {
40 if ((size = set_dist(c, cube.var_mask[var])) < 2) {
41 (void) set_or(base, base, cube.var_mask[var]);
42 } else {
43 expansion *= size;
44 }
45 }
46 (void) set_and(base, c, base);
47
48 /* Add the unravelled sets starting at the last element of B1 */
49 offset = B1->count;
50 B1->count += expansion;
51 foreach_remaining_set(B1, last, GETSET(B1, offset-1), p) {
52 INLINEset_copy(p, base);
53 }
54
55 place = expansion;
56 for(var = start; var <= end; var++) {
57 if ((size = set_dist(c, cube.var_mask[var])) > 1) {
58 skip = place;
59 place = place / size;
60 n = 0;
61 for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
62 if (is_in_set(c, i)) {
63 for(j = n; j < expansion; j += skip) {
64 for(k = 0; k < place; k++) {
65 p = GETSET(B1, j+k+offset);
66 (void) set_insert(p, i);
67 }
68 }
69 n += place;
70 }
71 }
72 }
73 }
74}
75
76
77pcover unravel_range(B, start, end)
78IN pcover B;
79IN int start, end;
80{
81 pcover B1;
82 int var, total_size, expansion, size;
83 register pcube p, last, startbase = cube.temp[1];
84
85 /* Create the starting base for those variables not being unravelled */
86 (void) set_copy(startbase, cube.emptyset);
87 for(var = 0; var < start; var++)
88 (void) set_or(startbase, startbase, cube.var_mask[var]);
89 for(var = end+1; var < cube.num_vars; var++)
90 (void) set_or(startbase, startbase, cube.var_mask[var]);
91
92 /* Determine how many cubes it will blow up into */
93 total_size = 0;
94 foreach_set(B, last, p) {
95 expansion = 1;
96 for(var = start; var <= end; var++)
97 if ((size = set_dist(p, cube.var_mask[var])) >= 2)
98 if ((expansion *= size) > 1000000)
99 fatal("unreasonable expansion in unravel");
100 total_size += expansion;
101 }
102
103 /* We can now allocate a cover of exactly the correct size */
104 B1 = new_cover(total_size);
105 foreach_set(B, last, p) {
106 cb_unravel(p, start, end, startbase, B1);
107 }
108 free_cover(B);
109 return B1;
110}
111
112
114IN pcover B;
115IN int start;
116{
117 return unravel_range(B, start, cube.num_vars-1);
118}
119
120/* lex_sort -- sort cubes in a standard lexical fashion */
122pcover T;
123{
124 pcover T1 = sf_unlist(sf_sort(T, lex_order), T->count, T->sf_size);
125 free_cover(T);
126 return T1;
127}
128
129
130/* size_sort -- sort cubes by their size */
132pcover T;
133{
134 pcover T1 = sf_unlist(sf_sort(T, descend), T->count, T->sf_size);
135 free_cover(T);
136 return T1;
137}
138
139
140/* mini_sort -- sort cubes according to the heuristics of mini */
141pcover mini_sort(F, compare)
142pcover F;
143int (*compare)();
144{
145 register int *count, cnt, n = cube.size, i;
146 register pcube p, last;
147 pcover F_sorted;
148 pcube *F1;
149
150 /* Perform a column sum over the set family */
151 count = sf_count(F);
152
153 /* weight is "inner product of the cube and the column sums" */
154 foreach_set(F, last, p) {
155 cnt = 0;
156 for(i = 0; i < n; i++)
157 if (is_in_set(p, i))
158 cnt += count[i];
159 PUTSIZE(p, cnt);
160 }
161 FREE(count);
162
163 /* use qsort to sort the array */
164 qsort((char *) (F1 = sf_list(F)), (size_t)F->count, sizeof(pcube), compare);
165 F_sorted = sf_unlist(F1, F->count, F->sf_size);
166 free_cover(F);
167
168 return F_sorted;
169}
170
171
172/* sort_reduce -- Espresso strategy for ordering the cubes before reduction */
174IN pcover T;
175{
176 register pcube p, last, largest = NULL;
177 register int bestsize = -1, size, n = cube.num_vars;
178 pcover T_sorted;
179 pcube *T1;
180
181 if (T->count == 0)
182 return T;
183
184 /* find largest cube */
185 foreach_set(T, last, p)
186 if ((size = set_ord(p)) > bestsize)
187 largest = p, bestsize = size;
188
189 foreach_set(T, last, p)
190 PUTSIZE(p, ((n - cdist(largest,p)) << 7) + MIN(set_ord(p),127));
191
192 qsort((char *) (T1 = sf_list(T)), (size_t)T->count, sizeof(pcube), (int (*)()) descend);
193 T_sorted = sf_unlist(T1, T->count, T->sf_size);
194 free_cover(T);
195
196 return T_sorted;
197}
198
200register pcover F;
201{
202 pset temp;
203 register int i, k;
204#ifdef RANDOM
205 long random();
206#endif
207
208 temp = set_new(F->sf_size);
209 for(i = F->count - 1; i > 0; i--) {
210 /* Choose a random number between 0 and i */
211#ifdef RANDOM
212 k = random() % i;
213#else
214 /* this is not meant to be really used; just provides an easy
215 "out" if random() and srandom() aren't around
216 */
217 k = (i*23 + 997) % i;
218#endif
219 /* swap sets i and k */
220 (void) set_copy(temp, GETSET(F, k));
221 (void) set_copy(GETSET(F, k), GETSET(F, i));
222 (void) set_copy(GETSET(F, i), temp);
223 }
224 set_free(temp);
225 return F;
226}
227
228/*
229 * cubelist_partition -- take a cubelist T and see if it has any components;
230 * if so, return cubelist's of the two partitions A and B; the return value
231 * is the size of the partition; if not, A and B
232 * are undefined and the return value is 0
233 */
234int cubelist_partition(T, A, B, comp_debug)
235pcube *T; /* a list of cubes */
236pcube **A, **B; /* cubelist of partition and remainder */
237unsigned int comp_debug;
238{
239 register pcube *T1, p, seed, cof;
240 pcube *A1, *B1;
241 bool change;
242 int count, numcube;
243
244 numcube = CUBELISTSIZE(T);
245
246 /* Mark all cubes -- covered cubes belong to the partition */
247 for(T1 = T+2; (p = *T1++) != NULL; ) {
248 RESET(p, COVERED);
249 }
250
251 /*
252 * Extract a partition from the cubelist T; start with the first cube as a
253 * seed, and then pull in all cubes which share a variable with the seed;
254 * iterate until no new cubes are brought into the partition.
255 */
256 seed = set_save(T[2]);
257 cof = T[0];
258 SET(T[2], COVERED);
259 count = 1;
260
261 do {
262 change = FALSE;
263 for(T1 = T+2; (p = *T1++) != NULL; ) {
264 if (! TESTP(p, COVERED) && ccommon(p, seed, cof)) {
265 INLINEset_and(seed, seed, p);
266 SET(p, COVERED);
267 change = TRUE;
268 count++;
269 }
270
271 }
272 } while (change);
273
274 set_free(seed);
275
276 if (comp_debug) {
277 (void) printf("COMPONENT_REDUCTION: split into %d %d\n",
278 count, numcube - count);
279 }
280
281 if (count != numcube) {
282 /* Allocate and setup the cubelist's for the two partitions */
283 *A = A1 = ALLOC(pcube, numcube+3);
284 *B = B1 = ALLOC(pcube, numcube+3);
285 (*A)[0] = set_save(T[0]);
286 (*B)[0] = set_save(T[0]);
287 A1 = *A + 2;
288 B1 = *B + 2;
289
290 /* Loop over the cubes in T and distribute to A and B */
291 for(T1 = T+2; (p = *T1++) != NULL; ) {
292 if (TESTP(p, COVERED)) {
293 *A1++ = p;
294 } else {
295 *B1++ = p;
296 }
297 }
298
299 /* Stuff needed at the end of the cubelist's */
300 *A1++ = NULL;
301 (*A)[1] = (pcube) A1;
302 *B1++ = NULL;
303 (*B)[1] = (pcube) B1;
304 }
305
306 return numcube - count;
307}
308
309/*
310 * quick cofactor against a single output function
311 */
313pcover T;
314register int i;
315{
316 pcover T1;
317 register pcube p, last, pdest, mask;
318
319 mask = cube.var_mask[cube.output];
320 T1 = new_cover(T->count);
321 foreach_set(T, last, p) {
322 if (is_in_set(p, i)) {
323 pdest = GETSET(T1, T1->count++);
324 INLINEset_or(pdest, p, mask);
325 RESET(pdest, PRIME);
326 }
327 }
328 return T1;
329}
330
331
332/*
333 * quick intersection against a single output function
334 */
336pcover T;
337int i;
338{
339 register pcube p, last, mask;
340
341 if (T == NULL) {
342 return T;
343 }
344
345 mask = cube.var_mask[cube.output];
346 foreach_set(T, last, p) {
347 INLINEset_diff(p, p, mask);
348 set_insert(p, i);
349 }
350 return T;
351}
352
353
354/*
355 * A generic routine to perform an operation for each output function
356 *
357 * func() is called with a PLA for each output function (with the output
358 * part effectively removed).
359 * func1() is called after reforming the equivalent output function
360 *
361 * Each function returns TRUE if process is to continue
362 */
363void foreach_output_function(PLA, func, func1)
364pPLA PLA;
365int (*func)();
366int (*func1)();
367{
368 pPLA PLA1;
369 int i;
370
371 /* Loop for each output function */
372 for(i = 0; i < cube.part_size[cube.output]; i++) {
373
374 /* cofactor on the output part */
375 PLA1 = new_PLA();
376 PLA1->F = cof_output(PLA->F, i + cube.first_part[cube.output]);
377 PLA1->R = cof_output(PLA->R, i + cube.first_part[cube.output]);
378 PLA1->D = cof_output(PLA->D, i + cube.first_part[cube.output]);
379
380 /* Call a routine to do something with the cover */
381 if ((*func)(PLA1, i) == 0) {
382 free_PLA(PLA1);
383 return;
384 }
385
386 /* intersect with the particular output part again */
387 PLA1->F = uncof_output(PLA1->F, i + cube.first_part[cube.output]);
388 PLA1->R = uncof_output(PLA1->R, i + cube.first_part[cube.output]);
389 PLA1->D = uncof_output(PLA1->D, i + cube.first_part[cube.output]);
390
391 /* Call a routine to do something with the final result */
392 if ((*func1)(PLA1, i) == 0) {
393 free_PLA(PLA1);
394 return;
395 }
396
397 /* Cleanup for next go-around */
398 free_PLA(PLA1);
399
400
401 }
402}
403
404static pcover Fmin;
405static pcube phase;
406
407/*
408 * minimize each output function individually
409 */
410void so_espresso(PLA, strategy)
411pPLA PLA;
412int strategy;
413{
414 Fmin = new_cover(PLA->F->count);
415 if (strategy == 0) {
417 } else {
419 }
420 sf_free(PLA->F);
421 PLA->F = Fmin;
422}
423
424
425/*
426 * minimize each output function, choose function or complement based on the
427 * one with the fewer number of terms
428 */
429void so_both_espresso(PLA, strategy)
430pPLA PLA;
431int strategy;
432{
433 phase = set_save(cube.fullset);
434 Fmin = new_cover(PLA->F->count);
435 if (strategy == 0) {
437 } else {
439 }
440 sf_free(PLA->F);
441 PLA->F = Fmin;
442 PLA->phase = phase;
443}
444
445
446int so_do_espresso(PLA, i)
447pPLA PLA;
448int i;
449{
450 char word[32];
451
452 /* minimize the single-output function (on-set) */
454 (void) sprintf(word, "ESPRESSO-POS(%d)", i);
455 EXEC_S(PLA->F = espresso(PLA->F, PLA->D, PLA->R), word, PLA->F);
456 return 1;
457}
458
459
460int so_do_exact(PLA, i)
461pPLA PLA;
462int i;
463{
464 char word[32];
465
466 /* minimize the single-output function (on-set) */
468 (void) sprintf(word, "EXACT-POS(%d)", i);
469 EXEC_S(PLA->F = minimize_exact(PLA->F, PLA->D, PLA->R, 1), word, PLA->F);
470 return 1;
471}
472
473
474/*ARGSUSED*/
475int so_save(PLA, i)
476pPLA PLA;
477int i;
478{
479 Fmin = sf_append(Fmin, PLA->F); /* disposes of PLA->F */
480 PLA->F = NULL;
481 return 1;
482}
483
484
486pPLA PLA;
487int i;
488{
489 char word[32];
490
491 /* minimize the single-output function (on-set) */
492 (void) sprintf(word, "ESPRESSO-POS(%d)", i);
494 EXEC_S(PLA->F = espresso(PLA->F, PLA->D, PLA->R), word, PLA->F);
495
496 /* minimize the single-output function (off-set) */
497 (void) sprintf(word, "ESPRESSO-NEG(%d)", i);
499 EXEC_S(PLA->R = espresso(PLA->R, PLA->D, PLA->F), word, PLA->R);
500
501 return 1;
502}
503
504
506pPLA PLA;
507int i;
508{
509 char word[32];
510
511 /* minimize the single-output function (on-set) */
512 (void) sprintf(word, "EXACT-POS(%d)", i);
514 EXEC_S(PLA->F = minimize_exact(PLA->F, PLA->D, PLA->R, 1), word, PLA->F);
515
516 /* minimize the single-output function (off-set) */
517 (void) sprintf(word, "EXACT-NEG(%d)", i);
519 EXEC_S(PLA->R = minimize_exact(PLA->R, PLA->D, PLA->F, 1), word, PLA->R);
520
521 return 1;
522}
523
524
525int so_both_save(PLA, i)
526pPLA PLA;
527int i;
528{
529 if (PLA->F->count > PLA->R->count) {
530 sf_free(PLA->F);
531 PLA->F = PLA->R;
532 PLA->R = NULL;
533 i += cube.first_part[cube.output];
534 set_remove(phase, i);
535 } else {
536 sf_free(PLA->R);
537 PLA->R = NULL;
538 }
539 Fmin = sf_append(Fmin, PLA->F);
540 PLA->F = NULL;
541 return 1;
542}
544
#define TRUE
Definition abcBm.c:38
#define FALSE
Definition abcBm.c:37
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define ALLOC(type, num)
Definition avl.h:27
#define FREE(obj)
Definition avl.h:31
pPLA new_PLA()
Definition cvrin.c:648
int so_both_do_espresso(pPLA PLA, int i)
Definition cvrm.c:485
int so_both_do_exact(pPLA PLA, int i)
Definition cvrm.c:505
int so_save(pPLA PLA, int i)
Definition cvrm.c:475
int so_do_espresso(pPLA PLA, int i)
Definition cvrm.c:446
int so_do_exact(pPLA PLA, int i)
Definition cvrm.c:460
int so_both_save(pPLA PLA, int i)
Definition cvrm.c:525
ABC_NAMESPACE_IMPL_START pcover espresso(pcover F, pcover D1, pcover R)
Definition espresso.c:53
int lex_order()
#define pcover
Definition espresso.h:264
#define set_save(r)
Definition espresso.h:166
#define INLINEset_diff(r, a, b)
Definition espresso.h:208
#define INLINEset_or(r, a, b)
Definition espresso.h:205
int so_save()
pcover size_sort()
#define PUTSIZE(set, size)
Definition espresso.h:113
struct PLA_t * pPLA
#define is_in_set(set, e)
Definition espresso.h:170
#define set_free(r)
Definition espresso.h:167
#define TESTP(set, flag)
Definition espresso.h:124
int so_do_exact()
#define set_new(size)
Definition espresso.h:164
#define set_insert(set, e)
Definition espresso.h:172
pset set_and()
int * sf_count()
void fatal()
pcover random_order()
pcover mini_sort()
#define INOUT
Definition espresso.h:334
void so_both_espresso()
#define COVERED
Definition espresso.h:131
void sf_free()
void free_PLA()
pcover sort_reduce()
#define pcube
Definition espresso.h:261
pset_family sf_unlist()
#define free_cover(r)
Definition espresso.h:266
int so_both_do_espresso()
pcover unravel()
pcover uncof_output()
#define GETSET(family, index)
Definition espresso.h:161
#define INLINEset_copy(r, a)
Definition espresso.h:195
int so_do_espresso()
#define set_remove(set, e)
Definition espresso.h:171
bool skip_make_sparse
Definition globals.c:28
#define foreach_set(R, last, p)
Definition espresso.h:135
#define SET(set, flag)
Definition espresso.h:122
pcover minimize_exact()
int so_both_save()
int set_ord()
void so_espresso()
#define INLINEset_and(r, a, b)
Definition espresso.h:202
pcover unravel_range()
int cdist()
#define IN
Definition espresso.h:332
#define RESET(set, flag)
Definition espresso.h:123
#define PRIME
Definition espresso.h:127
pcover lex_sort()
int cubelist_partition()
#define foreach_remaining_set(R, last, pfirst, p)
Definition espresso.h:137
pcover cof_output()
unsigned int * pset
Definition espresso.h:73
pset set_or()
pset * sf_sort()
pset_family sf_append()
pset * sf_list()
int so_both_do_exact()
pset set_copy()
#define CUBELISTSIZE(T)
Definition espresso.h:329
#define EXEC_S(fct, name, S)
Definition espresso.h:420
#define new_cover(i)
Definition espresso.h:265
bool ccommon()
void foreach_output_function()
int set_dist()
Cube * p
Definition exorList.c:222
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
unsigned long long size
Definition giaNewBdd.h:39
unsigned short var
Definition giaNewBdd.h:35
pcover D
Definition espresso.h:316
pcover R
Definition espresso.h:316
pcover F
Definition espresso.h:316
Definition exor.h:123
#define MIN(a, b)
Definition util_old.h:256
char * sprintf()
long random()