Version abc71001

1 files changed, 1134 insertions, 0 deletions

diff --git a/src/base/abci/abcOdc.c b/src/base/abci/abcOdc.c
new file mode 100644
index 00000000..d6e59328
--- /dev/null
+++ b/src/base/abci/abcOdc.c
@@ -0,0 +1,1134 @@
+/**CFile****************************************************************
+
+  FileName    [abcOdc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Scalable computation of observability don't-cares.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcOdc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define ABC_DC_MAX_NODES   (1<<15)
+
+typedef unsigned short Odc_Lit_t;
+
+typedef struct Odc_Obj_t_ Odc_Obj_t;     // 16 bytes
+struct Odc_Obj_t_
+{
+    Odc_Lit_t               iFan0;       // first fanin
+    Odc_Lit_t               iFan1;       // second fanin
+    Odc_Lit_t               iNext;       // next node in the hash table
+    unsigned short          TravId;      // the traversal ID
+    unsigned                uData;       // the computed data
+    unsigned                uMask;       // the variable mask 
+};
+
+typedef struct Odc_Man_t_ Odc_Man_t;
+struct Odc_Man_t_
+{
+    // dont'-care parameters
+    int                     nVarsMax;    // the max number of cut variables
+    int                     nLevels;     // the number of ODC levels
+    int                     fVerbose;    // the verbosiness flag
+    int                     fVeryVerbose;// the verbosiness flag to print per-node stats
+    int                     nPercCutoff; // cutoff percentage
+
+    // windowing
+    Abc_Obj_t *             pNode;       // the node for windowing
+    Vec_Ptr_t *             vLeaves;     // the number of the cut
+    Vec_Ptr_t *             vRoots;      // the roots of the cut
+    Vec_Ptr_t *             vBranches;   // additional inputs 
+
+    // internal AIG package
+    // objects
+    int                     nPis;        // number of PIs (nVarsMax + 32)
+    int                     nObjs;       // number of objects (Const1, PIs, ANDs)
+    int                     nObjsAlloc;  // number of objects allocated
+    Odc_Obj_t *             pObjs;       // objects 
+    Odc_Lit_t               iRoot;       // the root object
+    unsigned short          nTravIds;    // the number of travIDs
+    // structural hashing
+    Odc_Lit_t *             pTable;      // hash table
+    int                     nTableSize;  // hash table size
+    Vec_Int_t *             vUsedSpots;  // the used spots
+
+    // truth tables
+    int                     nBits;       // the number of bits
+    int                     nWords;      // the number of words 
+    Vec_Ptr_t *             vTruths;     // truth tables for each node
+    Vec_Ptr_t *             vTruthsElem; // elementary truth tables for the PIs
+    unsigned *              puTruth;     // the place where the resulting truth table does
+
+    // statistics
+    int                     nWins;       // the number of windows processed
+    int                     nWinsEmpty;  // the number of empty windows
+    int                     nSimsEmpty;  // the number of empty simulation infos
+    int                     nQuantsOver; // the number of quantification overflows
+    int                     nWinsFinish; // the number of windows that finished
+    int                     nTotalDcs;   // total percentage of DCs
+
+    // runtime
+    int                     timeClean;   // windowing
+    int                     timeWin;     // windowing
+    int                     timeMiter;   // computing the miter
+    int                     timeSim;     // simulation
+    int                     timeQuant;   // quantification
+    int                     timeTruth;   // truth table
+    int                     timeTotal;   // useful runtime
+    int                     timeAbort;   // aborted runtime
+};
+
+
+// quantity of different objects
+static inline int           Odc_PiNum( Odc_Man_t * p )                     { return p->nPis;                       }
+static inline int           Odc_NodeNum( Odc_Man_t * p )                   { return p->nObjs - p->nPis - 1;        }
+static inline int           Odc_ObjNum( Odc_Man_t * p )                    { return p->nObjs;                      }
+
+// complemented attributes of objects
+static inline int           Odc_IsComplement( Odc_Lit_t Lit )              { return Lit &  (Odc_Lit_t)1;           }
+static inline Odc_Lit_t     Odc_Regular( Odc_Lit_t Lit )                   { return Lit & ~(Odc_Lit_t)1;           }
+static inline Odc_Lit_t     Odc_Not( Odc_Lit_t Lit )                       { return Lit ^  (Odc_Lit_t)1;           }
+static inline Odc_Lit_t     Odc_NotCond( Odc_Lit_t Lit, int c )            { return Lit ^  (Odc_Lit_t)(c!=0);      }
+
+// specialized Literals
+static inline Odc_Lit_t     Odc_Const0()                                   { return 1;                             }
+static inline Odc_Lit_t     Odc_Const1()                                   { return 0;                             }
+static inline Odc_Lit_t     Odc_Var( Odc_Man_t * p, int i )                { assert( i >= 0 && i < p->nPis ); return (i+1) << 1;  }
+static inline int           Odc_IsConst( Odc_Lit_t Lit )                   { return Lit <  (Odc_Lit_t)2;           }
+static inline int           Odc_IsTerm( Odc_Man_t * p, Odc_Lit_t Lit )     { return (int)(Lit>>1) <= p->nPis;      }
+
+// accessing internal storage
+static inline Odc_Obj_t *   Odc_ObjNew( Odc_Man_t * p )                    { assert( p->nObjs < p->nObjsAlloc ); return p->pObjs + p->nObjs++;        }
+static inline Odc_Lit_t     Odc_Obj2Lit( Odc_Man_t * p, Odc_Obj_t * pObj ) { assert( pObj ); return (pObj - p->pObjs) << 1;                           }
+static inline Odc_Obj_t *   Odc_Lit2Obj( Odc_Man_t * p, Odc_Lit_t Lit )    { assert( !(Lit & 1) && (int)(Lit>>1) < p->nObjs ); return p->pObjs + (Lit>>1); }
+
+// fanins and their complements
+static inline Odc_Lit_t     Odc_ObjChild0( Odc_Obj_t * pObj )              { return pObj->iFan0;                   }
+static inline Odc_Lit_t     Odc_ObjChild1( Odc_Obj_t * pObj )              { return pObj->iFan1;                   }
+static inline Odc_Lit_t     Odc_ObjFanin0( Odc_Obj_t * pObj )              { return Odc_Regular(pObj->iFan0);      }
+static inline Odc_Lit_t     Odc_ObjFanin1( Odc_Obj_t * pObj )              { return Odc_Regular(pObj->iFan1);      }
+static inline int           Odc_ObjFaninC0( Odc_Obj_t * pObj )             { return Odc_IsComplement(pObj->iFan0); }
+static inline int           Odc_ObjFaninC1( Odc_Obj_t * pObj )             { return Odc_IsComplement(pObj->iFan1); }
+
+// traversal IDs
+static inline void          Odc_ManIncrementTravId( Odc_Man_t * p )                         { p->nTravIds++;                                    }
+static inline void          Odc_ObjSetTravIdCurrent( Odc_Man_t * p, Odc_Obj_t * pObj )      { pObj->TravId = p->nTravIds;                       }
+static inline int           Odc_ObjIsTravIdCurrent( Odc_Man_t * p, Odc_Obj_t * pObj )       { return (int )((int)pObj->TravId == p->nTravIds);  }
+
+// truth tables
+static inline unsigned *    Odc_ObjTruth( Odc_Man_t * p, Odc_Lit_t Lit )   { assert( !(Lit & 1) ); return Vec_PtrEntry(p->vTruths, Lit >> 1);  }
+
+// iterators 
+#define Odc_ForEachPi( p, Lit, i )                                                 \
+    for ( i = 0; (i < Odc_PiNum(p)) && (((Lit) = Odc_Var(p, i)), 1); i++ )
+#define Odc_ForEachAnd( p, pObj, i )                                               \
+    for ( i = 1 + Odc_CiNum(p); (i < Odc_ObjNum(p)) && ((pObj) = (p)->pObjs + i); i++ )
+
+ 
+// exported functions
+extern Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose );
+extern void Abc_NtkDontCareClear( Odc_Man_t * p );
+extern void Abc_NtkDontCareFree( Odc_Man_t * p );
+extern int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the don't-care manager.]
+
+  Description [The parameters are the max number of cut variables, 
+  the number of fanout levels used for the ODC computation, and verbosiness.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose )
+{
+    Odc_Man_t * p;
+    unsigned * pData;
+    int i, k;
+    p = ALLOC( Odc_Man_t, 1 );
+    memset( p, 0, sizeof(Odc_Man_t) );
+    assert( nVarsMax > 4 && nVarsMax < 16 );
+    assert( nLevels > 0 && nLevels < 10 );
+
+    srand( 0xABC );
+
+    // dont'-care parameters
+    p->nVarsMax     = nVarsMax;
+    p->nLevels      = nLevels;
+    p->fVerbose     = fVerbose;
+    p->fVeryVerbose = fVeryVerbose;
+    p->nPercCutoff  = 10;
+
+    // windowing
+    p->vRoots    = Vec_PtrAlloc( 128 );
+    p->vBranches = Vec_PtrAlloc( 128 );
+
+    // internal AIG package
+    // allocate room for objects
+    p->nObjsAlloc = ABC_DC_MAX_NODES; 
+    p->pObjs = ALLOC( Odc_Obj_t, p->nObjsAlloc * sizeof(Odc_Obj_t) );
+    p->nPis  = nVarsMax + 32;
+    p->nObjs = 1 + p->nPis;
+    memset( p->pObjs, 0, p->nObjs * sizeof(Odc_Obj_t) );
+    // set the PI masks
+    for ( i = 0; i < 32; i++ )
+        p->pObjs[1 + p->nVarsMax + i].uMask = (1 << i);
+    // allocate hash table
+    p->nTableSize = p->nObjsAlloc/3 + 1;
+    p->pTable = ALLOC( Odc_Lit_t, p->nTableSize * sizeof(Odc_Lit_t) );
+    memset( p->pTable, 0, p->nTableSize * sizeof(Odc_Lit_t) );
+    p->vUsedSpots = Vec_IntAlloc( 1000 );
+
+    // truth tables
+    p->nWords = Abc_TruthWordNum( p->nVarsMax );
+    p->nBits = p->nWords * 8 * sizeof(unsigned);
+    p->vTruths = Vec_PtrAllocSimInfo( p->nObjsAlloc, p->nWords );
+    p->vTruthsElem = Vec_PtrAllocSimInfo( p->nVarsMax, p->nWords );
+
+    // set elementary truth tables
+    Abc_InfoFill( Vec_PtrEntry(p->vTruths, 0), p->nWords );
+    for ( k = 0; k < p->nVarsMax; k++ )
+    {
+//        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
+        pData = Vec_PtrEntry( p->vTruthsElem, k );
+        Abc_InfoClear( pData, p->nWords );
+        for ( i = 0; i < p->nBits; i++ )
+            if ( i & (1 << k) )
+                pData[i>>5] |= (1 << (i&31));
+    }
+
+    // set random truth table for the additional inputs
+    for ( k = p->nVarsMax; k < p->nPis; k++ )
+    {
+        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
+        Abc_InfoRandom( pData, p->nWords );
+    }
+
+    // set the miter to the unused value
+    p->iRoot = 0xffff;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Clears the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDontCareClear( Odc_Man_t * p )
+{
+    int clk = clock();
+    // clean the structural hashing table
+    if ( Vec_IntSize(p->vUsedSpots) > p->nTableSize/3 ) // more than one third
+        memset( p->pTable, 0, sizeof(Odc_Lit_t) * p->nTableSize );
+    else
+    {
+        int iSpot, i;
+        Vec_IntForEachEntry( p->vUsedSpots, iSpot, i )
+            p->pTable[iSpot] = 0;
+    }
+    Vec_IntClear( p->vUsedSpots ); 
+    // reset the number of nodes
+    p->nObjs = 1 + p->nPis;
+    // reset the root node
+    p->iRoot = 0xffff;
+
+p->timeClean += clock() - clk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the don't-care manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDontCareFree( Odc_Man_t * p )
+{
+    if ( p->fVerbose )
+    {
+        printf( "Wins = %5d. Empty = %5d. SimsEmpty = %5d. QuantOver = %5d. WinsFinish = %5d.\n", 
+            p->nWins, p->nWinsEmpty, p->nSimsEmpty, p->nQuantsOver, p->nWinsFinish );
+        printf( "Ave DCs per window = %6.2f %%. Ave DCs per finished window = %6.2f %%.\n", 
+            1.0*p->nTotalDcs/p->nWins, 1.0*p->nTotalDcs/p->nWinsFinish );
+        printf( "Runtime stats of the ODC manager:\n" );
+        PRT( "Cleaning    ", p->timeClean );
+        PRT( "Windowing   ", p->timeWin   );
+        PRT( "Miter       ", p->timeMiter );
+        PRT( "Simulation  ", p->timeSim   );
+        PRT( "Quantifying ", p->timeQuant );
+        PRT( "Truth table ", p->timeTruth );
+        PRT( "TOTAL       ", p->timeTotal );
+        PRT( "Aborted     ", p->timeAbort );
+    }
+    Vec_PtrFree( p->vRoots );
+    Vec_PtrFree( p->vBranches );
+    Vec_PtrFree( p->vTruths );
+    Vec_PtrFree( p->vTruthsElem );
+    Vec_IntFree( p->vUsedSpots );
+    free( p->pObjs );
+    free( p->pTable );
+    free( p );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFO of the collected nodes up to the given level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDontCareWinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit || pObj == pNode )
+        return;
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return;
+    Abc_NodeSetTravIdCurrent( pObj );
+    ////////////////////////////////////////
+    // try to reduce the runtime
+    if ( Abc_ObjFanoutNum(pObj) > 100 )
+        return;
+    ////////////////////////////////////////
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Abc_NtkDontCareWinSweepLeafTfo_rec( pFanout, nLevelLimit, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFO of the collected nodes up to the given level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDontCareWinSweepLeafTfo( Odc_Man_t * p )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        Abc_NtkDontCareWinSweepLeafTfo_rec( pObj, p->pNode->Level + p->nLevels, p->pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively collects the roots.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDontCareWinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    assert( Abc_ObjIsNode(pObj) );
+    assert( Abc_NodeIsTravIdCurrent(pObj) );
+    // check if the node has all fanouts marked
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        if ( !Abc_NodeIsTravIdCurrent(pFanout) )
+            break;
+    // if some of the fanouts are unmarked, add the node to the root
+    if ( i < Abc_ObjFanoutNum(pObj) ) 
+    {
+        Vec_PtrPushUnique( vRoots, pObj );
+        return;
+    }
+    // otherwise, call recursively
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Abc_NtkDontCareWinCollectRoots_rec( pFanout, vRoots );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the roots of the window.]
+
+  Description [Roots of the window are the nodes that have at least
+  one fanout that it not in the TFO of the leaves.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDontCareWinCollectRoots( Odc_Man_t * p )
+{
+    assert( !Abc_NodeIsTravIdCurrent(p->pNode) );
+    // mark the node with the old traversal ID
+    Abc_NodeSetTravIdCurrent( p->pNode ); 
+    // collect the roots
+    Vec_PtrClear( p->vRoots );
+    Abc_NtkDontCareWinCollectRoots_rec( p->pNode, p->vRoots );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Recursively adds missing nodes and leaves.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+int Abc_NtkDontCareWinAddMissing_rec( Odc_Man_t * p, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    // skip the already collected leaves and branches
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return 1;
+    // if this is not an internal node - make it a new branch
+    if ( !Abc_NodeIsTravIdPrevious(pObj) || Abc_ObjIsCi(pObj) ) //|| (int)pObj->Level <= p->nLevLeaves )
+    {
+        Abc_NodeSetTravIdCurrent( pObj );
+        Vec_PtrPush( p->vBranches, pObj );
+        return Vec_PtrSize(p->vBranches) <= 32;
+    }
+    // visit the fanins of the node
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        if ( !Abc_NtkDontCareWinAddMissing_rec( p, pFanin ) )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds to the window nodes and leaves in the TFI of the roots.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDontCareWinAddMissing( Odc_Man_t * p )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    // set the leaves
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        Abc_NodeSetTravIdCurrent( pObj );        
+    // explore from the roots
+    Vec_PtrClear( p->vBranches );
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+        if ( !Abc_NtkDontCareWinAddMissing_rec( p, pObj ) )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes window for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDontCareWindow( Odc_Man_t * p )
+{
+    // mark the TFO of the collected nodes up to the given level (p->pNode->Level + p->nWinTfoMax)
+    Abc_NtkDontCareWinSweepLeafTfo( p );
+    // find the roots of the window
+    Abc_NtkDontCareWinCollectRoots( p );
+    if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
+    {
+//        printf( "Empty window\n" );
+        return 0;
+    }
+    // add the nodes in the TFI of the roots that are not yet in the window
+    if ( !Abc_NtkDontCareWinAddMissing( p ) )
+    {
+//        printf( "Too many branches (%d)\n", Vec_PtrSize(p->vBranches) );
+        return 0;
+    }
+    return 1;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performing hashing of two AIG Literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Odc_HashKey( Odc_Lit_t iFan0, Odc_Lit_t iFan1, int TableSize ) 
+{
+    unsigned Key = 0;
+    Key ^= Odc_Regular(iFan0) * 7937;
+    Key ^= Odc_Regular(iFan1) * 2971;
+    Key ^= Odc_IsComplement(iFan0) * 911;
+    Key ^= Odc_IsComplement(iFan1) * 353;
+    return Key % TableSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the given name node already exists in the table.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Odc_Lit_t * Odc_HashLookup( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 )
+{
+    Odc_Obj_t * pObj;
+    Odc_Lit_t * pEntry;
+    unsigned uHashKey;
+    assert( iFan0 < iFan1 );
+    // get the hash key for this node
+    uHashKey = Odc_HashKey( iFan0, iFan1, p->nTableSize );
+    // remember the spot in the hash table that will be used
+    if ( p->pTable[uHashKey] == 0 )
+        Vec_IntPush( p->vUsedSpots, uHashKey );
+    // find the entry
+    for ( pEntry = p->pTable + uHashKey; *pEntry; pEntry = &pObj->iNext )
+    {
+        pObj = Odc_Lit2Obj( p, *pEntry );
+        if ( pObj->iFan0 == iFan0 && pObj->iFan1 == iFan1 )
+            return pEntry;
+    }
+    return pEntry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds node by structural hashing or creates a new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Odc_Lit_t Odc_And( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 )
+{
+    Odc_Obj_t * pObj;
+    Odc_Lit_t * pEntry;
+    unsigned uMask0, uMask1;
+    int Temp;
+    // consider trivial cases
+    if ( iFan0 == iFan1 )
+        return iFan0;
+    if ( iFan0 == Odc_Not(iFan1) )
+        return Odc_Const0();
+    if ( Odc_Regular(iFan0) == Odc_Const1() )
+        return iFan0 == Odc_Const1() ? iFan1 : Odc_Const0();
+    if ( Odc_Regular(iFan1) == Odc_Const1() )
+        return iFan1 == Odc_Const1() ? iFan0 : Odc_Const0();
+    // canonicize the fanin order
+    if ( iFan0 > iFan1 )
+        Temp = iFan0, iFan0 = iFan1, iFan1 = Temp;
+    // check if a node with these fanins exists
+    pEntry = Odc_HashLookup( p, iFan0, iFan1 );
+    if ( *pEntry )
+        return *pEntry;
+    // create a new node
+    pObj = Odc_ObjNew( p );
+    pObj->iFan0 = iFan0;
+    pObj->iFan1 = iFan1;
+    pObj->iNext = 0;
+    pObj->TravId = 0;
+    // set the mask
+    uMask0 = Odc_Lit2Obj(p, Odc_Regular(iFan0))->uMask;
+    uMask1 = Odc_Lit2Obj(p, Odc_Regular(iFan1))->uMask;
+    pObj->uMask = uMask0 | uMask1;
+    // add to the table
+    *pEntry = Odc_Obj2Lit( p, pObj );
+    return *pEntry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Boolean OR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Odc_Lit_t Odc_Or( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 )
+{
+    return Odc_Not( Odc_And(p, Odc_Not(iFan0), Odc_Not(iFan1)) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Boolean XOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Odc_Lit_t Odc_Xor( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 )
+{
+    return Odc_Or( p, Odc_And(p, iFan0, Odc_Not(iFan1)), Odc_And(p, Odc_Not(iFan0), iFan1) );
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the window into the AIG package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Abc_NtkDontCareTransfer_rec( Odc_Man_t * p, Abc_Obj_t * pNode, Abc_Obj_t * pPivot )
+{
+    unsigned uData0, uData1;
+    Odc_Lit_t uLit0, uLit1, uRes0, uRes1;
+    assert( !Abc_ObjIsComplement(pNode) );
+    // skip visited objects
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
+        return pNode->pCopy;
+    Abc_NodeSetTravIdCurrent(pNode);
+    assert( Abc_ObjIsNode(pNode) );
+    // consider the case when the node is the pivot
+    if ( pNode == pPivot )
+        return pNode->pCopy = (void *)((Odc_Const1() << 16) | Odc_Const0());
+    // compute the cofactors
+    uData0 = (unsigned)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin0(pNode), pPivot );
+    uData1 = (unsigned)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin1(pNode), pPivot );
+    // find the 0-cofactor
+    uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Abc_ObjFaninC0(pNode) );
+    uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Abc_ObjFaninC1(pNode) );
+    uRes0 = Odc_And( p, uLit0, uLit1 );
+    // find the 1-cofactor
+    uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 >> 16), Abc_ObjFaninC0(pNode) );
+    uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Abc_ObjFaninC1(pNode) );
+    uRes1 = Odc_And( p, uLit0, uLit1 );
+    // find the result
+    return pNode->pCopy = (void *)((uRes1 << 16) | uRes0);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the window into the AIG package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDontCareTransfer( Odc_Man_t * p )
+{
+    Abc_Obj_t * pObj;
+    Odc_Lit_t uRes0, uRes1;
+    Odc_Lit_t uLit;
+    unsigned uData;
+    int i;
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    // set elementary variables at the leaves 
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+    {
+        uLit = Odc_Var( p, i );
+        pObj->pCopy = (void *)((uLit << 16) | uLit);
+        Abc_NodeSetTravIdCurrent(pObj);
+    }
+    // set elementary variables at the branched 
+    Vec_PtrForEachEntry( p->vBranches, pObj, i )
+    {
+        uLit = Odc_Var( p, i+p->nVarsMax );
+        pObj->pCopy = (void *)((uLit << 16) | uLit);
+        Abc_NodeSetTravIdCurrent(pObj);
+    }
+    // compute the AIG for the window
+    p->iRoot = Odc_Const0();
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+    {
+        uData = (unsigned)Abc_NtkDontCareTransfer_rec( p, pObj, p->pNode );
+        // get the cofactors
+        uRes0 = uData & 0xffff;
+        uRes1 = uData >> 16;
+        // compute the miter
+//        assert( uRes0 != uRes1 ); // may be false if the node is redundant w.r.t. this root
+        uLit = Odc_Xor( p, uRes0, uRes1 );
+        p->iRoot = Odc_Or( p, p->iRoot, uLit );
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes the pair of cofactors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Abc_NtkDontCareCofactors_rec( Odc_Man_t * p, Odc_Lit_t Lit, unsigned uMask )
+{
+    Odc_Obj_t * pObj;
+    unsigned uData0, uData1;
+    Odc_Lit_t uLit0, uLit1, uRes0, uRes1;
+    assert( !Odc_IsComplement(Lit) );
+    // skip visited objects
+    pObj = Odc_Lit2Obj( p, Lit );
+    if ( Odc_ObjIsTravIdCurrent(p, pObj) )
+        return pObj->uData;
+    Odc_ObjSetTravIdCurrent(p, pObj);
+    // skip objects out of the cone
+    if ( (pObj->uMask & uMask) == 0 )
+        return pObj->uData = ((Lit << 16) | Lit);
+    // consider the case when the node is the var
+    if ( pObj->uMask == uMask && Odc_IsTerm(p, Lit) )
+        return pObj->uData = ((Odc_Const1() << 16) | Odc_Const0());
+    // compute the cofactors
+    uData0 = Abc_NtkDontCareCofactors_rec( p, Odc_ObjFanin0(pObj), uMask );
+    uData1 = Abc_NtkDontCareCofactors_rec( p, Odc_ObjFanin1(pObj), uMask );
+    // find the 0-cofactor
+    uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Odc_ObjFaninC0(pObj) );
+    uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Odc_ObjFaninC1(pObj) );
+    uRes0 = Odc_And( p, uLit0, uLit1 );
+    // find the 1-cofactor
+    uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 >> 16), Odc_ObjFaninC0(pObj) );
+    uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Odc_ObjFaninC1(pObj) );
+    uRes1 = Odc_And( p, uLit0, uLit1 );
+    // find the result
+    return pObj->uData = ((uRes1 << 16) | uRes0);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Quantifies the branch variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDontCareQuantify( Odc_Man_t * p )
+{   
+    Odc_Lit_t uRes0, uRes1;
+    unsigned uData;
+    int i;
+    assert( p->iRoot < 0xffff );
+    assert( Vec_PtrSize(p->vBranches) <= 32 ); // the mask size
+    for ( i = 0; i < Vec_PtrSize(p->vBranches); i++ )
+    {
+        // compute the cofactors w.r.t. this variable
+        Odc_ManIncrementTravId( p );
+        uData = Abc_NtkDontCareCofactors_rec( p, Odc_Regular(p->iRoot), (1 << i) );
+        uRes0 = Odc_NotCond( (Odc_Lit_t)(uData & 0xffff), Odc_IsComplement(p->iRoot) );
+        uRes1 = Odc_NotCond( (Odc_Lit_t)(uData >> 16),    Odc_IsComplement(p->iRoot) );
+        // quantify this variable existentially
+        p->iRoot = Odc_Or( p, uRes0, uRes1 );
+        // check the limit
+        if ( Odc_ObjNum(p) > ABC_DC_MAX_NODES/2 )
+            return 0;
+    }
+    assert( p->nObjs <= p->nObjsAlloc );
+    return 1;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Set elementary truth tables for PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDontCareSimulateSetElem2( Odc_Man_t * p )
+{
+    unsigned * pData;
+    int i, k;
+    for ( k = 0; k < p->nVarsMax; k++ )
+    {
+        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
+        Abc_InfoClear( pData, p->nWords );
+        for ( i = 0; i < p->nBits; i++ )
+            if ( i & (1 << k) )
+                pData[i>>5] |= (1 << (i&31));
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Set elementary truth tables for PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDontCareSimulateSetElem( Odc_Man_t * p )
+{
+    unsigned * pData, * pData2;
+    int k;
+    for ( k = 0; k < p->nVarsMax; k++ )
+    {
+        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
+        pData2 = Vec_PtrEntry( p->vTruthsElem, k );
+        Abc_InfoCopy( pData, pData2, p->nWords );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Set random simulation words for PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDontCareSimulateSetRand( Odc_Man_t * p )
+{
+    unsigned * pData;
+    int w, k, Number;
+    for ( w = 0; w < p->nWords; w++ )
+    {
+        Number = rand();
+        for ( k = 0; k < p->nVarsMax; k++ )
+        {
+            pData = Odc_ObjTruth( p, Odc_Var(p, k) );
+            pData[w] = (Number & (1<<k)) ? ~0 : 0;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Set random simulation words for PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDontCareCountMintsWord( Odc_Man_t * p, unsigned * puTruth )
+{
+    int w, Counter = 0;
+    for ( w = 0; w < p->nWords; w++ )
+        if ( puTruth[w] )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDontCareTruthOne( Odc_Man_t * p, Odc_Lit_t Lit )
+{
+    Odc_Obj_t * pObj;
+    unsigned * pInfo, * pInfo1, * pInfo2;
+    int k, fComp1, fComp2;
+    assert( !Odc_IsComplement( Lit ) );
+    assert( !Odc_IsTerm( p, Lit ) );
+    // get the truth tables
+    pObj   = Odc_Lit2Obj( p, Lit );
+    pInfo  = Odc_ObjTruth( p, Lit );
+    pInfo1 = Odc_ObjTruth( p, Odc_ObjFanin0(pObj) );
+    pInfo2 = Odc_ObjTruth( p, Odc_ObjFanin1(pObj) );
+    fComp1 = Odc_ObjFaninC0( pObj );
+    fComp2 = Odc_ObjFaninC1( pObj );
+    // simulate
+    if ( fComp1 && fComp2 )
+        for ( k = 0; k < p->nWords; k++ )
+            pInfo[k] = ~pInfo1[k] & ~pInfo2[k];
+    else if ( fComp1 && !fComp2 )
+        for ( k = 0; k < p->nWords; k++ )
+            pInfo[k] = ~pInfo1[k] &  pInfo2[k];
+    else if ( !fComp1 && fComp2 )
+        for ( k = 0; k < p->nWords; k++ )
+            pInfo[k] =  pInfo1[k] & ~pInfo2[k];
+    else // if ( fComp1 && fComp2 )
+        for ( k = 0; k < p->nWords; k++ )
+            pInfo[k] =  pInfo1[k] &  pInfo2[k];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDontCareSimulate_rec( Odc_Man_t * p, Odc_Lit_t Lit )
+{
+    Odc_Obj_t * pObj;
+    assert( !Odc_IsComplement(Lit) );
+    // skip terminals
+    if ( Odc_IsTerm(p, Lit) )
+        return;
+    // skip visited objects
+    pObj = Odc_Lit2Obj( p, Lit );
+    if ( Odc_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Odc_ObjSetTravIdCurrent(p, pObj);
+    // call recursively
+    Abc_NtkDontCareSimulate_rec( p, Odc_ObjFanin0(pObj) );
+    Abc_NtkDontCareSimulate_rec( p, Odc_ObjFanin1(pObj) );
+    // construct the truth table
+    Abc_NtkDontCareTruthOne( p, Lit );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table of the care set.]
+
+  Description [Returns the number of ones in the simulation info.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDontCareSimulate( Odc_Man_t * p, unsigned * puTruth )
+{
+    Odc_ManIncrementTravId( p );
+    Abc_NtkDontCareSimulate_rec( p, Odc_Regular(p->iRoot) );
+    Abc_InfoCopy( puTruth, Odc_ObjTruth(p, Odc_Regular(p->iRoot)), p->nWords );
+    if ( Odc_IsComplement(p->iRoot) )
+        Abc_InfoNot( puTruth, p->nWords );
+    return Extra_TruthCountOnes( puTruth, p->nVarsMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table of the care set.]
+
+  Description [Returns the number of ones in the simulation info.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDontCareSimulateBefore( Odc_Man_t * p, unsigned * puTruth )
+{
+    int nIters = 2;
+    int nRounds, Counter, r;
+    // decide how many rounds to simulate
+    nRounds = p->nBits / p->nWords;
+    Counter = 0;
+    for ( r = 0; r < nIters; r++ )
+    {
+        Abc_NtkDontCareSimulateSetRand( p );
+        Abc_NtkDontCareSimulate( p, puTruth );
+        Counter += Abc_NtkDontCareCountMintsWord( p, puTruth );
+    }
+    // normalize
+    Counter = Counter * nRounds / nIters;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes ODCs for the node in terms of the cut variables.]
+
+  Description [Returns the number of don't care minterms in the truth table.
+  In particular, this procedure returns 0 if there is no don't-cares.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth )
+{
+    int nMints, RetValue;
+    int clk, clkTotal = clock();
+
+    p->nWins++;
+    
+    // set the parameters
+    assert( !Abc_ObjIsComplement(pNode) );
+    assert( Abc_ObjIsNode(pNode) );
+    assert( Vec_PtrSize(vLeaves) <= p->nVarsMax );
+    p->vLeaves = vLeaves;
+    p->pNode = pNode;
+
+    // compute the window
+clk = clock();
+    RetValue = Abc_NtkDontCareWindow( p );
+p->timeWin += clock() - clk;
+    if ( !RetValue )
+    {
+p->timeAbort += clock() - clkTotal;
+        Abc_InfoFill( puTruth, p->nWords );
+        p->nWinsEmpty++;        
+        return 0;
+    }
+
+    if ( p->fVeryVerbose )
+    {
+        printf( " %5d : ", pNode->Id );
+        printf( "Leaf = %2d ", Vec_PtrSize(p->vLeaves) );
+        printf( "Root = %2d ", Vec_PtrSize(p->vRoots) );
+        printf( "Bran = %2d ", Vec_PtrSize(p->vBranches) );
+        printf( " |  " );
+    }
+
+    // transfer the window into the AIG package
+clk = clock();
+    Abc_NtkDontCareTransfer( p );
+p->timeMiter += clock() - clk;
+
+    // simulate to estimate the amount of don't-cares
+clk = clock();
+    nMints = Abc_NtkDontCareSimulateBefore( p, puTruth );
+p->timeSim += clock() - clk;
+    if ( p->fVeryVerbose )
+    {
+        printf( "AIG = %5d ", Odc_NodeNum(p) );
+        printf( "%6.2f %%  ", 100.0 * (p->nBits - nMints) / p->nBits );
+    }
+
+    // if there is less then the given percentage of don't-cares, skip
+    if ( 100.0 * (p->nBits - nMints) / p->nBits < 1.0 * p->nPercCutoff )
+    {
+p->timeAbort += clock() - clkTotal;
+        if ( p->fVeryVerbose )
+            printf( "Simulation cutoff.\n" );
+        Abc_InfoFill( puTruth, p->nWords );
+        p->nSimsEmpty++;
+        return 0;
+    }
+
+    // quantify external variables
+clk = clock();
+    RetValue = Abc_NtkDontCareQuantify( p );
+p->timeQuant += clock() - clk;
+    if ( !RetValue )
+    {
+p->timeAbort += clock() - clkTotal;
+        if ( p->fVeryVerbose )
+            printf( "=== Overflow! ===\n" );
+        Abc_InfoFill( puTruth, p->nWords );
+        p->nQuantsOver++;
+        return 0;
+    }
+
+    // get the truth table
+clk = clock();
+    Abc_NtkDontCareSimulateSetElem( p );
+    nMints = Abc_NtkDontCareSimulate( p, puTruth );
+p->timeTruth += clock() - clk;
+    if ( p->fVeryVerbose )
+    {
+        printf( "AIG = %5d ", Odc_NodeNum(p) );
+        printf( "%6.2f %%  ", 100.0 * (p->nBits - nMints) / p->nBits );
+        printf( "\n" );
+    }
+p->timeTotal += clock() - clkTotal;
+    p->nWinsFinish++;
+    p->nTotalDcs += (int)(100.0 * (p->nBits - nMints) / p->nBits);
+    return nMints;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+