ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cswCut.c
Go to the documentation of this file.
1
20
21#include "cswInt.h"
22
24
25
29
33
45static inline int Csw_CutFindCost( Csw_Man_t * p, Csw_Cut_t * pCut )
46{
47 Aig_Obj_t * pLeaf;
48 int i, Cost = 0;
49 assert( pCut->nFanins > 0 );
50 Csw_CutForEachLeaf( p->pManRes, pCut, pLeaf, i )
51 {
52// Cost += pLeaf->nRefs;
53 Cost += Csw_ObjRefs( p, pLeaf );
54// printf( "%d ", pLeaf->nRefs );
55 }
56//printf( "\n" );
57 return Cost * 100 / pCut->nFanins;
58}
59
71static inline float Csw_CutFindCost2( Csw_Man_t * p, Csw_Cut_t * pCut )
72{
73 Aig_Obj_t * pLeaf;
74 float Cost = 0.0;
75 int i;
76 assert( pCut->nFanins > 0 );
77 Csw_CutForEachLeaf( p->pManRes, pCut, pLeaf, i )
78 Cost += (float)1.0/pLeaf->nRefs;
79 return 1/Cost;
80}
81
93static inline Csw_Cut_t * Csw_CutFindFree( Csw_Man_t * p, Aig_Obj_t * pObj )
94{
95 Csw_Cut_t * pCut, * pCutMax;
96 int i;
97 pCutMax = NULL;
98 Csw_ObjForEachCut( p, pObj, pCut, i )
99 {
100 if ( pCut->nFanins == 0 )
101 return pCut;
102 if ( pCutMax == NULL || pCutMax->Cost < pCut->Cost )
103 pCutMax = pCut;
104 }
105 assert( pCutMax != NULL );
106 pCutMax->nFanins = 0;
107 return pCutMax;
108}
109
121static inline unsigned Cut_TruthPhase( Csw_Cut_t * pCut, Csw_Cut_t * pCut1 )
122{
123 unsigned uPhase = 0;
124 int i, k;
125 for ( i = k = 0; i < pCut->nFanins; i++ )
126 {
127 if ( k == pCut1->nFanins )
128 break;
129 if ( pCut->pFanins[i] < pCut1->pFanins[k] )
130 continue;
131 assert( pCut->pFanins[i] == pCut1->pFanins[k] );
132 uPhase |= (1 << i);
133 k++;
134 }
135 return uPhase;
136}
137
149unsigned * Csw_CutComputeTruth( Csw_Man_t * p, Csw_Cut_t * pCut, Csw_Cut_t * pCut0, Csw_Cut_t * pCut1, int fCompl0, int fCompl1 )
150{
151 // permute the first table
152 if ( fCompl0 )
153 Kit_TruthNot( p->puTemp[0], Csw_CutTruth(pCut0), p->nLeafMax );
154 else
155 Kit_TruthCopy( p->puTemp[0], Csw_CutTruth(pCut0), p->nLeafMax );
156 Kit_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nFanins, p->nLeafMax, Cut_TruthPhase(pCut, pCut0), 0 );
157 // permute the second table
158 if ( fCompl1 )
159 Kit_TruthNot( p->puTemp[1], Csw_CutTruth(pCut1), p->nLeafMax );
160 else
161 Kit_TruthCopy( p->puTemp[1], Csw_CutTruth(pCut1), p->nLeafMax );
162 Kit_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nFanins, p->nLeafMax, Cut_TruthPhase(pCut, pCut1), 0 );
163 // produce the resulting table
164 Kit_TruthAnd( Csw_CutTruth(pCut), p->puTemp[2], p->puTemp[3], p->nLeafMax );
165// assert( pCut->nFanins >= Kit_TruthSupportSize( Csw_CutTruth(pCut), p->nLeafMax ) );
166 return Csw_CutTruth(pCut);
167}
168
181{
182 unsigned * pTruth;
183 int uSupp, nFansNew, i, k;
184 // get truth table
185 pTruth = Csw_CutTruth( pCut );
186 // get support
187 uSupp = Kit_TruthSupport( pTruth, p->nLeafMax );
188 // get the new support size
189 nFansNew = Kit_WordCountOnes( uSupp );
190 // check if there are redundant variables
191 if ( nFansNew == pCut->nFanins )
192 return nFansNew;
193 assert( nFansNew < pCut->nFanins );
194 // minimize support
195 Kit_TruthShrink( p->puTemp[0], pTruth, nFansNew, p->nLeafMax, uSupp, 1 );
196 for ( i = k = 0; i < pCut->nFanins; i++ )
197 if ( uSupp & (1 << i) )
198 pCut->pFanins[k++] = pCut->pFanins[i];
199 assert( k == nFansNew );
200 pCut->nFanins = nFansNew;
201// assert( nFansNew == Kit_TruthSupportSize( pTruth, p->nLeafMax ) );
202//Extra_PrintBinary( stdout, pTruth, (1<<p->nLeafMax) ); printf( "\n" );
203 return nFansNew;
204}
205
217static inline int Csw_CutCheckDominance( Csw_Cut_t * pDom, Csw_Cut_t * pCut )
218{
219 int i, k;
220 for ( i = 0; i < (int)pDom->nFanins; i++ )
221 {
222 for ( k = 0; k < (int)pCut->nFanins; k++ )
223 if ( pDom->pFanins[i] == pCut->pFanins[k] )
224 break;
225 if ( k == (int)pCut->nFanins ) // node i in pDom is not contained in pCut
226 return 0;
227 }
228 // every node in pDom is contained in pCut
229 return 1;
230}
231
244{
245 Csw_Cut_t * pTemp;
246 int i;
247 // go through the cuts of the node
248 Csw_ObjForEachCut( p, pObj, pTemp, i )
249 {
250 if ( pTemp->nFanins < 2 )
251 continue;
252 if ( pTemp == pCut )
253 continue;
254 if ( pTemp->nFanins > pCut->nFanins )
255 {
256 // skip the non-contained cuts
257 if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
258 continue;
259 // check containment seriously
260 if ( Csw_CutCheckDominance( pCut, pTemp ) )
261 {
262 // remove contained cut
263 pTemp->nFanins = 0;
264 }
265 }
266 else
267 {
268 // skip the non-contained cuts
269 if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
270 continue;
271 // check containment seriously
272 if ( Csw_CutCheckDominance( pTemp, pCut ) )
273 {
274 // remove the given
275 pCut->nFanins = 0;
276 return 1;
277 }
278 }
279 }
280 return 0;
281}
282
294static inline int Csw_CutMergeOrdered( Csw_Man_t * p, Csw_Cut_t * pC0, Csw_Cut_t * pC1, Csw_Cut_t * pC )
295{
296 int i, k, c;
297 assert( pC0->nFanins >= pC1->nFanins );
298 // the case of the largest cut sizes
299 if ( pC0->nFanins == p->nLeafMax && pC1->nFanins == p->nLeafMax )
300 {
301 for ( i = 0; i < pC0->nFanins; i++ )
302 if ( pC0->pFanins[i] != pC1->pFanins[i] )
303 return 0;
304 for ( i = 0; i < pC0->nFanins; i++ )
305 pC->pFanins[i] = pC0->pFanins[i];
306 pC->nFanins = pC0->nFanins;
307 return 1;
308 }
309 // the case when one of the cuts is the largest
310 if ( pC0->nFanins == p->nLeafMax )
311 {
312 for ( i = 0; i < pC1->nFanins; i++ )
313 {
314 for ( k = pC0->nFanins - 1; k >= 0; k-- )
315 if ( pC0->pFanins[k] == pC1->pFanins[i] )
316 break;
317 if ( k == -1 ) // did not find
318 return 0;
319 }
320 for ( i = 0; i < pC0->nFanins; i++ )
321 pC->pFanins[i] = pC0->pFanins[i];
322 pC->nFanins = pC0->nFanins;
323 return 1;
324 }
325
326 // compare two cuts with different numbers
327 i = k = 0;
328 for ( c = 0; c < p->nLeafMax; c++ )
329 {
330 if ( k == pC1->nFanins )
331 {
332 if ( i == pC0->nFanins )
333 {
334 pC->nFanins = c;
335 return 1;
336 }
337 pC->pFanins[c] = pC0->pFanins[i++];
338 continue;
339 }
340 if ( i == pC0->nFanins )
341 {
342 if ( k == pC1->nFanins )
343 {
344 pC->nFanins = c;
345 return 1;
346 }
347 pC->pFanins[c] = pC1->pFanins[k++];
348 continue;
349 }
350 if ( pC0->pFanins[i] < pC1->pFanins[k] )
351 {
352 pC->pFanins[c] = pC0->pFanins[i++];
353 continue;
354 }
355 if ( pC0->pFanins[i] > pC1->pFanins[k] )
356 {
357 pC->pFanins[c] = pC1->pFanins[k++];
358 continue;
359 }
360 pC->pFanins[c] = pC0->pFanins[i++];
361 k++;
362 }
363 if ( i < pC0->nFanins || k < pC1->nFanins )
364 return 0;
365 pC->nFanins = c;
366 return 1;
367}
368
380int Csw_CutMerge( Csw_Man_t * p, Csw_Cut_t * pCut0, Csw_Cut_t * pCut1, Csw_Cut_t * pCut )
381{
382 assert( p->nLeafMax > 0 );
383 // merge the nodes
384 if ( pCut0->nFanins < pCut1->nFanins )
385 {
386 if ( !Csw_CutMergeOrdered( p, pCut1, pCut0, pCut ) )
387 return 0;
388 }
389 else
390 {
391 if ( !Csw_CutMergeOrdered( p, pCut0, pCut1, pCut ) )
392 return 0;
393 }
394 pCut->uSign = pCut0->uSign | pCut1->uSign;
395 return 1;
396}
397
410{
411 Aig_Obj_t * pRes, * pIn0, * pIn1;
412 int nVars, uTruth, fCompl = 0;
413 assert( pCut->nFanins > 2 );
414 // minimize support of this cut
415 nVars = Csw_CutSupportMinimize( p, pCut );
416 assert( nVars == 2 );
417 // get the fanins
418 pIn0 = Aig_ManObj( p->pManRes, pCut->pFanins[0] );
419 pIn1 = Aig_ManObj( p->pManRes, pCut->pFanins[1] );
420 // derive the truth table
421 uTruth = 0xF & *Csw_CutTruth(pCut);
422 if ( uTruth == 14 || uTruth == 13 || uTruth == 11 || uTruth == 7 )
423 {
424 uTruth = 0xF & ~uTruth;
425 fCompl = 1;
426 }
427 // compute the result
428 pRes = NULL;
429 if ( uTruth == 1 ) // 0001 // 1110 14
430 pRes = Aig_And( p->pManRes, Aig_Not(pIn0), Aig_Not(pIn1) );
431 if ( uTruth == 2 ) // 0010 // 1101 13
432 pRes = Aig_And( p->pManRes, pIn0 , Aig_Not(pIn1) );
433 if ( uTruth == 4 ) // 0100 // 1011 11
434 pRes = Aig_And( p->pManRes, Aig_Not(pIn0), pIn1 );
435 if ( uTruth == 8 ) // 1000 // 0111 7
436 pRes = Aig_And( p->pManRes, pIn0 , pIn1 );
437 if ( pRes )
438 pRes = Aig_NotCond( pRes, fCompl );
439 return pRes;
440}
441
454{
455 Csw_Cut_t * pCutSet, * pCut;
456 int i;
457 // create the cutset of the node
458 pCutSet = (Csw_Cut_t *)Aig_MmFixedEntryFetch( p->pMemCuts );
459 Csw_ObjSetCuts( p, pObj, pCutSet );
460 Csw_ObjForEachCut( p, pObj, pCut, i )
461 {
462 pCut->nFanins = 0;
463 pCut->iNode = pObj->Id;
464 pCut->nCutSize = p->nCutSize;
465 pCut->nLeafMax = p->nLeafMax;
466 }
467 // add unit cut if needed
468 if ( fTriv )
469 {
470 pCut = pCutSet;
471 pCut->Cost = 0;
472 pCut->iNode = pObj->Id;
473 pCut->nFanins = 1;
474 pCut->pFanins[0] = pObj->Id;
475 pCut->uSign = Aig_ObjCutSign( pObj->Id );
476 memset( Csw_CutTruth(pCut), 0xAA, sizeof(unsigned) * p->nTruthWords );
477 }
478 return pCutSet;
479}
480
492Aig_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv )
493{
494 int fUseResub = 1;
495 Csw_Cut_t * pCut0, * pCut1, * pCut, * pCutSet;
496 Aig_Obj_t * pFanin0 = Aig_ObjFanin0(pObj);
497 Aig_Obj_t * pFanin1 = Aig_ObjFanin1(pObj);
498 Aig_Obj_t * pObjNew;
499 unsigned * pTruth;
500 int i, k, nVars, nFanins, iVar;
501 abctime clk;
502
503 assert( !Aig_IsComplement(pObj) );
504 if ( !Aig_ObjIsNode(pObj) )
505 return pObj;
506 if ( Csw_ObjCuts(p, pObj) )
507 return pObj;
508 // the node is not processed yet
509 assert( Csw_ObjCuts(p, pObj) == NULL );
510 assert( Aig_ObjIsNode(pObj) );
511
512 // set up the first cut
513 pCutSet = Csw_ObjPrepareCuts( p, pObj, fTriv );
514
515 // compute pair-wise cut combinations while checking table
516 Csw_ObjForEachCut( p, pFanin0, pCut0, i )
517 if ( pCut0->nFanins > 0 )
518 Csw_ObjForEachCut( p, pFanin1, pCut1, k )
519 if ( pCut1->nFanins > 0 )
520 {
521 // make sure K-feasible cut exists
522 if ( Kit_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->nLeafMax )
523 continue;
524 // get the next cut of this node
525 pCut = Csw_CutFindFree( p, pObj );
526clk = Abc_Clock();
527 // assemble the new cut
528 if ( !Csw_CutMerge( p, pCut0, pCut1, pCut ) )
529 {
530 assert( pCut->nFanins == 0 );
531 continue;
532 }
533 // check containment
534 if ( Csw_CutFilter( p, pObj, pCut ) )
535 {
536 assert( pCut->nFanins == 0 );
537 continue;
538 }
539 // create its truth table
540 pTruth = Csw_CutComputeTruth( p, pCut, pCut0, pCut1, Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
541 // support minimize the truth table
542 nFanins = pCut->nFanins;
543// nVars = Csw_CutSupportMinimize( p, pCut ); // leads to quality degradation
544 nVars = Kit_TruthSupportSize( pTruth, p->nLeafMax );
545p->timeCuts += Abc_Clock() - clk;
546
547 // check for trivial truth tables
548 if ( nVars == 0 )
549 {
550 p->nNodesTriv0++;
551 return Aig_NotCond( Aig_ManConst1(p->pManRes), !(pTruth[0] & 1) );
552 }
553 if ( nVars == 1 )
554 {
555 p->nNodesTriv1++;
556 iVar = Kit_WordFindFirstBit( Kit_TruthSupport(pTruth, p->nLeafMax) );
557 assert( iVar < pCut->nFanins );
558 return Aig_NotCond( Aig_ManObj(p->pManRes, pCut->pFanins[iVar]), (pTruth[0] & 1) );
559 }
560 if ( nVars == 2 && nFanins > 2 && fUseResub )
561 {
562 if ( (pObjNew = Csw_ObjTwoVarCut( p, pCut )) )
563 {
564 p->nNodesTriv2++;
565 return pObjNew;
566 }
567 }
568
569 // check if an equivalent node with the same cut exists
570clk = Abc_Clock();
571 pObjNew = pCut->nFanins > 2 ? Csw_TableCutLookup( p, pCut ) : NULL;
572p->timeHash += Abc_Clock() - clk;
573 if ( pObjNew )
574 {
575 p->nNodesCuts++;
576 return pObjNew;
577 }
578
579 // assign the cost
580 pCut->Cost = Csw_CutFindCost( p, pCut );
581 assert( pCut->nFanins > 0 );
582 assert( pCut->Cost > 0 );
583 }
584 p->nNodesTried++;
585
586 // load the resulting cuts into the table
587clk = Abc_Clock();
588 Csw_ObjForEachCut( p, pObj, pCut, i )
589 {
590 if ( pCut->nFanins > 2 )
591 {
592 assert( pCut->Cost > 0 );
593 Csw_TableCutInsert( p, pCut );
594 }
595 }
596p->timeHash += Abc_Clock() - clk;
597
598 // return the node if could not replace it
599 return pObj;
600}
601
605
606
608
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
char * Aig_MmFixedEntryFetch(Aig_MmFixed_t *p)
Definition aigMem.c:161
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:104
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Csw_Cut_t * Csw_ObjPrepareCuts(Csw_Man_t *p, Aig_Obj_t *pObj, int fTriv)
FUNCTION DECLARATIONS ///.
Definition cswCut.c:453
int Csw_CutSupportMinimize(Csw_Man_t *p, Csw_Cut_t *pCut)
Definition cswCut.c:180
int Csw_CutFilter(Csw_Man_t *p, Aig_Obj_t *pObj, Csw_Cut_t *pCut)
Definition cswCut.c:243
Aig_Obj_t * Csw_ObjSweep(Csw_Man_t *p, Aig_Obj_t *pObj, int fTriv)
Definition cswCut.c:492
unsigned * Csw_CutComputeTruth(Csw_Man_t *p, Csw_Cut_t *pCut, Csw_Cut_t *pCut0, Csw_Cut_t *pCut1, int fCompl0, int fCompl1)
Definition cswCut.c:149
Aig_Obj_t * Csw_ObjTwoVarCut(Csw_Man_t *p, Csw_Cut_t *pCut)
Definition cswCut.c:409
int Csw_CutMerge(Csw_Man_t *p, Csw_Cut_t *pCut0, Csw_Cut_t *pCut1, Csw_Cut_t *pCut)
Definition cswCut.c:380
void Csw_TableCutInsert(Csw_Man_t *p, Csw_Cut_t *pCut)
Definition cswTable.c:103
#define Csw_CutForEachLeaf(p, pCut, pLeaf, i)
Definition cswInt.h:131
struct Csw_Cut_t_ Csw_Cut_t
Definition cswInt.h:53
#define Csw_ObjForEachCut(p, pObj, pCut, i)
MACRO DEFINITIONS ///.
Definition cswInt.h:128
Aig_Obj_t * Csw_TableCutLookup(Csw_Man_t *p, Csw_Cut_t *pCut)
Definition cswTable.c:121
typedefABC_NAMESPACE_HEADER_START struct Csw_Man_t_ Csw_Man_t
INCLUDES ///.
Definition cswInt.h:52
Cube * p
Definition exorList.c:222
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition kitTruth.c:346
int Kit_TruthSupportSize(unsigned *pTruth, int nVars)
Definition kitTruth.c:327
void Kit_TruthShrink(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition kitTruth.c:200
void Kit_TruthStretch(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition kitTruth.c:166
int Id
Definition aig.h:85
unsigned int nRefs
Definition aig.h:81
unsigned uSign
Definition cswInt.h:61
int pFanins[0]
Definition cswInt.h:66
short nCutSize
Definition cswInt.h:63
char nLeafMax
Definition cswInt.h:64
char nFanins
Definition cswInt.h:65
int iNode
Definition cswInt.h:62
int Cost
Definition cswInt.h:59
#define assert(ex)
Definition util_old.h:213
char * memset()