Adding switch &w -p to dump AIG in a Verilog file.

1 files changed, 185 insertions, 0 deletions

diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 98907491..53b686a4 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -22,6 +22,7 @@
 #include "misc/tim/tim.h"
 #include "proof/abs/abs.h"
 #include "opt/dar/dar.h"
+#include "misc/extra/extra.h"
 
 #ifdef WIN32
 #include <windows.h>
@@ -1121,6 +1122,190 @@ void Gia_ManDfsSlacksPrint( Gia_Man_t * p )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Compute arrival/required times.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Bit_t * Gia_ManGenUsed( Gia_Man_t * p, int fBuf )
+{
+    Gia_Obj_t * pObj; int i;
+    Vec_Bit_t * vUsed = Vec_BitStart( Gia_ManObjNum(p) );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( fBuf )
+            Vec_BitWriteEntry( vUsed, i, 1 );
+        if ( Gia_ObjFaninC0(pObj) ^ fBuf )
+            Vec_BitWriteEntry( vUsed, Gia_ObjFaninId0(pObj, i), 1 );
+        if ( Gia_ObjFaninC1(pObj) ^ fBuf )
+            Vec_BitWriteEntry( vUsed, Gia_ObjFaninId1(pObj, i), 1 );
+    }
+    Gia_ManForEachCo( p, pObj, i )
+        if ( Gia_ObjFaninC0(pObj) ^ fBuf )
+            Vec_BitWriteEntry( vUsed, Gia_ObjFaninId0p(p, pObj), 1 );
+    Vec_BitWriteEntry( vUsed, 0, 0 ); // clean zero
+    return vUsed;
+}
+int Gia_ManNameIsLegalInVerilog( char * pName )
+{
+    // identifier ::= simple_identifier | escaped_identifier
+    // simple_identifier ::= [a-zA-Z_][a-zA-Z0-9_$]
+    // escaped_identifier ::= \ {Any_ASCII_character_except_white_space} white_space
+    // white_space ::= space | tab | newline
+    assert( pName != NULL && *pName != '\0' );
+    if ( *pName == '\\' )
+        return 1;
+    if ( (*pName < 'a' || *pName > 'z') && (*pName < 'A' || *pName > 'Z') && *pName != '_' )
+        return 0;
+    while ( *(++pName) )
+        if ( (*pName < 'a' || *pName > 'z') && (*pName < 'A' || *pName > 'Z') && (*pName < '0' || *pName > '9') && *pName != '_' && *pName != '$' ) 
+            return 0;
+    return 1;
+}
+char * Gia_ObjGetDumpName( Vec_Ptr_t * vNames, char c, int i, int d )
+{
+    static char pBuffer[10000];
+    if ( vNames )
+    {
+        char * pName = (char *)Vec_PtrEntry(vNames, i);
+        if ( Gia_ManNameIsLegalInVerilog(pName) )
+            sprintf( pBuffer, "%s", pName );
+        else
+            sprintf( pBuffer, "\\%s ", pName );
+    }
+    else
+        sprintf( pBuffer, "%c%0*d%c", c, d, i, c );
+    return pBuffer;
+}
+void Gia_ManWriteNames( FILE * pFile, char c, int n, Vec_Ptr_t * vNames, int Start, int Skip, Vec_Bit_t * vObjs )
+{
+    int Digits = Abc_Base10Log( n );
+    int Length = Start, i, fFirst = 1; 
+    char * pName;
+    for ( i = 0; i < n; i++ )
+    {
+        if ( vObjs && !Vec_BitEntry(vObjs, i) )
+            continue;
+        pName = Gia_ObjGetDumpName( vNames, c, i, Digits );
+        Length += strlen(pName) + 2;
+        if ( Length > 60 )
+        {
+            fprintf( pFile, ",\n    " );
+            Length = Skip;
+            fFirst = 1;
+        }
+        fprintf( pFile, "%s%s", fFirst ? "":", ", pName );
+        fFirst = 0;
+    }
+}
+void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName )
+{
+    FILE * pFile;
+    Gia_Obj_t * pObj;
+    Vec_Bit_t * vInvs, * vUsed;
+    int i, nDigits, nDigits2;
+    if ( Gia_ManRegNum(p) )
+    {
+        printf( "Currently cannot write sequential AIG.\n" );
+        return;
+    }
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open output file \"%s\".\n", pFileName );
+        return;
+    }
+
+    vInvs = Gia_ManGenUsed( p, 0 );
+    vUsed = Gia_ManGenUsed( p, 1 );
+
+    fprintf( pFile, "// This Verilog file is written by ABC on %s\n\n", Extra_TimeStamp() );
+
+    fprintf( pFile, "module %s (\n    ", p->pName );
+    Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 4, 4, NULL );
+    fprintf( pFile, ",\n    " );
+
+    Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 4, 4, NULL );
+    fprintf( pFile, "\n  );\n\n" );
+
+    fprintf( pFile, "  input " );
+    Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
+    fprintf( pFile, ";\n\n" );
+
+    fprintf( pFile, "  output " );
+    Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
+    fprintf( pFile, ";\n\n" );
+
+    if ( Vec_BitCount(vUsed) )
+    {
+        fprintf( pFile, "  wire " );
+        Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed );
+        fprintf( pFile, ";\n\n" );
+    }
+
+    if ( Vec_BitCount(vInvs) )
+    {
+        fprintf( pFile, "  wire " );
+        Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs );
+        fprintf( pFile, ";\n\n" );
+    }
+
+    // input inverters
+    nDigits = Abc_Base10Log( Gia_ManObjNum(p) );
+    nDigits2 = Abc_Base10Log( Gia_ManPiNum(p) );
+    Gia_ManForEachPi( p, pObj, i )
+    {
+        if ( Vec_BitEntry(vUsed, Gia_ObjId(p, pObj)) )
+        {
+            fprintf( pFile, "  buf( %s,", Gia_ObjGetDumpName(NULL, 'n', Gia_ObjId(p, pObj), nDigits) );
+            fprintf( pFile, " %s );\n",   Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigits2) );
+        }
+        if ( Vec_BitEntry(vInvs, Gia_ObjId(p, pObj)) )
+        {
+            fprintf( pFile, "  not( %s,", Gia_ObjGetDumpName(NULL, 'i', Gia_ObjId(p, pObj), nDigits) );
+            fprintf( pFile, " %s );\n",   Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigits2) );
+        }
+    }
+
+    // internal nodes and their inverters
+    fprintf( pFile, "\n" );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        fprintf( pFile, "  and( %s,", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) );
+        fprintf( pFile, " %s,",       Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0(pObj, i), nDigits) );
+        fprintf( pFile, " %s );\n",   Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC1(pObj)? 'i':'n'), Gia_ObjFaninId1(pObj, i), nDigits) );
+        if ( Vec_BitEntry(vInvs, i) )
+        {
+            fprintf( pFile, "  not( %s,", Gia_ObjGetDumpName(NULL, 'i', i, nDigits) );
+            fprintf( pFile, " %s );\n",   Gia_ObjGetDumpName(NULL, 'n', i, nDigits) );
+        }
+    }
+    
+    // output drivers
+    fprintf( pFile, "\n" );
+    nDigits2 = Abc_Base10Log( Gia_ManPoNum(p) );
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        fprintf( pFile, "  assign %s = ", Gia_ObjGetDumpName(p->vNamesOut, 'z', i, nDigits2) );
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+            fprintf( pFile, "1\'b%d;\n", Gia_ObjFaninC0(pObj) );
+        else 
+            fprintf( pFile, "%s;\n", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0p(p, pObj), nDigits) );
+    }
+
+    fprintf( pFile, "\nendmodule\n\n" );
+    fclose( pFile );
+
+    Vec_BitFree( vInvs );
+    Vec_BitFree( vUsed );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////