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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START pcover essential (IN pcover *Fp, IN pcover *Dp)
 
bool essen_cube (IN pcover F, IN pcover D, IN pcube c)
 
pcover cb_consensus (pcover T, pcube c)
 
pcover cb_consensus_dist0 (pcover R, pcube p, pcube c)
 

Function Documentation

◆ cb_consensus()

pcover cb_consensus ( pcover T,
pcube c )

Definition at line 109 of file essen.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}
#define pcover
Definition espresso.h:264
pset_family sf_addset()
#define new_cube()
Definition espresso.h:262
#define set_free(r)
Definition espresso.h:167
void consensus()
#define pcube
Definition espresso.h:261
#define foreach_set(R, last, p)
Definition espresso.h:135
int cdist01()
pcover cb_consensus_dist0()
#define new_cover(i)
Definition espresso.h:265
Cube * p
Definition exorList.c:222
Here is the call graph for this function:

◆ cb_consensus_dist0()

pcover cb_consensus_dist0 ( pcover R,
pcube p,
pcube c )

Definition at line 143 of file essen.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}
#define TRUE
Definition abcBm.c:38
#define FALSE
Definition abcBm.c:37
#define INLINEset_diff(r, a, b)
Definition espresso.h:208
bool setp_disjoint()
#define INLINEset_merge(r, a, b, mask)
Definition espresso.h:225
#define INLINEset_and(r, a, b)
Definition espresso.h:202
bool setp_implies()
unsigned short var
Definition giaNewBdd.h:35
Definition exor.h:123
Here is the call graph for this function:

◆ essen_cube()

bool essen_cube ( IN pcover F,
IN pcover D,
IN pcube c )

Definition at line 83 of file essen.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}
pcover cb_consensus()
pcube * cube2list()
#define free_cover(r)
Definition espresso.h:266
bool cube_is_covered()
pset_family sf_join()
#define free_cubelist(T)
Definition espresso.h:267
Here is the call graph for this function:

◆ essential()

ABC_NAMESPACE_IMPL_START pcover essential ( IN pcover * Fp,
IN pcover * Dp )

Definition at line 39 of file essen.c.

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}
char * pc1()
#define RELESSEN
Definition espresso.h:132
#define ESSEN
Definition espresso.h:352
pset_family sf_inactive()
#define TESTP(set, flag)
Definition espresso.h:124
#define ACTIVE
Definition espresso.h:129
bool essen_cube()
void sf_free()
pset_family sf_active()
unsigned int debug
Definition globals.c:19
#define NONESSEN
Definition espresso.h:128
#define RESET(set, flag)
Definition espresso.h:123
Here is the call graph for this function: