ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
essen.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: essen.c
12 purpose: Find essential primes in a multiple-valued function
13*/
14
15#include "espresso.h"
16
18
19
20/*
21 essential -- return a cover consisting of the cubes of F which are
22 essential prime implicants (with respect to F u D); Further, remove
23 these cubes from the ON-set F, and add them to the OFF-set D.
24
25 Sometimes EXPAND can determine that a cube is not an essential prime.
26 If so, it will set the "NONESSEN" flag in the cube.
27
28 We count on IRREDUNDANT to have set the flag RELESSEN to indicate
29 that a prime was relatively essential (i.e., covers some minterm
30 not contained in any other prime in the current cover), or to have
31 reset the flag to indicate that a prime was relatively redundant
32 (i.e., all minterms covered by other primes in the current cover).
33 Of course, after executing irredundant, all of the primes in the
34 cover are relatively essential, but we can mark the primes which
35 were redundant at the start of irredundant and avoid an extra check
36 on these primes for essentiality.
37*/
38
40IN pcover *Fp, *Dp;
41{
42 register pcube last, p;
43 pcover E, F = *Fp, D = *Dp;
44
45 /* set all cubes in F active */
46 (void) sf_active(F);
47
48 /* Might as well start out with some cubes in E */
49 E = new_cover(10);
50
51 foreach_set(F, last, p) {
52 /* don't test a prime which EXPAND says is nonessential */
53 if (! TESTP(p, NONESSEN)) {
54 /* only test a prime which was relatively essential */
55 if (TESTP(p, RELESSEN)) {
56 /* Check essentiality */
57 if (essen_cube(F, D, p)) {
58 if (debug & ESSEN)
59 printf("ESSENTIAL: %s\n", pc1(p));
60 E = sf_addset(E, p);
61 RESET(p, ACTIVE);
62 F->active_count--;
63 }
64 }
65 }
66 }
67
68 *Fp = sf_inactive(F); /* delete the inactive cubes from F */
69 *Dp = sf_join(D, E); /* add the essentials to D */
70 sf_free(D);
71 return E;
72}
73
74/*
75 essen_cube -- check if a single cube is essential or not
76
77 The prime c is essential iff
78
79 consensus((F u D) # c, c) u D
80
81 does not contain c.
82*/
83bool essen_cube(F, D, c)
84IN pcover F, D;
85IN pcube c;
86{
87 pcover H, FD;
88 pcube *H1;
89 bool essen;
90
91 /* Append F and D together, and take the sharp-consensus with c */
92 FD = sf_join(F, D);
93 H = cb_consensus(FD, c);
94 free_cover(FD);
95
96 /* Add the don't care set, and see if this covers c */
97 H1 = cube2list(H, D);
98 essen = ! cube_is_covered(H1, c);
99 free_cubelist(H1);
100
101 free_cover(H);
102 return essen;
103}
104
105
106/*
107 * cb_consensus -- compute consensus(T # c, c)
108 */
110register pcover T;
111register pcube c;
112{
113 register pcube temp, last, p;
114 register pcover R;
115
116 R = new_cover(T->count*2);
117 temp = new_cube();
118 foreach_set(T, last, p) {
119 if (p != c) {
120 switch (cdist01(p, c)) {
121 case 0:
122 /* distance-0 needs special care */
123 R = cb_consensus_dist0(R, p, c);
124 break;
125
126 case 1:
127 /* distance-1 is easy because no sharping required */
128 consensus(temp, p, c);
129 R = sf_addset(R, temp);
130 break;
131 }
132 }
133 }
134 set_free(temp);
135 return R;
136}
137
138
139/*
140 * form the sharp-consensus for p and c when they intersect
141 * What we are forming is consensus(p # c, c).
142 */
144pcover R;
145register pcube p, c;
146{
147 int var;
148 bool got_one;
149 register pcube temp, mask;
150 register pcube p_diff_c=cube.temp[0], p_and_c=cube.temp[1];
151
152 /* If c contains p, then this gives us no information for essential test */
153 if (setp_implies(p, c)) {
154 return R;
155 }
156
157 /* For the multiple-valued variables */
158 temp = new_cube();
159 got_one = FALSE;
160 INLINEset_diff(p_diff_c, p, c);
161 INLINEset_and(p_and_c, p, c);
162
163 for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
164 /* Check if c(var) is contained in p(var) -- if so, no news */
165 mask = cube.var_mask[var];
166 if (! setp_disjoint(p_diff_c, mask)) {
167 INLINEset_merge(temp, c, p_and_c, mask);
168 R = sf_addset(R, temp);
169 got_one = TRUE;
170 }
171 }
172
173 /* if no cube so far, add one for the intersection */
174 if (! got_one && cube.num_binary_vars > 0) {
175 /* Add a single cube for the intersection of p and c */
176 INLINEset_and(temp, p, c);
177 R = sf_addset(R, temp);
178 }
179
180 set_free(temp);
181 return R;
182}
184
#define TRUE
Definition abcBm.c:38
#define FALSE
Definition abcBm.c:37
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define pcover
Definition espresso.h:264
pset_family sf_addset()
#define new_cube()
Definition espresso.h:262
char * pc1()
#define RELESSEN
Definition espresso.h:132
#define ESSEN
Definition espresso.h:352
#define INLINEset_diff(r, a, b)
Definition espresso.h:208
pset_family sf_inactive()
#define set_free(r)
Definition espresso.h:167
#define TESTP(set, flag)
Definition espresso.h:124
bool setp_disjoint()
#define ACTIVE
Definition espresso.h:129
pcover cb_consensus()
void consensus()
pcube * cube2list()
bool essen_cube()
void sf_free()
pset_family sf_active()
#define pcube
Definition espresso.h:261
#define free_cover(r)
Definition espresso.h:266
pcover essential()
#define foreach_set(R, last, p)
Definition espresso.h:135
unsigned int debug
Definition globals.c:19
#define INLINEset_merge(r, a, b, mask)
Definition espresso.h:225
#define INLINEset_and(r, a, b)
Definition espresso.h:202
#define NONESSEN
Definition espresso.h:128
bool setp_implies()
#define IN
Definition espresso.h:332
#define RESET(set, flag)
Definition espresso.h:123
bool cube_is_covered()
int cdist01()
pcover cb_consensus_dist0()
pset_family sf_join()
#define free_cubelist(T)
Definition espresso.h:267
#define new_cover(i)
Definition espresso.h:265
Cube * p
Definition exorList.c:222
Definition exor.h:123