Added equivalence class computation for flop outputs only in &equiv2.

2 files changed, 13 insertions, 8 deletions

diff --git a/src/aig/ssw/sswFilter.c b/src/aig/ssw/sswFilter.c
index a0c0934a..8b758915 100644
--- a/src/aig/ssw/sswFilter.c
+++ b/src/aig/ssw/sswFilter.c
@@ -378,7 +378,7 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fVerbose )
+void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 {
     Ssw_Pars_t Pars, * pPars = &Pars;
     Ssw_Man_t * p;
@@ -401,7 +401,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
     pPars->nFramesK  = nFramesMax;
     // create trivial equivalence classes with all nodes being candidates for constant 1
     if ( pAig->pReprs == NULL )
-        p->ppClasses = Ssw_ClassesPrepareSimple( pAig, 0, 0 );
+        p->ppClasses = Ssw_ClassesPrepareSimple( pAig, fLatchOnly, 0 );
     else
         p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
     Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
@@ -468,7 +468,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fVerbose )
+void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 { 
     Aig_Man_t * pAig;
     pAig = Gia_ManToAigSimple( p );
@@ -478,7 +478,7 @@ void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRoun
         ABC_FREE( p->pReprs );
         ABC_FREE( p->pNexts );
     }
-    Ssw_SignalFilter( pAig, nFramesMax, nConfMax, nRounds, TimeLimit, TimeLimit2, pCex, fVerbose );
+    Ssw_SignalFilter( pAig, nFramesMax, nConfMax, nRounds, TimeLimit, TimeLimit2, pCex, fLatchOnly, fVerbose );
     Gia_ManReprFromAigRepr( pAig, p );
     Aig_ManStop( pAig );
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7490751a..3bf303e2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -24998,17 +24998,18 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Equiv2( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fVerbose );
+    extern void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
     int nFramesMax =   20;
     int nConfMax   =  500;
     int nRounds    =   10;
     int TimeLimit  =    0;
     int TimeLimit2 =    0;
     int fUseCex    =    0;
+    int fLatchOnly =    0;
     int fVerbose   =    0;
     int c;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCRTSxvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCRTSxlvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -25070,6 +25071,9 @@ int Abc_CommandAbc9Equiv2( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'x':
             fUseCex ^= 1;
             break;
+        case 'l':
+            fLatchOnly ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -25098,14 +25102,14 @@ int Abc_CommandAbc9Equiv2( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
     }
-    Ssw_SignalFilterGia( pAbc->pGia, nFramesMax, nConfMax, nRounds, TimeLimit, TimeLimit2, fUseCex? pAbc->pCex: NULL, fVerbose );
+    Ssw_SignalFilterGia( pAbc->pGia, nFramesMax, nConfMax, nRounds, TimeLimit, TimeLimit2, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
     pAbc->Status  = -1;
 //    pAbc->nFrames = pAbc->pCex->iFrame;
 //    Abc_FrameReplaceCex( pAbc, &pAbc->pCex );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &equiv2 [-FCRTS num] [-xvh]\n" );
+    Abc_Print( -2, "usage: &equiv2 [-FCRTS num] [-xlvh]\n" );
     Abc_Print( -2, "\t         computes candidate equivalence classes\n" );
     Abc_Print( -2, "\t-F num : the max number of frames for BMC [default = %d]\n", nFramesMax );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax );
@@ -25113,6 +25117,7 @@ usage:
     Abc_Print( -2, "\t-T num : runtime limit in seconds for all rounds [default = %d]\n", TimeLimit );
     Abc_Print( -2, "\t-S num : runtime limit in seconds for one round [default = %d]\n", TimeLimit2 );
     Abc_Print( -2, "\t-x     : toggle using the current cex to perform refinement [default = %s]\n", fUseCex? "yes": "no" );
+    Abc_Print( -2, "\t-l     : toggle considering only latch output equivalences [default = %s]\n", fLatchOnly? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;