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