| /**CFile**************************************************************** |
| |
| FileName [lpkSets.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: lpkSets.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "lpkInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| typedef struct Lpk_Set_t_ Lpk_Set_t; |
| struct Lpk_Set_t_ |
| { |
| char iVar; // the cofactoring variable |
| char Over; // the overlap in supports |
| char SRed; // the support reduction |
| char Size; // the size of the boundset |
| unsigned uSubset0; // the first subset (with removed) |
| unsigned uSubset1; // the second subset (with removed) |
| }; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Recursively computes decomposable subsets.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned Lpk_ComputeSets_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, 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_ComputeSets_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_ComputeSets_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 [] |
| |
| ***********************************************************************/ |
| unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets ) |
| { |
| unsigned uSupport, Entry; |
| int Number, i; |
| assert( p->nVars <= 16 ); |
| Vec_IntClear( vSets ); |
| Vec_IntPush( vSets, 0 ); |
| if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 ) |
| return 0; |
| if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR ) |
| { |
| uSupport = ( 1 << Abc_Lit2Var(Kit_DsdNtkRoot(p)->pFans[0]) ); |
| Vec_IntPush( vSets, uSupport ); |
| return uSupport; |
| } |
| uSupport = Lpk_ComputeSets_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 uSupport; |
| } |
| |
| /**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 [Computes maximal support reducing bound-sets.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCofVar, |
| Lpk_Set_t * pStore, int * pSize, int nSizeLimit ) |
| { |
| static int nTravId = 0; // the number of the times this is visited |
| static int TravId[1<<16] = {0}; // last visited |
| static char SRed[1<<16]; // best support reduction |
| static char Over[1<<16]; // best overlaps |
| static unsigned Parents[1<<16]; // best set of parents |
| static unsigned short Used[1<<16]; // storage for used subsets |
| int nSuppSize, nSuppOver, nSuppRed, nUsed, nMinOver, i, k, s; |
| unsigned Entry, Entry0, Entry1; |
| unsigned uSupp, uSupp0, uSupp1, uSuppTotal; |
| Lpk_Set_t * pEntry; |
| |
| if ( nTravId == (1 << 30) ) |
| memset( TravId, 0, sizeof(int) * (1 << 16) ); |
| |
| // collect support reducing subsets |
| nUsed = 0; |
| nTravId++; |
| uSuppTotal = Kit_BitMask(nVars) & ~(1<<iCofVar); |
| Vec_IntForEachEntry( vSets0, Entry0, i ) |
| Vec_IntForEachEntry( vSets1, Entry1, k ) |
| { |
| uSupp0 = (Entry0 & 0xFFFF); |
| uSupp1 = (Entry1 & 0xFFFF); |
| // skip trivial |
| if ( uSupp0 == 0 || uSupp1 == 0 || (uSupp0 | uSupp1) == uSuppTotal ) |
| continue; |
| if ( Kit_WordHasOneBit(uSupp0) && Kit_WordHasOneBit(uSupp1) ) |
| continue; |
| // get the entry |
| Entry = Entry0 | Entry1; |
| uSupp = Entry & 0xFFFF; |
| // set the bound set size |
| nSuppSize = Kit_WordCountOnes( uSupp ); |
| // get the number of overlapping vars |
| nSuppOver = Kit_WordCountOnes( Entry & (Entry >> 16) ); |
| // get the support reduction |
| nSuppRed = nSuppSize - 1 - nSuppOver; |
| // only consider support-reducing subsets |
| if ( nSuppRed <= 0 ) |
| continue; |
| // check if this support is already used |
| if ( TravId[uSupp] < nTravId ) |
| { |
| Used[nUsed++] = uSupp; |
| |
| TravId[uSupp] = nTravId; |
| SRed[uSupp] = nSuppRed; |
| Over[uSupp] = nSuppOver; |
| Parents[uSupp] = (k << 16) | i; |
| } |
| else if ( TravId[uSupp] == nTravId && SRed[uSupp] < nSuppRed ) |
| { |
| TravId[uSupp] = nTravId; |
| SRed[uSupp] = nSuppRed; |
| Over[uSupp] = nSuppOver; |
| Parents[uSupp] = (k << 16) | i; |
| } |
| } |
| |
| // find the minimum overlap |
| nMinOver = 1000; |
| for ( s = 0; s < nUsed; s++ ) |
| if ( nMinOver > Over[Used[s]] ) |
| nMinOver = Over[Used[s]]; |
| |
| |
| // collect the accumulated ones |
| for ( s = 0; s < nUsed; s++ ) |
| if ( Over[Used[s]] == nMinOver ) |
| { |
| // save the entry |
| if ( *pSize == nSizeLimit ) |
| return; |
| pEntry = pStore + (*pSize)++; |
| |
| i = Parents[Used[s]] & 0xFFFF; |
| k = Parents[Used[s]] >> 16; |
| |
| pEntry->uSubset0 = Vec_IntEntry(vSets0, i); |
| pEntry->uSubset1 = Vec_IntEntry(vSets1, k); |
| Entry = pEntry->uSubset0 | pEntry->uSubset1; |
| |
| // record the cofactoring variable |
| pEntry->iVar = iCofVar; |
| // set the bound set size |
| pEntry->Size = Kit_WordCountOnes( Entry & 0xFFFF ); |
| // get the number of overlapping vars |
| pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) ); |
| // get the support reduction |
| pEntry->SRed = pEntry->Size - 1 - pEntry->Over; |
| assert( pEntry->SRed > 0 ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Prints one set.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Lpk_MapSuppPrintSet( Lpk_Set_t * pSet, int i ) |
| { |
| unsigned Entry; |
| Entry = pSet->uSubset0 | pSet->uSubset1; |
| printf( "%2d : ", i ); |
| printf( "Var = %c ", 'a' + pSet->iVar ); |
| printf( "Size = %2d ", pSet->Size ); |
| printf( "Over = %2d ", pSet->Over ); |
| printf( "SRed = %2d ", pSet->SRed ); |
| Lpk_PrintSetOne( Entry ); |
| printf( " " ); |
| Lpk_PrintSetOne( Entry >> 16 ); |
| printf( "\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Evaluates the cofactors.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused ) |
| { |
| static int nStoreSize = 256; |
| static Lpk_Set_t pStore[256], * pSet, * pSetBest; |
| Kit_DsdNtk_t * ppNtks[2], * pTemp; |
| Vec_Int_t * vSets0 = p->vSets[0]; |
| Vec_Int_t * vSets1 = p->vSets[1]; |
| unsigned * pCof0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 0 ); |
| unsigned * pCof1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 1 ); |
| int nSets, i, SizeMax;//, SRedMax; |
| unsigned Entry; |
| int fVerbose = p->pPars->fVeryVerbose; |
| // int fVerbose = 0; |
| |
| // collect decomposable subsets for each pair of cofactors |
| if ( fVerbose ) |
| { |
| printf( "\nExploring support-reducing bound-sets of function:\n" ); |
| Kit_DsdPrintFromTruth( pTruth, nVars ); |
| } |
| nSets = 0; |
| for ( i = 0; i < nVars; i++ ) |
| { |
| if ( fVerbose ) |
| printf( "Evaluating variable %c:\n", 'a'+i ); |
| // evaluate the cofactor pair |
| Kit_TruthCofactor0New( pCof0, pTruth, nVars, i ); |
| Kit_TruthCofactor1New( pCof1, pTruth, nVars, i ); |
| // decompose and expand |
| ppNtks[0] = Kit_DsdDecompose( pCof0, nVars ); |
| ppNtks[1] = Kit_DsdDecompose( pCof1, nVars ); |
| ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp ); |
| ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp ); |
| if ( fVerbose ) |
| Kit_DsdPrint( stdout, ppNtks[0] ); |
| if ( fVerbose ) |
| Kit_DsdPrint( stdout, ppNtks[1] ); |
| // compute subsets |
| Lpk_ComputeSets( ppNtks[0], vSets0 ); |
| Lpk_ComputeSets( ppNtks[1], vSets1 ); |
| // print subsets |
| if ( fVerbose ) |
| Lpk_PrintSets( vSets0 ); |
| if ( fVerbose ) |
| Lpk_PrintSets( vSets1 ); |
| // free the networks |
| Kit_DsdNtkFree( ppNtks[0] ); |
| Kit_DsdNtkFree( ppNtks[1] ); |
| // evaluate the pair |
| Lpk_ComposeSets( vSets0, vSets1, nVars, i, pStore, &nSets, nStoreSize ); |
| } |
| |
| // print the results |
| if ( fVerbose ) |
| printf( "\n" ); |
| if ( fVerbose ) |
| for ( i = 0; i < nSets; i++ ) |
| Lpk_MapSuppPrintSet( pStore + i, i ); |
| |
| // choose the best subset |
| SizeMax = 0; |
| pSetBest = NULL; |
| for ( i = 0; i < nSets; i++ ) |
| { |
| pSet = pStore + i; |
| if ( pSet->Size > p->pPars->nLutSize - 1 ) |
| continue; |
| if ( SizeMax < pSet->Size ) |
| { |
| pSetBest = pSet; |
| SizeMax = pSet->Size; |
| } |
| } |
| /* |
| // if the best is not choosen, select the one with largest reduction |
| SRedMax = 0; |
| if ( pSetBest == NULL ) |
| { |
| for ( i = 0; i < nSets; i++ ) |
| { |
| pSet = pStore + i; |
| if ( SRedMax < pSet->SRed ) |
| { |
| pSetBest = pSet; |
| SRedMax = pSet->SRed; |
| } |
| } |
| } |
| */ |
| if ( pSetBest == NULL ) |
| { |
| if ( fVerbose ) |
| printf( "Could not select a subset.\n" ); |
| return 0; |
| } |
| else |
| { |
| if ( fVerbose ) |
| printf( "Selected the following subset:\n" ); |
| if ( fVerbose ) |
| Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore ); |
| } |
| |
| // prepare the return result |
| // get the remaining variables |
| Entry = ((pSetBest->uSubset0 >> 16) | (pSetBest->uSubset1 >> 16)); |
| // get the variables to be removed |
| Entry = Kit_BitMask(nVars) & ~(1<<pSetBest->iVar) & ~Entry; |
| // make sure there are some - otherwise it is not supp-red |
| assert( Entry ); |
| // remember the first such variable |
| *piVarReused = Kit_WordFindFirstBit( Entry ); |
| *piVar = pSetBest->iVar; |
| return (pSetBest->uSubset1 << 16) | (pSetBest->uSubset0 & 0xFFFF); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
