diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-07-21 17:55:44 +0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-07-21 17:55:44 +0700 |
commit | 9a2a0f2912e296e866ba220dce6ccf25018cf29b (patch) | |
tree | 54ea0dae7c4d13a67db0a7b509e738d1e50acb17 /src/base/abci/abcDar.c | |
parent | 515835579ede817bcab09ee67b32ff4f7acaae32 (diff) | |
download | abc-9a2a0f2912e296e866ba220dce6ccf25018cf29b.tar.gz abc-9a2a0f2912e296e866ba220dce6ccf25018cf29b.tar.bz2 abc-9a2a0f2912e296e866ba220dce6ccf25018cf29b.zip |
Changes to enable smarter simulation.
Diffstat (limited to 'src/base/abci/abcDar.c')
-rw-r--r-- | src/base/abci/abcDar.c | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 97ee8c42..ff8aac38 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -3009,6 +3009,52 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in /**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.] Description [] |