Version abc60823

6 files changed, 105 insertions, 30 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index 0cc3c7d9..86e8845b 100644
--- a/src/base/io/io.c
+++ b/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 )
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 8c8d6bed..c42d2016 100644
--- a/src/base/io/io.h
+++ b/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
 }
diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c
index 83b642a0..367d693b 100644
--- a/src/base/io/ioReadBaf.c
+++ b/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 );
 
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index ade9051f..5d6bc2f1 100644
--- a/src/base/io/ioReadBlif.c
+++ b/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] );
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index a4610cac..4550d286 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/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 );
 
diff --git a/src/base/io/ioWriteVer.c b/src/base/io/ioWriteVer.c
index 594bf4eb..2234b3a3 100644
--- a/src/base/io/ioWriteVer.c
+++ b/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 []