Version abc71001

1 files changed, 551 insertions, 0 deletions

diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
new file mode 100644
index 00000000..c00a7d7c
--- /dev/null
+++ b/src/base/abci/abcDsd.c
@@ -0,0 +1,551 @@
+/**CFile****************************************************************
+
+  FileName    [abcDsd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Decomposes the network using disjoint-support decomposition.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dsd.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+static Abc_Ntk_t *     Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
+static void            Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t *     Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew, int * pCounters );
+
+static Vec_Ptr_t *     Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk );
+static void            Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd, bool fRecursive, int * pCounters );
+static bool            Abc_NodeIsForDsd( Abc_Obj_t * pNode );
+static int             Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the DSD network.]
+
+  Description [Takes the strashed network (pNtk), derives global BDDs for
+  the combinational outputs of this network, and decomposes these BDDs using
+  disjoint support decomposition. Finally, constructs and return a new 
+  network, which is topologically equivalent to the decomposition tree.
+  Allocates and frees a new BDD manager and a new DSD manager.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
+{
+    DdManager * dd;
+    Abc_Ntk_t * pNtkNew;
+    assert( Abc_NtkIsStrash(pNtk) );
+    dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
+    if ( dd == NULL )
+        return NULL;
+    if ( fVerbose )
+        printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+    // transform the result of mapping into a BDD network
+    pNtkNew = Abc_NtkDsdInternal( pNtk, fVerbose, fPrint, fShort );
+    Extra_StopManager( dd );
+    if ( pNtkNew == NULL )
+        return NULL;
+    // copy EXDC network
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkDsdGlobal: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
+{
+    char ** ppNamesCi, ** ppNamesCo;
+    Vec_Ptr_t * vFuncsGlob;
+    Dsd_Manager_t * pManDsd;
+    Abc_Ntk_t * pNtkNew;
+    DdManager * dd;
+    Abc_Obj_t * pObj;
+    int i;
+
+    // complement the global functions
+    vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Vec_PtrPush( vFuncsGlob, Cudd_NotCond(Abc_ObjGlobalBdd(pObj), Abc_ObjFaninC0(pObj)) );
+
+    // perform the decomposition
+    dd = Abc_NtkGlobalBddMan(pNtk);
+    pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
+    Dsd_Decompose( pManDsd, (DdNode **)vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) );
+    Vec_PtrFree( vFuncsGlob );
+    Abc_NtkFreeGlobalBdds( pNtk, 0 );
+    if ( pManDsd == NULL )
+    {
+        Cudd_Quit( dd );
+        return NULL;
+    }
+
+    // start the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    // make sure the new manager has enough inputs
+    Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 );
+    // put the results into the new network (save new CO drivers in old CO drivers)
+    Abc_NtkDsdConstruct( pManDsd, pNtk, pNtkNew );
+    // finalize the new network
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
+    if ( fPrint )
+    {
+        ppNamesCi = Abc_NtkCollectCioNames( pNtk, 0 );
+        ppNamesCo = Abc_NtkCollectCioNames( pNtk, 1 );
+        Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1 );
+        free( ppNamesCi );
+        free( ppNamesCo );
+    }
+
+    // stop the DSD manager
+    Dsd_ManagerStop( pManDsd );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+{
+    Dsd_Node_t ** ppNodesDsd;
+    Dsd_Node_t * pNodeDsd;
+    Abc_Obj_t * pNode, * pNodeNew, * pDriver;
+    int i, nNodesDsd;
+
+    // save the CI nodes in the DSD nodes
+    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NtkCreateNodeConst1(pNtkNew) );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+    {
+        pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
+        Dsd_NodeSetMark( pNodeDsd, (int)pNode->pCopy );
+    }
+
+    // collect DSD nodes in DFS order (leaves and const1 are not collected)
+    ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd );
+    for ( i = 0; i < nNodesDsd; i++ )
+        Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNtkNew, NULL );
+    free( ppNodesDsd );
+
+    // set the pointers to the CO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pDriver = Abc_ObjFanin0( pNode );
+        if ( !Abc_ObjIsNode(pDriver) )
+            continue;
+        if ( !Abc_AigNodeIsAnd(pDriver) )
+            continue;
+        pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
+        pNodeNew = (Abc_Obj_t *)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
+        assert( !Abc_ObjIsComplement(pNodeNew) );
+        pDriver->pCopy = Abc_ObjNotCond( pNodeNew, Dsd_IsComplement(pNodeDsd) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DSD using the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew, int * pCounters )
+{
+    DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd );
+    DdManager * ddNew = pNtkNew->pManFunc;
+    Dsd_Node_t * pFaninDsd;
+    Abc_Obj_t * pNodeNew, * pFanin;
+    DdNode * bLocal, * bTemp, * bVar;
+    Dsd_Type_t Type;
+    int i, nDecs;
+
+    // create the new node
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    // add the fanins
+    Type  = Dsd_NodeReadType( pNodeDsd );
+    nDecs = Dsd_NodeReadDecsNum( pNodeDsd );
+    assert( nDecs > 1 );
+    for ( i = 0; i < nDecs; i++ )
+    {
+        pFaninDsd  = Dsd_NodeReadDec( pNodeDsd, i );
+        pFanin     = (Abc_Obj_t *)Dsd_NodeReadMark(Dsd_Regular(pFaninDsd));
+        Abc_ObjAddFanin( pNodeNew, pFanin );
+        assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) );
+    }
+
+    // create the local function depending on the type of the node
+    ddNew = pNtkNew->pManFunc;
+    switch ( Type )
+    {
+        case DSD_NODE_CONST1:
+        {
+            bLocal = ddNew->one; Cudd_Ref( bLocal );
+            break;
+        }
+        case DSD_NODE_OR:
+        {
+            bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal );
+            for ( i = 0; i < nDecs; i++ )
+            {
+                pFaninDsd  = Dsd_NodeReadDec( pNodeDsd, i );
+                bVar   = Cudd_NotCond( ddNew->vars[i], Dsd_IsComplement(pFaninDsd) );
+                bLocal = Cudd_bddOr( ddNew, bTemp = bLocal, bVar );               Cudd_Ref( bLocal );
+                Cudd_RecursiveDeref( ddNew, bTemp );
+            }
+            break;
+        }
+        case DSD_NODE_EXOR:
+        {
+            bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal );
+            for ( i = 0; i < nDecs; i++ )
+            {
+                bLocal = Cudd_bddXor( ddNew, bTemp = bLocal, ddNew->vars[i] );    Cudd_Ref( bLocal );
+                Cudd_RecursiveDeref( ddNew, bTemp );
+            }
+            break;
+        }
+        case DSD_NODE_PRIME:
+        {
+            if ( pCounters )
+            {
+                if ( nDecs < 10 )
+                    pCounters[nDecs]++;
+                else
+                    pCounters[10]++;
+            }
+            bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd );                Cudd_Ref( bLocal );
+            bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal );
+/*
+if ( nDecs == 3 )
+{
+Extra_bddPrint( ddDsd, bTemp );
+printf( "\n" );
+}
+*/
+            Cudd_RecursiveDeref( ddDsd, bTemp );
+            // bLocal is now in the new BDD manager
+            break;
+        }
+        default:
+        {
+            assert( 0 );
+            break;
+        }
+    }
+    pNodeNew->pData = bLocal;
+    Dsd_NodeSetMark( pNodeDsd, (int)pNodeNew );
+    return pNodeNew;
+}
+
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively decomposes internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive )
+{
+    Dsd_Manager_t * pManDsd;
+    DdManager * dd = pNtk->pManFunc;
+    Vec_Ptr_t * vNodes;
+    int i;
+    int pCounters[11] = {0};
+
+    assert( Abc_NtkIsBddLogic(pNtk) );
+
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtk );
+
+    // start the DSD manager
+    pManDsd = Dsd_ManagerStart( dd, dd->size, 0 );
+
+    // collect nodes for decomposition
+    vNodes = Abc_NtkCollectNodesForDsd( pNtk );
+    for ( i = 0; i < vNodes->nSize; i++ )
+        Abc_NodeDecompDsdAndMux( vNodes->pArray[i], vNodes, pManDsd, fRecursive, pCounters );
+    Vec_PtrFree( vNodes );
+
+    printf( "Number of non-decomposable functions:\n" );
+    for ( i = 3; i < 10; i++ )
+        printf( "Inputs = %d.  Functions = %6d.\n", i, pCounters[i] );
+    printf( "Inputs > %d.  Functions = %6d.\n", 9, pCounters[10] );
+
+    // stop the DSD manager
+    Dsd_ManagerStop( pManDsd );
+
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkDsdRecursive: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes that may need decomposition.]
+
+  Description [The nodes that do not need decomposition are those
+  whose BDD has more internal nodes than the support size.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode;
+    int i;
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_NodeIsForDsd(pNode) )
+            Vec_PtrPush( vNodes, pNode );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd, bool fRecursive, int * pCounters )
+{
+    DdManager * dd = pNode->pNtk->pManFunc;
+    Abc_Obj_t * pRoot, * pFanin, * pNode1, * pNode2, * pNodeC;
+    Dsd_Node_t ** ppNodesDsd, * pNodeDsd, * pFaninDsd;
+    int i, nNodesDsd, iVar, fCompl;
+
+    // try disjoint support decomposition
+    pNodeDsd = Dsd_DecomposeOne( pManDsd, pNode->pData );
+    fCompl   = Dsd_IsComplement( pNodeDsd );
+    pNodeDsd = Dsd_Regular( pNodeDsd );
+
+    // determine what decomposition to use   
+    if ( !fRecursive || Dsd_NodeReadDecsNum(pNodeDsd) != Abc_ObjFaninNum(pNode) )
+    { // perform DSD
+
+        // set the inputs
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            pFaninDsd = Dsd_ManagerReadInput( pManDsd, i );
+            Dsd_NodeSetMark( pFaninDsd, (int)pFanin );
+        }
+
+        // construct the intermediate nodes
+        ppNodesDsd = Dsd_TreeCollectNodesDfsOne( pManDsd, pNodeDsd, &nNodesDsd );
+        for ( i = 0; i < nNodesDsd; i++ )
+        {
+            pRoot = Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNode->pNtk, pCounters );
+            if ( Abc_NodeIsForDsd(pRoot) && fRecursive )
+                Vec_PtrPush( vNodes, pRoot );
+        }
+        free( ppNodesDsd );
+
+        // remove the current fanins
+        Abc_ObjRemoveFanins( pNode );
+        // add fanin to the root
+        Abc_ObjAddFanin( pNode, pRoot );
+        // update the function to be that of buffer
+        Cudd_RecursiveDeref( dd, pNode->pData );
+        pNode->pData = Cudd_NotCond( dd->vars[0], fCompl ); Cudd_Ref( pNode->pData );
+    }
+    else // perform MUX-decomposition
+    {
+        // get the cofactoring variable
+        iVar = Abc_NodeFindMuxVar( dd, pNode->pData, Abc_ObjFaninNum(pNode) );
+        pNodeC = Abc_ObjFanin( pNode, iVar );
+
+        // get the negative cofactor
+        pNode1 = Abc_NtkCloneObj( pNode );
+        pNode1->pData = Cudd_Cofactor( dd, pNode->pData, Cudd_Not(dd->vars[iVar]) );  Cudd_Ref( pNode1->pData );
+        Abc_NodeMinimumBase( pNode1 );
+        if ( Abc_NodeIsForDsd(pNode1) )
+            Vec_PtrPush( vNodes, pNode1 );
+
+        // get the positive cofactor
+        pNode2 = Abc_NtkCloneObj( pNode );
+        pNode2->pData = Cudd_Cofactor( dd, pNode->pData, dd->vars[iVar] );            Cudd_Ref( pNode2->pData );
+        Abc_NodeMinimumBase( pNode2 );
+        if ( Abc_NodeIsForDsd(pNode2) )
+            Vec_PtrPush( vNodes, pNode2 );
+
+        // remove the current fanins
+        Abc_ObjRemoveFanins( pNode );
+        // add new fanins
+        Abc_ObjAddFanin( pNode, pNodeC );
+        Abc_ObjAddFanin( pNode, pNode2 );
+        Abc_ObjAddFanin( pNode, pNode1 );
+        // update the function to be that of MUX
+        Cudd_RecursiveDeref( dd, pNode->pData );
+        pNode->pData = Cudd_bddIte( dd, dd->vars[0], dd->vars[1], dd->vars[2] );    Cudd_Ref( pNode->pData );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the node should be decomposed by DSD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NodeIsForDsd( Abc_Obj_t * pNode )
+{
+    DdManager * dd = pNode->pNtk->pManFunc;
+//    DdNode * bFunc, * bFunc0, * bFunc1;
+    assert( Abc_ObjIsNode(pNode) );
+//    if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) )
+//        return 1;
+//    return 0;
+
+/*
+    // this does not catch things like a(b+c), which should be decomposed
+    for ( bFunc = Cudd_Regular(pNode->pData); !cuddIsConstant(bFunc); )
+    {
+        bFunc0 = Cudd_Regular( cuddE(bFunc) );
+        bFunc1 = cuddT(bFunc);
+        if ( bFunc0 == b1 )
+            bFunc = bFunc1;
+        else if ( bFunc1 == b1 || bFunc0 == bFunc1 )
+            bFunc = bFunc0;
+        else
+            return 1;
+    }
+*/
+    if ( Abc_ObjFaninNum(pNode) > 2 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determines a cofactoring variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars )
+{
+    DdNode * bVar, * bCof0, * bCof1;
+    int SuppSumMin = 1000000;
+    int i, nSSD, nSSQ, iVar;
+
+//    printf( "\n\nCofactors:\n\n" );
+    iVar = -1;
+    for ( i = 0; i < nVars; i++ )
+    {
+        bVar = dd->vars[i];
+
+        bCof0 = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) );  Cudd_Ref( bCof0 );
+        bCof1 = Cudd_Cofactor( dd, bFunc,          bVar  );  Cudd_Ref( bCof1 );
+
+//        nodD = Cudd_DagSize(bCof0);
+//        nodQ = Cudd_DagSize(bCof1);
+//        printf( "+%02d: D=%2d. Q=%2d.  ", i, nodD, nodQ );
+//        printf( "S=%2d. D=%2d.  ", nodD + nodQ, abs(nodD-nodQ) );
+
+        nSSD = Cudd_SupportSize( dd, bCof0 );
+        nSSQ = Cudd_SupportSize( dd, bCof1 );
+
+//        printf( "SD=%2d. SQ=%2d.  ", nSSD, nSSQ );
+//        printf( "S=%2d. D=%2d.  ", nSSD + nSSQ, abs(nSSD - nSSQ) );
+//        printf( "Cost=%3d. ", Cost(nodD,nodQ,nSSD,nSSQ) );
+//        printf( "\n" );
+
+        Cudd_RecursiveDeref( dd, bCof0 );
+        Cudd_RecursiveDeref( dd, bCof1 );
+
+        if ( SuppSumMin > nSSD + nSSQ )
+        {
+             SuppSumMin = nSSD + nSSQ;
+             iVar = i;
+        }
+    }
+    return iVar;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+