Changes to enable smarter simulation.

5 files changed, 319 insertions, 82 deletions

diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 7632d923..1361893a 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -119,8 +119,8 @@ extern int           Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars
 extern int           Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
 extern int           Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose );
 /*=== sswRarity2.c ===================================================*/
-extern int           Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
-extern int           Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose );
+extern int           Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
+extern int           Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
 /*=== sswSim.c ===================================================*/
 extern Ssw_Sml_t *   Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
 extern Ssw_Sml_t *   Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c
index f24e2d85..3026cf6b 100644
--- a/src/aig/ssw/sswRarity.c
+++ b/src/aig/ssw/sswRarity.c
@@ -261,7 +261,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
     int f, i, iBit;
     // assign register outputs
     Saig_ManForEachLi( pAig, pObj, i )
-        pObj->fMarkB = 0;
+        pObj->fMarkB = Aig_InfoHasBit( pCex->pData, i );
     // simulate the timeframes
     iBit = pCex->nRegs;
     for ( f = 0; f <= pCex->iFrame; f++ )
@@ -304,7 +304,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose )
+int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose )
 {
     int fMiter = 1;
     Ssw_RarMan_t * p;
@@ -381,7 +381,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
+int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 {
     int fMiter = 0;
     Ssw_RarMan_t * p;
@@ -486,7 +486,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
+int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 { 
     Aig_Man_t * pAig;
     int RetValue;
@@ -497,7 +497,7 @@ int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize
         ABC_FREE( p->pReprs );
         ABC_FREE( p->pNexts );
     }
-    RetValue = Ssw_RarSignalFilter( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose );
+    RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose );
     Gia_ManReprFromAigRepr( pAig, p );
     Aig_ManStop( pAig );
     return RetValue;
diff --git a/src/aig/ssw/sswRarity2.c b/src/aig/ssw/sswRarity2.c
index c0305931..59f59f93 100644
--- a/src/aig/ssw/sswRarity2.c
+++ b/src/aig/ssw/sswRarity2.c
@@ -89,6 +89,25 @@ static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id )  { assert( Id < 6
 
 /**Function*************************************************************
 
+  Synopsis    [Prepares random number generator.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_RarManPrepareRandom( int nRandSeed )
+{
+    int i;
+    Aig_ManRandom( 1 );
+    for ( i = 0; i < nRandSeed; i++ )
+        Aig_ManRandom( 0 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Initializes random primary inputs.]
 
   Description []
@@ -133,7 +152,7 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin
     // compute the pattern sequence
     iPatThis = iPatFinal;
     vTrace = Vec_IntStartFull( iFrame / p->nFrames + 1 );
-    Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatFinal );
+    Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatThis );
     for ( r = iFrame / p->nFrames - 1; r >= 0; r-- )
     {
         iPatThis = Vec_IntEntry( p->vPatBests, r * p->nWords + iPatThis / 64 );
@@ -145,7 +164,7 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin
     pCex->iPo = iPo;
     // insert the bits
     iBit = Aig_ManRegNum(p->pAig);
-    for ( f = 0; f < iFrame; f++ )
+    for ( f = 0; f <= iFrame; f++ )
     {
         Ssw_RarManAssingRandomPis( p );
         iPatThis = Vec_IntEntry( vTrace, f / p->nFrames );
@@ -158,6 +177,19 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin
         }
     }
     Vec_IntFree( vTrace );
+    assert( iBit == pCex->nBits );
+    // verify the counter example
+    if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
+    {
+        printf( "Ssw_RarDeriveCex(): Counter-example is invalid.\n" );
+        Abc_CexFree( pCex );
+        pCex = NULL;
+    }
+    else
+    {
+//      printf( "Counter-example verification is successful.\n" );
+        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
+    }
     return pCex;
 }
 
@@ -394,34 +426,6 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
-{
-    word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
-    word Flip = pObj->fPhase ? ~0 : 0;
-    int w, i;
-    for ( w = 0; w < p->nWords; w++ )
-        if ( pSim[w] ^ Flip )
-        {
-            for ( i = 0; i < 64; i++ )
-                if ( ((pSim[w] ^ Flip) >> i) & 1 )
-                    break;
-            assert( i < 64 );
-            return w * 64 + i;
-        }
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Ssw_RarManObjIsConst( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
 {
     word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
@@ -496,6 +500,34 @@ unsigned Ssw_RarManObjHashWord( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
+{
+    word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
+    word Flip = pObj->fPhase ? ~0 : 0;
+    int w, i;
+    for ( w = 0; w < p->nWords; w++ )
+        if ( pSim[w] ^ Flip )
+        {
+            for ( i = 0; i < 64; i++ )
+                if ( ((pSim[w] ^ Flip) >> i) & 1 )
+                    break;
+            assert( i < 64 );
+            return w * 64 + i;
+        }
+    return -1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Check if any of the POs becomes non-constant.]
 
   Description []
@@ -509,7 +541,7 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
 {
     Aig_Obj_t * pObj;
     int i;
-    p->iFailPo = -1;
+    p->iFailPo  = -1;
     p->iFailPat = -1;
     Saig_ManForEachPo( p->pAig, pObj, i )
     {
@@ -772,7 +804,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
     int f, i, iBit;
     // assign register outputs
     Saig_ManForEachLi( pAig, pObj, i )
-        pObj->fMarkB = 0;
+        pObj->fMarkB = Aig_InfoHasBit( pCex->pData, i );
     // simulate the timeframes
     iBit = pCex->nRegs;
     for ( f = 0; f <= pCex->iFrame; f++ )
@@ -815,7 +847,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose )
+int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose )
 {
     int fMiter = 1;
     Ssw_RarMan_t * p;
@@ -827,10 +859,10 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
     if ( Aig_ManNodeNum(pAig) == 0 )
         return -1;
     if ( fVerbose )
-        printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", 
-            nWords, nFrames, nBinSize, nRounds, TimeOut );
+        printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", 
+            nWords, nFrames, nRounds, nRandSeed, TimeOut );
     // reset random numbers
-    Aig_ManRandom( 1 );
+    Ssw_RarManPrepareRandom( nRandSeed );
 
     // create manager
     p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
@@ -847,7 +879,8 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
             if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
             {
                 if ( fVerbose ) printf( "\n" );
-                printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+//                printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+                Ssw_RarManPrepareRandom( nRandSeed );
                 ABC_FREE( pAig->pSeqModel );
                 pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat );
                 RetValue = 0;
@@ -872,7 +905,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
         }
     }
 finish:
-    if ( r == nRounds )
+    if ( r == nRounds && f == nFrames )
     {
         if ( fVerbose ) printf( "\n" );
         printf( "Simulation did not assert POs in the first %d frames.  ", nRounds * nFrames );
@@ -886,6 +919,30 @@ finish:
 
 /**Function*************************************************************
 
+  Synopsis    [Perform sequential simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose )
+{
+    Aig_Man_t * pAig;
+    int RetValue;
+    pAig = Gia_ManToAigSimple( p );
+    RetValue = Ssw_RarSimulate2( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose );
+    // save counter-example
+    Abc_CexFree( p->pCexSeq );
+    p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
+    Aig_ManStop( pAig );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Filter equivalence classes of nodes.]
 
   Description []
@@ -895,9 +952,8 @@ finish:
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
+int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 {
-    int fMiter = 0;
     Ssw_RarMan_t * p;
     int r, f, i, k, clkTotal = clock();
     int RetValue = -1;
@@ -907,10 +963,10 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
     if ( Aig_ManNodeNum(pAig) == 0 )
         return -1;
     if ( fVerbose )
-        printf( "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", 
-            nWords, nFrames, nBinSize, nRounds, TimeOut );
+        printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", 
+            nWords, nFrames, nRounds, nRandSeed, TimeOut );
     // reset random numbers
-    Aig_ManRandom( 1 );
+    Ssw_RarManPrepareRandom( nRandSeed );
 
     // create manager
     p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
@@ -953,9 +1009,11 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
             Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
             if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
             {
-                if ( fVerbose ) printf( "\n" );
-                printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
-                ABC_FREE( pAig->pSeqModel );
+                if ( !fVerbose ) 
+                    printf( "\r" );
+//                printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+                Ssw_RarManPrepareRandom( nRandSeed );
+                Abc_CexFree( pAig->pSeqModel );
                 pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat );
                 RetValue = 0;
                 goto finish;
@@ -968,25 +1026,31 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
                 goto finish;
             }
         }
+        // get initialization patterns
+        Ssw_RarTransferPatterns( p, p->vInits );
         // printout
         if ( fVerbose )
         {
             printf( "Round %3d:  ", r );
             Ssw_ClassesPrint( p->ppClasses, 0 );
         }
-        // get initialization patterns
-        Ssw_RarTransferPatterns( p, p->vInits );
+        else
+        {
+            printf( "." );
+        }
     }
 finish:
     // report
-    if ( r == nRounds )
+    if ( r == nRounds && f == nFrames )
     {
+        if ( !fVerbose ) 
+            printf( "\r" );
         printf( "Simulation did not assert POs in the first %d frames.  ", nRounds * nFrames );
         Abc_PrintTime( 1, "Time", clock() - clkTotal );
     }
     // cleanup
     Ssw_RarManStop( p );
-    return -1;
+    return RetValue;
 }
 
 /**Function*************************************************************
@@ -1000,7 +1064,7 @@ finish:
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
+int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 { 
     Aig_Man_t * pAig;
     int RetValue;
@@ -1011,8 +1075,11 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz
         ABC_FREE( p->pReprs );
         ABC_FREE( p->pNexts );
     }
-    RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose );
+    RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, pCex, fLatchOnly, fVerbose );
     Gia_ManReprFromAigRepr( pAig, p );
+    // save counter-example
+    Abc_CexFree( p->pCexSeq );
+    p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
     Aig_ManStop( pAig );
     return RetValue;
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7756dbdc..e319c4f8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -337,6 +337,7 @@ static int Abc_CommandAbc9Cof                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Trim               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Dfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Sim                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Sim3               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Resim              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SpecI              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Equiv              ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -758,6 +759,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&trim",         Abc_CommandAbc9Trim,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&dfs",          Abc_CommandAbc9Dfs,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&sim",          Abc_CommandAbc9Sim,          0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&sim3",         Abc_CommandAbc9Sim3,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&resim",        Abc_CommandAbc9Resim,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&speci",        Abc_CommandAbc9SpecI,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&equiv",        Abc_CommandAbc9Equiv,        0 );
@@ -15795,19 +15797,21 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nWords;
     int nBinSize;
     int nRounds;
+    int nRandSeed;
     int TimeOut;
     int fVerbose;
-    extern int Abc_NtkDarSeqSim2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose );
+    extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
     // set defaults
     nFrames    =  20;
     nWords     =  50;
     nBinSize   =   8;
     nRounds    =  80;
+    nRandSeed  =   0;
     TimeOut    =   0;
-    fVerbose   =   1;
+    fVerbose   =   0;
     // parse command line
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRNTvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15855,6 +15859,17 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nRounds < 0 ) 
                 goto usage;
             break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nRandSeed = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nRandSeed < 0 ) 
+                goto usage;
+            break;
         case 'T':
             if ( globalUtilOptind >= argc )
             {
@@ -15886,17 +15901,19 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     ABC_FREE( pNtk->pSeqModel );
-    pAbc->Status = Abc_NtkDarSeqSim2( pNtk, nFrames, nWords, nBinSize, nRounds, TimeOut, fVerbose );  
+    pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose );  
+//    pAbc->nFrames = pAbc->pCex->iFrame;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: sim3 [-FWBRT num] [-vh]\n" );
+    Abc_Print( -2, "usage: sim3 [-FWBRNT num] [-vh]\n" );
     Abc_Print( -2, "\t         performs random simulation of the sequential miter\n" );
     Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
     Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n",  nWords );
     Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n",   nBinSize );
     Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n",  nRounds );
+    Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", nRandSeed );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut );
     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");
@@ -24644,7 +24661,7 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Gia_ManSimSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FWRTmvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWNTmvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -24670,10 +24687,10 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nWords < 0 ) 
                 goto usage;
             break;
-        case 'R':
+        case 'N':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
                 goto usage;
             }
             pPars->RandSeed = atoi(argv[globalUtilOptind]);
@@ -24725,12 +24742,12 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &sim [-FWRT num] [-mvh]\n" );
+    Abc_Print( -2, "usage: &sim [-FWNT num] [-mvh]\n" );
     Abc_Print( -2, "\t         performs random simulation of the sequential miter\n" );
     Abc_Print( -2, "\t         (if candidate equivalences are defined, performs refinement)\n" );
     Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", pPars->nIters );
     Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords );
-    Abc_Print( -2, "\t-R num : random number seed (1 <= num <= 10000) [default = %d]\n", pPars->RandSeed );
+    Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", pPars->RandSeed );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
     Abc_Print( -2, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
@@ -24749,6 +24766,142 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    int nFrames;
+    int nWords;
+    int nBinSize;
+    int nRounds;
+    int nRandSeed;
+    int TimeOut;
+    int fVerbose;
+    extern int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
+    // set defaults
+    nFrames    =  20;
+    nWords     =  50;
+    nBinSize   =   8;
+    nRounds    =  80;
+    nRandSeed  =   0;
+    TimeOut    =   0;
+    fVerbose   =   0;
+    // parse command line
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRNTvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nWords < 0 ) 
+                goto usage;
+            break;
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBinSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBinSize < 0 ) 
+                goto usage;
+            break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nRounds = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nRounds < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nRandSeed = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nRandSeed < 0 ) 
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            TimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( TimeOut < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Sim3(): There is no AIG.\n" );
+        return 1;
+    }
+    pAbc->Status = Ssw_RarSimulate2Gia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose );  
+//    pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame;
+    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &sim3 [-FWBRNT num] [-vh]\n" );
+    Abc_Print( -2, "\t         performs random simulation of the sequential miter\n" );
+    Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+    Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n",  nWords );
+    Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n",   nBinSize );
+    Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n",  nRounds );
+    Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", nRandSeed );
+    Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut );
+    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;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Resim( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cec_ParSim_t Pars, * pPars = &Pars;
@@ -25156,21 +25309,22 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-//    extern int Abc_NtkDarSeqEquiv2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
-    extern int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
-    extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
+//    extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
+    extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
     int c;
     int nFrames    =   20;
     int nWords     =   50;
     int nBinSize   =    8;
     int nRounds    =   80;
+    int nRandSeed  =    0;
     int TimeOut    =    0;
+    int fMiter     =    0;
     int fUseCex    =    0;
     int fLatchOnly =    0;
     int fNewAlgo   =    1;
     int fVerbose   =    0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTxlavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRNTmxlavh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -25218,6 +25372,17 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nRounds < 0 ) 
                 goto usage;
             break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nRandSeed = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nRandSeed < 0 ) 
+                goto usage;
+            break;
         case 'T':
             if ( globalUtilOptind >= argc )
             {
@@ -25229,6 +25394,9 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( TimeOut < 0 ) 
                 goto usage;
             break;
+        case 'm':
+            fMiter ^= 1;
+            break;
         case 'x':
             fUseCex ^= 1;
             break;
@@ -25266,22 +25434,24 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
     }
-    if ( fNewAlgo )
-        pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
-    else
-        pAbc->Status = Ssw_RarSignalFilterGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
-//    pAbc->nFrames = pAbc->pCex->iFrame;
-//    Abc_FrameReplaceCex( pAbc, &pAbc->pCex );
+//    if ( fNewAlgo )
+        pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
+//    else
+//        pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
+//    pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame;
+    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &equiv3 [-FWRT num] [-xlvh]\n" );
+    Abc_Print( -2, "usage: &equiv3 [-FWRNT num] [-mxlvh]\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",    nFrames );
     Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n",     nWords );
 //    Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n",      nBinSize );
     Abc_Print( -2, "\t-R num : the max number of simulation rounds [default = %d]\n", nRounds );
+    Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", nRandSeed );
     Abc_Print( -2, "\t-T num : runtime limit in seconds for all rounds [default = %d]\n", TimeOut );
+    Abc_Print( -2, "\t-m     : toggle miter vs. any circuit [default = %s]\n",        fMiter? "miter": "circuit" );
     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-a     : toggle using a new algorithm [default = %s]\n",        fNewAlgo? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 0f1ee007..4232ab1f 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -3017,7 +3017,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarSeqSim2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose )
+int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose )
 {
     Aig_Man_t * pMan;
     int status, RetValue = -1, clk = clock();
@@ -3027,7 +3027,7 @@ int Abc_NtkDarSeqSim2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
         Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
     }
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
-    if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, TimeOut, fVerbose ) == 0 )
+    if ( Ssw_RarSimulate2( pMan, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ) == 0 )
     { 
         if ( pMan->pSeqModel )
         {