Version abc71001

1 files changed, 582 insertions, 0 deletions

diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
new file mode 100644
index 00000000..f127811e
--- /dev/null
+++ b/src/base/abci/abcNtbdd.c
@@ -0,0 +1,582 @@
+/**CFile****************************************************************
+
+  FileName    [abcNtbdd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Procedures to translate between the BDD and the network.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcNtbdd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void        Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node );
+static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the network isomorphic to the given BDD.]
+
+  Description [Assumes that the BDD depends on the variables whose indexes
+  correspond to the names in the array (pNamesPi). Otherwise, returns NULL.
+  The resulting network comes with one node, whose functionality is
+  equal to the given BDD. To decompose this BDD into the network of
+  multiplexers use Abc_NtkBddToMuxes(). To decompose this BDD into
+  an And-Inverter Graph, use Abc_NtkStrash().]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi )
+{
+    Abc_Ntk_t * pNtk; 
+    Vec_Ptr_t * vNamesPiFake = NULL;
+    Abc_Obj_t * pNode, * pNodePi, * pNodePo;
+    DdNode * bSupp, * bTemp;
+    char * pName;
+    int i;
+
+    // supply fake names if real names are not given
+    if ( pNamePo == NULL )
+        pNamePo = "F";
+    if ( vNamesPi == NULL )
+    {
+        vNamesPiFake = Abc_NodeGetFakeNames( dd->size );
+        vNamesPi = vNamesPiFake;
+    }
+
+    // make sure BDD depends on the variables whose index 
+    // does not exceed the size of the array with PI names
+    bSupp = Cudd_Support( dd, bFunc );   Cudd_Ref( bSupp );
+    for ( bTemp = bSupp; bTemp != Cudd_ReadOne(dd); bTemp = cuddT(bTemp) )
+        if ( (int)Cudd_NodeReadIndex(bTemp) >= Vec_PtrSize(vNamesPi) )
+            break;
+    Cudd_RecursiveDeref( dd, bSupp );
+    if ( bTemp != Cudd_ReadOne(dd) )
+        return NULL;
+
+    // start the network
+    pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
+    pNtk->pName = Extra_UtilStrsav(pNamePo);
+    // make sure the new manager has enough inputs
+    Cudd_bddIthVar( pNtk->pManFunc, Vec_PtrSize(vNamesPi) );
+    // add the PIs corresponding to the names
+    Vec_PtrForEachEntry( vNamesPi, pName, i )
+        Abc_ObjAssignName( Abc_NtkCreatePi(pNtk), pName, NULL );
+    // create the node
+    pNode = Abc_NtkCreateNode( pNtk );
+    pNode->pData = Cudd_bddTransfer( dd, pNtk->pManFunc, bFunc ); Cudd_Ref(pNode->pData);
+    Abc_NtkForEachPi( pNtk, pNodePi, i )
+        Abc_ObjAddFanin( pNode, pNodePi );
+    // create the only PO
+    pNodePo = Abc_NtkCreatePo( pNtk );
+    Abc_ObjAddFanin( pNodePo, pNode );
+    Abc_ObjAssignName( pNodePo, pNamePo, NULL );
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtk );
+    if ( vNamesPiFake )
+        Abc_NodeFreeNames( vNamesPiFake );
+    if ( !Abc_NtkCheck( pNtk ) )
+        fprintf( stdout, "Abc_NtkDeriveFromBdd(): Network check has failed.\n" );
+    return pNtk;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the network isomorphic to the union of local BDDs of the nodes.]
+
+  Description [The nodes of the local BDDs are converted into the network nodes 
+  with logic functions equal to the MUX.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew;
+    assert( Abc_NtkIsBddLogic(pNtk) );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    Abc_NtkBddToMuxesPerform( pNtk, pNtkNew );
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkBddToMuxes: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network to MUXes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+{
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode, * pNodeNew;
+    Vec_Ptr_t * vNodes;
+    int i;
+    // perform conversion in the topological order
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // convert one node
+        assert( Abc_ObjIsNode(pNode) );
+        pNodeNew = Abc_NodeBddToMuxes( pNode, pNtkNew );
+        // mark the old node with the new one
+        assert( pNode->pCopy == NULL );
+        pNode->pCopy = pNodeNew;
+    }
+    Vec_PtrFree( vNodes );
+    Extra_ProgressBarStop( pProgress );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the node to MUXes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
+{
+    DdManager * dd = pNodeOld->pNtk->pManFunc;
+    DdNode * bFunc = pNodeOld->pData;
+    Abc_Obj_t * pFaninOld, * pNodeNew;
+    st_table * tBdd2Node;
+    int i;
+    // create the table mapping BDD nodes into the ABC nodes
+    tBdd2Node = st_init_table( st_ptrcmp, st_ptrhash );
+    // add the constant and the elementary vars
+    Abc_ObjForEachFanin( pNodeOld, pFaninOld, i )
+        st_insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pFaninOld->pCopy );
+    // create the new nodes recursively
+    pNodeNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node );
+    st_free_table( tBdd2Node );
+    if ( Cudd_IsComplement(bFunc) )
+        pNodeNew = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew );
+    return pNodeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the node to MUXes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node )
+{
+    Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
+    assert( !Cudd_IsComplement(bFunc) );
+    if ( bFunc == b1 )
+        return Abc_NtkCreateNodeConst1(pNtkNew);
+    if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
+        return pNodeNew;
+    // solve for the children nodes
+    pNodeNew0 = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(cuddE(bFunc)), pNtkNew, tBdd2Node );
+    if ( Cudd_IsComplement(cuddE(bFunc)) )
+        pNodeNew0 = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew0 );
+    pNodeNew1 = Abc_NodeBddToMuxes_rec( dd, cuddT(bFunc), pNtkNew, tBdd2Node );
+    if ( !st_lookup( tBdd2Node, (char *)Cudd_bddIthVar(dd, bFunc->index), (char **)&pNodeNewC ) )
+        assert( 0 );
+    // create the MUX node
+    pNodeNew = Abc_NtkCreateNodeMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 );
+    st_insert( tBdd2Node, (char *)bFunc, (char *)pNodeNew );
+    return pNodeNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives global BDDs for the COs of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdManager * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose )
+{
+    ProgressBar * pProgress;
+    Abc_Obj_t * pObj, * pFanin;
+    Vec_Att_t * pAttMan;
+    DdManager * dd;
+    DdNode * bFunc;
+    int i, k, Counter;
+
+    // remove dangling nodes
+    Abc_AigCleanup( pNtk->pManFunc );
+
+    // start the manager
+    assert( Abc_NtkGlobalBdd(pNtk) == NULL );
+    dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    pAttMan = Vec_AttAlloc( 0, Abc_NtkObjNumMax(pNtk) + 1, dd, Extra_StopManager, NULL, Cudd_RecursiveDeref );
+    Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD, pAttMan );
+
+    // set reordering
+    if ( fReorder )
+        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+
+    // assign the constant node BDD
+    pObj = Abc_AigConst1(pNtk);
+    if ( Abc_ObjFanoutNum(pObj) > 0 )
+    {
+        bFunc = dd->one;
+        Abc_ObjSetGlobalBdd( pObj, bFunc );   Cudd_Ref( bFunc );
+    }
+    // set the elementary variables
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+        {
+            bFunc = dd->vars[i];
+//            bFunc = dd->vars[Abc_NtkCiNum(pNtk) - 1 - i];
+            Abc_ObjSetGlobalBdd( pObj, bFunc );  Cudd_Ref( bFunc );
+        }
+
+    // collect the global functions of the COs
+    Counter = 0;
+    // construct the BDDs
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose );
+        if ( bFunc == NULL )
+        {
+            if ( fVerbose )
+            printf( "Constructing global BDDs is aborted.\n" );
+            Abc_NtkFreeGlobalBdds( pNtk, 0 );
+            Cudd_Quit( dd );
+            return NULL;
+        }
+        bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pObj) );  Cudd_Ref( bFunc ); 
+        Abc_ObjSetGlobalBdd( pObj, bFunc );
+    }
+    Extra_ProgressBarStop( pProgress );
+
+/*
+    // derefence the intermediate BDDs
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        if ( pObj->pCopy ) 
+        {
+            Cudd_RecursiveDeref( dd, (DdNode *)pObj->pCopy );
+            pObj->pCopy = NULL;
+        }
+*/
+/*
+    // make sure all nodes are derefed
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( pObj->pCopy != NULL )
+            printf( "Abc_NtkBuildGlobalBdds() error: Node %d has BDD assigned\n", pObj->Id );
+        if ( pObj->vFanouts.nSize > 0 )
+            printf( "Abc_NtkBuildGlobalBdds() error: Node %d has refs assigned\n", pObj->Id );
+    }
+*/
+    // reset references
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                pFanin->vFanouts.nSize++;
+
+    // reorder one more time
+    if ( fReorder )
+    {
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
+        Cudd_AutodynDisable( dd );
+    }
+//    Cudd_PrintInfo( dd, stdout );
+    return dd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the global BDD for one AIG node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose )
+{
+    DdNode * bFunc, * bFunc0, * bFunc1, * bFuncC;
+    int fDetectMuxes = 1;
+    assert( !Abc_ObjIsComplement(pNode) );
+    if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
+    {
+        Extra_ProgressBarStop( pProgress );
+        if ( fVerbose )
+        printf( "The number of live nodes reached %d.\n", nBddSizeMax );
+        fflush( stdout );
+        return NULL;
+    }
+    // if the result is available return
+    if ( Abc_ObjGlobalBdd(pNode) == NULL )
+    {
+        Abc_Obj_t * pNodeC, * pNode0, * pNode1;
+        pNode0 = Abc_ObjFanin0(pNode);
+        pNode1 = Abc_ObjFanin1(pNode);
+        // check for the special case when it is MUX/EXOR
+        if ( fDetectMuxes && 
+             Abc_ObjGlobalBdd(pNode0) == NULL && Abc_ObjGlobalBdd(pNode1) == NULL &&
+             Abc_ObjIsNode(pNode0) && Abc_ObjFanoutNum(pNode0) == 1 && 
+             Abc_ObjIsNode(pNode1) && Abc_ObjFanoutNum(pNode1) == 1 && 
+             Abc_NodeIsMuxType(pNode) )
+        {
+            // deref the fanins
+            pNode0->vFanouts.nSize--;
+            pNode1->vFanouts.nSize--;
+            // recognize the MUX
+            pNodeC = Abc_NodeRecognizeMux( pNode, &pNode1, &pNode0 );
+            assert( Abc_ObjFanoutNum(pNodeC) > 1 );
+            // dereference the control once (the second time it will be derefed when BDDs are computed)
+            pNodeC->vFanouts.nSize--;
+
+            // compute the result for all branches
+            bFuncC = Abc_NodeGlobalBdds_rec( dd, pNodeC, nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
+            if ( bFuncC == NULL )
+                return NULL;
+            Cudd_Ref( bFuncC );
+            bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode0), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
+            if ( bFunc0 == NULL )
+                return NULL;
+            Cudd_Ref( bFunc0 );
+            bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode1), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
+            if ( bFunc1 == NULL )
+                return NULL;
+            Cudd_Ref( bFunc1 );
+
+            // complement the branch BDDs
+            bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjIsComplement(pNode0) );
+            bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjIsComplement(pNode1) );
+            // get the final result
+            bFunc = Cudd_bddIte( dd, bFuncC, bFunc1, bFunc0 );   Cudd_Ref( bFunc );
+            Cudd_RecursiveDeref( dd, bFunc0 );
+            Cudd_RecursiveDeref( dd, bFunc1 );
+            Cudd_RecursiveDeref( dd, bFuncC );
+            // add the number of used nodes
+            (*pCounter) += 3;
+        }
+        else
+        {
+            // compute the result for both branches
+            bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
+            if ( bFunc0 == NULL )
+                return NULL;
+            Cudd_Ref( bFunc0 );
+            bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
+            if ( bFunc1 == NULL )
+                return NULL;
+            Cudd_Ref( bFunc1 );
+            bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
+            bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
+            // get the final result
+            bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
+            Cudd_RecursiveDeref( dd, bFunc0 );
+            Cudd_RecursiveDeref( dd, bFunc1 );
+            // add the number of used nodes
+            (*pCounter)++;
+        }
+        // set the result
+        assert( Abc_ObjGlobalBdd(pNode) == NULL );
+        Abc_ObjSetGlobalBdd( pNode, bFunc );
+        // increment the progress bar
+        if ( pProgress )
+            Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
+    }
+    // prepare the return value
+    bFunc = Abc_ObjGlobalBdd(pNode);
+    // dereference BDD at the node
+    if ( --pNode->vFanouts.nSize == 0 && fDropInternal )
+    {
+        Cudd_Deref( bFunc );
+        Abc_ObjSetGlobalBdd( pNode, NULL );
+    }
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the global BDDs of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdManager * Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan ) 
+{ 
+    return Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, fFreeMan ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the shared size of global BDDs of the COs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkSizeOfGlobalBdds( Abc_Ntk_t * pNtk ) 
+{
+    Vec_Ptr_t * vFuncsGlob;
+    Abc_Obj_t * pObj;
+    int RetValue, i;
+    // complement the global functions
+    vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Vec_PtrPush( vFuncsGlob, Abc_ObjGlobalBdd(pObj) );
+    RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
+    Vec_PtrFree( vFuncsGlob );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the BDD of the logic cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
+{
+    /*
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pNodeR;
+    DdManager * dd;
+    DdNode * bFunc;
+    double Result;
+    int i;
+    pNodeR = Abc_ObjRegular(pNode);
+    assert( Abc_NtkIsStrash(pNodeR->pNtk) );
+    Abc_NtkCleanCopy( pNodeR->pNtk );
+    // get the CIs in the support of the node
+    vNodes = Abc_NtkNodeSupport( pNodeR->pNtk, &pNodeR, 1 );
+    // start the manager
+    dd = Cudd_Init( Vec_PtrSize(vNodes), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    // assign elementary BDDs for the CIs
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)dd->vars[i];
+    // build the BDD of the cone
+    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000, 1, NULL, NULL, 1 );  Cudd_Ref( bFunc );
+    bFunc = Cudd_NotCond( bFunc, pNode != pNodeR );
+    // count minterms
+    Result = Cudd_CountMinterm( dd, bFunc, dd->size );
+    // get the percentagle
+    Result *= 100.0;
+    for ( i = 0; i < dd->size; i++ )
+        Result /= 2;
+    // clean up
+    Cudd_Quit( dd );
+    Vec_PtrFree( vNodes );
+    return Result;
+    */
+    return 0.0;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Experiment with BDD-based representation of implications.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBddImplicationTest()
+{
+    DdManager * dd;
+    DdNode * bImp, * bSum, * bTemp;
+    int nVars = 200;
+    int nImps = 200;
+    int i, clk;
+clk = clock();
+    dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd, CUDD_REORDER_SIFT );
+    bSum = b0;   Cudd_Ref( bSum );
+    for ( i = 0; i < nImps; i++ )
+    {
+        printf( "." );
+        bImp = Cudd_bddAnd( dd, dd->vars[rand()%nVars], dd->vars[rand()%nVars] );  Cudd_Ref( bImp );
+        bSum = Cudd_bddOr( dd, bTemp = bSum, bImp );     Cudd_Ref( bSum );
+        Cudd_RecursiveDeref( dd, bTemp );
+        Cudd_RecursiveDeref( dd, bImp );
+    }
+    printf( "The BDD before = %d.\n", Cudd_DagSize(bSum) );
+    Cudd_ReduceHeap( dd, CUDD_REORDER_SIFT, 1 );
+    printf( "The BDD after  = %d.\n", Cudd_DagSize(bSum) );
+PRT( "Time", clock() - clk );
+    Cudd_RecursiveDeref( dd, bSum );
+    Cudd_Quit( dd );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+