Version abc60825

16 files changed, 368 insertions, 177 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 1a3f3264..a921081b 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -787,7 +787,8 @@ extern int                Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkCleanNext( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NodeHasCoFanout( Abc_Obj_t * pNode );
+extern Abc_Obj_t *        Abc_NodeFindCoFanout( Abc_Obj_t * pNode );
+extern Abc_Obj_t *        Abc_NodeFindNonCoFanout( Abc_Obj_t * pNode );
 extern Abc_Obj_t *        Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode );
 extern bool               Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 7ffe7eac..7818cc05 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -744,6 +744,9 @@ void Abc_ConvertAigToBdd_rec2( DdManager * dd, Aig_Obj_t * pObj )
 DdNode * Abc_ConvertAigToBdd( DdManager * dd, Aig_Obj_t * pRoot )
 {
     DdNode * bFunc;
+    // check the case of a constant
+    if ( Aig_ObjIsConst1( Aig_Regular(pRoot) ) )
+        return Cudd_NotCond( Cudd_ReadOne(dd), Aig_IsComplement(pRoot) );
     // construct BDD
     Abc_ConvertAigToBdd_rec1( dd, Aig_Regular(pRoot) );
     // hold on to the result
diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c
index 604dd96e..13f422f4 100644
--- a/src/base/abc/abcMinBase.c
+++ b/src/base/abc/abcMinBase.c
@@ -112,12 +112,11 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
 int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
-    int i, Counter, fChanged;
+    int i, Counter;
     assert( Abc_NtkIsBddLogic(pNtk) );
     Counter = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
-        while ( fChanged = Abc_NodeRemoveDupFanins(pNode) )
-            Counter += fChanged;
+        Counter += Abc_NodeRemoveDupFanins( pNode );
     return Counter;
 }
 
@@ -132,7 +131,7 @@ int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode )
+int Abc_NodeRemoveDupFanins_int( Abc_Obj_t * pNode )
 {
     Abc_Obj_t * pFanin1, * pFanin2;
     int i, k;
@@ -165,6 +164,24 @@ int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Removes duplicated fanins if present.]
+
+  Description [Returns the number of fanins removed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode )
+{
+    int Counter = 0;
+    while ( Abc_NodeRemoveDupFanins_int(pNode) )
+        Counter++;
+    return Counter;
+}
+/**Function*************************************************************
+
   Synopsis    [Computes support of the node.]
 
   Description []
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 0650896d..f71093ef 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -321,6 +321,9 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pNet, * pDriver, * pFanin;
     int i, k;
 
+    // remove dangling nodes
+    Abc_NtkCleanup( pNtk, 0 );
+
     assert( Abc_NtkIsLogic(pNtk) );
     assert( Abc_NtkLogicHasSimpleCos(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
@@ -340,11 +343,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
     }
     // duplicate all nodes
     Abc_NtkForEachNode( pNtk, pObj, i )
-    {
-        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
-            continue;
         Abc_NtkDupObj(pNtkNew, pObj, 0);
-    }
     // first add the nets to the CO drivers
     Abc_NtkForEachCo( pNtk, pObj, i )
     {
@@ -367,13 +366,14 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
             pDriver->pCopy->pCopy = pNet;
         }
         else
+        {
             assert( !strcmp( Abc_ObjName(pDriver->pCopy->pCopy), Abc_ObjName(pObj) ) );
+            Abc_ObjAddFanin( pObj->pCopy, pDriver->pCopy->pCopy );
+        }
     }
     // create the missing nets
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
-        if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
-            continue;
         if ( pObj->pCopy->pCopy ) // the net of the new object is already created
             continue;
         // create the new net
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 37461c22..d7283d55 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -767,6 +767,12 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNet, * pNode;
     int i;
 
+    if ( Abc_NtkNodeNum(pNtk) == 0 )
+    {
+        pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
+        return;
+    }
+
     // check for non-driven nets
     vNets = Vec_PtrAlloc( 100 );
     Abc_NtkForEachNet( pNtk, pNet, i )
@@ -784,7 +790,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
     // print the warning
     if ( vNets->nSize > 0 )
     {
-        printf( "Constant-zero drivers were added to %d non-driven nets:\n", vNets->nSize );
+        printf( "Constant-zero drivers were added to %d non-driven nets in network %s:\n", vNets->nSize, pNtk->pName );
         for ( i = 0; i < vNets->nSize; i++ )
         {
             if ( i == 0 )
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 2dbfef33..6e506b0e 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -444,12 +444,10 @@ void Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeHasCoFanout( Abc_Obj_t * pNode )
+Abc_Obj_t * Abc_NodeFindCoFanout( Abc_Obj_t * pNode )
 {
     Abc_Obj_t * pFanout;
     int i;
-    if ( !Abc_ObjIsNode(pNode) )
-        return NULL;
     Abc_ObjForEachFanout( pNode, pFanout, i )
         if ( Abc_ObjIsCo(pFanout) )
             return pFanout;
@@ -458,9 +456,30 @@ Abc_Obj_t * Abc_NodeHasCoFanout( Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Checks if the internal node has CO fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeFindNonCoFanout( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        if ( !Abc_ObjIsCo(pFanout) )
+            return pFanout;
+    return NULL;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks if the internal node has CO drivers with the same name.]
 
-  Description [Checks if the internal node can borrow a name from CO fanouts. 
+  Description [Checks if the internal node can borrow its name from CO fanouts. 
   This is possible if all COs with non-complemented fanin edge pointing to this 
   node have the same name.]
                
@@ -473,8 +492,6 @@ Abc_Obj_t * Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode )
 {
     Abc_Obj_t * pFanout, * pFanoutCo;
     int i;
-    if ( !Abc_ObjIsNode(pNode) )
-        return NULL;
     pFanoutCo = NULL;
     Abc_ObjForEachFanout( pNode, pFanout, i )
     {
@@ -497,13 +514,60 @@ Abc_Obj_t * Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Fixes the CO driver problem.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFixCoDriverProblem( Abc_Obj_t * pDriver, Abc_Obj_t * pNodeCo, int fDuplicate )
+{
+    Abc_Ntk_t * pNtk = pDriver->pNtk;
+    Abc_Obj_t * pDriverNew, * pFanin;
+    int k;
+    if ( fDuplicate && !Abc_ObjIsCi(pDriver) )
+    {
+        pDriverNew = Abc_NtkDupObj( pNtk, pDriver, 0 ); 
+        Abc_ObjForEachFanin( pDriver, pFanin, k )
+            Abc_ObjAddFanin( pDriverNew, pFanin );
+        if ( Abc_ObjFaninC0(pNodeCo) )
+        {
+            // change polarity of the duplicated driver
+            Abc_NodeComplement( pDriverNew );
+            Abc_ObjXorFaninC( pNodeCo, 0 );
+        }
+    }
+    else
+    {
+        // add inverters and buffers when necessary
+        if ( Abc_ObjFaninC0(pNodeCo) )
+        {
+            pDriverNew = Abc_NodeCreateInv( pNtk, pDriver );
+            Abc_ObjXorFaninC( pNodeCo, 0 );
+        }
+        else
+            pDriverNew = Abc_NodeCreateBuf( pNtk, pDriver );        
+    }
+    // update the fanin of the PO node
+    Abc_ObjPatchFanin( pNodeCo, pDriver, pDriverNew );
+    assert( Abc_ObjFanoutNum(pDriverNew) == 1 );
+    // remove the old driver if it dangles
+    // (this happens when the duplicated driver had only one complemented fanout)
+    if ( Abc_ObjFanoutNum(pDriver) == 0 )
+        Abc_NtkDeleteObj( pDriver );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if COs of a logic network are simple.]
 
   Description [The COs of a logic network are simple under three conditions:
   (1) The edge from CO to its driver is not complemented.
-  (2) No two COs share the same driver. 
-  (3) The driver is not a CI unless the CI and the CO have the same name 
-  (and so the inv/buf should not be written into a file).]
+  (2) If CI is a driver of a CO, they have the same name.]
+  (2) If two COs share the same driver, they have the same name.]
                
   SideEffects []
 
@@ -514,19 +578,27 @@ bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode, * pDriver;
     int i;
-    assert( !Abc_NtkIsNetlist(pNtk) );
-    // check if there are complemented or idential POs
+    assert( Abc_NtkIsLogic(pNtk) );
     Abc_NtkIncrementTravId( pNtk );
     Abc_NtkForEachCo( pNtk, pNode, i ) 
     {
+        // if the driver is complemented, this is an error
         pDriver = Abc_ObjFanin0(pNode);
         if ( Abc_ObjFaninC0(pNode) )
             return 0;
-        if ( Abc_NodeIsTravIdCurrent(pDriver) )
+        // if the driver is a CI and has different name, this is an error
+        if ( Abc_ObjIsCi(pDriver) && strcmp(Abc_ObjName(pDriver), Abc_ObjName(pNode)) )
             return 0;
-        if ( Abc_ObjIsCi(pDriver) && strcmp( Abc_ObjName(pDriver), Abc_ObjName(pNode) ) != 0 )
+        // if the driver is visited for the first time, remember the CO name
+        if ( !Abc_NodeIsTravIdCurrent(pDriver) )
+        {
+            pDriver->pNext = (Abc_Obj_t *)Abc_ObjName(pNode);
+            Abc_NodeSetTravIdCurrent(pDriver);
+            continue;
+        }
+        // the driver has second CO - if they have different name, this is an error
+        if ( strcmp((char *)pDriver->pNext, Abc_ObjName(pNode)) ) // diff names
             return 0;
-        Abc_NodeSetTravIdCurrent(pDriver);
     }
     return 1;
 }
@@ -536,10 +608,9 @@ bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk )
   Synopsis    [Transforms the network to have simple COs.]
 
   Description [The COs of a logic network are simple under three conditions:
-  (1) The edge from the CO to its driver is not complemented.
-  (2) No two COs share the same driver (unless they have the same name!). 
-  (3) The driver is not a CI unless the CI and the CO have the same name 
-  (and so the inv/buf should not be written into a file).
+  (1) The edge from CO to its driver is not complemented.
+  (2) If CI is a driver of a CO, they have the same name.]
+  (2) If two COs share the same driver, they have the same name.
   In some cases, such as FPGA mapping, we prevent the increase in delay
   by duplicating the driver nodes, rather than adding invs/bufs.]
                
@@ -550,58 +621,41 @@ bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate )
 {
-    Abc_Obj_t * pNode, * pDriver, * pDriverNew, * pFanin;
-    int i, k, nDupGates = 0;
+    Abc_Obj_t * pNode, * pDriver;
+    int i, nDupGates = 0;
     assert( Abc_NtkIsLogic(pNtk) );
-    // process the COs by adding inverters and buffers when necessary
+    Abc_NtkIncrementTravId( pNtk );
     Abc_NtkForEachCo( pNtk, pNode, i ) 
     {
+        // if the driver is complemented, this is an error
         pDriver = Abc_ObjFanin0(pNode);
-        if ( Abc_ObjIsCi(pDriver) )
+        if ( Abc_ObjFaninC0(pNode) )
         {
-            // skip the case when the driver is a different node with the same name
-            if ( pDriver != pNode && strcmp(Abc_ObjName(pDriver), Abc_ObjName(pNode)) == 0 )
-            {
-                assert( !Abc_ObjFaninC0(pNode) );
-                continue;
-            }
+            Abc_NtkFixCoDriverProblem( pDriver, pNode, fDuplicate );
+            nDupGates++;
+            continue;
         }
-        else if ( !Abc_ObjFaninC0(pNode) )
+        // if the driver is a CI and has different name, this is an error
+        if ( Abc_ObjIsCi(pDriver) && strcmp(Abc_ObjName(pDriver), Abc_ObjName(pNode)) )
         {
-            // skip the case when all CO fanouts of the driver have the same name
-            if ( Abc_NodeHasUniqueCoFanout(pDriver) )
-                continue;
+            Abc_NtkFixCoDriverProblem( pDriver, pNode, fDuplicate );
+            nDupGates++;
+            continue;
         }
-        if ( fDuplicate && !Abc_ObjIsCi(pDriver) )
+        // if the driver is visited for the first time, remember the CO name
+        if ( !Abc_NodeIsTravIdCurrent(pDriver) )
         {
-            pDriverNew = Abc_NtkDupObj( pNtk, pDriver, 0 ); 
-            Abc_ObjForEachFanin( pDriver, pFanin, k )
-                Abc_ObjAddFanin( pDriverNew, pFanin );
-            if ( Abc_ObjFaninC0(pNode) )
-            {
-                // change polarity of the duplicated driver
-                Abc_NodeComplement( pDriverNew );
-                Abc_ObjXorFaninC( pNode, 0 );
-            }
+            pDriver->pNext = (Abc_Obj_t *)Abc_ObjName(pNode);
+            Abc_NodeSetTravIdCurrent(pDriver);
+            continue;
         }
-        else
+        // the driver has second CO - if they have different name, this is an error
+        if ( strcmp((char *)pDriver->pNext, Abc_ObjName(pNode)) ) // diff names
         {
-            // add inverters and buffers when necessary
-            if ( Abc_ObjFaninC0(pNode) )
-            {
-                pDriverNew = Abc_NodeCreateInv( pNtk, pDriver );
-                Abc_ObjXorFaninC( pNode, 0 );
-            }
-            else
-                pDriverNew = Abc_NodeCreateBuf( pNtk, pDriver );        
+            Abc_NtkFixCoDriverProblem( pDriver, pNode, fDuplicate );
+            nDupGates++;
+            continue;
         }
-        // update the fanin of the PO node
-        Abc_ObjPatchFanin( pNode, pDriver, pDriverNew );
-        assert( Abc_ObjFanoutNum(pDriverNew) == 1 );
-        nDupGates++;
-        // remove the old driver if it dangles
-        if ( Abc_ObjFanoutNum(pDriver) == 0 )
-            Abc_NtkDeleteObj( pDriver );
     }
     assert( Abc_NtkLogicHasSimpleCos(pNtk) );
     return nDupGates;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index bbc9a226..0f20e4d8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2175,9 +2175,9 @@ int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsSopLogic(pNtk) && !Abc_NtkIsBddLogic(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) )
     {
-        fprintf( pErr, "Sweep cannot be performed on an AIG or a mapped network (run \"unmap\").\n" );
+        fprintf( pErr, "The classical (SIS-like) sweep can only be performed on a logic network.\n" );
         return 1;
     }
     // modify the current network
@@ -3401,7 +3401,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkLogicToSop(pNtk, fDirect) )
     {
-        fprintf( pErr, "Converting to BDD has failed.\n" );
+        fprintf( pErr, "Converting to SOP has failed.\n" );
         return 1;
     }
     return 0;
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index ab61dd45..64f414aa 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -593,7 +593,7 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter )
     Abc_NtkForEachPo( pMiter, pNodePo, i )
     {
         pChild = Abc_ObjChild0( pNodePo );
-        if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_AigNodeIsConst(pChild) )
+        if ( Abc_AigNodeIsConst(pChild) )
         {
             assert( Abc_ObjRegular(pChild) == Abc_AigConst1(pMiter) );
             if ( !Abc_ObjIsComplement(pChild) )
@@ -629,7 +629,7 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
     if ( Abc_NtkPoNum(pMiter) == 1 )
     {
         pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,0) );
-        if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_AigNodeIsConst(pChild) )
+        if ( Abc_AigNodeIsConst(pChild) )
         {
             if ( Abc_ObjIsComplement(pChild) )
                 printf( "Unsatisfiable.\n" );
@@ -645,7 +645,7 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
         {
             pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,i) );
             printf( "Output #%2d : ", i );
-            if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_AigNodeIsConst(pChild) )
+            if ( Abc_AigNodeIsConst(pChild) )
             {
                 if ( Abc_ObjIsComplement(pChild) )
                     printf( "Unsatisfiable.\n" );
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 7c6df88a..cac634da 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -197,7 +197,7 @@ stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose )
         if ( pNodeAig == NULL )
             continue;
         // skip the nodes that fanout into COs
-        if ( Abc_NodeHasCoFanout(pNode) )
+        if ( Abc_NodeFindCoFanout(pNode) )
             continue;
         // get the FRAIG node
         gNode = Fraig_NotCond( Abc_ObjRegular(pNodeAig)->pCopy, Abc_ObjIsComplement(pNodeAig) );
@@ -495,12 +495,8 @@ int Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes )
     int i, Counter;
     assert( Abc_NtkIsLogic(pNtk) );
     // mark the nodes reachable from the POs
-    for ( i = 0; i < vNodes->nSize; i++ )
-    {
-        pNode = vNodes->pArray[i];
-        assert( Abc_ObjIsNode(pNode) );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
         pNode->fMarkA = 1;
-    }
     // remove the non-marked nodes
     Counter = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
@@ -510,7 +506,7 @@ int Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes )
             Counter++;
         }
     // unmark the remaining nodes
-    Abc_NtkForEachNode( pNtk, pNode, i )
+    Vec_PtrForEachEntry( vNodes, pNode, i )
         pNode->fMarkA = 0;
     // check
     if ( !Abc_NtkCheck( pNtk ) )
@@ -534,86 +530,40 @@ int Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes )
 ***********************************************************************/
 int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
 {
-    Abc_Obj_t * pNode;
-    int i, fConvert, nSwept, nSweptNew;
-    assert( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsBddLogic(pNtk) ); 
-    // convert to the BDD representation
-    fConvert = 0;
-    if ( Abc_NtkIsSopLogic(pNtk) )
-        Abc_NtkSopToBdd(pNtk), fConvert = 1;
-    // perform cleanup to get rid of dangling nodes
-    nSwept = Abc_NtkCleanup( pNtk, 0 );
-    // make the network minimum base
-    Abc_NtkRemoveDupFanins(pNtk);
-    Abc_NtkMinimumBase(pNtk);
-    do
-    {
-        // sweep constants and single-input nodes
-        Abc_NtkForEachNode( pNtk, pNode, i )
-            if ( i && Abc_ObjFaninNum(pNode) < 2 )
-                Abc_NodeSweep( pNode, fVerbose );
-        // make the network minimum base
-        Abc_NtkRemoveDupFanins(pNtk);
-        Abc_NtkMinimumBase(pNtk);
-        // perform final clean up (in case new danglies are created)
-        nSweptNew = Abc_NtkCleanup( pNtk, 0 );
-        nSwept += nSweptNew;
-    }
-    while ( nSweptNew );
-    // conver back to BDD
-    if ( fConvert )
-        Abc_NtkBddToSop(pNtk, 0);
-    // report
-    if ( fVerbose )
-        printf( "Sweep removed %d nodes.\n", nSwept );
-    // check
-    if ( !Abc_NtkCheck( pNtk ) )
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode, * pFanout, * pDriver;
+    int i, nNodesOld;
+    assert( Abc_NtkIsLogic(pNtk) ); 
+    // convert network to BDD representation
+    if ( !Abc_NtkLogicToBdd(pNtk) )
     {
-        printf( "Abc_NtkSweep: The network check has failed.\n" );
-        return -1;
+        fprintf( stdout, "Converting to BDD has failed.\n" );
+        return 1;
     }
-    return nSwept;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Tranditional sweep of the network.]
-
-  Description [Propagates constant and single-input node, removes dangling nodes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose )
-{
-    Abc_Obj_t * pFanout, * pDriver;
-    Vec_Ptr_t * vFanout;
-    int i;
-    assert( Abc_ObjFaninNum(pNode) < 2 );
-    assert( Abc_ObjFanoutNum(pNode) > 0 );
-    // iterate through the fanouts
-    vFanout = Vec_PtrAlloc( Abc_ObjFanoutNum(pNode) );
-    Abc_NodeCollectFanouts( pNode, vFanout );
-    Vec_PtrForEachEntry( vFanout, pFanout, i )
+    // perform cleanup
+    nNodesOld = Abc_NtkNodeNum(pNtk);
+    Abc_NtkCleanup( pNtk, 0 );
+    // prepare nodes for sweeping
+    Abc_NtkRemoveDupFanins(pNtk);
+    Abc_NtkMinimumBase(pNtk);
+    // collect sweepable nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( Abc_ObjFaninNum(pNode) < 2 )
+            Vec_PtrPush( vNodes, pNode );
+    // sweep the nodes
+    while ( Vec_PtrSize(vNodes) > 0 )
     {
-        if ( Abc_ObjIsCo(pFanout) )
-        {
-            if ( Abc_ObjFaninNum(pNode) == 1 )
-            {
-                pDriver = Abc_ObjFanin0(pNode);
-                if ( Abc_ObjIsCi(pDriver) || Abc_ObjFanoutNum(pDriver) > 1 || Abc_ObjFanoutNum(pNode) > 1 )
-                    continue;
-                // the driver is a node and its only fanout is this node
-                if ( Abc_NodeIsInv(pNode) )
-                    pDriver->pData = Cudd_Not(pDriver->pData);
-                // replace the fanin of the fanout
-                Abc_ObjPatchFanin( pFanout, pNode, pDriver );
-            }
+        // get any sweepable node
+        pNode = Vec_PtrPop(vNodes);
+        if ( !Abc_ObjIsNode(pNode) )
             continue;
-        }
-        // the fanout is a regular node
+        // get any non-CO fanout of this node
+        pFanout = Abc_NodeFindNonCoFanout(pNode);
+        if ( pFanout == NULL )
+            continue;
+        assert( Abc_ObjIsNode(pFanout) );
+        // transform the function of the fanout
         if ( Abc_ObjFaninNum(pNode) == 0 )
             Abc_NodeConstantInput( pFanout, pNode, Abc_NodeIsConst0(pNode) );
         else 
@@ -624,10 +574,44 @@ void Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose )
                 Abc_NodeComplementInput( pFanout, pNode );
             Abc_ObjPatchFanin( pFanout, pNode, pDriver );
         }
+        Abc_NodeRemoveDupFanins( pFanout );
+        Abc_NodeMinimumBase( pFanout );
+        // check if the fanout should be added
+        if ( Abc_ObjFaninNum(pFanout) < 2 )
+            Vec_PtrPush( vNodes, pFanout );
+        // check if the node has other fanouts
+        if ( Abc_ObjFanoutNum(pNode) > 0 )
+            Vec_PtrPush( vNodes, pNode );
+        else
+            Abc_NtkDeleteObj_rec( pNode );
     }
-    Vec_PtrFree( vFanout );
+    Vec_PtrFree( vNodes );
+    // sweep a node into its CO fanout if all of this is true:
+    // (a) this node is a single-input node
+    // (b) the driver of the node has only one fanout (this node)
+    // (c) the driver is a node
+    Abc_NtkForEachCo( pNtk, pFanout, i )
+    {
+        pNode = Abc_ObjFanin0(pFanout);
+        if ( Abc_ObjFaninNum(pNode) != 1 )
+            continue;
+        pDriver = Abc_ObjFanin0(pNode);
+        if ( !(Abc_ObjFanoutNum(pDriver) == 1 && Abc_ObjIsNode(pDriver)) )
+            continue;
+        // trasform this CO
+        if ( Abc_NodeIsInv(pNode) )
+            pDriver->pData = Cudd_Not(pDriver->pData);
+        Abc_ObjPatchFanin( pFanout, pNode, pDriver );
+    }
+    // perform cleanup
+    Abc_NtkCleanup( pNtk, 0 );
+    // report
+    if ( fVerbose )
+        printf( "Sweep removed %d nodes.\n", nNodesOld - Abc_NtkNodeNum(pNtk) );
+    return nNodesOld - Abc_NtkNodeNum(pNtk);
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Replaces the local function by its cofactor.]
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 535789d2..8b7e015b 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -1057,7 +1057,7 @@ int Io_ReadBlifNetworkConnectBoxesOne( Io_ReadBlif_t * p, Abc_Ntk_t * pNtk, stmm
     Abc_Obj_t * pBox;
     int i;
     // go through the boxes
-    Abc_NtkForEachBox( pNtk, pBox, i )
+    Abc_NtkForEachBlackbox( pNtk, pBox, i )
         if ( Io_ReadBlifNetworkConnectBoxesOneBox( p, pBox, tName2Model ) )
             return 1;
     Abc_NtkFinalizeRead( pNtk );
diff --git a/src/temp/aig/aig.h b/src/temp/aig/aig.h
index e489d978..5166d0c3 100644
--- a/src/temp/aig/aig.h
+++ b/src/temp/aig/aig.h
@@ -137,7 +137,7 @@ static inline int          Aig_ManObjNum( Aig_Man_t * p )         { return p->nC
 
 static inline Aig_Type_t   Aig_ObjType( Aig_Obj_t * pObj )        { return pObj->Type;               }
 static inline int          Aig_ObjIsNone( Aig_Obj_t * pObj )      { return pObj->Type == AIG_NONE;   }
-static inline int          Aig_ObjIsConst1( Aig_Obj_t * pObj )    { return pObj->Type == AIG_CONST1; }
+static inline int          Aig_ObjIsConst1( Aig_Obj_t * pObj )    { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_CONST1; }
 static inline int          Aig_ObjIsPi( Aig_Obj_t * pObj )        { return pObj->Type == AIG_PI;     }
 static inline int          Aig_ObjIsPo( Aig_Obj_t * pObj )        { return pObj->Type == AIG_PO;     }
 static inline int          Aig_ObjIsAnd( Aig_Obj_t * pObj )       { return pObj->Type == AIG_AND;    }
diff --git a/src/temp/aig/aigDfs.c b/src/temp/aig/aigDfs.c
index e289f6ec..2fe8b2ef 100644
--- a/src/temp/aig/aigDfs.c
+++ b/src/temp/aig/aigDfs.c
@@ -325,9 +325,12 @@ Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pRoo
     if ( Aig_ObjIsConst1( Aig_Regular(pRoot) ) )
         return Aig_NotCond( Aig_ManConst1(pDest), Aig_IsComplement(pRoot) );
     // set the PI mapping
-    Aig_ManForEachPi( pDest, pObj, i )
-        if ( i < nVars )
-            Aig_IthVar(pSour, i)->pData = Aig_IthVar(pDest, i);
+    Aig_ManForEachPi( pSour, pObj, i )
+    {
+        if ( i == nVars )
+           break;
+        pObj->pData = Aig_IthVar(pDest, i);
+    }
     // transfer and set markings
     Aig_Transfer_rec( pDest, Aig_Regular(pRoot) );
     // clear the markings
diff --git a/src/temp/aig/aigMan.c b/src/temp/aig/aigMan.c
index af6df62d..bb39712f 100644
--- a/src/temp/aig/aigMan.c
+++ b/src/temp/aig/aigMan.c
@@ -56,6 +56,7 @@ Aig_Man_t * Aig_ManStart()
     Aig_ManStartMemory( p );
     // create the constant node
     p->pConst1 = Aig_ManFetchMemory( p );
+    p->pConst1->Type = AIG_CONST1;
     p->pConst1->fPhase = 1;
     p->nCreated = 1;
     // start the table
diff --git a/src/temp/aig/aigOper.c b/src/temp/aig/aigOper.c
index cad240ae..9985093e 100644
--- a/src/temp/aig/aigOper.c
+++ b/src/temp/aig/aigOper.c
@@ -183,6 +183,7 @@ Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
 ***********************************************************************/
 Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 )
 {
+/*    
     Aig_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
     int Count0, Count1;
     // consider trivial cases
@@ -190,6 +191,9 @@ Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t *
         return Aig_Exor( p, pC, p0 );
     // other cases can be added
     // implement the first MUX (F = C * x1 + C' * x0)
+
+    // check for constants here!!!
+
     pTempA1 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, pC,          p1, AIG_AND) );
     pTempA2 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pC), p0, AIG_AND) );
     if ( pTempA1 && pTempA2 )
@@ -217,8 +221,8 @@ Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t *
     pTempB1 = pTempB1? pTempB1 : Aig_And(p, pC,          Aig_Not(p1));
     pTempB2 = pTempB2? pTempB2 : Aig_And(p, Aig_Not(pC), Aig_Not(p0));
     return Aig_Not( Aig_Or( p, pTempB1, pTempB2 ) );
-
-//    return Aig_Or( Aig_And(pC, p1), Aig_And(Aig_Not(pC), p0) );
+*/
+    return Aig_Or( p, Aig_And(p, pC, p1), Aig_And(p, Aig_Not(pC), p0) );
 }
 
 /**Function*************************************************************
diff --git a/src/temp/ver/verCore.c b/src/temp/ver/verCore.c
index 303fe7d1..6c8192f5 100644
--- a/src/temp/ver/verCore.c
+++ b/src/temp/ver/verCore.c
@@ -34,6 +34,18 @@ typedef enum {
     VER_SIG_WIRE
 } Ver_SignalType_t;
 
+// types of verilog gates
+typedef enum { 
+    VER_GATE_AND = 0,
+    VER_GATE_OR,
+    VER_GATE_XOR,
+    VER_GATE_BUF,
+    VER_GATE_NAND,
+    VER_GATE_NOR,
+    VER_GATE_XNOR,
+    VER_GATE_NOT
+} Ver_GateType_t;
+
 static Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib );
 static void Ver_ParseStop( Ver_Man_t * p );
 static void Ver_ParseFreeData( Ver_Man_t * p );
@@ -44,6 +56,7 @@ static int  Ver_ParseAssign( Ver_Man_t * p );
 static int  Ver_ParseAlways( Ver_Man_t * p );
 static int  Ver_ParseInitial( Ver_Man_t * p );
 static int  Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtkGate );
+static int  Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType );
 
 static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName );
 static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName );
@@ -201,6 +214,7 @@ void Ver_ParseFreeData( Ver_Man_t * p )
 {
     if ( p->pNtkCur )
     {
+        p->pNtkCur->pManFunc = NULL;
         Abc_NtkDelete( p->pNtkCur );
         p->pNtkCur = NULL;
     }
@@ -324,7 +338,25 @@ int Ver_ParseModule( Ver_Man_t * pMan )
     while ( 1 )
     {
         Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
-        if ( !strcmp( pWord, "assign" ) )
+
+        if ( !strcmp( pWord, "and" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_AND );
+        else if ( !strcmp( pWord, "or" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_OR );
+        else if ( !strcmp( pWord, "xor" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_XOR );
+        else if ( !strcmp( pWord, "buf" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_BUF );
+        else if ( !strcmp( pWord, "nand" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NAND );
+        else if ( !strcmp( pWord, "nor" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NOR );
+        else if ( !strcmp( pWord, "xnor" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_XNOR );
+        else if ( !strcmp( pWord, "not" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NOT );
+
+        else if ( !strcmp( pWord, "assign" ) )
             RetValue = Ver_ParseAssign( pMan );
         else if ( !strcmp( pWord, "always" ) )
             RetValue = Ver_ParseAlways( pMan );
@@ -348,6 +380,9 @@ int Ver_ParseModule( Ver_Man_t * pMan )
         }
         if ( RetValue == 0 )
             return 0;
+        // skip the comments
+        if ( !Ver_ParseSkipComments( pMan ) )
+            return 0;
         // get new word
         pWord = Ver_ParseGetName( pMan );
         if ( pWord == NULL )
@@ -469,14 +504,6 @@ int Ver_ParseAssign( Ver_Man_t * pMan )
             Ver_ParsePrintErrorMessage( pMan );
             return 0;
         }
-        // get the fanout net
-        pNet = Abc_NtkFindNet( pNtk, pWord );
-        if ( pNet == NULL )
-        {
-            sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
         // get the equal sign
         if ( Ver_StreamPopChar(p) != '=' )
         {
@@ -893,6 +920,97 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
 
 /**Function*************************************************************
 
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Aig_Man_t * pAig = pMan->pNtkCur->pManFunc;
+    Abc_Obj_t * pNet, * pNode;
+    char * pWord, Symbol;
+    // this is gate name - throw it away
+    if ( Ver_StreamPopChar(p) != '(' )
+    {
+        sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    Ver_ParseSkipComments( pMan );
+    // create the node
+    pNode = Abc_NtkCreateNode( pMan->pNtkCur );
+    // parse pairs of formal/actural inputs
+    while ( 1 )
+    {
+        // parse the output name
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // get the net corresponding to this output
+        pNet = Abc_NtkFindNet( pMan->pNtkCur, pWord );
+        if ( pNet == NULL )
+        {
+            sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // if this is the first net, add it as an output
+        if ( Abc_ObjFanoutNum(pNode) == 0 )
+            Abc_ObjAddFanin( pNet, pNode );
+        else
+            Abc_ObjAddFanin( pNode, pNet );
+        // check if it is the end of gate
+        Ver_ParseSkipComments( pMan );
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol == ')' )
+            break;
+        // skip comma
+        if ( Symbol != ',' )
+        {
+            sprintf( pMan->sError, "Cannot parse a standard gate %s (expected closing paranthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        Ver_ParseSkipComments( pMan );
+    }
+    if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 )
+    {
+        sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    if ( Ver_StreamPopChar(p) != ';' )
+    {
+        sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    // add logic function
+    if ( GateType == VER_GATE_AND || GateType == VER_GATE_NAND )
+        pNode->pData = Aig_CreateAnd( pAig, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR )
+        pNode->pData = Aig_CreateOr( pAig, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR )
+        pNode->pData = Aig_CreateExor( pAig, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT )
+        pNode->pData = Aig_CreateAnd( pAig, Abc_ObjFaninNum(pNode) );
+    if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT )
+        pNode->pData = Aig_Not( pNode->pData );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Creates PI terminal and net.]
 
   Description []
diff --git a/src/temp/ver/verFormula.c b/src/temp/ver/verFormula.c
index 2c2881c0..8bb21547 100644
--- a/src/temp/ver/verFormula.c
+++ b/src/temp/ver/verFormula.c
@@ -392,7 +392,7 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
         if ( nLength2 != nLength )
             continue;
         pTemp2   = Vec_PtrEntry( vNames, 2*i + 1 );
-        if ( strncmp( pTemp, pTemp2, nLength ) )
+        if ( strncmp( pString, pTemp2, nLength ) )
             continue;
         return i;
     }