Version abc70911

5 files changed, 24 insertions, 9 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a8888d81..bbaa80a4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3095,7 +3095,7 @@ usage:
     fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax );
     fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver );
     fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared );
-    fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
+    fprintf( pErr, "\t-L <num> : max level increase after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     fprintf( pErr, "\t-s       : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" );
     fprintf( pErr, "\t-z       : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" );
     fprintf( pErr, "\t-f       : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 356a5565..06e425d5 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -49,10 +49,10 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
     Aig_Man_t * pMan;
     Aig_Obj_t * pObjNew;
     Abc_Obj_t * pObj;
-    int i, nNodes;
+    int i, nNodes, nDontCares;
     // make sure the latches follow PIs/POs
-    if ( fRegisters )
-    {
+    if ( fRegisters ) 
+    { 
         assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
         Abc_NtkForEachCi( pNtk, pObj, i )
             if ( i < Abc_NtkPiNum(pNtk) )
@@ -64,6 +64,21 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
                 assert( Abc_ObjIsPo(pObj) );
             else
                 assert( Abc_ObjIsBi(pObj) );
+        // print warning about initial values
+        nDontCares = 0;
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            if ( Abc_LatchIsInitDc(pObj) )
+            {
+                Abc_LatchSetInit0(pObj);
+                nDontCares++;
+            }
+        if ( nDontCares )
+        {
+            printf( "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
+            printf( "The don't-care are assumed to be 0. The result may not verify.\n" );
+            printf( "Use command \"print_latch\" to see the init values of registers.\n" );
+            printf( "Use command \"init\" to change the values.\n" );
+        }
     }
     // create the manager
     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
@@ -985,7 +1000,7 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
     pMan = Abc_NtkToDar( pNtk, 1 );
     if ( pMan == NULL )
         return NULL;
-    pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, fVerbose, NULL );
+    pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL );
     Aig_ManStop( pTemp );
     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
         pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 69373597..c77f8dea 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -80,7 +80,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
     }
 //timeRetime = clock() - timeRetime;
 //    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) )
-//        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+//        printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
     return pNtkAig;
 
 }
@@ -145,7 +145,7 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup )
     }
 //timeRetime = clock() - timeRetime;
 //    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) )
-//        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+//        printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
     return pNtkAig;
 
 }
diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c
index a4bcaefc..16c7cc92 100644
--- a/src/base/seq/seqCreate.c
+++ b/src/base/seq/seqCreate.c
@@ -82,7 +82,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsDfsOrdered(pNtk) );
 
     if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
-        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+        printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
     assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
 
     // start the network
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index ba2c154c..27638644 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -99,7 +99,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
     // make sure it is an AIG without self-feeding latches
     assert( !Abc_NtkHasAig(pNtk) );
     if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
-        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+        printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
     assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
 
     // remove the dangling nodes