| /**CFile**************************************************************** |
| |
| FileName [lpkAbcDsd.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Fast Boolean matching for LUT structures.] |
| |
| Synopsis [LUT-decomposition based on recursive DSD.] |
| |
| 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" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Cofactors TTs w.r.t. all vars and finds the best var.] |
| |
| Description [The best variable is the variable with the minimum |
| sum total of the support sizes of all truth tables. This procedure |
| computes and returns cofactors w.r.t. the best variable.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs, unsigned uNonDecSupp ) |
| { |
| int i, Var, VarBest, nSuppSize0, nSuppSize1; |
| int nSuppTotalMin = -1; // Suppress "might be used uninitialized" |
| int nSuppTotalCur; |
| int nSuppMaxMin = -1; // Suppress "might be used uninitialized" |
| int nSuppMaxCur; |
| assert( nTruths > 0 ); |
| VarBest = -1; |
| Lpk_SuppForEachVar( p->uSupp, Var ) |
| { |
| if ( (uNonDecSupp & (1 << Var)) == 0 ) |
| continue; |
| nSuppMaxCur = 0; |
| nSuppTotalCur = 0; |
| for ( i = 0; i < nTruths; i++ ) |
| { |
| if ( nTruths == 1 ) |
| { |
| nSuppSize0 = Kit_WordCountOnes( p->puSupps[2*Var+0] ); |
| nSuppSize1 = Kit_WordCountOnes( p->puSupps[2*Var+1] ); |
| } |
| else |
| { |
| 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_MaxInt( nSuppMaxCur, nSuppSize0 ); |
| nSuppMaxCur = Abc_MaxInt( nSuppMaxCur, nSuppSize1 ); |
| nSuppTotalCur += nSuppSize0 + nSuppSize1; |
| } |
| if ( VarBest == -1 || nSuppMaxMin > nSuppMaxCur || |
| (nSuppMaxMin == nSuppMaxCur && nSuppTotalMin > nSuppTotalCur) ) |
| { |
| 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, int nSizeMax ) |
| { |
| unsigned i, iLitFanin, uSupport, uSuppCur; |
| Kit_DsdObj_t * pObj; |
| // consider the case of simple gate |
| pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) ); |
| if ( pObj == NULL ) |
| return (1 << Abc_Lit2Var(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, nSizeMax ); |
| 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]; |
| if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax ) |
| 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, nSizeMax ); |
| uSupport |= uSuppCur; |
| if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax ) |
| 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 << Abc_Lit2Var(Kit_DsdNtkRoot(p)->pFans[0]) ); |
| if ( Kit_WordCountOnes(uSupport) <= nSizeMax ) |
| Vec_IntPush( vSets, uSupport ); |
| return vSets; |
| } |
| uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets, nSizeMax ); |
| assert( (uSupport & 0xFFFF0000) == 0 ); |
| // add the total support of the network |
| if ( Kit_WordCountOnes(uSupport) <= nSizeMax ) |
| 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 [Prints the sets of subsets.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static 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 [] |
| |
| ***********************************************************************/ |
| static void Lpk_PrintSets( Vec_Int_t * vSets ) |
| { |
| unsigned uSupport; |
| int Number, i; |
| printf( "Subsets(%d): ", Vec_IntSize(vSets) ); |
| Vec_IntForEachEntry( vSets, Number, i ) |
| { |
| uSupport = Number; |
| Lpk_PrintSetOne( uSupport ); |
| } |
| printf( "\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Merges two bound sets.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSizeMax ) |
| { |
| 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; |
| if ( Kit_WordCountOnes(Entry & 0xffff) <= nSizeMax ) |
| Vec_IntPush( vSets, Entry ); |
| } |
| return vSets; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs DSD-based decomposition of the function.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Lpk_FunCompareBoundSets( Lpk_Fun_t * p, Vec_Int_t * vBSets, int nCofDepth, unsigned uNonDecSupp, unsigned uLateArrSupp, Lpk_Res_t * pRes ) |
| { |
| int fVerbose = 0; |
| unsigned uBoundSet; |
| int i, nVarsBS, nVarsRem, Delay, Area; |
| |
| // compare the resulting boundsets |
| memset( pRes, 0, sizeof(Lpk_Res_t) ); |
| Vec_IntForEachEntry( vBSets, uBoundSet, i ) |
| { |
| if ( (uBoundSet & 0xFFFF) == 0 ) // skip empty boundset |
| continue; |
| if ( (uBoundSet & uNonDecSupp) == 0 ) // skip those boundsets that are not in the domain of interest |
| continue; |
| if ( (uBoundSet & uLateArrSupp) ) // skip those boundsets that are late arriving |
| continue; |
| if ( fVerbose ) |
| { |
| Lpk_PrintSetOne( uBoundSet & 0xFFFF ); |
| //printf( "\n" ); |
| //Lpk_PrintSetOne( uBoundSet >> 16 ); |
| //printf( "\n" ); |
| } |
| assert( (uBoundSet & (uBoundSet >> 16)) == 0 ); |
| nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF ); |
| if ( nVarsBS == 1 ) |
| continue; |
| assert( nVarsBS <= (int)p->nLutK - nCofDepth ); |
| nVarsRem = p->nVars - nVarsBS + 1; |
| Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK ); |
| Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays ); |
| if ( fVerbose ) |
| printf( "area = %d limit = %d delay = %d limit = %d\n", Area, (int)p->nAreaLim, Delay, (int)p->nDelayLim ); |
| if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim ) |
| continue; |
| if ( pRes->BSVars == 0 || pRes->nSuppSizeL > nVarsRem || (pRes->nSuppSizeL == nVarsRem && pRes->DelayEst > Delay) ) |
| { |
| pRes->nBSVars = nVarsBS; |
| pRes->BSVars = (uBoundSet & 0xFFFF); |
| pRes->nSuppSizeS = nVarsBS + nCofDepth; |
| pRes->nSuppSizeL = nVarsRem; |
| pRes->DelayEst = Delay; |
| pRes->AreaEst = Area; |
| } |
| } |
| if ( fVerbose ) |
| { |
| if ( pRes->BSVars ) |
| { |
| printf( "Found bound set " ); |
| Lpk_PrintSetOne( pRes->BSVars ); |
| printf( "\n" ); |
| } |
| else |
| printf( "Did not find boundsets.\n" ); |
| printf( "\n" ); |
| } |
| if ( pRes->BSVars ) |
| { |
| assert( pRes->DelayEst <= (int)p->nDelayLim ); |
| assert( pRes->AreaEst <= (int)p->nAreaLim ); |
| } |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Finds late arriving inputs, which cannot be in the bound set.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned Lpk_DsdLateArriving( Lpk_Fun_t * p ) |
| { |
| unsigned i, uLateArrSupp = 0; |
| Lpk_SuppForEachVar( p->uSupp, i ) |
| if ( p->pDelays[i] > (int)p->nDelayLim - 2 ) |
| uLateArrSupp |= (1 << i); |
| return uLateArrSupp; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs DSD-based decomposition of the function.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Lpk_DsdAnalizeOne( Lpk_Fun_t * p, unsigned * ppTruths[5][16], Kit_DsdNtk_t * pNtks[], char pCofVars[], int nCofDepth, Lpk_Res_t * pRes ) |
| { |
| int fVerbose = 0; |
| Vec_Int_t * pvBSets[4][8]; |
| unsigned uNonDecSupp, uLateArrSupp; |
| int i, k, nNonDecSize, nNonDecSizeMax; |
| assert( nCofDepth >= 1 && nCofDepth <= 3 ); |
| assert( nCofDepth < (int)p->nLutK - 1 ); |
| assert( p->fSupports ); |
| |
| // find the support of the largest non-DSD block |
| nNonDecSizeMax = 0; |
| uNonDecSupp = p->uSupp; |
| for ( i = 0; i < (1<<(nCofDepth-1)); i++ ) |
| { |
| nNonDecSize = Kit_DsdNonDsdSizeMax( pNtks[i] ); |
| if ( nNonDecSizeMax < nNonDecSize ) |
| { |
| nNonDecSizeMax = nNonDecSize; |
| uNonDecSupp = Kit_DsdNonDsdSupports( pNtks[i] ); |
| } |
| else if ( nNonDecSizeMax == nNonDecSize ) |
| uNonDecSupp |= Kit_DsdNonDsdSupports( pNtks[i] ); |
| } |
| |
| // remove those variables that cannot be used because of delay constraints |
| // if variables arrival time is more than p->DelayLim - 2, it cannot be used |
| uLateArrSupp = Lpk_DsdLateArriving( p ); |
| if ( (uNonDecSupp & ~uLateArrSupp) == 0 ) |
| { |
| memset( pRes, 0, sizeof(Lpk_Res_t) ); |
| return 0; |
| } |
| |
| // find the next cofactoring variable |
| pCofVars[nCofDepth-1] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[nCofDepth-1], 1<<(nCofDepth-1), ppTruths[nCofDepth], uNonDecSupp & ~uLateArrSupp ); |
| |
| // derive decomposed networks |
| for ( i = 0; i < (1<<nCofDepth); i++ ) |
| { |
| if ( pNtks[i] ) |
| Kit_DsdNtkFree( pNtks[i] ); |
| pNtks[i] = Kit_DsdDecomposeExpand( ppTruths[nCofDepth][i], p->nVars ); |
| if ( fVerbose ) |
| Kit_DsdPrint( stdout, pNtks[i] ); |
| pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtks[i], p->nLutK - nCofDepth ); // try restricting to those in uNonDecSupp!!! |
| } |
| |
| // 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], p->nLutK - nCofDepth ); |
| // compare bound-sets |
| Lpk_FunCompareBoundSets( p, pvBSets[0][0], nCofDepth, uNonDecSupp, uLateArrSupp, pRes ); |
| // free the bound sets |
| for ( i = nCofDepth; i >= 0; i-- ) |
| for ( k = 0; k < (1<<i); k++ ) |
| Vec_IntFree( pvBSets[i][k] ); |
| |
| // copy the cofactoring variables |
| if ( pRes->BSVars ) |
| { |
| pRes->nCofVars = nCofDepth; |
| for ( i = 0; i < nCofDepth; i++ ) |
| pRes->pCofVars[i] = pCofVars[i]; |
| } |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs DSD-based decomposition of the function.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Lpk_Res_t * Lpk_DsdAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p, int nShared ) |
| { |
| static Lpk_Res_t Res0, * pRes0 = &Res0; |
| static Lpk_Res_t Res1, * pRes1 = &Res1; |
| static Lpk_Res_t Res2, * pRes2 = &Res2; |
| static Lpk_Res_t Res3, * pRes3 = &Res3; |
| int fUseBackLooking = 1; |
| Lpk_Res_t * pRes = NULL; |
| Vec_Int_t * vBSets; |
| Kit_DsdNtk_t * pNtks[8] = {NULL}; |
| char pCofVars[5]; |
| int i; |
| |
| assert( p->nLutK >= 3 ); |
| assert( nShared >= 0 && nShared <= 3 ); |
| assert( p->uSupp == Kit_BitMask(p->nVars) ); |
| |
| // try decomposition without cofactoring |
| pNtks[0] = Kit_DsdDecomposeExpand( Lpk_FunTruth( p, 0 ), p->nVars ); |
| if ( pMan->pPars->fVerbose ) |
| pMan->nBlocks[ Kit_DsdNonDsdSizeMax(pNtks[0]) ]++; |
| vBSets = Lpk_ComputeBoundSets( pNtks[0], p->nLutK ); |
| Lpk_FunCompareBoundSets( p, vBSets, 0, 0xFFFF, Lpk_DsdLateArriving(p), pRes0 ); |
| Vec_IntFree( vBSets ); |
| |
| // check the result |
| if ( pRes0->nBSVars == (int)p->nLutK ) |
| { pRes = pRes0; goto finish; } |
| if ( pRes0->nBSVars == (int)p->nLutK - 1 ) |
| { pRes = pRes0; goto finish; } |
| if ( nShared == 0 ) |
| goto finish; |
| |
| // prepare storage |
| Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth( p, 0 ), p->nVars ); |
| |
| // cofactor 1 time |
| if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 1, pRes1 ) ) |
| goto finish; |
| assert( pRes1->nBSVars <= (int)p->nLutK - 1 ); |
| if ( pRes1->nBSVars == (int)p->nLutK - 1 ) |
| { pRes = pRes1; goto finish; } |
| if ( pRes0->nBSVars == (int)p->nLutK - 2 ) |
| { pRes = pRes0; goto finish; } |
| if ( pRes1->nBSVars == (int)p->nLutK - 2 ) |
| { pRes = pRes1; goto finish; } |
| if ( nShared == 1 ) |
| goto finish; |
| |
| // cofactor 2 times |
| if ( p->nLutK >= 4 ) |
| { |
| if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 2, pRes2 ) ) |
| goto finish; |
| assert( pRes2->nBSVars <= (int)p->nLutK - 2 ); |
| if ( pRes2->nBSVars == (int)p->nLutK - 2 ) |
| { pRes = pRes2; goto finish; } |
| if ( fUseBackLooking ) |
| { |
| if ( pRes0->nBSVars == (int)p->nLutK - 3 ) |
| { pRes = pRes0; goto finish; } |
| if ( pRes1->nBSVars == (int)p->nLutK - 3 ) |
| { pRes = pRes1; goto finish; } |
| } |
| if ( pRes2->nBSVars == (int)p->nLutK - 3 ) |
| { pRes = pRes2; goto finish; } |
| if ( nShared == 2 ) |
| goto finish; |
| assert( nShared == 3 ); |
| } |
| |
| // cofactor 3 times |
| if ( p->nLutK >= 5 ) |
| { |
| if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 3, pRes3 ) ) |
| goto finish; |
| assert( pRes3->nBSVars <= (int)p->nLutK - 3 ); |
| if ( pRes3->nBSVars == (int)p->nLutK - 3 ) |
| { pRes = pRes3; goto finish; } |
| if ( fUseBackLooking ) |
| { |
| if ( pRes0->nBSVars == (int)p->nLutK - 4 ) |
| { pRes = pRes0; goto finish; } |
| if ( pRes1->nBSVars == (int)p->nLutK - 4 ) |
| { pRes = pRes1; goto finish; } |
| if ( pRes2->nBSVars == (int)p->nLutK - 4 ) |
| { pRes = pRes2; goto finish; } |
| } |
| if ( pRes3->nBSVars == (int)p->nLutK - 4 ) |
| { pRes = pRes3; goto finish; } |
| } |
| |
| finish: |
| // free the networks |
| for ( i = 0; i < (1<<nShared); i++ ) |
| if ( pNtks[i] ) |
| Kit_DsdNtkFree( pNtks[i] ); |
| // choose the best under these conditions |
| return pRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Splits the function into two subfunctions using DSD.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Lpk_Fun_t * Lpk_DsdSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet ) |
| { |
| Lpk_Fun_t * pNew; |
| Kit_DsdNtk_t * pNtkDec; |
| int i, k, iVacVar, nCofs; |
| // prepare storage |
| Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth(p, 0), p->nVars ); |
| // get the vacuous variable |
| iVacVar = Kit_WordFindFirstBit( uBoundSet ); |
| // compute the cofactors |
| for ( i = 0; i < nCofVars; i++ ) |
| for ( k = 0; k < (1<<i); k++ ) |
| { |
| Kit_TruthCofactor0New( pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i][k], p->nVars, pCofVars[i] ); |
| Kit_TruthCofactor1New( pMan->ppTruths[i+1][2*k+1], pMan->ppTruths[i][k], p->nVars, pCofVars[i] ); |
| } |
| // decompose each cofactor w.r.t. the bound set |
| nCofs = (1<<nCofVars); |
| for ( k = 0; k < nCofs; k++ ) |
| { |
| pNtkDec = Kit_DsdDecomposeExpand( pMan->ppTruths[nCofVars][k], p->nVars ); |
| Kit_DsdTruthPartialTwo( pMan->pDsdMan, pNtkDec, uBoundSet, iVacVar, pMan->ppTruths[nCofVars+1][k], pMan->ppTruths[nCofVars+1][nCofs+k] ); |
| Kit_DsdNtkFree( pNtkDec ); |
| } |
| // compute the composition/decomposition functions (they will be in pMan->ppTruths[1][0]/pMan->ppTruths[1][1]) |
| for ( i = nCofVars; i >= 1; i-- ) |
| for ( k = 0; k < (1<<i); k++ ) |
| Kit_TruthMuxVar( pMan->ppTruths[i][k], pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i+1][2*k+1], p->nVars, pCofVars[i-1] ); |
| |
| // derive the new component (decomposition function) |
| pNew = Lpk_FunDup( p, pMan->ppTruths[1][1] ); |
| // update the old component (composition function) |
| Kit_TruthCopy( Lpk_FunTruth(p, 0), pMan->ppTruths[1][0], p->nVars ); |
| p->uSupp = Kit_TruthSupport( Lpk_FunTruth(p, 0), p->nVars ); |
| p->pFanins[iVacVar] = pNew->Id; |
| p->pDelays[iVacVar] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays ); |
| // support minimize both |
| p->fSupports = 0; |
| Lpk_FunSuppMinimize( p ); |
| Lpk_FunSuppMinimize( pNew ); |
| // update delay and area requirements |
| pNew->nDelayLim = p->pDelays[iVacVar]; |
| pNew->nAreaLim = 1; |
| p->nAreaLim = p->nAreaLim - 1; |
| return pNew; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
