diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-05-07 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-05-07 08:01:00 -0700 |
| commit | 6175fcb8026bae3db5b4280b655131322d7944da (patch) | |
| tree | 41889f98814c981dcadcc5ce0f1990b74981cd49 /src/base/abci/abcDar.c | |
| parent | 436d5d2103b2cfec6a6deb5bbba72ce8e820f785 (diff) | |
| download | abc-6175fcb8026bae3db5b4280b655131322d7944da.tar.gz abc-6175fcb8026bae3db5b4280b655131322d7944da.tar.bz2 abc-6175fcb8026bae3db5b4280b655131322d7944da.zip | |
Version abc80507
Diffstat (limited to 'src/base/abci/abcDar.c')
| -rw-r--r-- | src/base/abci/abcDar.c | 33 |
1 files changed, 29 insertions, 4 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 4b1a37c2..88435e3f 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1239,7 +1239,7 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose ) +int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ) { Aig_Man_t * pMan; int RetValue; @@ -1252,7 +1252,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraig } assert( pMan->nRegs > 0 ); // perform verification - RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose ); + RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; if ( pNtk->pSeqModel ) { @@ -1274,7 +1274,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraig SeeAlso [] ***********************************************************************/ -int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose ) +int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ) { // Fraig_Params_t Params; Aig_Man_t * pMan; @@ -1346,7 +1346,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim assert( pMan->nRegs > 0 ); // perform verification - RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose ); + RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose ); Aig_ManStop( pMan ); return RetValue; } @@ -1909,6 +1909,31 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in return pNtkAig; } +/**Function************************************************************* + + Synopsis [Performs BDD-based reachability analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ) +{ + extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ); + Aig_Man_t * pMan; + pMan = Abc_NtkToDar( pNtk, 0, 0 ); + pMan->nRegs = Abc_NtkLatchNum(pNtk); + pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); + pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); + if ( pMan == NULL ) + return; + Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); + Aig_ManStop( pMan ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |