ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
ifCount.h
Go to the documentation of this file.
1
20
21#ifndef ABC__map__if__if_Count_h
22#define ABC__map__if__if_Count_h
23
27
28ABC_NAMESPACE_HEADER_START
29
33
37
41
45
57static inline int If_LogCreateAnd( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll )
58{
59 int iObjId = Vec_IntSize(vAig)/2 + nSuppAll;
60 assert( Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
61 Vec_IntPush( vAig, iLit0 );
62 Vec_IntPush( vAig, iLit1 );
63 return Abc_Var2Lit( iObjId, 0 );
64}
65static inline int If_LogCreateMux( Vec_Int_t * vAig, int iLitC, int iLit1, int iLit0, int nSuppAll )
66{
67 int iFanLit0 = If_LogCreateAnd( vAig, iLitC, iLit1, nSuppAll );
68 int iFanLit1 = If_LogCreateAnd( vAig, Abc_LitNot(iLitC), iLit0, nSuppAll );
69 int iResLit = If_LogCreateAnd( vAig, Abc_LitNot(iFanLit0), Abc_LitNot(iFanLit1), nSuppAll );
70 return Abc_LitNot(iResLit);
71}
72static inline int If_LogCreateXor( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll )
73{
74 return If_LogCreateMux( vAig, iLit0, Abc_LitNot(iLit1), iLit1, nSuppAll );
75}
76static inline int If_LogCreateAndXor( Vec_Int_t * vAig, int iLit0, int iLit1, int nSuppAll, int fXor )
77{
78 return fXor ? If_LogCreateXor(vAig, iLit0, iLit1, nSuppAll) : If_LogCreateAnd(vAig, iLit0, iLit1, nSuppAll);
79}
80static inline int If_LogCreateAndXorMulti( Vec_Int_t * vAig, int * pFaninLits, int nFanins, int nSuppAll, int fXor )
81{
82 int i;
83 assert( nFanins > 0 );
84 for ( i = nFanins - 1; i > 0; i-- )
85 pFaninLits[i-1] = If_LogCreateAndXor( vAig, pFaninLits[i], pFaninLits[i-1], nSuppAll, fXor );
86 return pFaninLits[0];
87}
88static inline int If_LogCounterAddAig( int * pTimes, int * pnTimes, int * pFaninLits, int Num, int iLit, Vec_Int_t * vAig, int nSuppAll, int fXor, int fXorFunc )
89{
90 int nTimes = *pnTimes;
91 if ( vAig )
92 pFaninLits[nTimes] = iLit;
93 pTimes[nTimes++] = Num;
94 if ( nTimes > 1 )
95 {
96 int i, k;
97 for ( k = nTimes-1; k > 0; k-- )
98 {
99 if ( pTimes[k] < pTimes[k-1] )
100 break;
101 if ( pTimes[k] > pTimes[k-1] )
102 {
103 ABC_SWAP( int, pTimes[k], pTimes[k-1] );
104 if ( vAig )
105 ABC_SWAP( int, pFaninLits[k], pFaninLits[k-1] );
106 continue;
107 }
108 pTimes[k-1] += 1 + fXor;
109 if ( vAig )
110 pFaninLits[k-1] = If_LogCreateAndXor( vAig, pFaninLits[k], pFaninLits[k-1], nSuppAll, fXorFunc );
111 for ( nTimes--, i = k; i < nTimes; i++ )
112 {
113 pTimes[i] = pTimes[i+1];
114 if ( vAig )
115 pFaninLits[i] = pFaninLits[i+1];
116 }
117 }
118 }
119 assert( nTimes > 0 );
120 *pnTimes = nTimes;
121 return pTimes[0] + (nTimes > 1 ? 1 + fXor : 0);
122}
123static inline int If_LogCounterDelayXor( int * pTimes, int nTimes )
124{
125 int i;
126 assert( nTimes > 0 );
127 for ( i = nTimes - 1; i > 0; i-- )
128 pTimes[i-1] = 2 + Abc_MaxInt( pTimes[i], pTimes[i-1] );
129 return pTimes[0];
130}
131
132
144static inline int If_CutPinDelayGet( word D, int v ) { assert(v >= 0 && v < 16); return (int)((D >> (v << 2)) & 0xF); }
145static inline void If_CutPinDelaySet( word * pD, int v, int d ) { assert(v >= 0 && v < 16); assert(d >= 0 && d < 16); *pD |= ((word)d << (v << 2)); }
146static inline word If_CutPinDelayInit( int v ) { assert(v >= 0 && v < 16); return (word)1 << (v << 2); }
147static inline word If_CutPinDelayMax( word D1, word D2, int nVars, int AddOn )
148{
149 int v, Max;
150 word D = 0;
151 for ( v = 0; v < nVars; v++ )
152 if ( (Max = Abc_MaxInt(If_CutPinDelayGet(D1, v), If_CutPinDelayGet(D2, v))) )
153 If_CutPinDelaySet( &D, v, Abc_MinInt(Max + AddOn, 15) );
154 return D;
155}
156static inline word If_CutPinDelayDecrement( word D1, int nVars )
157{
158 int v;
159 word D = 0;
160 for ( v = 0; v < nVars; v++ )
161 if ( If_CutPinDelayGet(D1, v) )
162 If_CutPinDelaySet( &D, v, If_CutPinDelayGet(D1, v) - 1 );
163 return D;
164}
165static inline int If_CutPinDelayEqual( word D1, word D2, int nVars ) // returns 1 if D1 has the same delays than D2
166{
167 int v;
168 for ( v = 0; v < nVars; v++ )
169 if ( If_CutPinDelayGet(D1, v) != If_CutPinDelayGet(D2, v) )
170 return 0;
171 return 1;
172}
173static inline int If_CutPinDelayDom( word D1, word D2, int nVars ) // returns 1 if D1 has the same or smaller delays than D2
174{
175 int v;
176 for ( v = 0; v < nVars; v++ )
177 if ( If_CutPinDelayGet(D1, v) > If_CutPinDelayGet(D2, v) )
178 return 0;
179 return 1;
180}
181static inline void If_CutPinDelayTranslate( word D, int nVars, char * pPerm )
182{
183 int v, Delay;
184 for ( v = 0; v < nVars; v++ )
185 {
186 Delay = If_CutPinDelayGet(D, v);
187 assert( Delay > 1 );
188 pPerm[v] = Delay - 1;
189 }
190}
191static inline void If_CutPinDelayPrint( word D, int nVars )
192{
193 int v;
194 printf( "Delay profile = {" );
195 for ( v = 0; v < nVars; v++ )
196 printf( " %d", If_CutPinDelayGet(D, v) );
197 printf( " }\n" );
198}
199static inline int If_LogCounterPinDelays( int * pTimes, int * pnTimes, word * pPinDels, int Num, word PinDel, int nSuppAll, int fXor )
200{
201 int nTimes = *pnTimes;
202 pPinDels[nTimes] = PinDel;
203 pTimes[nTimes++] = Num;
204 if ( nTimes > 1 )
205 {
206 int i, k;
207 for ( k = nTimes-1; k > 0; k-- )
208 {
209 if ( pTimes[k] < pTimes[k-1] )
210 break;
211 if ( pTimes[k] > pTimes[k-1] )
212 {
213 ABC_SWAP( int, pTimes[k], pTimes[k-1] );
214 ABC_SWAP( word, pPinDels[k], pPinDels[k-1] );
215 continue;
216 }
217 pTimes[k-1] += 1 + fXor;
218 pPinDels[k-1] = If_CutPinDelayMax( pPinDels[k], pPinDels[k-1], nSuppAll, 1 + fXor );
219 for ( nTimes--, i = k; i < nTimes; i++ )
220 {
221 pTimes[i] = pTimes[i+1];
222 pPinDels[i] = pPinDels[i+1];
223 }
224 }
225 }
226 assert( nTimes > 0 );
227 *pnTimes = nTimes;
228 return pTimes[0] + (nTimes > 1 ? 1 + fXor : 0);
229}
230static inline word If_LogPinDelaysMulti( word * pPinDels, int nFanins, int nSuppAll, int fXor )
231{
232 int i;
233 assert( nFanins > 0 );
234 for ( i = nFanins - 1; i > 0; i-- )
235 pPinDels[i-1] = If_CutPinDelayMax( pPinDels[i], pPinDels[i-1], nSuppAll, 1 + fXor );
236 return pPinDels[0];
237}
238
239
251static inline word If_AigVerifyArray( Vec_Int_t * vAig, int nLeaves )
252{
253 assert( Vec_IntSize(vAig) > 0 );
254 assert( Vec_IntEntryLast(vAig) < 2 );
255 if ( Vec_IntSize(vAig) == 1 ) // const
256 return Vec_IntEntry(vAig, 0) ? ~((word)0) : 0;
257 if ( Vec_IntSize(vAig) == 2 ) // variable
258 {
259 assert( Vec_IntEntry(vAig, 0) == 0 );
260 return Vec_IntEntry(vAig, 1) ? ~s_Truths6[0] : s_Truths6[0];
261 }
262 else
263 {
264 word Truth0 = 0, Truth1 = 0, TruthR;
265 int i, iVar0, iVar1, iLit0, iLit1;
266 assert( Vec_IntSize(vAig) & 1 );
267 Vec_IntForEachEntryDouble( vAig, iLit0, iLit1, i )
268 {
269 iVar0 = Abc_Lit2Var( iLit0 );
270 iVar1 = Abc_Lit2Var( iLit1 );
271 Truth0 = iVar0 < nLeaves ? s_Truths6[iVar0] : Vec_WrdEntry( (Vec_Wrd_t *)vAig, iVar0 - nLeaves );
272 Truth1 = iVar1 < nLeaves ? s_Truths6[iVar1] : Vec_WrdEntry( (Vec_Wrd_t *)vAig, iVar1 - nLeaves );
273 if ( Abc_LitIsCompl(iLit0) )
274 Truth0 = ~Truth0;
275 if ( Abc_LitIsCompl(iLit1) )
276 Truth1 = ~Truth1;
277 assert( (i & 1) == 0 );
278 Vec_WrdWriteEntry( (Vec_Wrd_t *)vAig, Abc_Lit2Var(i), Truth0 & Truth1 ); // overwriting entries
279 }
280 assert( i == Vec_IntSize(vAig) - 1 );
281 TruthR = Truth0 & Truth1;
282 if ( Vec_IntEntry(vAig, i) )
283 TruthR = ~TruthR;
284 Vec_IntClear( vAig ); // useless
285 return TruthR;
286 }
287}
288
300static inline void If_AigPrintArray( Vec_Int_t * vAig, int nLeaves )
301{
302 assert( Vec_IntSize(vAig) > 0 );
303 assert( Vec_IntEntryLast(vAig) < 2 );
304 if ( Vec_IntSize(vAig) == 1 ) // const
305 printf( "Const %d\n", Vec_IntEntry(vAig, 0) );
306 else if ( Vec_IntSize(vAig) == 2 ) // variable
307 printf( "Variable %s\n", Vec_IntEntry(vAig, 1) ? "Compl" : "" );
308 else
309 {
310 int i, iLit0, iLit1;
311 assert( Vec_IntSize(vAig) & 1 );
312 Vec_IntForEachEntryDouble( vAig, iLit0, iLit1, i )
313 printf( "%d %d\n", iLit0, iLit1 );
314 assert( i == Vec_IntSize(vAig) - 1 );
315 printf( "%s\n", Vec_IntEntry(vAig, i) ? "Compl" : "" );
316 }
317}
318
319
331static inline int If_LogCounter64Eval( word Count )
332{
333 int n = ((Count & (Count - 1)) > 0) ? -1 : 0;
334 assert( Count > 0 );
335 if ( (Count & ABC_CONST(0xFFFFFFFF00000000)) == 0 ) { n += 32; Count <<= 32; }
336 if ( (Count & ABC_CONST(0xFFFF000000000000)) == 0 ) { n += 16; Count <<= 16; }
337 if ( (Count & ABC_CONST(0xFF00000000000000)) == 0 ) { n += 8; Count <<= 8; }
338 if ( (Count & ABC_CONST(0xF000000000000000)) == 0 ) { n += 4; Count <<= 4; }
339 if ( (Count & ABC_CONST(0xC000000000000000)) == 0 ) { n += 2; Count <<= 2; }
340 if ( (Count & ABC_CONST(0x8000000000000000)) == 0 ) { n++; }
341 return 63 - n;
342}
343static word If_LogCounter64Add( word Count, int Num )
344{
345 assert( Num < 48 );
346 return Count + (((word)1) << Num);
347}
348
361static int If_LogCounter32Eval( unsigned Count, int Start )
362{
363 int n = (Abc_LitIsCompl(Start) || (Count & (Count - 1)) > 0) ? -1 : 0;
364 assert( Count > 0 );
365 if ( (Count & 0xFFFF0000) == 0 ) { n += 16; Count <<= 16; }
366 if ( (Count & 0xFF000000) == 0 ) { n += 8; Count <<= 8; }
367 if ( (Count & 0xF0000000) == 0 ) { n += 4; Count <<= 4; }
368 if ( (Count & 0xC0000000) == 0 ) { n += 2; Count <<= 2; }
369 if ( (Count & 0x80000000) == 0 ) { n++; }
370 return Abc_Lit2Var(Start) + 31 - n;
371}
372static unsigned If_LogCounter32Add( unsigned Count, int * pStart, int Num )
373{
374 int Start = Abc_Lit2Var(*pStart);
375 if ( Num < Start )
376 {
377 *pStart |= 1;
378 return Count;
379 }
380 if ( Num > Start + 16 )
381 {
382 int Shift = Num - (Start + 16);
383 if ( !Abc_LitIsCompl(*pStart) && (Shift >= 32 ? Count : Count & ~(~0 << Shift)) > 0 )
384 *pStart |= 1;
385 Count >>= Shift;
386 Start += Shift;
387 *pStart = Abc_Var2Lit( Start, Abc_LitIsCompl(*pStart) );
388 assert( Num <= Start + 16 );
389 }
390 return Count + (1 << (Num-Start));
391}
392
404/*
405void If_LogCounterTest2()
406{
407 word Count64 = 0;
408
409 unsigned Count = 0;
410 int Start = 0;
411
412 int Result, Result64;
413
414 Count = If_LogCounter32Add( Count, &Start, 39 );
415 Count = If_LogCounter32Add( Count, &Start, 35 );
416 Count = If_LogCounter32Add( Count, &Start, 35 );
417 Count = If_LogCounter32Add( Count, &Start, 36 );
418 Count = If_LogCounter32Add( Count, &Start, 37 );
419 Count = If_LogCounter32Add( Count, &Start, 38 );
420 Count = If_LogCounter32Add( Count, &Start, 40 );
421 Count = If_LogCounter32Add( Count, &Start, 1 );
422 Count = If_LogCounter32Add( Count, &Start, 41 );
423 Count = If_LogCounter32Add( Count, &Start, 42 );
424
425 Count64 = If_LogCounter64Add( Count64, 1 );
426 Count64 = If_LogCounter64Add( Count64, 35 );
427 Count64 = If_LogCounter64Add( Count64, 35 );
428 Count64 = If_LogCounter64Add( Count64, 36 );
429 Count64 = If_LogCounter64Add( Count64, 37 );
430 Count64 = If_LogCounter64Add( Count64, 38 );
431 Count64 = If_LogCounter64Add( Count64, 39 );
432 Count64 = If_LogCounter64Add( Count64, 40 );
433 Count64 = If_LogCounter64Add( Count64, 41 );
434 Count64 = If_LogCounter64Add( Count64, 42 );
435
436 Result = If_LogCounter32Eval( Count, Start );
437 Result64 = If_LogCounter64Eval( Count64 );
438
439 printf( "%d %d\n", Result, Result64 );
440}
441*/
442
454static inline int If_LogCounterAdd( int * pTimes, int * pnTimes, int Num, int fXor )
455{
456 int nTimes = *pnTimes;
457 pTimes[nTimes++] = Num;
458 if ( nTimes > 1 )
459 {
460 int i, k;
461 for ( k = nTimes-1; k > 0; k-- )
462 {
463 if ( pTimes[k] < pTimes[k-1] )
464 break;
465 if ( pTimes[k] > pTimes[k-1] )
466 {
467 ABC_SWAP( int, pTimes[k], pTimes[k-1] );
468 continue;
469 }
470 pTimes[k-1] += 1 + fXor;
471 for ( nTimes--, i = k; i < nTimes; i++ )
472 pTimes[i] = pTimes[i+1];
473 }
474 }
475 assert( nTimes > 0 );
476 *pnTimes = nTimes;
477 return pTimes[0] + (nTimes > 1 ? 1 + fXor : 0);
478}
479
491/*
492void If_LogCounterTest()
493{
494 int pArray[10] = { 1, 2, 4, 5, 6, 3, 1 };
495 int i, nSize = 4;
496
497 word Count64 = 0;
498 int Result, Result64;
499
500 int pTimes[100];
501 int nTimes = 0;
502
503 for ( i = 0; i < nSize; i++ )
504 Count64 = If_LogCounter64Add( Count64, pArray[i] );
505 Result64 = If_LogCounter64Eval( Count64 );
506
507 for ( i = 0; i < nSize; i++ )
508 Result = If_LogCounterAdd( pTimes, &nTimes, pArray[i], 0 );
509
510 printf( "%d %d\n", Result64, Result );
511}
512*/
513
514ABC_NAMESPACE_HEADER_END
515
516#endif
517
521
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
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
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42