Special BLIF writing (bug fixes).

3 files changed, 50 insertions, 49 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index c0f6b5a9..7f077e29 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1559,9 +1559,9 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the corresponding file writer
-//    if ( fSpecial )
-//        Io_WriteBlifSpecial( pAbc->pNtkCur, pFileName );
-//    else
+    if ( fSpecial )
+        Io_WriteBlifSpecial( pAbc->pNtkCur, pFileName );
+    else
         Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIF );
     return 0;
 
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 2a28f6ab..52856437 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -641,19 +641,21 @@ void Abc_NtkConvertBb2Wb( char * pFileNameIn, char * pFileNameOut, int fSeq, int
   SeeAlso     []
 
 ***********************************************************************/
-char * Io_NtkDeriveSop( Mem_Flex_t * pMem, unsigned uTruth, int nVars )
+char * Io_NtkDeriveSop( Mem_Flex_t * pMem, unsigned uTruth, int nVars, Vec_Int_t * vCover )
 {
     char * pSop;
-    Vec_Int_t * vCover = Vec_IntAlloc( 100 );
     int RetValue = Kit_TruthIsop( &uTruth, nVars, vCover, 1 );
     assert( RetValue == 0 || RetValue == 1 );
     // check the case of constant cover
-    assert( !(Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0)) );
+    if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) )
+    {
+        assert( RetValue == 0 );
+        return Vec_IntSize(vCover) == 0 ? " 0\n" : " 1\n";
+    }
     // derive the AIG for that tree
     pSop = Abc_SopCreateFromIsop( pMem, nVars, vCover );
     if ( RetValue )
         Abc_SopComplement( pSop );
-    Vec_IntFree( vCover );
     return pSop;
 }
 
@@ -668,7 +670,7 @@ char * Io_NtkDeriveSop( Mem_Flex_t * pMem, unsigned uTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode )
+void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCover )
 {
     Abc_Obj_t * pNet;
     int i, nVars = Abc_ObjFaninNum(pNode);
@@ -677,6 +679,8 @@ void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode )
         printf( "Node \"%s\" has more than 7 inputs. Writing BLIF has failed.\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
         return;
     }
+
+    fprintf( pFile, "\n" );
     if ( nVars <= 4 )
     {
         // write the .names line
@@ -716,6 +720,7 @@ void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode )
             uTruth6 = Abc_SopToTruth( (char*)Abc_ObjData(pNode), nVars );
             iVar = If_Dec6PickBestMux( uTruth6, Cofs6 );
         }
+
         // perform MUX decomposition
         if ( iVar >= 0 )
         {
@@ -731,41 +736,49 @@ void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode )
             }
             assert( nVarsMin[0] < 5 );
             assert( nVarsMin[1] < 5 );
+            // write MUX
+            fprintf( pFile, ".names" );
+            fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,iVar)) );
+            fprintf( pFile, " %s_cascade0", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            fprintf( pFile, " %s_cascade1", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            fprintf( pFile, " %s\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            fprintf( pFile, "1-1 1\n01- 1\n" );
             // write cofactors
             for ( c = 0; c < 2; c++ )
             {
                 pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, 
-                    (unsigned)(nVars == 7 ? Cofs7[c][0] : Cofs6[c]), nVarsMin[c] );
+                    (unsigned)(nVars == 7 ? Cofs7[c][0] : Cofs6[c]), nVarsMin[c], vCover );
                 fprintf( pFile, ".names" );
                 for ( i = 0; i < nVarsMin[c]; i++ )
                     fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,pVars[c][i])) );
                 fprintf( pFile, " %s_cascade%d\n", Abc_ObjName(Abc_ObjFanout0(pNode)), c );
                 fprintf( pFile, "%s", pSop );
             }
-            // write MUX
-            fprintf( pFile, ".names" );
-            fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,iVar)) );
-            fprintf( pFile, " %s_cascade0", Abc_ObjName(Abc_ObjFanout0(pNode)) );
-            fprintf( pFile, " %s_cascade1", Abc_ObjName(Abc_ObjFanout0(pNode)) );
-            fprintf( pFile, " %s\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
-            fprintf( pFile, "1-1 1\n01- 1\n" );
             return;
         }
+        assert( nVars == 6 || nVars == 7 );
 
         // try cascade decomposition
         if ( nVars == 7 )
+        {
             z = If_Dec7Perform( uTruth7, 1 );
+            //If_Dec7Verify( uTruth7, z );
+        }
         else
+        {
             z = If_Dec6Perform( uTruth6, 1 );
+            //If_Dec6Verify( uTruth6, z );
+        }
         if ( z == 0 )
         {
             printf( "Node \"%s\" is not decomposable. Writing BLIF has failed.\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
             return;
         }
 
-        // collect the nodes
-        for ( c = 0; c < 2; i++ )
+        // derive nodes
+        for ( c = 1; c >= 0; c-- )
         {
+            // collect fanins
             uTruth7[c]  = ((c ? z >> 32 : z) & 0xffff);
             uTruth7[c] |= (uTruth7[c] << 16);
             uTruth7[c] |= (uTruth7[c] << 32);
@@ -773,18 +786,20 @@ void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode )
                 pVars[c][i] = (z >> (c*32+16+4*i)) & 7;
 
             // minimize truth table
-            Cofs6[i] = If_Dec6MinimumBase( uTruth7[i], pVars[i], 4, &nVarsMin[i] );
-            assert( c ? nVarsMin[0] == 4 : nVarsMin[1] <= 4 );
+            Cofs6[c] = If_Dec6MinimumBase( uTruth7[c], pVars[c], 4, &nVarsMin[c] );
 
             // write the nodes
-            pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, (unsigned)Cofs6[c], nVarsMin[c] );
             fprintf( pFile, ".names" );
             for ( i = 0; i < nVarsMin[c]; i++ )
                 if ( pVars[c][i] == 7 )
                     fprintf( pFile, " %s_cascade", Abc_ObjName(Abc_ObjFanout0(pNode)) );
                 else
                     fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,pVars[c][i])) );
-            fprintf( pFile, " %s%s\n", Abc_ObjName(Abc_ObjFanout0(pNode)), c? "_cascade" : "" );
+                fprintf( pFile, " %s%s\n", Abc_ObjName(Abc_ObjFanout0(pNode)), c? "" : "_cascade" );
+
+            // write SOP
+            pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, 
+                (unsigned)Cofs6[c], nVarsMin[c], vCover );
             fprintf( pFile, "%s", pSop );
         }
     }
@@ -804,6 +819,7 @@ void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode )
 void Io_WriteBlifInt( Abc_Ntk_t * pNtk, char * FileName )
 {
     FILE * pFile;
+    Vec_Int_t * vCover;
     Abc_Obj_t * pNode, * pLatch;
     int i;
     assert( Abc_NtkIsNetlist(pNtk) );
@@ -833,8 +849,10 @@ void Io_WriteBlifInt( Abc_Ntk_t * pNtk, char * FileName )
     if ( Abc_NtkLatchNum(pNtk) )
         fprintf( pFile, "\n" );
     // write each internal node
+    vCover = Vec_IntAlloc( (1<<16) );
     Abc_NtkForEachNode( pNtk, pNode, i )
-        Io_NtkWriteNodeInt( pFile, pNode );
+        Io_NtkWriteNodeInt( pFile, pNode, vCover );
+    Vec_IntFree( vCover );
     // write the end
     fprintf( pFile, ".end\n\n" );
     fclose( pFile );
diff --git a/src/map/if/ifDec.c b/src/map/if/ifDec.c
index 2dd91cd2..38952217 100644
--- a/src/map/if/ifDec.c
+++ b/src/map/if/ifDec.c
@@ -72,7 +72,7 @@ extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-static void If_DecPrintConfig( word z )
+void If_DecPrintConfig( word z )
 {
    unsigned S[1];
    S[0] = (z & 0xffff) | ((z & 0xffff) << 16);
@@ -113,7 +113,7 @@ static word If_Dec6ComposeLut4( int t, word f[4] )
     }
     return r;
 }
-static void If_Dec6Verify( word t, word z )
+void If_Dec6Verify( word t, word z )
 {
     word r, q, f[4];
     int i, v;
@@ -160,7 +160,7 @@ static void If_Dec7ComposeLut4( int t, word f[4][2], word r[2] )
         r[1] |= c[1];
     }
 }
-static void If_Dec7Verify( word t[2], word z )
+void If_Dec7Verify( word t[2], word z )
 {
     word f[4][2], r[2];
     int i, v;
@@ -374,6 +374,7 @@ static word If_Dec7DeriveDisjoint( word t[2], int Pla2Var[7], int Var2Pla[7] )
     z |= ((word)((Cof1 << 8) | Cof0) << 32);
     for ( i = 0; i < 3; i++ )
         z |= (((word)Pla2Var[i]) << (48 + 4*i));
+    z |= (((word)7) << (48 + 4*i));
     return z;
 }
 
@@ -641,7 +642,7 @@ int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] )
 {
     word c0[2], c1[2];
     int v, vBest = -1, Count0, Count1, CountBest = 1000;
-    for ( v = 0; v < 6; v++ )
+    for ( v = 0; v < 7; v++ )
     {
         If_Dec7Cofactor( t, v, 0, c0 );
         If_Dec7Cofactor( t, v, 1, c1 );
@@ -659,7 +660,6 @@ int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] )
 }
 
 
-
 /**Function*************************************************************
 
   Synopsis    [Performs additional check.]
@@ -671,9 +671,9 @@ int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] )
   SeeAlso     []
 
 ***********************************************************************/
-int If_CutPerformCheckInt( unsigned * pTruth, int nVars, int nLeaves )
+int If_CutPerformCheck( unsigned * pTruth, int nVars, int nLeaves )
 {
-    int fDerive = 0;
+    int fDerive = 1;
     if ( nLeaves < 6 )
         return 1;
     if ( nLeaves == 6 )
@@ -696,30 +696,13 @@ int If_CutPerformCheckInt( unsigned * pTruth, int nVars, int nLeaves )
         z = If_Dec7Perform( t, fDerive );
         if ( fDerive && z )
             If_Dec7Verify( t, z );
+
+
         return z != 0;
     }
     assert( 0 );
     return 0;
 }
-int If_CutPerformCheck( unsigned * pTruth, int nVars, int nLeaves )
-{
-    int RetValue = If_CutPerformCheckInt( pTruth, nVars, nLeaves );
-/*
-//    if ( nLeaves == 6 || nLeaves == 7 )
-    if ( nLeaves == 7 )
-    {
-        if ( RetValue == 0 )
-        {
-            printf( "%d ", RetValue );
-            Kit_DsdPrintFromTruth( pTruth, nLeaves );
-            printf( "\n" );
-            If_CutPerformCheckInt( pTruth, nVars, nLeaves );
-        }
-    }
-*/
-    return RetValue;
-}
-
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///