abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
lpkAbcDsd.c File Reference
#include "lpkInt.h"

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 ///. More...
 
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)
 
static void Lpk_PrintSetOne (int uSupport)
 
static void Lpk_PrintSets (Vec_Int_t *vSets)
 
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

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 }
static Kit_DsdObj_t * Kit_DsdNtkRoot(Kit_DsdNtk_t *pNtk)
Definition: kit.h:151
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
unsigned short Root
Definition: kit.h:127
unsigned Lpk_ComputeBoundSets_rec(Kit_DsdNtk_t *p, int iLit, Vec_Int_t *vSets, int nSizeMax)
Definition: lpkAbcDsd.c:108
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
#define assert(ex)
Definition: util_old.h:213
static int Kit_WordCountOnes(unsigned uWord)
Definition: kit.h:243
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
unsigned short nVars
Definition: kit.h:124
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 }
unsigned Type
Definition: kit.h:112
unsigned nFans
Definition: kit.h:116
static Kit_DsdObj_t * Kit_DsdNtkObj(Kit_DsdNtk_t *pNtk, int Id)
Definition: kit.h:150
unsigned Lpk_ComputeBoundSets_rec(Kit_DsdNtk_t *p, int iLit, Vec_Int_t *vSets, int nSizeMax)
Definition: lpkAbcDsd.c:108
#define Kit_DsdObjForEachFanin(pNtk, pObj, iLit, i)
Definition: kit.h:157
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
#define assert(ex)
Definition: util_old.h:213
static int Kit_WordCountOnes(unsigned uWord)
Definition: kit.h:243
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 
544 finish:
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 }
Lpk_Par_t * pPars
Definition: lpkInt.h:72
int Kit_DsdNonDsdSizeMax(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:1211
unsigned Lpk_DsdLateArriving(Lpk_Fun_t *p)
Definition: lpkAbcDsd.c:352
unsigned nVars
Definition: lpkInt.h:148
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
unsigned nLutK
Definition: lpkInt.h:149
Kit_DsdNtk_t * Kit_DsdDecomposeExpand(unsigned *pTruth, int nVars)
Definition: kitDsd.c:2330
unsigned uSupp
Definition: lpkInt.h:154
int nBSVars
Definition: lpkInt.h:165
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
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
static unsigned * Lpk_FunTruth(Lpk_Fun_t *p, int Num)
Definition: lpkInt.h:179
Vec_Int_t * Lpk_ComputeBoundSets(Kit_DsdNtk_t *p, int nSizeMax)
Definition: lpkAbcDsd.c:162
unsigned * ppTruths[5][16]
Definition: lpkInt.h:103
static void Kit_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:355
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:163
#define assert(ex)
Definition: util_old.h:213
int nBlocks[17]
Definition: lpkInt.h:122
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static unsigned Kit_BitMask(int nBits)
Definition: kit.h:225
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 );
415 if ( fVerbose )
416 Kit_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 }
char * memset()
int Kit_DsdNonDsdSizeMax(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:1211
int nCofVars
Definition: lpkInt.h:167
unsigned Lpk_DsdLateArriving(Lpk_Fun_t *p)
Definition: lpkAbcDsd.c:352
unsigned nVars
Definition: lpkInt.h:148
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
unsigned nLutK
Definition: lpkInt.h:149
Kit_DsdNtk_t * Kit_DsdDecomposeExpand(unsigned *pTruth, int nVars)
Definition: kitDsd.c:2330
unsigned Kit_DsdNonDsdSupports(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:1264
unsigned uSupp
Definition: lpkInt.h:154
unsigned fSupports
Definition: lpkInt.h:152
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
unsigned BSVars
Definition: lpkInt.h:166
char pCofVars[4]
Definition: lpkInt.h:168
void Kit_DsdPrint(FILE *pFile, Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:374
Vec_Int_t * Lpk_ComputeBoundSets(Kit_DsdNtk_t *p, int nSizeMax)
Definition: lpkAbcDsd.c:162
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
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:163
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
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 }
unsigned uSupp
Definition: lpkInt.h:154
if(last==0)
Definition: sparse_int.h:34
#define Lpk_SuppForEachVar(Supp, Var)
Definition: lpkInt.h:195
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;
602  Lpk_FunSuppMinimize( p );
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 nAreaLim
Definition: lpkInt.h:150
unsigned nVars
Definition: lpkInt.h:148
int Lpk_SuppDelay(unsigned uSupp, char *pDelays)
Definition: lpkAbcUtil.c:215
Kit_DsdNtk_t * Kit_DsdDecomposeExpand(unsigned *pTruth, int nVars)
Definition: kitDsd.c:2330
unsigned uSupp
Definition: lpkInt.h:154
unsigned fSupports
Definition: lpkInt.h:152
void Kit_TruthMuxVar(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
Definition: kitTruth.c:1069
void Kit_DsdTruthPartialTwo(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp, int iVar, unsigned *pTruthCo, unsigned *pTruthDec)
Definition: kitDsd.c:1089
unsigned Id
Definition: lpkInt.h:147
static unsigned * Lpk_FunTruth(Lpk_Fun_t *p, int Num)
Definition: lpkInt.h:179
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:521
unsigned * ppTruths[5][16]
Definition: lpkInt.h:103
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:573
int Lpk_FunSuppMinimize(Lpk_Fun_t *p)
Definition: lpkAbcUtil.c:143
Kit_DsdMan_t * pDsdMan
Definition: lpkInt.h:106
static int Kit_WordFindFirstBit(unsigned uWord)
Definition: kit.h:231
char pDelays[16]
Definition: lpkInt.h:156
Lpk_Fun_t * Lpk_FunDup(Lpk_Fun_t *p, unsigned *pTruth)
Definition: lpkAbcUtil.c:114
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition: kitTruth.c:346
static void Kit_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:355
char pFanins[16]
Definition: lpkInt.h:157
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:163
unsigned nDelayLim
Definition: lpkInt.h:151
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;
292 if ( fVerbose )
293 {
294 Lpk_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 );
307 if ( fVerbose )
308 printf( "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  }
321 if ( fVerbose )
322 {
323 if ( pRes->BSVars )
324 {
325 printf( "Found bound set " );
326 Lpk_PrintSetOne( pRes->BSVars );
327 printf( "\n" );
328 }
329 else
330 printf( "Did not find boundsets.\n" );
331 printf( "\n" );
332 }
333  if ( pRes->BSVars )
334  {
335  assert( pRes->DelayEst <= (int)p->nDelayLim );
336  assert( pRes->AreaEst <= (int)p->nAreaLim );
337  }
338 }
char * memset()
unsigned nAreaLim
Definition: lpkInt.h:150
unsigned nVars
Definition: lpkInt.h:148
int Lpk_SuppDelay(unsigned uSupp, char *pDelays)
Definition: lpkAbcUtil.c:215
unsigned nLutK
Definition: lpkInt.h:149
int AreaEst
Definition: lpkInt.h:172
int nBSVars
Definition: lpkInt.h:165
unsigned BSVars
Definition: lpkInt.h:166
static void Lpk_PrintSetOne(int uSupport)
Definition: lpkAbcDsd.c:204
int DelayEst
Definition: lpkInt.h:171
int nSuppSizeS
Definition: lpkInt.h:169
char pDelays[16]
Definition: lpkInt.h:156
static int Lpk_LutNumLuts(int nVarsMax, int nLutK)
Definition: lpkInt.h:178
#define assert(ex)
Definition: util_old.h:213
static int Kit_WordCountOnes(unsigned uWord)
Definition: kit.h:243
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int nSuppSizeL
Definition: lpkInt.h:170
unsigned nDelayLim
Definition: lpkInt.h:151
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 }
unsigned nVars
Definition: lpkInt.h:148
unsigned uSupp
Definition: lpkInt.h:154
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:521
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:573
int Var
Definition: SolverTypes.h:42
#define assert(ex)
Definition: util_old.h:213
static int Kit_WordCountOnes(unsigned uWord)
Definition: kit.h:243
#define Lpk_SuppForEachVar(Supp, Var)
Definition: lpkInt.h:195
unsigned puSupps[32]
Definition: lpkInt.h:155
int Kit_TruthSupportSize(unsigned *pTruth, int nVars)
Definition: kitTruth.c:327
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 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Kit_WordCountOnes(unsigned uWord)
Definition: kit.h:243
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static void Lpk_PrintSetOne ( int  uSupport)
static

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

Synopsis [Prints the sets of subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 204 of file lpkAbcDsd.c.

205 {
206  unsigned k;
207  for ( k = 0; k < 16; k++ )
208  if ( uSupport & (1<<k) )
209  printf( "%c", 'a'+k );
210  printf( " " );
211 }
static void Lpk_PrintSets ( Vec_Int_t vSets)
static

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

Synopsis [Prints the sets of subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file lpkAbcDsd.c.

224 {
225  unsigned uSupport;
226  int Number, i;
227  printf( "Subsets(%d): ", Vec_IntSize(vSets) );
228  Vec_IntForEachEntry( vSets, Number, i )
229  {
230  uSupport = Number;
231  Lpk_PrintSetOne( uSupport );
232  }
233  printf( "\n" );
234 }
static void Lpk_PrintSetOne(int uSupport)
Definition: lpkAbcDsd.c:204
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54