Adding API to dump MiniAIG into a Verilog file and other small changes.

11 files changed, 144 insertions, 9 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 2e07c861..e9a9ea46 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -4771,6 +4771,10 @@ SOURCE=.\src\aig\gia\giaIiff.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaIiff.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaIso.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/giaIiff.h b/src/aig/gia/giaIiff.h
new file mode 100644
index 00000000..d1f9b5b3
--- /dev/null
+++ b/src/aig/gia/giaIiff.h
@@ -0,0 +1,54 @@
+/**CFile****************************************************************
+
+  FileName    [giaIiff.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaIiff.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__gia__giaIiff_h
+#define ABC__aig__gia__giaIiff_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c
index 3fb8aecb..9a6102fe 100644
--- a/src/aig/gia/giaMini.c
+++ b/src/aig/gia/giaMini.c
@@ -188,6 +188,7 @@ void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName )
 {
     Mini_Aig_t * p = Gia_ManToMiniAig( pGia );
     Mini_AigDump( p, pFileName );
+    //Mini_AigDumpVerilog( "test_miniaig.v", "top", p );
     Mini_AigStop( p );
 }
 
diff --git a/src/aig/miniaig/miniaig.h b/src/aig/miniaig/miniaig.h
index 217fea51..06769830 100644
--- a/src/aig/miniaig/miniaig.h
+++ b/src/aig/miniaig/miniaig.h
@@ -92,11 +92,13 @@ static void Mini_AigPush( Mini_Aig_t * p, int Lit0, int Lit1 )
 static int Mini_AigNodeFanin0( Mini_Aig_t * p, int Id )
 {
     assert( Id >= 0 && 2*Id < p->nSize );
+    assert( p->pArray[2*Id] == 0x7FFFFFFF || p->pArray[2*Id] < 2*Id );
     return p->pArray[2*Id];
 }
 static int Mini_AigNodeFanin1( Mini_Aig_t * p, int Id )
 {
     assert( Id >= 0 && 2*Id < p->nSize );
+    assert( p->pArray[2*Id+1] == 0x7FFFFFFF || p->pArray[2*Id+1] < 2*Id );
     return p->pArray[2*Id+1];
 }
 
@@ -145,19 +147,30 @@ static void Mini_AigStop( Mini_Aig_t * p )
     MINI_AIG_FREE( p->pArray );
     MINI_AIG_FREE( p );
 }
-static void Mini_AigPrintStats( Mini_Aig_t * p )
+static int Mini_AigPiNum( Mini_Aig_t * p )
 {
-    int i, nPis, nPos, nNodes;
-    nPis = 0;
+    int i, nPis = 0;
     Mini_AigForEachPi( p, i )
         nPis++;
-    nPos = 0;
+    return nPis;
+}
+static int Mini_AigPoNum( Mini_Aig_t * p )
+{
+    int i, nPos = 0;
     Mini_AigForEachPo( p, i )
         nPos++;
-    nNodes = 0;
+    return nPos;
+}
+static int Mini_AigAndNum( Mini_Aig_t * p )
+{
+    int i, nNodes = 0;
     Mini_AigForEachAnd( p, i )
         nNodes++;
-    printf( "PI = %d. PO = %d. Node = %d.\n", nPis, nPos, nNodes );
+    return nNodes;
+}
+static void Mini_AigPrintStats( Mini_Aig_t * p )
+{
+    printf( "PI = %d. PO = %d. Node = %d.\n", Mini_AigPiNum(p), Mini_AigPoNum(p), Mini_AigAndNum(p) );
 }
 
 // serialization
@@ -265,7 +278,59 @@ static int Mini_AigCheck( Mini_Aig_t * p )
     return status;
 }
 
-
+// procedure to dump MiniAIG into a Verilog file
+static void Mini_AigDumpVerilog( char * pFileName, char * pModuleName, Mini_Aig_t * p )
+{
+    int i, k, iFaninLit0, iFaninLit1, Length = strlen(pModuleName), nPos = Mini_AigPoNum(p); 
+    Vec_Bit_t * vObjIsPi = Vec_BitStart( Mini_AigNodeNum(p) );
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL ) { printf( "Cannot open output file %s\n", pFileName ); return; }
+    // write interface
+    fprintf( pFile, "// This MiniAIG dump was produced by ABC on %s\n\n", Extra_TimeStamp() );
+    fprintf( pFile, "module %s (\n", pModuleName );
+    if ( Mini_AigPiNum(p) > 0 )
+    {
+        fprintf( pFile, "%*sinput wire", Length+10, "" );
+        k = 0;
+        Mini_AigForEachPi( p, i )
+        {
+            if ( k++ % 12 == 0 ) fprintf( pFile, "\n%*s", Length+10, "" );
+            fprintf( pFile, "i%d, ", i );
+            Vec_BitWriteEntry( vObjIsPi, i, 1 );
+        }
+    }
+    fprintf( pFile, "\n%*soutput wire", Length+10, "" );
+    k = 0;
+    Mini_AigForEachPo( p, i )
+    {
+        if ( k++ % 12 == 0 ) fprintf( pFile, "\n%*s", Length+10, "" );
+        fprintf( pFile, "o%d%s", i, k==nPos ? "":", " );
+    }
+    fprintf( pFile, "\n%*s);\n\n", Length+8, "" );
+    // write LUTs
+    Mini_AigForEachAnd( p, i )
+    {
+        iFaninLit0 = Mini_AigNodeFanin0( p, i );
+        iFaninLit1 = Mini_AigNodeFanin1( p, i );
+        fprintf( pFile, "  assign n%d = ", i );
+        fprintf( pFile, "%s%c%d", (iFaninLit0 & 1) ? "~":"", Vec_BitEntry(vObjIsPi, iFaninLit0 >> 1) ? 'i':'n', iFaninLit0 >> 1 );
+        fprintf( pFile, " & " );
+        fprintf( pFile, "%s%c%d", (iFaninLit1 & 1) ? "~":"", Vec_BitEntry(vObjIsPi, iFaninLit1 >> 1) ? 'i':'n', iFaninLit1 >> 1  );
+        fprintf( pFile, ";\n" );
+    }
+    // write assigns
+    fprintf( pFile, "\n" );
+    Mini_AigForEachPo( p, i )
+    {
+        iFaninLit0 = Mini_AigNodeFanin0( p, i );
+        fprintf( pFile, "  assign o%d = ", i );
+        fprintf( pFile, "%s%c%d", (iFaninLit0 & 1) ? "~":"", Vec_BitEntry(vObjIsPi, iFaninLit0 >> 1) ? 'i':'n', iFaninLit0 >> 1 );
+        fprintf( pFile, ";\n" );
+    }
+    fprintf( pFile, "\nendmodule // %s \n\n\n", pModuleName );
+    Vec_BitFree( vObjIsPi );
+    fclose( pFile );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 6bbc061d..20751d3b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -12657,7 +12657,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        Cba_PrsReadBlifTest();
     }
 //    Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) );
-    Maj_ManExactSynthesisTest();
+//    Maj_ManExactSynthesisTest();
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
diff --git a/src/base/main/abcapis.h b/src/base/main/abcapis.h
index 8c188b67..34001bc7 100644
--- a/src/base/main/abcapis.h
+++ b/src/base/main/abcapis.h
@@ -90,6 +90,7 @@ extern ABC_DLL void   Abc_NtkSetAndGateDelay( Abc_Frame_t * pAbc, float Delay );
 // procedures to return the mapped network
 extern ABC_DLL int *  Abc_NtkOutputMiniMapping( Abc_Frame_t * pAbc );
 extern ABC_DLL void   Abc_NtkPrintMiniMapping( int * pArray );
+extern ABC_DLL int *  Abc_FrameReadArrayMapping( Abc_Frame_t * pAbc );              
 
 // procedures to access verifization status and a counter-example
 extern ABC_DLL int    Abc_FrameReadProbStatus( Abc_Frame_t * pAbc );   
diff --git a/src/base/main/main.h b/src/base/main/main.h
index a59a9a40..3887d764 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -160,6 +160,8 @@ extern ABC_DLL float           Abc_FrameReadMaxLoad();
 extern ABC_DLL void            Abc_FrameSetDrivingCell( char * pName );
 extern ABC_DLL void            Abc_FrameSetMaxLoad( float Load );
 
+extern ABC_DLL void            Abc_FrameSetArrayMapping( int * p );
+
 ABC_NAMESPACE_HEADER_END
 
 #endif
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 96373ad9..e496d8ee 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -106,7 +106,10 @@ void        Abc_FrameSetBridgeMode()                         { if ( s_GlobalFram
 char *      Abc_FrameReadDrivingCell()                       { return s_GlobalFrame->pDrivingCell;    }              
 float       Abc_FrameReadMaxLoad()                           { return s_GlobalFrame->MaxLoad;         }      
 void        Abc_FrameSetDrivingCell( char * pName )          { ABC_FREE(s_GlobalFrame->pDrivingCell); s_GlobalFrame->pDrivingCell   = pName; }      
-void        Abc_FrameSetMaxLoad( float Load )                { s_GlobalFrame->MaxLoad        = Load;  }      
+void        Abc_FrameSetMaxLoad( float Load )                { s_GlobalFrame->MaxLoad = Load;         }      
+
+int *       Abc_FrameReadArrayMapping( Abc_Frame_t * pAbc )  { return pAbc->pArray;                                            }
+void        Abc_FrameSetArrayMapping( int * p )              { ABC_FREE( s_GlobalFrame->pArray ); s_GlobalFrame->pArray = p;   }      
 
 /**Function*************************************************************
 
@@ -232,6 +235,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     Gia_ManStopP( &p->pGiaMiniLut );
     Vec_IntFreeP( &p->vCopyMiniAig );
     Vec_IntFreeP( &p->vCopyMiniLut );
+    ABC_FREE( p->pArray );
 
     ABC_FREE( p );
     s_GlobalFrame = NULL;
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 5f330e4a..66432c78 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -148,6 +148,7 @@ struct Abc_Frame_t_
     Gia_Man_t *     pGiaMiniLut; 
     Vec_Int_t *     vCopyMiniAig;
     Vec_Int_t *     vCopyMiniLut;
+    int *           pArray;
 
     Abc_Frame_Callback_BmcFrameDone_Func pFuncOnFrameDone;
 };
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 7cc852af..d7b0de54 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -270,6 +270,8 @@ struct If_Man_t_
     int                pArrTimeProfile[IF_MAX_FUNC_LUTSIZE];
     Vec_Ptr_t *        vVisited;
     void *             pUserMan;
+    Vec_Int_t *        vDump;
+    int                pDumpIns[16];
 
     // timing manager
     Tim_Man_t *        pManTim;
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 414a1911..27d7245e 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -260,6 +260,7 @@ void If_ManStop( If_Man_t * p )
     Vec_PtrFreeP( &p->vObjsRev );
     Vec_PtrFreeP( &p->vLatchOrder );
     Vec_IntFreeP( &p->vLags );
+    Vec_IntFreeP( &p->vDump );
     for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
         Vec_IntFreeP( &p->vTtDsds[i] );
     for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )