luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

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

This commit is contained in:
Alan Mishchenko 2012-08-24 11:12:51 -07:00
parent 12c776ed6e
commit 942600414d
8 changed files with 206 additions and 140 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
src/base/abci/abc.c
View File

@ -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;
}

128
src/base/abci/abcDar.c
View File

@ -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 );

2
src/opt/mfs/mfsStrash.c
View File

@ -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 );

3
src/proof/fra/fra.h
View File

@ -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 );

2
src/proof/fra/fraClass.c
View File

@ -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) );

6
src/proof/fra/fraClaus.c
View File

@ -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 );

6
src/proof/fra/fraImp.c
View File

@ -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 );

153
src/proof/fra/fraSim.c
View File

@ -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;
}