Changes to enable smarter simulation.

src/aig/saig/saigMiter.c

@@ -1234,7 +1234,7 @@ int Saig_ManDemiterNew( Aig_Man_t * pMan )
     vSuper = Vec_PtrAlloc( 100 );
     Saig_ManForEachPo( pMan, pObj, i )
     {
-        if ( pMan->nConstrs && i >= pMan->nConstrs )
+        if ( pMan->nConstrs && i >= Saig_ManPoNum(pMan) - pMan->nConstrs )
             break;
         printf( "Output %3d : ", i );
         if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )

src/aig/ssw/ssw.h

@@ -115,6 +115,8 @@ extern int           Ssw_MiterStatus( Aig_Man_t * p, int fVerbose );
 extern int           Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars );
 extern int           Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
 extern int           Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
+/*=== sswRarity.c ===================================================*/
+extern int           Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, 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 );
@@ -125,6 +127,7 @@ extern int           Ssw_SmlNumWordsTotal( Ssw_Sml_t * p );
 extern unsigned *    Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj );
 extern int           Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
 extern void          Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit );
+extern int           Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p );
 extern Vec_Ptr_t *   Ssw_SmlSimDataPointers( Ssw_Sml_t * p );
 
 

src/aig/ssw/sswRarity.c

@@ -94,11 +94,12 @@ Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int n
     p->nFrames = nFrames;
     p->nBinSize = nBinSize;
     p->fVerbose = fVerbose;
-    p->nGroups = Aig_ManRegNum(pAig) / nBinSize;
+    p->nGroups  = Aig_ManRegNum(pAig) / nBinSize;
-    p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
+    p->pRarity  = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
-    p->pGroupValues = ABC_CALLOC( int, (Aig_ManRegNum(pAig) / nBinSize) );
+    p->pGroupValues = ABC_CALLOC( int, p->nGroups );
     p->pPatCosts = ABC_CALLOC( double, p->nWords * 32 );
     p->pSml = Ssw_SmlStart( pAig, 0, nFrames, nWords );
+    p->vSimInfo = Ssw_SmlSimDataPointers( p->pSml );
     return p;
 }
 
@@ -115,8 +116,8 @@ Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int n
 ***********************************************************************/
 void Ssw_RarManStop( Ssw_RarMan_t * p )
 {
-    Ssw_SmlStop( p->pSml );
+    if ( p->pSml ) Ssw_SmlStop( p->pSml );
-    Ssw_ClassesStop( p->ppClasses );
+    if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
     Vec_PtrFreeP( &p->vSimInfo );
     Vec_IntFreeP( &p->vInits );
     ABC_FREE( p->pGroupValues );
@@ -142,19 +143,34 @@ void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
     Aig_Obj_t * pObj;
     unsigned * pData;
     int i, k;
+/*
+    Saig_ManForEachLi( p->pAig, pObj, i )
+    {
+        pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
+        Extra_PrintBinary( stdout, pData, 32 );  printf( "\n" );
+    }
+*/
     for ( k = 0; k < p->nWords * 32; k++ )
     {
         for ( i = 0; i < p->nGroups; i++ )
             p->pGroupValues[i] = 0;
         Saig_ManForEachLi( p->pAig, pObj, i )
         {
-            pData = Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) );
+            pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
-            if ( Aig_InfoHasBit(pData, k) )
+            if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups )
                 p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize));
         }
         for ( i = 0; i < p->nGroups; i++ )
             Ssw_RarAddToBinPat( p, i, p->pGroupValues[i] );
     }
+/*
+    for ( i = 0; i < p->nGroups; i++ )
+    {
+        for ( k = 0; k < (1 << p->nBinSize); k++ )
+            printf( "%d ", Ssw_RarGetBinPat(p, i, k) );
+        printf( "\n" );
+    }
+*/
 }
 
 /**Function*************************************************************
@@ -173,21 +189,36 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
     Aig_Obj_t * pObj;
     unsigned * pData;
     int i, k, Value;
-    for ( i = 0; i < p->nWords * 32; i++ )
+
-        p->pPatCosts[i] = 0.0;
+    // for each pattern
-    for ( i = 0; i < p->nGroups; i++ )
+    for ( k = 0; k < p->nWords * 32; k++ )
     {
-        for ( k = 0; k < p->nWords * 32; k++ )
+        for ( i = 0; i < p->nGroups; i++ )
+            p->pGroupValues[i] = 0;
+        // compute its group values
+        Saig_ManForEachLi( p->pAig, pObj, i )
         {
-            Value = Ssw_RarGetBinPat( p, i, k );
+            pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
-            if ( Value == 0 )
+            if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups )
-                continue;
+                p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize));
-            p->pPatCosts[k] += 1.0/(Value*Value);
         }
+        // find the cost of its values
+        p->pPatCosts[k] = 0.0;
+        for ( i = 0; i < p->nGroups; i++ )
+        {
+            Value = Ssw_RarGetBinPat( p, i, p->pGroupValues[i] );
+            assert( Value > 0 );
+            p->pPatCosts[k] += 1.0/(Value*Value);
+//            printf( "%d ", Value );
+        }
+//        printf( "\n" );
+        // print the result
+//        printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
     }
+
     // choose as many as there are words
     Vec_IntClear( vInits );
-    for ( i = 0; i < p->nFrames; i++ )
+    for ( i = 0; i < p->nWords; i++ )
     {
         // select the best
         int iPatBest = -1;
@@ -202,13 +233,15 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
         assert( iPatBest >= 0 );
         p->pPatCosts[iPatBest] = -ABC_INFINITY;
         // set the flops
-        Saig_ManForEachLo( p->pAig, pObj, k )
+        Saig_ManForEachLi( p->pAig, pObj, k )
         {
-            pData = Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) );
+            pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
             Vec_IntPush( vInits, Aig_InfoHasBit(pData, iPatBest) );
         }
+//printf( "Best pattern %5d\n", iPatBest );
+
     }
-    assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nFrames );
+    assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
 }
 
 
@@ -265,15 +298,14 @@ Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
 
   Synopsis    [Filter equivalence classes of nodes.]
 
-  Description [Unrolls at most nFramesMax frames. Works with nConfMax 
+  Description []
-  conflicts until the first undefined SAT call. Verbose prints the message.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_RarSignalFilter( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int nRounds, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
+int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int nRounds, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 {
     Ssw_RarMan_t * p;
     int r, i, k, clkTotal = clock();
@@ -281,7 +313,7 @@ void Ssw_RarSignalFilter( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSiz
     assert( Aig_ManConstrNum(pAig) == 0 );
     // consider the case of empty AIG
     if ( Aig_ManNodeNum(pAig) == 0 )
-        return;
+        return -1;
     // reset random numbers
     Aig_ManRandom( 1 );
     // create manager
@@ -299,13 +331,11 @@ void Ssw_RarSignalFilter( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSiz
     else
         p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) );
     // duplicate the array
-    for ( i = 1; i < nFrames; i++ )
+    for ( i = 1; i < nWords; i++ )
         for ( k = 0; k < Aig_ManRegNum(pAig); k++ )
             Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) );
-    assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * nFrames );
+    assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * nWords );
     // initialize simulation manager
-    p->pSml = Ssw_SmlStart( pAig, 0, nFrames, nWords );
-    p->vSimInfo = Ssw_SmlSimDataPointers( p->pSml );
     Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
     // print the stats
     if ( fVerbose )
@@ -349,6 +379,83 @@ void Ssw_RarSignalFilter( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSiz
     }
     // cleanup
     Ssw_RarManStop( p );
+    return -1;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Perform sequential simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose )
+{
+    int fMiter = 1;
+    Ssw_RarMan_t * p;
+    int r, clk, clkTotal = clock();
+    int RetValue = -1;
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManConstrNum(pAig) == 0 );
+    // consider the case of empty AIG
+    if ( Aig_ManNodeNum(pAig) == 0 )
+        return -1;
+    if ( fVerbose )
+        printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d timeout.\n", 
+            nWords, nFrames, nBinSize, nRounds, TimeOut );
+    // reset random numbers
+    Aig_ManRandom( 1 );
+    // create manager
+    p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
+    p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords );
+    Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
+    // perform simulation rounds
+    for ( r = 0; r < nRounds; r++ )
+    {
+        clk = clock();
+        // simulate
+        Ssw_SmlSimulateOne( p->pSml );
+        if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
+        {
+            if ( fVerbose ) printf( "\n" );
+            printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+            RetValue = 0;
+            break;
+        }
+        // get initialization patterns
+        Ssw_RarUpdateCounters( p );
+        Ssw_RarTransferPatterns( p, p->vInits );
+        Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
+        // printout
+        if ( fVerbose )
+        {
+//            printf( "Round %3d:  ", r );
+//            Abc_PrintTime( 1, "Time", clock() - clk );
+            printf( "." );
+        }
+        // check timeout
+        if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+        {
+            if ( fVerbose ) printf( "\n" );
+            printf( "Reached timeout (%d seconds).\n",  TimeOut );
+            break;
+        }
+    }
+    if ( r == nRounds )
+    {
+        if ( fVerbose ) printf( "\n" );
+        printf( "Simulation did not assert POs in the first %d frames.  ", nRounds * nFrames );
+        Abc_PrintTime( 1, "Time", clock() - clkTotal );
+    }
+    // cleanup
+    Ssw_RarManStop( p );
+    return RetValue;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/aig/ssw/sswSim.c

@@ -928,11 +928,11 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
 void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit )
 {
     Aig_Obj_t * pObj;
-    int Entry, i, k, nRegs;
+    int Entry, i, nRegs;
     nRegs = Aig_ManRegNum(p->pAig);
     assert( nRegs > 0 );
     assert( nRegs <= Aig_ManPiNum(p->pAig) );
-    assert( Vec_IntSize(vInit) == nRegs * p->nFrames );
+    assert( Vec_IntSize(vInit) == nRegs * p->nWordsFrame );
     // assign random info for primary inputs
     Saig_ManForEachPi( p->pAig, pObj, i )
         Ssw_SmlAssignRandom( p, pObj );
@@ -982,8 +982,12 @@ int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p )
     Aig_Obj_t * pObj;
     int i;
     Saig_ManForEachPo( p->pAig, pObj, i )
+    {
+        if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
+            return 0;
         if ( !Ssw_SmlNodeIsZero(p, pObj) )
             return 1;
+    }
     return 0;
 }
 

src/base/abci/abc.c

@@ -247,6 +247,7 @@ static int Abc_CommandSeqCleanup             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandCycle                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandXsim                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSim                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSim2                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDarPhase               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSynch                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandClockGate              ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -666,6 +667,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "cycle",         Abc_CommandCycle,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "xsim",          Abc_CommandXsim,             0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "sim",           Abc_CommandSim,              0 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "sim2",          Abc_CommandSim2,             0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "phase",         Abc_CommandDarPhase,         1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "synch",         Abc_CommandSynch,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "clockgate",     Abc_CommandClockGate,        1 );
@@ -15764,6 +15766,135 @@ usage:
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandSim2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int c;
+    int nFrames;
+    int nWords;
+    int nBinSize;
+    int nRounds;
+    int TimeOut;
+    int fVerbose;
+    extern int Abc_NtkDarSeqSim2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose );
+    // set defaults
+    nFrames    =  20;
+    nWords     =  50;
+    nBinSize   =   8;
+    nRounds    =  80;
+    TimeOut    =   0;
+    fVerbose   =   1;
+    // parse command line
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTvh" ) ) != 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 '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 ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        Abc_Print( -1, "Only works for strashed networks.\n" );
+        return 1;
+    }
+    ABC_FREE( pNtk->pSeqModel );
+    pAbc->Status = Abc_NtkDarSeqSim2( pNtk, nFrames, nWords, nBinSize, nRounds, TimeOut, fVerbose );  
+    Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: sim2 [-FWBRT 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-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    []
@@ -24632,21 +24763,10 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Gia_ManSimSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFRTmvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWRTmvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'W':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nWords = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nWords < 0 ) 
-                goto usage;
-            break;
         case 'F':
             if ( globalUtilOptind >= argc )
             {
@@ -24658,6 +24778,17 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nIters < 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;
+            }
+            pPars->nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nWords < 0 ) 
+                goto usage;
+            break;
         case 'R':
             if ( globalUtilOptind >= argc )
             {
@@ -24713,11 +24844,11 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &sim [-WFRT num] [-mvh]\n" );
+    Abc_Print( -2, "usage: &sim [-FWRT 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-W num : the number of words to simulate [default = %d]\n", pPars->nWords );
     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-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" );

src/base/abci/abcDar.c

@@ -3007,6 +3007,52 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs random simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarSeqSim2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose )
+{
+    Aig_Man_t * pMan;
+    int status, RetValue = -1, clk = clock();
+    if ( Abc_NtkGetChoiceNum(pNtk) )
+    {
+        printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
+        Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
+    }
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, TimeOut, fVerbose ) )
+    { 
+        if ( pMan->pSeqModel )
+        {
+            printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
+                nFrames, nWords, pMan->pSeqModel->iPo, pMan->pSeqModel->iFrame );
+            status = Saig_ManVerifyCex( pMan, pMan->pSeqModel );
+            if ( status == 0 )
+                printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+        }
+        ABC_FREE( pNtk->pModel );
+        ABC_FREE( pNtk->pSeqModel );
+        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+        RetValue = 0;
+    }
+    else
+    {
+        printf( "Simulation of %d frames with %d words did not assert the outputs.    ", 
+            nFrames, nWords );
+    }
+    ABC_PRT( "Time", clock() - clk );
+    Aig_ManStop( pMan );
+    return RetValue;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Gives the current ABC network to AIG manager for processing.]