Version abc70926

4 files changed, 167 insertions, 7 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index 20caeb57..ca4cab95 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -34,6 +34,7 @@ static int IoCommandReadBench   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadDsd     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEdif    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEqn     ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadInit    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadPla     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadTruth   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -86,6 +87,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_dsd",      IoCommandReadDsd,      1 );
 //    Cmd_CommandAdd( pAbc, "I/O", "read_edif",     IoCommandReadEdif,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_eqn",      IoCommandReadEqn,      1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_init",     IoCommandReadInit,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_pla",      IoCommandReadPla,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_truth",    IoCommandReadTruth,    1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_verilog",  IoCommandReadVerilog,  1 );
@@ -654,6 +656,65 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    char * pFileName;
+    int c;
+    extern void Io_ReadBenchInit( Abc_Ntk_t * pNtk, char * pFileName );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    // get the input file name
+    pFileName = argv[globalUtilOptind];
+    // read the file using the corresponding file reader
+    pNtk = Abc_NtkDup( pNtk );
+    Io_ReadBenchInit( pNtk, pFileName );
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_init [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         reads initial state of the network in BENCH format\n" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk;
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index be80dc82..d3c4c878 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -245,6 +245,21 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
 //        printf( "Io_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
         Abc_NtkShortNames( pNtkNew );
     }
+
+    // read the name of the model if given
+    if ( *pCur == 'c' )
+    {
+        if ( !strncmp( pCur + 2, ".model", 6 ) )
+        {
+            char * pTemp;
+            for ( pTemp = pCur + 9; *pTemp && *pTemp != '\n'; pTemp++ );
+            *pTemp = 0;
+            free( pNtkNew->pName );
+            pNtkNew->pName = Extra_UtilStrsav( pCur + 9 );
+        }
+    }
+
+
     // skipping the comments
     free( pContents );
     Vec_PtrFree( vNodes );
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index ba622e40..007147bc 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -66,6 +66,7 @@ Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck )
     }
     return pNtk;
 }
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -82,7 +83,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
     ProgressBar * pProgress;
     Vec_Ptr_t * vTokens;
     Abc_Ntk_t * pNtk;
-    Abc_Obj_t * pNode;
+    Abc_Obj_t * pNode, * pNet;
     Vec_Str_t * vString;
     unsigned uTruth[8];
     char * pType, ** ppNames, * pString;
@@ -241,11 +242,34 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
     Extra_ProgressBarStop( pProgress );
     Vec_StrFree( vString );
 
-    // check if constant have been added
-//    if ( pNet = Abc_NtkFindNet( pNtk, "vdd" ) )
-//        Io_ReadCreateConst( pNtk, "vdd", 1 );
-//    if ( pNet = Abc_NtkFindNet( pNtk, "gnd" ) )
-//        Io_ReadCreateConst( pNtk, "gnd", 0 );
+    // check if constant 0 is present
+    if ( (pNet = Abc_NtkFindNet( pNtk, "gnd" )) )
+    {
+        if ( Abc_ObjFaninNum(pNet) == 0 )
+            Io_ReadCreateConst( pNtk, "gnd", 0 );
+    }
+    if ( (pNet = Abc_NtkFindNet( pNtk, "1" )) )
+    {
+        if ( Abc_ObjFaninNum(pNet) == 0 )
+        {
+            printf( "Io_ReadBenchNetwork(): Adding constant 0 fanin to non-driven net \"1\".\n" );
+            Io_ReadCreateConst( pNtk, "1", 0 );
+        }
+    }
+    // check if constant 1 is present
+    if ( (pNet = Abc_NtkFindNet( pNtk, "vdd" )) )
+    {
+        if ( Abc_ObjFaninNum(pNet) == 0 )
+            Io_ReadCreateConst( pNtk, "vdd", 1 );
+    }
+    if ( (pNet = Abc_NtkFindNet( pNtk, "2" )) )
+    {
+        if ( Abc_ObjFaninNum(pNet) == 0 )
+        {
+            printf( "Io_ReadBenchNetwork(): Adding constant 1 fanin to non-driven net \"2\".\n" );
+            Io_ReadCreateConst( pNtk, "2", 1 );
+        }
+    }
 
     Abc_NtkFinalizeRead( pNtk );
 
@@ -269,6 +293,65 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Reads initial state in BENCH format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_ReadBenchInit( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    char pBuffer[1000];
+    FILE * pFile;
+    char * pToken;
+    Abc_Obj_t * pObj;
+    int Num;
+    pFile = fopen( pFileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Io_ReadBenchInit(): Failed to open file \"%s\".\n", pFileName );
+        return;
+    }
+    while ( fgets( pBuffer, 999, pFile ) )
+    {
+        pToken = strtok( pBuffer, " \n\t\r" );
+        // find the latch output
+        Num = Nm_ManFindIdByName( pNtk->pManName, pToken, ABC_OBJ_BO );
+        if ( Num < 0 )
+        {
+            printf( "Io_ReadBenchInit(): Cannot find register with output %s.\n", pToken );
+            continue;
+        }
+        pObj = Abc_ObjFanin0( Abc_NtkObj( pNtk, Num ) );
+        if ( !Abc_ObjIsLatch(pObj) )
+        {
+            printf( "Io_ReadBenchInit(): The signal is not a register output %s.\n", pToken );
+            continue;
+        }
+        // assign the new init state
+        pToken = strtok( NULL, " \n\t\r" );
+        if ( pToken[0] == '0' )
+            Abc_LatchSetInit0( pObj );
+        else if ( pToken[0] == '1' )
+            Abc_LatchSetInit1( pObj );
+        else if ( pToken[0] == '2' )
+            Abc_LatchSetInitDc( pObj );
+        else
+        {
+            printf( "Io_ReadBenchInit(): The signal %s has unknown initial value (%s).\n", 
+                Abc_ObjName(Abc_ObjFanout0(pObj)), pToken );
+            continue;
+        }
+    }
+    fclose( pFile );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index e805fbc2..ff34b177 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -248,7 +248,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
 
     // write the comment
     fprintf( pFile, "c\n" );
-    fprintf( pFile, "%s\n", pNtk->pName );
+    if ( pNtk->pName && strlen(pNtk->pName) > 0 )
+        fprintf( pFile, ".model %s\n", pNtk->pName );
     fprintf( pFile, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
     fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
     fclose( pFile );