Bug fixing in %blast when blasting mod operator (handling zero divisor).

src/base/abci/abcPrint.c

@@ -443,13 +443,13 @@ void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintFlops )
 
     fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) );
     Abc_NtkForEachPi( pNtk, pObj, i )
-        fprintf( pFile, " %s", Abc_ObjName(pObj) );
+        fprintf( pFile, " %d=%s", i, Abc_ObjName(pObj) );
 //        fprintf( pFile, " %s(%d)", Abc_ObjName(pObj), Abc_ObjFanoutNum(pObj) );
     fprintf( pFile, "\n" );
 
     fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) );
     Abc_NtkForEachPo( pNtk, pObj, i )
-        fprintf( pFile, " %s", Abc_ObjName(pObj) );
+        fprintf( pFile, " %d=%s", i, Abc_ObjName(pObj) );
     fprintf( pFile, "\n" );
 
     if ( !fPrintFlops )

src/base/wlc/wlc.h

@@ -270,7 +270,7 @@ extern int            Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd );
 /*=== wlcReadVer.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadVer( char * pFileName );
 /*=== wlcWriteVer.c ========================================================*/
-extern void           Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName );
+extern void           Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName, int fAddCos );
 
 
 ABC_NAMESPACE_HEADER_END

src/base/wlc/wlcBlast.c

@@ -742,7 +742,8 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
             else
                 Wlc_BlastDivider( pNew, pArg0, nRangeMax, pArg1, nRangeMax, pObj->Type == WLC_OBJ_ARI_DIVIDE, vRes );
             Vec_IntShrink( vRes, nRange );
-            Wlc_BlastZeroCondition( pNew, pFans1, nRange1, vRes );
+            if ( pObj->Type == WLC_OBJ_ARI_DIVIDE )
+                Wlc_BlastZeroCondition( pNew, pFans1, nRange1, vRes );
         }
         else if ( pObj->Type == WLC_OBJ_ARI_MINUS )
         {

src/base/wlc/wlcCom.c

@@ -178,12 +178,20 @@ int Abc_CommandWriteWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
     char * pFileName = NULL;
+    int fAddCos      =    0; 
+    int fSplitNodes  =    0; 
     int c, fVerbose  =    0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "anvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'a':
+            fAddCos ^= 1;
+            break;
+        case 'n':
+            fSplitNodes ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -207,12 +215,22 @@ int Abc_CommandWriteWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Output file name should be given on the command line.\n" );
         return 0;
     }
-    Wlc_WriteVer( pNtk, pFileName );
+    if ( fSplitNodes )
+    {
+        pNtk = Wlc_NtkDupSingleNodes( pNtk );
+        Wlc_WriteVer( pNtk, pFileName, fAddCos );
+        Wlc_NtkFree( pNtk );
+    }
+    else
+        Wlc_WriteVer( pNtk, pFileName, fAddCos );
+
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%write [-vh]\n" );
+    Abc_Print( -2, "usage: %%write [-anvh]\n" );
     Abc_Print( -2, "\t         writes the design into a file\n" );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",        fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-a     : toggle adding a CO for each node [default = %s]\n",       fAddCos? "yes": "no" );
+    Abc_Print( -2, "\t-n     : toggle splitting into individual nodes [default = %s]\n", fSplitNodes? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",    fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }

src/base/wlc/wlcNtk.c

@@ -531,6 +531,8 @@ Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p )
             continue;
         if ( pObj->Type == WLC_OBJ_ARI_MULTI )
             continue;
+        if ( pObj->Type == WLC_OBJ_MUX && Wlc_ObjFaninNum(pObj) > 3 )
+            continue;
         // create CIs for the fanins
         Wlc_ObjForEachFanin( pObj, iFanin, k )
         {

src/base/wlc/wlcReadVer.c

@@ -1194,7 +1194,7 @@ void Io_ReadWordTest( char * pFileName )
     Wlc_Ntk_t * pNtk = Wlc_ReadVer( pFileName );
     if ( pNtk == NULL )
         return;
-    Wlc_WriteVer( pNtk, "test.v" );
+    Wlc_WriteVer( pNtk, "test.v", 0 );
 
     pNew = Wlc_NtkBitBlast( pNtk, NULL );
     Gia_AigerWrite( pNew, "test.aig", 0, 0 );

src/base/wlc/wlcWriteVer.c

@@ -381,7 +381,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
     assert( !p->vInits || iFanin == (int)strlen(p->pInits) );
     fprintf( pFile, "endmodule\n\n" );
 } 
-void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName )
+void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName, int fAddCos )
 {
     FILE * pFile;
     pFile = fopen( pFileName, "w" );
@@ -393,7 +393,8 @@ void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName )
     fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", p->pName, Extra_TimeStamp() );
     fprintf( pFile, "\n" );
     Wlc_WriteTables( pFile, p );
-//    Wlc_WriteAddPos( p );
+    if ( fAddCos )
+        Wlc_WriteAddPos( p );
     Wlc_WriteVerInt( pFile, p );
     fprintf( pFile, "\n" );
     fclose( pFile );