Adding switch -a to 'write_verilog' to write factored forms without XORs and MUXes.

7 files changed, 41 insertions, 28 deletions

diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index bf9f0c7b..6b8085cc 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -337,7 +337,7 @@ extern int             Hop_ObjIsMuxType( Hop_Obj_t * pObj );
 extern int             Hop_ObjRecognizeExor( Hop_Obj_t * pObj, Hop_Obj_t ** ppFan0, Hop_Obj_t ** ppFan1 );
 extern Hop_Obj_t *     Hop_ObjRecognizeMux( Hop_Obj_t * pObj, Hop_Obj_t ** ppObjT, Hop_Obj_t ** ppObjE );
 extern void            Hop_ObjPrintEqn( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
-extern void            Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
+extern void            Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level, int fOnlyAnds );
 extern void            Hop_ObjPrintVerbose( Hop_Obj_t * pObj, int fHaig );
 extern void            Hop_ManPrintVerbose( Hop_Man_t * p, int fHaig );
 extern void            Hop_ManDumpBlif( Hop_Man_t * p, char * pFileName );
diff --git a/src/aig/hop/hopUtil.c b/src/aig/hop/hopUtil.c
index 8cc7bdde..02cb08e3 100644
--- a/src/aig/hop/hopUtil.c
+++ b/src/aig/hop/hopUtil.c
@@ -366,7 +366,7 @@ void Hop_ObjPrintEqn( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int L
   SeeAlso     []
 
 ***********************************************************************/
-void Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
+void Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level, int fOnlyAnds )
 {
     Vec_Ptr_t * vSuper;
     Hop_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC;
@@ -387,7 +387,7 @@ void Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, i
         return;
     }
     // EXOR case
-    if ( Hop_ObjIsExor(pObj) )
+    if ( !fOnlyAnds && Hop_ObjIsExor(pObj) )
     {
         Vec_VecExpand( vLevels, Level );
         vSuper = Vec_VecEntry( vLevels, Level );
@@ -395,7 +395,7 @@ void Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, i
         fprintf( pFile, "%s", (Level==0? "" : "(") );
         Vec_PtrForEachEntry( Hop_Obj_t *, vSuper, pFanin, i )
         {
-            Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 );
+            Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1, fOnlyAnds );
             if ( i < Vec_PtrSize(vSuper) - 1 )
                 fprintf( pFile, " ^ " );
         }
@@ -403,25 +403,25 @@ void Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, i
         return;
     }
     // MUX case
-    if ( Hop_ObjIsMuxType(pObj) )
+    if ( !fOnlyAnds && Hop_ObjIsMuxType(pObj) )
     {
         if ( Hop_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) )
         {
             fprintf( pFile, "%s", (Level==0? "" : "(") );
-            Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin0, fCompl), vLevels, Level+1 );
+            Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin0, fCompl), vLevels, Level+1, fOnlyAnds );
             fprintf( pFile, " ^ " );
-            Hop_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 );
+            Hop_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1, fOnlyAnds );
             fprintf( pFile, "%s", (Level==0? "" : ")") );
         }
         else 
         {
             pFaninC = Hop_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 );
             fprintf( pFile, "%s", (Level==0? "" : "(") );
-            Hop_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 );
+            Hop_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1, fOnlyAnds );
             fprintf( pFile, " ? " );
-            Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin1, fCompl), vLevels, Level+1 );
+            Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin1, fCompl), vLevels, Level+1, fOnlyAnds );
             fprintf( pFile, " : " );
-            Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin0, fCompl), vLevels, Level+1 );
+            Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin0, fCompl), vLevels, Level+1, fOnlyAnds );
             fprintf( pFile, "%s", (Level==0? "" : ")") );
         }
         return;
@@ -433,7 +433,7 @@ void Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, i
     fprintf( pFile, "%s", (Level==0? "" : "(") );
     Vec_PtrForEachEntry( Hop_Obj_t *, vSuper, pFanin, i )
     {
-        Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin, fCompl), vLevels, Level+1 );
+        Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin, fCompl), vLevels, Level+1, fOnlyAnds );
         if ( i < Vec_PtrSize(vSuper) - 1 )
             fprintf( pFile, " %s ", fCompl? "|" : "&" );
     }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 20751d3b..b1d0df9b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -29075,7 +29075,7 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     Abc_NtkInsertHierarchyGia( pNtkSpec, pAbc->pNtkCur, fVerbose );
-    Io_WriteVerilog( pNtkSpec, pFileName );
+    Io_WriteVerilog( pNtkSpec, pFileName, 0 );
     Abc_NtkDelete( pNtkSpec );
     return 0;
 
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 2e1ae591..b047bf92 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -2719,13 +2719,16 @@ usage:
 int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
-    int c;
+    int c, fOnlyAnds = 0;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'a':
+                fOnlyAnds ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -2742,12 +2745,22 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the corresponding file writer
+    if ( fOnlyAnds )
+    {
+        Abc_Ntk_t * pNtkTemp = Abc_NtkToNetlist( pAbc->pNtkCur );
+        if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
+            Abc_NtkToAig( pNtkTemp );
+        Io_WriteVerilog( pNtkTemp, pFileName, 1 );
+        Abc_NtkDelete( pNtkTemp );
+    }
+    else
     Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_VERILOG );
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_verilog [-h] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_verilog [-ah] <file>\n" );
     fprintf( pAbc->Err, "\t         writes the current network in Verilog format\n" );
+    fprintf( pAbc->Err, "\t-a     : toggle writing expressions with only ANDs (without XORs and MUXes) [default = %s]\n", fOnlyAnds? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
     return 1;
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index 16980fbe..4f82efac 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -135,7 +135,7 @@ extern int                Io_WriteMoPla( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteSmv.c ===========================================================*/
 extern int                Io_WriteSmv( 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 fOnlyAnds );
 /*=== abcUtil.c ===============================================================*/
 extern Io_FileType_t      Io_ReadFileType( char * pFileName );
 extern Io_FileType_t      Io_ReadLibType( char * pFileName );
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 055efe91..c6b47b11 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -462,7 +462,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
     {
         if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
             Abc_NtkToAig( pNtkTemp );
-        Io_WriteVerilog( pNtkTemp, pFileName );
+        Io_WriteVerilog( pNtkTemp, pFileName, 0 );
     }
     else 
         fprintf( stderr, "Unknown file format.\n" );
@@ -590,7 +590,7 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
             if ( !Abc_NtkHasAig(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) )
                 Abc_NtkToAig( pNtkResult );
         }
-        Io_WriteVerilog( pNtkResult, pFileName );
+        Io_WriteVerilog( pNtkResult, pFileName, 0 );
     }
     else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV )
     {
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index c909e846..2e481324 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -29,13 +29,13 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds );
 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 );
 static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
-static void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds );
 static int  Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
 static char * Io_WriteVerilogGetName( char * pName );
 
@@ -54,7 +54,7 @@ static char * Io_WriteVerilogGetName( char * pName );
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
+void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fOnlyAnds )
 {
     Abc_Ntk_t * pNetlist;
     FILE * pFile;
@@ -81,7 +81,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
     if ( pNtk->pDesign )
     {
         // write the network first
-        Io_WriteVerilogInt( pFile, pNtk );
+        Io_WriteVerilogInt( pFile, pNtk, fOnlyAnds );
         // write other things
         Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pNetlist, i )
         {
@@ -89,12 +89,12 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
             if ( pNetlist == pNtk )
                 continue;
             fprintf( pFile, "\n" );
-            Io_WriteVerilogInt( pFile, pNetlist );
+            Io_WriteVerilogInt( pFile, pNetlist, fOnlyAnds );
         }
     }
     else
     {
-        Io_WriteVerilogInt( pFile, pNtk );
+        Io_WriteVerilogInt( pFile, pNtk, fOnlyAnds );
     }
 
     fprintf( pFile, "\n" );
@@ -112,7 +112,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
+void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
 {
     // write inputs and outputs
 //    fprintf( pFile, "module %s ( gclk,\n   ", Abc_NtkName(pNtk) );
@@ -163,7 +163,7 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
             fprintf( pFile, ";\n" );
         }
         // write nodes
-        Io_WriteVerilogObjects( pFile, pNtk );        
+        Io_WriteVerilogObjects( pFile, pNtk, fOnlyAnds );        
         // write registers
         if ( Abc_NtkLatchNum(pNtk) > 0 )
             Io_WriteVerilogLatches( pFile, pNtk );
@@ -483,7 +483,7 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk )
+void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
 {
     int fUseSimpleGateNames = 0;
     Vec_Vec_t * vLevels;
@@ -566,7 +566,7 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk )
             Abc_ObjForEachFanin( pObj, pFanin, k )
                 Hop_IthVar((Hop_Man_t *)pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(Abc_ObjName(pFanin)));
             // write the formula
-            Hop_ObjPrintVerilog( pFile, pFunc, vLevels, 0 );
+            Hop_ObjPrintVerilog( pFile, pFunc, vLevels, 0, fOnlyAnds );
             fprintf( pFile, ";\n" );
             // clear the input names
             Abc_ObjForEachFanin( pObj, pFanin, k )