diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-07-30 13:37:02 +0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-07-30 13:37:02 +0700 |
commit | c60852f4a935f72bb399414853b130eb49b79804 (patch) | |
tree | 74a27300f7a63699d0908ecd667a5528c916b360 /src/base/abci | |
parent | 2ea0ded0bced0c24ed3ec498ca8d7701315b7408 (diff) | |
download | abc-c60852f4a935f72bb399414853b130eb49b79804.tar.gz abc-c60852f4a935f72bb399414853b130eb49b79804.tar.bz2 abc-c60852f4a935f72bb399414853b130eb49b79804.zip |
Changes to enable smarter simulation.
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 8 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 48 |
2 files changed, 5 insertions, 51 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e319c4f8..ee0c98ff 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -24776,7 +24776,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) 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 ); + extern int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ); // set defaults nFrames = 20; nWords = 50; @@ -24871,7 +24871,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) 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->Status = Ssw_RarSimulateGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ); // pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; @@ -25310,7 +25310,7 @@ usage: int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) { // 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 ); + extern int Ssw_RarSignalFilterGia( 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; @@ -25435,7 +25435,7 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) } } // if ( fNewAlgo ) - pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); + pAbc->Status = Ssw_RarSignalFilterGia( 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; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 4232ab1f..695ae4ef 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -3027,53 +3027,7 @@ int Abc_NtkDarSeqSim3( 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_RarSimulate2( pMan, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ) == 0 ) - { - 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 [Performs random simulation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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 ) -{ - 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_RarSignalFilter( pMan, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose ) == 0 ) + if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ) == 0 ) { if ( pMan->pSeqModel ) { |