summaryrefslogtreecommitdiffstats
path: root/src/opt/lpk/lpkSets.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/lpk/lpkSets.c')
-rw-r--r--src/opt/lpk/lpkSets.c440
1 files changed, 440 insertions, 0 deletions
diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c
new file mode 100644
index 00000000..90e46863
--- /dev/null
+++ b/src/opt/lpk/lpkSets.c
@@ -0,0 +1,440 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+/// 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, 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_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 << Kit_DsdLit2Var(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 = Vec_PtrEntry( p->vTtNodes, 0 );
+ unsigned * pCof1 = 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 ///
+////////////////////////////////////////////////////////////////////////
+
+