Outputting initial state in Wlc_Ntk_t.

4 files changed, 71 insertions, 20 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index ed5fe5bd..3b7c9153 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -120,7 +120,7 @@ struct Wlc_Ntk_t_
     Vec_Int_t              vCis;               // combinational inputs
     Vec_Int_t              vCos;               // combinational outputs
     Vec_Int_t              vFfs;               // flops
-    Vec_Int_t              vInits;             // initial values
+    Vec_Int_t *            vInits;             // initial values
     char *                 pInits;             // initial values
     int                    nObjs[WLC_OBJ_NUMBER]; // counter of objects of each type
     int                    nAnds[WLC_OBJ_NUMBER]; // counter of AND gates after blasting
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 7c49f73d..90287781 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -206,7 +206,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p )
     ABC_FREE( p->vCis.pArray );
     ABC_FREE( p->vCos.pArray );
     ABC_FREE( p->vFfs.pArray );
-    ABC_FREE( p->vInits.pArray );
+    Vec_IntFreeP( &p->vInits );
     ABC_FREE( p->vTravIds.pArray );
     ABC_FREE( p->vNameIds.pArray );
     ABC_FREE( p->vCopies.pArray );
@@ -471,6 +471,7 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p )
         Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
     Wlc_NtkForEachCo( p, pObj, i )
         Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
+    pNew->vInits = Vec_IntDup( p->vInits );
     pNew->pInits = Abc_UtilStrsav( p->pInits );
     Vec_IntFree( vFanins );
     return pNew;
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 1a83753a..8ed33909 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -419,7 +419,7 @@ char * Wlc_PrsConvertInitValues( Wlc_Ntk_t * p )
     int i, k, Value, * pInits;
     char * pResult;
     Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
-    Vec_IntForEachEntry( &p->vInits, Value, i )
+    Vec_IntForEachEntry( p->vInits, Value, i )
     {
         if ( Value < 0 )
         {
@@ -428,11 +428,17 @@ char * Wlc_PrsConvertInitValues( Wlc_Ntk_t * p )
             continue;
         }
         pObj = Wlc_NtkObj( p, Value );
+        Value = Wlc_ObjRange(pObj);
         while ( pObj->Type == WLC_OBJ_BUF )
             pObj = Wlc_NtkObj( p, Wlc_ObjFaninId0(pObj) );
         pInits = pObj->Type == WLC_OBJ_CONST ? Wlc_ObjConstValue(pObj) : NULL;
-        for ( k = 0; k < Wlc_ObjRange(pObj); k++ )
+        for ( k = 0; k < Abc_MinInt(Value, Wlc_ObjRange(pObj)); k++ )
             Vec_StrPush( vStr, (char)(pInits ? '0' + Abc_InfoHasBit((unsigned *)pInits, k) : 'X') );
+        // extend values with zero, in case the init value signal has different range compared to constant used
+        for ( ; k < Value; k++ )
+            Vec_StrPush( vStr, '0' );
+        // update vInits to contain either number of values or PI index
+        Vec_IntWriteEntry( p->vInits, i, pInits ? -Value : Wlc_ObjCiId(pObj) );
     }
     Vec_StrPush( vStr, '\0' );
     pResult = Vec_StrReleaseArray( vStr );
@@ -918,7 +924,7 @@ startword:
             Vec_IntFree( vTemp );
             // move FO/FI to be part of CI/CO
             assert( (Vec_IntSize(&p->pNtk->vFfs) & 1) == 0 );
-            assert( Vec_IntSize(&p->pNtk->vFfs) == 2 * Vec_IntSize(&p->pNtk->vInits) );
+            assert( Vec_IntSize(&p->pNtk->vFfs) == 2 * Vec_IntSize(p->pNtk->vInits) );
             Wlc_NtkForEachFf( p->pNtk, pObj, i )
                 if ( i & 1 )
                     Wlc_ObjSetCo( p->pNtk, pObj, 1 );
@@ -1071,7 +1077,7 @@ startword:
         }
         else if ( Wlc_PrsStrCmp( pStart, "CPL_FF" ) )
         {
-            int NameId = -1, NameIdIn = -1, NameIdOut = -1, fFound, nBits = 1, fFlopOut, fFlopIn;
+            int NameId = -1, NameIdIn = -1, NameIdOut = -1, fFound, nBits = 1, fFlopIn, fFlopOut;
             pStart += strlen("CPL_FF");
             if ( pStart[0] == '#' )
                 nBits = atoi(pStart+1);
@@ -1084,18 +1090,18 @@ startword:
                 pStart = Wlc_PrsSkipSpaces( pStart+1 );
                 if ( pStart[0] != 'd' && (pStart[0] != 'q' || pStart[1] == 'b') && strncmp(pStart, "arstval", 7) )
                     continue;
-                fFlopIn = (pStart[0] == 'q');
-                fFlopOut = (pStart[0] == 'd');
+                fFlopIn = (pStart[0] == 'd');
+                fFlopOut = (pStart[0] == 'q');
                 pStart = Wlc_PrsFindSymbol( pStart, '(' );
                 if ( pStart == NULL )
                     return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read opening paranthesis in the flop description." );
                 pStart = Wlc_PrsFindName( pStart+1, &pName );
                 if ( pStart == NULL )
                     return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read name inside flop description." );
-                if ( fFlopOut )
-                    NameIdOut = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
-                else if ( fFlopIn ) 
+                if ( fFlopIn )
                     NameIdIn = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                else if ( fFlopOut ) 
+                    NameIdOut = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
                 else
                     NameId = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
                 if ( !fFound )
@@ -1104,18 +1110,28 @@ startword:
             if ( NameIdIn == -1 || NameIdOut == -1 )
                 return Wlc_PrsWriteErrorMessage( p, pStart, "Name of flop input or flop output is missing." );
             // create flop output
-            pObj = Wlc_NtkObj( p->pNtk, NameIdIn );
+            pObj = Wlc_NtkObj( p->pNtk, NameIdOut );
             Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_FO );
-            Vec_IntPush( &p->pNtk->vFfs, NameIdIn );
+            Vec_IntPush( &p->pNtk->vFfs, NameIdOut );
             if ( nBits != Wlc_ObjRange(pObj) )
-                printf( "Warning!  Flop input has bit-width (%d) that differs from the declaration (%d)\n", nBits, Wlc_ObjRange(pObj) );
+                printf( "Warning!  Flop input has bit-width (%d) that differs from the flop declaration (%d)\n", Wlc_ObjRange(pObj), nBits );
             // create flop input
-            pObj = Wlc_NtkObj( p->pNtk, NameIdOut );
-            Vec_IntPush( &p->pNtk->vFfs, NameIdOut );
+            pObj = Wlc_NtkObj( p->pNtk, NameIdIn );
+            Vec_IntPush( &p->pNtk->vFfs, NameIdIn );
             if ( nBits != Wlc_ObjRange(pObj) )
-                printf( "Warning!  Flop output has bit-width (%d) that differs from the declaration (%d)\n", nBits, Wlc_ObjRange(pObj) );
+                printf( "Warning!  Flop output has bit-width (%d) that differs from the flop declaration (%d)\n", Wlc_ObjRange(pObj), nBits );
             // save flop init value
-            Vec_IntPush( &p->pNtk->vInits, NameId > 0 ? NameId : -Wlc_ObjRange(pObj) );
+            if ( NameId == -1 )
+                printf( "Initial value of flop \"%s\" is not specified. Zero is assumed.\n", Abc_NamStr(p->pNtk->pManName, NameIdOut) );
+            else
+            {
+                pObj = Wlc_NtkObj( p->pNtk, NameId );
+                if ( nBits != Wlc_ObjRange(pObj) )
+                    printf( "Warning!  Flop init signal bit-width (%d) is different from the flop declaration (%d)\n", Wlc_ObjRange(pObj), nBits );
+            }
+            if ( p->pNtk->vInits == NULL )
+                p->pNtk->vInits = Vec_IntAlloc( 100 );
+            Vec_IntPush( p->pNtk->vInits, NameId > 0 ? NameId : -nBits );
         }
         else if ( pStart[0] != '`' )
         {
diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c
index 4e5e6727..8352e4ac 100644
--- a/src/base/wlc/wlcWriteVer.c
+++ b/src/base/wlc/wlcWriteVer.c
@@ -339,16 +339,50 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
         fprintf( pFile, "         " );
         fprintf( pFile, "CPL_FF" );
         if ( Wlc_ObjRange(pObj) > 1 )
-            fprintf( pFile, "#%d", Wlc_ObjRange(pObj) );
+            fprintf( pFile, "#%d%*s", Wlc_ObjRange(pObj), 4 - Abc_Base10Log(Wlc_ObjRange(pObj)+1), "" );
+        else
+            fprintf( pFile, "     " );
         fprintf( pFile, " reg%d (",       i );
         fprintf( pFile, " .q( %s ),",      pName );
         fprintf( pFile, " .qbar()," );
         fprintf( pFile, " .d( %s ),",      Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFoToFi(p, pObj))) );
         fprintf( pFile, " .clk( %s ),",    "1\'b0" );
         fprintf( pFile, " .arst( %s ),",   "1\'b0" );
-        fprintf( pFile, " .arstval( %s )", "1\'b0" );
+        if ( p->vInits )
+            fprintf( pFile, " .arstval( %s_init )", pName );
+        else
+            fprintf( pFile, " .arstval( %s )", "1\'b0" );
         fprintf( pFile, " ) ;\n" );
     }
+    iFanin = 0;
+    assert( !p->vInits || Wlc_NtkFfNum(p) == Vec_IntSize(p->vInits) );
+    if ( p->vInits )
+    Wlc_NtkForEachCi( p, pObj, i )
+    {
+        int nDigits   = Abc_Base10Log(pObj->End+1) + 1;
+        char * pName  = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
+        assert( i == Wlc_ObjCiId(pObj) );
+        if ( pObj->Type == WLC_OBJ_PI )
+            continue;
+        sprintf( Range, "       [%d:%d]%*s", Wlc_ObjRange(pObj) - 1, 0, 8-nDigits, "" );
+        fprintf( pFile, "         " );
+        fprintf( pFile, "wire %s ", Range );
+        fprintf( pFile, "%s_init%*s = ", pName, 11 - strlen(pName), "" );
+        if ( Vec_IntEntry(p->vInits, i-Wlc_NtkPiNum(p)) > 0 )
+            fprintf( pFile, "%s", Wlc_ObjName(p, Wlc_ObjId(p, Wlc_NtkPi(p, Vec_IntEntry(p->vInits, i-Wlc_NtkPiNum(p))))));
+        else
+        {
+            fprintf( pFile, "%d\'b", Wlc_ObjRange(pObj) );
+            for ( k = 0; k < Wlc_ObjRange(pObj); k++ )
+                fprintf( pFile, "%c", p->pInits[iFanin + k] );
+        }
+        fprintf( pFile, ";\n" );
+        iFanin += Wlc_ObjRange(pObj);
+
+        //printf( "%d %d %s\n", iFanin, Wlc_ObjRange(pObj), Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
+    }
+    k = (int)strlen(p->pInits);
+    //assert( !p->vInits || iFanin == (int)strlen(p->pInits) );
     fprintf( pFile, "endmodule\n\n" );
 } 
 void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName )