Various changes.

3 files changed, 278 insertions, 7 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4e986360..d4155ca6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -770,6 +770,11 @@ void Abc_FrameUpdateGia( Abc_Frame_t * pAbc, Gia_Man_t * pNew )
         pNew->vNamesOut = pAbc->pGia->vNamesOut;
         pAbc->pGia->vNamesOut = NULL;
     }
+    if (!pNew->vNamesNode && pAbc->pGia && pAbc->pGia->vNamesNode && Gia_ManObjNum(pNew) == Vec_PtrSize(pAbc->pGia->vNamesNode))
+    {
+        pNew->vNamesNode = pAbc->pGia->vNamesNode;
+        pAbc->pGia->vNamesNode = NULL;
+    }
     // update
     if ( pAbc->pGia2 )
         Gia_ManStop( pAbc->pGia2 );
@@ -30088,6 +30093,7 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Abc3_ReadShowHie( char * pFileName, int fFlat );
     extern Gia_Man_t * Gia_MiniAigSuperDerive( char * pFileName, int fVerbose );
+    extern Gia_Man_t * Gia_FileSimpleRead( char * pFileName, int fNames, char * pFileW );
     Gia_Man_t * pAig = NULL;
     FILE * pFile;
     char ** pArgvNew;
@@ -30099,8 +30105,9 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose = 0;
     int fGiaSimple = 0;
     int fSkipStrash = 0;
+    int fNewReader = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "csmnlvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "csmnlpvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -30119,6 +30126,9 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'l':
             fMiniLut ^= 1;
             break;
+        case 'p':
+            fNewReader ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -30150,7 +30160,9 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     fclose( pFile );
 
-    if ( fMiniAig )
+    if ( fNewReader )
+        pAig = Gia_FileSimpleRead( FileName, fGiaSimple, NULL );
+    else if ( fMiniAig )
         pAig = Gia_ManReadMiniAig( FileName );
     else if ( fMiniAig2 )
         pAig = Gia_MiniAigSuperDerive( FileName, fVerbose );
@@ -30702,6 +30714,8 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
         }
     }
+    if ( pAbc->pGia->vNamesNode )
+        Abc_Print( 0, "Internal nodes names are not transferred.\n" );
 
     // decouple CI/CO with the same name
     if ( pAbc->pGia->vNamesIn || pAbc->pGia->vNamesOut )
diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c
index a8cae33d..5105f463 100644
--- a/src/base/acb/acbFunc.c
+++ b/src/base/acb/acbFunc.c
@@ -210,17 +210,78 @@ Vec_Int_t * Acb_VerilogSimpleLex( char * pFileName, Abc_Nam_t * pNames )
     Vec_Int_t * vBuffer = Vec_IntAlloc( 1000 );
     char * pBuffer = Extra_FileReadContents( pFileName );
     char * pToken, * pStart, * pLimit = pBuffer + strlen(pBuffer);
+    int i, iToken, RLeft = -1, RRight = -1;
     if ( pBuffer == NULL )
         return NULL;
     Acb_VerilogRemoveComments( pBuffer );
     pToken = strtok( pBuffer, "  \n\r\t(),;=" );
     while ( pToken )
     {
-        int iToken = Abc_NamStrFindOrAdd( pNames, pToken, NULL );
+        if ( 0 )
+        {
+            if ( !strcmp(pToken, "assign") )
+            {
+                int fBuffer = 0;
+                int nToks = 0, pToks[4];
+                while ( 1 )
+                {
+                    pToken = strtok( NULL, "  \n\r\t(),=~&" );
+                    if ( pToken[0] == ';' )
+                        break;
+                    if ( pToken[strlen(pToken)-1] == ';' )
+                    {
+                        pToken[strlen(pToken)-1] = 0;
+                        assert( nToks < 3 );
+                        pToks[nToks++] = Abc_NamStrFindOrAdd( pNames, pToken, NULL );
+                        fBuffer = 1;
+                        break;
+                    }
+                    else
+                    {
+                        assert( nToks < 3 );
+                        pToks[nToks++] = Abc_NamStrFindOrAdd( pNames, pToken, NULL );
+                    }
+                }
+                assert( nToks == 2 || nToks == 3 );
+                Vec_IntPush( vBuffer, fBuffer ? ACB_AND : ACB_NAND );
+                Vec_IntPush( vBuffer, pToks[0] );
+                Vec_IntPush( vBuffer, pToks[1] );
+                Vec_IntPush( vBuffer, nToks == 3 ? pToks[2] : pToks[1] );
+                pToken = strtok( NULL, "  \n\r\t(),;=" );
+                continue;
+            }
+        }
+
+        if ( pToken[0] == '[' )
+        {
+            assert( RLeft == -1 );
+            RLeft  = atoi(pToken+1);
+            RRight = atoi(strstr(pToken,":")+1);
+            pToken = strtok( NULL, "  \n\r\t(),;=" );
+            continue;
+        }
+        if ( pToken[0] == '\\' )
+            pToken++;
         if ( !strcmp(pToken, "assign") )
-            Vec_IntPush( vBuffer, ACB_BUF );
+            iToken = ACB_BUF;
         else
-            Vec_IntPush( vBuffer, iToken );
+            iToken = Abc_NamStrFindOrAdd( pNames, pToken, NULL );
+        if ( iToken < ACB_UNUSED )
+            RLeft = RRight = -1;
+        else if ( RLeft != -1 )
+        {
+            char Buffer[1000];
+            assert( strlen(pToken) < 990 );
+            for ( i = RRight; i <= RLeft; i++ )
+            {
+                sprintf( Buffer, "%s[%d]", pToken, i );
+                iToken = Abc_NamStrFindOrAdd( pNames, Buffer, NULL );
+                Vec_IntPush( vBuffer, iToken );
+            }
+            pToken = strtok( NULL, "  \n\r\t(),;=" );
+            continue;
+        }
+        Vec_IntPush( vBuffer, iToken );
         if ( iToken >= ACB_BUF && iToken < ACB_UNUSED )
         {
             for ( pStart = pToken; pStart < pLimit && *pStart != '\n'; pStart++ )
@@ -328,6 +389,178 @@ void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_FileSimpleParse_rec( Gia_Man_t * pNew, int Token, Vec_Int_t * vMapType, Vec_Int_t * vTypes, Vec_Int_t * vFanins, Vec_Int_t * vMap )
+{
+    int nFanins, * pFanins, pLits[16];
+    int i, Type, Size, Place = Vec_IntEntry( vMapType, Token ); 
+    int iLit = Vec_IntEntry( vMap, Token );
+    if ( iLit >= 0 )
+        return iLit;
+    Place = Vec_IntEntry( vMapType, Token );
+    assert( Place >= 0 );
+    Type = Vec_IntEntry( vTypes, Place );
+    Size = Vec_IntEntry( vTypes, Place+1 );
+    nFanins = Vec_IntEntry(vTypes, Place+3) - Size - 1;
+    pFanins = Vec_IntEntryP(vFanins, Size+1);
+    assert( nFanins > 0 && nFanins < 16 );
+    for ( i = 0; i < nFanins; i++ )
+        Gia_FileSimpleParse_rec( pNew, pFanins[i], vMapType, vTypes, vFanins, vMap );
+    for ( i = 0; i < nFanins; i++ )
+        pLits[i] = Vec_IntEntry( vMap, pFanins[i] );
+    if ( nFanins == 1 )
+    {
+        assert( Type == ACB_BUF || Type == ACB_NOT );
+        iLit = Abc_LitNotCond( pLits[0], Type == ACB_NOT );
+        iLit = Gia_ManAppendAnd2( pNew, iLit, iLit );
+    }
+    else
+    {
+        iLit = pLits[0];
+        if ( Type == ACB_AND || Type == ACB_NAND )
+            for ( i = 1; i < nFanins; i++ )
+                iLit = Gia_ManAppendAnd2( pNew, iLit, pLits[i] );
+        else if ( Type == ACB_OR || Type == ACB_NOR )
+            for ( i = 1; i < nFanins; i++ )
+                iLit = Gia_ManAppendOr2( pNew, iLit, pLits[i] );
+        else if ( Type == ACB_XOR || Type == ACB_XNOR )
+            for ( i = 1; i < nFanins; i++ )
+                iLit = Gia_ManAppendXor2( pNew, iLit, pLits[i] );
+        else assert( 0 );
+        iLit = Abc_LitNotCond( iLit, (Type == ACB_NAND || Type == ACB_NOR || Type == ACB_XNOR) );
+    }
+    Vec_IntWriteEntry( vMap, Token, iLit );
+    return iLit;
+}
+Gia_Man_t * Gia_FileSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames, int fNames, char * pFileW )
+{
+    Gia_Man_t * pNew     = NULL;
+    Vec_Int_t * vInputs  = Vec_IntAlloc(100);
+    Vec_Int_t * vOutputs = Vec_IntAlloc(100);
+    Vec_Int_t * vWires   = Vec_IntAlloc(100);
+    Vec_Int_t * vTypes   = Vec_IntAlloc(100);
+    Vec_Int_t * vFanins  = Vec_IntAlloc(100);
+    Vec_Int_t * vCur     = NULL;  
+    Vec_Int_t * vMap     = Vec_IntStartFull( Abc_NamObjNumMax(pNames) );
+    Vec_Int_t * vMapType = Vec_IntStartFull( Abc_NamObjNumMax(pNames) );
+    int i, iLit, Token, Size;
+    char Buffer[1000];
+    assert( Vec_IntEntry(vBuffer, 0) == ACB_MODULE );
+    Vec_IntForEachEntryStart( vBuffer, Token, i, 2 )
+    {
+        if ( vCur == NULL && Token >= ACB_UNUSED )
+            continue;
+        if ( Token == ACB_ENDMODULE )
+            break;
+        if ( Token == ACB_INPUT )
+            vCur = vInputs;
+        else if ( Token == ACB_OUTPUT )
+            vCur = vOutputs;
+        else if ( Token == ACB_WIRE )
+            vCur = vWires;
+        else if ( Token >= ACB_BUF && Token < ACB_UNUSED )
+        {
+            Vec_IntPush( vTypes, Token );
+            Vec_IntPush( vTypes, Vec_IntSize(vFanins) );
+            vCur = vFanins;
+        }
+        else 
+            Vec_IntPush( vCur, Token );
+    }
+    Vec_IntPush( vTypes, -1 );
+    Vec_IntPush( vTypes, Vec_IntSize(vFanins) );
+    // map types
+    Vec_IntForEachEntryDouble( vTypes, Token, Size, i ) 
+        if ( Token > 0 )
+            Vec_IntWriteEntry( vMapType, Vec_IntEntry(vFanins, Size), i );
+    // create design
+    pNew = Gia_ManStart( 10000 );
+    pNew->pName = Abc_UtilStrsav( Abc_NamStr(pNames, Vec_IntEntry(vBuffer, 1)) );
+    pNew->fGiaSimple = 1;
+    if ( (Token = Abc_NamStrFind(pNames, "1\'b0")) )
+        Vec_IntWriteEntry( vMap, Token, 0 );
+    if ( (Token = Abc_NamStrFind(pNames, "1\'b1")) )
+        Vec_IntWriteEntry( vMap, Token, 1 );
+    if ( (Token = Abc_NamStrFind(pNames, "1\'bx")) )
+        Vec_IntWriteEntry( vMap, Token, 0 );
+    if ( (Token = Abc_NamStrFind(pNames, "1\'bz")) )
+        Vec_IntWriteEntry( vMap, Token, 0 );
+    Vec_IntForEachEntry( vInputs, Token, i )
+        Gia_ManAppendCi(pNew);
+    Vec_IntForEachEntry( vInputs, Token, i )
+        Vec_IntWriteEntry( vMap, Token, Gia_ManAppendAnd2(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, i)) );
+    Vec_IntForEachEntry( vOutputs, Token, i )
+        Gia_FileSimpleParse_rec( pNew, Token, vMapType, vTypes, vFanins, vMap );
+    Vec_IntForEachEntry( vOutputs, Token, i )
+        Gia_ManAppendCo( pNew, Vec_IntEntry(vMap, Token) );
+    // create names
+    if ( fNames ) 
+    {
+        pNew->vNamesNode = Vec_PtrStart( Gia_ManObjNum(pNew) );
+        Vec_IntForEachEntry( vMap, iLit, Token )
+        {
+            if ( iLit == -1 || !Gia_ObjIsAnd(Gia_ManObj(pNew, Abc_Lit2Var(iLit))) )
+                continue;
+            sprintf( Buffer, "%c_%s", Abc_LitIsCompl(iLit) ? 'c' : 'd', Abc_NamStr(pNames, Token) );
+            assert( Vec_PtrEntry(pNew->vNamesNode, Abc_Lit2Var(iLit)) == NULL );
+            Vec_PtrWriteEntry( pNew->vNamesNode, Abc_Lit2Var(iLit), Abc_UtilStrsav(Buffer) );
+        }
+    }
+    else
+    {
+        Gia_Man_t * pTemp;
+        pNew = Gia_ManDupDfsRehash( pTemp = pNew );
+        Gia_ManStop( pTemp );
+    }
+    pNew->vNamesIn  = Vec_PtrAlloc( Vec_IntSize(vInputs) );
+    Vec_IntForEachEntry( vInputs, Token, i )
+        Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Abc_NamStr(pNames, Token)) );
+    pNew->vNamesOut = Vec_PtrAlloc( Vec_IntSize(vOutputs) );
+    Vec_IntForEachEntry( vOutputs, Token, i )
+        Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Abc_NamStr(pNames, Token)) );
+    if ( pFileW )
+    {
+        extern Vec_Int_t * Acb_ReadWeightMap( char * pFileName, Abc_Nam_t * pNames );
+        Vec_Int_t * vT2W = Acb_ReadWeightMap( pFileW, pNames );
+        assert( pNew->vWeights == NULL );
+        pNew->vWeights = Vec_IntStartFull( Gia_ManObjNum(pNew) );
+        Vec_IntForEachEntry( vMap, iLit, Token )
+            if ( iLit != -1 && Vec_IntEntry(vT2W, Token) != -1 )
+                Vec_IntWriteEntry( pNew->vWeights, Abc_Lit2Var(iLit), Vec_IntEntry(vT2W, Token) );
+        Vec_IntFree( vT2W );
+    }
+    // cleanup
+    Vec_IntFree( vInputs );
+    Vec_IntFree( vOutputs );
+    Vec_IntFree( vWires );
+    Vec_IntFree( vTypes );
+    Vec_IntFree( vFanins );
+    Vec_IntFree( vMap );
+    Vec_IntFree( vMapType );
+    return pNew;
+}
+Gia_Man_t * Gia_FileSimpleRead( char * pFileName, int fNames, char * pFileW )
+{
+    Abc_Nam_t * pNames = Acb_VerilogStartNames();
+    Vec_Int_t * vBuffer = Acb_VerilogSimpleLex( pFileName, pNames );
+    Gia_Man_t * pNew = vBuffer ? Gia_FileSimpleParse( vBuffer, pNames, fNames, pFileW ) : NULL;
+    assert( pNew->pSpec == NULL );
+    pNew->pSpec = Abc_UtilStrsav( pFileName );
+    Abc_NamDeref( pNames );
+    Vec_IntFree( vBuffer );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Read weights of nodes from the weight file.]
 
   Description []
@@ -374,10 +607,18 @@ Vec_Int_t * Acb_ReadWeightMap( char * pFileName, Abc_Nam_t * pNames )
   SeeAlso     []
 
 ***********************************************************************/
+char ** Acb_PrepareNames( Abc_Nam_t * p )
+{
+    char ** ppRes = ABC_CALLOC( char *, Abc_NamObjNumMax(p) );
+    int i;
+    for ( i = 0; i < Abc_NamObjNumMax(p); i++ )
+        ppRes[i] = Abc_NamStr( p, i );
+    return ppRes;
+}
 Acb_Ntk_t * Acb_VerilogSimpleRead( char * pFileName, char * pFileNameW )
 {
     extern Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames, Vec_Int_t * vWeights, int nNameIdMax );
-    Acb_Ntk_t * pNtk;
+    Acb_Ntk_t * pNtk; //char ** ppNames;
     Abc_Nam_t * pNames = Acb_VerilogStartNames();
     Vec_Int_t * vBuffer = Acb_VerilogSimpleLex( pFileName, pNames );
     void * pModule = vBuffer ? Acb_VerilogSimpleParse( vBuffer, pNames ) : NULL;
@@ -392,7 +633,9 @@ Acb_Ntk_t * Acb_VerilogSimpleRead( char * pFileName, char * pFileNameW )
         printf( "Cannot read weight file \"%s\".\n", pFileNameW );
         return NULL;
     }
-//    Ndr_ModuleWriteVerilog( "iccad17/unit1/test.v", pModule, pNameStrs );
+    //ppNames = Acb_PrepareNames(pNames);
+    //Ndr_WriteVerilog( Extra_FileNameGenericAppend(pFileName, "_ndr.v"), pModule, ppNames, 1 );
+    //ABC_FREE( ppNames );
     pNtk = Acb_NtkFromNdr( pFileName, pModule, pNames, vWeights, Abc_NamObjNumMax(pNames) );
     Ndr_Delete( pModule );
     Vec_IntFree( vBuffer );
@@ -400,6 +643,11 @@ Acb_Ntk_t * Acb_VerilogSimpleRead( char * pFileName, char * pFileNameW )
     Abc_NamDeref( pNames );
     return pNtk;
 }
+void Acb_VerilogSimpleReadTest( char * pFileName )
+{
+    Acb_Ntk_t * p = Acb_VerilogSimpleRead( pFileName, NULL );
+    Acb_NtkFree( p );
+}
 
 /**Function*************************************************************
 
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index f87d971f..9cf41413 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -480,6 +480,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     if ( pCur < pContents + nFileSize && *pCur != 'c' )
     {
         int Counter = 0;
+        int fNodeNames = 0;
         while ( pCur < pContents + nFileSize && *pCur != 'c' )
         {
             // get the terminal type
@@ -490,6 +491,12 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
                 vTerms = pNtkNew->vBoxes;
             else if ( *pCur == 'o' || *pCur == 'b' || *pCur == 'c' || *pCur == 'j' || *pCur == 'f' )
                 vTerms = pNtkNew->vPos;
+            else if ( *pCur == 'n' )
+            {
+                fNodeNames++;
+                while ( *pCur++ != '\n' );
+                continue;
+            }
             else
             {
 //                fprintf( stdout, "Wrong terminal type.\n" );
@@ -543,6 +550,8 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
         }
 //        if ( Counter )
 //            printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
+        if ( fNodeNames )
+            printf( "Io_ReadAiger(): The names of internal nodes are not supported. Ignoring %d node names.\n", fNodeNames );
     }
     else
     {