summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/kit/kit.h15
-rw-r--r--src/opt/kit/kitDsd.c492
-rw-r--r--src/opt/lpk/lpk.h82
-rw-r--r--src/opt/lpk/lpkCore.c280
-rw-r--r--src/opt/lpk/lpkCut.c584
-rw-r--r--src/opt/lpk/lpkInt.h161
-rw-r--r--src/opt/lpk/lpkMan.c96
-rw-r--r--src/opt/lpk/lpkMap.c349
-rw-r--r--src/opt/lpk/lpkMulti.c495
-rw-r--r--src/opt/lpk/lpkMux.c257
-rw-r--r--src/opt/lpk/lpkSets.c399
-rw-r--r--src/opt/lpk/lpk_.c48
-rw-r--r--src/opt/lpk/module.make7
13 files changed, 3167 insertions, 98 deletions
diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index a0552b19..229b0bce 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -159,6 +159,7 @@ static inline unsigned Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit )
#define KIT_MIN(a,b) (((a) < (b))? (a) : (b))
#define KIT_MAX(a,b) (((a) > (b))? (a) : (b))
+#define KIT_INFINITY (100000000)
#ifndef ALLOC
#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
@@ -235,6 +236,10 @@ static inline int Kit_WordFindFirstBit( unsigned uWord )
return i;
return -1;
}
+static inline int Kit_WordHasOneBit( unsigned uWord )
+{
+ return (uWord & (uWord - 1)) == 0;
+}
static inline int Kit_WordCountOnes( unsigned uWord )
{
uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
@@ -250,6 +255,14 @@ static inline int Kit_TruthCountOnes( unsigned * pIn, int nVars )
Counter += Kit_WordCountOnes(pIn[w]);
return Counter;
}
+static inline int Kit_TruthFindFirstBit( unsigned * pIn, int nVars )
+{
+ int w;
+ for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
+ if ( pIn[w] )
+ return Kit_WordFindFirstBit(pIn[w]);
+ return -1;
+}
static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
@@ -433,7 +446,9 @@ extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nV
/*=== kitDsd.c ==========================================================*/
extern Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
+extern void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes );
extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
+extern void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk );
extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
index 8dd1b06f..8b6b6979 100644
--- a/src/opt/kit/kitDsd.c
+++ b/src/opt/kit/kitDsd.c
@@ -47,7 +47,7 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars )
p->nVars = nVars;
p->nWords = Kit_TruthWordNum( p->nVars );
p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
- p->vTtNodes = Vec_PtrAllocSimInfo( 64, p->nWords );
+ p->vTtNodes = Vec_PtrAllocSimInfo( 1024, p->nWords );
return p;
}
@@ -262,6 +262,25 @@ void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk )
/**Function*************************************************************
+ Synopsis [Print the DSD formula.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
+{
+ Kit_DsdNtk_t * pTemp;
+ pTemp = Kit_DsdExpand( pNtk );
+ Kit_DsdPrint( stdout, pNtk );
+ Kit_DsdNtkFree( pTemp );
+}
+
+/**Function*************************************************************
+
Synopsis [Derives the truth table of the DSD node.]
Description []
@@ -384,6 +403,26 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk )
return pTruthRes;
}
+/**Function*************************************************************
+
+ Synopsis [Derives the truth table of the DSD network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
+{
+ Kit_DsdMan_t * p;
+ unsigned * pTruth;
+ p = Kit_DsdManAlloc( pNtk->nVars );
+ pTruth = Kit_DsdTruthCompute( p, pNtk );
+ Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
+ Kit_DsdManFree( p );
+}
/**Function*************************************************************
@@ -551,29 +590,25 @@ void Kit_DsdExpandCollectXor_rec( Kit_DsdNtk_t * p, int iLit, int * piLitsNew, i
int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
{
unsigned * pTruth, * pTruthNew;
- unsigned i, fCompl, iLitFanin, piLitsNew[16], nLitsNew = 0;
+ unsigned i, iLitFanin, piLitsNew[16], nLitsNew = 0;
Kit_DsdObj_t * pObj, * pObjNew;
- // remember the complement
- fCompl = Kit_DsdLitIsCompl(iLit);
- iLit = Kit_DsdLitRegular(iLit);
- assert( !Kit_DsdLitIsCompl(iLit) );
-
// consider the case of simple gate
pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
if ( pObj == NULL )
- return Kit_DsdLitNotCond( iLit, fCompl );
+ return iLit;
if ( pObj->Type == KIT_DSD_AND )
{
- Kit_DsdExpandCollectAnd_rec( p, iLit, piLitsNew, &nLitsNew );
+ Kit_DsdExpandCollectAnd_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, &nLitsNew );
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, nLitsNew );
for ( i = 0; i < pObjNew->nFans; i++ )
pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, piLitsNew[i] );
- return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
+ return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) );
}
if ( pObj->Type == KIT_DSD_XOR )
{
- Kit_DsdExpandCollectXor_rec( p, iLit, piLitsNew, &nLitsNew );
+ int fCompl = Kit_DsdLitIsCompl(iLit);
+ Kit_DsdExpandCollectXor_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, &nLitsNew );
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, nLitsNew );
for ( i = 0; i < pObjNew->nFans; i++ )
{
@@ -602,7 +637,7 @@ int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
}
}
// if the incoming phase is complemented, absorb it into the prime node
- if ( fCompl )
+ if ( Kit_DsdLitIsCompl(iLit) )
Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
return Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
@@ -655,46 +690,48 @@ Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p )
SeeAlso []
***********************************************************************/
-void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], int piLitsNew[], int nVars )
+void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned char * piLits, int nVars, int piLitsRes[] )
{
- int nSuppSizes[16], Priority[16], pOrder[16], Temp[16];
- int i, k, iVarBest, SuppMax, PrioMin;
+ int nSuppSizes[16], Priority[16], pOrder[16];
+ int i, k, iVarBest, SuppMax, PrioMax;
// compute support sizes and priorities of the components
for ( i = 0; i < nVars; i++ )
{
- Temp[i] = piLitsNew[i];
+ assert( uSupps[i] );
pOrder[i] = i;
- Priority[i] = 16;
- nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]);
+ Priority[i] = KIT_INFINITY;
for ( k = 0; k < 16; k++ )
if ( uSupps[i] & (1 << k) )
Priority[i] = KIT_MIN( Priority[i], pPrios[k] );
assert( Priority[i] != 16 );
+ nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]);
}
- // find the component by with largest size and smallest priority
+ // sort the components by pririty
+ Extra_BubbleSort( pOrder, Priority, nVars, 0 );
+ // find the component by with largest size and lowest priority
iVarBest = -1;
- SuppMax = 0;
- PrioMin = 16;
+ SuppMax = 0;
+ PrioMax = 0;
for ( i = 0; i < nVars; i++ )
{
- if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMin > Priority[i]) )
+ if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMax < Priority[i]) )
{
- SuppMax = nSuppSizes[i];
- PrioMin = Priority[i];
+ SuppMax = nSuppSizes[i];
+ PrioMax = Priority[i];
iVarBest = i;
}
}
- // sort the components by pririty
- Extra_BubbleSort( pOrder, Priority, nVars, 1 );
+ assert( iVarBest != -1 );
// copy the resulting literals
k = 0;
- piLitsNew[k++] = piLitsNew[iVarBest];
+ piLitsRes[k++] = piLits[iVarBest];
for ( i = 0; i < nVars; i++ )
{
if ( pOrder[i] == iVarBest )
continue;
- piLitsNew[k++] = piLitsNew[pOrder[i]];
+ piLitsRes[k++] = piLits[pOrder[i]];
}
+ assert( k == nVars );
}
/**Function*************************************************************
@@ -713,76 +750,52 @@ int Kit_DsdShrink_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit, int pPri
Kit_DsdObj_t * pObj, * pObjNew;
unsigned * pTruth, * pTruthNew;
unsigned i, piLitsNew[16], uSupps[16];
- int fCompl, iLitFanin, iLitNew;
-
- // remember the complement
- fCompl = Kit_DsdLitIsCompl(iLit);
- iLit = Kit_DsdLitRegular(iLit);
- assert( !Kit_DsdLitIsCompl(iLit) );
+ int iLitFanin, iLitNew;
// consider the case of simple gate
pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
if ( pObj == NULL )
- return Kit_DsdLitNotCond( iLit, fCompl );
+ return iLit;
if ( pObj->Type == KIT_DSD_AND )
{
- if ( pObj->nFans == 2 )
+ // get the supports
+ Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
+ uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
+ // put the largest component last
+ // sort other components in the decreasing order of priority of their vars
+ Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew );
+ // construct the two-input node network
+ iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
+ for ( i = 1; i < pObj->nFans; i++ )
{
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 );
- pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[0], pPrios );
- pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[1], pPrios );
- }
- else
- {
- // get the supports
- Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
- {
- piLitsNew[i] = iLitFanin;
- uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
- }
- // put the largest component first
- // sort other components in the increasing order of the highest variable
- Kit_DsdCompSort( pPrios, uSupps, piLitsNew, pObj->nFans );
- iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
- for ( i = 1; i < pObj->nFans; i++ )
- {
- pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 );
- pObjNew->pFans[0] = iLitNew;
- pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
- iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
- }
+ pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
+ pObjNew->pFans[1] = iLitNew;
+ iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
- return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
+ return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) );
}
if ( pObj->Type == KIT_DSD_XOR )
{
- if ( pObj->nFans == 2 )
+ // get the supports
+ Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
{
- pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
- pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[0], pPrios );
- pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[1], pPrios );
+ assert( !Kit_DsdLitIsCompl(iLitFanin) );
+ uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
}
- else
+ // put the largest component last
+ // sort other components in the decreasing order of priority of their vars
+ Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew );
+ // construct the two-input node network
+ iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
+ for ( i = 1; i < pObj->nFans; i++ )
{
- // get the supports
- Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
- {
- piLitsNew[i] = iLitFanin;
- uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
- }
- // put the largest component first
- // sort other components in the increasing order of the highest variable
- Kit_DsdCompSort( pPrios, uSupps, piLitsNew, pObj->nFans );
- iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
- for ( i = 1; i < pObj->nFans; i++ )
- {
- pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
- pObjNew->pFans[0] = iLitNew;
- pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
- iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
- }
+ pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
+ pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
+ pObjNew->pFans[1] = iLitNew;
+ iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
- return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
+ return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) );
}
assert( pObj->Type == KIT_DSD_PRIME );
@@ -804,7 +817,7 @@ int Kit_DsdShrink_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit, int pPri
}
}
// if the incoming phase is complemented, absorb it into the prime node
- if ( fCompl )
+ if ( Kit_DsdLitIsCompl(iLit) )
Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
return Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
@@ -877,22 +890,26 @@ void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
Weights[k] = 0;
for ( v = 0; v < 16; v++ )
if ( uSuppFanin & (1 << v) )
- Weights[k] += pFreqs[v];
+ Weights[k] += pFreqs[v] - 1;
}
// find the most frequent fanin
- WeightMax = FaninMax = 0;
+ WeightMax = 0;
+ FaninMax = -1;
for ( k = 0; k < pObj->nFans; k++ )
if ( WeightMax < Weights[k] )
{
WeightMax = Weights[k];
FaninMax = k;
}
- assert( k < pObj->nFans );
+ // no need to reorder if there are no frequent fanins
+ if ( FaninMax == -1 )
+ continue;
// move the fanins number k to the first place
nSwaps = 0;
pIn = Kit_DsdObjTruth(pObj);
- pOut = p->pSupps;
- for ( v = k-1; v >= 0; v-- )
+ pOut = p->pMem;
+// for ( v = FaninMax; v < ((int)pObj->nFans)-1; v++ )
+ for ( v = FaninMax-1; v >= 0; v-- )
{
// swap the fanins
Temp = pObj->pFans[v];
@@ -903,8 +920,8 @@ void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
pTemp = pIn; pIn = pOut; pOut = pTemp;
nSwaps++;
}
- if ( nSwaps & 1)
- Kit_TruthCopy( pIn, pOut, pObj->nFans );
+ if ( nSwaps & 1 )
+ Kit_TruthCopy( pOut, pIn, pObj->nFans );
}
}
@@ -919,19 +936,53 @@ void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
SeeAlso []
***********************************************************************/
-void Kit_DsdGetSupports( Kit_DsdNtk_t * p )
+unsigned Kit_DsdGetSupports_rec( Kit_DsdNtk_t * p, int iLit )
{
Kit_DsdObj_t * pObj;
unsigned uSupport, k;
- int iFaninLit, i;
+ int iFaninLit;
+ pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
+ if ( pObj == NULL )
+ return Kit_DsdLitSupport( p, iLit );
+ uSupport = 0;
+ Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
+ uSupport |= Kit_DsdGetSupports_rec( p, iFaninLit );
+ p->pSupps[pObj->Id - p->nVars] = uSupport;
+ assert( uSupport <= 0xFFFF );
+ return uSupport;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compute the support.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdGetSupports( Kit_DsdNtk_t * p )
+{
+ Kit_DsdObj_t * pRoot;
+ assert( p->pSupps == NULL );
p->pSupps = ALLOC( unsigned, p->nNodes );
- Kit_DsdNtkForEachObj( p, pObj, i )
+ // consider simple special cases
+ pRoot = Kit_DsdNtkRoot(p);
+ if ( pRoot->Type == KIT_DSD_CONST1 )
{
- uSupport = 0;
- Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
- uSupport |= Kit_DsdLitSupport( p, iFaninLit );
- p->pSupps[pObj->Id - p->nVars] = uSupport;
- }
+ assert( p->nNodes == 1 );
+ p->pSupps[0] = 0;
+ }
+ if ( pRoot->Type == KIT_DSD_VAR )
+ {
+ assert( p->nNodes == 1 );
+ p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] );
+ }
+ else
+ Kit_DsdGetSupports_rec( p, p->Root );
+ assert( p->pSupps[0] <= 0xFFFF );
}
/**Function*************************************************************
@@ -1772,6 +1823,251 @@ int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit
return nStep;
}
+/**Function*************************************************************
+
+ Synopsis [Canonical decomposition into completely DSD-structure.]
+
+ Description [Returns the number of cofactoring steps. Also returns
+ the cofactoring variables in pVars.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose )
+{
+ Kit_DsdNtk_t * ppNtks[32] = {0}, * pTemp;
+ unsigned * ppCofs[5][16];
+ int piCofVar[5];
+ int nPrimeSizeMax, nPrimeSizeCur, nSuppSizeMax;
+ int i, k, v1, v2, v3, v4, s, nSteps, nSize, nMemSize;
+ assert( nCofLevel < 5 );
+
+ // print the function
+ ppNtks[0] = Kit_DsdDecompose( pTruth, nVars );
+ ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
+ Kit_DsdNtkFree( pTemp );
+ if ( fVerbose )
+ Kit_DsdPrint( stdout, ppNtks[0] );
+ Kit_DsdNtkFree( ppNtks[0] );
+
+ // allocate storage for cofactors
+ nMemSize = Kit_TruthWordNum(nVars);
+ ppCofs[0][0] = ALLOC( unsigned, 80 * nMemSize );
+ nSize = 0;
+ for ( i = 0; i < 5; i++ )
+ for ( k = 0; k < 16; k++ )
+ ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
+ assert( nSize == 80 );
+
+ // copy the function
+ Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
+
+ if ( nCofLevel == 1 )
+ for ( v1 = 0; v1 < nVars; v1++ )
+ {
+ nSteps = 0;
+ piCofVar[nSteps++] = v1;
+
+ printf( " Variables { " );
+ for ( i = 0; i < nSteps; i++ )
+ printf( "%c ", 'a' + piCofVar[i] );
+ printf( "}\n" );
+
+ // single cofactors
+ for ( s = 1; s <= nSteps; s++ )
+ {
+ for ( k = 0; k < s; k++ )
+ {
+ nSize = (1 << k);
+ for ( i = 0; i < nSize; i++ )
+ {
+ Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
+ Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
+ }
+ }
+ }
+ // compute DSD networks
+ nSize = (1 << nSteps);
+ nPrimeSizeMax = 0;
+ nSuppSizeMax = 0;
+ for ( i = 0; i < nSize; i++ )
+ {
+ ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
+ ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
+ Kit_DsdNtkFree( pTemp );
+ if ( fVerbose )
+ {
+ printf( "Cof%d%d: ", nSteps, i );
+ Kit_DsdPrint( stdout, ppNtks[i] );
+ }
+ // compute the largest non-decomp block
+ nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
+ nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
+ Kit_DsdNtkFree( ppNtks[i] );
+ nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
+ }
+ printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
+ }
+
+ if ( nCofLevel == 2 )
+ for ( v1 = 0; v1 < nVars; v1++ )
+ for ( v2 = v1+1; v2 < nVars; v2++ )
+ {
+ nSteps = 0;
+ piCofVar[nSteps++] = v1;
+ piCofVar[nSteps++] = v2;
+
+ printf( " Variables { " );
+ for ( i = 0; i < nSteps; i++ )
+ printf( "%c ", 'a' + piCofVar[i] );
+ printf( "}\n" );
+
+ // single cofactors
+ for ( s = 1; s <= nSteps; s++ )
+ {
+ for ( k = 0; k < s; k++ )
+ {
+ nSize = (1 << k);
+ for ( i = 0; i < nSize; i++ )
+ {
+ Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
+ Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
+ }
+ }
+ }
+ // compute DSD networks
+ nSize = (1 << nSteps);
+ nPrimeSizeMax = 0;
+ nSuppSizeMax = 0;
+ for ( i = 0; i < nSize; i++ )
+ {
+ ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
+ ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
+ Kit_DsdNtkFree( pTemp );
+ if ( fVerbose )
+ {
+ printf( "Cof%d%d: ", nSteps, i );
+ Kit_DsdPrint( stdout, ppNtks[i] );
+ }
+ // compute the largest non-decomp block
+ nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
+ nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
+ Kit_DsdNtkFree( ppNtks[i] );
+ nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
+ }
+ printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
+ }
+
+ if ( nCofLevel == 3 )
+ for ( v1 = 0; v1 < nVars; v1++ )
+ for ( v2 = v1+1; v2 < nVars; v2++ )
+ for ( v3 = v2+1; v3 < nVars; v3++ )
+ {
+ nSteps = 0;
+ piCofVar[nSteps++] = v1;
+ piCofVar[nSteps++] = v2;
+ piCofVar[nSteps++] = v3;
+
+ printf( " Variables { " );
+ for ( i = 0; i < nSteps; i++ )
+ printf( "%c ", 'a' + piCofVar[i] );
+ printf( "}\n" );
+
+ // single cofactors
+ for ( s = 1; s <= nSteps; s++ )
+ {
+ for ( k = 0; k < s; k++ )
+ {
+ nSize = (1 << k);
+ for ( i = 0; i < nSize; i++ )
+ {
+ Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
+ Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
+ }
+ }
+ }
+ // compute DSD networks
+ nSize = (1 << nSteps);
+ nPrimeSizeMax = 0;
+ nSuppSizeMax = 0;
+ for ( i = 0; i < nSize; i++ )
+ {
+ ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
+ ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
+ Kit_DsdNtkFree( pTemp );
+ if ( fVerbose )
+ {
+ printf( "Cof%d%d: ", nSteps, i );
+ Kit_DsdPrint( stdout, ppNtks[i] );
+ }
+ // compute the largest non-decomp block
+ nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
+ nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
+ Kit_DsdNtkFree( ppNtks[i] );
+ nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
+ }
+ printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
+ }
+
+ if ( nCofLevel == 4 )
+ for ( v1 = 0; v1 < nVars; v1++ )
+ for ( v2 = v1+1; v2 < nVars; v2++ )
+ for ( v3 = v2+1; v3 < nVars; v3++ )
+ for ( v4 = v3+1; v4 < nVars; v4++ )
+ {
+ nSteps = 0;
+ piCofVar[nSteps++] = v1;
+ piCofVar[nSteps++] = v2;
+ piCofVar[nSteps++] = v3;
+ piCofVar[nSteps++] = v4;
+
+ printf( " Variables { " );
+ for ( i = 0; i < nSteps; i++ )
+ printf( "%c ", 'a' + piCofVar[i] );
+ printf( "}\n" );
+
+ // single cofactors
+ for ( s = 1; s <= nSteps; s++ )
+ {
+ for ( k = 0; k < s; k++ )
+ {
+ nSize = (1 << k);
+ for ( i = 0; i < nSize; i++ )
+ {
+ Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
+ Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
+ }
+ }
+ }
+ // compute DSD networks
+ nSize = (1 << nSteps);
+ nPrimeSizeMax = 0;
+ nSuppSizeMax = 0;
+ for ( i = 0; i < nSize; i++ )
+ {
+ ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
+ ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
+ Kit_DsdNtkFree( pTemp );
+ if ( fVerbose )
+ {
+ printf( "Cof%d%d: ", nSteps, i );
+ Kit_DsdPrint( stdout, ppNtks[i] );
+ }
+ // compute the largest non-decomp block
+ nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
+ nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
+ Kit_DsdNtkFree( ppNtks[i] );
+ nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
+ }
+ printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
+ }
+
+
+ free( ppCofs[0][0] );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/lpk/lpk.h b/src/opt/lpk/lpk.h
new file mode 100644
index 00000000..092b43e1
--- /dev/null
+++ b/src/opt/lpk/lpk.h
@@ -0,0 +1,82 @@
+/**CFile****************************************************************
+
+ FileName [lpk.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Fast Boolean matching for LUT structures.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: lpk.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __LPK_H__
+#define __LPK_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Lpk_Par_t_ Lpk_Par_t;
+struct Lpk_Par_t_
+{
+ // user-controlled parameters
+ int nLutsMax; // (N) the maximum number of LUTs in the structure
+ int nLutsOver; // (Q) the maximum number of LUTs not in the MFFC
+ int nVarsShared; // (S) the maximum number of shared variables (crossbars)
+ int nGrowthLevel; // (L) the maximum increase in the node level after resynthesis
+ int fSatur; // iterate till saturation
+ int fZeroCost; // accept zero-cost replacements
+ int fVerbose; // the verbosiness flag
+ int fVeryVerbose; // additional verbose info printout
+ // internal parameters
+ int nLutSize; // (K) the LUT size (determined by the input network)
+ int nVarsMax; // (V) the largest number of variables: V = N * (K-1) + 1
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// ITERATORS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== lpkCore.c ========================================================*/
+extern int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
new file mode 100644
index 00000000..cbd971e3
--- /dev/null
+++ b/src/opt/lpk/lpkCore.c
@@ -0,0 +1,280 @@
+/**CFile****************************************************************
+
+ FileName [lpkCore.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: lpkCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if at least one entry has changed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pTemp;
+ int i;
+ vNodes = Vec_VecEntry( p->vVisited, iNode );
+ if ( Vec_PtrSize(vNodes) == 0 )
+ return 1;
+ Vec_PtrForEachEntry( vNodes, pTemp, i )
+ {
+ // check if the node has changed
+ pTemp = Abc_NtkObj( p->pNtk, (int)pTemp );
+ if ( pTemp == NULL )
+ return 1;
+ // check if the number of fanouts has changed
+// if ( Abc_ObjFanoutNum(pTemp) != (int)Vec_PtrEntry(vNodes, i+1) )
+// return 1;
+ i++;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs resynthesis for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Lpk_ResynthesizeNode( Lpk_Man_t * p )
+{
+ Kit_DsdNtk_t * pDsdNtk;
+ Lpk_Cut_t * pCut;
+ unsigned * pTruth;
+ void * pDsd = NULL;
+ int i, RetValue, clk;
+
+ Lpk_Cut_t * pCutMax;
+
+ // compute the cuts
+clk = clock();
+ if ( !Lpk_NodeCuts( p ) )
+ {
+p->timeCuts += clock() - clk;
+ return 0;
+ }
+p->timeCuts += clock() - clk;
+
+ // find the max volume cut
+ pCutMax = NULL;
+ for ( i = 0; i < p->nEvals; i++ )
+ {
+ pCut = p->pCuts + p->pEvals[i];
+ if ( pCutMax == NULL || pCutMax->nNodes < pCut->nNodes )
+ pCutMax = pCut;
+ }
+ assert( pCutMax != NULL );
+
+
+ if ( p->pPars->fVeryVerbose )
+ printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
+ // try the good cuts
+ p->nCutsTotal += p->nCuts;
+ p->nCutsUseful += p->nEvals;
+ for ( i = 0; i < p->nEvals; i++ )
+ {
+ // get the cut
+ pCut = p->pCuts + p->pEvals[i];
+
+ if ( pCut != pCutMax )
+ continue;
+
+ // compute the truth table
+clk = clock();
+ pTruth = Lpk_CutTruth( p, pCut );
+p->timeTruth += clock() - clk;
+
+clk = clock();
+ pDsdNtk = Kit_DsdDeriveNtk( pTruth, pCut->nLeaves, p->pPars->nLutSize );
+p->timeEval += clock() - clk;
+
+ if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) // skip 16-input non-DSD because ISOP will not work
+ {
+ Kit_DsdNtkFree( pDsdNtk );
+ continue;
+ }
+
+ if ( p->pPars->fVeryVerbose )
+ {
+ printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ",
+ i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
+ Kit_DsdPrint( stdout, pDsdNtk );
+ }
+
+ // update the network
+clk = clock();
+ RetValue = Lpk_CutExplore( p, pCut, pDsdNtk );
+ Kit_DsdNtkFree( pDsdNtk );
+p->timeMap += clock() - clk;
+ if ( RetValue )
+ break;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs resynthesis for one network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
+{
+ ProgressBar * pProgress;
+ Lpk_Man_t * p;
+ Abc_Obj_t * pObj;
+ double Delta;
+ int i, Iter, nNodes, nNodesPrev, clk = clock();
+ assert( Abc_NtkIsLogic(pNtk) );
+
+ // get the number of inputs
+ pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
+ // adjust the number of crossbars based on LUT size
+ if ( pPars->nVarsShared > pPars->nLutSize - 2 )
+ pPars->nVarsShared = pPars->nLutSize - 2;
+ // get the max number of LUTs tried
+ pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1; // V = N * (K-1) + 1
+ while ( pPars->nVarsMax > 16 )
+ {
+ pPars->nLutsMax--;
+ pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1;
+
+ }
+ if ( pPars->fVerbose )
+ {
+ printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n",
+ pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax );
+ }
+
+ // convert logic to AIGs
+ Abc_NtkToAig( pNtk );
+
+ // start the manager
+ p = Lpk_ManStart( pPars );
+ p->pNtk = pNtk;
+ p->nNodesTotal = Abc_NtkNodeNum(pNtk);
+ p->vLevels = Vec_VecStart( 3 * Abc_NtkLevel(pNtk) ); // computes levels of all nodes
+ if ( p->pPars->fSatur )
+ p->vVisited = Vec_VecStart( 0 );
+
+ // iterate over the network
+ nNodesPrev = p->nNodesTotal;
+ for ( Iter = 1; ; Iter++ )
+ {
+ // expand storage for changed nodes
+ if ( p->pPars->fSatur )
+ Vec_VecExpand( p->vVisited, Abc_NtkObjNumMax(pNtk) + 1 );
+
+ // consider all nodes
+ nNodes = Abc_NtkObjNumMax(pNtk);
+ if ( !pPars->fVeryVerbose )
+ pProgress = Extra_ProgressBarStart( stdout, nNodes );
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ {
+ // skip all except the final node
+// if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
+// continue;
+
+ if ( i >= nNodes )
+ break;
+ if ( !pPars->fVeryVerbose )
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ // skip the nodes that did not change
+ if ( p->pPars->fSatur && !Lpk_NodeHasChanged(p, pObj->Id) )
+ continue;
+ // resynthesize
+ p->pObj = pObj;
+ Lpk_ResynthesizeNode( p );
+
+ if ( p->nChanges == 3 )
+ break;
+ }
+ if ( !pPars->fVeryVerbose )
+ Extra_ProgressBarStop( pProgress );
+
+ // check the increase
+ Delta = 100.00 * (nNodesPrev - Abc_NtkNodeNum(pNtk)) / p->nNodesTotal;
+ if ( Delta < 0.05 )
+ break;
+ nNodesPrev = Abc_NtkNodeNum(pNtk);
+ if ( !p->pPars->fSatur )
+ break;
+
+ break;
+ }
+
+ if ( pPars->fVerbose )
+ {
+ printf( "N = %5d (%3d) Cut = %5d (%4d) Change = %5d Gain = %5d (%5.2f %%) Iter = %2d\n",
+ p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal, Iter );
+ printf( "Non_DSD blocks: " );
+ for ( i = 3; i <= pPars->nVarsMax; i++ )
+ if ( p->nBlocks[i] )
+ printf( "%d=%d ", i, p->nBlocks[i] );
+ printf( "\n" );
+ p->timeTotal = clock() - clk;
+ p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
+ PRTP( "Cuts ", p->timeCuts, p->timeTotal );
+ PRTP( "Truth ", p->timeTruth, p->timeTotal );
+ PRTP( "Eval ", p->timeEval, p->timeTotal );
+ PRTP( "Map ", p->timeMap, p->timeTotal );
+ PRTP( "Other ", p->timeOther, p->timeTotal );
+ PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
+ }
+
+ Lpk_ManStop( p );
+ // check the resulting network
+ if ( !Abc_NtkCheck( pNtk ) )
+ {
+ printf( "Lpk_Resynthesize: The network check has failed.\n" );
+ return 0;
+ }
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
new file mode 100644
index 00000000..251ec829
--- /dev/null
+++ b/src/opt/lpk/lpkCut.c
@@ -0,0 +1,584 @@
+/**CFile****************************************************************
+
+ FileName [lpkCut.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: lpkCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Computes the truth able of one cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * iCount )
+{
+ unsigned * pTruth, * pTruth0, * pTruth1;
+ assert( !Hop_IsComplement(pObj) );
+ if ( pObj->pData )
+ {
+ assert( ((unsigned)pObj->pData) & 0xffff0000 );
+ return pObj->pData;
+ }
+ // get the plan for a new truth table
+ pTruth = Vec_PtrEntry( vTtNodes, (*iCount)++ );
+ if ( Hop_ObjIsConst1(pObj) )
+ Extra_TruthFill( pTruth, nVars );
+ else
+ {
+ assert( Hop_ObjIsAnd(pObj) );
+ // compute the truth tables of the fanins
+ pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, iCount );
+ pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, iCount );
+ // creat the truth table of the node
+ Extra_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) );
+ }
+ pObj->pData = pTruth;
+ return pTruth;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the truth able of one cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut )
+{
+ Hop_Man_t * pManHop = p->pNtk->pManFunc;
+ Hop_Obj_t * pObjHop;
+ Abc_Obj_t * pObj, * pFanin;
+ unsigned * pTruth;
+ int i, k, iCount = 0;
+// Lpk_NodePrintCut( p, pCut );
+
+ // initialize the leaves
+ Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
+ pObj->pCopy = Vec_PtrEntry( p->vTtElems, i );
+
+ // construct truth table in the topological order
+ Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
+ {
+ // get the local AIG
+ pObjHop = Hop_Regular(pObj->pData);
+ // clean the data field of the nodes in the AIG subgraph
+ Hop_ObjCleanData_rec( pObjHop );
+ // set the initial truth tables at the fanins
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ {
+ assert( ((unsigned)pFanin->pCopy) & 0xffff0000 );
+ Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
+ }
+ // compute the truth table of internal nodes
+ pTruth = Lpk_CutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount );
+ if ( Hop_IsComplement(pObj->pData) )
+ Extra_TruthNot( pTruth, pTruth, pCut->nLeaves );
+ // set the truth table at the node
+ pObj->pCopy = (Abc_Obj_t *)pTruth;
+ }
+
+ return pTruth;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if at least one entry has changed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_NodeRecordImpact( Lpk_Man_t * p )
+{
+ Lpk_Cut_t * pCut;
+ Vec_Ptr_t * vNodes = Vec_VecEntry( p->vVisited, p->pObj->Id );
+ Abc_Obj_t * pNode;
+ int i, k;
+ // collect the nodes that impact the given node
+ Vec_PtrClear( vNodes );
+ for ( i = 0; i < p->nCuts; i++ )
+ {
+ pCut = p->pCuts + i;
+ for ( k = 0; k < (int)pCut->nLeaves; k++ )
+ {
+ pNode = Abc_NtkObj( p->pNtk, pCut->pLeaves[k] );
+ if ( pNode->fMarkC )
+ continue;
+ pNode->fMarkC = 1;
+ Vec_PtrPush( vNodes, (void *)pNode->Id );
+ Vec_PtrPush( vNodes, (void *)Abc_ObjFanoutNum(pNode) );
+ }
+ }
+ // clear the marks
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ pNode = Abc_NtkObj( p->pNtk, (int)pNode );
+ pNode->fMarkC = 0;
+ i++;
+ }
+//printf( "%d ", Vec_PtrSize(vNodes) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the cut has structural DSD.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Lpk_NodeCutsCheckDsd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
+{
+ Abc_Obj_t * pObj, * pFanin;
+ int i, k, nCands, fLeavesOnly, RetValue;
+ assert( pCut->nLeaves > 0 );
+ // clear ref counters
+ memset( p->pRefs, 0, sizeof(int) * pCut->nLeaves );
+ // mark cut leaves
+ Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
+ {
+ assert( pObj->fMarkA == 0 );
+ pObj->fMarkA = 1;
+ pObj->pCopy = (void *)i;
+ }
+ // ref leaves pointed from the internal nodes
+ nCands = 0;
+ Lpk_CutForEachNode( p->pNtk, pCut, pObj, i )
+ {
+ fLeavesOnly = 1;
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ if ( pFanin->fMarkA )
+ p->pRefs[(int)pFanin->pCopy]++;
+ else
+ fLeavesOnly = 0;
+ if ( fLeavesOnly )
+ p->pCands[nCands++] = pObj->Id;
+ }
+ // look at the nodes that only point to the leaves
+ RetValue = 0;
+ for ( i = 0; i < nCands; i++ )
+ {
+ pObj = Abc_NtkObj( p->pNtk, p->pCands[i] );
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ {
+ assert( pFanin->fMarkA == 1 );
+ if ( p->pRefs[(int)pFanin->pCopy] > 1 )
+ break;
+ }
+ if ( k == Abc_ObjFaninNum(pObj) )
+ {
+ RetValue = 1;
+ break;
+ }
+ }
+ // unmark cut leaves
+ Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
+ pObj->fMarkA = 0;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if pDom is contained in pCut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Lpk_NodeCutsOneDominance( Lpk_Cut_t * pDom, Lpk_Cut_t * pCut )
+{
+ int i, k;
+ for ( i = 0; i < (int)pDom->nLeaves; i++ )
+ {
+ for ( k = 0; k < (int)pCut->nLeaves; k++ )
+ if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
+ break;
+ if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
+ return 0;
+ }
+ // every node in pDom is contained in pCut
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check if the cut exists.]
+
+ Description [Returns 1 if the cut exists.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Lpk_NodeCutsOneFilter( Lpk_Cut_t * pCuts, int nCuts, Lpk_Cut_t * pCutNew )
+{
+ Lpk_Cut_t * pCut;
+ int i, k;
+ assert( pCutNew->uSign[0] || pCutNew->uSign[1] );
+ // try to find the cut
+ for ( i = 0; i < nCuts; i++ )
+ {
+ pCut = pCuts + i;
+ if ( pCut->nLeaves == 0 )
+ continue;
+ if ( pCut->nLeaves == pCutNew->nLeaves )
+ {
+ if ( pCut->uSign[0] == pCutNew->uSign[0] && pCut->uSign[1] == pCutNew->uSign[1] )
+ {
+ for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
+ if ( pCut->pLeaves[k] != pCutNew->pLeaves[k] )
+ break;
+ if ( k == (int)pCutNew->nLeaves )
+ return 1;
+ }
+ continue;
+ }
+ if ( pCut->nLeaves < pCutNew->nLeaves )
+ {
+ // skip the non-contained cuts
+ if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCut->uSign[0] )
+ continue;
+ if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCut->uSign[1] )
+ continue;
+ // check containment seriously
+ if ( Lpk_NodeCutsOneDominance( pCut, pCutNew ) )
+ return 1;
+ continue;
+ }
+ // check potential containment of other cut
+
+ // skip the non-contained cuts
+ if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCutNew->uSign[0] )
+ continue;
+ if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCutNew->uSign[1] )
+ continue;
+ // check containment seriously
+ if ( Lpk_NodeCutsOneDominance( pCutNew, pCut ) )
+ pCut->nLeaves = 0; // removed
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the given cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_NodePrintCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fLeavesOnly )
+{
+ Abc_Obj_t * pObj;
+ int i;
+ if ( !fLeavesOnly )
+ printf( "LEAVES:\n" );
+ Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
+ printf( "%d,", pObj->Id );
+ if ( !fLeavesOnly )
+ {
+ printf( "\nNODES:\n" );
+ Lpk_CutForEachNode( p->pNtk, pCut, pObj, i )
+ {
+ printf( "%d,", pObj->Id );
+ assert( Abc_ObjIsNode(pObj) );
+ }
+ printf( "\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Set the cut signature.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_NodeCutSignature( Lpk_Cut_t * pCut )
+{
+ unsigned i;
+ pCut->uSign[0] = pCut->uSign[1] = 0;
+ for ( i = 0; i < pCut->nLeaves; i++ )
+ {
+ pCut->uSign[(pCut->pLeaves[i] & 32) > 0] |= (1 << (pCut->pLeaves[i] & 31));
+ if ( i != pCut->nLeaves - 1 )
+ assert( pCut->pLeaves[i] < pCut->pLeaves[i+1] );
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes the set of all cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node )
+{
+ Lpk_Cut_t * pCutNew;
+ Abc_Obj_t * pObj, * pFanin;
+ int i, k, j, nLeavesNew;
+/*
+ printf( "Exploring cut " );
+ Lpk_NodePrintCut( p, pCut, 1 );
+ printf( "with node %d\n", Node );
+*/
+ // check if the cut can stand adding one more internal node
+ if ( pCut->nNodes == LPK_SIZE_MAX )
+ return;
+
+ // if the node is a PI, quit
+ pObj = Abc_NtkObj( p->pNtk, Node );
+ if ( Abc_ObjIsCi(pObj) )
+ return;
+ assert( Abc_ObjIsNode(pObj) );
+ assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize );
+
+ // if the node is not in the MFFC, check the limit
+ if ( !Abc_NodeIsTravIdCurrent(pObj) )
+ {
+ if ( (int)pCut->nNodesDup == p->pPars->nLutsOver )
+ return;
+ assert( (int)pCut->nNodesDup < p->pPars->nLutsOver );
+ }
+
+ // check the possibility of adding this node using the signature
+ nLeavesNew = pCut->nLeaves - 1;
+ Abc_ObjForEachFanin( pObj, pFanin, i )
+ {
+ if ( (pCut->uSign[(pFanin->Id & 32) > 0] & (1 << (pFanin->Id & 31))) )
+ continue;
+ if ( ++nLeavesNew > p->pPars->nVarsMax )
+ return;
+ }
+
+ // initialize the set of leaves to the nodes in the cut
+ assert( p->nCuts < LPK_CUTS_MAX );
+ pCutNew = p->pCuts + p->nCuts;
+/*
+if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1] == 34 && pCut->pNodes[2] == 35 )//p->nCuts == 48 )
+{
+ int x = 0;
+ printf( "Start:\n" );
+ Lpk_NodePrintCut( p, pCut );
+}
+*/
+ pCutNew->nLeaves = 0;
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ if ( pCut->pLeaves[i] != Node )
+ pCutNew->pLeaves[pCutNew->nLeaves++] = pCut->pLeaves[i];
+
+ // add new nodes
+ Abc_ObjForEachFanin( pObj, pFanin, i )
+ {
+ // find the place where this node belongs
+ for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
+ if ( pCutNew->pLeaves[k] >= pFanin->Id )
+ break;
+ if ( k < (int)pCutNew->nLeaves && pCutNew->pLeaves[k] == pFanin->Id )
+ continue;
+ // check if there is room
+ if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax )
+ return;
+ // move all the nodes
+ for ( j = pCutNew->nLeaves; j > k; j-- )
+ pCutNew->pLeaves[j] = pCutNew->pLeaves[j-1];
+ pCutNew->pLeaves[k] = pFanin->Id;
+ pCutNew->nLeaves++;
+ assert( pCutNew->nLeaves <= LPK_SIZE_MAX );
+
+ }
+/*
+ printf( " Trying cut: " );
+ Lpk_NodePrintCut( p, pCutNew, 1 );
+ printf( "\n" );
+*/
+ // skip the contained cuts
+ Lpk_NodeCutSignature( pCutNew );
+ if ( Lpk_NodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) )
+ return;
+
+
+ // update the set of internal nodes
+ assert( pCut->nNodes < LPK_SIZE_MAX );
+ memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) );
+ pCutNew->nNodes = pCut->nNodes;
+ pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
+
+ // add the marked node
+ pCutNew->nNodesDup = pCut->nNodesDup + !Abc_NodeIsTravIdCurrent(pObj);
+/*
+if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
+{
+ int x = 0;
+ printf( "Finish:\n" );
+ Lpk_NodePrintCut( p, pCutNew );
+}
+*/
+ // add the cut to storage
+ assert( p->nCuts < LPK_CUTS_MAX );
+ p->nCuts++;
+
+ assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup );
+/*
+ printf( " Creating cut: " );
+ Lpk_NodePrintCut( p, pCutNew, 1 );
+ printf( "\n" );
+*/
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the set of all cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Lpk_NodeCuts( Lpk_Man_t * p )
+{
+ Lpk_Cut_t * pCut, * pCut2;
+ int i, k, Temp, nMffc, fChanges;
+
+ // mark the MFFC of the node with the current trav ID
+ nMffc = p->nMffc = Abc_NodeMffcLabel( p->pObj );
+ assert( nMffc > 0 );
+ if ( nMffc == 1 )
+ return 0;
+
+ // initialize the first cut
+ pCut = p->pCuts; p->nCuts = 1;
+ pCut->nNodes = 0;
+ pCut->nNodesDup = 0;
+ pCut->nLeaves = 1;
+ pCut->pLeaves[0] = p->pObj->Id;
+ // assign the signature
+ Lpk_NodeCutSignature( pCut );
+
+ // perform the cut computation
+ for ( i = 0; i < p->nCuts; i++ )
+ {
+ pCut = p->pCuts + i;
+ if ( pCut->nLeaves == 0 )
+ continue;
+ // try to expand the fanins of this cut
+ for ( k = 0; k < (int)pCut->nLeaves; k++ )
+ {
+ // create a new cut
+ Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] );
+ // quit if the number of cuts has exceeded the limit
+ if ( p->nCuts == LPK_CUTS_MAX )
+ break;
+ }
+ if ( p->nCuts == LPK_CUTS_MAX )
+ break;
+ }
+ if ( p->nCuts == LPK_CUTS_MAX )
+ p->nNodesOver++;
+
+ // record the impact of this node
+ if ( p->pPars->fSatur )
+ Lpk_NodeRecordImpact( p );
+
+ // compress the cuts by removing empty ones, those with negative Weight, and decomposable ones
+ p->nEvals = 0;
+ for ( i = 0; i < p->nCuts; i++ )
+ {
+ pCut = p->pCuts + i;
+ if ( pCut->nLeaves < 2 )
+ continue;
+ // compute the number of LUTs neede to implement this cut
+ // V = N * (K-1) + 1 ~~~~~ N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
+ pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 );
+ pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
+ if ( pCut->Weight <= 1.0 )
+ continue;
+ pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut );
+ if ( pCut->fHasDsd )
+ continue;
+ p->pEvals[p->nEvals++] = i;
+ }
+ if ( p->nEvals == 0 )
+ return 0;
+
+ // sort the cuts by Weight
+ do {
+ fChanges = 0;
+ for ( i = 0; i < p->nEvals - 1; i++ )
+ {
+ pCut = p->pCuts + p->pEvals[i];
+ pCut2 = p->pCuts + p->pEvals[i+1];
+ if ( pCut->Weight >= pCut2->Weight )
+ continue;
+ Temp = p->pEvals[i];
+ p->pEvals[i] = p->pEvals[i+1];
+ p->pEvals[i+1] = Temp;
+ fChanges = 1;
+ }
+ } while ( fChanges );
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
new file mode 100644
index 00000000..fe442302
--- /dev/null
+++ b/src/opt/lpk/lpkInt.h
@@ -0,0 +1,161 @@
+/**CFile****************************************************************
+
+ FileName [lpkInt.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Fast Boolean matching for LUT structures.]
+
+ Synopsis [Internal declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: lpkInt.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __LPK_INT_H__
+#define __LPK_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "abc.h"
+#include "kit.h"
+#include "if.h"
+#include "lpk.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+#define LPK_SIZE_MAX 24 // the largest size of the function
+#define LPK_CUTS_MAX 512 // the largest number of cuts considered
+
+typedef struct Lpk_Man_t_ Lpk_Man_t;
+typedef struct Lpk_Cut_t_ Lpk_Cut_t;
+
+struct Lpk_Cut_t_
+{
+ unsigned nLeaves : 6; // (L) the number of leaves
+ unsigned nNodes : 6; // (M) the number of nodes
+ unsigned nNodesDup : 6; // (Q) nodes outside of MFFC
+ unsigned nLuts : 6; // (N) the number of LUTs to try
+ unsigned unused : 6; // unused
+ unsigned fHasDsd : 1; // set to 1 if the cut has structural DSD (and so cannot be used)
+ unsigned fMark : 1; // multipurpose mark
+ unsigned uSign[2]; // the signature
+ float Weight; // the weight of the cut: (M - Q)/N(V) (the larger the better)
+ int Gain; // the gain achieved using this cut
+ int pLeaves[LPK_SIZE_MAX]; // the leaves of the cut
+ int pNodes[LPK_SIZE_MAX]; // the nodes of the cut
+};
+
+struct Lpk_Man_t_
+{
+ // parameters
+ Lpk_Par_t * pPars; // the set of parameters
+ // current representation
+ Abc_Ntk_t * pNtk; // the network
+ Abc_Obj_t * pObj; // the node to resynthesize
+ // cut representation
+ int nMffc; // the size of MFFC of the node
+ int nCuts; // the total number of cuts
+ int nCutsMax; // the largest possible number of cuts
+ int nEvals; // the number of good cuts
+ Lpk_Cut_t pCuts[LPK_CUTS_MAX]; // the storage for cuts
+ int pEvals[LPK_CUTS_MAX]; // the good cuts
+ // visited nodes
+ Vec_Vec_t * vVisited;
+ // mapping manager
+ If_Man_t * pIfMan;
+ Vec_Int_t * vCover;
+ Vec_Vec_t * vLevels;
+ // temporary variables
+ int fCofactoring; // working in the cofactoring mode
+ int fCalledOnce; // limits the depth of MUX cofactoring
+ int pRefs[LPK_SIZE_MAX]; // fanin reference counters
+ int pCands[LPK_SIZE_MAX]; // internal nodes pointing only to the leaves
+ // truth table representation
+ Vec_Ptr_t * vTtElems; // elementary truth tables
+ Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes
+ // variable sets
+ Vec_Int_t * vSets[8];
+ // statistics
+ int nNodesTotal; // total number of nodes
+ int nNodesOver; // nodes with cuts over the limit
+ int nCutsTotal; // total number of cuts
+ int nCutsUseful; // useful cuts
+ int nGainTotal; // the gain in LUTs
+ int nChanges; // the number of changed nodes
+ // counter of non-DSD blocks
+ int nBlocks[17];
+ // rutime
+ int timeCuts;
+ int timeTruth;
+ int timeEval;
+ int timeMap;
+ int timeOther;
+ int timeTotal;
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// ITERATORS ///
+////////////////////////////////////////////////////////////////////////
+
+#define Lpk_CutForEachLeaf( pNtk, pCut, pObj, i ) \
+ for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ )
+#define Lpk_CutForEachNode( pNtk, pCut, pObj, i ) \
+ for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ )
+#define Lpk_CutForEachNodeReverse( pNtk, pCut, pObj, i ) \
+ for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== lpkCut.c =========================================================*/
+extern unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut );
+extern int Lpk_NodeCuts( Lpk_Man_t * p );
+/*=== lpkMap.c =========================================================*/
+extern Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars );
+extern void Lpk_ManStop( Lpk_Man_t * p );
+/*=== lpkMap.c =========================================================*/
+extern int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk );
+extern If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
+extern If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult );
+/*=== lpkMulti.c =======================================================*/
+extern If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nLeaves, If_Obj_t ** ppLeaves );
+/*=== lpkMux.c =========================================================*/
+extern If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
+extern If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
+/*=== lpkSets.c =========================================================*/
+extern unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
new file mode 100644
index 00000000..da8b0e3a
--- /dev/null
+++ b/src/opt/lpk/lpkMan.c
@@ -0,0 +1,96 @@
+/**CFile****************************************************************
+
+ FileName [lpkMan.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: lpkMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
+{
+ Lpk_Man_t * p;
+ int i;
+ assert( pPars->nLutsMax <= 16 );
+ assert( pPars->nVarsMax > 0 );
+ p = ALLOC( Lpk_Man_t, 1 );
+ memset( p, 0, sizeof(Lpk_Man_t) );
+ p->pPars = pPars;
+ p->nCutsMax = LPK_CUTS_MAX;
+ p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
+ p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) );
+ p->vCover = Vec_IntAlloc( 1 << 12 );
+ for ( i = 0; i < 8; i++ )
+ p->vSets[i] = Vec_IntAlloc(100);
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_ManStop( Lpk_Man_t * p )
+{
+ int i;
+ for ( i = 0; i < 8; i++ )
+ Vec_IntFree(p->vSets[i]);
+ if ( p->pIfMan )
+ {
+ void * pPars = p->pIfMan->pPars;
+ If_ManStop( p->pIfMan );
+ free( pPars );
+ }
+ if ( p->vLevels )
+ Vec_VecFree( p->vLevels );
+ if ( p->vVisited )
+ Vec_VecFree( p->vVisited );
+ Vec_IntFree( p->vCover );
+ Vec_PtrFree( p->vTtElems );
+ Vec_PtrFree( p->vTtNodes );
+ free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkMap.c b/src/opt/lpk/lpkMap.c
new file mode 100644
index 00000000..c647fdf7
--- /dev/null
+++ b/src/opt/lpk/lpkMap.c
@@ -0,0 +1,349 @@
+/**CFile****************************************************************
+
+ FileName [lpkMap.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: lpkMap.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_IfManStart( Lpk_Man_t * p )
+{
+ If_Par_t * pPars;
+ assert( p->pIfMan == NULL );
+ // set defaults
+ pPars = ALLOC( If_Par_t, 1 );
+ memset( pPars, 0, sizeof(If_Par_t) );
+ // user-controlable paramters
+ pPars->nLutSize = p->pPars->nLutSize;
+ pPars->nCutsMax = 16;
+ pPars->nFlowIters = 0; // 1
+ pPars->nAreaIters = 0; // 1
+ pPars->DelayTarget = -1;
+ pPars->fPreprocess = 0;
+ pPars->fArea = 1;
+ pPars->fFancy = 0;
+ pPars->fExpRed = 0; //
+ pPars->fLatchPaths = 0;
+ pPars->fSeqMap = 0;
+ pPars->fVerbose = 0;
+ // internal parameters
+ pPars->fTruth = 0;
+ pPars->fUsePerm = 0;
+ pPars->nLatches = 0;
+ pPars->pLutLib = NULL; // Abc_FrameReadLibLut();
+ pPars->pTimesArr = NULL;
+ pPars->pTimesArr = NULL;
+ pPars->fUseBdds = 0;
+ pPars->fUseSops = 0;
+ pPars->fUseCnfs = 0;
+ pPars->fUseMv = 0;
+ // start the mapping manager and set its parameters
+ p->pIfMan = If_ManStart( pPars );
+ If_ManSetupSetAll( p->pIfMan, 1000 );
+ p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the decomposition graph into the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapPrimeInternal( If_Man_t * pIfMan, Kit_Graph_t * pGraph )
+{
+ Kit_Node_t * pNode;
+ If_Obj_t * pAnd0, * pAnd1;
+ int i;
+ // check for constant function
+ if ( Kit_GraphIsConst(pGraph) )
+ return If_ManConst1(pIfMan);
+ // check for a literal
+ if ( Kit_GraphIsVar(pGraph) )
+ return Kit_GraphVar(pGraph)->pFunc;
+ // build the AIG nodes corresponding to the AND gates of the graph
+ Kit_GraphForEachNode( pGraph, pNode, i )
+ {
+ pAnd0 = Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
+ pAnd1 = Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
+ pNode->pFunc = If_ManCreateAnd( pIfMan,
+ If_NotCond( If_Regular(pAnd0), If_IsComplement(pAnd0) ^ pNode->eEdge0.fCompl ),
+ If_NotCond( If_Regular(pAnd1), If_IsComplement(pAnd1) ^ pNode->eEdge1.fCompl ) );
+ }
+ return pNode->pFunc;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Strashes one logic node using its SOP.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
+{
+ Kit_Graph_t * pGraph;
+ Kit_Node_t * pNode;
+ If_Obj_t * pRes;
+ int i;
+ // derive the factored form
+ pGraph = Kit_TruthToGraph( pTruth, nVars, p->vCover );
+ if ( pGraph == NULL )
+ return NULL;
+ // collect the fanins
+ Kit_GraphForEachLeaf( pGraph, pNode, i )
+ pNode->pFunc = ppLeaves[i];
+ // perform strashing
+ pRes = Lpk_MapPrimeInternal( p->pIfMan, pGraph );
+ pRes = If_NotCond( pRes, Kit_GraphIsComplement(pGraph) );
+ Kit_GraphFree( pGraph );
+ return pRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
+{
+ extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
+ Kit_DsdObj_t * pRoot;
+ If_Obj_t * pDriver, * ppLeaves[16];
+ Abc_Obj_t * pLeaf, * pObjNew;
+ int nGain, i;
+// int nOldShared;
+
+ // check special cases
+ pRoot = Kit_DsdNtkRoot( pNtk );
+ if ( pRoot->Type == KIT_DSD_CONST1 )
+ {
+ if ( Kit_DsdLitIsCompl(pNtk->Root) )
+ pObjNew = Abc_NtkCreateNodeConst0( p->pNtk );
+ else
+ pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
+
+ // perform replacement
+ pObjNew->Level = p->pObj->Level;
+ Abc_ObjReplace( p->pObj, pObjNew );
+ Res_UpdateNetworkLevel( pObjNew, p->vLevels );
+ p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
+ return 1;
+ }
+ if ( pRoot->Type == KIT_DSD_VAR )
+ {
+ pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
+ if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) )
+ pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew );
+
+ // perform replacement
+ pObjNew->Level = p->pObj->Level;
+ Abc_ObjReplace( p->pObj, pObjNew );
+ Res_UpdateNetworkLevel( pObjNew, p->vLevels );
+ p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
+ return 1;
+ }
+ assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
+
+ // start the mapping manager
+ if ( p->pIfMan == NULL )
+ Lpk_IfManStart( p );
+
+ // prepare the mapping manager
+ If_ManRestart( p->pIfMan );
+ // create the PI variables
+ for ( i = 0; i < p->pPars->nVarsMax; i++ )
+ ppLeaves[i] = If_ManCreateCi( p->pIfMan );
+ // set the arrival times
+ Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
+ p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
+ // prepare the PI cuts
+ If_ManSetupCiCutSets( p->pIfMan );
+ // create the internal nodes
+ p->fCalledOnce = 0;
+ pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL );
+ if ( pDriver == NULL )
+ return 0;
+ // create the PO node
+ If_ManCreateCo( p->pIfMan, If_Regular(pDriver) );
+
+ // perform mapping
+ p->pIfMan->pPars->fAreaOnly = 1;
+ If_ManPerformMappingComb( p->pIfMan );
+
+ // compute the gain in area
+ nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
+ if ( p->pPars->fVeryVerbose )
+ printf( " Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d.\n",
+ pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level );
+
+ // quit if there is no gain
+ if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
+ return 0;
+
+ // quit if depth increases too much
+ if ( (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level > p->pPars->nGrowthLevel )
+ return 0;
+
+ // perform replacement
+ p->nGainTotal += nGain;
+ p->nChanges++;
+
+ // prepare the mapping manager
+ If_ManCleanNodeCopy( p->pIfMan );
+ If_ManCleanCutData( p->pIfMan );
+ // set the PIs of the cut
+ Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
+ If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
+ // get the area of mapping
+ pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
+ pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
+
+ // perform replacement
+ pObjNew->Level = p->pObj->Level;
+ Abc_ObjReplace( p->pObj, pObjNew );
+ Res_UpdateNetworkLevel( pObjNew, p->vLevels );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult )
+{
+ Kit_DsdObj_t * pObj;
+ If_Obj_t * pObjNew, * pFansNew[16];
+ unsigned i, iLitFanin;
+
+ assert( iLit >= 0 );
+
+ // consider the case of a gate
+ pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) );
+ if ( pObj == NULL )
+ {
+ pObjNew = ppLeaves[Kit_DsdLit2Var(iLit)];
+ return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
+ }
+ if ( pObj->Type == KIT_DSD_CONST1 )
+ {
+ return If_NotCond( If_ManConst1(p->pIfMan), Kit_DsdLitIsCompl(iLit) );
+ }
+ if ( pObj->Type == KIT_DSD_VAR )
+ {
+ pObjNew = ppLeaves[Kit_DsdLit2Var(pObj->pFans[0])];
+ return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ^ Kit_DsdLitIsCompl(pObj->pFans[0]) );
+ }
+ if ( pObj->Type == KIT_DSD_AND )
+ {
+ assert( pObj->nFans == 2 );
+ pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
+ pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
+ if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
+ return NULL;
+ pObjNew = If_ManCreateAnd( p->pIfMan, pFansNew[0], pFansNew[1] );
+ return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
+ }
+ if ( pObj->Type == KIT_DSD_XOR )
+ {
+ int fCompl = Kit_DsdLitIsCompl(iLit);
+ assert( pObj->nFans == 2 );
+ pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
+ pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
+ if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
+ return NULL;
+ fCompl ^= If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]);
+ pObjNew = If_ManCreateXor( p->pIfMan, If_Regular(pFansNew[0]), If_Regular(pFansNew[1]) );
+ return If_NotCond( pObjNew, fCompl );
+ }
+ assert( pObj->Type == KIT_DSD_PRIME );
+ p->nBlocks[pObj->nFans]++;
+
+ // solve for the inputs
+ Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
+ {
+ if ( i == 0 )
+ pFansNew[i] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
+ else
+ pFansNew[i] = Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
+ if ( pFansNew[i] == NULL )
+ return NULL;
+ }
+/*
+ if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
+ {
+ pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+ return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
+ }
+*/
+
+ // find best cofactoring variable
+ if ( pObj->nFans > 3 && !p->fCalledOnce )
+// pObjNew = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+ pObjNew = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+ else
+ pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+ return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkMulti.c b/src/opt/lpk/lpkMulti.c
new file mode 100644
index 00000000..82cf3578
--- /dev/null
+++ b/src/opt/lpk/lpkMulti.c
@@ -0,0 +1,495 @@
+/**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 $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// 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 []
+
+***********************************************************************/
+void Lpk_CreateVarOrder( Kit_DsdNtk_t * pNtk, char pTable[][16] )
+{
+ Kit_DsdObj_t * pObj;
+ unsigned uSuppFanins, k;
+ int Above[16], Below[16];
+ int nAbove, nBelow, iFaninLit, i, x, y;
+ // iterate through the nodes
+ Kit_DsdNtkForEachObj( pNtk, pObj, i )
+ {
+ // collect fanin support of this node
+ nAbove = 0;
+ uSuppFanins = 0;
+ Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k )
+ {
+ if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) )
+ Above[nAbove++] = Kit_DsdLit2Var(iFaninLit);
+ else
+ uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit );
+ }
+ // find the below variables
+ nBelow = 0;
+ for ( y = 0; y < 16; y++ )
+ if ( uSuppFanins & (1 << y) )
+ Below[nBelow++] = y;
+ // create all pairs
+ for ( x = 0; x < nAbove; x++ )
+ for ( y = 0; y < nBelow; y++ )
+ pTable[Above[x]][Below[y]]++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates commmon variable order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_CreateCommonOrder( char pTable[][16], int piCofVar[], int nCBars, int pPrios[], int nVars, int fVerbose )
+{
+ int Score[16] = {0}, pPres[16];
+ int i, y, x, iVarBest, ScoreMax, PrioCount;
+
+ // mark the present variables
+ for ( i = 0; i < nVars; i++ )
+ pPres[i] = 1;
+ // remove cofactored variables
+ for ( i = 0; i < nCBars; i++ )
+ pPres[piCofVar[i]] = 0;
+
+ // compute scores for each leaf
+ for ( i = 0; i < nVars; i++ )
+ {
+ if ( pPres[i] == 0 )
+ continue;
+ for ( y = 0; y < nVars; y++ )
+ Score[i] += pTable[i][y];
+ for ( x = 0; x < nVars; x++ )
+ Score[i] -= pTable[x][i];
+ }
+
+ // print the scores
+ if ( fVerbose )
+ {
+ printf( "Scores: " );
+ for ( i = 0; i < nVars; i++ )
+ printf( "%c=%d ", 'a'+i, Score[i] );
+ printf( " " );
+ printf( "Prios: " );
+ }
+
+ // derive variable priority
+ // variables with equal score receive the same priority
+ for ( i = 0; i < nVars; i++ )
+ pPrios[i] = 16;
+
+ // iterate until variables remain
+ for ( PrioCount = 1; ; PrioCount++ )
+ {
+ // find the present variable with the highest score
+ iVarBest = -1;
+ ScoreMax = -100000;
+ for ( i = 0; i < nVars; i++ )
+ {
+ if ( pPres[i] == 0 )
+ continue;
+ if ( ScoreMax < Score[i] )
+ {
+ ScoreMax = Score[i];
+ iVarBest = i;
+ }
+ }
+ if ( iVarBest == -1 )
+ break;
+ // give the next priority to all vars having this score
+ if ( fVerbose )
+ printf( "%d=", PrioCount );
+ for ( i = 0; i < nVars; i++ )
+ {
+ if ( pPres[i] == 0 )
+ continue;
+ if ( Score[i] == ScoreMax )
+ {
+ pPrios[i] = PrioCount;
+ pPres[i] = 0;
+ if ( fVerbose )
+ printf( "%c", 'a'+i );
+ }
+ }
+ if ( fVerbose )
+ printf( " " );
+ }
+ if ( fVerbose )
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Finds components with the highest priority.]
+
+ Description [Returns the number of components selected.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Lpk_FindHighest( Kit_DsdNtk_t ** ppNtks, int * piLits, int nSize, int * pPrio, int * pDecision )
+{
+ Kit_DsdObj_t * pObj;
+ unsigned uSupps[8], uSuppFanin, uSuppTotal, uSuppLarge;
+ int i, pTriv[8], PrioMin, iVarMax, nComps, fOneNonTriv;
+
+ // find individual support and total support
+ uSuppTotal = 0;
+ for ( i = 0; i < nSize; i++ )
+ {
+ pTriv[i] = 1;
+ if ( piLits[i] < 0 )
+ uSupps[i] = 0;
+ else if ( Kit_DsdLitIsLeaf(ppNtks[i], piLits[i]) )
+ uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] );
+ else
+ {
+ pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
+ if ( pObj->Type == KIT_DSD_PRIME )
+ {
+ pTriv[i] = 0;
+ uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] );
+ }
+ else
+ {
+ assert( pObj->nFans == 2 );
+ if ( !Kit_DsdLitIsLeaf(ppNtks[i], pObj->pFans[0]) )
+ pTriv[i] = 0;
+ uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[1] );
+ }
+ uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin;
+ }
+ assert( uSupps[i] <= 0xFFFF );
+ uSuppTotal |= uSupps[i];
+ }
+ if ( uSuppTotal == 0 )
+ return 0;
+
+ // find one support variable with the highest priority
+ PrioMin = ABC_INFINITY;
+ iVarMax = -1;
+ for ( i = 0; i < 16; i++ )
+ if ( uSuppTotal & (1 << i) )
+ if ( PrioMin > pPrio[i] )
+ {
+ PrioMin = pPrio[i];
+ iVarMax = i;
+ }
+ assert( iVarMax != -1 );
+
+ // select components, which have this variable
+ nComps = 0;
+ fOneNonTriv = 0;
+ uSuppLarge = 0;
+ for ( i = 0; i < nSize; i++ )
+ if ( uSupps[i] & (1<<iVarMax) )
+ {
+ if ( pTriv[i] || !fOneNonTriv )
+ {
+ if ( !pTriv[i] )
+ {
+ uSuppLarge = uSupps[i];
+ fOneNonTriv = 1;
+ }
+ pDecision[i] = 1;
+ nComps++;
+ }
+ else
+ pDecision[i] = 0;
+ }
+ else
+ pDecision[i] = 0;
+
+ // add other non-trivial not-taken components whose support is contained in the current large component support
+ if ( fOneNonTriv )
+ for ( i = 0; i < nSize; i++ )
+ if ( !pTriv[i] && pDecision[i] == 0 && (uSupps[i] & ~uSuppLarge) == 0 )
+ {
+ pDecision[i] = 1;
+ nComps++;
+ }
+
+ return nComps;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+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 )
+{
+ Kit_DsdObj_t * pObj;
+ If_Obj_t * pObjsNew[4][8], * pResPrev;
+ int piLitsNew[8], pDecision[8];
+ int i, k, nComps, nSize;
+
+ // find which of the variables is highest in the order
+ nSize = (1 << nCBars);
+ nComps = Lpk_FindHighest( ppNtks, piLits, nSize, pPrio, pDecision );
+ if ( nComps == 0 )
+ return If_Not( If_ManConst1(p->pIfMan) );
+
+ // iterate over the nodes
+ if ( p->pPars->fVeryVerbose )
+ printf( "Decision: " );
+ for ( i = 0; i < nSize; i++ )
+ {
+ if ( pDecision[i] )
+ {
+ if ( p->pPars->fVeryVerbose )
+ printf( "%d ", i );
+ assert( piLits[i] >= 0 );
+ pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
+ if ( pObj == NULL )
+ piLitsNew[i] = -2;
+ else if ( pObj->Type == KIT_DSD_PRIME )
+ piLitsNew[i] = pObj->pFans[0];
+ else
+ piLitsNew[i] = pObj->pFans[1];
+ }
+ else
+ piLitsNew[i] = piLits[i];
+ }
+ if ( p->pPars->fVeryVerbose )
+ printf( "\n" );
+
+ // call again
+ pResPrev = Lpk_MapTreeMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pPrio );
+
+ // create new set of nodes
+ for ( i = 0; i < nSize; i++ )
+ {
+ if ( pDecision[i] )
+ pObjsNew[nCBars][i] = Lpk_MapTree_rec( p, ppNtks[i], ppLeaves, piLits[i], pResPrev );
+ else if ( piLits[i] == -1 )
+ pObjsNew[nCBars][i] = If_ManConst1(p->pIfMan);
+ else if ( piLits[i] == -2 )
+ pObjsNew[nCBars][i] = If_Not( If_ManConst1(p->pIfMan) );
+ else
+ pObjsNew[nCBars][i] = pResPrev;
+ }
+
+ // create MUX using these outputs
+ for ( k = nCBars; k > 0; k-- )
+ {
+ nSize /= 2;
+ for ( i = 0; i < nSize; i++ )
+ pObjsNew[k-1][i] = If_ManCreateMux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] );
+ }
+ assert( nSize == 1 );
+ return pObjsNew[0][0];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
+{
+ static Counter = 0;
+ If_Obj_t * pResult;
+ Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp;
+ Kit_DsdObj_t * pRoot;
+ int piCofVar[4], pPrios[16], pFreqs[16] = {0}, piLits[16];
+ int i, k, nCBars, nSize, nMemSize;
+ unsigned * ppCofs[4][8], uSupport;
+ char pTable[16][16] = {0};
+ int fVerbose = p->pPars->fVeryVerbose;
+
+ Counter++;
+// printf( "Run %d.\n", Counter );
+
+ // allocate storage for cofactors
+ nMemSize = Kit_TruthWordNum(nVars);
+ ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize );
+ nSize = 0;
+ for ( i = 0; i < 4; i++ )
+ for ( k = 0; k < 8; k++ )
+ ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
+ assert( nSize == 32 );
+
+ // find the best cofactoring variables
+ nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 );
+// nCBars = 2;
+// piCofVar[0] = 0;
+// piCofVar[1] = 1;
+
+
+ // copy the function
+ Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
+
+ // decompose w.r.t. these variables
+ for ( k = 0; k < nCBars; k++ )
+ {
+ nSize = (1 << k);
+ for ( i = 0; i < nSize; i++ )
+ {
+ Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
+ Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
+ }
+ }
+ nSize = (1 << nCBars);
+ // compute DSD networks
+ for ( i = 0; i < nSize; i++ )
+ {
+ ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars );
+ ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
+ Kit_DsdNtkFree( pTemp );
+ if ( fVerbose )
+ {
+ printf( "Cof%d%d: ", nCBars, i );
+ Kit_DsdPrint( stdout, ppNtks[i] );
+ }
+ }
+
+ // compute variable frequences
+ for ( i = 0; i < nSize; i++ )
+ {
+ uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars );
+ for ( k = 0; k < nVars; k++ )
+ if ( uSupport & (1<<k) )
+ pFreqs[k]++;
+ }
+
+ // find common variable order
+ for ( i = 0; i < nSize; i++ )
+ {
+ Kit_DsdGetSupports( ppNtks[i] );
+ Lpk_CreateVarOrder( ppNtks[i], pTable );
+ }
+ Lpk_CreateCommonOrder( pTable, piCofVar, nCBars, pPrios, nVars, fVerbose );
+ // update priorities with frequences
+ for ( i = 0; i < nVars; i++ )
+ pPrios[i] = pPrios[i] * 256 + (16 - pFreqs[i]) * 16 + i;
+
+ if ( fVerbose )
+ printf( "After restructuring with priority:\n" );
+
+ if ( Counter == 1 )
+ {
+ int x = 0;
+ }
+ // transform all networks according to the variable order
+ for ( i = 0; i < nSize; i++ )
+ {
+ ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios );
+ Kit_DsdNtkFree( pTemp );
+ Kit_DsdGetSupports( ppNtks[i] );
+ assert( ppNtks[i]->pSupps[0] <= 0xFFFF );
+ // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible
+ Kit_DsdRotate( ppNtks[i], pFreqs );
+ // print the resulting networks
+ if ( fVerbose )
+ {
+ printf( "Cof%d%d: ", nCBars, i );
+ Kit_DsdPrint( stdout, ppNtks[i] );
+ }
+ }
+
+ for ( i = 0; i < nSize; i++ )
+ {
+ // collect the roots
+ pRoot = Kit_DsdNtkRoot(ppNtks[i]);
+ if ( pRoot->Type == KIT_DSD_CONST1 )
+ piLits[i] = Kit_DsdLitIsCompl(ppNtks[i]->Root)? -2: -1;
+ else if ( pRoot->Type == KIT_DSD_VAR )
+ piLits[i] = Kit_DsdLitNotCond( pRoot->pFans[0], Kit_DsdLitIsCompl(ppNtks[i]->Root) );
+ else
+ piLits[i] = ppNtks[i]->Root;
+ }
+
+
+ // recursively construct AIG for mapping
+ p->fCofactoring = 1;
+ pResult = Lpk_MapTreeMulti_rec( p, ppNtks, piLits, piCofVar, nCBars, ppLeaves, nVars, pPrios );
+ p->fCofactoring = 0;
+
+ if ( fVerbose )
+ printf( "\n" );
+
+ // verify the transformations
+ nSize = (1 << nCBars);
+ for ( i = 0; i < nSize; i++ )
+ Kit_DsdTruth( ppNtks[i], ppCofs[nCBars][i] );
+ // mux the truth tables
+ for ( k = nCBars-1; k >= 0; k-- )
+ {
+ nSize = (1 << k);
+ for ( i = 0; i < nSize; i++ )
+ Kit_TruthMuxVar( ppCofs[k][i], ppCofs[k+1][2*i+0], ppCofs[k+1][2*i+1], nVars, piCofVar[k] );
+ }
+ if ( !Extra_TruthIsEqual( pTruth, ppCofs[0][0], nVars ) )
+ printf( "Verification failed.\n" );
+
+
+ // free the networks
+ for ( i = 0; i < 8; i++ )
+ if ( ppNtks[i] )
+ Kit_DsdNtkFree( ppNtks[i] );
+ free( ppCofs[0][0] );
+
+ return pResult;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkMux.c b/src/opt/lpk/lpkMux.c
new file mode 100644
index 00000000..d9e013f0
--- /dev/null
+++ b/src/opt/lpk/lpkMux.c
@@ -0,0 +1,257 @@
+/**CFile****************************************************************
+
+ FileName [lpkMux.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: lpkMux.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Find the best cofactoring variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
+{
+// Kit_DsdNtk_t * ppNtks[2], * pTemp;
+ unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
+ unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
+ int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
+// int nPrimeSizeCur0, nPrimeSizeCur1, nPrimeSizeCur, nPrimeSizeMin;
+
+ // iterate through variables
+ iBestVar = -1;
+ nSuppSizeMin = ABC_INFINITY;
+// nPrimeSizeMin = ABC_INFINITY;
+ for ( i = 0; i < nVars; i++ )
+ {
+ // cofactor the functiona and get support sizes
+ Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
+ Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
+ nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
+ nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
+ nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1;
+/*
+ // check the size of the largest prime components
+ ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
+ ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
+ // compute the largest non-decomp block
+ nPrimeSizeCur0 = Kit_DsdNonDsdSizeMax(ppNtks[0]);
+ nPrimeSizeCur1 = Kit_DsdNonDsdSizeMax(ppNtks[1]);
+ nPrimeSizeCur = KIT_MAX( nPrimeSizeCur0, nPrimeSizeCur1 );
+
+ printf( "Evaluating variable %c:\n", 'a'+i );
+// Kit_DsdPrintExpanded( ppNtks[0] );
+// Kit_DsdPrintExpanded( ppNtks[1] );
+
+ ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
+ Kit_DsdNtkFree( pTemp );
+
+ ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );
+ Kit_DsdNtkFree( pTemp );
+
+ Kit_DsdPrint( stdout, ppNtks[0] );
+ Kit_DsdPrint( stdout, ppNtks[1] );
+
+// Lpk_DsdEvalSets( p, ppNtks[0], ppNtks[1] );
+
+ // free the networks
+ Kit_DsdNtkFree( ppNtks[0] );
+ Kit_DsdNtkFree( ppNtks[1] );
+*/
+ // compare this variable with other variables
+ if ( nSuppSizeMin > nSuppSizeCur ) //|| (nSuppSizeMin == nSuppSizeCur && nPrimeSizeMin > nPrimeSizeCur ) )
+ {
+ nSuppSizeMin = nSuppSizeCur;
+// nPrimeSizeMin = nPrimeSizeCur;
+ iBestVar = i;
+ }
+ }
+ printf( "\n" );
+ assert( iBestVar != -1 );
+ return iBestVar;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Maps the function by the best cofactoring.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
+{
+ If_Obj_t * pObj0, * pObj1;
+ Kit_DsdNtk_t * ppNtks[2];
+ unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
+ unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
+ int iBestVar;
+ assert( nVars > 3 );
+ p->fCalledOnce = 1;
+
+ // cofactor w.r.t. the best variable
+ iBestVar = Lpk_MapTreeBestVar( p, pTruth, nVars );
+ Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
+ Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
+ // decompose the functions
+ ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
+ ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
+ if ( p->pPars->fVeryVerbose )
+ {
+ printf( "Cofactoring w.r.t. var %c (%d -> %d+%d supp vars):\n",
+ 'a'+iBestVar, nVars, Kit_TruthSupportSize(pCof0, nVars), Kit_TruthSupportSize(pCof1, nVars) );
+ Kit_DsdPrintExpanded( ppNtks[0] );
+ Kit_DsdPrintExpanded( ppNtks[1] );
+ }
+ // map the DSD structures
+ pObj0 = Lpk_MapTree_rec( p, ppNtks[0], ppLeaves, ppNtks[0]->Root, NULL );
+ pObj1 = Lpk_MapTree_rec( p, ppNtks[1], ppLeaves, ppNtks[1]->Root, NULL );
+ Kit_DsdNtkFree( ppNtks[0] );
+ Kit_DsdNtkFree( ppNtks[1] );
+ return If_ManCreateMux( p->pIfMan, pObj0, pObj1, ppLeaves[iBestVar] );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Implements support-reducing decomposition.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
+{
+ Kit_DsdNtk_t * pNtkDec, * pNtkComp;
+ If_Obj_t * pObjNew;
+ unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
+ unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
+ unsigned * pDec0 = Vec_PtrEntry( p->vTtNodes, 2 );
+ unsigned * pDec1 = Vec_PtrEntry( p->vTtNodes, 3 );
+ unsigned * pDec = Vec_PtrEntry( p->vTtNodes, 4 );
+ unsigned * pCo00 = Vec_PtrEntry( p->vTtNodes, 5 );
+ unsigned * pCo01 = Vec_PtrEntry( p->vTtNodes, 6 );
+ unsigned * pCo10 = Vec_PtrEntry( p->vTtNodes, 7 );
+ unsigned * pCo11 = Vec_PtrEntry( p->vTtNodes, 8 );
+ unsigned * pCo0 = Vec_PtrEntry( p->vTtNodes, 9 );
+ unsigned * pCo1 = Vec_PtrEntry( p->vTtNodes, 10 );
+ unsigned * pCo = Vec_PtrEntry( p->vTtNodes, 11 );
+ int TrueMint0, TrueMint1;
+ int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i;
+
+ // determine if supp-red decomposition exists
+ uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused );
+ if ( uSubsets == 0 )
+ return NULL;
+
+ // get the bound sets
+ uSubset0 = uSubsets & 0xFFFF;
+ uSubset1 = uSubsets >> 16;
+ // get the cofactors
+ Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar );
+ Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar );
+ // find any true assignments of the cofactors
+ TrueMint0 = Kit_TruthFindFirstBit( pCof0, nVars );
+ TrueMint1 = Kit_TruthFindFirstBit( pCof1, nVars );
+ assert( TrueMint0 >= 0 && TrueMint1 >= 0 );
+ // cofactor the cofactors according to these minterms
+ Kit_TruthCopy( pDec0, pCof0, nVars );
+ Kit_TruthCopy( pDec1, pCof1, nVars );
+ for ( i = 0; i < nVars; i++ )
+ if ( !(uSubset0 & (1 << i)) )
+ {
+ if ( TrueMint0 & (1 << i) )
+ Kit_TruthCofactor1( pDec0, nVars, i );
+ else
+ Kit_TruthCofactor0( pDec0, nVars, i );
+ }
+ for ( i = 0; i < nVars; i++ )
+ if ( !(uSubset1 & (1 << i)) )
+ {
+ if ( TrueMint1 & (1 << i) )
+ Kit_TruthCofactor1( pDec1, nVars, i );
+ else
+ Kit_TruthCofactor0( pDec1, nVars, i );
+ }
+ // get the decomposed function
+ Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
+
+ // derive the remainders
+ Kit_TruthAndPhase( pCo00, pCof0, pDec0, nVars, 0, 1 );
+ Kit_TruthAndPhase( pCo01, pCof0, pDec0, nVars, 0, 0 );
+ Kit_TruthAndPhase( pCo10, pCof1, pDec1, nVars, 0, 1 );
+ Kit_TruthAndPhase( pCo11, pCof1, pDec1, nVars, 0, 0 );
+ // quantify bound set variables
+ for ( i = 0; i < nVars; i++ )
+ if ( uSubset0 & (1 << i) )
+ {
+ Kit_TruthExist( pCo00, nVars, i );
+ Kit_TruthExist( pCo01, nVars, i );
+ }
+ for ( i = 0; i < nVars; i++ )
+ if ( uSubset1 & (1 << i) )
+ {
+ Kit_TruthExist( pCo10, nVars, i );
+ Kit_TruthExist( pCo11, nVars, i );
+ }
+ // derive the functions by composing them with the new variable (iVarReused)
+ Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused );
+ Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused );
+ // derive the composition function
+ Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar );
+
+ // process the decomposed function
+ pNtkDec = Kit_DsdDecompose( pDec, nVars );
+ Kit_DsdPrint( stdout, pNtkDec );
+ ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
+ Kit_DsdNtkFree( pNtkDec );
+
+ // process the composition function
+ pNtkComp = Kit_DsdDecompose( pCo, nVars );
+ Kit_DsdPrint( stdout, pNtkComp );
+ pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL );
+ Kit_DsdNtkFree( pNtkComp );
+ return pObjNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c
new file mode 100644
index 00000000..721705cb
--- /dev/null
+++ b/src/opt/lpk/lpkSets.c
@@ -0,0 +1,399 @@
+/**CFile****************************************************************
+
+ FileName [lpkSets.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: lpkSets.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Lpk_Set_t_ Lpk_Set_t;
+struct Lpk_Set_t_
+{
+ char iVar; // the cofactoring variable
+ char Over; // the overlap in supports
+ char SRed; // the support reduction
+ char Size; // the size of the boundset
+ unsigned uSubset0; // the first subset (with removed)
+ unsigned uSubset1; // the second subset (with removed)
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Recursively computes decomposable subsets.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Lpk_ComputeSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
+{
+ unsigned i, iLitFanin, uSupport, uSuppCur;
+ Kit_DsdObj_t * pObj;
+ // consider the case of simple gate
+ pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
+ if ( pObj == NULL )
+ return (1 << Kit_DsdLit2Var(iLit));
+ if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
+ {
+ unsigned uSupps[16], Limit, s;
+ uSupport = 0;
+ Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
+ {
+ uSupps[i] = Lpk_ComputeSets_rec( p, iLitFanin, vSets );
+ uSupport |= uSupps[i];
+ }
+ // create all subsets, except empty and full
+ Limit = (1 << pObj->nFans) - 1;
+ for ( s = 1; s < Limit; s++ )
+ {
+ uSuppCur = 0;
+ for ( i = 0; i < pObj->nFans; i++ )
+ if ( s & (1 << i) )
+ uSuppCur |= uSupps[i];
+ Vec_IntPush( vSets, uSuppCur );
+ }
+ return uSupport;
+ }
+ assert( pObj->Type == KIT_DSD_PRIME );
+ // get the cumulative support of all fanins
+ uSupport = 0;
+ Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
+ {
+ uSuppCur = Lpk_ComputeSets_rec( p, iLitFanin, vSets );
+ uSupport |= uSuppCur;
+ Vec_IntPush( vSets, uSuppCur );
+ }
+ return uSupport;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the set of subsets of decomposable variables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
+{
+ unsigned uSupport, Entry, i;
+ assert( p->nVars <= 16 );
+ Vec_IntClear( vSets );
+ Vec_IntPush( vSets, 0 );
+ if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
+ return 0;
+ if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
+ {
+ uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
+ Vec_IntPush( vSets, uSupport );
+ return uSupport;
+ }
+ uSupport = Lpk_ComputeSets_rec( p, p->Root, vSets );
+ assert( (uSupport & 0xFFFF0000) == 0 );
+ Vec_IntPush( vSets, uSupport );
+ // set the remaining variables
+ Vec_IntForEachEntry( vSets, Entry, i )
+ Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
+ return uSupport;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the sets of subsets.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_PrintSetOne( int uSupport )
+{
+ unsigned k;
+ for ( k = 0; k < 16; k++ )
+ if ( uSupport & (1<<k) )
+ printf( "%c", 'a'+k );
+ printf( " " );
+}
+/**Function*************************************************************
+
+ Synopsis [Prints the sets of subsets.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_PrintSets( Vec_Int_t * vSets )
+{
+ unsigned uSupport, i;
+ printf( "Subsets(%d): ", Vec_IntSize(vSets) );
+ Vec_IntForEachEntry( vSets, uSupport, i )
+ Lpk_PrintSetOne( uSupport );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes maximal support reducing bound-sets.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCofVar,
+ Lpk_Set_t * pStore, int * pSize, int nSizeLimit )
+{
+ static int nTravId = 0; // the number of the times this is visited
+ static int TravId[1<<16] = {0}; // last visited
+ static char SRed[1<<16]; // best support reduction
+ static char Over[1<<16]; // best overlaps
+ static unsigned Parents[1<<16]; // best set of parents
+ static unsigned short Used[1<<16]; // storage for used subsets
+ int nSuppSize, nSuppOver, nSuppRed, nUsed, nMinOver, i, k, s;
+ unsigned Entry, Entry0, Entry1;
+ unsigned uSupp, uSupp0, uSupp1, uSuppTotal;
+ Lpk_Set_t * pEntry;
+
+ if ( nTravId == (1 << 30) )
+ memset( TravId, 0, sizeof(int) * (1 << 16) );
+
+ // collect support reducing subsets
+ nUsed = 0;
+ nTravId++;
+ uSuppTotal = Kit_BitMask(nVars) & ~(1<<iCofVar);
+ Vec_IntForEachEntry( vSets0, Entry0, i )
+ Vec_IntForEachEntry( vSets1, Entry1, k )
+ {
+ uSupp0 = (Entry0 & 0xFFFF);
+ uSupp1 = (Entry1 & 0xFFFF);
+ // skip trivial
+ if ( uSupp0 == 0 || uSupp1 == 0 || (uSupp0 | uSupp1) == uSuppTotal )
+ continue;
+ if ( Kit_WordHasOneBit(uSupp0) && Kit_WordHasOneBit(uSupp1) )
+ continue;
+ // get the entry
+ Entry = Entry0 | Entry1;
+ uSupp = Entry & 0xFFFF;
+ // set the bound set size
+ nSuppSize = Kit_WordCountOnes( uSupp );
+ // get the number of overlapping vars
+ nSuppOver = Kit_WordCountOnes( Entry & (Entry >> 16) );
+ // get the support reduction
+ nSuppRed = nSuppSize - 1 - nSuppOver;
+ // only consider support-reducing subsets
+ if ( nSuppRed <= 0 )
+ continue;
+ // check if this support is already used
+ if ( TravId[uSupp] < nTravId )
+ {
+ Used[nUsed++] = uSupp;
+
+ TravId[uSupp] = nTravId;
+ SRed[uSupp] = nSuppRed;
+ Over[uSupp] = nSuppOver;
+ Parents[uSupp] = (k << 16) | i;
+ }
+ else if ( TravId[uSupp] == nTravId && SRed[uSupp] < nSuppRed )
+ {
+ TravId[uSupp] = nTravId;
+ SRed[uSupp] = nSuppRed;
+ Over[uSupp] = nSuppOver;
+ Parents[uSupp] = (k << 16) | i;
+ }
+ }
+
+ // check if there are non-overlapping
+ nMinOver = 1000;
+ for ( s = 0; s < nUsed; s++ )
+ if ( nMinOver > Over[Used[s]] )
+ nMinOver = Over[Used[s]];
+
+
+ // collect the accumulated ones
+ for ( s = 0; s < nUsed; s++ )
+ if ( Over[Used[s]] == nMinOver )
+ {
+ // save the entry
+ if ( *pSize == nSizeLimit )
+ return;
+ pEntry = pStore + (*pSize)++;
+
+ i = Parents[Used[s]] & 0xFFFF;
+ k = Parents[Used[s]] >> 16;
+
+ pEntry->uSubset0 = Vec_IntEntry(vSets0, i);
+ pEntry->uSubset1 = Vec_IntEntry(vSets1, k);
+ Entry = pEntry->uSubset0 | pEntry->uSubset1;
+
+ // record the cofactoring variable
+ pEntry->iVar = iCofVar;
+ // set the bound set size
+ pEntry->Size = Kit_WordCountOnes( Entry & 0xFFFF );
+ // get the number of overlapping vars
+ pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) );
+ // get the support reduction
+ pEntry->SRed = pEntry->Size - 1 - pEntry->Over;
+ assert( pEntry->SRed > 0 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints one set.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_MapSuppPrintSet( Lpk_Set_t * pSet, int i )
+{
+ unsigned Entry;
+ Entry = pSet->uSubset0 | pSet->uSubset1;
+ printf( "%2d : ", i );
+ printf( "Var = %c ", 'a' + pSet->iVar );
+ printf( "Size = %2d ", pSet->Size );
+ printf( "Over = %2d ", pSet->Over );
+ printf( "SRed = %2d ", pSet->SRed );
+ Lpk_PrintSetOne( Entry );
+ printf( " " );
+ Lpk_PrintSetOne( Entry >> 16 );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Evaluates the cofactors.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused )
+{
+ static int nStoreSize = 256;
+ static Lpk_Set_t pStore[256], * pSet, * pSetBest;
+ Kit_DsdNtk_t * ppNtks[2], * pTemp;
+ Vec_Int_t * vSets0 = p->vSets[0];
+ Vec_Int_t * vSets1 = p->vSets[1];
+ unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
+ unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
+ int nSets, i, SizeMax;
+ unsigned Entry;
+
+ // collect decomposable subsets for each pair of cofactors
+ nSets = 0;
+ for ( i = 0; i < nVars; i++ )
+ {
+ printf( "Evaluating variable %c:\n", 'a'+i );
+ // evaluate the cofactor pair
+ Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
+ Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
+ // decompose and expand
+ ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
+ ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
+ ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp );
+ ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp );
+ Kit_DsdPrint( stdout, ppNtks[0] );
+ Kit_DsdPrint( stdout, ppNtks[1] );
+ // compute subsets
+ Lpk_ComputeSets( ppNtks[0], vSets0 );
+ Lpk_ComputeSets( ppNtks[1], vSets1 );
+ // print subsets
+ Lpk_PrintSets( vSets0 );
+ Lpk_PrintSets( vSets1 );
+ // free the networks
+ Kit_DsdNtkFree( ppNtks[0] );
+ Kit_DsdNtkFree( ppNtks[1] );
+ // evaluate the pair
+ Lpk_ComposeSets( vSets0, vSets1, nVars, i, pStore, &nSets, nStoreSize );
+ }
+
+ // print the results
+ printf( "\n" );
+ for ( i = 0; i < nSets; i++ )
+ Lpk_MapSuppPrintSet( pStore + i, i );
+
+ // choose the best subset
+ SizeMax = 0;
+ pSetBest = NULL;
+ for ( i = 0; i < nSets; i++ )
+ {
+ pSet = pStore + i;
+ if ( pSet->Size > p->pPars->nLutSize - 1 )
+ continue;
+ if ( SizeMax < pSet->Size )
+ {
+ pSetBest = pSet;
+ SizeMax = pSet->Size;
+ }
+ }
+ if ( pSetBest == NULL )
+ {
+ printf( "Could not select a subset.\n" );
+ return 0;
+ }
+ else
+ {
+ printf( "Selected the following subset:\n" );
+ Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore );
+ }
+
+ // prepare the return result
+ // get the remaining variables
+ Entry = ((pSetBest->uSubset0 >> 16) | (pSetBest->uSubset1 >> 16));
+ // get the variables to be removed
+ Entry = Kit_BitMask(nVars) & ~(1<<pSetBest->iVar) & ~Entry;
+ // make sure there are some - otherwise it is not supp-red
+ assert( Entry );
+ // remember the first such variable
+ *piVarReused = Kit_WordFindFirstBit( Entry );
+ *piVar = pSetBest->iVar;
+ return (pSetBest->uSubset1 << 16) | (pSetBest->uSubset0 & 0xFFFF);
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpk_.c b/src/opt/lpk/lpk_.c
new file mode 100644
index 00000000..d8555e08
--- /dev/null
+++ b/src/opt/lpk/lpk_.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+ FileName [lpk_.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: lpk_.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/module.make b/src/opt/lpk/module.make
new file mode 100644
index 00000000..9e7bbc7c
--- /dev/null
+++ b/src/opt/lpk/module.make
@@ -0,0 +1,7 @@
+SRC += src/aig/lpk/lpkCore.c \
+ src/aig/lpk/lpkCut.c \
+ src/aig/lpk/lpkMan.c \
+ src/aig/lpk/lpkMap.c \
+ src/aig/lpk/lpkMulti.c \
+ src/aig/lpk/lpkMux.c \
+ src/aig/lpk/lpkSets.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-17 07:23:36 +0000