ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
lpkAbcDsd.c File Reference
#include "lpkInt.h"
Include dependency graph for lpkAbcDsd.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Lpk_FunComputeMinSuppSizeVar (Lpk_Fun_t *p, unsigned **ppTruths, int nTruths, unsigned **ppCofs, unsigned uNonDecSupp)
 DECLARATIONS ///.
 
unsigned Lpk_ComputeBoundSets_rec (Kit_DsdNtk_t *p, int iLit, Vec_Int_t *vSets, int nSizeMax)
 
Vec_Int_tLpk_ComputeBoundSets (Kit_DsdNtk_t *p, int nSizeMax)
 
Vec_Int_tLpk_MergeBoundSets (Vec_Int_t *vSets0, Vec_Int_t *vSets1, int nSizeMax)
 
void Lpk_FunCompareBoundSets (Lpk_Fun_t *p, Vec_Int_t *vBSets, int nCofDepth, unsigned uNonDecSupp, unsigned uLateArrSupp, Lpk_Res_t *pRes)
 
unsigned Lpk_DsdLateArriving (Lpk_Fun_t *p)
 
int Lpk_DsdAnalizeOne (Lpk_Fun_t *p, unsigned *ppTruths[5][16], Kit_DsdNtk_t *pNtks[], char pCofVars[], int nCofDepth, Lpk_Res_t *pRes)
 
Lpk_Res_tLpk_DsdAnalize (Lpk_Man_t *pMan, Lpk_Fun_t *p, int nShared)
 
Lpk_Fun_tLpk_DsdSplit (Lpk_Man_t *pMan, Lpk_Fun_t *p, char *pCofVars, int nCofVars, unsigned uBoundSet)
 

Function Documentation

◆ Lpk_ComputeBoundSets()

Vec_Int_t * Lpk_ComputeBoundSets ( Kit_DsdNtk_t * p,
int nSizeMax )

Function*************************************************************

Synopsis [Computes the set of subsets of decomposable variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file lpkAbcDsd.c.

163{
164 Vec_Int_t * vSets;
165 unsigned uSupport, Entry;
166 int Number, i;
167 assert( p->nVars <= 16 );
168 vSets = Vec_IntAlloc( 100 );
169 Vec_IntPush( vSets, 0 );
170 if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
171 return vSets;
172 if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
173 {
174 uSupport = ( 1 << Abc_Lit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
175 if ( Kit_WordCountOnes(uSupport) <= nSizeMax )
176 Vec_IntPush( vSets, uSupport );
177 return vSets;
178 }
179 uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets, nSizeMax );
180 assert( (uSupport & 0xFFFF0000) == 0 );
181 // add the total support of the network
182 if ( Kit_WordCountOnes(uSupport) <= nSizeMax )
183 Vec_IntPush( vSets, uSupport );
184 // set the remaining variables
185 Vec_IntForEachEntry( vSets, Number, i )
186 {
187 Entry = Number;
188 Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
189 }
190 return vSets;
191}
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
@ KIT_DSD_CONST1
Definition kit.h:103
@ KIT_DSD_VAR
Definition kit.h:104
unsigned Lpk_ComputeBoundSets_rec(Kit_DsdNtk_t *p, int iLit, Vec_Int_t *vSets, int nSizeMax)
Definition lpkAbcDsd.c:108
#define assert(ex)
Definition util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_ComputeBoundSets_rec()

unsigned Lpk_ComputeBoundSets_rec ( Kit_DsdNtk_t * p,
int iLit,
Vec_Int_t * vSets,
int nSizeMax )

Function*************************************************************

Synopsis [Recursively computes decomposable subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 108 of file lpkAbcDsd.c.

109{
110 unsigned i, iLitFanin, uSupport, uSuppCur;
111 Kit_DsdObj_t * pObj;
112 // consider the case of simple gate
113 pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
114 if ( pObj == NULL )
115 return (1 << Abc_Lit2Var(iLit));
116 if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
117 {
118 unsigned uSupps[16], Limit, s;
119 uSupport = 0;
120 Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
121 {
122 uSupps[i] = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets, nSizeMax );
123 uSupport |= uSupps[i];
124 }
125 // create all subsets, except empty and full
126 Limit = (1 << pObj->nFans) - 1;
127 for ( s = 1; s < Limit; s++ )
128 {
129 uSuppCur = 0;
130 for ( i = 0; i < pObj->nFans; i++ )
131 if ( s & (1 << i) )
132 uSuppCur |= uSupps[i];
133 if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax )
134 Vec_IntPush( vSets, uSuppCur );
135 }
136 return uSupport;
137 }
138 assert( pObj->Type == KIT_DSD_PRIME );
139 // get the cumulative support of all fanins
140 uSupport = 0;
141 Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
142 {
143 uSuppCur = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets, nSizeMax );
144 uSupport |= uSuppCur;
145 if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax )
146 Vec_IntPush( vSets, uSuppCur );
147 }
148 return uSupport;
149}
@ KIT_DSD_XOR
Definition kit.h:106
@ KIT_DSD_PRIME
Definition kit.h:107
@ KIT_DSD_AND
Definition kit.h:105
struct Kit_DsdObj_t_ Kit_DsdObj_t
Definition kit.h:111
#define Kit_DsdObjForEachFanin(pNtk, pObj, iLit, i)
Definition kit.h:160
unsigned Type
Definition kit.h:115
unsigned nFans
Definition kit.h:119
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_DsdAnalize()

Lpk_Res_t * Lpk_DsdAnalize ( Lpk_Man_t * pMan,
Lpk_Fun_t * p,
int nShared )

Function*************************************************************

Synopsis [Performs DSD-based decomposition of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 452 of file lpkAbcDsd.c.

453{
454 static Lpk_Res_t Res0, * pRes0 = &Res0;
455 static Lpk_Res_t Res1, * pRes1 = &Res1;
456 static Lpk_Res_t Res2, * pRes2 = &Res2;
457 static Lpk_Res_t Res3, * pRes3 = &Res3;
458 int fUseBackLooking = 1;
459 Lpk_Res_t * pRes = NULL;
460 Vec_Int_t * vBSets;
461 Kit_DsdNtk_t * pNtks[8] = {NULL};
462 char pCofVars[5];
463 int i;
464
465 assert( p->nLutK >= 3 );
466 assert( nShared >= 0 && nShared <= 3 );
467 assert( p->uSupp == Kit_BitMask(p->nVars) );
468
469 // try decomposition without cofactoring
470 pNtks[0] = Kit_DsdDecomposeExpand( Lpk_FunTruth( p, 0 ), p->nVars );
471 if ( pMan->pPars->fVerbose )
472 pMan->nBlocks[ Kit_DsdNonDsdSizeMax(pNtks[0]) ]++;
473 vBSets = Lpk_ComputeBoundSets( pNtks[0], p->nLutK );
474 Lpk_FunCompareBoundSets( p, vBSets, 0, 0xFFFF, Lpk_DsdLateArriving(p), pRes0 );
475 Vec_IntFree( vBSets );
476
477 // check the result
478 if ( pRes0->nBSVars == (int)p->nLutK )
479 { pRes = pRes0; goto finish; }
480 if ( pRes0->nBSVars == (int)p->nLutK - 1 )
481 { pRes = pRes0; goto finish; }
482 if ( nShared == 0 )
483 goto finish;
484
485 // prepare storage
486 Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth( p, 0 ), p->nVars );
487
488 // cofactor 1 time
489 if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 1, pRes1 ) )
490 goto finish;
491 assert( pRes1->nBSVars <= (int)p->nLutK - 1 );
492 if ( pRes1->nBSVars == (int)p->nLutK - 1 )
493 { pRes = pRes1; goto finish; }
494 if ( pRes0->nBSVars == (int)p->nLutK - 2 )
495 { pRes = pRes0; goto finish; }
496 if ( pRes1->nBSVars == (int)p->nLutK - 2 )
497 { pRes = pRes1; goto finish; }
498 if ( nShared == 1 )
499 goto finish;
500
501 // cofactor 2 times
502 if ( p->nLutK >= 4 )
503 {
504 if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 2, pRes2 ) )
505 goto finish;
506 assert( pRes2->nBSVars <= (int)p->nLutK - 2 );
507 if ( pRes2->nBSVars == (int)p->nLutK - 2 )
508 { pRes = pRes2; goto finish; }
509 if ( fUseBackLooking )
510 {
511 if ( pRes0->nBSVars == (int)p->nLutK - 3 )
512 { pRes = pRes0; goto finish; }
513 if ( pRes1->nBSVars == (int)p->nLutK - 3 )
514 { pRes = pRes1; goto finish; }
515 }
516 if ( pRes2->nBSVars == (int)p->nLutK - 3 )
517 { pRes = pRes2; goto finish; }
518 if ( nShared == 2 )
519 goto finish;
520 assert( nShared == 3 );
521 }
522
523 // cofactor 3 times
524 if ( p->nLutK >= 5 )
525 {
526 if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 3, pRes3 ) )
527 goto finish;
528 assert( pRes3->nBSVars <= (int)p->nLutK - 3 );
529 if ( pRes3->nBSVars == (int)p->nLutK - 3 )
530 { pRes = pRes3; goto finish; }
531 if ( fUseBackLooking )
532 {
533 if ( pRes0->nBSVars == (int)p->nLutK - 4 )
534 { pRes = pRes0; goto finish; }
535 if ( pRes1->nBSVars == (int)p->nLutK - 4 )
536 { pRes = pRes1; goto finish; }
537 if ( pRes2->nBSVars == (int)p->nLutK - 4 )
538 { pRes = pRes2; goto finish; }
539 }
540 if ( pRes3->nBSVars == (int)p->nLutK - 4 )
541 { pRes = pRes3; goto finish; }
542 }
543
544finish:
545 // free the networks
546 for ( i = 0; i < (1<<nShared); i++ )
547 if ( pNtks[i] )
548 Kit_DsdNtkFree( pNtks[i] );
549 // choose the best under these conditions
550 return pRes;
551}
int Kit_DsdNonDsdSizeMax(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:1212
Kit_DsdNtk_t * Kit_DsdDecomposeExpand(unsigned *pTruth, int nVars)
Definition kitDsd.c:2331
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:164
struct Kit_DsdNtk_t_ Kit_DsdNtk_t
Definition kit.h:124
Vec_Int_t * Lpk_ComputeBoundSets(Kit_DsdNtk_t *p, int nSizeMax)
Definition lpkAbcDsd.c:162
unsigned Lpk_DsdLateArriving(Lpk_Fun_t *p)
Definition lpkAbcDsd.c:352
int Lpk_DsdAnalizeOne(Lpk_Fun_t *p, unsigned *ppTruths[5][16], Kit_DsdNtk_t *pNtks[], char pCofVars[], int nCofDepth, Lpk_Res_t *pRes)
Definition lpkAbcDsd.c:372
void Lpk_FunCompareBoundSets(Lpk_Fun_t *p, Vec_Int_t *vBSets, int nCofDepth, unsigned uNonDecSupp, unsigned uLateArrSupp, Lpk_Res_t *pRes)
Definition lpkAbcDsd.c:276
struct Lpk_Res_t_ Lpk_Res_t
Definition lpkInt.h:163
unsigned * ppTruths[5][16]
Definition lpkInt.h:104
int nBlocks[17]
Definition lpkInt.h:123
Lpk_Par_t * pPars
Definition lpkInt.h:72
int nBSVars
Definition lpkInt.h:166
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_DsdAnalizeOne()

int Lpk_DsdAnalizeOne ( Lpk_Fun_t * p,
unsigned * ppTruths[5][16],
Kit_DsdNtk_t * pNtks[],
char pCofVars[],
int nCofDepth,
Lpk_Res_t * pRes )

Function*************************************************************

Synopsis [Performs DSD-based decomposition of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 372 of file lpkAbcDsd.c.

373{
374 int fVerbose = 0;
375 Vec_Int_t * pvBSets[4][8];
376 unsigned uNonDecSupp, uLateArrSupp;
377 int i, k, nNonDecSize, nNonDecSizeMax;
378 assert( nCofDepth >= 1 && nCofDepth <= 3 );
379 assert( nCofDepth < (int)p->nLutK - 1 );
380 assert( p->fSupports );
381
382 // find the support of the largest non-DSD block
383 nNonDecSizeMax = 0;
384 uNonDecSupp = p->uSupp;
385 for ( i = 0; i < (1<<(nCofDepth-1)); i++ )
386 {
387 nNonDecSize = Kit_DsdNonDsdSizeMax( pNtks[i] );
388 if ( nNonDecSizeMax < nNonDecSize )
389 {
390 nNonDecSizeMax = nNonDecSize;
391 uNonDecSupp = Kit_DsdNonDsdSupports( pNtks[i] );
392 }
393 else if ( nNonDecSizeMax == nNonDecSize )
394 uNonDecSupp |= Kit_DsdNonDsdSupports( pNtks[i] );
395 }
396
397 // remove those variables that cannot be used because of delay constraints
398 // if variables arrival time is more than p->DelayLim - 2, it cannot be used
399 uLateArrSupp = Lpk_DsdLateArriving( p );
400 if ( (uNonDecSupp & ~uLateArrSupp) == 0 )
401 {
402 memset( pRes, 0, sizeof(Lpk_Res_t) );
403 return 0;
404 }
405
406 // find the next cofactoring variable
407 pCofVars[nCofDepth-1] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[nCofDepth-1], 1<<(nCofDepth-1), ppTruths[nCofDepth], uNonDecSupp & ~uLateArrSupp );
408
409 // derive decomposed networks
410 for ( i = 0; i < (1<<nCofDepth); i++ )
411 {
412 if ( pNtks[i] )
413 Kit_DsdNtkFree( pNtks[i] );
414 pNtks[i] = Kit_DsdDecomposeExpand( ppTruths[nCofDepth][i], p->nVars );
415if ( fVerbose )
416Kit_DsdPrint( stdout, pNtks[i] );
417 pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtks[i], p->nLutK - nCofDepth ); // try restricting to those in uNonDecSupp!!!
418 }
419
420 // derive the set of feasible boundsets
421 for ( i = nCofDepth - 1; i >= 0; i-- )
422 for ( k = 0; k < (1<<i); k++ )
423 pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1], p->nLutK - nCofDepth );
424 // compare bound-sets
425 Lpk_FunCompareBoundSets( p, pvBSets[0][0], nCofDepth, uNonDecSupp, uLateArrSupp, pRes );
426 // free the bound sets
427 for ( i = nCofDepth; i >= 0; i-- )
428 for ( k = 0; k < (1<<i); k++ )
429 Vec_IntFree( pvBSets[i][k] );
430
431 // copy the cofactoring variables
432 if ( pRes->BSVars )
433 {
434 pRes->nCofVars = nCofDepth;
435 for ( i = 0; i < nCofDepth; i++ )
436 pRes->pCofVars[i] = pCofVars[i];
437 }
438 return 1;
439}
void Kit_DsdPrint(FILE *pFile, Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:375
unsigned Kit_DsdNonDsdSupports(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:1265
ABC_NAMESPACE_IMPL_START int Lpk_FunComputeMinSuppSizeVar(Lpk_Fun_t *p, unsigned **ppTruths, int nTruths, unsigned **ppCofs, unsigned uNonDecSupp)
DECLARATIONS ///.
Definition lpkAbcDsd.c:47
Vec_Int_t * Lpk_MergeBoundSets(Vec_Int_t *vSets0, Vec_Int_t *vSets1, int nSizeMax)
Definition lpkAbcDsd.c:247
int nCofVars
Definition lpkInt.h:168
unsigned BSVars
Definition lpkInt.h:167
char pCofVars[4]
Definition lpkInt.h:169
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_DsdLateArriving()

unsigned Lpk_DsdLateArriving ( Lpk_Fun_t * p)

Function*************************************************************

Synopsis [Finds late arriving inputs, which cannot be in the bound set.]

Description []

SideEffects []

SeeAlso []

Definition at line 352 of file lpkAbcDsd.c.

353{
354 unsigned i, uLateArrSupp = 0;
355 Lpk_SuppForEachVar( p->uSupp, i )
356 if ( p->pDelays[i] > (int)p->nDelayLim - 2 )
357 uLateArrSupp |= (1 << i);
358 return uLateArrSupp;
359}
#define Lpk_SuppForEachVar(Supp, Var)
Definition lpkInt.h:196
Here is the caller graph for this function:

◆ Lpk_DsdSplit()

Lpk_Fun_t * Lpk_DsdSplit ( Lpk_Man_t * pMan,
Lpk_Fun_t * p,
char * pCofVars,
int nCofVars,
unsigned uBoundSet )

Function*************************************************************

Synopsis [Splits the function into two subfunctions using DSD.]

Description []

SideEffects []

SeeAlso []

Definition at line 564 of file lpkAbcDsd.c.

565{
566 Lpk_Fun_t * pNew;
567 Kit_DsdNtk_t * pNtkDec;
568 int i, k, iVacVar, nCofs;
569 // prepare storage
570 Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth(p, 0), p->nVars );
571 // get the vacuous variable
572 iVacVar = Kit_WordFindFirstBit( uBoundSet );
573 // compute the cofactors
574 for ( i = 0; i < nCofVars; i++ )
575 for ( k = 0; k < (1<<i); k++ )
576 {
577 Kit_TruthCofactor0New( pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i][k], p->nVars, pCofVars[i] );
578 Kit_TruthCofactor1New( pMan->ppTruths[i+1][2*k+1], pMan->ppTruths[i][k], p->nVars, pCofVars[i] );
579 }
580 // decompose each cofactor w.r.t. the bound set
581 nCofs = (1<<nCofVars);
582 for ( k = 0; k < nCofs; k++ )
583 {
584 pNtkDec = Kit_DsdDecomposeExpand( pMan->ppTruths[nCofVars][k], p->nVars );
585 Kit_DsdTruthPartialTwo( pMan->pDsdMan, pNtkDec, uBoundSet, iVacVar, pMan->ppTruths[nCofVars+1][k], pMan->ppTruths[nCofVars+1][nCofs+k] );
586 Kit_DsdNtkFree( pNtkDec );
587 }
588 // compute the composition/decomposition functions (they will be in pMan->ppTruths[1][0]/pMan->ppTruths[1][1])
589 for ( i = nCofVars; i >= 1; i-- )
590 for ( k = 0; k < (1<<i); k++ )
591 Kit_TruthMuxVar( pMan->ppTruths[i][k], pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i+1][2*k+1], p->nVars, pCofVars[i-1] );
592
593 // derive the new component (decomposition function)
594 pNew = Lpk_FunDup( p, pMan->ppTruths[1][1] );
595 // update the old component (composition function)
596 Kit_TruthCopy( Lpk_FunTruth(p, 0), pMan->ppTruths[1][0], p->nVars );
597 p->uSupp = Kit_TruthSupport( Lpk_FunTruth(p, 0), p->nVars );
598 p->pFanins[iVacVar] = pNew->Id;
599 p->pDelays[iVacVar] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
600 // support minimize both
601 p->fSupports = 0;
603 Lpk_FunSuppMinimize( pNew );
604 // update delay and area requirements
605 pNew->nDelayLim = p->pDelays[iVacVar];
606 pNew->nAreaLim = 1;
607 p->nAreaLim = p->nAreaLim - 1;
608 return pNew;
609}
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition kitTruth.c:346
void Kit_TruthMuxVar(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
Definition kitTruth.c:1069
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:573
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:521
void Kit_DsdTruthPartialTwo(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp, int iVar, unsigned *pTruthCo, unsigned *pTruthDec)
Definition kitDsd.c:1090
Lpk_Fun_t * Lpk_FunDup(Lpk_Fun_t *p, unsigned *pTruth)
Definition lpkAbcUtil.c:114
int Lpk_SuppDelay(unsigned uSupp, int *pDelays)
Definition lpkAbcUtil.c:215
int Lpk_FunSuppMinimize(Lpk_Fun_t *p)
Definition lpkAbcUtil.c:143
struct Lpk_Fun_t_ Lpk_Fun_t
Definition lpkInt.h:144
int pDelays[16]
Definition lpkInt.h:157
unsigned nAreaLim
Definition lpkInt.h:151
unsigned nDelayLim
Definition lpkInt.h:156
unsigned uSupp
Definition lpkInt.h:154
unsigned Id
Definition lpkInt.h:148
Kit_DsdMan_t * pDsdMan
Definition lpkInt.h:107
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_FunCompareBoundSets()

void Lpk_FunCompareBoundSets ( Lpk_Fun_t * p,
Vec_Int_t * vBSets,
int nCofDepth,
unsigned uNonDecSupp,
unsigned uLateArrSupp,
Lpk_Res_t * pRes )

Function*************************************************************

Synopsis [Performs DSD-based decomposition of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 276 of file lpkAbcDsd.c.

277{
278 int fVerbose = 0;
279 unsigned uBoundSet;
280 int i, nVarsBS, nVarsRem, Delay, Area;
281
282 // compare the resulting boundsets
283 memset( pRes, 0, sizeof(Lpk_Res_t) );
284 Vec_IntForEachEntry( vBSets, uBoundSet, i )
285 {
286 if ( (uBoundSet & 0xFFFF) == 0 ) // skip empty boundset
287 continue;
288 if ( (uBoundSet & uNonDecSupp) == 0 ) // skip those boundsets that are not in the domain of interest
289 continue;
290 if ( (uBoundSet & uLateArrSupp) ) // skip those boundsets that are late arriving
291 continue;
292if ( fVerbose )
293{
294Lpk_PrintSetOne( uBoundSet & 0xFFFF );
295//printf( "\n" );
296//Lpk_PrintSetOne( uBoundSet >> 16 );
297//printf( "\n" );
298}
299 assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
300 nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
301 if ( nVarsBS == 1 )
302 continue;
303 assert( nVarsBS <= (int)p->nLutK - nCofDepth );
304 nVarsRem = p->nVars - nVarsBS + 1;
305 Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK );
306 Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
307if ( fVerbose )
308printf( "area = %d limit = %d delay = %d limit = %d\n", Area, (int)p->nAreaLim, Delay, (int)p->nDelayLim );
309 if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim )
310 continue;
311 if ( pRes->BSVars == 0 || pRes->nSuppSizeL > nVarsRem || (pRes->nSuppSizeL == nVarsRem && pRes->DelayEst > Delay) )
312 {
313 pRes->nBSVars = nVarsBS;
314 pRes->BSVars = (uBoundSet & 0xFFFF);
315 pRes->nSuppSizeS = nVarsBS + nCofDepth;
316 pRes->nSuppSizeL = nVarsRem;
317 pRes->DelayEst = Delay;
318 pRes->AreaEst = Area;
319 }
320 }
321if ( fVerbose )
322{
323if ( pRes->BSVars )
324{
325printf( "Found bound set " );
326Lpk_PrintSetOne( pRes->BSVars );
327printf( "\n" );
328}
329else
330printf( "Did not find boundsets.\n" );
331printf( "\n" );
332}
333 if ( pRes->BSVars )
334 {
335 assert( pRes->DelayEst <= (int)p->nDelayLim );
336 assert( pRes->AreaEst <= (int)p->nAreaLim );
337 }
338}
int nSuppSizeS
Definition lpkInt.h:170
int DelayEst
Definition lpkInt.h:172
int AreaEst
Definition lpkInt.h:173
int nSuppSizeL
Definition lpkInt.h:171
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_FunComputeMinSuppSizeVar()

ABC_NAMESPACE_IMPL_START int Lpk_FunComputeMinSuppSizeVar ( Lpk_Fun_t * p,
unsigned ** ppTruths,
int nTruths,
unsigned ** ppCofs,
unsigned uNonDecSupp )

DECLARATIONS ///.

CFile****************************************************************

FileName [lpkAbcDsd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast Boolean matching for LUT structures.]

Synopsis [LUT-decomposition based on recursive DSD.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
lpkAbcDsd.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Cofactors TTs w.r.t. all vars and finds the best var.]

Description [The best variable is the variable with the minimum sum total of the support sizes of all truth tables. This procedure computes and returns cofactors w.r.t. the best variable.]

SideEffects []

SeeAlso []

Definition at line 47 of file lpkAbcDsd.c.

48{
49 int i, Var, VarBest, nSuppSize0, nSuppSize1;
50 int nSuppTotalMin = -1; // Suppress "might be used uninitialized"
51 int nSuppTotalCur;
52 int nSuppMaxMin = -1; // Suppress "might be used uninitialized"
53 int nSuppMaxCur;
54 assert( nTruths > 0 );
55 VarBest = -1;
56 Lpk_SuppForEachVar( p->uSupp, Var )
57 {
58 if ( (uNonDecSupp & (1 << Var)) == 0 )
59 continue;
60 nSuppMaxCur = 0;
61 nSuppTotalCur = 0;
62 for ( i = 0; i < nTruths; i++ )
63 {
64 if ( nTruths == 1 )
65 {
66 nSuppSize0 = Kit_WordCountOnes( p->puSupps[2*Var+0] );
67 nSuppSize1 = Kit_WordCountOnes( p->puSupps[2*Var+1] );
68 }
69 else
70 {
71 Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var );
72 Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var );
73 nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars );
74 nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars );
75 }
76 nSuppMaxCur = Abc_MaxInt( nSuppMaxCur, nSuppSize0 );
77 nSuppMaxCur = Abc_MaxInt( nSuppMaxCur, nSuppSize1 );
78 nSuppTotalCur += nSuppSize0 + nSuppSize1;
79 }
80 if ( VarBest == -1 || nSuppMaxMin > nSuppMaxCur ||
81 (nSuppMaxMin == nSuppMaxCur && nSuppTotalMin > nSuppTotalCur) )
82 {
83 VarBest = Var;
84 nSuppMaxMin = nSuppMaxCur;
85 nSuppTotalMin = nSuppTotalCur;
86 }
87 }
88 // recompute cofactors for the best var
89 for ( i = 0; i < nTruths; i++ )
90 {
91 Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, VarBest );
92 Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, VarBest );
93 }
94 return VarBest;
95}
int Var
Definition exorList.c:228
int Kit_TruthSupportSize(unsigned *pTruth, int nVars)
Definition kitTruth.c:327
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_MergeBoundSets()

Vec_Int_t * Lpk_MergeBoundSets ( Vec_Int_t * vSets0,
Vec_Int_t * vSets1,
int nSizeMax )

Function*************************************************************

Synopsis [Merges two bound sets.]

Description []

SideEffects []

SeeAlso []

Definition at line 247 of file lpkAbcDsd.c.

248{
249 Vec_Int_t * vSets;
250 int Entry0, Entry1, Entry;
251 int i, k;
252 vSets = Vec_IntAlloc( 100 );
253 Vec_IntForEachEntry( vSets0, Entry0, i )
254 Vec_IntForEachEntry( vSets1, Entry1, k )
255 {
256 Entry = Entry0 | Entry1;
257 if ( (Entry & (Entry >> 16)) )
258 continue;
259 if ( Kit_WordCountOnes(Entry & 0xffff) <= nSizeMax )
260 Vec_IntPush( vSets, Entry );
261 }
262 return vSets;
263}
Here is the caller graph for this function: