Version abc70831

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