Bug fixing in %blast when blasting MUX coming from always-statement.

5 files changed, 92 insertions, 63 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index c84fbf68..0767b354 100644
--- a/src/base/wlc/wlc.h
+++ b/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, int fAddCos );
+extern void           Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName, int fAddCos, int fNoFlops );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index eb6a2db6..74be8843 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -411,7 +411,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
     int fVerbose = 0;
     Tim_Man_t * pManTime = NULL;
     Gia_Man_t * pTemp, * pNew, * pExtra = NULL;
-    Wlc_Obj_t * pObj, * pPrev = NULL;
+    Wlc_Obj_t * pObj;
     Vec_Int_t * vBits = &p->vBits, * vTemp0, * vTemp1, * vTemp2, * vRes;
     int nBits = Wlc_NtkPrepareBits( p );
     int nRange, nRange0, nRange1, nRange2;
@@ -541,6 +541,23 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
         }
         else if ( pObj->Type == WLC_OBJ_MUX )
         {
+            // It is strange and disturbing that Verilog standard treats these statements differently:
+            // Statement 1:   
+            //     assign o = i ? b : a;
+            // Statement 2:
+            //     always @( i or a or b )
+            //       begin
+            //         case ( i )
+            //           0 : o = a ;
+            //           1 : o = b ;
+            //         endcase
+            //       end
+            // If a is signed and b is unsigned,  Statement 1 does not sign-extend a, while Statement 2 does.
+            // The signedness of o does not matter.
+            //
+            // Below we (somewhat arbitrarily) distinguish these two by assuming that 
+            // Statement 1 has three fanins, while Statement 2 has more than three fanins.
+            //
             int fSigned = 1;
             assert( nRange0 >= 1 && Wlc_ObjFaninNum(pObj) >= 3 );
             assert( 1 + (1 << nRange0) == Wlc_ObjFaninNum(pObj) );
@@ -555,7 +572,10 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
                     {
                         nRange1 = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
                         pFans1  = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, iFanin) );
-                        Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (fSigned? pFans1[nRange1-1] : 0) );
+                        if ( Wlc_ObjFaninNum(pObj) == 3 ) // Statement 1
+                            Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (fSigned? pFans1[nRange1-1] : 0) );
+                        else // Statement 2
+                            Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (Wlc_NtkObj(p, iFanin)->Signed? pFans1[nRange1-1] : 0) );
                     }
                 Vec_IntPush( vRes, Wlc_NtkMuxTree_rec(pNew, pFans0, nRange0, vTemp0, 0) );
             }
@@ -765,7 +785,6 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
         else assert( 0 );
         assert( Vec_IntSize(vBits) == Wlc_ObjCopy(p, i) );
         Vec_IntAppend( vBits, vRes );
-        pPrev = pObj;
         p->nAnds[pObj->Type] += Gia_ManAndNum(pNew) - nAndPrev;
     }
     p->nAnds[0] = Gia_ManAndNum(pNew);
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 57e97045..5213e152 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -180,9 +180,10 @@ int Abc_CommandWriteWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
     char * pFileName = NULL;
     int fAddCos      =    0; 
     int fSplitNodes  =    0; 
+    int fNoFlops     =    0;
     int c, fVerbose  =    0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "anvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "anfvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -192,6 +193,9 @@ int Abc_CommandWriteWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'n':
             fSplitNodes ^= 1;
             break;
+        case 'f':
+            fNoFlops ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -218,18 +222,19 @@ int Abc_CommandWriteWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fSplitNodes )
     {
         pNtk = Wlc_NtkDupSingleNodes( pNtk );
-        Wlc_WriteVer( pNtk, pFileName, fAddCos );
+        Wlc_WriteVer( pNtk, pFileName, fAddCos, fNoFlops );
         Wlc_NtkFree( pNtk );
     }
     else
-        Wlc_WriteVer( pNtk, pFileName, fAddCos );
+        Wlc_WriteVer( pNtk, pFileName, fAddCos, fNoFlops );
 
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%write [-anvh]\n" );
+    Abc_Print( -2, "usage: %%write [-anfvh]\n" );
     Abc_Print( -2, "\t         writes the design into a file\n" );
     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-f     : toggle skipping flops when writing file [default = %s]\n",fNoFlops? "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;
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 5f9b972c..05e02e9d 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1083,6 +1083,8 @@ startword:
             pObj = Wlc_NtkObj( p->pNtk, Vec_IntEntry(p->vFanins, 0) );
             if ( (1 << Wlc_ObjRange(pObj)) != Vec_IntSize(p->vFanins) - 1 )
                 return Wlc_PrsWriteErrorMessage( p, pStart, "The number of values in the case statement is wrong.", pName );
+            if ( Wlc_ObjRange(pObj) == 1 )
+                return Wlc_PrsWriteErrorMessage( p, pStart, "Always-statement with 1-bit control is not bit-blasted correctly.", pName );
             pObj = Wlc_NtkObj( p->pNtk, NameIdOut );
             Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_MUX );
             Wlc_ObjAddFanins( p->pNtk, pObj, p->vFanins );
@@ -1194,7 +1196,7 @@ void Io_ReadWordTest( char * pFileName )
     Wlc_Ntk_t * pNtk = Wlc_ReadVer( pFileName );
     if ( pNtk == NULL )
         return;
-    Wlc_WriteVer( pNtk, "test.v", 0 );
+    Wlc_WriteVer( pNtk, "test.v", 0, 0 );
 
     pNew = Wlc_NtkBitBlast( pNtk, NULL );
     Gia_AigerWrite( pNew, "test.aig", 0, 0 );
diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c
index f895d42c..4165b53d 100644
--- a/src/base/wlc/wlcWriteVer.c
+++ b/src/base/wlc/wlcWriteVer.c
@@ -144,20 +144,20 @@ void Wlc_WriteVerIntVec( FILE * pFile, Wlc_Ntk_t * p, Vec_Int_t * vVec, int Star
         NameCounter++;
     }
 } 
-void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
+void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
 {
     Wlc_Obj_t * pObj;
     int i, k, iFanin;
     char Range[100];
     fprintf( pFile, "module %s ( ", p->pName );
     fprintf( pFile, "\n   " );
-    if ( Wlc_NtkPiNum(p) > 0  )
+    if ( Wlc_NtkPiNum(p) > 0 || (fNoFlops && Wlc_NtkCiNum(p)) )
     {
-        Wlc_WriteVerIntVec( pFile, p, &p->vPis, 3 );
+        Wlc_WriteVerIntVec( pFile, p, fNoFlops ? &p->vCis : &p->vPis, 3 );
         fprintf( pFile, ",\n   " );
     }
-    if ( Wlc_NtkPoNum(p) > 0  )
-        Wlc_WriteVerIntVec( pFile, p, &p->vPos, 3 );
+    if ( Wlc_NtkPoNum(p) > 0 || (fNoFlops && Wlc_NtkCoNum(p))  )
+        Wlc_WriteVerIntVec( pFile, p, fNoFlops ? &p->vCos : &p->vPos, 3 );
     fprintf( pFile, "  );\n" );
     // mark fanins of rotation shifts
     Wlc_NtkForEachObj( p, pObj, i )
@@ -173,20 +173,20 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
         }
         sprintf( Range, "%s[%d:%d]%*s", Wlc_ObjIsSigned(pObj) ? "signed ":"       ", pObj->End, pObj->Beg, 8-nDigits, "" );
         fprintf( pFile, "  " );
-        if ( pObj->Type == WLC_OBJ_PI )
+        if ( pObj->Type == WLC_OBJ_PI || (fNoFlops && pObj->Type == WLC_OBJ_FO) )
             fprintf( pFile, "input  " );
-        else if ( pObj->fIsPo )
+        else if ( pObj->fIsPo || (fNoFlops && pObj->fIsFi) )
             fprintf( pFile, "output " );
         else
             fprintf( pFile, "       " );
-        if ( Wlc_ObjIsCi(pObj) || pObj->fIsPo )
+        if ( Wlc_ObjIsCi(pObj) || pObj->fIsPo || (fNoFlops && pObj->fIsFi) )
         {
             fprintf( pFile, "wire %s %s ;\n", Range, Wlc_ObjName(p, i) );
             if ( Wlc_ObjIsCi(pObj) )
                 continue;
             Range[0] = 0;
         }
-        if ( pObj->fIsPo )
+        if ( pObj->fIsPo || (fNoFlops && pObj->fIsFi) )
             fprintf( pFile, "  assign                         " );
         else if ( pObj->Type == WLC_OBJ_MUX && Wlc_ObjFaninNum(pObj) > 3 )
             fprintf( pFile, "reg  %s ", Range );
@@ -332,56 +332,59 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
     }
     iFanin = 0;
     assert( !p->vInits || Wlc_NtkFfNum(p) == Vec_IntSize(p->vInits) );
-    if ( p->vInits )
-    Wlc_NtkForEachCi( p, pObj, i )
+    if ( !fNoFlops )
     {
-        int nDigits   = Abc_Base10Log(pObj->End+1) + 1;
-        char * pName  = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
-        assert( i == Wlc_ObjCiId(pObj) );
-        if ( pObj->Type == WLC_OBJ_PI )
-            continue;
-        sprintf( Range, "       [%d:%d]%*s", Wlc_ObjRange(pObj) - 1, 0, 8-nDigits, "" );
-        fprintf( pFile, "         " );
-        fprintf( pFile, "wire %s ", Range );
-        fprintf( pFile, "%s_init%*s = ", pName, 11 - (int)strlen(pName), "" );
-        if ( Vec_IntEntry(p->vInits, i-Wlc_NtkPiNum(p)) > 0 )
-            fprintf( pFile, "%s", Wlc_ObjName(p, Wlc_ObjId(p, Wlc_NtkPi(p, Vec_IntEntry(p->vInits, i-Wlc_NtkPiNum(p))))));
-        else
+        if ( p->vInits )
+        Wlc_NtkForEachCi( p, pObj, i )
         {
-            fprintf( pFile, "%d\'b", Wlc_ObjRange(pObj) );
-            for ( k = 0; k < Wlc_ObjRange(pObj); k++ )
-                fprintf( pFile, "%c", p->pInits[iFanin + k] );
+            int nDigits   = Abc_Base10Log(pObj->End+1) + 1;
+            char * pName  = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
+            assert( i == Wlc_ObjCiId(pObj) );
+            if ( pObj->Type == WLC_OBJ_PI )
+                continue;
+            sprintf( Range, "       [%d:%d]%*s", Wlc_ObjRange(pObj) - 1, 0, 8-nDigits, "" );
+            fprintf( pFile, "         " );
+            fprintf( pFile, "wire %s ", Range );
+            fprintf( pFile, "%s_init%*s = ", pName, 11 - (int)strlen(pName), "" );
+            if ( Vec_IntEntry(p->vInits, i-Wlc_NtkPiNum(p)) > 0 )
+                fprintf( pFile, "%s", Wlc_ObjName(p, Wlc_ObjId(p, Wlc_NtkPi(p, Vec_IntEntry(p->vInits, i-Wlc_NtkPiNum(p))))));
+            else
+            {
+                fprintf( pFile, "%d\'b", Wlc_ObjRange(pObj) );
+                for ( k = Wlc_ObjRange(pObj)-1; k >= 0; k-- )
+                    fprintf( pFile, "%c", p->pInits[iFanin + k] );
+            }
+            fprintf( pFile, ";\n" );
+            iFanin += Wlc_ObjRange(pObj);
         }
-        fprintf( pFile, ";\n" );
-        iFanin += Wlc_ObjRange(pObj);
-    }
-    Wlc_NtkForEachCi( p, pObj, i )
-    {
-        assert( i == Wlc_ObjCiId(pObj) );
-        if ( pObj->Type == WLC_OBJ_PI )
-            continue;
-        fprintf( pFile, "         " );
-        fprintf( pFile, "CPL_FF" );
-        if ( Wlc_ObjRange(pObj) > 1 )
-            fprintf( pFile, "#%d%*s", Wlc_ObjRange(pObj), 4 - Abc_Base10Log(Wlc_ObjRange(pObj)+1), "" );
-        else
-            fprintf( pFile, "     " );
-        fprintf( pFile, " reg%d (",       i );
-        fprintf( pFile, " .q( %s ),",      Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
-        fprintf( pFile, " .qbar()," );
-        fprintf( pFile, " .d( %s ),",      Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFoToFi(p, pObj))) );
-        fprintf( pFile, " .clk( %s ),",    "1\'b0" );
-        fprintf( pFile, " .arst( %s ),",   "1\'b0" );
-        if ( p->vInits )
-            fprintf( pFile, " .arstval( %s_init )", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
-        else
-            fprintf( pFile, " .arstval( %s )", "1\'b0" );
-        fprintf( pFile, " ) ;\n" );
+        Wlc_NtkForEachCi( p, pObj, i )
+        {
+            assert( i == Wlc_ObjCiId(pObj) );
+            if ( pObj->Type == WLC_OBJ_PI )
+                continue;
+            fprintf( pFile, "         " );
+            fprintf( pFile, "CPL_FF" );
+            if ( Wlc_ObjRange(pObj) > 1 )
+                fprintf( pFile, "#%d%*s", Wlc_ObjRange(pObj), 4 - Abc_Base10Log(Wlc_ObjRange(pObj)+1), "" );
+            else
+                fprintf( pFile, "     " );
+            fprintf( pFile, " reg%d (",       i );
+            fprintf( pFile, " .q( %s ),",      Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
+            fprintf( pFile, " .qbar()," );
+            fprintf( pFile, " .d( %s ),",      Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFoToFi(p, pObj))) );
+            fprintf( pFile, " .clk( %s ),",    "1\'b0" );
+            fprintf( pFile, " .arst( %s ),",   "1\'b0" );
+            if ( p->vInits )
+                fprintf( pFile, " .arstval( %s_init )", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
+            else
+                fprintf( pFile, " .arstval( %s )", "1\'b0" );
+            fprintf( pFile, " ) ;\n" );
+        }
+        assert( !p->vInits || iFanin == (int)strlen(p->pInits) );
     }
-    assert( !p->vInits || iFanin == (int)strlen(p->pInits) );
     fprintf( pFile, "endmodule\n\n" );
 } 
-void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName, int fAddCos )
+void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName, int fAddCos, int fNoFlops )
 {
     FILE * pFile;
     pFile = fopen( pFileName, "w" );
@@ -395,7 +398,7 @@ void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName, int fAddCos )
     Wlc_WriteTables( pFile, p );
     if ( fAddCos )
         Wlc_WriteAddPos( p );
-    Wlc_WriteVerInt( pFile, p );
+    Wlc_WriteVerInt( pFile, p, fNoFlops );
     fprintf( pFile, "\n" );
     fclose( pFile );
 }