ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
exp.h
Go to the documentation of this file.
1
20
21#ifndef ABC__map__mio__exp_h
22#define ABC__map__mio__exp_h
23
27
31
32
33ABC_NAMESPACE_HEADER_START
34
38
42
43#define EXP_CONST0 -1
44#define EXP_CONST1 -2
45
46static inline Vec_Int_t * Exp_Const0()
47{
48 Vec_Int_t * vExp;
49 vExp = Vec_IntAlloc( 1 );
50 Vec_IntPush( vExp, EXP_CONST0 );
51 return vExp;
52}
53static inline Vec_Int_t * Exp_Const1()
54{
55 Vec_Int_t * vExp;
56 vExp = Vec_IntAlloc( 1 );
57 Vec_IntPush( vExp, EXP_CONST1 );
58 return vExp;
59}
60static inline int Exp_IsConst( Vec_Int_t * p )
61{
62 return Vec_IntEntry(p,0) == EXP_CONST0 || Vec_IntEntry(p,0) == EXP_CONST1;
63}
64static inline int Exp_IsConst0( Vec_Int_t * p )
65{
66 return Vec_IntEntry(p,0) == EXP_CONST0;
67}
68static inline int Exp_IsConst1( Vec_Int_t * p )
69{
70 return Vec_IntEntry(p,0) == EXP_CONST1;
71}
72static inline Vec_Int_t * Exp_Var( int iVar )
73{
74 Vec_Int_t * vExp;
75 vExp = Vec_IntAlloc( 1 );
76 Vec_IntPush( vExp, 2 * iVar );
77 return vExp;
78}
79static inline int Exp_LitShift( int nVars, int Lit, int Shift )
80{
81 if ( Lit < 2 * nVars )
82 return Lit;
83 return Lit + 2 * Shift;
84}
85static inline int Exp_IsLit( Vec_Int_t * p )
86{
87 return Vec_IntSize(p) == 1 && !Exp_IsConst(p);
88}
89static inline int Exp_NodeNum( Vec_Int_t * p )
90{
91 return Vec_IntSize(p)/2;
92}
93static inline Vec_Int_t * Exp_Not( Vec_Int_t * p )
94{
95 Vec_IntWriteEntry( p, 0, Vec_IntEntry(p,0) ^ 1 );
96 return p;
97}
98static inline void Exp_PrintLit( int nVars, int Lit )
99{
100 if ( Lit == EXP_CONST0 )
101 Abc_Print( 1, "Const0" );
102 else if ( Lit == EXP_CONST1 )
103 Abc_Print( 1, "Const1" );
104 else if ( Lit < 2 * nVars )
105 Abc_Print( 1, "%s%c", (Lit&1) ? "!" : " ", 'a' + Lit/2 );
106 else
107 Abc_Print( 1, "%s%d", (Lit&1) ? "!" : " ", Lit/2 );
108}
109static inline void Exp_Print( int nVars, Vec_Int_t * p )
110{
111 int i;
112 for ( i = 0; i < Exp_NodeNum(p); i++ )
113 {
114 Abc_Print( 1, "%2d = ", nVars + i );
115 Exp_PrintLit( nVars, Vec_IntEntry(p, 2*i+0) );
116 Abc_Print( 1, " & " );
117 Exp_PrintLit( nVars, Vec_IntEntry(p, 2*i+1) );
118 Abc_Print( 1, "\n" );
119 }
120 Abc_Print( 1, " F = " );
121 Exp_PrintLit( nVars, Vec_IntEntryLast(p) );
122 Abc_Print( 1, "\n" );
123}
124static inline Vec_Int_t * Exp_Reverse( Vec_Int_t * p )
125{
126 Vec_IntReverseOrder( p );
127 return p;
128}
129static inline void Exp_PrintReverse( int nVars, Vec_Int_t * p )
130{
131 Exp_Reverse( p );
132 Exp_Print( nVars, p );
133 Exp_Reverse( p );
134}
135static inline Vec_Int_t * Exp_And( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1, int fCompl0, int fCompl1 )
136{
137 int i, Len0 = Vec_IntSize(p0), Len1 = Vec_IntSize(p1);
138 Vec_Int_t * r = Vec_IntAlloc( Len0 + Len1 + 1 );
139 assert( (Len0 & 1) && (Len1 & 1) );
140 Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2) );
141 Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, 0) ^ fCompl0, Len1/2 ) );
142 Vec_IntPush( r, Vec_IntEntry(p1, 0) ^ fCompl1 );
143 for ( i = 1; i < Len0; i++ )
144 Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, i), Len1/2 ) );
145 for ( i = 1; i < Len1; i++ )
146 Vec_IntPush( r, Vec_IntEntry(p1, i) );
147 assert( Vec_IntSize(r) == Len0 + Len1 + 1 );
148 return r;
149}
150static inline Vec_Int_t * Exp_Or( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1 )
151{
152 return Exp_Not( Exp_And(pMan, nVars, p0, p1, 1, 1) );
153}
154static inline Vec_Int_t * Exp_Xor( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1 )
155{
156 int i, Len0 = Vec_IntSize(p0), Len1 = Vec_IntSize(p1);
157 Vec_Int_t * r = Vec_IntAlloc( Len0 + Len1 + 5 );
158 assert( (Len0 & 1) && (Len1 & 1) );
159 Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 2) );
160 Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 1) + 1 );
161 Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 0) + 1 );
162 Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, 0) ^ 1, Len1/2 ) );
163 Vec_IntPush( r, Vec_IntEntry(p1, 0) );
164 Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, 0), Len1/2 ) );
165 Vec_IntPush( r, Vec_IntEntry(p1, 0) ^ 1 );
166 for ( i = 1; i < Len0; i++ )
167 Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, i), Len1/2 ) );
168 for ( i = 1; i < Len1; i++ )
169 Vec_IntPush( r, Vec_IntEntry(p1, i) );
170 assert( Vec_IntSize(r) == Len0 + Len1 + 5 );
171 return Exp_Not( r );
172}
173static inline word Exp_Truth6Lit( int nVars, int Lit, word * puFanins, word * puNodes )
174{
175 if ( Lit == EXP_CONST0 )
176 return 0;
177 if ( Lit == EXP_CONST1 )
178 return ~(word)0;
179 if ( Lit < 2 * nVars )
180 return (Lit&1) ? ~puFanins[Lit/2] : puFanins[Lit/2];
181 return (Lit&1) ? ~puNodes[Lit/2-nVars] : puNodes[Lit/2-nVars];
182}
183static inline word Exp_Truth6( int nVars, Vec_Int_t * p, word * puFanins )
184{
185 static word Truth6[6] = {
186 ABC_CONST(0xAAAAAAAAAAAAAAAA),
187 ABC_CONST(0xCCCCCCCCCCCCCCCC),
188 ABC_CONST(0xF0F0F0F0F0F0F0F0),
189 ABC_CONST(0xFF00FF00FF00FF00),
190 ABC_CONST(0xFFFF0000FFFF0000),
191 ABC_CONST(0xFFFFFFFF00000000)
192 };
193 word * puNodes, Res;
194 int i;
195 if ( puFanins == NULL )
196 puFanins = (word *)Truth6;
197 puNodes = ABC_CALLOC( word, Exp_NodeNum(p) );
198 for ( i = 0; i < Exp_NodeNum(p); i++ )
199 puNodes[i] = Exp_Truth6Lit( nVars, Vec_IntEntry(p, 2*i+0), puFanins, puNodes ) &
200 Exp_Truth6Lit( nVars, Vec_IntEntry(p, 2*i+1), puFanins, puNodes );
201 Res = Exp_Truth6Lit( nVars, Vec_IntEntryLast(p), puFanins, puNodes );
202 ABC_FREE( puNodes );
203 return Res;
204}
205static inline void Exp_Truth8( int nVars, Vec_Int_t * p, word ** puFanins, word * puRes )
206{
207 word Truth8[8][4] = {
208 { ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA) },
209 { ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC) },
210 { ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0) },
211 { ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00) },
212 { ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000) },
213 { ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000) },
214 { ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF) },
215 { ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) }
216 };
217 word * puFaninsInt[8], * pStore, * pThis = NULL;
218 int i, k, iRoot = Vec_IntEntryLast(p);
219 if ( puFanins == NULL )
220 {
221 puFanins = puFaninsInt;
222 for ( k = 0; k < 8; k++ )
223 puFanins[k] = Truth8[k];
224 }
225 if ( Exp_NodeNum(p) == 0 )
226 {
227 assert( iRoot < 2 * nVars );
228 if ( iRoot == EXP_CONST0 || iRoot == EXP_CONST1 )
229 for ( k = 0; k < 4; k++ )
230 puRes[k] = iRoot == EXP_CONST0 ? 0 : ~(word)0;
231 else
232 for ( k = 0; k < 4; k++ )
233 puRes[k] = Abc_LitIsCompl(iRoot) ? ~puFanins[Abc_Lit2Var(iRoot)][k] : puFanins[Abc_Lit2Var(iRoot)][k];
234 return;
235 }
236 pStore = ABC_CALLOC( word, 4 * Exp_NodeNum(p) );
237 for ( i = 0; i < Exp_NodeNum(p); i++ )
238 {
239 int iVar0 = Abc_Lit2Var( Vec_IntEntry(p, 2*i+0) );
240 int iVar1 = Abc_Lit2Var( Vec_IntEntry(p, 2*i+1) );
241 int fCompl0 = Abc_LitIsCompl( Vec_IntEntry(p, 2*i+0) );
242 int fCompl1 = Abc_LitIsCompl( Vec_IntEntry(p, 2*i+1) );
243 word * pIn0 = iVar0 < nVars ? puFanins[iVar0] : pStore + 4 * (iVar0 - nVars);
244 word * pIn1 = iVar1 < nVars ? puFanins[iVar1] : pStore + 4 * (iVar1 - nVars);
245 pThis = pStore + 4 * i;
246 if ( fCompl0 && fCompl1 )
247 for ( k = 0; k < 4; k++ )
248 pThis[k] = ~pIn0[k] & ~pIn1[k];
249 else if ( fCompl0 && !fCompl1 )
250 for ( k = 0; k < 4; k++ )
251 pThis[k] = ~pIn0[k] & pIn1[k];
252 else if ( !fCompl0 && fCompl1 )
253 for ( k = 0; k < 4; k++ )
254 pThis[k] = pIn0[k] & ~pIn1[k];
255 else //if ( !fCompl0 && !fCompl1 )
256 for ( k = 0; k < 4; k++ )
257 pThis[k] = pIn0[k] & pIn1[k];
258 }
259 assert( Abc_Lit2Var(iRoot) - nVars == i - 1 );
260 for ( k = 0; k < 4; k++ )
261 puRes[k] = Abc_LitIsCompl(iRoot) ? ~pThis[k] : pThis[k];
262 ABC_FREE( pStore );
263}
264static inline void Exp_TruthLit( int nVars, int Lit, word ** puFanins, word ** puNodes, word * pRes, int nWords )
265{
266 int w;
267 if ( Lit == EXP_CONST0 )
268 for ( w = 0; w < nWords; w++ )
269 pRes[w] = 0;
270 else if ( Lit == EXP_CONST1 )
271 for ( w = 0; w < nWords; w++ )
272 pRes[w] = ~(word)0;
273 else if ( Lit < 2 * nVars )
274 for ( w = 0; w < nWords; w++ )
275 pRes[w] = (Lit&1) ? ~puFanins[Lit/2][w] : puFanins[Lit/2][w];
276 else
277 for ( w = 0; w < nWords; w++ )
278 pRes[w] = (Lit&1) ? ~puNodes[Lit/2-nVars][w] : puNodes[Lit/2-nVars][w];
279}
280static inline void Exp_Truth( int nVars, Vec_Int_t * p, word * pRes )
281{
282 static word Truth6[6] = {
283 ABC_CONST(0xAAAAAAAAAAAAAAAA),
284 ABC_CONST(0xCCCCCCCCCCCCCCCC),
285 ABC_CONST(0xF0F0F0F0F0F0F0F0),
286 ABC_CONST(0xFF00FF00FF00FF00),
287 ABC_CONST(0xFFFF0000FFFF0000),
288 ABC_CONST(0xFFFFFFFF00000000)
289 };
290 word ** puFanins, ** puNodes, * pTemp0, * pTemp1;
291 int i, w, nWords = (nVars <= 6 ? 1 : 1 << (nVars-6));
292 // create elementary variables
293 puFanins = ABC_ALLOC( word *, nVars );
294 for ( i = 0; i < nVars; i++ )
295 puFanins[i] = ABC_ALLOC( word, nWords );
296 // assign elementary truth tables
297 for ( i = 0; i < nVars; i++ )
298 if ( i < 6 )
299 for ( w = 0; w < nWords; w++ )
300 puFanins[i][w] = Truth6[i];
301 else
302 for ( w = 0; w < nWords; w++ )
303 puFanins[i][w] = (w & (1 << (i-6))) ? ~(word)0 : 0;
304 // create intermediate nodes
305 puNodes = ABC_ALLOC( word *, Exp_NodeNum(p) );
306 for ( i = 0; i < Exp_NodeNum(p); i++ )
307 puNodes[i] = ABC_ALLOC( word, nWords );
308 // evaluate the expression
309 pTemp0 = ABC_ALLOC( word, nWords );
310 pTemp1 = ABC_ALLOC( word, nWords );
311 for ( i = 0; i < Exp_NodeNum(p); i++ )
312 {
313 Exp_TruthLit( nVars, Vec_IntEntry(p, 2*i+0), puFanins, puNodes, pTemp0, nWords );
314 Exp_TruthLit( nVars, Vec_IntEntry(p, 2*i+1), puFanins, puNodes, pTemp1, nWords );
315 for ( w = 0; w < nWords; w++ )
316 puNodes[i][w] = pTemp0[w] & pTemp1[w];
317 }
318 ABC_FREE( pTemp0 );
319 ABC_FREE( pTemp1 );
320 // copy the final result
321 Exp_TruthLit( nVars, Vec_IntEntryLast(p), puFanins, puNodes, pRes, nWords );
322 // cleanup
323 for ( i = 0; i < nVars; i++ )
324 ABC_FREE( puFanins[i] );
325 ABC_FREE( puFanins );
326 for ( i = 0; i < Exp_NodeNum(p); i++ )
327 ABC_FREE( puNodes[i] );
328 ABC_FREE( puNodes );
329}
330
334
335ABC_NAMESPACE_HEADER_END
336
337
338#endif
339
343
nWords
int nWords
Definition abcNpn.c:127
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_END
Definition abc_namespaces.h:51
ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition abc_namespaces.h:50
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
p
Cube * p
Definition exorList.c:222
EXP_CONST1
#define EXP_CONST1
Definition exp.h:44
EXP_CONST0
#define EXP_CONST0
INCLUDES ///.
Definition exp.h:43
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
assert
#define assert(ex)
Definition util_old.h:213