Version abc70428

abc.dsp

@@ -42,7 +42,7 @@ RSC=rc.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
-# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
 # ADD BASE RSC /l 0x409 /d "NDEBUG"
 # ADD RSC /l 0x409 /d "NDEBUG"
 BSC32=bscmake.exe
@@ -66,7 +66,7 @@ LINK32=link.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
-# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
 # SUBTRACT CPP /X
 # ADD BASE RSC /l 0x409 /d "_DEBUG"
 # ADD RSC /l 0x409 /d "_DEBUG"
@@ -214,6 +214,10 @@ SOURCE=.\src\base\abci\abcCut.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcDar.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcDebug.c
 # End Source File
 # Begin Source File
@@ -278,6 +282,10 @@ SOURCE=.\src\base\abci\abcMap.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcMeasure.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcMini.c
 # End Source File
 # Begin Source File
@@ -797,6 +805,66 @@ SOURCE=.\src\aig\mem\mem.h
 
 # PROP Default_Filter ""
 # End Group
+# Begin Group "dar"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\dar\dar.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darBalance.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darData.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darDfs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darObj.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darOper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darUtil.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "bdd"
 

abc.rc

@@ -166,3 +166,4 @@ alias tst6     "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_
 
 
 alias bug      "r pj1_if3.blif; lp"
+alias table    "r lutexp.baf; test"

src/aig/dar/darCheck.c

+/**CFile****************************************************************
+
+  FileName    [darCheck.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    [AIG checking procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darCheck.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the consistency of the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ManCheck( Dar_Man_t * p )
+{
+    Dar_Obj_t * pObj, * pObj2;
+    int i;
+    // check primary inputs
+    Dar_ManForEachPi( p, pObj, i )
+    {
+        if ( Dar_ObjFanin0(pObj) || Dar_ObjFanin1(pObj) )
+        {
+            printf( "Dar_ManCheck: The PI node \"%p\" has fanins.\n", pObj );
+            return 0;
+        }
+    }
+    // check primary outputs
+    Dar_ManForEachPo( p, pObj, i )
+    {
+        if ( !Dar_ObjFanin0(pObj) )
+        {
+            printf( "Dar_ManCheck: The PO node \"%p\" has NULL fanin.\n", pObj );
+            return 0;
+        }
+        if ( Dar_ObjFanin1(pObj) )
+        {
+            printf( "Dar_ManCheck: The PO node \"%p\" has second fanin.\n", pObj );
+            return 0;
+        }
+    }
+    // check internal nodes
+    Dar_ManForEachObj( p, pObj, i )
+    {
+        if ( !Dar_ObjIsNode(pObj) )
+            continue;
+        if ( !Dar_ObjFanin0(pObj) || !Dar_ObjFanin1(pObj) )
+        {
+            printf( "Dar_ManCheck: The AIG has internal node \"%p\" with a NULL fanin.\n", pObj );
+            return 0;
+        }
+        if ( Dar_ObjFanin0(pObj)->Id >= Dar_ObjFanin1(pObj)->Id )
+        {
+            printf( "Dar_ManCheck: The AIG has node \"%p\" with a wrong ordering of fanins.\n", pObj );
+            return 0;
+        }
+        pObj2 = Dar_TableLookup( p, pObj );
+        if ( pObj2 != pObj )
+        {
+            printf( "Dar_ManCheck: Node \"%p\" is not in the structural hashing table.\n", pObj );
+            return 0;
+        }
+    }
+    // count the total number of nodes
+    if ( Dar_ManObjNum(p) != 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) )
+    {
+        printf( "Dar_ManCheck: The number of created nodes is wrong.\n" );
+        return 0;
+    }
+    // count the number of nodes in the table
+    if ( Dar_TableCountEntries(p) != Dar_ManAndNum(p) + Dar_ManExorNum(p) )
+    {
+        printf( "Dar_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
+        return 0;
+    }
+//    if ( !Dar_ManIsAcyclic(p) )
+//        return 0;
+    return 1; 
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/dar/darCore.c

+/**CFile****************************************************************
+
+  FileName    [darCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    [Core of the rewriting package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ManRewrite( Dar_Man_t * p )
+{
+    ProgressBar * pProgress;
+    Dar_Obj_t * pObj, * pObjNew;
+    int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
+    int clk = 0, clkStart = clock();
+    // remove dangling nodes
+    Dar_ManCleanup( p );
+    // set elementary cuts for the PIs
+    Dar_ManSetupPis( p );
+//    if ( p->pPars->fUpdateLevel )
+//        Dar_NtkStartReverseLevels( p );
+    // resynthesize each node once
+    nNodesOld = Vec_PtrSize( p->vObjs );
+    pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
+    Dar_ManForEachObj( p, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( !Dar_ObjIsNode(pObj) )
+            continue;
+        if ( i > nNodesOld )
+            break;
+        // compute cuts for the node
+        Dar_ObjComputeCuts_rec( p, pObj );
+        // go through the cuts of this node
+        Required = 1000000;
+        p->GainBest = -1;
+        for ( k = 1; k < (int)pObj->nCuts; k++ )
+            Dar_LibEval( p, pObj, (Dar_Cut_t *)pObj->pData + k, Required );
+        // check the best gain
+        if ( !(p->GainBest > 0 || p->GainBest == 0 && p->pPars->fUseZeros) )
+            continue;
+        // if we end up here, a rewriting step is accepted
+        nNodeBefore = Dar_ManNodeNum( p );
+        pObjNew = Dar_LibBuildBest( p );
+        pObjNew = Dar_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase );
+        // remove the old nodes
+        Dar_ObjReplace( p, pObj, pObjNew );
+        // compare the gains
+        nNodeAfter = Dar_ManNodeNum( p );
+        assert( p->GainBest == nNodeBefore - nNodeAfter );
+        assert( (int)pObjNew->Level <= Required );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Dar_ManCutsFree( p );
+    // put the nodes into the DFS order and reassign their IDs
+//    Dar_NtkReassignIds( p );
+
+    // fix the levels
+//    if ( p->pPars->fUpdateLevel )
+//        Dar_NtkStopReverseLevels( p );
+    // check
+    if ( !Dar_ManCheck( p ) )
+    {
+        printf( "Dar_ManRewrite: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/dar/darMan.c

+/**CFile****************************************************************
+
+  FileName    [darMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    [AIG manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the AIG manager.]
+
+  Description [The argument of this procedure is a soft limit on the
+  the number of nodes, or 0 if the limit is unknown.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dar_Man_t * Dar_ManStart( int nNodesMax )
+{
+    Dar_Man_t * p;
+    int i;
+    if ( nNodesMax <= 0 )
+        nNodesMax = 10007;
+    // start the manager
+    p = ALLOC( Dar_Man_t, 1 );
+    memset( p, 0, sizeof(Dar_Man_t) );
+    // perform initializations
+    p->nTravIds = 1;
+    p->fCatchExor = 0;
+    // allocate arrays for nodes
+    p->vPis = Vec_PtrAlloc( 100 );
+    p->vPos = Vec_PtrAlloc( 100 );
+    // prepare the internal memory manager
+    p->pMemObjs = Dar_MmFixedStart( sizeof(Dar_Obj_t), nNodesMax );
+    p->pMemCuts = Dar_MmFlexStart();
+    // prepare storage for cuts
+    p->nBaseCuts = DAR_CUT_BASE;
+    for ( i = 0; i < p->nBaseCuts; i++ )
+        p->pBaseCuts[i] = p->BaseCuts + i;
+    // create the constant node
+    p->pConst1 = Dar_ManFetchMemory( p );
+    p->pConst1->Type = DAR_AIG_CONST1;
+    p->pConst1->fPhase = 1;
+    p->nCreated = 1;
+    // start the table
+    p->nTableSize = nNodesMax;
+    p->pTable = ALLOC( Dar_Obj_t *, p->nTableSize );
+    memset( p->pTable, 0, sizeof(Dar_Obj_t *) * p->nTableSize );
+    // other data
+    p->vLeavesBest = Vec_PtrAlloc( 4 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ManStop( Dar_Man_t * p )
+{
+    Dar_Obj_t * pObj;
+    int i;
+    // make sure the nodes have clean marks
+    Dar_ManForEachObj( p, pObj, i )
+        assert( !pObj->fMarkA && !pObj->fMarkB );
+    // print time
+    if ( p->time1 ) { PRT( "time1", p->time1 ); }
+    if ( p->time2 ) { PRT( "time2", p->time2 ); }
+//    Dar_TableProfile( p );
+    Dar_MmFixedStop( p->pMemObjs, 0 );
+    Dar_MmFlexStop( p->pMemCuts, 0 );
+    if ( p->vPis )      Vec_PtrFree( p->vPis );
+    if ( p->vPos )      Vec_PtrFree( p->vPos );
+    if ( p->vObjs )     Vec_PtrFree( p->vObjs );
+    if ( p->vRequired ) Vec_IntFree( p->vRequired );
+    if ( p->vLeavesBest ) Vec_PtrFree( p->vLeavesBest );
+    free( p->pTable );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ManCleanup( Dar_Man_t * p )
+{
+    Vec_Ptr_t * vObjs;
+    Dar_Obj_t * pNode;
+    int i, nNodesOld;
+    nNodesOld = Dar_ManNodeNum(p);
+    // collect roots of dangling nodes
+    vObjs = Vec_PtrAlloc( 100 );
+    Dar_ManForEachObj( p, pNode, i )
+        if ( Dar_ObjIsNode(pNode) && Dar_ObjRefs(pNode) == 0 )
+            Vec_PtrPush( vObjs, pNode );
+    // recursively remove dangling nodes
+    Vec_PtrForEachEntry( vObjs, pNode, i )
+        Dar_ObjDelete_rec( p, pNode, 1 );
+    Vec_PtrFree( vObjs );
+    return nNodesOld - Dar_ManNodeNum(p);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ManPrintStats( Dar_Man_t * p )
+{
+    printf( "PI/PO = %d/%d. ", Dar_ManPiNum(p), Dar_ManPoNum(p) );
+    printf( "A = %7d. ",       Dar_ManAndNum(p) );
+    printf( "X = %5d. ",       Dar_ManExorNum(p) );
+    printf( "Cre = %7d. ",     p->nCreated );
+    printf( "Del = %7d. ",     p->nDeleted );
+    printf( "Lev = %3d. ",     Dar_ManCountLevels(p) );
+    printf( "\n" );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/dar/darObj.c

+/**CFile****************************************************************
+
+  FileName    [darObj.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    [Adding/removing objects.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darObj.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates primary input.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dar_Obj_t * Dar_ObjCreatePi( Dar_Man_t * p )
+{
+    Dar_Obj_t * pObj;
+    pObj = Dar_ManFetchMemory( p );
+    pObj->Type = DAR_AIG_PI;
+    Vec_PtrPush( p->vPis, pObj );
+    p->nObjs[DAR_AIG_PI]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates primary output with the given driver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dar_Obj_t * Dar_ObjCreatePo( Dar_Man_t * p, Dar_Obj_t * pDriver )
+{
+    Dar_Obj_t * pObj;
+    pObj = Dar_ManFetchMemory( p );
+    pObj->Type = DAR_AIG_PO;
+    Vec_PtrPush( p->vPos, pObj );
+    // add connections
+    Dar_ObjConnect( p, pObj, pDriver, NULL );
+    // update node counters of the manager
+    p->nObjs[DAR_AIG_PO]++;
+    return pObj;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dar_Obj_t * Dar_ObjCreate( Dar_Man_t * p, Dar_Obj_t * pGhost )
+{
+    Dar_Obj_t * pObj;
+    assert( !Dar_IsComplement(pGhost) );
+    assert( Dar_ObjIsNode(pGhost) );
+    assert( pGhost == &p->Ghost );
+    // get memory for the new object
+    pObj = Dar_ManFetchMemory( p );
+    pObj->Type = pGhost->Type;
+    // add connections
+    Dar_ObjConnect( p, pObj, pGhost->pFanin0, pGhost->pFanin1 );
+    // update node counters of the manager
+    p->nObjs[Dar_ObjType(pObj)]++;
+    assert( pObj->pData == NULL );
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connect the object to the fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFan0, Dar_Obj_t * pFan1 )
+{
+    assert( !Dar_IsComplement(pObj) );
+    assert( Dar_ObjIsNode(pObj) );
+    // add the first fanin
+    pObj->pFanin0 = pFan0;
+    pObj->pFanin1 = pFan1;
+    // increment references of the fanins and add their fanouts
+    if ( pFan0 != NULL )
+        Dar_ObjRef( Dar_ObjFanin0(pObj) );
+    if ( pFan1 != NULL )
+        Dar_ObjRef( Dar_ObjFanin1(pObj) );
+    // set level and phase
+    if ( pFan1 != NULL )
+    {
+        pObj->Level = Dar_ObjLevelNew( pObj );
+        pObj->fPhase = Dar_ObjFaninPhase(pFan0) & Dar_ObjFaninPhase(pFan1);
+    }
+    else
+    {
+        pObj->Level = pFan0->Level;
+        pObj->fPhase = Dar_ObjFaninPhase(pFan0);
+    }
+    // add the node to the structural hash table
+    if ( Dar_ObjIsNode(pObj) )
+        Dar_TableInsert( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Disconnects the object from the fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ObjDisconnect( Dar_Man_t * p, Dar_Obj_t * pObj )
+{
+    assert( !Dar_IsComplement(pObj) );
+    // remove connections
+    if ( pObj->pFanin0 != NULL )
+        Dar_ObjDeref(Dar_ObjFanin0(pObj));
+    if ( pObj->pFanin1 != NULL )
+        Dar_ObjDeref(Dar_ObjFanin1(pObj));
+    // remove the node from the structural hash table
+    if ( Dar_ObjIsNode(pObj) )
+        Dar_TableDelete( p, pObj );
+    // add the first fanin
+    pObj->pFanin0 = NULL;
+    pObj->pFanin1 = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ObjDelete( Dar_Man_t * p, Dar_Obj_t * pObj )
+{
+    assert( !Dar_IsComplement(pObj) );
+    assert( !Dar_ObjIsTerm(pObj) );
+    assert( Dar_ObjRefs(pObj) == 0 );
+    p->nDeleted++;
+    Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+    Dar_ManRecycleMemory( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the MFFC of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop )
+{
+    Dar_Obj_t * pFanin0, * pFanin1;
+    assert( !Dar_IsComplement(pObj) );
+    if ( Dar_ObjIsConst1(pObj) || Dar_ObjIsPi(pObj) )
+        return;
+    assert( Dar_ObjIsNode(pObj) );
+    pFanin0 = Dar_ObjFanin0(pObj);
+    pFanin1 = Dar_ObjFanin1(pObj);
+    Dar_ObjDisconnect( p, pObj );
+    p->nObjs[pObj->Type]--;
+    if ( fFreeTop )
+        Dar_ObjDelete( p, pObj );
+    if ( pFanin0 && !Dar_ObjIsNone(pFanin0) && Dar_ObjRefs(pFanin0) == 0 )
+        Dar_ObjDelete_rec( p, pFanin0, 1 );
+    if ( pFanin1 && !Dar_ObjIsNone(pFanin1) && Dar_ObjRefs(pFanin1) == 0 )
+        Dar_ObjDelete_rec( p, pFanin1, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces one object by another.]
+
+  Description [Both objects are currently in the manager. The new object
+  (pObjNew) should be used instead of the old object (pObjOld). If the 
+  new object is complemented or used, the buffer is added.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew )
+{
+    Dar_Obj_t * pObjNewR = Dar_Regular(pObjNew);
+    // the object to be replaced cannot be complemented
+    assert( !Dar_IsComplement(pObjOld) );
+    // the object to be replaced cannot be a terminal
+    assert( !Dar_ObjIsPi(pObjOld) && !Dar_ObjIsPo(pObjOld) );
+    // the object to be used cannot be a buffer
+    assert( !Dar_ObjIsBuf(pObjNewR) && !Dar_ObjIsPo(pObjNewR) );
+    // the object cannot be the same
+    assert( pObjOld != pObjNewR );
+    // make sure object is not pointing to itself
+    assert( pObjOld != Dar_ObjFanin0(pObjNewR) );
+    assert( pObjOld != Dar_ObjFanin1(pObjNewR) );
+    // delete the old node
+    Dar_ObjDelete_rec( p, pObjOld, 0 );
+    // if the new object is complemented or already used, create a buffer
+    if ( Dar_IsComplement(pObjNew) || Dar_ObjRefs(pObjNew) > 0 || !Dar_ObjIsNode(pObjNew) )
+    {
+        pObjOld->Type = DAR_AIG_BUF;
+        p->nObjs[pObjOld->Type]++;
+        Dar_ObjConnect( p, pObjOld, pObjNew, NULL );
+    }
+    else
+    {
+        Dar_Obj_t * pFanin0 = pObjNew->pFanin0;
+        Dar_Obj_t * pFanin1 = pObjNew->pFanin1;
+        pObjOld->Type = pObjNew->Type;
+        Dar_ObjDisconnect( p, pObjNew );
+        Dar_ObjDelete( p, pObjNew );
+        Dar_ObjConnect( p, pObjOld, pFanin0, pFanin1 );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/dar/darTable.c

+/**CFile****************************************************************
+
+  FileName    [darTable.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    [Structural hashing table.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darTable.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// hashing the node
+static unsigned long Dar_Hash( Dar_Obj_t * pObj, int TableSize ) 
+{
+    unsigned long Key = Dar_ObjIsExor(pObj) * 1699;
+    Key ^= (long)Dar_ObjFanin0(pObj) * 7937;
+    Key ^= (long)Dar_ObjFanin1(pObj) * 2971;
+    Key ^= Dar_ObjFaninC0(pObj) * 911;
+    Key ^= Dar_ObjFaninC1(pObj) * 353;
+    return Key % TableSize;
+}
+
+// returns the place where this node is stored (or should be stored)
+static Dar_Obj_t ** Dar_TableFind( Dar_Man_t * p, Dar_Obj_t * pObj )
+{
+    Dar_Obj_t ** ppEntry;
+    assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) );
+    assert( Dar_ObjFanin0(pObj)->Id < Dar_ObjFanin1(pObj)->Id );
+    for ( ppEntry = p->pTable + Dar_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext )
+        if ( *ppEntry == pObj )
+            return ppEntry;
+    assert( *ppEntry == NULL );
+    return ppEntry;
+}
+
+static void         Dar_TableResize( Dar_Man_t * p );
+static unsigned int Cudd_PrimeAig( unsigned int  p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+/**Function*************************************************************
+
+  Synopsis    [Checks if node with the given attributes is in the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dar_Obj_t * Dar_TableLookup( Dar_Man_t * p, Dar_Obj_t * pGhost )
+{
+    Dar_Obj_t * pEntry;
+    assert( !Dar_IsComplement(pGhost) );
+    assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) );
+    assert( Dar_ObjFanin0(pGhost)->Id < Dar_ObjFanin1(pGhost)->Id );
+    if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) || !Dar_ObjRefs(Dar_ObjFanin1(pGhost)) )
+        return NULL;
+    for ( pEntry = p->pTable[Dar_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext )
+    {
+        if ( Dar_ObjChild0(pEntry) == Dar_ObjChild0(pGhost) && 
+             Dar_ObjChild1(pEntry) == Dar_ObjChild1(pGhost) && 
+             Dar_ObjType(pEntry) == Dar_ObjType(pGhost) )
+            return pEntry;
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the new node to the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_TableInsert( Dar_Man_t * p, Dar_Obj_t * pObj )
+{
+    Dar_Obj_t ** ppPlace;
+    assert( !Dar_IsComplement(pObj) );
+    assert( Dar_TableLookup(p, pObj) == NULL );
+    if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Dar_ManNodeNum(p) )
+        Dar_TableResize( p );
+    ppPlace = Dar_TableFind( p, pObj );
+    assert( *ppPlace == NULL );
+    *ppPlace = pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node from the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_TableDelete( Dar_Man_t * p, Dar_Obj_t * pObj )
+{
+    Dar_Obj_t ** ppPlace;
+    assert( !Dar_IsComplement(pObj) );
+    ppPlace = Dar_TableFind( p, pObj );
+    assert( *ppPlace == pObj ); // node should be in the table
+    // remove the node
+    *ppPlace = pObj->pNext;
+    pObj->pNext = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of nodes in the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_TableCountEntries( Dar_Man_t * p )
+{
+    Dar_Obj_t * pEntry;
+    int i, Counter = 0;
+    for ( i = 0; i < p->nTableSize; i++ )
+        for ( pEntry = p->pTable[i]; pEntry; pEntry = pEntry->pNext )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the table.]
+
+  Description [Typically this procedure should not be called.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_TableResize( Dar_Man_t * p )
+{
+    Dar_Obj_t * pEntry, * pNext;
+    Dar_Obj_t ** pTableOld, ** ppPlace;
+    int nTableSizeOld, Counter, nEntries, i, clk;
+clk = clock();
+    // save the old table
+    pTableOld = p->pTable;
+    nTableSizeOld = p->nTableSize;
+    // get the new table
+    p->nTableSize = Cudd_PrimeAig( 2 * Dar_ManNodeNum(p) ); 
+    p->pTable = ALLOC( Dar_Obj_t *, p->nTableSize );
+    memset( p->pTable, 0, sizeof(Dar_Obj_t *) * p->nTableSize );
+    // rehash the entries from the old table
+    Counter = 0;
+    for ( i = 0; i < nTableSizeOld; i++ )
+    for ( pEntry = pTableOld[i], pNext = pEntry? pEntry->pNext : NULL; pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL )
+    {
+        // get the place where this entry goes in the table 
+        ppPlace = Dar_TableFind( p, pEntry );
+        assert( *ppPlace == NULL ); // should not be there
+        // add the entry to the list
+        *ppPlace = pEntry;
+        pEntry->pNext = NULL;
+        Counter++;
+    }
+    nEntries = Dar_ManNodeNum(p);
+    assert( Counter == nEntries );
+    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
+    PRT( "Time", clock() - clk );
+    // replace the table and the parameters
+    free( pTableOld );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Profiles the hash table.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Dar_TableProfile( Dar_Man_t * p )
+{
+    Dar_Obj_t * pEntry;
+    int i, Counter;
+    for ( i = 0; i < p->nTableSize; i++ )
+    {
+        Counter = 0;
+        for ( pEntry = p->pTable[i]; pEntry; pEntry = pEntry->pNext )
+            Counter++;
+        if ( Counter ) 
+            printf( "%d ", Counter );
+    }
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the next prime &gt;= p.]
+
+  Description [Copied from CUDD, for stand-aloneness.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+unsigned int Cudd_PrimeAig( unsigned int  p)
+{
+    int i,pn;
+    p--;
+    do {
+        p++;
+        if (p&1) {
+        pn = 1;
+        i = 3;
+        while ((unsigned) (i * i) <= p) {
+        if (p % i == 0) {
+            pn = 0;
+            break;
+        }
+        i += 2;
+        }
+    } else {
+        pn = 0;
+    }
+    } while (!pn);
+    return(p);
+
+} /* end of Cudd_Prime */
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/dar/dar_.c

+/**CFile****************************************************************
+
+  FileName    [dar_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: dar_.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/dar/module.make

+SRC +=    src/aig/dar/darBalance.c \
+    src/aig/dar/darCheck.c \
+    src/aig/dar/darCore.c \
+    src/aig/dar/darCut.c \
+    src/aig/dar/darData.c \
+    src/aig/dar/darDfs.c \
+    src/aig/dar/darLib.c \
+    src/aig/dar/darMan.c \
+    src/aig/dar/darMem.c \
+    src/aig/dar/darObj.c \
+    src/aig/dar/darOper.c \
+    src/aig/dar/darTable.c \
+    src/aig/dar/darUtil.c 

src/aig/hop/hop.h

@@ -149,7 +149,7 @@ static inline int          Hop_ManNodeNum( Hop_Man_t * p )        { return p->nO
 static inline int          Hop_ManGetCost( Hop_Man_t * p )        { return p->nObjs[AIG_AND]+3*p->nObjs[AIG_EXOR]; }
 static inline int          Hop_ManObjNum( Hop_Man_t * p )         { return p->nCreated - p->nDeleted;           }
 
-static inline Hop_Type_t   Hop_ObjType( Hop_Obj_t * pObj )        { return pObj->Type;               }
+static inline Hop_Type_t   Hop_ObjType( Hop_Obj_t * pObj )        { return (Hop_Type_t)pObj->Type;               }
 static inline int          Hop_ObjIsNone( Hop_Obj_t * pObj )      { return pObj->Type == AIG_NONE;   }
 static inline int          Hop_ObjIsConst1( Hop_Obj_t * pObj )    { assert(!Hop_IsComplement(pObj)); return pObj->Type == AIG_CONST1; }
 static inline int          Hop_ObjIsPi( Hop_Obj_t * pObj )        { return pObj->Type == AIG_PI;     }
@@ -182,8 +182,8 @@ static inline Hop_Obj_t *  Hop_ObjFanin0( Hop_Obj_t * pObj )      { return Hop_R
 static inline Hop_Obj_t *  Hop_ObjFanin1( Hop_Obj_t * pObj )      { return Hop_Regular(pObj->pFanin1);             }
 static inline Hop_Obj_t *  Hop_ObjChild0( Hop_Obj_t * pObj )      { return pObj->pFanin0;                          }
 static inline Hop_Obj_t *  Hop_ObjChild1( Hop_Obj_t * pObj )      { return pObj->pFanin1;                          }
-static inline Hop_Obj_t *  Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin0(pObj)? Hop_NotCond(Hop_ObjFanin0(pObj)->pData, Hop_ObjFaninC0(pObj)) : NULL;  }
-static inline Hop_Obj_t *  Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond(Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL;  }
+static inline Hop_Obj_t *  Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin0(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin0(pObj)->pData, Hop_ObjFaninC0(pObj)) : NULL;  }
+static inline Hop_Obj_t *  Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL;  }
 static inline int          Hop_ObjLevel( Hop_Obj_t * pObj )       { return pObj->nRefs;                            }
 static inline int          Hop_ObjLevelNew( Hop_Obj_t * pObj )    { return 1 + Hop_ObjIsExor(pObj) + AIG_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs);       }
 static inline int          Hop_ObjFaninPhase( Hop_Obj_t * pObj )  { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; }
@@ -210,8 +210,16 @@ static inline Hop_Obj_t *  Hop_ObjCreateGhost( Hop_Man_t * p, Hop_Obj_t * p0, Ho
     assert( Type == AIG_PI || Hop_Regular(p0) != Hop_Regular(p1) );
     pGhost = Hop_ManGhost(p);
     pGhost->Type = Type;
-    pGhost->pFanin0 = p0 < p1? p0 : p1;
-    pGhost->pFanin1 = p0 < p1? p1 : p0;
+    if ( Hop_Regular(p0)->Id < Hop_Regular(p1)->Id )
+    {
+        pGhost->pFanin0 = p0;
+        pGhost->pFanin1 = p1;
+    }
+    else
+    {
+        pGhost->pFanin0 = p1;
+        pGhost->pFanin1 = p0;
+    }
     return pGhost;
 }
 

src/aig/hop/hopCheck.c

@@ -74,7 +74,7 @@ int Hop_ManCheck( Hop_Man_t * p )
             printf( "Hop_ManCheck: The AIG has internal node \"%p\" with a NULL fanin.\n", pObj );
             return 0;
         }
-        if ( Hop_ObjFanin0(pObj) >= Hop_ObjFanin1(pObj) )
+        if ( Hop_ObjFanin0(pObj)->Id >= Hop_ObjFanin1(pObj)->Id )
         {
             printf( "Hop_ManCheck: The AIG has node \"%p\" with a wrong ordering of fanins.\n", pObj );
             return 0;

src/aig/hop/hopMan.c

@@ -60,6 +60,7 @@ Hop_Man_t * Hop_ManStart()
     p->pConst1->fPhase = 1;
     p->nCreated = 1;
     // start the table
+//    p->nTableSize = 107;
     p->nTableSize = 10007;
     p->pTable = ALLOC( Hop_Obj_t *, p->nTableSize );
     memset( p->pTable, 0, sizeof(Hop_Obj_t *) * p->nTableSize );

src/aig/hop/hopTable.c

@@ -38,13 +38,14 @@ static unsigned long Hop_Hash( Hop_Obj_t * pObj, int TableSize )
 // returns the place where this node is stored (or should be stored)
 static Hop_Obj_t ** Hop_TableFind( Hop_Man_t * p, Hop_Obj_t * pObj )
 {
-    int i;
+    Hop_Obj_t ** ppEntry;
     assert( Hop_ObjChild0(pObj) && Hop_ObjChild1(pObj) );
-    assert( Hop_ObjChild0(pObj) <  Hop_ObjChild1(pObj) );
-    for ( i = Hop_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
-        if ( p->pTable[i] == pObj )
-            break;
-    return p->pTable + i;
+    assert( Hop_ObjFanin0(pObj)->Id < Hop_ObjFanin1(pObj)->Id );
+    for ( ppEntry = p->pTable + Hop_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext )
+        if ( *ppEntry == pObj )
+            return ppEntry;
+    assert( *ppEntry == NULL );
+    return ppEntry;
 }
 
 static void         Hop_TableResize( Hop_Man_t * p );
@@ -56,7 +57,7 @@ static unsigned int Cudd_PrimeAig( unsigned int  p );
  
 /**Function*************************************************************
 
-  Synopsis    [Checks if node with the given attributes is in the hash table.]
+  Synopsis    [Checks if a node with the given attributes is in the hash table.]
 
   Description []
                
@@ -67,18 +68,18 @@ static unsigned int Cudd_PrimeAig( unsigned int  p );
 ***********************************************************************/
 Hop_Obj_t * Hop_TableLookup( Hop_Man_t * p, Hop_Obj_t * pGhost )
 {
-    int i;
+    Hop_Obj_t * pEntry;
     assert( !Hop_IsComplement(pGhost) );
     assert( Hop_ObjChild0(pGhost) && Hop_ObjChild1(pGhost) );
-    assert( Hop_ObjChild0(pGhost) <  Hop_ObjChild1(pGhost) );
+    assert( Hop_ObjFanin0(pGhost)->Id < Hop_ObjFanin1(pGhost)->Id );
     if ( p->fRefCount && (!Hop_ObjRefs(Hop_ObjFanin0(pGhost)) || !Hop_ObjRefs(Hop_ObjFanin1(pGhost))) )
         return NULL;
-    for ( i = Hop_Hash(pGhost, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
+    for ( pEntry = p->pTable[Hop_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext )
     {
-        if ( Hop_ObjChild0(p->pTable[i]) == Hop_ObjChild0(pGhost) && 
-             Hop_ObjChild1(p->pTable[i]) == Hop_ObjChild1(pGhost) && 
-             Hop_ObjType(p->pTable[i]) == Hop_ObjType(pGhost) )
-            return p->pTable[i];
+        if ( Hop_ObjChild0(pEntry) == Hop_ObjChild0(pGhost) && 
+             Hop_ObjChild1(pEntry) == Hop_ObjChild1(pGhost) && 
+             Hop_ObjType(pEntry) == Hop_ObjType(pGhost) )
+            return pEntry;
     }
     return NULL;
 }
@@ -99,7 +100,7 @@ void Hop_TableInsert( Hop_Man_t * p, Hop_Obj_t * pObj )
     Hop_Obj_t ** ppPlace;
     assert( !Hop_IsComplement(pObj) );
     assert( Hop_TableLookup(p, pObj) == NULL );
-    if ( p->nTableSize < 2 * Hop_ManNodeNum(p) )
+    if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Hop_ManNodeNum(p) )
         Hop_TableResize( p );
     ppPlace = Hop_TableFind( p, pObj );
     assert( *ppPlace == NULL );
@@ -119,20 +120,13 @@ void Hop_TableInsert( Hop_Man_t * p, Hop_Obj_t * pObj )
 ***********************************************************************/
 void Hop_TableDelete( Hop_Man_t * p, Hop_Obj_t * pObj )
 {
-    Hop_Obj_t * pEntry, ** ppPlace;
-    int i;
+    Hop_Obj_t ** ppPlace;
     assert( !Hop_IsComplement(pObj) );
     ppPlace = Hop_TableFind( p, pObj );
     assert( *ppPlace == pObj ); // node should be in the table
-    *ppPlace = NULL;
-    // rehash the adjacent entries
-    i = ppPlace - p->pTable;
-    for ( i = (i+1) % p->nTableSize; p->pTable[i]; i = (i+1) % p->nTableSize )
-    {
-        pEntry = p->pTable[i];
-        p->pTable[i] = 0;
-        Hop_TableInsert( p, pEntry );
-    }
+    // remove the node
+    *ppPlace = pObj->pNext;
+    pObj->pNext = NULL;
 }
 
 /**Function*************************************************************
@@ -148,9 +142,11 @@ void Hop_TableDelete( Hop_Man_t * p, Hop_Obj_t * pObj )
 ***********************************************************************/
 int Hop_TableCountEntries( Hop_Man_t * p )
 {
+    Hop_Obj_t * pEntry;
     int i, Counter = 0;
     for ( i = 0; i < p->nTableSize; i++ )
-        Counter += (p->pTable[i] != NULL);
+        for ( pEntry = p->pTable[i]; pEntry; pEntry = pEntry->pNext )
+            Counter++;
     return Counter;
 }
 
@@ -167,30 +163,32 @@ int Hop_TableCountEntries( Hop_Man_t * p )
 ***********************************************************************/
 void Hop_TableResize( Hop_Man_t * p )
 {
+    Hop_Obj_t * pEntry, * pNext;
     Hop_Obj_t ** pTableOld, ** ppPlace;
-    int nTableSizeOld, Counter, nEntries, e, clk;
+    int nTableSizeOld, Counter, nEntries, i, clk;
 clk = clock();
     // save the old table
     pTableOld = p->pTable;
     nTableSizeOld = p->nTableSize;
     // get the new table
-    p->nTableSize = Cudd_PrimeAig( 5 * Hop_ManNodeNum(p) ); 
+    p->nTableSize = Cudd_PrimeAig( 2 * Hop_ManNodeNum(p) ); 
     p->pTable = ALLOC( Hop_Obj_t *, p->nTableSize );
     memset( p->pTable, 0, sizeof(Hop_Obj_t *) * p->nTableSize );
     // rehash the entries from the old table
     Counter = 0;
-    for ( e = 0; e < nTableSizeOld; e++ )
+    for ( i = 0; i < nTableSizeOld; i++ )
+    for ( pEntry = pTableOld[i], pNext = pEntry? pEntry->pNext : NULL; pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL )
     {
-        if ( pTableOld[e] == 0 )
-            continue;
+        // get the place where this entry goes in the table 
+        ppPlace = Hop_TableFind( p, pEntry );
+        assert( *ppPlace == NULL ); // should not be there
+        // add the entry to the list
+        *ppPlace = pEntry;
+        pEntry->pNext = NULL;
         Counter++;
-        // get the place where this entry goes in the table table
-        ppPlace = Hop_TableFind( p, pTableOld[e] );
-        assert( *ppPlace == NULL ); // should not be in the table
-        *ppPlace = pTableOld[e];
     }
     nEntries = Hop_ManNodeNum(p);
-//    assert( Counter == nEntries );
+    assert( Counter == nEntries );
 //    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
 //    PRT( "Time", clock() - clk );
     // replace the table and the parameters
@@ -210,16 +208,15 @@ clk = clock();
 ******************************************************************************/
 void Hop_TableProfile( Hop_Man_t * p )
 {
-    int i, Counter = 0;
+    Hop_Obj_t * pEntry;
+    int i, Counter;
     for ( i = 0; i < p->nTableSize; i++ )
     {
-        if ( p->pTable[i] )
+        Counter = 0;
+        for ( pEntry = p->pTable[i]; pEntry; pEntry = pEntry->pNext )
             Counter++;
-        else if ( Counter )
-        {
+        if ( Counter ) 
             printf( "%d ", Counter );
-            Counter = 0;
-        }
     }
 }
 
@@ -237,7 +234,6 @@ void Hop_TableProfile( Hop_Man_t * p )
 unsigned int Cudd_PrimeAig( unsigned int  p)
 {
     int i,pn;
-
     p--;
     do {
         p++;

src/base/abc/abc.h

@@ -330,7 +330,7 @@ static inline bool        Abc_NtkIsComb( Abc_Ntk_t * pNtk )          { return Ab
 static inline bool        Abc_NtkHasOnlyLatchBoxes(Abc_Ntk_t * pNtk ){ return Abc_NtkLatchNum(pNtk) == Abc_NtkBoxNum(pNtk); }
 
 // creating simple objects
-extern inline Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
+extern        Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
 static inline Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PI );         }
 static inline Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PO );         }
 static inline Abc_Obj_t * Abc_NtkCreateBi( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BI );         }
@@ -417,8 +417,8 @@ static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )          { return Ab
 static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) );  }
 static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );    }
 static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );    }
-static inline Abc_Obj_t * Abc_ObjChild0Data( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pData, Abc_ObjFaninC0(pObj) );    }
-static inline Abc_Obj_t * Abc_ObjChild1Data( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pData, Abc_ObjFaninC1(pObj) );    }
+static inline Abc_Obj_t * Abc_ObjChild0Data( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( (Abc_Obj_t *)Abc_ObjFanin0(pObj)->pData, Abc_ObjFaninC0(pObj) );    }
+static inline Abc_Obj_t * Abc_ObjChild1Data( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( (Abc_Obj_t *)Abc_ObjFanin1(pObj)->pData, Abc_ObjFaninC1(pObj) );    }
 static inline Hop_Obj_t * Abc_ObjChild0Equiv( Abc_Obj_t * pObj )     { return Hop_NotCond( Abc_ObjFanin0(pObj)->pEquiv, Abc_ObjFaninC0(pObj) );      }
 static inline Hop_Obj_t * Abc_ObjChild1Equiv( Abc_Obj_t * pObj )     { return Hop_NotCond( Abc_ObjFanin1(pObj)->pEquiv, Abc_ObjFaninC1(pObj) );      }
 
@@ -452,17 +452,17 @@ static inline int         Abc_LatchInit( Abc_Obj_t * pLatch )        { assert(Ab
 
 // global BDDs of the nodes
 static inline void *      Abc_NtkGlobalBdd( Abc_Ntk_t * pNtk )          { return (void *)Vec_PtrEntry(pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD);             }
-static inline DdManager * Abc_NtkGlobalBddMan( Abc_Ntk_t * pNtk )       { return (DdManager *)Vec_AttMan( Abc_NtkGlobalBdd(pNtk) );                   }
-static inline DdNode **   Abc_NtkGlobalBddArray( Abc_Ntk_t * pNtk )     { return (DdNode **)Vec_AttArray( Abc_NtkGlobalBdd(pNtk) );                   }
-static inline DdNode *    Abc_ObjGlobalBdd( Abc_Obj_t * pObj )          { return (DdNode *)Vec_AttEntry( Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id );    }
-static inline void        Abc_ObjSetGlobalBdd( Abc_Obj_t * pObj, DdNode * bF )   { Vec_AttWriteEntry( Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id, bF );   }
+static inline DdManager * Abc_NtkGlobalBddMan( Abc_Ntk_t * pNtk )       { return (DdManager *)Vec_AttMan( (Vec_Att_t *)Abc_NtkGlobalBdd(pNtk) );                   }
+static inline DdNode **   Abc_NtkGlobalBddArray( Abc_Ntk_t * pNtk )     { return (DdNode **)Vec_AttArray( (Vec_Att_t *)Abc_NtkGlobalBdd(pNtk) );                   }
+static inline DdNode *    Abc_ObjGlobalBdd( Abc_Obj_t * pObj )          { return (DdNode *)Vec_AttEntry( (Vec_Att_t *)Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id );    }
+static inline void        Abc_ObjSetGlobalBdd( Abc_Obj_t * pObj, DdNode * bF )   { Vec_AttWriteEntry( (Vec_Att_t *)Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id, bF );   }
 
 // MV variables of the nodes
 static inline void *      Abc_NtkMvVar( Abc_Ntk_t * pNtk )              { return Vec_PtrEntry(pNtk->vAttrs, VEC_ATTR_MVVAR);                          }
-static inline void *      Abc_NtkMvVarMan( Abc_Ntk_t * pNtk )           { return Abc_NtkMvVar(pNtk)? Vec_AttMan( Abc_NtkMvVar(pNtk) ) : NULL;         }
-static inline void *      Abc_ObjMvVar( Abc_Obj_t * pObj )              { return Abc_NtkMvVar(pObj->pNtk)? Vec_AttEntry( Abc_NtkMvVar(pObj->pNtk), pObj->Id ) : NULL; }
+static inline void *      Abc_NtkMvVarMan( Abc_Ntk_t * pNtk )           { return Abc_NtkMvVar(pNtk)? Vec_AttMan( (Vec_Att_t *)Abc_NtkMvVar(pNtk) ) : NULL;         }
+static inline void *      Abc_ObjMvVar( Abc_Obj_t * pObj )              { return Abc_NtkMvVar(pObj->pNtk)? Vec_AttEntry( (Vec_Att_t *)Abc_NtkMvVar(pObj->pNtk), pObj->Id ) : NULL; }
 static inline int         Abc_ObjMvVarNum( Abc_Obj_t * pObj )           { return (Abc_NtkMvVar(pObj->pNtk) && Abc_ObjMvVar(pObj))? *((int*)Abc_ObjMvVar(pObj)) : 2;   }
-static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_AttWriteEntry( Abc_NtkMvVar(pObj->pNtk), pObj->Id, pV );                }
+static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_AttWriteEntry( (Vec_Att_t *)Abc_NtkMvVar(pObj->pNtk), pObj->Id, pV );                }
 
 // outputs the runtime in seconds
 #define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))

src/base/abci/abc.c

@@ -329,6 +329,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Abc_NtkPrint256();
 //    Kit_TruthCountMintermsPrecomp();
 //    Kit_DsdPrecompute4Vars();
+
+    Dar_LibStart();
 } 
 
 /**Function*************************************************************
@@ -344,6 +346,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
 ***********************************************************************/
 void Abc_End()
 {
+    Dar_LibStop();
+
     Abc_NtkFraigStoreClean();
 //    Rwt_Man4ExplorePrint();
 }
@@ -6034,13 +6038,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 //    Abc_NtkCompareSupports( pNtk );
 //    Abc_NtkCompareCones( pNtk );
-
+/*
     {
         extern Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int fVerbose );
         Vec_Vec_t * vParts;
         vParts = Abc_NtkPartitionSmart( pNtk, 1 );
         Vec_VecFree( vParts );
     }
+*/
+//    Abc_Ntk4VarTable( pNtk );
+//    Dat_NtkGenerateArrays( pNtk );
 
     return 0;
 
@@ -7677,7 +7684,8 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fUseInv;
     int fExdc;
     int fVerbose;
-    extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
+    int fVeryVerbose;
+    extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -7687,8 +7695,9 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     fUseInv   = 1;
     fExdc     = 0;
     fVerbose  = 0;
+    fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ievh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ievwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7701,6 +7710,9 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             fVerbose ^= 1;
             break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -7724,7 +7736,7 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     // modify the current network
-    if ( !Abc_NtkFraigSweep( pNtk, fUseInv, fExdc, fVerbose ) )
+    if ( !Abc_NtkFraigSweep( pNtk, fUseInv, fExdc, fVerbose, fVeryVerbose ) )
     {
         fprintf( pErr, "Sweeping has failed.\n" );
         return 1;
@@ -7732,10 +7744,11 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: fraig_sweep [-evh]\n" );
+    fprintf( pErr, "usage: fraig_sweep [-evwh]\n" );
     fprintf( pErr, "\t        performs technology-dependent sweep\n" );
     fprintf( pErr, "\t-e    : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" );
     fprintf( pErr, "\t-v    : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-w    : prints equivalence class information [default = %s]\n", fVeryVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -8284,7 +8297,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     int c;
     extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose );
-    extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
+    extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -8375,7 +8388,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     if ( fSweep )
-        Abc_NtkFraigSweep( pNtkRes, 0, 0, 0 );
+        Abc_NtkFraigSweep( pNtkRes, 0, 0, 0, 0 );
 
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -10346,11 +10359,12 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nPartSize;
     int nConfLimit;
     int nInsLimit;
+    int fPartition;
 
     extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit );
     extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
     extern void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nPartSize, int fVerbose );
-
+    extern void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10363,8 +10377,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     nPartSize  = 0;
     nConfLimit = 10000;   
     nInsLimit  = 0;
+    fPartition = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "TCIPsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "TCIPpsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10412,6 +10427,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nPartSize < 0 ) 
                 goto usage;
             break;
+        case 'p':
+            fPartition ^= 1;
+            break;
         case 's':
             fSat ^= 1;
             break;
@@ -10429,7 +10447,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
 
     // perform equivalence checking
-    if ( nPartSize )
+    if ( fPartition )
+        Abc_NtkCecFraigPartAuto( pNtk1, pNtk2, nSeconds, fVerbose );
+    else if ( nPartSize )
         Abc_NtkCecFraigPart( pNtk1, pNtk2, nSeconds, nPartSize, fVerbose );
     else if ( fSat )
         Abc_NtkCecSat( pNtk1, pNtk2, nConfLimit, nInsLimit );
@@ -10445,12 +10465,13 @@ usage:
         strcpy( Buffer, "unused" );
     else
         sprintf( Buffer, "%d", nPartSize );
-    fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-P num] [-svh] <file1> <file2>\n" );
+    fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-P num] [-psvh] <file1> <file2>\n" );
     fprintf( pErr, "\t         performs combinational equivalence checking\n" );
     fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     fprintf( pErr, "\t-I num : limit on the number of clause inspections [default = %d]\n", nInsLimit );
     fprintf( pErr, "\t-P num : partition size for multi-output networks [default = %s]\n", Buffer );
+    fprintf( pErr, "\t-p     : toggle automatic partitioning [default = %s]\n", fPartition? "yes": "no" );
     fprintf( pErr, "\t-s     : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");

src/base/abci/abcDar.c

+/**CFile****************************************************************
+
+  FileName    [abcDar.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [DAG-aware rewriting.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcDar.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkAig;
+    Dar_Man_t * pMan;//, * pTemp;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // convert to the AIG manager
+    pMan = Abc_NtkToDar( pNtk );
+    if ( pMan == NULL )
+        return NULL;
+    if ( !Dar_ManCheck( pMan ) )
+    {
+        printf( "Abc_NtkDar: AIG check has failed.\n" );
+        Dar_ManStop( pMan );
+        return NULL;
+    }
+    // perform balance
+    Dar_ManPrintStats( pMan );
+//    Dar_ManDumpBlif( pMan, "aig_temp.blif" );
+    pMan->pPars = Dar_ManDefaultParams();
+    Dar_ManRewrite( pMan );
+    Dar_ManPrintStats( pMan );
+    // convert from the AIG manager
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    if ( pNtkAig == NULL )
+        return NULL;
+    Dar_ManStop( pMan );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_NtkDar: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+    }
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
+{
+    Dar_Man_t * pMan;
+    Abc_Obj_t * pObj;
+    int i;
+    // create the manager
+    pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) );
+    // transfer the pointers to the basic nodes
+    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Dar_ManConst1(pMan);
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Dar_ObjCreatePi(pMan);
+    // perform the conversion of the internal nodes (assumes DFS ordering)
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Dar_And( pMan, (Dar_Obj_t *)Abc_ObjChild0Copy(pObj), (Dar_Obj_t *)Abc_ObjChild1Copy(pObj) );
+    // create the POs
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Dar_ObjCreatePo( pMan, (Dar_Obj_t *)Abc_ObjChild0Copy(pObj) );
+    Dar_ManCleanup( pMan );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew;
+    Dar_Obj_t * pObj;
+    int i;
+    // perform strashing
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // transfer the pointers to the basic nodes
+    Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+    Dar_ManForEachPi( pMan, pObj, i )
+        pObj->pData = Abc_NtkCi(pNtkNew, i);
+    // rebuild the AIG
+    vNodes = Dar_ManDfs( pMan );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Dar_ObjChild0Copy(pObj), (Abc_Obj_t *)Dar_ObjChild1Copy(pObj) );
+    Vec_PtrFree( vNodes );
+    // connect the PO nodes
+    Dar_ManForEachPo( pMan, pObj, i )
+        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Dar_ObjChild0Copy(pObj) );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abci/abcDsdRes.c

@@ -994,6 +994,73 @@ If_Obj_t * Abc_LutIfManMap_New_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit
 
 /**Function*************************************************************
 
+  Synopsis    [Find the best cofactoring variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+int Abc_LutFindBestCofactoring( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
+{
+    Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp;
+//    Kit_DsdObj_t * pRoot;
+    unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
+    unsigned i, * pTruth;
+    int MaxBlock
+        Verbose = 0;
+    int RetValue = 0;
+
+    if ( fVerbose )
+    {
+        printf( "Function: " );
+//        Extra_PrintBinary( stdout, pTruth, (1 << nVars) ); 
+        Extra_PrintHexadecimal( stdout, pTruth, nVars ); 
+        printf( "\n" );
+        Kit_DsdPrint( stdout, pNtk );
+    }
+    for ( i = 0; i < nVars; i++ )
+    {
+        Kit_TruthCofactor0New( pCofs2[0], pTruth, nVars, i );
+        pNtk0 = Kit_DsdDecompose( pCofs2[0], nVars );
+        pNtk0 = Kit_DsdExpand( pTemp = pNtk0 );
+        Kit_DsdNtkFree( pTemp );
+
+        if ( fVerbose )
+        {
+            printf( "Cof%d0: ", i );
+            Kit_DsdPrint( stdout, pNtk0 );
+        }
+
+        Kit_TruthCofactor1New( pCofs2[1], pTruth, nVars, i );
+        pNtk1 = Kit_DsdDecompose( pCofs2[1], nVars );
+        pNtk1 = Kit_DsdExpand( pTemp = pNtk1 );
+        Kit_DsdNtkFree( pTemp );
+
+        if ( fVerbose )
+        {
+            printf( "Cof%d1: ", i );
+            Kit_DsdPrint( stdout, pNtk1 );
+        }
+
+        if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) )
+            RetValue = 1;
+
+        Kit_DsdNtkFree( pNtk0 );
+        Kit_DsdNtkFree( pNtk1 );
+    }
+    if ( fVerbose )
+        printf( "\n" );
+
+    return RetValue;
+    
+}
+*/
+/**Function*************************************************************
+
   Synopsis    [Prepares the mapping manager.]
 
   Description []
@@ -1220,6 +1287,7 @@ clk = clock();
         pTruth = Abc_LutCutTruth( p, pCut );
 p->timeTruth += clock() - clk;
 
+
 /*
         // evaluate the result of decomposition        
         Result = Kit_DsdEval( pTruth, pCut->nLeaves, 3 );
@@ -1247,6 +1315,18 @@ p->timeEval += clock() - clk;
             continue;
         }
 */
+  
+/*        
+        if ( pCut->nLeaves > 6 && pCut->nLeaves < 12 && Kit_DsdNonDsdSizeMax(pDsdNtk) == pCut->nLeaves )
+        {
+//            Abc_NtkPrintMeasures( pTruth, pCut->nLeaves );
+//            Kit_DsdTestCofs( pDsdNtk, pTruth );
+
+//            Abc_NtkPrintOneDecomp( pTruth, pCut->nLeaves );
+            Abc_NtkPrintOneDec( pTruth, pCut->nLeaves );
+        }
+*/
+
         if ( p->pPars->fVeryVerbose )
         {
 //            Extra_PrintHexadecimal( stdout, pTruth, pCut->nLeaves ); printf( "\n" );

src/base/abci/abcIvy.c

@@ -525,6 +525,8 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
     if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
     {
         pParams->fUseRewriting = 0;
+        pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
+        Abc_NtkDelete( pNtkTemp );
         Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
         pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
         Abc_NtkDelete( pNtkTemp );

src/base/abci/abcPart.c

@@ -74,9 +74,9 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Int_t * vOne )
+int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, int nPartSizeLimit, Vec_Int_t * vOne )
 {
-    Vec_Int_t * vPartSupp;
+    Vec_Int_t * vPartSupp, * vPart;
     double Attract, Repulse, Cost, CostBest;
     int i, nCommon, iBest;
     iBest = -1;
@@ -84,6 +84,11 @@ int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Int_t * vOne )
     Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i )
     {
         nCommon = Vec_IntTwoCountCommon( vPartSupp, vOne );
+        if ( nCommon == 0 )
+            continue;
+        vPart = Vec_PtrEntry( vPartsAll, i );
+        if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) > nPartSizeLimit )
+            continue;
         if ( nCommon == Vec_IntSize(vOne) )
             return i;
         Attract = 1.0 * nCommon / Vec_IntSize(vOne);
@@ -143,17 +148,20 @@ void Abc_NtkPartitionPrint( Abc_Ntk_t * pNtk, Vec_Ptr_t * vPartsAll, Vec_Ptr_t *
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll )
+void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll, int nPartSizeLimit )
 {
     Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
     int i, iPart;
 
+    if ( nPartSizeLimit == 0 )
+        nPartSizeLimit = 200;
+
     // pack smaller partitions into larger blocks
     iPart = 0;
     vPart = vPartSupp = NULL;
     Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
     {
-        if ( Vec_IntSize(vOne) < 200 )
+        if ( Vec_IntSize(vOne) < nPartSizeLimit )
         {
             if ( vPartSupp == NULL )
             {
@@ -169,7 +177,7 @@ void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll )
                 Vec_IntFree( vTemp );
                 Vec_IntFree( Vec_PtrEntry(vPartsAll, i) );
             }
-            if ( Vec_IntSize(vPartSupp) < 200 )
+            if ( Vec_IntSize(vPartSupp) < nPartSizeLimit )
                 continue;
         }
         else
@@ -212,7 +220,7 @@ void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int fVerbose )
+Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose )
 {
     Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll, * vPartPtr;
     Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
@@ -235,7 +243,7 @@ clk = clock();
         // get the output number
         iOut = Vec_IntPop(vOne);
         // find closely matching part
-        iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vOne );
+        iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vPartsAll, nPartSizeLimit, vOne );
         if ( iPart == -1 )
         {
             // create new partition
@@ -280,7 +288,7 @@ clk = clock();
 
     // compact small partitions
 //    Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
-    Abc_NtkPartitionCompact( vPartsAll, vPartSuppsAll );
+    Abc_NtkPartitionCompact( vPartsAll, vPartSuppsAll, nPartSizeLimit );
     if ( fVerbose )
     Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
 if ( fVerbose )
@@ -668,7 +676,7 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
     // perform partitioning
     assert( Abc_NtkIsStrash(pNtk) );
 //    vParts = Abc_NtkPartitionNaive( pNtk, 20 );
-    vParts = Abc_NtkPartitionSmart( pNtk, 0 );
+    vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
 
     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
 

src/base/abci/abcSweep.c

@@ -26,7 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static void           Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
-static stmm_table *   Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose );
+static stmm_table *   Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose, int fVeryVerbose );
 static void           Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv, bool fVerbose );
 static void           Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
 static void           Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
@@ -54,7 +54,7 @@ static void           Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pF
   SeeAlso     []
 
 ***********************************************************************/
-bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
+bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose )
 {
     Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig;
@@ -100,9 +100,11 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
         else
             Abc_NtkFraigSweepUsingExdc( pMan, pNtk );
     }
+    // assign levels to the nodes of the network
+    Abc_NtkLevel( pNtk );
 
     // collect the classes of equivalent nets
-    tEquiv = Abc_NtkFraigEquiv( pNtk, fUseInv, fVerbose );
+    tEquiv = Abc_NtkFraigEquiv( pNtk, fUseInv, fVerbose, fVeryVerbose );
 
     // transform the network into the equivalent one
     Abc_NtkFraigTransform( pNtk, tEquiv, fUseInv, fVerbose );
@@ -113,7 +115,11 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
     Abc_NtkDelete( pNtkAig );
 
     // cleanup the dangling nodes
+    if ( Abc_NtkHasMapping(pNtk) )
         Abc_NtkCleanup( pNtk, fVerbose );
+    else
+        Abc_NtkSweep( pNtk, fVerbose );
+
     // check
     if ( !Abc_NtkCheck( pNtk ) )
     {
@@ -175,7 +181,7 @@ void Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose )
+stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose, int fVeryVerbose )
 {
     Abc_Obj_t * pList, * pNode, * pNodeAig;
     Fraig_Node_t * gNode;
@@ -225,22 +231,22 @@ stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose )
         // count nodes in the non-trival classes
         for ( pNode = pList; pNode; pNode = pNode->pNext )
             Counter++;
-/*
-        if ( fVerbose )
+
+        if ( fVeryVerbose )
         {
             printf( "Class %2d : {", c );
             for ( pNode = pList; pNode; pNode = pNode->pNext )
             {
                 pNode->pCopy = NULL;
                 printf( " %s", Abc_ObjName(pNode) );
-                if ( pNode->fPhase )  printf( "(*)" );
+                printf( "(%c)", pNode->fPhase? '-' : '+' );
+                printf( "(%d)", pNode->Level );
             }
             printf( " }\n" );
             c++;
         }
-*/
     }
-    if ( fVerbose )
+    if ( fVerbose || fVeryVerbose )
     {
         printf( "Sweeping stats for network \"%s\":\n", pNtk->pName );
         printf( "Internal nodes = %d. Different functions (up to compl) = %d.\n", Abc_NtkNodeNum(pNtk), stmm_count(tStrash2Net) );
@@ -268,8 +274,6 @@ void Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv,
     Abc_Obj_t * pList;
     if ( stmm_count(tEquiv) == 0 )
         return;
-    // assign levels to the nodes of the network
-    Abc_NtkLevel( pNtk );
     // merge nodes in the classes
     if ( Abc_NtkHasMapping( pNtk ) )
     {

src/base/abci/abcVerify.c

@@ -313,6 +313,123 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
 
 /**Function*************************************************************
 
+  Synopsis    [Verifies sequential equivalence by fraiging followed by SAT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
+{
+    extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
+    extern Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose );
+    extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+    extern void * Abc_FrameGetGlobalFrame();
+
+    Vec_Vec_t * vParts;
+    Vec_Ptr_t * vOne;
+    Prove_Params_t Params, * pParams = &Params;
+    Abc_Ntk_t * pMiter, * pMiterPart;
+    int i, RetValue, Status, nOutputs;
+
+    // solve the CNF using the SAT solver
+    Prove_ParamsSetDefault( pParams );
+    pParams->nItersMax = 5;
+    //    pParams->fVerbose = 1;
+
+    // get the miter of the two networks
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1 );
+    if ( pMiter == NULL )
+    {
+        printf( "Miter computation has failed.\n" );
+        return;
+    }
+    RetValue = Abc_NtkMiterIsConstant( pMiter );
+    if ( RetValue == 0 )
+    {
+        printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
+        // report the error
+        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
+        Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
+        FREE( pMiter->pModel );
+        Abc_NtkDelete( pMiter );
+        return;
+    }
+    if ( RetValue == 1 )
+    {
+        printf( "Networks are equivalent after structural hashing.\n" );
+        Abc_NtkDelete( pMiter );
+        return;
+    }
+
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
+
+    // partition the outputs
+    vParts = Abc_NtkPartitionSmart( pMiter, 50, 0 );
+
+    // fraig each partition
+    Status = 1;
+    nOutputs = 0;
+    Vec_VecForEachLevel( vParts, vOne, i )
+    {
+        // get this part of the miter
+        pMiterPart = Abc_NtkCreateConeArray( pMiter, vOne, 0 );
+        Abc_NtkCombinePos( pMiterPart, 0 );
+        // check the miter for being constant
+        RetValue = Abc_NtkMiterIsConstant( pMiterPart );
+        if ( RetValue == 0 )
+        {
+            printf( "Networks are NOT EQUIVALENT after partitioning.\n" );
+            Abc_NtkDelete( pMiterPart );
+            break;
+        }
+        if ( RetValue == 1 )
+        {
+            Abc_NtkDelete( pMiterPart );
+            continue;
+        }
+        // solve the problem
+        RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
+        if ( RetValue == -1 )
+        {
+            printf( "Networks are undecided (resource limits is reached).\r" );
+            Status = -1;
+        }
+        else if ( RetValue == 0 )
+        {
+            int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiterPart, pMiterPart->pModel );
+            if ( pSimInfo[0] != 1 )
+                printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
+            else
+                printf( "Networks are NOT EQUIVALENT.                 \n" );
+            free( pSimInfo );
+            Status = 0;
+            Abc_NtkDelete( pMiterPart );
+            break;
+        }
+        else
+        {
+            printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) );
+            nOutputs += Vec_PtrSize(vOne);
+        }
+        Abc_NtkDelete( pMiterPart );
+    }
+    Vec_VecFree( vParts );
+
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
+
+    if ( Status == 1 )
+        printf( "Networks are equivalent.                         \n" );
+    else if ( Status == -1 )
+        printf( "Timed out after verifying %d outputs (out of %d).\n", nOutputs, Abc_NtkCoNum(pNtk1) );
+    Abc_NtkDelete( pMiter );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Verifies sequential equivalence by brute-force SAT.]
 
   Description []

src/base/abci/module.make

@@ -7,6 +7,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcClpBdd.c \
     src/base/abci/abcClpSop.c \
     src/base/abci/abcCut.c \
+    src/base/abci/abcDar.c \
     src/base/abci/abcDebug.c \
     src/base/abci/abcDress.c \
     src/base/abci/abcDsd.c \

src/base/abci/xaaaa.c

+/**CFile****************************************************************
+
+  FileName    [abc_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintMeasures( unsigned * pTruth, int nVars )
+{
+    unsigned uCofs[10][32];
+    int i, k, nOnes;
+
+    // total pairs
+    nOnes =  Kit_TruthCountOnes( uCofs[0], nVars );
+    printf( "Total = %d.\n", nOnes * ((1 << nVars) - nOnes) );
+
+    // print measures for individual variables
+    for ( i = 0; i < nVars; i++ )
+    {
+        Kit_TruthUniqueNew( uCofs[0], pTruth, nVars, i );
+        nOnes = Kit_TruthCountOnes( uCofs[0], nVars );
+        printf( "%7d ", nOnes );
+    }
+    printf( "\n" );
+
+    // consider pairs
+    for ( i = 0; i < nVars; i++ )
+    for ( k = 0; k < nVars; k++ )
+    {
+        if ( i == k )
+        {
+            printf( "        " );
+            continue;
+        }
+        Kit_TruthCofactor0New( uCofs[0], pTruth, nVars, i );
+        Kit_TruthCofactor1New( uCofs[1], pTruth, nVars, i );
+
+        Kit_TruthCofactor0New( uCofs[2], uCofs[0], nVars, k ); // 00
+        Kit_TruthCofactor1New( uCofs[3], uCofs[0], nVars, k ); // 01
+        Kit_TruthCofactor0New( uCofs[4], uCofs[1], nVars, k ); // 10
+        Kit_TruthCofactor1New( uCofs[5], uCofs[1], nVars, k ); // 11
+
+        Kit_TruthAndPhase( uCofs[6], uCofs[2], uCofs[5], nVars, 0, 1 ); // 00  & 11'
+        Kit_TruthAndPhase( uCofs[7], uCofs[2], uCofs[5], nVars, 1, 0 ); // 00' & 11
+        Kit_TruthAndPhase( uCofs[8], uCofs[3], uCofs[4], nVars, 0, 1 ); // 01  & 10'
+        Kit_TruthAndPhase( uCofs[9], uCofs[3], uCofs[4], nVars, 1, 0 ); // 01' & 10
+
+        nOnes = Kit_TruthCountOnes( uCofs[6], nVars ) + 
+                Kit_TruthCountOnes( uCofs[7], nVars ) + 
+                Kit_TruthCountOnes( uCofs[8], nVars ) + 
+                Kit_TruthCountOnes( uCofs[9], nVars );
+
+        printf( "%7d ", nOnes );
+        if ( k == nVars - 1 )
+            printf( "\n" );
+    }
+    printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_Ntk4VarTable( Abc_Ntk_t * pNtk )
+{
+    static u4VarTts[222] = {
+        0x0000, 0x0001, 0x0003, 0x0006, 0x0007, 0x000f, 0x0016, 0x0017, 0x0018, 0x0019, 
+        0x001b, 0x001e, 0x001f, 0x003c, 0x003d, 0x003f, 0x0069, 0x006b, 0x006f, 0x007e, 
+        0x007f, 0x00ff, 0x0116, 0x0117, 0x0118, 0x0119, 0x011a, 0x011b, 0x011e, 0x011f, 
+        0x012c, 0x012d, 0x012f, 0x013c, 0x013d, 0x013e, 0x013f, 0x0168, 0x0169, 0x016a, 
+        0x016b, 0x016e, 0x016f, 0x017e, 0x017f, 0x0180, 0x0181, 0x0182, 0x0183, 0x0186, 
+        0x0187, 0x0189, 0x018b, 0x018f, 0x0196, 0x0197, 0x0198, 0x0199, 0x019a, 0x019b, 
+        0x019e, 0x019f, 0x01a8, 0x01a9, 0x01aa, 0x01ab, 0x01ac, 0x01ad, 0x01ae, 0x01af, 
+        0x01bc, 0x01bd, 0x01be, 0x01bf, 0x01e8, 0x01e9, 0x01ea, 0x01eb, 0x01ee, 0x01ef, 
+        0x01fe, 0x033c, 0x033d, 0x033f, 0x0356, 0x0357, 0x0358, 0x0359, 0x035a, 0x035b, 
+        0x035e, 0x035f, 0x0368, 0x0369, 0x036a, 0x036b, 0x036c, 0x036d, 0x036e, 0x036f, 
+        0x037c, 0x037d, 0x037e, 0x03c0, 0x03c1, 0x03c3, 0x03c5, 0x03c6, 0x03c7, 0x03cf, 
+        0x03d4, 0x03d5, 0x03d6, 0x03d7, 0x03d8, 0x03d9, 0x03db, 0x03dc, 0x03dd, 0x03de, 
+        0x03fc, 0x0660, 0x0661, 0x0662, 0x0663, 0x0666, 0x0667, 0x0669, 0x066b, 0x066f, 
+        0x0672, 0x0673, 0x0676, 0x0678, 0x0679, 0x067a, 0x067b, 0x067e, 0x0690, 0x0691, 
+        0x0693, 0x0696, 0x0697, 0x069f, 0x06b0, 0x06b1, 0x06b2, 0x06b3, 0x06b4, 0x06b5, 
+        0x06b6, 0x06b7, 0x06b9, 0x06bd, 0x06f0, 0x06f1, 0x06f2, 0x06f6, 0x06f9, 0x0776, 
+        0x0778, 0x0779, 0x077a, 0x077e, 0x07b0, 0x07b1, 0x07b4, 0x07b5, 0x07b6, 0x07bc, 
+        0x07e0, 0x07e1, 0x07e2, 0x07e3, 0x07e6, 0x07e9, 0x07f0, 0x07f1, 0x07f2, 0x07f8, 
+        0x0ff0, 0x1668, 0x1669, 0x166a, 0x166b, 0x166e, 0x167e, 0x1681, 0x1683, 0x1686, 
+        0x1687, 0x1689, 0x168b, 0x168e, 0x1696, 0x1697, 0x1698, 0x1699, 0x169a, 0x169b, 
+        0x169e, 0x16a9, 0x16ac, 0x16ad, 0x16bc, 0x16e9, 0x177e, 0x178e, 0x1796, 0x1798, 
+        0x179a, 0x17ac, 0x17e8, 0x18e7, 0x19e1, 0x19e3, 0x19e6, 0x1bd8, 0x1be4, 0x1ee1, 
+        0x3cc3, 0x6996
+    };
+    int Counters[222];
+
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i;
+
+    // set elementary truth tables
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj
+
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        vNodes = Abc_NtkDfsNodes( pNtk, &pObj, i );
+        Vec_PtrFree( vNodes );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/io/ioReadAiger.c

@@ -25,7 +25,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static unsigned Io_ReadAigerDecode( char ** ppPos );
+unsigned Io_ReadAigerDecode( char ** ppPos );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///

src/base/io/ioWriteAiger.c

@@ -129,7 +129,7 @@ static unsigned Io_ObjMakeLit( int Var, int fCompl )                 { return (V
 static unsigned Io_ObjAigerNum( Abc_Obj_t * pObj )                   { return (unsigned)pObj->pCopy;  }
 static void     Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num )  { pObj->pCopy = (void *)Num;     }
 
-static int      Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
+int      Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///

src/base/io/ioWriteVerilog.c

@@ -213,17 +213,33 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 ***********************************************************************/
 void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 {
-    Abc_Obj_t * pTerm, * pNet;
+    Abc_Obj_t * pTerm, * pNet, * pSkip;
     int LineLength;
     int AddedLength;
     int NameCounter;
     int i;
+    int nskip;
+
+    pSkip = 0;
+    nskip = 0;
 
     LineLength  = Start;
     NameCounter = 0;
     Abc_NtkForEachPo( pNtk, pTerm, i )
     {
         pNet = Abc_ObjFanin0(pTerm);
+        
+        if ( Abc_ObjIsPi(Abc_ObjFanin0(pNet)) )
+        {
+            // Skip this output since it is a feedthrough -- the same
+            // name will appear as an input and an output which other
+            // tools reading verilog do not like.
+            
+            nskip++;
+            pSkip = pNet;   // save an example of skipped net
+            continue;
+        }
+        
         // get the line length after this name is written
         AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
@@ -237,6 +253,14 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
         LineLength += AddedLength;
         NameCounter++;
     }
+
+    if (nskip != 0)
+    {
+        assert (pSkip);
+        printf( "Io_WriteVerilogPos(): Omitted %d feedthrough nets from output list of module (e.g. %s).\n", nskip, Abc_ObjName(pSkip) );
+        return;
+    }
+
 }
 
 /**Function*************************************************************

src/base/main/mainInt.h

@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#ifndef __Abc_INT_H__
-#define __Abc_INT_H__
+#ifndef __MAIN_INT_H__
+#define __MAIN_INT_H__
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///

src/misc/vec/vecPtr.h

@@ -196,7 +196,7 @@ static inline Vec_Ptr_t * Vec_PtrAllocTruthTables( int nVars )
     p = Vec_PtrAllocSimInfo( nVars, nWords );
     for ( i = 0; i < nVars; i++ )
     {
-        pTruth = p->pArray[i];
+        pTruth = (unsigned *)p->pArray[i];
         if ( i < 5 )
         {
             for ( k = 0; k < nWords; k++ )

src/opt/kit/kit.h

@@ -477,6 +477,7 @@ extern void            Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, in
 extern void            Kit_TruthForall( unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
+extern void            Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
 extern void            Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
 extern int             Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );

src/opt/kit/kitDsd.c

@@ -1068,7 +1068,7 @@ int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit )
 //    Kit_DsdObj_t * pRoot;
     unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
     unsigned i, * pTruth;
-    int fVerbose = 0;
+    int fVerbose = 1;
     int RetValue = 0;
 
     pTruth = pTruthInit;
@@ -1108,8 +1108,8 @@ int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit )
             Kit_DsdPrint( stdout, pNtk1 );
         }
 
-        if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) )
-            RetValue = 1;
+//        if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) )
+//            RetValue = 1;
 
         Kit_DsdNtkFree( pNtk0 );
         Kit_DsdNtkFree( pNtk1 );

src/opt/kit/kitTruth.c

@@ -769,6 +769,61 @@ void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar
 
 /**Function*************************************************************
 
+  Synopsis    [Universally quantifies the variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
+{
+    int nWords = Kit_TruthWordNum( nVars );
+    int i, k, Step;
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
+        return;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
+        return;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
+        return;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
+        return;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
+        return;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+            {
+                pRes[i]      = pTruth[i] ^ pTruth[Step+i];
+                pRes[Step+i] = pRes[i];
+            }
+            pRes += 2*Step;
+            pTruth += 2*Step;
+        }
+        return;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Universally quantifies the set of variables.]
 
   Description []