Added simulation of comb circuits with user-specified patterns in command 'sim'.

8 files changed, 206 insertions, 140 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3eabc252..0dcce40a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -17148,7 +17148,8 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
     int TimeOut;
     int fMiter;
     int fVerbose;
-    extern int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, int fNew, int fComb, int fMiter, int fVerbose );
+    char * pFileSim;
+    extern int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, int fNew, int fMiter, int fVerbose, char * pFileSim );
     // set defaults
     fNew       =  0;
     fComb      =  0;
@@ -17157,8 +17158,9 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
     TimeOut    = 30;
     fMiter     =  0;
     fVerbose   =  0;
+    pFileSim   = NULL;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FWTncmvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWTAnmvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -17195,12 +17197,18 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( TimeOut < 0 ) 
                 goto usage;
             break;
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-A\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pFileSim = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
         case 'n':
             fNew ^= 1;
             break;
-        case 'c':
-            fComb ^= 1;
-            break;
         case 'm':
             fMiter ^= 1;
             break;
@@ -17223,22 +17231,28 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Only works for strashed networks.\n" );
         return 1;
     }
+    if ( pFileSim != NULL && Abc_NtkLatchNum(pNtk) )
+    {
+        Abc_Print( -1, "Currently simulation with user-specified patterns works only for comb miters.\n" );
+        return 1;
+    }
     ABC_FREE( pNtk->pSeqModel );
-    pAbc->Status = Abc_NtkDarSeqSim( pNtk, nFrames, nWords, TimeOut, fNew, fComb, fMiter, fVerbose );  
+    pAbc->Status = Abc_NtkDarSeqSim( pNtk, nFrames, nWords, TimeOut, fNew, fMiter, fVerbose, pFileSim );  
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: sim [-FWT num] [-ncmvh]\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-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut );
-    Abc_Print( -2, "\t-n     : toggle new vs. old implementation [default = %s]\n", fNew? "new": "old" );
-    Abc_Print( -2, "\t-c     : toggle comb vs. seq simulaton [default = %s]\n", fComb? "comb": "seq" );
-    Abc_Print( -2, "\t-m     : toggle miter vs. any circuit [default = %s]\n", fMiter? "miter": "circuit" );
-    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");
+    Abc_Print( -2, "usage: sim [-FWT num] [-A file] [-nmvh]\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-T num  : approximate runtime limit in seconds [default = %d]\n", TimeOut );
+    Abc_Print( -2, "\t-A file : text file name with user's patterns [default = random simulation]\n" );
+    Abc_Print( -2, "\t          (patterns are listed, one per line, as sequences of 0s and 1s)\n" );
+    Abc_Print( -2, "\t-n      : toggle new vs. old implementation [default = %s]\n", fNew? "new": "old" );
+    Abc_Print( -2, "\t-m      : toggle miter vs. any circuit [default = %s]\n", fMiter? "miter": "circuit" );
+    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;
 }
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 62c09e3f..bea8e6b9 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -3005,10 +3005,8 @@ Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, int fNew, int fComb, int fMiter, int fVerbose )
+int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, int fNew, int fMiter, int fVerbose, char * pFileSim )
 {
-    extern int Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
-    extern int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
     Aig_Man_t * pMan;
     Abc_Cex_t * pCex;
     int status, RetValue = -1;
@@ -3019,89 +3017,8 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
         Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
     }
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
-    if ( fComb || Abc_NtkLatchNum(pNtk) == 0 )
+    if ( fNew )
     {
-/*
-        if ( Cec_ManSimulate( pMan, nWords, nFrames, TimeOut, fMiter, fVerbose ) )
-        {
-            pCex = pMan->pSeqModel;
-            if ( pCex )
-            {
-            Abc_Print( 1, "Simulation iterated %d times with %d words asserted output %d in frame %d. ", 
-                nFrames, nWords, pCex->iPo, pCex->iFrame );
-            status = Saig_ManVerifyCex( pMan, pCex );
-            if ( status == 0 )
-                Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
-            }
-            ABC_FREE( pNtk->pModel );
-            ABC_FREE( pNtk->pSeqModel );
-            pNtk->pSeqModel = pCex;
-            RetValue = 1;
-        } 
-        else
-        {
-            RetValue = 0;
-            Abc_Print( 1, "Simulation iterated %d times with %d words did not assert the outputs. ", 
-                nFrames, nWords );
-        }
-*/
-        Abc_Print( 1, "Comb simulation is temporarily disabled.\n" );
-    }
-    else if ( fNew )
-    {
-/*
-        if ( Raig_ManSimulate( pMan, nWords, nFrames, TimeOut, fVerbose ) )
-        {
-            if ( (pCex = pMan->pSeqModel) )
-            {
-                Abc_Print( 1, "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
-                    nFrames, nWords, pCex->iPo, pCex->iFrame );
-                status = Saig_ManVerifyCex( pMan, pCex );
-                if ( status == 0 )
-                    Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
-            }
-            ABC_FREE( pNtk->pModel );
-            ABC_FREE( pNtk->pSeqModel );
-            pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
-            RetValue = 1;
-        }
-        else
-        {
-            RetValue = 0;
-            Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs. ", 
-                nFrames, nWords );
-        }
-*/
-/*
-        Fsim_ParSim_t Pars, * pPars = &Pars;
-        Fsim_ManSetDefaultParamsSim( pPars );
-        pPars->nWords = nWords;
-        pPars->nIters = nFrames;
-        pPars->TimeLimit = TimeOut;
-        pPars->fCheckMiter = fMiter;
-        pPars->fVerbose = fVerbose;
-        if ( Fsim_ManSimulate( pMan, pPars ) )
-        { 
-            if ( (pCex = pMan->pSeqModel) )
-            {
-                Abc_Print( 1, "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
-                    nFrames, nWords, pCex->iPo, pCex->iFrame );
-                status = Saig_ManVerifyCex( pMan, pCex );
-                if ( status == 0 )
-                    Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
-            }
-            ABC_FREE( pNtk->pModel );
-            ABC_FREE( pNtk->pSeqModel );
-            pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
-            RetValue = 1;
-        }
-        else
-        {
-            RetValue = 0;
-            Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs. ", 
-                nFrames, nWords );
-        }
-*/ 
         Gia_Man_t * pGia;
         Gia_ParSim_t Pars, * pPars = &Pars;
         Gia_ManSimSetDefaultParams( pPars );
@@ -3133,17 +3050,27 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
         }
         Gia_ManStop( pGia );
     }
-    else
+    else // comb/seq simulator
     {
         Fra_Sml_t * pSml;
-        pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords, fMiter );
+        if ( pFileSim != NULL )
+        {
+            assert( Abc_NtkLatchNum(pNtk) == 0 );
+            pSml = Fra_SmlSimulateCombGiven( pMan, pFileSim, fMiter, fVerbose );
+        }
+        else if ( Abc_NtkLatchNum(pNtk) == 0 )
+            pSml = Fra_SmlSimulateComb( pMan, nWords, fMiter );
+        else
+            pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords, fMiter );
         if ( pSml->fNonConstOut )
         {
             pCex = Fra_SmlGetCounterExample( pSml );
             if ( pCex )
             {
-                Abc_Print( 1, "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
-                    nFrames, nWords, pCex->iPo, pCex->iFrame );
+                Abc_Print( 1, "Simulation of %d frame%s with %d word%s asserted output %d in frame %d. ", 
+                    pSml->nFrames, pSml->nFrames == 1 ? "": "s", 
+                    pSml->nWordsFrame, pSml->nWordsFrame == 1 ? "": "s", 
+                    pCex->iPo, pCex->iFrame );
                 status = Saig_ManVerifyCex( pMan, pCex );
                 if ( status == 0 )
                     Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
@@ -3159,29 +3086,6 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
                 nFrames, nWords );
         }
         Fra_SmlStop( pSml );
-/*
-        if ( Raig_ManSimulate( pMan, nWords, nFrames, TimeOut, fMiter, fVerbose ) )
-        {
-            if ( (pCex = pMan->pSeqModel) )
-            {
-                Abc_Print( 1, "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
-                    nFrames, nWords, pCex->iPo, pCex->iFrame );
-                status = Saig_ManVerifyCex( pMan, pCex );
-                if ( status == 0 )
-                    Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
-            }
-            ABC_FREE( pNtk->pModel );
-            ABC_FREE( pNtk->pSeqModel );
-            pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
-            RetValue = 1;
-        }
-        else
-        {
-            RetValue = 0;
-            Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs. ", 
-                nFrames, nWords );
-        }
-*/
     }
     ABC_PRT( "Time", clock() - clk );
     Aig_ManStop( pMan );
diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c
index 6f8891b3..8b9460d4 100644
--- a/src/opt/mfs/mfsStrash.c
+++ b/src/opt/mfs/mfsStrash.c
@@ -390,7 +390,7 @@ double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode )
     Fra_Sml_t * pSim;
     int Counter;
     pMan = Abc_NtkAigForConstraints( p, pNode );
-    pSim = Fra_SmlSimulateComb( pMan, nSimWords );
+    pSim = Fra_SmlSimulateComb( pMan, nSimWords, 0 );
     Counter = Fra_SmlNodeCountOnes( pSim, Aig_ManCo(pMan, 0) );
     Aig_ManStop( pMan );
     Fra_SmlStop( pSim );
diff --git a/src/proof/fra/fra.h b/src/proof/fra/fra.h
index 1690b463..b1fdb539 100644
--- a/src/proof/fra/fra.h
+++ b/src/proof/fra/fra.h
@@ -371,8 +371,9 @@ extern void                Fra_SmlSimulate( Fra_Man_t * p, int fInit );
 extern void                Fra_SmlResimulate( Fra_Man_t * p );
 extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
 extern void                Fra_SmlStop( Fra_Sml_t * p );
+extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords, int fCheckMiter );
+extern Fra_Sml_t *         Fra_SmlSimulateCombGiven( Aig_Man_t * pAig, char * pFileName, int fCheckMiter, int fVerbose );
 extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter );
-extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
 extern Abc_Cex_t *         Fra_SmlGetCounterExample( Fra_Sml_t * p );
 extern Abc_Cex_t *         Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
 
diff --git a/src/proof/fra/fraClass.c b/src/proof/fra/fraClass.c
index cef2f673..47a9e7a0 100644
--- a/src/proof/fra/fraClass.c
+++ b/src/proof/fra/fraClass.c
@@ -645,7 +645,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
     Aig_Obj_t * pObj, * pRepr, ** ppClass;
     int * pWeights, WeightMax = 0, i, k, c;
     // perform combinational simulation
-    pComb = Fra_SmlSimulateComb( p->pAig, 32 );
+    pComb = Fra_SmlSimulateComb( p->pAig, 32, 0 );
     // compute the weight of each node in the classes
     pWeights = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) );
     memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c
index 95ab0c99..c4f50559 100644
--- a/src/proof/fra/fraClaus.c
+++ b/src/proof/fra/fraClaus.c
@@ -668,7 +668,7 @@ ABC_PRT( "Infoseq", clock() - clk );
 clk = clock();
 //    srand( 0xAABBAABB );
     Aig_ManRandom(1);
-    pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref  );
+    pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 );
 if ( p->fVerbose )
 {
 ABC_PRT( "Sim-cmb", clock() - clk );
@@ -753,7 +753,7 @@ if ( p->fVerbose )
 clk = clock();
 //    srand( 0xAABBAABB );
     Aig_ManRandom(1);
-    pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref  );
+    pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 );
 if ( p->fVerbose )
 {
 //ABC_PRT( "Sim-cmb", clock() - clk );
@@ -1628,7 +1628,7 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
     // simulate the circuit with nCombSimWords * 32 = 64K patterns
 //    srand( 0xAABBAABB );
     Aig_ManRandom(1);
-    pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords );
+    pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords, 0 );
     // create mapping from SAT vars to node IDs
     pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
     memset( pVar2Id, 0, sizeof(int) * p->pCnf->nVars );
diff --git a/src/proof/fra/fraImp.c b/src/proof/fra/fraImp.c
index 4d33717a..809ad8e4 100644
--- a/src/proof/fra/fraImp.c
+++ b/src/proof/fra/fraImp.c
@@ -332,8 +332,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
     // normalize both managers
-    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
-    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1, 1  );
+    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 );
+    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1, 1 );
     // get the nodes sorted by the number of 1s
     vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
     // count the total number of implications
@@ -635,7 +635,7 @@ double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
     if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
         return Ratio;
     // simulate the AIG manager with combinational patterns
-    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
+    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 );
     // go through the implications and collect where they do not hold
     pResult = Fra_ObjSim( pComb, 0 );
     assert( pResult[0] == 0 );
diff --git a/src/proof/fra/fraSim.c b/src/proof/fra/fraSim.c
index 76e0a132..b85107d7 100644
--- a/src/proof/fra/fraSim.c
+++ b/src/proof/fra/fraSim.c
@@ -380,7 +380,7 @@ void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFram
 {
     unsigned * pSims;
     int i;
-    assert( Aig_ObjIsCi(pObj) );
+    assert( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) );
     pSims = Fra_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     for ( i = 0; i < p->nWordsFrame; i++ )
         pSims[i] = fConst1? ~(unsigned)0 : 0;
@@ -590,6 +590,7 @@ void Fra_SmlNodeCopyFanin( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
     fCompl  = pObj->fPhase;
     fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
     // copy information as it is
+//    if ( Aig_ObjFaninC0(pObj) )
     if ( fCompl0 )
         for ( i = 0; i < p->nWordsFrame; i++ )
             pSims[i] = ~pSims0[i];
@@ -820,6 +821,7 @@ Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFr
     p->nWordsFrame = nWordsFrame;
     p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
     p->nWordsPref  = nPref * nWordsFrame;
+    // constant 1 is initialized to 0 because we store values modulus phase (pObj->fPhase)
     return p;
 }
 
@@ -851,12 +853,157 @@ void Fra_SmlStop( Fra_Sml_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords )
+Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords, int fCheckMiter )
 {
     Fra_Sml_t * p;
     p = Fra_SmlStart( pAig, 0, 1, nWords );
     Fra_SmlInitialize( p, 0 );
     Fra_SmlSimulateOne( p );
+    if ( fCheckMiter )
+        p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads simulation patterns from file.]
+
+  Description [Each pattern contains the given number (nInputs) of binary digits.
+  No other symbols (except spaces and line endings) are allowed in the file.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Fra_SmlSimulateReadFile( char * pFileName )
+{
+    Vec_Str_t * vRes;
+    FILE * pFile;
+    int c;
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" with simulation patterns.\n", pFileName );
+        return NULL;
+    }
+    vRes = Vec_StrAlloc( 1000 );
+    while ( (c = fgetc(pFile)) != EOF )
+    {
+        if ( c == '0' || c == '1' )
+            Vec_StrPush( vRes, (char)(c - '0') );
+        else if ( c != ' ' && c != '\r' && c != '\n' && c != '\t' )
+        {
+            printf( "File \"%s\" contains symbol (%c) other than \'0\' or \'1\'.\n", c );
+            Vec_StrFreeP( &vRes );
+            break;
+        }
+    }
+    fclose( pFile );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns simulation patters derived from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_SmlInitializeGiven( Fra_Sml_t * p, Vec_Str_t * vSimInfo )
+{
+    Aig_Obj_t * pObj;
+    unsigned * pSims;
+    int i, k, nPats = Vec_StrSize(vSimInfo) / Aig_ManCiNum(p->pAig);
+    int nPatsPadded = p->nWordsTotal * 32;
+    assert( Aig_ManRegNum(p->pAig) == 0 );
+    assert( Vec_StrSize(vSimInfo) % Aig_ManCiNum(p->pAig) == 0 );
+    assert( nPats <= nPatsPadded );
+    Aig_ManForEachCi( p->pAig, pObj, i )
+    {
+        pSims = Fra_ObjSim( p, pObj->Id );
+        // clean data
+        for ( k = 0; k < p->nWordsTotal; k++ )
+            pSims[k] = 0;
+        // load patterns
+        for ( k = 0; k < nPats; k++ )
+            if ( Vec_StrEntry(vSimInfo, k * Aig_ManCiNum(p->pAig) + i) )
+                Abc_InfoSetBit( pSims, k );
+        // pad the remaining bits with the value of the last pattern
+        for ( ; k < nPatsPadded; k++ )
+            if ( Vec_StrEntry(vSimInfo, (nPats-1) * Aig_ManCiNum(p->pAig) + i) )
+                Abc_InfoSetBit( pSims, k );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints output values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_SmlPrintOutputs( Fra_Sml_t * p, int nPatterns )
+{
+    Aig_Obj_t * pObj;
+    unsigned * pSims;
+    int i, k;
+    for ( k = 0; k < nPatterns; k++ )
+    {
+        Aig_ManForEachCo( p->pAig, pObj, i )
+        {
+            pSims = Fra_ObjSim( p, pObj->Id );
+            printf( "%d", Abc_InfoHasBit( pSims, k ) );
+        }
+        printf( "\n" );               ;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns simulation patters derived from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fra_Sml_t * Fra_SmlSimulateCombGiven( Aig_Man_t * pAig, char * pFileName, int fCheckMiter, int fVerbose )
+{
+    Vec_Str_t * vSimInfo;
+    Fra_Sml_t * p;
+    int nPatterns;
+    assert( Aig_ManRegNum(pAig) == 0 );
+    // read comb patterns from file
+    vSimInfo = Fra_SmlSimulateReadFile( pFileName );
+    if ( vSimInfo == NULL )
+        return NULL;
+    if ( Vec_StrSize(vSimInfo) % Aig_ManCiNum(pAig) != 0 )
+    {
+        printf( "File \"%s\": The number of binary digits (%d) is not divisible by the number of primary inputs (%d).\n", 
+            pFileName, Vec_StrSize(vSimInfo), Aig_ManCiNum(pAig) );
+        Vec_StrFree( vSimInfo );
+        return NULL;
+    }
+    p = Fra_SmlStart( pAig, 0, 1, Abc_BitWordNum(Vec_StrSize(vSimInfo) / Aig_ManCiNum(pAig)) );
+    Fra_SmlInitializeGiven( p, vSimInfo );
+    nPatterns = Vec_StrSize(vSimInfo) / Aig_ManCiNum(pAig);
+    Vec_StrFree( vSimInfo );
+    Fra_SmlSimulateOne( p );
+    if ( fCheckMiter )
+        p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
+    if ( fVerbose )
+        Fra_SmlPrintOutputs( p, nPatterns );
     return p;
 }
 
@@ -878,7 +1025,7 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
     Fra_SmlInitialize( p, 1 );
     Fra_SmlSimulateOne( p );
     if ( fCheckMiter )
-    p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
+        p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
     return p;
 }