Version abc80130_2

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                                ///
+////////////////////////////////////////////////////////////////////////
+
+