abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
lpkAbcDsd.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [lpkAbcDsd.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Fast Boolean matching for LUT structures.]
8 
9  Synopsis [LUT-decomposition based on recursive DSD.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - April 28, 2007.]
16 
17  Revision [$Id: lpkAbcDsd.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "lpkInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Cofactors TTs w.r.t. all vars and finds the best var.]
37 
38  Description [The best variable is the variable with the minimum
39  sum total of the support sizes of all truth tables. This procedure
40  computes and returns cofactors w.r.t. the best variable.]
41 
42  SideEffects []
43 
44  SeeAlso []
45 
46 ***********************************************************************/
47 int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs, unsigned uNonDecSupp )
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 }
96 
97 /**Function*************************************************************
98 
99  Synopsis [Recursively computes decomposable subsets.]
100 
101  Description []
102 
103  SideEffects []
104 
105  SeeAlso []
106 
107 ***********************************************************************/
108 unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets, int nSizeMax )
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 }
150 
151 /**Function*************************************************************
152 
153  Synopsis [Computes the set of subsets of decomposable variables.]
154 
155  Description []
156 
157  SideEffects []
158 
159  SeeAlso []
160 
161 ***********************************************************************/
162 Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax )
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 }
192 
193 /**Function*************************************************************
194 
195  Synopsis [Prints the sets of subsets.]
196 
197  Description []
198 
199  SideEffects []
200 
201  SeeAlso []
202 
203 ***********************************************************************/
204 static void Lpk_PrintSetOne( int uSupport )
205 {
206  unsigned k;
207  for ( k = 0; k < 16; k++ )
208  if ( uSupport & (1<<k) )
209  printf( "%c", 'a'+k );
210  printf( " " );
211 }
212 /**Function*************************************************************
213 
214  Synopsis [Prints the sets of subsets.]
215 
216  Description []
217 
218  SideEffects []
219 
220  SeeAlso []
221 
222 ***********************************************************************/
223 static void Lpk_PrintSets( Vec_Int_t * vSets )
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 }
235 
236 /**Function*************************************************************
237 
238  Synopsis [Merges two bound sets.]
239 
240  Description []
241 
242  SideEffects []
243 
244  SeeAlso []
245 
246 ***********************************************************************/
247 Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSizeMax )
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 }
264 
265 /**Function*************************************************************
266 
267  Synopsis [Performs DSD-based decomposition of the function.]
268 
269  Description []
270 
271  SideEffects []
272 
273  SeeAlso []
274 
275 ***********************************************************************/
276 void Lpk_FunCompareBoundSets( Lpk_Fun_t * p, Vec_Int_t * vBSets, int nCofDepth, unsigned uNonDecSupp, unsigned uLateArrSupp, Lpk_Res_t * pRes )
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 }
339 
340 
341 /**Function*************************************************************
342 
343  Synopsis [Finds late arriving inputs, which cannot be in the bound set.]
344 
345  Description []
346 
347  SideEffects []
348 
349  SeeAlso []
350 
351 ***********************************************************************/
352 unsigned Lpk_DsdLateArriving( Lpk_Fun_t * p )
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 }
360 
361 /**Function*************************************************************
362 
363  Synopsis [Performs DSD-based decomposition of the function.]
364 
365  Description []
366 
367  SideEffects []
368 
369  SeeAlso []
370 
371 ***********************************************************************/
372 int Lpk_DsdAnalizeOne( Lpk_Fun_t * p, unsigned * ppTruths[5][16], Kit_DsdNtk_t * pNtks[], char pCofVars[], int nCofDepth, Lpk_Res_t * pRes )
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 }
440 
441 /**Function*************************************************************
442 
443  Synopsis [Performs DSD-based decomposition of the function.]
444 
445  Description []
446 
447  SideEffects []
448 
449  SeeAlso []
450 
451 ***********************************************************************/
452 Lpk_Res_t * Lpk_DsdAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p, int nShared )
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 }
552 
553 /**Function*************************************************************
554 
555  Synopsis [Splits the function into two subfunctions using DSD.]
556 
557  Description []
558 
559  SideEffects []
560 
561  SeeAlso []
562 
563 ***********************************************************************/
564 Lpk_Fun_t * Lpk_DsdSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet )
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 }
610 
611 ////////////////////////////////////////////////////////////////////////
612 /// END OF FILE ///
613 ////////////////////////////////////////////////////////////////////////
614 
615 
616 ABC_NAMESPACE_IMPL_END
617 
memset
char * memset()
Kit_DsdObj_t_::Type
unsigned Type
Definition: kit.h:112
Lpk_Fun_t_::nAreaLim
unsigned nAreaLim
Definition: lpkInt.h:150
Kit_DsdNtkRoot
static Kit_DsdObj_t * Kit_DsdNtkRoot(Kit_DsdNtk_t *pNtk)
Definition: kit.h:151
Lpk_Man_t_::pPars
Lpk_Par_t * pPars
Definition: lpkInt.h:72
Kit_DsdNonDsdSizeMax
int Kit_DsdNonDsdSizeMax(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:1211
Lpk_Res_t_::nCofVars
int nCofVars
Definition: lpkInt.h:167
Lpk_DsdLateArriving
unsigned Lpk_DsdLateArriving(Lpk_Fun_t *p)
Definition: lpkAbcDsd.c:352
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Lpk_Fun_t_::nVars
unsigned nVars
Definition: lpkInt.h:148
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Kit_DsdObj_t_::nFans
unsigned nFans
Definition: kit.h:116
Lpk_SuppDelay
int Lpk_SuppDelay(unsigned uSupp, char *pDelays)
Definition: lpkAbcUtil.c:215
Lpk_Fun_t_::nLutK
unsigned nLutK
Definition: lpkInt.h:149
Lpk_Res_t_::AreaEst
int AreaEst
Definition: lpkInt.h:172
Kit_DsdDecomposeExpand
Kit_DsdNtk_t * Kit_DsdDecomposeExpand(unsigned *pTruth, int nVars)
Definition: kitDsd.c:2330
Kit_DsdNtkObj
static Kit_DsdObj_t * Kit_DsdNtkObj(Kit_DsdNtk_t *pNtk, int Id)
Definition: kit.h:150
Kit_DsdNonDsdSupports
unsigned Kit_DsdNonDsdSupports(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:1264
Lpk_Fun_t_::uSupp
unsigned uSupp
Definition: lpkInt.h:154
Kit_DsdNtk_t_::Root
unsigned short Root
Definition: kit.h:127
Lpk_Fun_t_::fSupports
unsigned fSupports
Definition: lpkInt.h:152
Lpk_ComputeBoundSets_rec
unsigned Lpk_ComputeBoundSets_rec(Kit_DsdNtk_t *p, int iLit, Vec_Int_t *vSets, int nSizeMax)
Definition: lpkAbcDsd.c:108
Kit_TruthMuxVar
void Kit_TruthMuxVar(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
Definition: kitTruth.c:1069
Lpk_Res_t_::nBSVars
int nBSVars
Definition: lpkInt.h:165
Kit_DsdObjForEachFanin
#define Kit_DsdObjForEachFanin(pNtk, pObj, iLit, i)
Definition: kit.h:157
Kit_DsdTruthPartialTwo
void Kit_DsdTruthPartialTwo(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp, int iVar, unsigned *pTruthCo, unsigned *pTruthDec)
Definition: kitDsd.c:1089
Lpk_Res_t_
Definition: lpkInt.h:163
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Lpk_FunCompareBoundSets
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
Lpk_DsdSplit
Lpk_Fun_t * Lpk_DsdSplit(Lpk_Man_t *pMan, Lpk_Fun_t *p, char *pCofVars, int nCofVars, unsigned uBoundSet)
Definition: lpkAbcDsd.c:564
Lpk_Res_t_::BSVars
unsigned BSVars
Definition: lpkInt.h:166
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)
Definition: lpkAbcDsd.c:372
Lpk_Fun_t_::Id
unsigned Id
Definition: lpkInt.h:147
Kit_DsdNtk_t_
Definition: kit.h:122
Kit_DsdObj_t_
Definition: kit.h:109
Lpk_FunTruth
static unsigned * Lpk_FunTruth(Lpk_Fun_t *p, int Num)
Definition: lpkInt.h:179
Kit_TruthCofactor0New
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:521
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Lpk_Res_t_::pCofVars
char pCofVars[4]
Definition: lpkInt.h:168
Kit_DsdPrint
void Kit_DsdPrint(FILE *pFile, Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:374
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Lpk_ComputeBoundSets
Vec_Int_t * Lpk_ComputeBoundSets(Kit_DsdNtk_t *p, int nSizeMax)
Definition: lpkAbcDsd.c:162
Lpk_PrintSetOne
static void Lpk_PrintSetOne(int uSupport)
Definition: lpkAbcDsd.c:204
Lpk_PrintSets
static void Lpk_PrintSets(Vec_Int_t *vSets)
Definition: lpkAbcDsd.c:223
Lpk_FunComputeMinSuppSizeVar
ABC_NAMESPACE_IMPL_START int Lpk_FunComputeMinSuppSizeVar(Lpk_Fun_t *p, unsigned **ppTruths, int nTruths, unsigned **ppCofs, unsigned uNonDecSupp)
DECLARATIONS ///.
Definition: lpkAbcDsd.c:47
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Lpk_Man_t_::ppTruths
unsigned * ppTruths[5][16]
Definition: lpkInt.h:103
Kit_TruthCofactor1New
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:573
Lpk_FunSuppMinimize
int Lpk_FunSuppMinimize(Lpk_Fun_t *p)
Definition: lpkAbcUtil.c:143
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Lpk_Res_t_::DelayEst
int DelayEst
Definition: lpkInt.h:171
Lpk_Res_t_::nSuppSizeS
int nSuppSizeS
Definition: lpkInt.h:169
Lpk_Man_t_::pDsdMan
Kit_DsdMan_t * pDsdMan
Definition: lpkInt.h:106
Lpk_DsdAnalize
Lpk_Res_t * Lpk_DsdAnalize(Lpk_Man_t *pMan, Lpk_Fun_t *p, int nShared)
Definition: lpkAbcDsd.c:452
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Lpk_Fun_t_
Definition: lpkInt.h:144
Lpk_MergeBoundSets
Vec_Int_t * Lpk_MergeBoundSets(Vec_Int_t *vSets0, Vec_Int_t *vSets1, int nSizeMax)
Definition: lpkAbcDsd.c:247
Kit_WordFindFirstBit
static int Kit_WordFindFirstBit(unsigned uWord)
Definition: kit.h:231
Lpk_Man_t_
Definition: lpkInt.h:69
Lpk_Fun_t_::pDelays
char pDelays[16]
Definition: lpkInt.h:156
Lpk_FunDup
Lpk_Fun_t * Lpk_FunDup(Lpk_Fun_t *p, unsigned *pTruth)
Definition: lpkAbcUtil.c:114
Kit_TruthSupport
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition: kitTruth.c:346
Kit_TruthCopy
static void Kit_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:355
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Minisat::Var
int Var
Definition: SolverTypes.h:42
Lpk_Fun_t_::pFanins
char pFanins[16]
Definition: lpkInt.h:157
Lpk_LutNumLuts
static int Lpk_LutNumLuts(int nVarsMax, int nLutK)
Definition: lpkInt.h:178
Kit_DsdNtkFree
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:163
assert
#define assert(ex)
Definition: util_old.h:213
Lpk_Man_t_::nBlocks
int nBlocks[17]
Definition: lpkInt.h:122
Kit_WordCountOnes
static int Kit_WordCountOnes(unsigned uWord)
Definition: kit.h:243
Lpk_SuppForEachVar
#define Lpk_SuppForEachVar(Supp, Var)
Definition: lpkInt.h:195
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Lpk_Fun_t_::puSupps
unsigned puSupps[32]
Definition: lpkInt.h:155
Kit_DsdNtk_t_::nVars
unsigned short nVars
Definition: kit.h:124
Kit_TruthSupportSize
int Kit_TruthSupportSize(unsigned *pTruth, int nVars)
Definition: kitTruth.c:327
Kit_BitMask
static unsigned Kit_BitMask(int nBits)
Definition: kit.h:225
Lpk_Res_t_::nSuppSizeL
int nSuppSizeL
Definition: lpkInt.h:170
Lpk_Fun_t_::nDelayLim
unsigned nDelayLim
Definition: lpkInt.h:151