ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
sbdCut.c
Go to the documentation of this file.
1
20
21#include "sbdInt.h"
22
24
25
29
30#define SBD_MAX_CUTSIZE 10
31#define SBD_MAX_CUTNUM 501
32#define SBD_MAX_TT_WORDS ((SBD_MAX_CUTSIZE > 6) ? 1 << (SBD_MAX_CUTSIZE-6) : 1)
33
34#define SBD_CUT_NO_LEAF 0xF
35
36typedef struct Sbd_Cut_t_ Sbd_Cut_t;
38{
39 word Sign; // signature
40 int iFunc; // functionality
41 int Cost; // cut cost
42 int CostLev; // cut cost
43 unsigned nTreeLeaves : 9; // tree leaves
44 unsigned nSlowLeaves : 9; // slow leaves
45 unsigned nTopLeaves : 10; // top leaves
46 unsigned nLeaves : 4; // leaf count
47 int pLeaves[SBD_MAX_CUTSIZE]; // leaves
48};
49
51{
57 Gia_Man_t * pGia; // user's AIG manager (will be modified by adding nodes)
58 Vec_Int_t * vMirrors; // mirrors for each node
59 Vec_Int_t * vDelays; // delays for each node
60 Vec_Int_t * vLevels; // levels for each node
61 Vec_Int_t * vRefs; // refs for each node
62 Vec_Wec_t * vCuts; // cuts for each node
63 Vec_Mem_t * vTtMem; // truth tables
64 Sbd_Cut_t pCuts[3][SBD_MAX_CUTNUM]; // temporary cuts
65 Sbd_Cut_t * ppCuts[SBD_MAX_CUTNUM]; // temporary cut pointers
66 int nCutsR; // the number of cuts
67 int Pivot; // current object
68 int iCutBest; // best-delay cut
69 int nCutsSpec; // special cuts
70 int nCutsOver; // overflow cuts
71 int DelayMin; // minimum delay
72 double CutCount[4]; // cut counters
73 abctime clkStart; // starting time
74};
75
76static inline word * Sbd_CutTruth( Sbd_Sto_t * p, Sbd_Cut_t * pCut ) { return Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut->iFunc)); }
77
78#define Sbd_ForEachCut( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 2 )
79
83
95static inline word Sbd_CutGetSign( Sbd_Cut_t * pCut )
96{
97 word Sign = 0; int i;
98 for ( i = 0; i < (int)pCut->nLeaves; i++ )
99 Sign |= ((word)1) << (pCut->pLeaves[i] & 0x3F);
100 return Sign;
101}
102static inline int Sbd_CutCheck( Sbd_Cut_t * pBase, Sbd_Cut_t * pCut ) // check if pCut is contained in pBase
103{
104 int nSizeB = pBase->nLeaves;
105 int nSizeC = pCut->nLeaves;
106 int i, * pB = pBase->pLeaves;
107 int k, * pC = pCut->pLeaves;
108 for ( i = 0; i < nSizeC; i++ )
109 {
110 for ( k = 0; k < nSizeB; k++ )
111 if ( pC[i] == pB[k] )
112 break;
113 if ( k == nSizeB )
114 return 0;
115 }
116 return 1;
117}
118static inline int Sbd_CutSetCheckArray( Sbd_Cut_t ** ppCuts, int nCuts )
119{
120 Sbd_Cut_t * pCut0, * pCut1;
121 int i, k, m, n, Value;
122 assert( nCuts > 0 );
123 for ( i = 0; i < nCuts; i++ )
124 {
125 pCut0 = ppCuts[i];
126 assert( pCut0->nLeaves <= SBD_MAX_CUTSIZE );
127 assert( pCut0->Sign == Sbd_CutGetSign(pCut0) );
128 // check duplicates
129 for ( m = 0; m < (int)pCut0->nLeaves; m++ )
130 for ( n = m + 1; n < (int)pCut0->nLeaves; n++ )
131 assert( pCut0->pLeaves[m] < pCut0->pLeaves[n] );
132 // check pairs
133 for ( k = 0; k < nCuts; k++ )
134 {
135 pCut1 = ppCuts[k];
136 if ( pCut0 == pCut1 )
137 continue;
138 // check containments
139 Value = Sbd_CutCheck( pCut0, pCut1 );
140 assert( Value == 0 );
141 }
142 }
143 return 1;
144}
145
146
158static inline int Sbd_CutMergeOrder( Sbd_Cut_t * pCut0, Sbd_Cut_t * pCut1, Sbd_Cut_t * pCut, int nCutSize )
159{
160 int nSize0 = pCut0->nLeaves;
161 int nSize1 = pCut1->nLeaves;
162 int i, * pC0 = pCut0->pLeaves;
163 int k, * pC1 = pCut1->pLeaves;
164 int c, * pC = pCut->pLeaves;
165 // the case of the largest cut sizes
166 if ( nSize0 == nCutSize && nSize1 == nCutSize )
167 {
168 for ( i = 0; i < nSize0; i++ )
169 {
170 if ( pC0[i] != pC1[i] ) return 0;
171 pC[i] = pC0[i];
172 }
173 pCut->nLeaves = nCutSize;
174 pCut->iFunc = -1;
175 pCut->Sign = pCut0->Sign | pCut1->Sign;
176 return 1;
177 }
178 // compare two cuts with different numbers
179 i = k = c = 0;
180 if ( nSize0 == 0 ) goto FlushCut1;
181 if ( nSize1 == 0 ) goto FlushCut0;
182 while ( 1 )
183 {
184 if ( c == nCutSize ) return 0;
185 if ( pC0[i] < pC1[k] )
186 {
187 pC[c++] = pC0[i++];
188 if ( i >= nSize0 ) goto FlushCut1;
189 }
190 else if ( pC0[i] > pC1[k] )
191 {
192 pC[c++] = pC1[k++];
193 if ( k >= nSize1 ) goto FlushCut0;
194 }
195 else
196 {
197 pC[c++] = pC0[i++]; k++;
198 if ( i >= nSize0 ) goto FlushCut1;
199 if ( k >= nSize1 ) goto FlushCut0;
200 }
201 }
202
203FlushCut0:
204 if ( c + nSize0 > nCutSize + i ) return 0;
205 while ( i < nSize0 )
206 pC[c++] = pC0[i++];
207 pCut->nLeaves = c;
208 pCut->iFunc = -1;
209 pCut->Sign = pCut0->Sign | pCut1->Sign;
210 return 1;
211
212FlushCut1:
213 if ( c + nSize1 > nCutSize + k ) return 0;
214 while ( k < nSize1 )
215 pC[c++] = pC1[k++];
216 pCut->nLeaves = c;
217 pCut->iFunc = -1;
218 pCut->Sign = pCut0->Sign | pCut1->Sign;
219 return 1;
220}
221static inline int Sbd_CutMergeOrder2( Sbd_Cut_t * pCut0, Sbd_Cut_t * pCut1, Sbd_Cut_t * pCut, int nCutSize )
222{
223 int x0, i0 = 0, nSize0 = pCut0->nLeaves, * pC0 = pCut0->pLeaves;
224 int x1, i1 = 0, nSize1 = pCut1->nLeaves, * pC1 = pCut1->pLeaves;
225 int xMin, c = 0, * pC = pCut->pLeaves;
226 while ( 1 )
227 {
228 x0 = (i0 == nSize0) ? ABC_INFINITY : pC0[i0];
229 x1 = (i1 == nSize1) ? ABC_INFINITY : pC1[i1];
230 xMin = Abc_MinInt(x0, x1);
231 if ( xMin == ABC_INFINITY ) break;
232 if ( c == nCutSize ) return 0;
233 pC[c++] = xMin;
234 if (x0 == xMin) i0++;
235 if (x1 == xMin) i1++;
236 }
237 pCut->nLeaves = c;
238 pCut->iFunc = -1;
239 pCut->Sign = pCut0->Sign | pCut1->Sign;
240 return 1;
241}
242static inline int Sbd_CutSetCutIsContainedOrder( Sbd_Cut_t * pBase, Sbd_Cut_t * pCut ) // check if pCut is contained in pBase
243{
244 int i, nSizeB = pBase->nLeaves;
245 int k, nSizeC = pCut->nLeaves;
246 if ( nSizeB == nSizeC )
247 {
248 for ( i = 0; i < nSizeB; i++ )
249 if ( pBase->pLeaves[i] != pCut->pLeaves[i] )
250 return 0;
251 return 1;
252 }
253 assert( nSizeB > nSizeC );
254 if ( nSizeC == 0 )
255 return 1;
256 for ( i = k = 0; i < nSizeB; i++ )
257 {
258 if ( pBase->pLeaves[i] > pCut->pLeaves[k] )
259 return 0;
260 if ( pBase->pLeaves[i] == pCut->pLeaves[k] )
261 {
262 if ( ++k == nSizeC )
263 return 1;
264 }
265 }
266 return 0;
267}
268static inline int Sbd_CutSetLastCutIsContained( Sbd_Cut_t ** pCuts, int nCuts )
269{
270 int i;
271 for ( i = 0; i < nCuts; i++ )
272 if ( pCuts[i]->nLeaves <= pCuts[nCuts]->nLeaves && (pCuts[i]->Sign & pCuts[nCuts]->Sign) == pCuts[i]->Sign && Sbd_CutSetCutIsContainedOrder(pCuts[nCuts], pCuts[i]) )
273 return 1;
274 return 0;
275}
276
288static inline int Sbd_CutCompare( Sbd_Cut_t * pCut0, Sbd_Cut_t * pCut1 )
289{
290 if ( pCut0->nLeaves <= 4 && pCut1->nLeaves <= 4 )
291 {
292 if ( pCut0->nLeaves < pCut1->nLeaves ) return -1;
293 if ( pCut0->nLeaves > pCut1->nLeaves ) return 1;
294 if ( pCut0->Cost < pCut1->Cost ) return -1;
295 if ( pCut0->Cost > pCut1->Cost ) return 1;
296 if ( pCut0->CostLev < pCut1->CostLev ) return -1;
297 if ( pCut0->CostLev > pCut1->CostLev ) return 1;
298 }
299 else if ( pCut0->nLeaves <= 4 )
300 return -1;
301 else if ( pCut1->nLeaves <= 4 )
302 return 1;
303 else
304 {
305 if ( pCut0->nTreeLeaves < pCut1->nTreeLeaves ) return -1;
306 if ( pCut0->nTreeLeaves > pCut1->nTreeLeaves ) return 1;
307 if ( pCut0->Cost < pCut1->Cost ) return -1;
308 if ( pCut0->Cost > pCut1->Cost ) return 1;
309 if ( pCut0->CostLev < pCut1->CostLev ) return -1;
310 if ( pCut0->CostLev > pCut1->CostLev ) return 1;
311 if ( pCut0->nLeaves < pCut1->nLeaves ) return -1;
312 if ( pCut0->nLeaves > pCut1->nLeaves ) return 1;
313 }
314 return 0;
315}
316static inline int Sbd_CutCompare2( Sbd_Cut_t * pCut0, Sbd_Cut_t * pCut1 )
317{
318 assert( pCut0->nLeaves > 4 && pCut1->nLeaves > 4 );
319 if ( pCut0->nSlowLeaves < pCut1->nSlowLeaves ) return -1;
320 if ( pCut0->nSlowLeaves > pCut1->nSlowLeaves ) return 1;
321 if ( pCut0->nTreeLeaves < pCut1->nTreeLeaves ) return -1;
322 if ( pCut0->nTreeLeaves > pCut1->nTreeLeaves ) return 1;
323 if ( pCut0->Cost < pCut1->Cost ) return -1;
324 if ( pCut0->Cost > pCut1->Cost ) return 1;
325 if ( pCut0->CostLev < pCut1->CostLev ) return -1;
326 if ( pCut0->CostLev > pCut1->CostLev ) return 1;
327 if ( pCut0->nLeaves < pCut1->nLeaves ) return -1;
328 if ( pCut0->nLeaves > pCut1->nLeaves ) return 1;
329 return 0;
330}
331
332static inline int Sbd_CutSetLastCutContains( Sbd_Cut_t ** pCuts, int nCuts )
333{
334 int i, k, fChanges = 0;
335 for ( i = 0; i < nCuts; i++ )
336 if ( pCuts[nCuts]->nLeaves < pCuts[i]->nLeaves && (pCuts[nCuts]->Sign & pCuts[i]->Sign) == pCuts[nCuts]->Sign && Sbd_CutSetCutIsContainedOrder(pCuts[i], pCuts[nCuts]) )
337 pCuts[i]->nLeaves = SBD_CUT_NO_LEAF, fChanges = 1;
338 if ( !fChanges )
339 return nCuts;
340 for ( i = k = 0; i <= nCuts; i++ )
341 {
342 if ( pCuts[i]->nLeaves == SBD_CUT_NO_LEAF )
343 continue;
344 if ( k < i )
345 ABC_SWAP( Sbd_Cut_t *, pCuts[k], pCuts[i] );
346 k++;
347 }
348 return k - 1;
349}
350static inline void Sbd_CutSetSortByCost( Sbd_Cut_t ** pCuts, int nCuts )
351{
352 int i;
353 for ( i = nCuts; i > 0; i-- )
354 {
355 if ( Sbd_CutCompare(pCuts[i - 1], pCuts[i]) < 0 )
356 return;
357 ABC_SWAP( Sbd_Cut_t *, pCuts[i - 1], pCuts[i] );
358 }
359}
360static inline int Sbd_CutSetAddCut( Sbd_Cut_t ** pCuts, int nCuts, int nCutNum )
361{
362 if ( nCuts == 0 )
363 return 1;
364 nCuts = Sbd_CutSetLastCutContains(pCuts, nCuts);
365 assert( nCuts >= 0 );
366 Sbd_CutSetSortByCost( pCuts, nCuts );
367 // add new cut if there is room
368 return Abc_MinInt( nCuts + 1, nCutNum - 1 );
369}
370
382static inline int Sbd_CutComputeTruth6( Sbd_Sto_t * p, Sbd_Cut_t * pCut0, Sbd_Cut_t * pCut1, int fCompl0, int fCompl1, Sbd_Cut_t * pCutR, int fIsXor )
383{
384 int nOldSupp = pCutR->nLeaves, truthId, fCompl; word t;
385 word t0 = *Sbd_CutTruth(p, pCut0);
386 word t1 = *Sbd_CutTruth(p, pCut1);
387 if ( Abc_LitIsCompl(pCut0->iFunc) ^ fCompl0 ) t0 = ~t0;
388 if ( Abc_LitIsCompl(pCut1->iFunc) ^ fCompl1 ) t1 = ~t1;
389 t0 = Abc_Tt6Expand( t0, pCut0->pLeaves, pCut0->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
390 t1 = Abc_Tt6Expand( t1, pCut1->pLeaves, pCut1->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
391 t = fIsXor ? t0 ^ t1 : t0 & t1;
392 if ( (fCompl = (int)(t & 1)) ) t = ~t;
393 pCutR->nLeaves = Abc_Tt6MinBase( &t, pCutR->pLeaves, pCutR->nLeaves );
394 assert( (int)(t & 1) == 0 );
395 truthId = Vec_MemHashInsert(p->vTtMem, &t);
396 pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
397 assert( (int)pCutR->nLeaves <= nOldSupp );
398 return (int)pCutR->nLeaves < nOldSupp;
399}
400static inline int Sbd_CutComputeTruth( Sbd_Sto_t * p, Sbd_Cut_t * pCut0, Sbd_Cut_t * pCut1, int fCompl0, int fCompl1, Sbd_Cut_t * pCutR, int fIsXor )
401{
402 if ( p->nCutSize <= 6 )
403 return Sbd_CutComputeTruth6( p, pCut0, pCut1, fCompl0, fCompl1, pCutR, fIsXor );
404 {
405 word uTruth[SBD_MAX_TT_WORDS], uTruth0[SBD_MAX_TT_WORDS], uTruth1[SBD_MAX_TT_WORDS];
406 int nOldSupp = pCutR->nLeaves, truthId;
407 int nCutSize = p->nCutSize, fCompl;
408 int nWords = Abc_Truth6WordNum(nCutSize);
409 word * pTruth0 = Sbd_CutTruth(p, pCut0);
410 word * pTruth1 = Sbd_CutTruth(p, pCut1);
411 Abc_TtCopy( uTruth0, pTruth0, nWords, Abc_LitIsCompl(pCut0->iFunc) ^ fCompl0 );
412 Abc_TtCopy( uTruth1, pTruth1, nWords, Abc_LitIsCompl(pCut1->iFunc) ^ fCompl1 );
413 Abc_TtExpand( uTruth0, nCutSize, pCut0->pLeaves, pCut0->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
414 Abc_TtExpand( uTruth1, nCutSize, pCut1->pLeaves, pCut1->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
415 if ( fIsXor )
416 Abc_TtXor( uTruth, uTruth0, uTruth1, nWords, (fCompl = (int)((uTruth0[0] ^ uTruth1[0]) & 1)) );
417 else
418 Abc_TtAnd( uTruth, uTruth0, uTruth1, nWords, (fCompl = (int)((uTruth0[0] & uTruth1[0]) & 1)) );
419 pCutR->nLeaves = Abc_TtMinBase( uTruth, pCutR->pLeaves, pCutR->nLeaves, nCutSize );
420 assert( (uTruth[0] & 1) == 0 );
421//Kit_DsdPrintFromTruth( uTruth, pCutR->nLeaves ), printf("\n" ), printf("\n" );
422 truthId = Vec_MemHashInsert(p->vTtMem, uTruth);
423 pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
424 assert( (int)pCutR->nLeaves <= nOldSupp );
425 return (int)pCutR->nLeaves < nOldSupp;
426 }
427}
428
440static inline int Sbd_CutCountBits( word i )
441{
442 i = i - ((i >> 1) & 0x5555555555555555);
443 i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333);
444 i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
445 return (i*(0x0101010101010101))>>56;
446}
447static inline int Sbd_CutCost( Sbd_Sto_t * p, Sbd_Cut_t * pCut )
448{
449 int i, Cost = 0;
450 for ( i = 0; i < (int)pCut->nLeaves; i++ )
451 Cost += Vec_IntEntry( p->vDelays, pCut->pLeaves[i] );
452 return Cost;
453}
454static inline int Sbd_CutCostLev( Sbd_Sto_t * p, Sbd_Cut_t * pCut )
455{
456 int i, Cost = 0;
457 for ( i = 0; i < (int)pCut->nLeaves; i++ )
458 Cost += Vec_IntEntry( p->vLevels, pCut->pLeaves[i] );
459 return Cost;
460}
461static inline int Sbd_CutTreeLeaves( Sbd_Sto_t * p, Sbd_Cut_t * pCut )
462{
463 int i, Cost = 0;
464 for ( i = 0; i < (int)pCut->nLeaves; i++ )
465 Cost += Vec_IntEntry( p->vRefs, pCut->pLeaves[i] ) == 1;
466 return Cost;
467}
468static inline int Sbd_CutSlowLeaves( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
469{
470 int i, Count = 0, Delay = Vec_IntEntry(p->vDelays, iObj);
471 for ( i = 0; i < (int)pCut->nLeaves; i++ )
472 Count += (Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay >= -1);
473 return Count;
474}
475static inline int Sbd_CutTopLeaves( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
476{
477 int i, Count = 0, Delay = Vec_IntEntry(p->vDelays, iObj);
478 for ( i = 0; i < (int)pCut->nLeaves; i++ )
479 Count += (Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay == -2);
480 return Count;
481}
482static inline void Sbd_CutAddUnit( Sbd_Sto_t * p, int iObj )
483{
484 Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
485 if ( Vec_IntSize(vThis) == 0 )
486 Vec_IntPush( vThis, 1 );
487 else
488 Vec_IntAddToEntry( vThis, 0, 1 );
489 Vec_IntPush( vThis, 1 );
490 Vec_IntPush( vThis, iObj );
491 Vec_IntPush( vThis, 2 );
492}
493static inline void Sbd_CutAddZero( Sbd_Sto_t * p, int iObj )
494{
495 Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
496 assert( Vec_IntSize(vThis) == 0 );
497 Vec_IntPush( vThis, 1 );
498 Vec_IntPush( vThis, 0 );
499 Vec_IntPush( vThis, 0 );
500}
501static inline int Sbd_StoPrepareSet( Sbd_Sto_t * p, int iObj, int Index )
502{
503 Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
504 int i, v, * pCut, * pList = Vec_IntArray( vThis );
505 Sbd_ForEachCut( pList, pCut, i )
506 {
507 Sbd_Cut_t * pCutTemp = &p->pCuts[Index][i];
508 pCutTemp->nLeaves = pCut[0];
509 for ( v = 1; v <= pCut[0]; v++ )
510 pCutTemp->pLeaves[v-1] = pCut[v];
511 pCutTemp->iFunc = pCut[pCut[0]+1];
512 pCutTemp->Sign = Sbd_CutGetSign( pCutTemp );
513 pCutTemp->Cost = Sbd_CutCost( p, pCutTemp );
514 pCutTemp->CostLev = Sbd_CutCostLev( p, pCutTemp );
515 pCutTemp->nTreeLeaves = Sbd_CutTreeLeaves( p, pCutTemp );
516 pCutTemp->nSlowLeaves = Sbd_CutSlowLeaves( p, iObj, pCutTemp );
517 pCutTemp->nTopLeaves = Sbd_CutTopLeaves( p, iObj, pCutTemp );
518 }
519 return pList[0];
520}
521static inline void Sbd_StoInitResult( Sbd_Sto_t * p )
522{
523 int i;
524 for ( i = 0; i < SBD_MAX_CUTNUM; i++ )
525 p->ppCuts[i] = &p->pCuts[2][i];
526}
527static inline void Sbd_StoStoreResult( Sbd_Sto_t * p, int iObj, Sbd_Cut_t ** pCuts, int nCuts )
528{
529 int i, v;
530 Vec_Int_t * vList = Vec_WecEntry( p->vCuts, iObj );
531 Vec_IntPush( vList, nCuts );
532 for ( i = 0; i < nCuts; i++ )
533 {
534 Vec_IntPush( vList, pCuts[i]->nLeaves );
535 for ( v = 0; v < (int)pCuts[i]->nLeaves; v++ )
536 Vec_IntPush( vList, pCuts[i]->pLeaves[v] );
537 Vec_IntPush( vList, pCuts[i]->iFunc );
538 }
539}
540static inline void Sbd_StoComputeDelay( Sbd_Sto_t * p, int iObj, Sbd_Cut_t ** pCuts, int nCuts )
541{
542 int i, v, Delay, DelayMin = ABC_INFINITY;
543 assert( nCuts > 0 );
544 p->iCutBest = -1;
545 for ( i = 0; i < nCuts; i++ )
546 {
547 if ( (int)pCuts[i]->nLeaves > p->nLutSize )
548 continue;
549 Delay = 0;
550 for ( v = 0; v < (int)pCuts[i]->nLeaves; v++ )
551 Delay = Abc_MaxInt( Delay, Vec_IntEntry(p->vDelays, pCuts[i]->pLeaves[v]) );
552 //DelayMin = Abc_MinInt( DelayMin, Delay );
553 if ( DelayMin > Delay )
554 {
555 DelayMin = Delay;
556 p->iCutBest = i;
557 }
558 else if ( DelayMin == Delay && p->iCutBest >= 0 && pCuts[p->iCutBest]->nLeaves > pCuts[i]->nLeaves )
559 p->iCutBest = i;
560 }
561 assert( p->iCutBest >= 0 );
562 assert( DelayMin < ABC_INFINITY );
563 DelayMin = (nCuts > 1 || pCuts[0]->nLeaves > 1) ? DelayMin + 1 : DelayMin;
564 Vec_IntWriteEntry( p->vDelays, iObj, DelayMin );
565 p->DelayMin = Abc_MaxInt( p->DelayMin, DelayMin );
566}
567static inline void Sbd_StoComputeSpec( Sbd_Sto_t * p, int iObj, Sbd_Cut_t ** pCuts, int nCuts )
568{
569 int i;
570 for ( i = 0; i < nCuts; i++ )
571 {
572 pCuts[i]->nTopLeaves = Sbd_CutTopLeaves( p, iObj, pCuts[i] );
573 pCuts[i]->nSlowLeaves = Sbd_CutSlowLeaves( p, iObj, pCuts[i] );
574 p->nCutsSpec += (pCuts[i]->nSlowLeaves == 0);
575 }
576}
577static inline void Sbd_CutPrint( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
578{
579 int i, nDigits = Abc_Base10Log(Gia_ManObjNum(p->pGia));
580 int Delay = Vec_IntEntry(p->vDelays, iObj);
581 if ( pCut == NULL ) { printf( "No cut.\n" ); return; }
582 printf( "%d {", pCut->nLeaves );
583 for ( i = 0; i < (int)pCut->nLeaves; i++ )
584 printf( " %*d", nDigits, pCut->pLeaves[i] );
585 for ( ; i < (int)p->nCutSize; i++ )
586 printf( " %*s", nDigits, " " );
587 printf( " } Cost = %3d CostL = %3d Tree = %d Slow = %d Top = %d ",
588 pCut->Cost, pCut->CostLev, pCut->nTreeLeaves, pCut->nSlowLeaves, pCut->nTopLeaves );
589 printf( "%c ", pCut->nSlowLeaves == 0 ? '*' : ' ' );
590 for ( i = 0; i < (int)pCut->nLeaves; i++ )
591 printf( "%3d ", Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay );
592 printf( "\n" );
593}
594void Sbd_StoMergeCuts( Sbd_Sto_t * p, int iObj )
595{
596 Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
597 int fIsXor = Gia_ObjIsXor(pObj);
598 int nCutSize = p->nCutSize;
599 int nCutNum = p->nCutNum;
600 int Lit0m = p->vMirrors ? Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) ) : -1;
601 int Lit1m = p->vMirrors ? Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) ) : -1;
602 int fComp0 = Gia_ObjFaninC0(pObj) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
603 int fComp1 = Gia_ObjFaninC1(pObj) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
604 int Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
605 int Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
606 int nCuts0 = Sbd_StoPrepareSet( p, Fan0, 0 );
607 int nCuts1 = Sbd_StoPrepareSet( p, Fan1, 1 );
608 int i, k, nCutsR = 0;
609 Sbd_Cut_t * pCut0, * pCut1, ** pCutsR = p->ppCuts;
610 assert( !Gia_ObjIsBuf(pObj) );
611 assert( !Gia_ObjIsMux(p->pGia, pObj) );
612 Sbd_StoInitResult( p );
613 p->CutCount[0] += nCuts0 * nCuts1;
614 for ( i = 0, pCut0 = p->pCuts[0]; i < nCuts0; i++, pCut0++ )
615 for ( k = 0, pCut1 = p->pCuts[1]; k < nCuts1; k++, pCut1++ )
616 {
617 if ( (int)(pCut0->nLeaves + pCut1->nLeaves) > nCutSize && Sbd_CutCountBits(pCut0->Sign | pCut1->Sign) > nCutSize )
618 continue;
619 p->CutCount[1]++;
620 if ( !Sbd_CutMergeOrder(pCut0, pCut1, pCutsR[nCutsR], nCutSize) )
621 continue;
622 if ( Sbd_CutSetLastCutIsContained(pCutsR, nCutsR) )
623 continue;
624 p->CutCount[2]++;
625 if ( p->fCutMin && Sbd_CutComputeTruth(p, pCut0, pCut1, fComp0, fComp1, pCutsR[nCutsR], fIsXor) )
626 pCutsR[nCutsR]->Sign = Sbd_CutGetSign(pCutsR[nCutsR]);
627 pCutsR[nCutsR]->Cost = Sbd_CutCost( p, pCutsR[nCutsR] );
628 pCutsR[nCutsR]->CostLev = Sbd_CutCostLev( p, pCutsR[nCutsR] );
629 pCutsR[nCutsR]->nTreeLeaves = Sbd_CutTreeLeaves( p, pCutsR[nCutsR] );
630 nCutsR = Sbd_CutSetAddCut( pCutsR, nCutsR, nCutNum );
631 }
632 Sbd_StoComputeDelay( p, iObj, pCutsR, nCutsR );
633 Sbd_StoComputeSpec( p, iObj, pCutsR, nCutsR );
634 p->CutCount[3] += nCutsR;
635 p->nCutsOver += nCutsR == nCutNum-1;
636 p->nCutsR = nCutsR;
637 p->Pivot = iObj;
638 // debug printout
639 if ( 0 )
640 {
641 printf( "*** Obj = %4d Delay = %4d NumCuts = %4d\n", iObj, Vec_IntEntry(p->vDelays, iObj), nCutsR );
642 for ( i = 0; i < nCutsR; i++ )
643 if ( (int)pCutsR[i]->nLeaves <= p->nLutSize || pCutsR[i]->nSlowLeaves < 2 )
644 Sbd_CutPrint( p, iObj, pCutsR[i] );
645 printf( "\n" );
646 }
647 // verify
648 assert( nCutsR > 0 && nCutsR < nCutNum );
649 assert( Sbd_CutSetCheckArray(pCutsR, nCutsR) );
650 // store the cutset
651 Sbd_StoStoreResult( p, iObj, pCutsR, nCutsR );
652 if ( nCutsR > 1 || pCutsR[0]->nLeaves > 1 )
653 Sbd_CutAddUnit( p, iObj );
654}
655
667Sbd_Sto_t * Sbd_StoAlloc( Gia_Man_t * pGia, Vec_Int_t * vMirrors, int nLutSize, int nCutSize, int nCutNum, int fCutMin, int fVerbose )
668{
669 Sbd_Sto_t * p;
670 assert( nLutSize <= nCutSize );
671 assert( nCutSize < SBD_CUT_NO_LEAF );
672 assert( nCutSize > 1 && nCutSize <= SBD_MAX_CUTSIZE );
673 assert( nCutNum > 1 && nCutNum < SBD_MAX_CUTNUM );
674 p = ABC_CALLOC( Sbd_Sto_t, 1 );
675 p->clkStart = Abc_Clock();
676 p->nLutSize = nLutSize;
677 p->nCutSize = nCutSize;
678 p->nCutNum = nCutNum;
679 p->fCutMin = fCutMin;
680 p->fVerbose = fVerbose;
681 p->pGia = pGia;
682 p->vMirrors = vMirrors;
683 p->vDelays = Vec_IntStart( Gia_ManObjNum(pGia) );
684 p->vLevels = Vec_IntStart( Gia_ManObjNum(pGia) );
685 p->vRefs = Vec_IntAlloc( Gia_ManObjNum(pGia) );
686 p->vCuts = Vec_WecStart( Gia_ManObjNum(pGia) );
687 p->vTtMem = fCutMin ? Vec_MemAllocForTT( nCutSize, 0 ) : NULL;
688 return p;
689}
691{
692 Vec_IntFree( p->vDelays );
693 Vec_IntFree( p->vLevels );
694 Vec_IntFree( p->vRefs );
695 Vec_WecFree( p->vCuts );
696 if ( p->fCutMin )
697 Vec_MemHashFree( p->vTtMem );
698 if ( p->fCutMin )
699 Vec_MemFree( p->vTtMem );
700 ABC_FREE( p );
701}
702void Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, int Level )
703{
704 if ( iObj < Vec_IntSize(p->vDelays) )
705 {
706 Vec_IntWriteEntry( p->vDelays, iObj, Delay );
707 Vec_IntWriteEntry( p->vLevels, iObj, Level );
708 }
709 else
710 {
711 assert( iObj == Vec_IntSize(p->vDelays) );
712 assert( iObj == Vec_IntSize(p->vLevels) );
713 assert( iObj == Vec_WecSize(p->vCuts) );
714 Vec_IntPush( p->vDelays, Delay );
715 Vec_IntPush( p->vLevels, Level );
716 Vec_WecPushLevel( p->vCuts );
717 }
718}
720{
721 Sbd_StoComputeCutsObj( p, iObj, 0, 0 );
722 Sbd_CutAddZero( p, iObj );
723}
724void Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level )
725{
726 Sbd_StoComputeCutsObj( p, iObj, Delay, Level );
727 Sbd_CutAddUnit( p, iObj );
728}
730{
731 Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
732 int Lev0 = Vec_IntEntry( p->vLevels, Gia_ObjFaninId0(pObj, iObj) );
733 int Lev1 = Vec_IntEntry( p->vLevels, Gia_ObjFaninId1(pObj, iObj) );
734 Sbd_StoComputeCutsObj( p, iObj, -1, 1 + Abc_MaxInt(Lev0, Lev1) );
735 Sbd_StoMergeCuts( p, iObj );
736 return Vec_IntEntry( p->vDelays, iObj );
737}
738void Sbd_StoSaveBestDelayCut( Sbd_Sto_t * p, int iObj, int * pCut )
739{
740 Sbd_Cut_t * pCutBest = p->ppCuts[p->iCutBest]; int i;
741 assert( iObj == p->Pivot );
742 pCut[0] = pCutBest->nLeaves;
743 for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
744 pCut[i+1] = pCutBest->pLeaves[i];
745}
746int Sbd_StoObjRefs( Sbd_Sto_t * p, int iObj )
747{
748 return Vec_IntEntry(p->vRefs, iObj);
749}
750void Sbd_StoRefObj( Sbd_Sto_t * p, int iObj, int iMirror )
751{
752 Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
753 assert( iObj == Vec_IntSize(p->vRefs) );
754 assert( iMirror < iObj );
755 Vec_IntPush( p->vRefs, 0 );
756//printf( "Ref %d\n", iObj );
757 if ( iMirror > 0 )
758 {
759 Vec_IntWriteEntry( p->vRefs, iObj, Vec_IntEntry(p->vRefs, iMirror) );
760 Vec_IntWriteEntry( p->vRefs, iMirror, 1 );
761 }
762 if ( Gia_ObjIsAnd(pObj) )
763 {
764 int Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
765 int Lit1m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) );
766 int Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
767 int Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
768 Vec_IntAddToEntry( p->vRefs, Fan0, 1 );
769 Vec_IntAddToEntry( p->vRefs, Fan1, 1 );
770 }
771 else if ( Gia_ObjIsCo(pObj) )
772 {
773 int Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
774 assert( Lit0m == -1 );
775 Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 );
776 }
777}
778void Sbd_StoDerefObj( Sbd_Sto_t * p, int iObj )
779{
780 Gia_Obj_t * pObj;
781 int Lit0m, Lit1m, Fan0, Fan1;
782 return;
783
784 pObj = Gia_ManObj(p->pGia, iObj);
785 if ( Vec_IntEntry(p->vRefs, iObj) == 0 )
786 printf( "Ref count mismatch at node %d\n", iObj );
787 assert( Vec_IntEntry(p->vRefs, iObj) > 0 );
788 Vec_IntAddToEntry( p->vRefs, iObj, -1 );
789 if ( Vec_IntEntry( p->vRefs, iObj ) > 0 )
790 return;
791 if ( Gia_ObjIsCi(pObj) )
792 return;
793//printf( "Deref %d\n", iObj );
794 assert( Gia_ObjIsAnd(pObj) );
795 Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
796 Lit1m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) );
797 Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
798 Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
799 if ( Fan0 ) Sbd_StoDerefObj( p, Fan0 );
800 if ( Fan1 ) Sbd_StoDerefObj( p, Fan1 );
801}
802int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves )
803{
804 int fVerbose = 0;
805 Sbd_Cut_t * pCutBest = NULL; int i;
806 assert( p->Pivot == iObj );
807 if ( fVerbose && iObj % 1000 == 0 )
808 printf( "Node %6d : \n", iObj );
809 for ( i = 0; i < p->nCutsR; i++ )
810 {
811 if ( fVerbose && iObj % 1000 == 0 )
812 Sbd_CutPrint( p, iObj, p->ppCuts[i] );
813 if ( nSize && (int)p->ppCuts[i]->nLeaves != nSize )
814 continue;
815 if ( (int)p->ppCuts[i]->nLeaves > p->nLutSize &&
816 (int)p->ppCuts[i]->nSlowLeaves <= 1 &&
817 (int)p->ppCuts[i]->nTopLeaves <= p->nLutSize-1 &&
818 (pCutBest == NULL || Sbd_CutCompare2(pCutBest, p->ppCuts[i]) == 1) )
819 pCutBest = p->ppCuts[i];
820 }
821 if ( fVerbose && iObj % 1000 == 0 )
822 {
823 printf( "Best cut of size %d:\n", nSize );
824 Sbd_CutPrint( p, iObj, pCutBest );
825 }
826 if ( pCutBest == NULL )
827 return -1;
828 assert( pCutBest->nLeaves <= SBD_DIV_MAX );
829 for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
830 pLeaves[i] = pCutBest->pLeaves[i];
831 return pCutBest->nLeaves;
832}
834{
835 Sbd_Sto_t * p = Sbd_StoAlloc( pGia, NULL, 4, 8, 100, 1, 1 );
836 Gia_Obj_t * pObj;
837 int i, iObj;
838 // prepare references
839 Gia_ManForEachObj( p->pGia, pObj, iObj )
840 Sbd_StoRefObj( p, iObj, -1 );
841 // compute cuts
843 Gia_ManForEachCiId( p->pGia, iObj, i )
844 Sbd_StoComputeCutsCi( p, iObj, 0, 0 );
845 Gia_ManForEachAnd( p->pGia, pObj, iObj )
846 Sbd_StoComputeCutsNode( p, iObj );
847 if ( p->fVerbose )
848 {
849 printf( "Running cut computation with LutSize = %d CutSize = %d CutNum = %d:\n", p->nLutSize, p->nCutSize, p->nCutNum );
850 printf( "CutPair = %.0f ", p->CutCount[0] );
851 printf( "Merge = %.0f (%.2f %%) ", p->CutCount[1], 100.0*p->CutCount[1]/p->CutCount[0] );
852 printf( "Eval = %.0f (%.2f %%) ", p->CutCount[2], 100.0*p->CutCount[2]/p->CutCount[0] );
853 printf( "Cut = %.0f (%.2f %%) ", p->CutCount[3], 100.0*p->CutCount[3]/p->CutCount[0] );
854 printf( "Cut/Node = %.2f ", p->CutCount[3] / Gia_ManAndNum(p->pGia) );
855 printf( "\n" );
856 printf( "Spec = %4d ", p->nCutsSpec );
857 printf( "Over = %4d ", p->nCutsOver );
858 printf( "Lev = %4d ", p->DelayMin );
859 Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart );
860 }
861 Sbd_StoFree( p );
862}
863
864
865
869
870
872
int nWords
Definition abcNpn.c:127
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
#define Gia_ManForEachCiId(p, Id, i)
Definition gia.h:1230
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
#define SBD_MAX_CUTSIZE
DECLARATIONS ///.
Definition sbdCut2.c:30
Sbd_Sto_t * Sbd_StoAlloc(Gia_Man_t *pGia, Vec_Int_t *vMirrors, int nLutSize, int nCutSize, int nCutNum, int fCutMin, int fVerbose)
MACRO DEFINITIONS ///.
Definition sbdCut.c:667
int Sbd_StoObjRefs(Sbd_Sto_t *p, int iObj)
Definition sbdCut.c:746
void Sbd_StoComputeCutsTest(Gia_Man_t *pGia)
Definition sbdCut.c:833
void Sbd_StoFree(Sbd_Sto_t *p)
Definition sbdCut.c:690
#define SBD_MAX_CUTSIZE
DECLARATIONS ///.
Definition sbdCut.c:30
#define Sbd_ForEachCut(pList, pCut, i)
Definition sbdCut.c:78
#define SBD_MAX_TT_WORDS
Definition sbdCut.c:32
int Sbd_StoComputeCutsNode(Sbd_Sto_t *p, int iObj)
Definition sbdCut.c:729
#define SBD_CUT_NO_LEAF
Definition sbdCut.c:34
void Sbd_StoMergeCuts(Sbd_Sto_t *p, int iObj)
Definition sbdCut.c:594
void Sbd_StoSaveBestDelayCut(Sbd_Sto_t *p, int iObj, int *pCut)
Definition sbdCut.c:738
void Sbd_StoComputeCutsConst0(Sbd_Sto_t *p, int iObj)
Definition sbdCut.c:719
void Sbd_StoComputeCutsObj(Sbd_Sto_t *p, int iObj, int Delay, int Level)
Definition sbdCut.c:702
struct Sbd_Cut_t_ Sbd_Cut_t
Definition sbdCut.c:36
void Sbd_StoRefObj(Sbd_Sto_t *p, int iObj, int iMirror)
Definition sbdCut.c:750
void Sbd_StoDerefObj(Sbd_Sto_t *p, int iObj)
Definition sbdCut.c:778
int Sbd_StoObjBestCut(Sbd_Sto_t *p, int iObj, int nSize, int *pLeaves)
Definition sbdCut.c:802
#define SBD_MAX_CUTNUM
Definition sbdCut.c:31
void Sbd_StoComputeCutsCi(Sbd_Sto_t *p, int iObj, int Delay, int Level)
Definition sbdCut.c:724
struct Sbd_Sto_t_ Sbd_Sto_t
BASIC TYPES ///.
Definition sbdInt.h:64
#define SBD_DIV_MAX
Definition sbdInt.h:57
int pLeaves[SBD_MAX_CUTSIZE]
Definition sbdCut.c:47
int Cost
Definition sbdCut.c:41
unsigned nTopLeaves
Definition sbdCut.c:45
unsigned nLeaves
Definition sbdCut.c:46
int CostLev
Definition sbdCut.c:42
int iFunc
Definition sbdCut.c:40
word Sign
Definition sbdCut.c:39
unsigned nSlowLeaves
Definition sbdCut.c:44
unsigned nTreeLeaves
Definition sbdCut.c:43
Vec_Int_t * vLevels
Definition sbdCut.c:60
Sbd_Cut_t pCuts[3][SBD_MAX_CUTNUM]
Definition sbdCut.c:64
Sbd_Cut_t * ppCuts[SBD_MAX_CUTNUM]
Definition sbdCut.c:65
int nLutSize
Definition sbdCut.c:52
abctime clkStart
Definition sbdCut.c:73
int nCutsOver
Definition sbdCut.c:70
Vec_Wec_t * vCuts
Definition sbdCut.c:62
int nCutNum
Definition sbdCut.c:54
Vec_Int_t * vRefs
Definition sbdCut.c:61
Vec_Int_t * vMirrors
Definition sbdCut.c:58
Vec_Mem_t * vTtMem
Definition sbdCut.c:63
int iCutBest
Definition sbdCut.c:68
double CutCount[4]
Definition sbdCut.c:72
int nCutsR
Definition sbdCut.c:66
int fVerbose
Definition sbdCut.c:56
int fCutMin
Definition sbdCut.c:55
Vec_Int_t * vDelays
Definition sbdCut.c:59
int Pivot
Definition sbdCut.c:67
Gia_Man_t * pGia
Definition sbdCut.c:57
int nCutsSpec
Definition sbdCut.c:69
int DelayMin
Definition sbdCut.c:71
int nCutSize
Definition sbdCut.c:53
typedefABC_NAMESPACE_IMPL_START struct Vec_Mem_t_ Vec_Mem_t
DECLARATIONS ///.
Definition utilMem.c:35
#define assert(ex)
Definition util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42