Version abc80919

3 files changed, 100 insertions, 14 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 26d72934..7247f8ed 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3131,7 +3131,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: fx [-S num] [-D num] [-N num] [-sdzcvh]\n");
+    fprintf( pErr, "usage: fx [-SDN num] [-sdzcvh]\n");
     fprintf( pErr, "\t         performs unate fast extract on the current network\n");
     fprintf( pErr, "\t-S num : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax );  
     fprintf( pErr, "\t-D num : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax );  
@@ -13876,19 +13876,24 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int nFramesP;
     int nConfMax;
+    int nVarsMax;
+    int fNewAlgor;
     int fVerbose;
     extern Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFramesP   = 0;
+    nFramesP   =     0;
     nConfMax   = 10000;
-    fVerbose   = 0;
+    nVarsMax   =  5000;
+    fNewAlgor  =     0;
+    fVerbose   =     1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PCSnvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -13914,6 +13919,20 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfMax < 0 ) 
                 goto usage;
             break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nVarsMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nVarsMax < 0 ) 
+                goto usage;
+            break;
+        case 'n':
+            fNewAlgor ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -13943,7 +13962,10 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose );
+    if ( fNewAlgor )
+        pNtkRes = Abc_NtkDarLcorrNew( pNtk, nVarsMax, nConfMax, fVerbose );
+    else
+        pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -13954,10 +13976,12 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: lcorr [-P num] [-C num] [-vh]\n" );
+    fprintf( pErr, "usage: lcorr [-PCS num] [-nvh]\n" );
     fprintf( pErr, "\t         computes latch correspondence using 1-step induction\n" );
     fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
     fprintf( pErr, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
+    fprintf( pErr, "\t-S num : the max number of SAT variables [default = %d]\n", nVarsMax );
+    fprintf( pErr, "\t-n     : toggle new algorithm [default = %s]\n", fNewAlgor? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index b84c5191..ac5ee882 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1316,6 +1316,50 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
 
 /**Function*************************************************************
 
+  Synopsis    [Computes latch correspondence.]
+
+  Description [] 
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose )
+{
+    Ssw_Pars_t Pars, * pPars = &Pars;
+    Aig_Man_t * pMan, * pTemp;
+    Abc_Ntk_t * pNtkAig = NULL;
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    Ssw_ManSetDefaultParams( pPars );
+    pPars->fLatchCorrOpt = 1;
+//    pPars->nFramesAddSim = 0;
+    pPars->nBTLimit      = nConfMax;
+    pPars->nSatVarMax    = nVarsMax;
+    pPars->fVerbose      = fVerbose;
+    pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
+    Aig_ManStop( pTemp );
+    if ( pMan )
+    {
+        if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
+            pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+        else
+        {
+            Abc_Obj_t * pObj;
+            int i;
+            pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+            Abc_NtkForEachLatch( pNtkAig, pObj, i )
+                Abc_LatchSetInit0( pObj );
+        }
+        Aig_ManStop( pMan );
+    }
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
 
   Description []
@@ -1342,6 +1386,8 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
     {
         int iFrame;
         RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame );
+        FREE( pNtk->pModel );
+        FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( RetValue == 1 )
             printf( "No output was asserted in %d frames. ", iFrame );
@@ -1350,17 +1396,19 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
         else // if ( RetValue == 0 )
         {
             Fra_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
+            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
         }
     }
     else
     {
         Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
+        FREE( pNtk->pModel );
+        FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( pNtk->pSeqModel )
         {
             Fra_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
+            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
             RetValue = 0;
         }
         else
@@ -1388,7 +1436,7 @@ PRT( "Time", clock() - clk );
 int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
 {
     Aig_Man_t * pMan;
-    int RetValue, Depth, clk = clock();
+    int RetValue, iFrame, clk = clock();
     // derive the AIG manager
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
@@ -1397,11 +1445,16 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
         return -1;
     }
     assert( pMan->nRegs > 0 );
-    RetValue = Inter_ManPerformInterpolation( pMan, pPars, &Depth );
+    RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
     else if ( RetValue == 0 )
-        printf( "Property DISPROVED with counter-example at depth %d.  ", Depth );
+    {
+        printf( "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness).  ", iFrame );
+        FREE( pNtk->pModel );
+        FREE( pNtk->pSeqModel );
+        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+    }
     else if ( RetValue == -1 )
         printf( "Property UNDECIDED.  " );
     else
@@ -1440,7 +1493,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
         Prove_ParamsSetDefault( pParams );
         RetValue = Abc_NtkIvyProve( &pNtkComb, pParams );
         // transfer model if given
-        pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
+//        pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
         Abc_NtkDelete( pNtkComb );
         // return the result, if solved
         if ( RetValue == 1 )
@@ -1485,11 +1538,15 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
     else
     {
         RetValue = Fra_FraigSec( pMan, pSecPar );
+        FREE( pNtk->pModel );
+        FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( pNtk->pSeqModel )
         {
             Fra_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace).\n", pCex->iPo, pCex->iFrame );
+            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame );
+            if ( !Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel ) )
+                printf( "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
         }
     }
     Aig_ManStop( pMan );
@@ -1842,6 +1899,8 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
         if ( pCex )
             printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
                 nFrames, nWords, pCex->iPo, pCex->iFrame );
+        FREE( pNtk->pModel );
+        FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pCex;
         RetValue = 1;
     }
@@ -2341,6 +2400,9 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
     if ( pMan == NULL )
         return;
     Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose, 0 );
+    FREE( pNtk->pModel );
+    FREE( pNtk->pSeqModel );
+    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     Aig_ManStop( pMan );
 }
 
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 371adfc9..6d7948ab 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1734,7 +1734,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
         fclose( pFile );
     }
     else
-    {
+    { 
         Fra_Cex_t * pCex = pNtk->pSeqModel;
         Abc_Obj_t * pObj;
         FILE * pFile;