diff options
Diffstat (limited to 'src/opt/lpk/lpkAbcDsd.c')
| -rw-r--r-- | src/opt/lpk/lpkAbcDsd.c | 395 |
1 files changed, 395 insertions, 0 deletions
diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c new file mode 100644 index 00000000..893844e0 --- /dev/null +++ b/src/opt/lpk/lpkAbcDsd.c @@ -0,0 +1,395 @@ +/**CFile**************************************************************** + + FileName [lpkAbcDsd.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: lpkAbcDsd.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the variable whose cofs have min sum of supp sizes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs ) +{ + int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur; + VarBest = -1; + Lpk_SuppForEachVar( p->uSupp, Var ) + { + nSuppMaxCur = 0; + nSuppTotalCur = 0; + for ( i = 0; i < nTruths; i++ ) + { + Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var ); + Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var ); + nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars ); + nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars ); + nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize0 ); + nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize1 ); + nSuppTotalCur += nSuppSize0 + nSuppSize1; + } + if ( VarBest == -1 || nSuppTotalMin > nSuppTotalCur || + (nSuppTotalMin == nSuppTotalCur && nSuppMaxMin > nSuppMaxCur) ) + { + VarBest = Var; + nSuppMaxMin = nSuppMaxCur; + nSuppTotalMin = nSuppTotalCur; + } + } + // recompute cofactors for the best var + for ( i = 0; i < nTruths; i++ ) + { + Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, VarBest ); + Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, VarBest ); + } + return VarBest; +} + +/**Function************************************************************* + + Synopsis [Recursively computes decomposable subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Lpk_ComputeBoundSets_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_ComputeBoundSets_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_ComputeBoundSets_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 [] + +***********************************************************************/ +Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax ) +{ + Vec_Int_t * vSets; + unsigned uSupport, Entry; + int Number, i; + assert( p->nVars <= 16 ); + vSets = Vec_IntAlloc( 100 ); + Vec_IntPush( vSets, 0 ); + if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 ) + return vSets; + if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR ) + { + uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) ); + Vec_IntPush( vSets, uSupport ); + return vSets; + } + uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets ); + assert( (uSupport & 0xFFFF0000) == 0 ); + Vec_IntPush( vSets, uSupport ); + // set the remaining variables + Vec_IntForEachEntry( vSets, Number, i ) + { + Entry = Number; + Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) ); + } + return vSets; +} + +/**Function************************************************************* + + Synopsis [Merges two bound sets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1 ) +{ + Vec_Int_t * vSets; + int Entry0, Entry1, Entry; + int i, k; + vSets = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vSets0, Entry0, i ) + Vec_IntForEachEntry( vSets1, Entry1, k ) + { + Entry = Entry0 | Entry1; + if ( (Entry & (Entry >> 16)) ) + continue; + Vec_IntPush( vSets, Entry ); + } + return vSets; +} + +/**Function************************************************************* + + Synopsis [Allocates truth tables for cofactors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_FunAllocTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] ) +{ + int i; + assert( nCofDepth <= 4 ); + ppTruths[0][0] = Lpk_FunTruth( p, 0 ); + if ( nCofDepth >= 1 ) + { + ppTruths[1][0] = Lpk_FunTruth( p, 1 ); + ppTruths[1][1] = Lpk_FunTruth( p, 2 ); + } + if ( nCofDepth >= 2 ) + { + ppTruths[2][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 4 ); + for ( i = 1; i < 4; i++ ) + ppTruths[2][i] = ppTruths[2][0] + Kit_TruthWordNum(p->nVars) * i; + } + if ( nCofDepth >= 3 ) + { + ppTruths[3][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 8 ); + for ( i = 1; i < 8; i++ ) + ppTruths[3][i] = ppTruths[3][0] + Kit_TruthWordNum(p->nVars) * i; + } + if ( nCofDepth >= 4 ) + { + ppTruths[4][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 16 ); + for ( i = 1; i < 16; i++ ) + ppTruths[4][i] = ppTruths[4][0] + Kit_TruthWordNum(p->nVars) * i; + } +} + +/**Function************************************************************* + + Synopsis [Allocates truth tables for cofactors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] ) +{ + if ( nCofDepth >= 2 ) + free( ppTruths[2][0] ); + if ( nCofDepth >= 3 ) + free( ppTruths[3][0] ); + if ( nCofDepth >= 4 ) + free( ppTruths[4][0] ); +} + +/**Function************************************************************* + + Synopsis [Performs DSD-based decomposition of the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Lpk_Res_t * Lpk_FunAnalizeDsd( Lpk_Fun_t * p, int nCofDepth ) +{ + static Lpk_Res_t Res, * pRes = &Res; + unsigned * ppTruths[5][16]; + Vec_Int_t * pvBSets[4][8]; + Kit_DsdNtk_t * pNtkDec, * pTemp; + unsigned uBoundSet; + int i, k, nVarsBS, nVarsRem, Delay, Area; + Lpk_FunAllocTruthTables( p, nCofDepth, ppTruths ); + // find the best cofactors + memset( pRes, 0, sizeof(Lpk_Res_t) ); + pRes->nCofVars = nCofDepth; + for ( i = 0; i < nCofDepth; i++ ) + pRes->pCofVars[i] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[i], 1<<i, ppTruths[i+1] ); + // derive decomposed networks + for ( i = 0; i < (1<<nCofDepth); i++ ) + { + pNtkDec = Kit_DsdDecompose( ppTruths[nCofDepth][i], p->nVars ); + pNtkDec = Kit_DsdExpand( pTemp = pNtkDec ); Kit_DsdNtkFree( pTemp ); + pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtkDec, p->nLutK - nCofDepth ); + Kit_DsdNtkFree( pNtkDec ); + } + // derive the set of feasible boundsets + for ( i = nCofDepth - 1; i >= 0; i-- ) + for ( k = 0; k < (1<<i); k++ ) + pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1] ); + // compare the resulting boundsets + Vec_IntForEachEntry( pvBSets[0][0], uBoundSet, i ) + { + if ( uBoundSet == 0 ) + continue; + assert( (uBoundSet & (uBoundSet >> 16)) == 0 ); + nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF ); + nVarsRem = p->nVars - nVarsBS + nCofDepth + 1; + Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays ); + Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK ); + if ( Delay > (int)p->nDelayLim || Area > (int)p->nAreaLim ) + continue; + if ( uBoundSet == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem ) + { + pRes->nBSVars = nVarsBS; + pRes->BSVars = uBoundSet; + pRes->nSuppSizeS = nVarsBS; + pRes->nSuppSizeL = nVarsRem; + pRes->DelayEst = Delay; + pRes->AreaEst = Area; + } + } + // free cofactor storage + Lpk_FunFreeTruthTables( p, nCofDepth, ppTruths ); + return pRes; +} + +/**Function************************************************************* + + Synopsis [Splits the function into two subfunctions using DSD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Lpk_Fun_t * Lpk_FunSplitDsd( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet ) +{ + Kit_DsdMan_t * pDsdMan; + Kit_DsdNtk_t * pNtkDec, * pTemp; + unsigned * pTruth = Lpk_FunTruth( p, 0 ); + unsigned * pTruth0 = Lpk_FunTruth( p, 1 ); + unsigned * pTruth1 = Lpk_FunTruth( p, 2 ); + Lpk_Fun_t * pNew; + unsigned * ppTruths[5][16]; + char pBSVars[5]; + int i, k, nVars, nCofs; + // get the bound set variables + nVars = Lpk_SuppToVars( uBoundSet, pBSVars ); + // compute the cofactors + Lpk_FunAllocTruthTables( p, nCofVars, ppTruths ); + for ( i = 0; i < nCofVars; i++ ) + for ( k = 0; k < (1<<i); k++ ) + { + Kit_TruthCofactor0New( ppTruths[i+1][2*k+0], ppTruths[i][k], p->nVars, pCofVars[i] ); + Kit_TruthCofactor1New( ppTruths[i+1][2*k+1], ppTruths[i][k], p->nVars, pCofVars[i] ); + } + // decompose each cofactor w.r.t. the bound set + nCofs = (1<<nCofVars); + pDsdMan = Kit_DsdManAlloc( p->nVars, p->nVars * 4 ); + for ( k = 0; k < nCofs; k++ ) + { + pNtkDec = Kit_DsdDecompose( ppTruths[nCofVars][k], p->nVars ); + pNtkDec = Kit_DsdExpand( pTemp = pNtkDec ); Kit_DsdNtkFree( pTemp ); + Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, pBSVars[0], ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] ); + Kit_DsdNtkFree( pNtkDec ); + } + Kit_DsdManFree( pDsdMan ); + // compute the composition function + for ( i = nCofVars - 1; i >= 1; i-- ) + for ( k = 0; k < (1<<i); k++ ) + Kit_TruthMuxVar( ppTruths[i][k], ppTruths[i+1][2*k+0], ppTruths[i+1][2*k+1], nVars, pCofVars[i] ); + // now the composition/decomposition functions are in pTruth0/pTruth1 + + // derive the new component + pNew = Lpk_FunDup( p, pTruth1 ); + // update the old component + Kit_TruthCopy( pTruth, pTruth0, p->nVars ); + p->uSupp = Kit_TruthSupport( pTruth0, p->nVars ); + p->pFanins[pBSVars[0]] = pNew->Id; + p->pDelays[pBSVars[0]] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays ); + // support minimize both + Lpk_FunSuppMinimize( p ); + Lpk_FunSuppMinimize( pNew ); + // update delay and area requirements + pNew->nDelayLim = p->nDelayLim - 1; + pNew->nAreaLim = 1; + p->nAreaLim = p->nAreaLim - 1; + + // free cofactor storage + Lpk_FunFreeTruthTables( p, nCofVars, ppTruths ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |