diff options
Diffstat (limited to 'abc70930/src/opt/lpk/lpkMulti.c')
| -rw-r--r-- | abc70930/src/opt/lpk/lpkMulti.c | 495 |
1 files changed, 495 insertions, 0 deletions
diff --git a/abc70930/src/opt/lpk/lpkMulti.c b/abc70930/src/opt/lpk/lpkMulti.c new file mode 100644 index 00000000..82cf3578 --- /dev/null +++ b/abc70930/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 /// +//////////////////////////////////////////////////////////////////////// + + |