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

Go to the source code of this file.

Macros

#define POW2(x)
 

Functions

void phase_assignment (pPLA PLA, int opo_strategy)
 
void repeated_phase_assignment (pPLA PLA)
 
pcube find_phase (pPLA PLA, int first_output, pcube phase1)
 
pcover opo (pcube phase, pcover T, pcover D, pcover R, int first_output)
 
pset_family opo_recur (pcover T, pcover D, pcube select, int offset, int first, int last)
 
pset_family opo_leaf (pcover T, pset select, int out1, int out2)
 
void output_phase_setup (INOUT pPLA PLA, int first_output)
 
pPLA set_phase (INOUT pPLA PLA)
 
void opoall (pPLA PLA, int first_output, int last_output, int opo_strategy)
 

Macro Definition Documentation

◆ POW2

#define POW2 ( x)
Value:
(1 << (x))

Definition at line 539 of file opo.c.

Function Documentation

◆ find_phase()

pcube find_phase ( pPLA PLA,
int first_output,
pcube phase1 )

Definition at line 129 of file opo.c.

133{
134 pcube phase;
135 pPLA PLA1;
136
137 phase = set_save(cube.fullset);
138
139 /* setup the double-phase characteristic function, resize the cube */
140 PLA1 = new_PLA();
141 PLA1->F = sf_save(PLA->F);
142 PLA1->R = sf_save(PLA->R);
143 PLA1->D = sf_save(PLA->D);
144 if (phase1 != NULL) {
145 PLA1->phase = set_save(phase1);
146 (void) set_phase(PLA1);
147 }
148 EXEC_S(output_phase_setup(PLA1, first_output), "OPO-SETUP ", PLA1->F);
149
150 /* minimize the double-phase function */
151 minimize(PLA1);
152
153 /* set the proper phases according to what gives a minimum solution */
154 EXEC_S(PLA1->F = opo(phase, PLA1->F, PLA1->D, PLA1->R, first_output),
155 "OPO ", PLA1->F);
156 free_PLA(PLA1);
157
158 /* set the cube structure to reflect the old size */
159 setdown_cube();
160 cube.part_size[cube.output] -=
161 (cube.part_size[cube.output] - first_output) / 2;
162 cube_setup();
163
164 return phase;
165}
void setdown_cube()
Definition cubestr.c:95
ABC_NAMESPACE_IMPL_START void cube_setup()
Definition cubestr.c:27
pPLA new_PLA()
Definition cvrin.c:648
#define set_save(r)
Definition espresso.h:166
struct PLA_t * pPLA
void free_PLA()
#define pcube
Definition espresso.h:261
pPLA set_phase()
pset_family sf_save()
pcover opo()
void output_phase_setup()
#define EXEC_S(fct, name, S)
Definition espresso.h:420
pcover D
Definition espresso.h:316
pcover R
Definition espresso.h:316
pcube phase
Definition espresso.h:319
pcover F
Definition espresso.h:316
Definition exor.h:123
Here is the call graph for this function:

◆ opo()

pcover opo ( pcube phase,
pcover T,
pcover D,
pcover R,
int first_output )

Definition at line 173 of file opo.c.

177{
178 int offset, output, i, last_output, ind;
179 pset pdest, select, p, p1, last, last1, not_covered, tmp;
180 pset_family temp, T1, T2;
181
182 /* must select all primes for outputs [0 .. first_output-1] */
183 select = set_full(T->count);
184 for(output = 0; output < first_output; output++) {
185 ind = cube.first_part[cube.output] + output;
186 foreachi_set(T, i, p) {
187 if (is_in_set(p, ind)) {
188 set_remove(select, i);
189 }
190 }
191 }
192
193 /* Recursively perform the intersections */
194 offset = (cube.part_size[cube.output] - first_output) / 2;
195 last_output = first_output + offset - 1;
196 temp = opo_recur(T, D, select, offset, first_output, last_output);
197
198 /* largest set is on top -- select primes which are inferred from it */
199 pdest = temp->data;
200 T1 = new_cover(T->count);
201 foreachi_set(T, i, p) {
202 if (! is_in_set(pdest, i)) {
203 T1 = sf_addset(T1, p);
204 }
205 }
206
207 set_free(select);
208 sf_free(temp);
209
210 /* finding phases is difficult -- see which functions are not covered */
211 T2 = complement(cube1list(T1));
212 not_covered = new_cube();
213 tmp = new_cube();
214 foreach_set(T, last, p) {
215 foreach_set(T2, last1, p1) {
216 if (cdist0(p, p1)) {
217 (void) set_or(not_covered, not_covered, set_and(tmp, p, p1));
218 }
219 }
220 }
221 free_cover(T);
222 free_cover(T2);
223 set_free(tmp);
224
225 /* Now reflect the phase choice in a single cube */
226 for(output = first_output; output <= last_output; output++) {
227 ind = cube.first_part[cube.output] + output;
228 if (is_in_set(not_covered, ind)) {
229 if (is_in_set(not_covered, ind + offset)) {
230 fatal("error in output phase assignment");
231 } else {
232 set_remove(phase, ind);
233 }
234 }
235 }
236 set_free(not_covered);
237 return T1;
238}
pset_family sf_addset()
#define new_cube()
Definition espresso.h:262
#define is_in_set(set, e)
Definition espresso.h:170
#define set_free(r)
Definition espresso.h:167
#define foreachi_set(R, i, p)
Definition espresso.h:143
pset_family opo_recur()
pset set_and()
void fatal()
#define set_full(size)
Definition espresso.h:165
void sf_free()
#define free_cover(r)
Definition espresso.h:266
#define set_remove(set, e)
Definition espresso.h:171
struct set_family * pset_family
#define foreach_set(R, last, p)
Definition espresso.h:135
unsigned int * pset
Definition espresso.h:73
pset set_or()
bool cdist0()
pcube * cube1list()
#define new_cover(i)
Definition espresso.h:265
pcover complement()
Cube * p
Definition exorList.c:222
pset data
Definition espresso.h:82
Here is the call graph for this function:

◆ opo_leaf()

pset_family opo_leaf ( pcover T,
pset select,
int out1,
int out2 )

Definition at line 278 of file opo.c.

282{
283 register pset_family temp;
284 register pset p, pdest;
285 register int i;
286
287 out1 += cube.first_part[cube.output];
288 out2 += cube.first_part[cube.output];
289
290 /* Allocate space for the result */
291 temp = sf_new(2, T->count);
292
293 /* Find which primes are needed for the ON-set of this fct */
294 pdest = GETSET(temp, temp->count++);
295 (void) set_copy(pdest, select);
296 foreachi_set(T, i, p) {
297 if (is_in_set(p, out1)) {
298 set_remove(pdest, i);
299 }
300 }
301
302 /* Find which primes are needed for the OFF-set of this fct */
303 pdest = GETSET(temp, temp->count++);
304 (void) set_copy(pdest, select);
305 foreachi_set(T, i, p) {
306 if (is_in_set(p, out2)) {
307 set_remove(pdest, i);
308 }
309 }
310
311 return temp;
312}
pset_family sf_new()
#define GETSET(family, index)
Definition espresso.h:161
pset set_copy()
int count
Definition espresso.h:80
Here is the call graph for this function:

◆ opo_recur()

pset_family opo_recur ( pcover T,
pcover D,
pcube select,
int offset,
int first,
int last )

Definition at line 240 of file opo.c.

244{
245 static int level = 0;
246 int middle;
247 pset_family sl, sr, temp;
248
249 level++;
250 if (first == last) {
251#if 0
252 if (opo_no_make_sparse) {
253 temp = form_cover_table(T, D, select, first, first + offset);
254 } else {
255 temp = opo_leaf(T, select, first, first + offset);
256 }
257#else
258 temp = opo_leaf(T, select, first, first + offset);
259#endif
260 } else {
261 middle = (first + last) / 2;
262 sl = opo_recur(T, D, select, offset, first, middle);
263 sr = opo_recur(T, D, select, offset, middle+1, last);
264 temp = unate_intersect(sl, sr, level == 1);
265 if (trace) {
266 printf("# OPO[%d]: %4d = %4d x %4d, time = %s\n", level - 1,
267 temp->count, sl->count, sr->count, print_time(ptime()));
268 (void) fflush(stdout);
269 }
270 free_cover(sl);
271 free_cover(sr);
272 }
273 level--;
274 return temp;
275}
pset_family opo_leaf()
#define print_time(t)
Definition espresso.h:22
bool trace
Definition globals.c:36
pset_family form_cover_table()
pset_family unate_intersect()
#define ptime()
Definition util_old.h:283
Here is the call graph for this function:

◆ opoall()

void opoall ( pPLA PLA,
int first_output,
int last_output,
int opo_strategy )

Definition at line 541 of file opo.c.

545{
546 pcover F, D, R, best_F, best_D, best_R;
547 int i, j, ind, num;
548 pcube bestphase;
549
550 opo_exact = opo_strategy;
551
552 if (PLA->phase != NULL) {
553 set_free(PLA->phase);
554 }
555
556 bestphase = set_save(cube.fullset);
557 best_F = sf_save(PLA->F);
558 best_D = sf_save(PLA->D);
559 best_R = sf_save(PLA->R);
560
561 for(i = 0; i < POW2(last_output - first_output + 1); i++) {
562
563 /* save the initial PLA covers */
564 F = sf_save(PLA->F);
565 D = sf_save(PLA->D);
566 R = sf_save(PLA->R);
567
568 /* compute the phase cube for this iteration */
569 PLA->phase = set_save(cube.fullset);
570 num = i;
571 for(j = last_output; j >= first_output; j--) {
572 if (num % 2 == 0) {
573 ind = cube.first_part[cube.output] + j;
574 set_remove(PLA->phase, ind);
575 }
576 num /= 2;
577 }
578
579 /* set the phase and minimize */
580 (void) set_phase(PLA);
581 printf("# phase is %s\n", pc1(PLA->phase));
582 summary = TRUE;
583 minimize(PLA);
584
585 /* see if this is the best so far */
586 if (PLA->F->count < best_F->count) {
587 /* save new best solution */
588 set_copy(bestphase, PLA->phase);
589 sf_free(best_F);
590 sf_free(best_D);
591 sf_free(best_R);
592 best_F = PLA->F;
593 best_D = PLA->D;
594 best_R = PLA->R;
595 } else {
596 /* throw away the solution */
597 free_cover(PLA->F);
598 free_cover(PLA->D);
599 free_cover(PLA->R);
600 }
601 set_free(PLA->phase);
602
603 /* restore the initial PLA covers */
604 PLA->F = F;
605 PLA->D = D;
606 PLA->R = R;
607 }
608
609 /* one more minimization to restore the best answer */
610 PLA->phase = bestphase;
611 sf_free(PLA->F);
612 sf_free(PLA->D);
613 sf_free(PLA->R);
614 PLA->F = best_F;
615 PLA->D = best_D;
616 PLA->R = best_R;
617}
#define TRUE
Definition abcBm.c:38
#define pcover
Definition espresso.h:264
char * pc1()
bool summary
Definition globals.c:35
#define POW2(x)
Definition opo.c:539
Here is the call graph for this function:

◆ output_phase_setup()

void output_phase_setup ( INOUT pPLA PLA,
int first_output )

Definition at line 417 of file opo.c.

420{
421 pcover F, R, D;
422 pcube mask, mask1, last;
423 int first_part, offset;
424 bool save;
425 register pcube p, pr, pf;
426 register int i, last_part;
427
428 if (cube.output == -1)
429 fatal("output_phase_setup: must have an output");
430
431 F = PLA->F;
432 D = PLA->D;
433 R = PLA->R;
434 first_part = cube.first_part[cube.output] + first_output;
435 last_part = cube.last_part[cube.output];
436 offset = cube.part_size[cube.output] - first_output;
437
438 /* Change the output size, setup the cube structure */
439 setdown_cube();
440 cube.part_size[cube.output] += offset;
441 cube_setup();
442
443 /* Create a mask to select that part of the cube which isn't changing */
444 mask = set_save(cube.fullset);
445 for(i = first_part; i < cube.size; i++)
446 set_remove(mask, i);
447 mask1 = set_save(mask);
448 for(i = cube.first_part[cube.output]; i < first_part; i++) {
449 set_remove(mask1, i);
450 }
451
452 PLA->F = new_cover(F->count + R->count);
453 PLA->R = new_cover(F->count + R->count);
454 PLA->D = new_cover(D->count);
455
456 foreach_set(F, last, p) {
457 pf = GETSET(PLA->F, (PLA->F)->count++);
458 pr = GETSET(PLA->R, (PLA->R)->count++);
459 INLINEset_and(pf, mask, p);
460 INLINEset_and(pr, mask1, p);
461 for(i = first_part; i <= last_part; i++)
462 if (is_in_set(p, i))
463 set_insert(pf, i);
464 save = FALSE;
465 for(i = first_part; i <= last_part; i++)
466 if (is_in_set(p, i))
467 save = TRUE, set_insert(pr, i+offset);
468 if (! save) PLA->R->count--;
469 }
470
471 foreach_set(R, last, p) {
472 pf = GETSET(PLA->F, (PLA->F)->count++);
473 pr = GETSET(PLA->R, (PLA->R)->count++);
474 INLINEset_and(pf, mask1, p);
475 INLINEset_and(pr, mask, p);
476 save = FALSE;
477 for(i = first_part; i <= last_part; i++)
478 if (is_in_set(p, i))
479 save = TRUE, set_insert(pf, i+offset);
480 if (! save) PLA->F->count--;
481 for(i = first_part; i <= last_part; i++)
482 if (is_in_set(p, i))
483 set_insert(pr, i);
484 }
485
486 foreach_set(D, last, p) {
487 pf = GETSET(PLA->D, (PLA->D)->count++);
488 INLINEset_and(pf, mask, p);
489 for(i = first_part; i <= last_part; i++)
490 if (is_in_set(p, i)) {
491 set_insert(pf, i);
492 set_insert(pf, i+offset);
493 }
494 }
495
496 free_cover(F);
497 free_cover(D);
498 free_cover(R);
499 set_free(mask);
500 set_free(mask1);
501}
#define FALSE
Definition abcBm.c:37
#define set_insert(set, e)
Definition espresso.h:172
#define INLINEset_and(r, a, b)
Definition espresso.h:202
Here is the call graph for this function:

◆ phase_assignment()

void phase_assignment ( pPLA PLA,
int opo_strategy )

Definition at line 67 of file opo.c.

70{
71 opo_no_make_sparse = opo_strategy % 2;
72 skip_make_sparse = opo_no_make_sparse;
73 opo_repeated = (opo_strategy / 2) % 2;
74 opo_exact = (opo_strategy / 4) % 2;
75
76 /* Determine a phase assignment */
77 if (PLA->phase != NULL) {
78 FREE(PLA->phase);
79 }
80
81 if (opo_repeated) {
82 PLA->phase = set_save(cube.fullset);
84 } else {
85 PLA->phase = find_phase(PLA, 0, (pcube) NULL);
86 }
87
88 /* Now minimize with this assignment */
90 (void) set_phase(PLA);
91 minimize(PLA);
92}
#define FREE(obj)
Definition avl.h:31
bool skip_make_sparse
Definition globals.c:28
pcube find_phase()
void repeated_phase_assignment()
Here is the call graph for this function:

◆ repeated_phase_assignment()

void repeated_phase_assignment ( pPLA PLA)

Definition at line 99 of file opo.c.

101{
102 int i;
103 pcube phase;
104
105 for(i = 0; i < cube.part_size[cube.output]; i++) {
106
107 /* Find best assignment for all undecided outputs */
108 phase = find_phase(PLA, i, PLA->phase);
109
110 /* Commit for only a single output ... */
111 if (! is_in_set(phase, cube.first_part[cube.output] + i)) {
112 set_remove(PLA->phase, cube.first_part[cube.output] + i);
113 }
114
115 if (trace || summary) {
116 printf("\nOPO loop for output #%d\n", i);
117 printf("PLA->phase is %s\n", pc1(PLA->phase));
118 printf("phase is %s\n", pc1(phase));
119 }
120 set_free(phase);
121 }
122}
Here is the call graph for this function:

◆ set_phase()

pPLA set_phase ( INOUT pPLA PLA)

Definition at line 507 of file opo.c.

509{
510 pcover F1, R1;
511 register pcube last, p, outmask;
512 register pcube temp=cube.temp[0], phase=PLA->phase, phase1=cube.temp[1];
513
514 outmask = cube.var_mask[cube.num_vars - 1];
515 set_diff(phase1, outmask, phase);
516 set_or(phase1, set_diff(temp, cube.fullset, outmask), phase1);
517 F1 = new_cover((PLA->F)->count + (PLA->R)->count);
518 R1 = new_cover((PLA->F)->count + (PLA->R)->count);
519
520 foreach_set(PLA->F, last, p) {
521 if (! setp_disjoint(set_and(temp, p, phase), outmask))
522 set_copy(GETSET(F1, F1->count++), temp);
523 if (! setp_disjoint(set_and(temp, p, phase1), outmask))
524 set_copy(GETSET(R1, R1->count++), temp);
525 }
526 foreach_set(PLA->R, last, p) {
527 if (! setp_disjoint(set_and(temp, p, phase), outmask))
528 set_copy(GETSET(R1, R1->count++), temp);
529 if (! setp_disjoint(set_and(temp, p, phase1), outmask))
530 set_copy(GETSET(F1, F1->count++), temp);
531 }
532 free_cover(PLA->F);
533 free_cover(PLA->R);
534 PLA->F = F1;
535 PLA->R = R1;
536 return PLA;
537}
bool setp_disjoint()
pset set_diff()
Here is the call graph for this function: