/**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"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// 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++] = Abc_Lit2Var(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], Abc_Lit2Var(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], Abc_Lit2Var(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 int 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,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}
};
int fVerbose = p->pPars->fVeryVerbose;
Counter++;
// printf( "Run %d.\n", Counter );
// allocate storage for cofactors
nMemSize = Kit_TruthWordNum(nVars);
ppCofs[0][0] = ABC_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" );
// 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] = Abc_LitIsCompl(ppNtks[i]->Root)? -2: -1;
else if ( pRoot->Type == KIT_DSD_VAR )
piLits[i] = Abc_LitNotCond( pRoot->pFans[0], Abc_LitIsCompl(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] );
ABC_FREE( ppCofs[0][0] );
return pResult;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END