Version abc60823

abc.rc

@@ -98,4 +98,7 @@ alias src_rs      "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l"
 alias src_rws     "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" 
 alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
 
+# temporaries
+alias test        "rvl th/lib.v; rvv th/t1.v"
+
 

src/base/abc/abcAig.c

@@ -136,12 +136,10 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
     pMan->vStackReplaceOld = Vec_PtrAlloc( 100 );
     pMan->vStackReplaceNew = Vec_PtrAlloc( 100 );
     // create the constant node
-    pMan->pConst1  = Abc_ObjAlloc( pNtkAig, ABC_OBJ_CONST1 );
-    // add to the array of objects, count it as object but not as node
     assert( pNtkAig->vObjs->nSize == 0 );
-    pMan->pConst1->Id = pNtkAig->vObjs->nSize;
-    Vec_PtrPush( pNtkAig->vObjs, pMan->pConst1 );
-    pNtkAig->nObjs++;
+    pMan->pConst1 = Abc_NtkObjAdd( pNtkAig, ABC_OBJ_NODE );
+    pMan->pConst1->Type = ABC_OBJ_CONST1;
+    pNtkAig->nObjCounts[ABC_OBJ_NODE]--;
     // save the current network
     pMan->pNtkAig = pNtkAig;
     return pMan;

src/base/abc/abcCheck.c

@@ -117,14 +117,14 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
     {
         fprintf( stdout, "NetworkCheck: Number of CIs does not match number of PIs and latches.\n" );
         fprintf( stdout, "One possible reason is that latches are added twice:\n" );
-        fprintf( stdout, "in procedure Abc_ObjAdd() and in the user's code.\n" );
+        fprintf( stdout, "in procedure Abc_NtkObjAdd() and in the user's code.\n" );
         return 0;
     }
     if ( Abc_NtkPoNum(pNtk) + Abc_NtkAssertNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCoNum(pNtk) )
     {
         fprintf( stdout, "NetworkCheck: Number of COs does not match number of POs, asserts, and latches.\n" );
         fprintf( stdout, "One possible reason is that latches are added twice:\n" );
-        fprintf( stdout, "in procedure Abc_ObjAdd() and in the user's code.\n" );
+        fprintf( stdout, "in procedure Abc_NtkObjAdd() and in the user's code.\n" );
         return 0;
     }
 

src/base/abc/abcFanio.c

@@ -167,6 +167,47 @@ void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFa
 
 /**Function*************************************************************
 
+  Synopsis    [Inserts one-input node of the type specified between the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_ObjInsertBetween( Abc_Obj_t * pNodeIn, Abc_Obj_t * pNodeOut, Abc_ObjType_t Type )
+{
+    Abc_Obj_t * pNodeNew;
+    int iFanoutIndex, iFaninIndex;
+    // find pNodeOut among the fanouts of pNodeIn
+    if ( (iFanoutIndex = Vec_IntFind( &pNodeIn->vFanouts, pNodeOut->Id )) == -1 )
+    {
+        printf( "Node %s is not among", Abc_ObjName(pNodeOut) );
+        printf( " the fanouts of node %s...\n", Abc_ObjName(pNodeIn) );
+        return NULL;
+    }
+    // find pNodeIn among the fanins of pNodeOut
+    if ( (iFaninIndex = Vec_IntFind( &pNodeOut->vFanins, pNodeIn->Id )) == -1 )
+    {
+        printf( "Node %s is not among", Abc_ObjName(pNodeIn) );
+        printf( " the fanins of node %s...\n", Abc_ObjName(pNodeOut) );
+        return NULL;
+    }
+    // create the new node
+    pNodeNew = Abc_NtkCreateObj( pNodeIn->pNtk, Type );
+    // add pNodeIn as fanin and pNodeOut as fanout
+    Vec_IntPushMem( pNodeNew->pNtk->pMmStep, &pNodeNew->vFanins,  pNodeIn->Id  );
+    Vec_IntPushMem( pNodeNew->pNtk->pMmStep, &pNodeNew->vFanouts, pNodeOut->Id );
+    // update the fanout of pNodeIn
+    Vec_IntWriteEntry( &pNodeIn->vFanouts, iFanoutIndex, pNodeNew->Id );
+    // update the fanin of pNodeOut
+    Vec_IntWriteEntry( &pNodeOut->vFanins, iFaninIndex, pNodeNew->Id );
+    return pNodeNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transfers fanout from the old node to the new node.]
 
   Description []

src/base/abc/abcLib.c

@@ -46,7 +46,9 @@ Abc_Lib_t * Abc_LibCreate( char * pName )
     memset( p, 0, sizeof(Abc_Lib_t) );
     p->pName    = Extra_UtilStrsav( pName );
     p->tModules = st_init_table( strcmp, st_strhash );
+    p->vModules = Vec_PtrAlloc( 100 );
     p->pManFunc = Aig_ManStart();
+    p->pLibrary = NULL;
     return p;
 }
 
@@ -63,18 +65,22 @@ Abc_Lib_t * Abc_LibCreate( char * pName )
 ***********************************************************************/
 void Abc_LibFree( Abc_Lib_t * pLib )
 {
-    st_generator * gen;
     Abc_Ntk_t * pNtk;
-    char * pName;
+    int i;
     if ( pLib->pName )
         free( pLib->pName );
     if ( pLib->pManFunc )
         Aig_ManStop( pLib->pManFunc );
     if ( pLib->tModules )
+        st_free_table( pLib->tModules );
+    if ( pLib->vModules )
+    {
+        Vec_PtrForEachEntry( pLib->vModules, pNtk, i )
         {
-        st_foreach_item( pLib->tModules, gen, (char**)&pName, (char**)&pNtk )
+            pNtk->pManFunc = NULL;
             Abc_NtkDelete( pNtk );
-        st_free_table( pLib->tModules );
+        }
+        Vec_PtrFree( pLib->vModules );
     }
     free( pLib );
 }
@@ -92,21 +98,198 @@ void Abc_LibFree( Abc_Lib_t * pLib )
 ***********************************************************************/
 Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib )
 {
-    st_generator * gen;
     Abc_Ntk_t * pNtk;
-    char * pName;
-    if ( st_count(pLib->tModules) > 1 )
+    if ( Vec_PtrSize(pLib->vModules) > 1 )
     {
         printf( "The design includes more than one module and is currently not used.\n" );
         return NULL;
     }
-    // find the network
-    st_foreach_item( pLib->tModules, gen, (char**)&pName, (char**)&pNtk )
+    pNtk = Vec_PtrEntry( pLib->vModules, 0 );  Vec_PtrClear( pLib->vModules );
+    pNtk->pManFunc = pLib->pManFunc;           pLib->pManFunc = NULL;
+    return pNtk;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Surround boxes without content (black boxes) with BIs/BOs.]
+
+  Description [Returns the number of black boxes converted.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_LibDeriveBlackBoxes( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib )
+{
+    Abc_Obj_t * pObj, * pFanin, * pFanout;
+    int i, k;
+    assert( Abc_NtkIsNetlist(pNtk) );
+    // collect blackbox nodes
+    assert( Vec_PtrSize(pNtk->vBoxes) == 0 );
+    Vec_PtrClear( pNtk->vBoxes );
+    Abc_NtkForEachBox( pNtk, pObj, i )
+        if ( Abc_NtkNodeNum(pObj->pData) == 0 )
+            Vec_PtrPush( pNtk->vBoxes, pObj );
+    // return if there is no black boxes without content
+    if ( Vec_PtrSize(pNtk->vBoxes) == 0 )
+        return 0;
+    // print the boxes
+    printf( "Black boxes are: " );
+    Abc_NtkForEachBox( pNtk, pObj, i )
+        printf( " %s", ((Abc_Ntk_t *)pObj->pData)->pName );
+    printf( "\n" );
+    // iterate through the boxes and add BIs/BOs
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        // go through the fanin nets
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Abc_ObjInsertBetween( pFanin, pObj, ABC_OBJ_BO );
+        // go through the fanout nets
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+        {
+            Abc_ObjInsertBetween( pObj, pFanout, ABC_OBJ_BI );
+            // if the name is not given assign name
+            if ( pFanout->pData == NULL )
             {
-        st_free_gen(gen);
-        break;
+                pFanout->pData = Abc_ObjName( pFanout );
+                Nm_ManStoreIdName( pNtk->pManName, pFanout->Id, pFanout->pData, NULL );
             }
-    return pNtk;
+        }
+    }
+    return Vec_PtrSize(pNtk->vBoxes);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive the AIG of the logic in the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeStrashUsingNetwork_rec( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    assert( !Abc_ObjIsNet(pObj) );
+    if ( pObj->pCopy )
+        return;
+    // call for the fanins
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Abc_NodeStrashUsingNetwork_rec( pNtkAig, Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)) );
+    // compute for the node
+    pObj->pCopy = Abc_NodeStrash( pNtkAig, pObj );
+    // set for the fanout net
+    Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive the AIG of the logic in the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeStrashUsingNetwork( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pBox )
+{
+    Abc_Ntk_t * pNtkGate;
+    Abc_Obj_t * pObj;
+    unsigned * pPolarity;
+    int i, fCompl;
+    assert( Abc_ObjIsBox(pBox) );
+    pNtkGate = pBox->pData;
+    pPolarity = (unsigned *)pBox->pNext;
+    assert( Abc_NtkIsNetlist(pNtkGate) );
+    assert( Abc_NtkLatchNum(pNtkGate) == 0 );
+    Abc_NtkCleanCopy( pNtkGate );
+    // set the PI values
+    Abc_NtkForEachPi( pNtkGate, pObj, i )
+    {
+        fCompl = (pPolarity && Abc_InfoHasBit(pPolarity, i));
+        pObj->pCopy = Abc_ObjNotCond( Abc_ObjFanin(pBox,i)->pCopy, fCompl );
+        Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
+    }
+    // build recursively and set the PO values
+    Abc_NtkForEachPo( pNtkGate, pObj, i )
+    {
+        Abc_NodeStrashUsingNetwork_rec( pNtkAig, Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)) );
+        Abc_ObjFanout(pBox,i)->pCopy = Abc_ObjFanin0(pObj)->pCopy;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive the AIG of the logic in the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib )
+{
+    ProgressBar * pProgress;
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkAig;
+    Abc_Obj_t * pObj;
+    int i, nBoxes;
+    // explicitly derive black boxes
+    assert( Abc_NtkIsNetlist(pNtk) );
+    nBoxes = Abc_LibDeriveBlackBoxes( pNtk, pLib );
+    if ( nBoxes )
+        printf( "Detected and transformed %d black boxes.\n", nBoxes );
+    // create the new network with black boxes in place
+    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // transer to the nets
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
+    // build the AIG for the remaining logic in the netlist
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodes) );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( Abc_ObjIsNode(pObj) )
+        {
+            pObj->pCopy = Abc_NodeStrash( pNtkAig, pObj );
+            Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
+            continue;
+        }
+        Abc_NodeStrashUsingNetwork( pNtkAig, pObj );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodes );
+    // deallocate memory manager, which remembers the phase
+    if ( pNtk->pData )
+    {
+        Extra_MmFlexStop( pNtk->pData, 0 );
+        pNtk->pData = NULL;
+    }
+    // set the COs
+//    Abc_NtkFinalize( pNtk, pNtkAig );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
+    Abc_AigCleanup( pNtkAig->pManFunc );
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_LibDeriveAig: The network check has failed.\n" );
+        return 0;
+    }
+    return pNtkAig;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/base/abc/abcNames.c

@@ -166,8 +166,8 @@ char * Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pObjNew, char * pNameOld, char * p
 ***********************************************************************/
 void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 {
-    Abc_Obj_t * pObj;
-    int i;
+    Abc_Obj_t * pObj, * pTerm;
+    int i, k;
     assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) );
     assert( Abc_NtkPoNum(pNtk) == Abc_NtkPoNum(pNtkNew) );
     assert( Abc_NtkAssertNum(pNtk) == Abc_NtkAssertNum(pNtkNew) );
@@ -181,6 +181,13 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
         Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i),      Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
     Abc_NtkForEachAssert( pNtk, pObj, i ) 
         Abc_NtkLogicStoreName( Abc_NtkAssert(pNtkNew,i),  Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+            Abc_NtkLogicStoreName( pTerm->pCopy,          Abc_ObjName(Abc_ObjFanin0Ntk(pTerm)) );
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+            Abc_NtkLogicStoreName( pTerm->pCopy,          Abc_ObjName(Abc_ObjFanout0Ntk(pTerm)) );
+    }
     if ( !Abc_NtkIsSeq(pNtk) )
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i),   Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) );

src/base/abc/abcNetlist.c

@@ -95,11 +95,11 @@ Abc_Ntk_t * Abc_NtkNetlistToLogicHie( Abc_Ntk_t * pNtk )
     int i, Counter = 0;
     assert( Abc_NtkIsNetlist(pNtk) );
     // start the network
-//    pNtkNew = Abc_NtkAlloc( Type, Func );
+//    pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
     if ( !Abc_NtkHasMapping(pNtk) )
-        pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+        pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
     else
-        pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_MAP );
+        pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_MAP, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);

src/base/abc/abcNtk.c

@@ -43,7 +43,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
+Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan )
 {
     Abc_Ntk_t * pNtk;
     pNtk = ALLOC( Abc_Ntk_t, 1 );
@@ -63,8 +63,8 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
     pNtk->vBoxes      = Vec_PtrAlloc( 100 );
     pNtk->vSkews      = Vec_FltAlloc( 100 );
     // start the memory managers
-    pNtk->pMmObj      = Extra_MmFixedStart( sizeof(Abc_Obj_t) );
-    pNtk->pMmStep     = Extra_MmStepStart( ABC_NUM_STEPS );
+    pNtk->pMmObj      = fUseMemMan? Extra_MmFixedStart( sizeof(Abc_Obj_t) ) : NULL;
+    pNtk->pMmStep     = fUseMemMan? Extra_MmStepStart( ABC_NUM_STEPS ) : NULL;
     // get ready to assign the first Obj ID
     pNtk->nTravIds    = 1;
     // start the functionality manager
@@ -101,12 +101,12 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj;
-    int i;
+    Abc_Obj_t * pObj, * pTerm;
+    int i, k;
     if ( pNtk == NULL )
         return NULL;
     // start the network
-    pNtkNew = Abc_NtkAlloc( Type, Func );
+    pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -125,6 +125,16 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
         Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        Abc_NtkDupObj(pNtkNew, pObj);
+        if ( Abc_NtkIsNetlist(pNtk) )
+            continue;
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+            Abc_NtkDupObj(pNtkNew, pTerm);
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+            Abc_NtkDupObj(pNtkNew, pTerm);
+    }
     // transfer the names
     if ( Type != ABC_NTK_NETLIST )
         Abc_NtkDupCioNamesTable( pNtk, pNtkNew );
@@ -155,7 +165,7 @@ Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc
     if ( pNtk == NULL )
         return NULL;
     // start the network
-    pNtkNew = Abc_NtkAlloc( Type, Func );
+    pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -172,6 +182,8 @@ Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc
         Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachAssert( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachBox( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
     // transfer the names
     if ( Type != ABC_NTK_NETLIST )
         Abc_NtkDupCioNamesTableNoLatches( pNtk, pNtkNew );
@@ -201,7 +213,7 @@ Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkF
     if ( pNtk == NULL )
         return NULL;
     // start the network
-    pNtkNew = Abc_NtkAlloc( Type, Func );
+    pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = NULL;
@@ -228,6 +240,8 @@ Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkF
         Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachBox( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
     // transfer the names
     Abc_NtkDupCioNamesTableDual( pNtk, pNtkNew );
     // check that the CI/CO/latches are copied correctly
@@ -276,7 +290,7 @@ Abc_Ntk_t * Abc_NtkStartRead( char * pName )
 {
     Abc_Ntk_t * pNtkNew; 
     // allocate the empty network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
     // set the specs
     pNtkNew->pName = Extra_FileNameGeneric(pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pName);
@@ -426,7 +440,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
     assert( Abc_ObjIsNode(pNode) ); 
     
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     // set the name
     sprintf( Buffer, "%s_%s", pNtk->pName, pNodeName );
     pNtkNew->pName = Extra_UtilStrsav(Buffer);
@@ -496,7 +510,7 @@ Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
     assert( Abc_ObjIsNode(pNode) ); 
     
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     // set the name
     sprintf( Buffer, "%s_%s", pNtk->pName, pNodeName );
     pNtkNew->pName = Extra_UtilStrsav(Buffer);
@@ -571,7 +585,7 @@ Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t
     
     // start the network
     Abc_NtkCleanCopy( pNtk );
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
 
     // collect the nodes in the TFI of the output
@@ -626,7 +640,7 @@ Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
     Abc_Obj_t * pFanin, * pNodePo;
     int i;
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     pNtkNew->pName = Extra_UtilStrsav(Abc_ObjName(pNode));
     // add the PIs corresponding to the fanins of the node
     Abc_ObjForEachFanin( pNode, pFanin, i )
@@ -665,7 +679,7 @@ Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop )
     Vec_Ptr_t * vNames;
     int i, nVars;
     // start the network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
     pNtkNew->pName = Extra_UtilStrsav("ex");
     // create PIs
     Vec_PtrPush( pNtkNew->vObjs, NULL );
@@ -706,11 +720,20 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     int LargePiece = (4 << ABC_NUM_STEPS);
     if ( pNtk == NULL )
         return;
+    // free EXDC Ntk
+    if ( pNtk->pExdc )
+        Abc_NtkDelete( pNtk->pExdc );
+    // dereference the BDDs
+    if ( Abc_NtkHasBdd(pNtk) )
+    {
+        Abc_NtkForEachNode( pNtk, pObj, i )
+            Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
+    }
     // make sure all the marks are clean
     Abc_NtkForEachObj( pNtk, pObj, i )
     {
         // free large fanout arrays
-        if ( pObj->vFanouts.nCap * 4 > LargePiece )
+        if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece )
             FREE( pObj->vFanouts.pArray );
         // these flags should be always zero
         // if this is not true, something is wrong somewhere
@@ -718,17 +741,23 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
         assert( pObj->fMarkB == 0 );
         assert( pObj->fMarkC == 0 );
     }
-
-    // dereference the BDDs
-    if ( Abc_NtkHasBdd(pNtk) )
-        Abc_NtkForEachNode( pNtk, pObj, i )
-            Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
+    // free the nodes
+    if ( pNtk->pMmStep == NULL )
+    {
+        Abc_NtkForEachObj( pNtk, pObj, i )
+        {
+            FREE( pObj->vFanouts.pArray );
+            FREE( pObj->vFanins.pArray );
+        }
+    }
+    if ( pNtk->pMmObj == NULL )
+    {
+        Abc_NtkForEachObj( pNtk, pObj, i )
+            free( pObj );
+    }
         
     FREE( pNtk->pName );
     FREE( pNtk->pSpec );
-    // copy the EXDC Ntk
-    if ( pNtk->pExdc )
-        Abc_NtkDelete( pNtk->pExdc );
     // free the arrays
     Vec_PtrFree( pNtk->vPios );
     Vec_PtrFree( pNtk->vPis );
@@ -743,11 +772,13 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     Vec_FltFree( pNtk->vSkews );
     if ( pNtk->pModel ) free( pNtk->pModel );
     TotalMemory  = 0;
-    TotalMemory += Extra_MmFixedReadMemUsage(pNtk->pMmObj);
-    TotalMemory += Extra_MmStepReadMemUsage(pNtk->pMmStep);
+    TotalMemory += pNtk->pMmObj? Extra_MmFixedReadMemUsage(pNtk->pMmObj)  : 0;
+    TotalMemory += pNtk->pMmStep? Extra_MmStepReadMemUsage(pNtk->pMmStep) : 0;
 //    fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) );
     // free the storage 
+    if ( pNtk->pMmObj )
         Extra_MmFixedStop( pNtk->pMmObj,   0 );
+    if ( pNtk->pMmStep )
         Extra_MmStepStop ( pNtk->pMmStep,  0 );
     // name manager
     Nm_ManFree( pNtk->pManName );
@@ -764,7 +795,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     else if ( Abc_NtkHasBdd(pNtk) )
         Extra_StopManager( pNtk->pManFunc );
     else if ( Abc_NtkHasAig(pNtk) )
-        Aig_ManStop( pNtk->pManFunc );
+        { if ( pNtk->pManFunc ) Aig_ManStop( pNtk->pManFunc ); }
     else if ( Abc_NtkHasMapping(pNtk) )
         pNtk->pManFunc = NULL;
     else if ( !Abc_NtkHasBlackbox(pNtk) )

src/base/abci/abcMiter.c

@@ -87,7 +87,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
     assert( Abc_NtkIsStrash(pNtk2) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
 
@@ -304,7 +304,7 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
 
@@ -356,7 +356,7 @@ Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
     assert( 1 == Abc_NtkCoNum(pNtk) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     sprintf( Buffer, "%s_miter", pNtk->pName );
     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
 
@@ -423,7 +423,7 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In
     assert( In2 < Abc_NtkCiNum(pNtk) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     sprintf( Buffer, "%s_miter", Abc_ObjName(Abc_NtkCo(pNtk, Out)) );
     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
 
@@ -488,7 +488,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
     assert( In < Abc_NtkCiNum(pNtk) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkMiter->pName = Extra_UtilStrsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) );
 
     // get the root output
@@ -669,7 +669,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkIsDfsOrdered(pNtk) );
     // start the new network
-    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
     pNtkFrames->pName = Extra_UtilStrsav(Buffer);
     // create new latches (or their initial values) and remember them in the new latches
@@ -806,7 +806,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram
     assert( nFrames > 0 );
     assert( Abc_NtkIsStrash(pNtk) );   
     // start the new network
-    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
     pNtkFrames->pName = Extra_UtilStrsav(Buffer);
     // create new latches (or their initial values) and remember them in the new latches

src/base/abci/abcNtbdd.c

@@ -78,7 +78,7 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo
         return NULL;
 
     // start the network
-    pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
     pNtk->pName = Extra_UtilStrsav(pNamePo);
     // make sure the new manager has enough inputs
     Cudd_bddIthVar( pNtk->pManFunc, Vec_PtrSize(vNamesPi) );

src/base/abci/abcPrint.c

@@ -67,6 +67,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     {
         fprintf( pFile, "  net = %5d", Abc_NtkNetNum(pNtk) );
         fprintf( pFile, "  nd = %5d",  Abc_NtkNodeNum(pNtk) );
+        fprintf( pFile, "  box = %5d", Abc_NtkBoxNum(pNtk) );
     }
     else if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) )
     {        
@@ -83,7 +84,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     else 
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
 
-    if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) || Abc_NtkIsNetlist(pNtk) )
     {
     }
     else if ( Abc_NtkHasSop(pNtk) )   

src/base/abci/abcRr.c

@@ -676,7 +676,7 @@ Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vC
     int i;
     assert( Abc_NtkIsStrash(pNtk) );
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav( "temp" );
     // map the constant nodes

src/base/abci/abcSat.c

@@ -436,6 +436,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
     int clk1 = clock(), clk;
     int fOrderCiVarsFirst = 0;
     int nLevelsMax = Abc_AigGetLevelNum(pNtk);
+    int RetValue = 0;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
@@ -481,7 +482,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
         }
         // add the trivial clause
         if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) )
-            return 0;
+            goto Quits;
     }
 
     // add the clauses
@@ -515,7 +516,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
             }
             // add the clauses
             if ( !Abc_NtkClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) )
-                return 0;
+                goto Quits;
         }
         else
         {
@@ -537,12 +538,12 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
             {
                 if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) )
 //                if ( !Abc_NtkClauseTriv( pSat, pNode, vVars ) )
-                    return 0;
+                    goto Quits;
             }
             else
             {
                 if ( !Abc_NtkClauseAnd( pSat, pNode, vSuper, vVars ) )
-                    return 0;
+                    goto Quits;
             }
         }
         // add the variables to the J-frontier
@@ -597,11 +598,13 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
     Asat_SolverSetFactors( pSat, Vec_IntReleaseArray(vLevels) );
     Vec_IntFree( vLevels );
 */
+    RetValue = 1;
+Quits :
     // delete
     Vec_IntFree( vVars );
     Vec_PtrFree( vNodes );
     Vec_PtrFree( vSuper );
-    return 1;
+    return RetValue;
 }
 
 /**Function*************************************************************

src/base/abci/abcStrash.c

@@ -250,7 +250,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
     Abc_Obj_t * pFanin;
     int i;
     assert( Abc_ObjIsNode(pNodeOld) );
-    assert( Abc_NtkIsAigLogic(pNodeOld->pNtk) );
+    assert( Abc_NtkHasAig(pNodeOld->pNtk) && !Abc_NtkIsStrash(pNodeOld->pNtk) );
     // get the local AIG manager and the local root node
     pMan = pNodeOld->pNtk->pManFunc;
     pRoot = pNodeOld->pData;
@@ -317,7 +317,7 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
     // get the cutoff level
     LevelCut = ABC_MAX( 0, Abc_AigGetLevelNum(pNtk) - nLevels );
     // start the network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
     // create PIs below the cut and nodes above the cut

src/base/abci/abcUnreach.c

@@ -284,7 +284,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     int i;
 
     // start the new network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
     pNtkNew->pName = Extra_UtilStrsav( "exdc" );
     pNtkNew->pSpec = NULL;
 

src/base/abci/abcVanEijk.c

@@ -514,7 +514,7 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF
     if ( vCorresp )
         Vec_PtrFill( vCorresp, (nFrames + fAddLast)*Abc_NtkObjNumMax(pNtk), NULL );
     // start the new network
-    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     if ( fShortNames )
     {
         pNtkFrames->pName = Extra_UtilStrsav(pNtk->pName);
@@ -719,7 +719,7 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
     assert( Abc_NtkIsStrash(pNtk) );
 
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     pNtkNew->pName = Extra_UtilStrsav("exdc");
     pNtkNew->pSpec = NULL;
 

src/base/abci/abcVanImp.c

@@ -877,7 +877,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I
     assert( Abc_NtkIsStrash(pNtk) );
 
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     pNtkNew->pName = Extra_UtilStrsav( "exdc" );
     pNtkNew->pSpec = NULL;
 

src/base/io/io.c

@@ -50,6 +50,8 @@ static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv );
 
+extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -667,13 +669,13 @@ usage:
 ***********************************************************************/
 int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Abc_Ntk_t * pNtk;
+    Abc_Ntk_t * pNtk, * pNtkNew;
     Abc_Lib_t * pDesign;
     char * FileName;
     FILE * pFile;
     int fCheck;
     int c;
-    extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck );
+    extern Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib );
 
     fCheck = 1;
     Extra_UtilGetoptReset();
@@ -709,21 +711,32 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     // set the new network
-    pDesign = Ver_ParseFile( FileName, Abc_FrameReadLibVer(), fCheck );
+    pDesign = Ver_ParseFile( FileName, Abc_FrameReadLibVer(), fCheck, 1 );
     if ( pDesign == NULL )
     {
         fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" );
         return 1;
     }
+
     // derive root design
     pNtk = Abc_LibDeriveRoot( pDesign );
+    Abc_LibFree( pDesign );
     if ( pNtk == NULL )
     {
         fprintf( pAbc->Err, "Deriving root module has failed.\n" );
         return 1;
     }
+
+    // derive the AIG network from this design
+    pNtkNew = Abc_LibDeriveAig( pNtk, Abc_FrameReadLibVer() );
+    Abc_NtkDelete( pNtk );
+    if ( pNtkNew == NULL )
+    {
+        fprintf( pAbc->Err, "Converting root module to AIG has failed.\n" );
+        return 1;
+    }
     // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
     return 0;
 
 usage:
@@ -753,7 +766,6 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pFile;
     int fCheck;
     int c;
-    extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck );
 
     fCheck = 1;
     Extra_UtilGetoptReset();
@@ -789,7 +801,7 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     // set the new network
-    pLibrary = Ver_ParseFile( FileName, NULL, fCheck );
+    pLibrary = Ver_ParseFile( FileName, NULL, fCheck, 0 );
     if ( pLibrary == NULL )
     {
         fprintf( pAbc->Err, "Reading library from the verilog file has failed.\n" );
@@ -1613,7 +1625,7 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
         fprintf( pAbc->Out, "Writing PLA has failed.\n" );
         return 0;
     }
-    Io_WriteVerilog( pNtkTemp, FileName );
+    Io_WriteVerilog( pNtkTemp, FileName, 0 );
     Abc_NtkDelete( pNtkTemp );
     return 0;
 
@@ -1638,10 +1650,10 @@ usage:
 ***********************************************************************/
 int IoCommandWriteVerLib( Abc_Frame_t * pAbc, int argc, char **argv )
 {
-    st_table * tLibrary;
+    Abc_Lib_t * pLibrary;
     char * FileName;
     int c;
-    extern void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName );
+    extern void Io_WriteVerilogLibrary( Abc_Lib_t * pLibrary, char * pFileName );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
@@ -1663,13 +1675,13 @@ int IoCommandWriteVerLib( Abc_Frame_t * pAbc, int argc, char **argv )
     FileName = argv[globalUtilOptind];
 
     // derive the netlist
-    tLibrary = Abc_FrameReadLibVer();
-    if ( tLibrary == NULL )
+    pLibrary = Abc_FrameReadLibVer();
+    if ( pLibrary == NULL )
     {
         fprintf( pAbc->Out, "Verilog library is not specified.\n" );
         return 0;
     }
-    Io_WriteVerilogLibrary( tLibrary, FileName );
+    Io_WriteVerilogLibrary( pLibrary, FileName );
     return 0;
 
 usage:
@@ -1741,7 +1753,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
         int i;
         if ( pFile == NULL )
         {
-            fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", FileName );
+            fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", FileName );
             return 1;
         }
         if ( fNames )

src/base/io/io.h

@@ -97,7 +97,7 @@ extern void               Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int
 /*=== abcWritePla.c ==========================================================*/
 extern int                Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteVerilog.c ==========================================================*/
-extern void               Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName );
+extern void               Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName, int fVerLibStyle );
 
 #ifdef __cplusplus
 }

src/base/io/ioReadBaf.c

@@ -73,7 +73,7 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
     nAnds = atoi( pCur );     while ( *pCur++ );
 
     // allocate the empty AIG
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkNew->pName = Extra_UtilStrsav( pName );
     pNtkNew->pSpec = Extra_UtilStrsav( pFileName );
 

src/base/io/ioReadBlif.c

@@ -211,7 +211,7 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
     assert( p->vTokens != NULL );
 
     // create the new network
-    p->pNtkCur = pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP );
+    p->pNtkCur = pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
     // read the model name
     if ( strcmp( p->vTokens->pArray[0], ".model" ) == 0 )
         pNtk->pName = Extra_UtilStrsav( p->vTokens->pArray[1] );

src/base/io/ioReadVerilog.c

@@ -271,7 +271,7 @@ Abc_Ntk_t * Io_ReadVerNetwork( Io_ReadVer_t * p )
     pModelName = vTokens->pArray[1];
 
     // allocate the empty network
-    pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP );
+    pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
     pNtk->pName = Extra_UtilStrsav( pModelName );
     pNtk->pSpec = Extra_UtilStrsav( p->pFileName );
 

src/base/io/ioWriteVer.c

@@ -26,7 +26,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fVerLibStyle );
 static void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
@@ -34,6 +34,7 @@ static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogGates( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogVerLibStyle( FILE * pFile, Abc_Ntk_t * pNtk );
 static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
 static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
 static int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
@@ -53,7 +54,7 @@ static int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
+void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fVerLibStyle )
 {
     FILE * pFile;
 
@@ -75,7 +76,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
 
     // write the equations for the network
     fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
-    Io_WriteVerilogInt( pFile, pNtk );
+    Io_WriteVerilogInt( pFile, pNtk, fVerLibStyle );
     fprintf( pFile, "\n" );
     fclose( pFile );
 }
@@ -91,12 +92,11 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName )
+void Io_WriteVerilogLibrary( Abc_Lib_t * pLibrary, char * pFileName )
 {
     FILE * pFile;
-    st_generator * gen;
     Abc_Ntk_t * pNtk, * pNetlist;
-    char * pName;
+    int i;
 
     // start the output stream
     pFile = fopen( pFileName, "w" );
@@ -109,15 +109,17 @@ void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName )
     fprintf( pFile, "// Verilog library \"%s\" written by ABC on %s\n", pFileName, Extra_TimeStamp() );
     fprintf( pFile, "\n" );
     // write modules
-    st_foreach_item( tLibrary, gen, (char**)&pName, (char**)&pNtk )
+    Vec_PtrForEachEntry( pLibrary->vModules, pNtk, i )
     {
         // create netlist
-        pNetlist = Abc_NtkLogicToNetlist( pNtk, 0 );
+//        pNetlist = Abc_NtkLogicToNetlist( pNtk, 0 );
+        assert( Abc_NtkIsNetlist(pNtk) );
+        pNetlist = pNtk;
         // write the equations for the network
-        Io_WriteVerilogInt( pFile, pNetlist );
+        Io_WriteVerilogInt( pFile, pNetlist, 1 );
         fprintf( pFile, "\n" );
         // delete the netlist
-        Abc_NtkDelete( pNetlist );
+//        Abc_NtkDelete( pNetlist );
     }
 
     fclose( pFile );
@@ -134,7 +136,7 @@ void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
+void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fVerLibStyle )
 {
     // write inputs and outputs
     fprintf( pFile, "module %s ( gclk,\n   ", Abc_NtkName(pNtk) );
@@ -161,8 +163,10 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
     Io_WriteVerilogWires( pFile, pNtk, 4 );
     fprintf( pFile, ";\n" );
     }
-    // write the nodes
-    if ( Abc_NtkHasMapping(pNtk) )
+    // write nodes
+    if ( fVerLibStyle )
+        Io_WriteVerilogVerLibStyle( pFile, pNtk );        
+    else if ( Abc_NtkHasMapping(pNtk) )
         Io_WriteVerilogGates( pFile, pNtk );
     else
         Io_WriteVerilogNodes( pFile, pNtk );
@@ -438,6 +442,65 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Writes the nodes and boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogVerLibStyle( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Vec_Vec_t * vLevels;
+    Abc_Ntk_t * pNtkGate;
+    Abc_Obj_t * pObj, * pTerm, * pFanin;
+    Aig_Obj_t * pFunc;
+    int i, k, Counter, nDigits;
+
+    Counter = 1;
+    nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) );
+
+    // write boxes
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        pNtkGate = pObj->pData;
+        fprintf( pFile, "  %s g%0*d", pNtkGate->pName, nDigits, Counter++ );
+        fprintf( pFile, "(" );
+        Abc_NtkForEachPi( pNtkGate, pTerm, k )
+        {
+            fprintf( pFile, ".%s ",   Io_WriteVerilogGetName(Abc_ObjFanout0(pTerm)) );
+            fprintf( pFile, "(%s), ", Io_WriteVerilogGetName(Abc_ObjFanin(pObj,k)) );
+        }
+        Abc_NtkForEachPo( pNtkGate, pTerm, k )
+        {
+            fprintf( pFile, ".%s ",   Io_WriteVerilogGetName(Abc_ObjFanin0(pTerm)) );
+            fprintf( pFile, "(%s)%s", Io_WriteVerilogGetName(Abc_ObjFanout(pObj,k)), k==Abc_NtkPoNum(pNtkGate)-1? "":", " );
+        }
+        fprintf( pFile, ");\n" );
+    }
+    // write nodes
+    vLevels = Vec_VecAlloc( 10 );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        pFunc = pObj->pData;
+        fprintf( pFile, "  assign %s = ", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+        // set the input names
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Aig_IthVar(pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(pFanin));
+        // write the formula
+        Aig_ObjPrintVerilog( pFile, pFunc, vLevels, 0 );
+        fprintf( pFile, ";\n" );
+        // clear the input names
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            free( Aig_IthVar(pNtk->pManFunc, k)->pData );
+    }
+    Vec_VecFree( vLevels );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Writes the gates.]
 
   Description []

src/base/seq/seqAigCore.c

@@ -303,7 +303,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int
 
     // create the network for the initial state computation
     // start the table and the array of PO values
-    pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
     tTable   = stmm_init_table( stmm_numcmp, stmm_numhash );
     vValues  = Vec_IntAlloc( 100 );
 

src/base/seq/seqCreate.c

@@ -86,7 +86,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
     assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
 
     // start the network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -109,7 +109,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
         Vec_PtrWriteEntry( pNtkNew->vObjs, pObj->pCopy->Id, pObj->pCopy );
         pNtkNew->nObjs++;
     }
-    pNtkNew->nNodes = pNtk->nNodes;
+    pNtkNew->nObjCounts[ABC_OBJ_NODE] = pNtk->nObjCounts[ABC_OBJ_NODE];
 
     // create PI/PO and their names
     Abc_NtkForEachPi( pNtk, pObj, i )

src/base/seq/seqRetCore.c

@@ -116,7 +116,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
     }
 
     // start the network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);

src/misc/extra/extraUtilMemory.c

@@ -322,7 +322,7 @@ Extra_MmFlex_t * Extra_MmFlexStart()
     p->pCurrent      = NULL;
     p->pEnd          = NULL;
 
-    p->nChunkSize    = (1 << 12);
+    p->nChunkSize    = (1 << 10);
     p->nChunksAlloc  = 64;
     p->nChunks       = 0;
     p->pChunks       = ALLOC( char *, p->nChunksAlloc );

src/misc/vec/vecInt.h

@@ -494,14 +494,18 @@ static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int
 
         if ( p->nSize == 0 )
             p->nCap = 1;
+        if ( pMemMan )
             pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
-//        pArray = ALLOC( int, p->nCap * 2 );
+        else
+            pArray = ALLOC( int, p->nCap * 2 );
         if ( p->pArray )
         {
             for ( i = 0; i < p->nSize; i++ )
                 pArray[i] = p->pArray[i];
+            if ( pMemMan )
                 Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
-//            free( p->pArray );
+            else
+                free( p->pArray );
         }
         p->nCap *= 2;
         p->pArray = pArray;

src/sat/csat/csat_apis.c

@@ -79,7 +79,7 @@ ABC_Manager ABC_InitManager()
     Abc_Start();
     mng = ALLOC( ABC_Manager_t, 1 );
     memset( mng, 0, sizeof(ABC_Manager_t) );
-    mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
     mng->pNtk->pName = Extra_UtilStrsav("csat_network");
     mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
     mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);

src/temp/aig/aig.h

@@ -290,9 +290,11 @@ extern void            Aig_TableProfile( Aig_Man_t * p );
 /*=== aigUtil.c =========================================================*/
 extern void            Aig_ManIncrementTravId( Aig_Man_t * p );
 extern void            Aig_ManCleanData( Aig_Man_t * p );
-extern int             Aig_ObjMffcLabel( Aig_Man_t * p, Aig_Obj_t * pNode );
+extern void            Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper );
 extern int             Aig_ObjIsMuxType( Aig_Obj_t * pObj );
+extern int             Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 );
 extern Aig_Obj_t *     Aig_ObjRecognizeMux( Aig_Obj_t * pObj, Aig_Obj_t ** ppObjT, Aig_Obj_t ** ppObjE );
+extern void            Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
 extern void            Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
 extern void            Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
 

src/temp/aig/aigUtil.c

@@ -73,6 +73,46 @@ void Aig_ManCleanData( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Detects multi-input gate rooted at this node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjCollectMulti_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
+{
+    if ( pRoot != pObj && (Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || Aig_ObjType(pRoot) != Aig_ObjType(pObj)) )
+    {
+        Vec_PtrPushUnique(vSuper, pObj);
+        return;
+    }
+    Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild0(pObj), vSuper );
+    Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild1(pObj), vSuper );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Detects multi-input gate rooted at this node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjCollectMulti( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper )
+{
+    assert( !Aig_IsComplement(pRoot) );
+    Vec_PtrClear( vSuper );
+    Aig_ObjCollectMulti_rec( pRoot, pRoot, vSuper );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
 
   Description []
@@ -106,6 +146,48 @@ int Aig_ObjIsMuxType( Aig_Obj_t * pNode )
            (Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)));
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Recognizes what nodes are inputs of the EXOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 )
+{
+    Aig_Obj_t * p0, * p1;
+    assert( !Aig_IsComplement(pObj) );
+    if ( !Aig_ObjIsNode(pObj) )
+        return 0;
+    if ( Aig_ObjIsExor(pObj) )
+    {
+        *ppFan0 = Aig_ObjChild0(pObj);
+        *ppFan1 = Aig_ObjChild1(pObj);
+        return 1;
+    }
+    assert( Aig_ObjIsAnd(pObj) );
+    p0 = Aig_ObjChild0(pObj);
+    p1 = Aig_ObjChild1(pObj);
+    if ( !Aig_IsComplement(p0) || !Aig_IsComplement(p1) )
+        return 0;
+    p0 = Aig_Regular(p0);
+    p1 = Aig_Regular(p1);
+    if ( !Aig_ObjIsAnd(p0) || !Aig_ObjIsAnd(p1) )
+        return 0;
+    if ( Aig_ObjFanin0(p0) != Aig_ObjFanin0(p1) || Aig_ObjFanin1(p0) != Aig_ObjFanin1(p1) )
+        return 0;
+    if ( Aig_ObjFaninC0(p0) == Aig_ObjFaninC0(p1) || Aig_ObjFaninC1(p0) == Aig_ObjFaninC1(p1) )
+        return 0;
+    *ppFan0 = Aig_ObjChild0(p0);
+    *ppFan1 = Aig_ObjChild1(p0);
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Recognizes what nodes are control and data inputs of a MUX.]
@@ -198,6 +280,95 @@ Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pNode, Aig_Obj_t ** ppNodeT, Aig_Ob
     return NULL;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Prints Verilog formula for the AIG rooted at this node.]
+
+  Description [The formula is in terms of PIs, which should have
+  their names assigned in pObj->pData fields.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
+{
+    Vec_Ptr_t * vSuper;
+    Aig_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC;
+    int fCompl, i;
+    // store the complemented attribute
+    fCompl = Aig_IsComplement(pObj);
+    pObj = Aig_Regular(pObj);
+    // constant case
+    if ( Aig_ObjIsConst1(pObj) )
+    {
+        fprintf( pFile, "%d", !fCompl );
+        return;
+    }
+    // PI case
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        fprintf( pFile, "%s%s", fCompl? "~" : "", pObj->pData );
+        return;
+    }
+    // EXOR case
+    if ( Aig_ObjIsExor(pObj) )
+    {
+        Vec_VecExpand( vLevels, Level );
+        vSuper = Vec_VecEntry( vLevels, Level );
+        Aig_ObjCollectMulti( pObj, vSuper );
+        fprintf( pFile, "%s", (Level==0? "" : "(") );
+        Vec_PtrForEachEntry( vSuper, pFanin, i )
+        {
+            Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 );
+            if ( i < Vec_PtrSize(vSuper) - 1 )
+                fprintf( pFile, " ^ " );
+        }
+        fprintf( pFile, "%s", (Level==0? "" : ")") );
+        return;
+    }
+    // MUX case
+    if ( Aig_ObjIsMuxType(pObj) )
+    {
+        if ( Aig_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) )
+        {
+            fprintf( pFile, "%s", (Level==0? "" : "(") );
+            Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
+            fprintf( pFile, " ^ " );
+            Aig_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 );
+            fprintf( pFile, "%s", (Level==0? "" : ")") );
+        }
+        else 
+        {
+            pFaninC = Aig_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 );
+            fprintf( pFile, "%s", (Level==0? "" : "(") );
+            Aig_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 );
+            fprintf( pFile, " ? " );
+            Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin1, fCompl), vLevels, Level+1 );
+            fprintf( pFile, " : " );
+            Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
+            fprintf( pFile, "%s", (Level==0? "" : ")") );
+        }
+        return;
+    }
+    // AND case
+    Vec_VecExpand( vLevels, Level );
+    vSuper = Vec_VecEntry(vLevels, Level);
+    Aig_ObjCollectMulti( pObj, vSuper );
+    fprintf( pFile, "%s", (Level==0? "" : "(") );
+    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    {
+        Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 );
+        if ( i < Vec_PtrSize(vSuper) - 1 )
+            fprintf( pFile, " %s ", fCompl? "|" : "&" );
+    }
+    fprintf( pFile, "%s", (Level==0? "" : ")") );
+    return;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Prints node in HAIG.]
@@ -250,6 +421,8 @@ void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig )
     printf( "\n" );
 }
 
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/temp/ver/ver.h

@@ -52,7 +52,9 @@ struct Ver_Man_t_
     // current network and library
     Abc_Ntk_t *     pNtkCur;       // the network under construction
     Abc_Lib_t *     pDesign;       // the current design 
-    Abc_Lib_t *     pGateLib;      // the current technology library
+    // parameters
+    int             fUseMemMan;    // allocate memory manager in the networks
+    int             fCheck;        // checks network for currectness
     // error recovery
     FILE *          Output;
     int             fTopLevel;
@@ -77,10 +79,11 @@ struct Ver_Man_t_
 ////////////////////////////////////////////////////////////////////////
 
 /*=== verCore.c ========================================================*/
-extern Abc_Lib_t *    Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck );
+extern Abc_Lib_t *    Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
 extern void           Ver_ParsePrintErrorMessage( Ver_Man_t * p );
 /*=== verFormula.c ========================================================*/
 extern void *         Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage );
+extern void *         Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage );
 /*=== verParse.c ========================================================*/
 extern int            Ver_ParseSkipComments( Ver_Man_t * p );
 extern char *         Ver_ParseGetName( Ver_Man_t * p );

src/temp/ver/verFormula.c

@@ -277,7 +277,7 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_
                     break;
                 }
                 Oper2 = Vec_IntPop( vStackOp ); // the operation before the last one
-                if ( Oper2 >= Oper1 )  
+                if ( Oper2 >= Oper1 && !(Oper1 == Oper2 && Oper1 == VER_PARSE_OPER_MUX) )  
                 {  // if Oper2 precedence is higher or equal, execute it
                     if ( Ver_FormulaParserTopOper( pMan, vStackFn, Oper2 ) == NULL )
                     {
@@ -378,7 +378,7 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
     int nLength, nLength2, i;
     // find the end of the string delimited by other characters
     pTemp = pString;
-    while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && 
+    while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && *pTemp != ',' && *pTemp != '}' && 
             *pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE && 
             *pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 && 
             *pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR && 
@@ -402,6 +402,55 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
     return i;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the AIG representation of the reduction formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage )
+{
+    Aig_Obj_t * pRes;
+    int v, fCompl;
+    char Symbol;
+
+    // get the operation
+    Symbol = *pFormula++;
+    fCompl = ( Symbol == '~' );
+    if ( fCompl )
+        Symbol = *pFormula++;
+    // check the operation
+    if ( Symbol != '&' && Symbol != '|' && Symbol != '^' )
+    {
+        sprintf( pErrorMessage, "Ver_FormulaReduction(): Unknown operation (%c)\n", Symbol );
+        return NULL;
+    }
+    // skip the brace
+    while ( *pFormula++ != '{' );
+    // parse the names
+    Vec_PtrClear( vNames );
+    while ( *pFormula != '}' )
+    {
+        v = Ver_FormulaParserFindVar( pFormula, vNames );
+        pFormula += (int)Vec_PtrEntry( vNames, 2*v );
+        while ( *pFormula == ' ' || *pFormula == ',' )
+            pFormula++;
+    }
+    // compute the function
+    if ( Symbol == '&' )
+        pRes = Aig_CreateAnd( pMan, Vec_PtrSize(vNames)/2 );
+    else if ( Symbol == '|' )
+        pRes = Aig_CreateOr( pMan, Vec_PtrSize(vNames)/2 );
+    else if ( Symbol == '^' )
+        pRes = Aig_CreateExor( pMan, Vec_PtrSize(vNames)/2 );
+    return Aig_NotCond( pRes, fCompl );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////