1 /**CFile****************************************************************
2
3 FileName [exp.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Boolean expression.]
8
9 Synopsis [External declarations.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: exp.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__map__mio__exp_h
22 #define ABC__map__mio__exp_h
23
24 ////////////////////////////////////////////////////////////////////////
25 /// INCLUDES ///
26 ////////////////////////////////////////////////////////////////////////
27
28 ////////////////////////////////////////////////////////////////////////
29 /// PARAMETERS ///
30 ////////////////////////////////////////////////////////////////////////
31
32
33 ABC_NAMESPACE_HEADER_START
34
35 ////////////////////////////////////////////////////////////////////////
36 /// BASIC TYPES ///
37 ////////////////////////////////////////////////////////////////////////
38
39 ////////////////////////////////////////////////////////////////////////
40 /// MACRO DEFINITIONS ///
41 ////////////////////////////////////////////////////////////////////////
42
43 #define EXP_CONST0 -1
44 #define EXP_CONST1 -2
45
Exp_Const0()46 static 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 }
Exp_Const1()53 static 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 }
Exp_IsConst(Vec_Int_t * p)60 static inline int Exp_IsConst( Vec_Int_t * p )
61 {
62 return Vec_IntEntry(p,0) == EXP_CONST0 || Vec_IntEntry(p,0) == EXP_CONST1;
63 }
Exp_IsConst0(Vec_Int_t * p)64 static inline int Exp_IsConst0( Vec_Int_t * p )
65 {
66 return Vec_IntEntry(p,0) == EXP_CONST0;
67 }
Exp_IsConst1(Vec_Int_t * p)68 static inline int Exp_IsConst1( Vec_Int_t * p )
69 {
70 return Vec_IntEntry(p,0) == EXP_CONST1;
71 }
Exp_Var(int iVar)72 static 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 }
Exp_LitShift(int nVars,int Lit,int Shift)79 static 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 }
Exp_IsLit(Vec_Int_t * p)85 static inline int Exp_IsLit( Vec_Int_t * p )
86 {
87 return Vec_IntSize(p) == 1 && !Exp_IsConst(p);
88 }
Exp_NodeNum(Vec_Int_t * p)89 static inline int Exp_NodeNum( Vec_Int_t * p )
90 {
91 return Vec_IntSize(p)/2;
92 }
Exp_Not(Vec_Int_t * p)93 static 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 }
Exp_PrintLit(int nVars,int Lit)98 static 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 }
Exp_Print(int nVars,Vec_Int_t * p)109 static 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 }
Exp_Reverse(Vec_Int_t * p)124 static inline Vec_Int_t * Exp_Reverse( Vec_Int_t * p )
125 {
126 Vec_IntReverseOrder( p );
127 return p;
128 }
Exp_PrintReverse(int nVars,Vec_Int_t * p)129 static 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 }
Exp_And(int * pMan,int nVars,Vec_Int_t * p0,Vec_Int_t * p1,int fCompl0,int fCompl1)135 static 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 }
Exp_Or(int * pMan,int nVars,Vec_Int_t * p0,Vec_Int_t * p1)150 static 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 }
Exp_Xor(int * pMan,int nVars,Vec_Int_t * p0,Vec_Int_t * p1)154 static 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 }
Exp_Truth6Lit(int nVars,int Lit,word * puFanins,word * puNodes)173 static 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 }
Exp_Truth6(int nVars,Vec_Int_t * p,word * puFanins)183 static 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 }
Exp_Truth8(int nVars,Vec_Int_t * p,word ** puFanins,word * puRes)205 static 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 }
Exp_TruthLit(int nVars,int Lit,word ** puFanins,word ** puNodes,word * pRes,int nWords)264 static 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 }
Exp_Truth(int nVars,Vec_Int_t * p,word * pRes)280 static 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
331 ////////////////////////////////////////////////////////////////////////
332 /// FUNCTION DECLARATIONS ///
333 ////////////////////////////////////////////////////////////////////////
334
335 ABC_NAMESPACE_HEADER_END
336
337
338 #endif
339
340 ////////////////////////////////////////////////////////////////////////
341 /// END OF FILE ///
342 ////////////////////////////////////////////////////////////////////////
343
344