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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Lpk_CreateVarOrder (Kit_DsdNtk_t *pNtk, char pTable[][16])
 DECLARATIONS ///. More...
 
void Lpk_CreateCommonOrder (char pTable[][16], int piCofVar[], int nCBars, int pPrios[], int nVars, int fVerbose)
 
int Lpk_FindHighest (Kit_DsdNtk_t **ppNtks, int *piLits, int nSize, int *pPrio, int *pDecision)
 
If_Obj_t * Lpk_MapTreeMulti_rec (Lpk_Man_t *p, Kit_DsdNtk_t **ppNtks, int *piLits, int *piCofVar, int nCBars, If_Obj_t **ppLeaves, int nLeaves, int *pPrio)
 
If_Obj_t * Lpk_MapTreeMulti (Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
 

Function Documentation

void Lpk_CreateCommonOrder ( char  pTable[][16],
int  piCofVar[],
int  nCBars,
int  pPrios[],
int  nVars,
int  fVerbose 
)

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

Synopsis [Creates commmon variable order.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file lpkMulti.c.

88 {
89  int Score[16] = {0}, pPres[16];
90  int i, y, x, iVarBest, ScoreMax, PrioCount;
91 
92  // mark the present variables
93  for ( i = 0; i < nVars; i++ )
94  pPres[i] = 1;
95  // remove cofactored variables
96  for ( i = 0; i < nCBars; i++ )
97  pPres[piCofVar[i]] = 0;
98 
99  // compute scores for each leaf
100  for ( i = 0; i < nVars; i++ )
101  {
102  if ( pPres[i] == 0 )
103  continue;
104  for ( y = 0; y < nVars; y++ )
105  Score[i] += pTable[i][y];
106  for ( x = 0; x < nVars; x++ )
107  Score[i] -= pTable[x][i];
108  }
109 
110  // print the scores
111  if ( fVerbose )
112  {
113  printf( "Scores: " );
114  for ( i = 0; i < nVars; i++ )
115  printf( "%c=%d ", 'a'+i, Score[i] );
116  printf( " " );
117  printf( "Prios: " );
118  }
119 
120  // derive variable priority
121  // variables with equal score receive the same priority
122  for ( i = 0; i < nVars; i++ )
123  pPrios[i] = 16;
124 
125  // iterate until variables remain
126  for ( PrioCount = 1; ; PrioCount++ )
127  {
128  // find the present variable with the highest score
129  iVarBest = -1;
130  ScoreMax = -100000;
131  for ( i = 0; i < nVars; i++ )
132  {
133  if ( pPres[i] == 0 )
134  continue;
135  if ( ScoreMax < Score[i] )
136  {
137  ScoreMax = Score[i];
138  iVarBest = i;
139  }
140  }
141  if ( iVarBest == -1 )
142  break;
143  // give the next priority to all vars having this score
144  if ( fVerbose )
145  printf( "%d=", PrioCount );
146  for ( i = 0; i < nVars; i++ )
147  {
148  if ( pPres[i] == 0 )
149  continue;
150  if ( Score[i] == ScoreMax )
151  {
152  pPrios[i] = PrioCount;
153  pPres[i] = 0;
154  if ( fVerbose )
155  printf( "%c", 'a'+i );
156  }
157  }
158  if ( fVerbose )
159  printf( " " );
160  }
161  if ( fVerbose )
162  printf( "\n" );
163 }
ABC_NAMESPACE_IMPL_START void Lpk_CreateVarOrder ( Kit_DsdNtk_t *  pNtk,
char  pTable[][16] 
)

DECLARATIONS ///.

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

FileName [lpkMulti.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast Boolean matching for LUT structures.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

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

Synopsis [Records variable order.]

Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.]

SideEffects []

SeeAlso []

Definition at line 45 of file lpkMulti.c.

46 {
47  Kit_DsdObj_t * pObj;
48  unsigned uSuppFanins, k;
49  int Above[16], Below[16];
50  int nAbove, nBelow, iFaninLit, i, x, y;
51  // iterate through the nodes
52  Kit_DsdNtkForEachObj( pNtk, pObj, i )
53  {
54  // collect fanin support of this node
55  nAbove = 0;
56  uSuppFanins = 0;
57  Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k )
58  {
59  if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) )
60  Above[nAbove++] = Abc_Lit2Var(iFaninLit);
61  else
62  uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit );
63  }
64  // find the below variables
65  nBelow = 0;
66  for ( y = 0; y < 16; y++ )
67  if ( uSuppFanins & (1 << y) )
68  Below[nBelow++] = y;
69  // create all pairs
70  for ( x = 0; x < nAbove; x++ )
71  for ( y = 0; y < nBelow; y++ )
72  pTable[Above[x]][Below[y]]++;
73  }
74 }
Kit_DsdObjForEachFanin
#define Kit_DsdObjForEachFanin(pNtk, pObj, iLit, i)
Definition: kit.h:157
Kit_DsdObj_t_
Definition: kit.h:109
Kit_DsdNtkForEachObj
#define Kit_DsdNtkForEachObj(pNtk, pObj, i)
Definition: kit.h:155
Kit_DsdLitIsLeaf
static int Kit_DsdLitIsLeaf(Kit_DsdNtk_t *pNtk, int Lit)
Definition: kit.h:152
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Kit_DsdLitSupport
static unsigned Kit_DsdLitSupport(Kit_DsdNtk_t *pNtk, int Lit)
Definition: kit.h:153
int Lpk_FindHighest ( Kit_DsdNtk_t **  ppNtks,
int *  piLits,
int  nSize,
int *  pPrio,
int *  pDecision 
)

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

Synopsis [Finds components with the highest priority.]

Description [Returns the number of components selected.]

SideEffects []

SeeAlso []

Definition at line 176 of file lpkMulti.c.

177 {
178  Kit_DsdObj_t * pObj;
179  unsigned uSupps[8], uSuppFanin, uSuppTotal, uSuppLarge;
180  int i, pTriv[8], PrioMin, iVarMax, nComps, fOneNonTriv;
181 
182  // find individual support and total support
183  uSuppTotal = 0;
184  for ( i = 0; i < nSize; i++ )
185  {
186  pTriv[i] = 1;
187  if ( piLits[i] < 0 )
188  uSupps[i] = 0;
189  else if ( Kit_DsdLitIsLeaf(ppNtks[i], piLits[i]) )
190  uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] );
191  else
192  {
193  pObj = Kit_DsdNtkObj( ppNtks[i], Abc_Lit2Var(piLits[i]) );
194  if ( pObj->Type == KIT_DSD_PRIME )
195  {
196  pTriv[i] = 0;
197  uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] );
198  }
199  else
200  {
201  assert( pObj->nFans == 2 );
202  if ( !Kit_DsdLitIsLeaf(ppNtks[i], pObj->pFans[0]) )
203  pTriv[i] = 0;
204  uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[1] );
205  }
206  uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin;
207  }
208  assert( uSupps[i] <= 0xFFFF );
209  uSuppTotal |= uSupps[i];
210  }
211  if ( uSuppTotal == 0 )
212  return 0;
213 
214  // find one support variable with the highest priority
215  PrioMin = ABC_INFINITY;
216  iVarMax = -1;
217  for ( i = 0; i < 16; i++ )
218  if ( uSuppTotal & (1 << i) )
219  if ( PrioMin > pPrio[i] )
220  {
221  PrioMin = pPrio[i];
222  iVarMax = i;
223  }
224  assert( iVarMax != -1 );
225 
226  // select components, which have this variable
227  nComps = 0;
228  fOneNonTriv = 0;
229  uSuppLarge = 0;
230  for ( i = 0; i < nSize; i++ )
231  if ( uSupps[i] & (1<<iVarMax) )
232  {
233  if ( pTriv[i] || !fOneNonTriv )
234  {
235  if ( !pTriv[i] )
236  {
237  uSuppLarge = uSupps[i];
238  fOneNonTriv = 1;
239  }
240  pDecision[i] = 1;
241  nComps++;
242  }
243  else
244  pDecision[i] = 0;
245  }
246  else
247  pDecision[i] = 0;
248 
249  // add other non-trivial not-taken components whose support is contained in the current large component support
250  if ( fOneNonTriv )
251  for ( i = 0; i < nSize; i++ )
252  if ( !pTriv[i] && pDecision[i] == 0 && (uSupps[i] & ~uSuppLarge) == 0 )
253  {
254  pDecision[i] = 1;
255  nComps++;
256  }
257 
258  return nComps;
259 }
Kit_DsdObj_t_::Type
unsigned Type
Definition: kit.h:112
Kit_DsdObj_t_::nFans
unsigned nFans
Definition: kit.h:116
Kit_DsdNtkObj
static Kit_DsdObj_t * Kit_DsdNtkObj(Kit_DsdNtk_t *pNtk, int Id)
Definition: kit.h:150
Kit_DsdObj_t_
Definition: kit.h:109
Kit_DsdObj_t_::pFans
unsigned short pFans[0]
Definition: kit.h:117
Kit_DsdLitIsLeaf
static int Kit_DsdLitIsLeaf(Kit_DsdNtk_t *pNtk, int Lit)
Definition: kit.h:152
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
assert
#define assert(ex)
Definition: util_old.h:213
Kit_DsdLitSupport
static unsigned Kit_DsdLitSupport(Kit_DsdNtk_t *pNtk, int Lit)
Definition: kit.h:153
If_Obj_t* Lpk_MapTreeMulti ( Lpk_Man_t *  p,
unsigned *  pTruth,
int  nVars,
If_Obj_t **  ppLeaves 
)

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

Synopsis [Prepares the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 347 of file lpkMulti.c.

348 {
349  static int Counter = 0;
350  If_Obj_t * pResult;
351  Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp;
352  Kit_DsdObj_t * pRoot;
353  int piCofVar[4], pPrios[16], pFreqs[16] = {0}, piLits[16];
354  int i, k, nCBars, nSize, nMemSize;
355  unsigned * ppCofs[4][8], uSupport;
356  char pTable[16][16] = {
357  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
358  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
359  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
360  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
361  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
362  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
363  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
364  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
365  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
366  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
367  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
368  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
369  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
370  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
371  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
372  {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}
373  };
374  int fVerbose = p->pPars->fVeryVerbose;
375 
376  Counter++;
377 // printf( "Run %d.\n", Counter );
378 
379  // allocate storage for cofactors
380  nMemSize = Kit_TruthWordNum(nVars);
381  ppCofs[0][0] = ABC_ALLOC( unsigned, 32 * nMemSize );
382  nSize = 0;
383  for ( i = 0; i < 4; i++ )
384  for ( k = 0; k < 8; k++ )
385  ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
386  assert( nSize == 32 );
387 
388  // find the best cofactoring variables
389  nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 );
390 // nCBars = 2;
391 // piCofVar[0] = 0;
392 // piCofVar[1] = 1;
393 
394 
395  // copy the function
396  Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
397 
398  // decompose w.r.t. these variables
399  for ( k = 0; k < nCBars; k++ )
400  {
401  nSize = (1 << k);
402  for ( i = 0; i < nSize; i++ )
403  {
404  Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
405  Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
406  }
407  }
408  nSize = (1 << nCBars);
409  // compute DSD networks
410  for ( i = 0; i < nSize; i++ )
411  {
412  ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars );
413  ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
414  Kit_DsdNtkFree( pTemp );
415  if ( fVerbose )
416  {
417  printf( "Cof%d%d: ", nCBars, i );
418  Kit_DsdPrint( stdout, ppNtks[i] );
419  }
420  }
421 
422  // compute variable frequences
423  for ( i = 0; i < nSize; i++ )
424  {
425  uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars );
426  for ( k = 0; k < nVars; k++ )
427  if ( uSupport & (1<<k) )
428  pFreqs[k]++;
429  }
430 
431  // find common variable order
432  for ( i = 0; i < nSize; i++ )
433  {
434  Kit_DsdGetSupports( ppNtks[i] );
435  Lpk_CreateVarOrder( ppNtks[i], pTable );
436  }
437  Lpk_CreateCommonOrder( pTable, piCofVar, nCBars, pPrios, nVars, fVerbose );
438  // update priorities with frequences
439  for ( i = 0; i < nVars; i++ )
440  pPrios[i] = pPrios[i] * 256 + (16 - pFreqs[i]) * 16 + i;
441 
442  if ( fVerbose )
443  printf( "After restructuring with priority:\n" );
444 
445  // transform all networks according to the variable order
446  for ( i = 0; i < nSize; i++ )
447  {
448  ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios );
449  Kit_DsdNtkFree( pTemp );
450  Kit_DsdGetSupports( ppNtks[i] );
451  assert( ppNtks[i]->pSupps[0] <= 0xFFFF );
452  // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible
453  Kit_DsdRotate( ppNtks[i], pFreqs );
454  // print the resulting networks
455  if ( fVerbose )
456  {
457  printf( "Cof%d%d: ", nCBars, i );
458  Kit_DsdPrint( stdout, ppNtks[i] );
459  }
460  }
461 
462  for ( i = 0; i < nSize; i++ )
463  {
464  // collect the roots
465  pRoot = Kit_DsdNtkRoot(ppNtks[i]);
466  if ( pRoot->Type == KIT_DSD_CONST1 )
467  piLits[i] = Abc_LitIsCompl(ppNtks[i]->Root)? -2: -1;
468  else if ( pRoot->Type == KIT_DSD_VAR )
469  piLits[i] = Abc_LitNotCond( pRoot->pFans[0], Abc_LitIsCompl(ppNtks[i]->Root) );
470  else
471  piLits[i] = ppNtks[i]->Root;
472  }
473 
474 
475  // recursively construct AIG for mapping
476  p->fCofactoring = 1;
477  pResult = Lpk_MapTreeMulti_rec( p, ppNtks, piLits, piCofVar, nCBars, ppLeaves, nVars, pPrios );
478  p->fCofactoring = 0;
479 
480  if ( fVerbose )
481  printf( "\n" );
482 
483  // verify the transformations
484  nSize = (1 << nCBars);
485  for ( i = 0; i < nSize; i++ )
486  Kit_DsdTruth( ppNtks[i], ppCofs[nCBars][i] );
487  // mux the truth tables
488  for ( k = nCBars-1; k >= 0; k-- )
489  {
490  nSize = (1 << k);
491  for ( i = 0; i < nSize; i++ )
492  Kit_TruthMuxVar( ppCofs[k][i], ppCofs[k+1][2*i+0], ppCofs[k+1][2*i+1], nVars, piCofVar[k] );
493  }
494  if ( !Extra_TruthIsEqual( pTruth, ppCofs[0][0], nVars ) )
495  printf( "Verification failed.\n" );
496 
497 
498  // free the networks
499  for ( i = 0; i < 8; i++ )
500  if ( ppNtks[i] )
501  Kit_DsdNtkFree( ppNtks[i] );
502  ABC_FREE( ppCofs[0][0] );
503 
504  return pResult;
505 }
Lpk_CreateCommonOrder
void Lpk_CreateCommonOrder(char pTable[][16], int piCofVar[], int nCBars, int pPrios[], int nVars, int fVerbose)
Definition: lpkMulti.c:87
Kit_DsdObj_t_::Type
unsigned Type
Definition: kit.h:112
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_TruthWordNum
static int Kit_TruthWordNum(int nVars)
Definition: kit.h:224
pFreqs
static int pFreqs[13719]
Definition: rwrTemp.c:31
Kit_DsdGetSupports
unsigned Kit_DsdGetSupports(Kit_DsdNtk_t *p)
Definition: kitDsd.c:1762
If_Obj_t_
Definition: if.h:303
Kit_DsdTruth
void Kit_DsdTruth(Kit_DsdNtk_t *pNtk, unsigned *pTruthRes)
Definition: kitDsd.c:1068
Kit_DsdNtk_t_::Root
unsigned short Root
Definition: kit.h:127
Kit_TruthMuxVar
void Kit_TruthMuxVar(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
Definition: kitTruth.c:1069
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Kit_DsdDecompose
Kit_DsdNtk_t * Kit_DsdDecompose(unsigned *pTruth, int nVars)
Definition: kitDsd.c:2314
Kit_DsdNtk_t_
Definition: kit.h:122
Kit_DsdObj_t_
Definition: kit.h:109
Lpk_MapTreeMulti_rec
If_Obj_t * Lpk_MapTreeMulti_rec(Lpk_Man_t *p, Kit_DsdNtk_t **ppNtks, int *piLits, int *piCofVar, int nCBars, If_Obj_t **ppLeaves, int nLeaves, int *pPrio)
Definition: lpkMulti.c:272
Kit_TruthCofactor0New
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:521
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Kit_DsdPrint
void Kit_DsdPrint(FILE *pFile, Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:374
Lpk_Man_t_::fCofactoring
int fCofactoring
Definition: lpkInt.h:90
Kit_TruthCofactor1New
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:573
Counter
static int Counter
Definition: extraBddMisc.c:1877
Kit_DsdRotate
void Kit_DsdRotate(Kit_DsdNtk_t *p, int pFreqs[])
Definition: kitDsd.c:1671
Kit_DsdObj_t_::pFans
unsigned short pFans[0]
Definition: kit.h:117
Extra_TruthIsEqual
static int Extra_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: extra.h:270
Kit_DsdShrink
Kit_DsdNtk_t * Kit_DsdShrink(Kit_DsdNtk_t *p, int pPrios[])
Definition: kitDsd.c:1633
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Kit_TruthSupport
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition: kitTruth.c:346
Kit_DsdCofactoring
int Kit_DsdCofactoring(unsigned *pTruth, int nVars, int *pCofVars, int nLimit, int fVerbose)
Definition: kitDsd.c:2678
pSupps
static int * pSupps
Definition: abcUtil.c:2053
Kit_TruthCopy
static void Kit_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:355
Kit_DsdNtkFree
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:163
assert
#define assert(ex)
Definition: util_old.h:213
Lpk_CreateVarOrder
ABC_NAMESPACE_IMPL_START void Lpk_CreateVarOrder(Kit_DsdNtk_t *pNtk, char pTable[][16])
DECLARATIONS ///.
Definition: lpkMulti.c:45
Kit_DsdExpand
Kit_DsdNtk_t * Kit_DsdExpand(Kit_DsdNtk_t *p)
Definition: kitDsd.c:1451
If_Obj_t* Lpk_MapTreeMulti_rec ( Lpk_Man_t *  p,
Kit_DsdNtk_t **  ppNtks,
int *  piLits,
int *  piCofVar,
int  nCBars,
If_Obj_t **  ppLeaves,
int  nLeaves,
int *  pPrio 
)

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

Synopsis [Prepares the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 272 of file lpkMulti.c.

273 {
274  Kit_DsdObj_t * pObj;
275  If_Obj_t * pObjsNew[4][8], * pResPrev;
276  int piLitsNew[8], pDecision[8];
277  int i, k, nComps, nSize;
278 
279  // find which of the variables is highest in the order
280  nSize = (1 << nCBars);
281  nComps = Lpk_FindHighest( ppNtks, piLits, nSize, pPrio, pDecision );
282  if ( nComps == 0 )
283  return If_Not( If_ManConst1(p->pIfMan) );
284 
285  // iterate over the nodes
286  if ( p->pPars->fVeryVerbose )
287  printf( "Decision: " );
288  for ( i = 0; i < nSize; i++ )
289  {
290  if ( pDecision[i] )
291  {
292  if ( p->pPars->fVeryVerbose )
293  printf( "%d ", i );
294  assert( piLits[i] >= 0 );
295  pObj = Kit_DsdNtkObj( ppNtks[i], Abc_Lit2Var(piLits[i]) );
296  if ( pObj == NULL )
297  piLitsNew[i] = -2;
298  else if ( pObj->Type == KIT_DSD_PRIME )
299  piLitsNew[i] = pObj->pFans[0];
300  else
301  piLitsNew[i] = pObj->pFans[1];
302  }
303  else
304  piLitsNew[i] = piLits[i];
305  }
306  if ( p->pPars->fVeryVerbose )
307  printf( "\n" );
308 
309  // call again
310  pResPrev = Lpk_MapTreeMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pPrio );
311 
312  // create new set of nodes
313  for ( i = 0; i < nSize; i++ )
314  {
315  if ( pDecision[i] )
316  pObjsNew[nCBars][i] = Lpk_MapTree_rec( p, ppNtks[i], ppLeaves, piLits[i], pResPrev );
317  else if ( piLits[i] == -1 )
318  pObjsNew[nCBars][i] = If_ManConst1(p->pIfMan);
319  else if ( piLits[i] == -2 )
320  pObjsNew[nCBars][i] = If_Not( If_ManConst1(p->pIfMan) );
321  else
322  pObjsNew[nCBars][i] = pResPrev;
323  }
324 
325  // create MUX using these outputs
326  for ( k = nCBars; k > 0; k-- )
327  {
328  nSize /= 2;
329  for ( i = 0; i < nSize; i++ )
330  pObjsNew[k-1][i] = If_ManCreateMux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] );
331  }
332  assert( nSize == 1 );
333  return pObjsNew[0][0];
334 }
Kit_DsdObj_t_::Type
unsigned Type
Definition: kit.h:112
Lpk_Man_t_::pPars
Lpk_Par_t * pPars
Definition: lpkInt.h:72
If_Obj_t_
Definition: if.h:303
Lpk_MapTree_rec
If_Obj_t * Lpk_MapTree_rec(Lpk_Man_t *p, Kit_DsdNtk_t *pNtk, If_Obj_t **ppLeaves, int iLit, If_Obj_t *pResult)
Definition: lpkMap.c:110
Kit_DsdNtkObj
static Kit_DsdObj_t * Kit_DsdNtkObj(Kit_DsdNtk_t *pNtk, int Id)
Definition: kit.h:150
If_Not
static If_Obj_t * If_Not(If_Obj_t *p)
Definition: if.h:356
Kit_DsdObj_t_
Definition: kit.h:109
Lpk_MapTreeMulti_rec
If_Obj_t * Lpk_MapTreeMulti_rec(Lpk_Man_t *p, Kit_DsdNtk_t **ppNtks, int *piLits, int *piCofVar, int nCBars, If_Obj_t **ppLeaves, int nLeaves, int *pPrio)
Definition: lpkMulti.c:272
If_ManCreateMux
If_Obj_t * If_ManCreateMux(If_Man_t *p, If_Obj_t *pFan0, If_Obj_t *pFan1, If_Obj_t *pCtrl)
Definition: ifMan.c:423
If_ManConst1
static If_Obj_t * If_ManConst1(If_Man_t *p)
Definition: if.h:365
Kit_DsdObj_t_::pFans
unsigned short pFans[0]
Definition: kit.h:117
Lpk_Man_t_::pIfMan
If_Man_t * pIfMan
Definition: lpkInt.h:86
Lpk_FindHighest
int Lpk_FindHighest(Kit_DsdNtk_t **ppNtks, int *piLits, int nSize, int *pPrio, int *pDecision)
Definition: lpkMulti.c:176
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
assert
#define assert(ex)
Definition: util_old.h:213