summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-07-31 20:22:57 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2011-07-31 20:22:57 +0700
commit0d65c49048eea6940e3f5fa9bbf28ee5c6b97102 (patch)
tree993f3276ed0eedace7c00b886a9a3519d87baa5a /src/base
parentd5955db9604a2eb9224941b5200648120b22fc82 (diff)
downloadabc-0d65c49048eea6940e3f5fa9bbf28ee5c6b97102.tar.gz
abc-0d65c49048eea6940e3f5fa9bbf28ee5c6b97102.tar.bz2
abc-0d65c49048eea6940e3f5fa9bbf28ee5c6b97102.zip
Improvements to 'bmc3' (start frame; stop when all POs are SAT; stop when 2^nRegs frames are completed).
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abcDar.c10
1 files changed, 4 insertions, 6 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index c0822ba9..064529cc 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1805,8 +1805,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( RetValue == 1 )
{
-// printf( "No output asserted in %d frames. ", pPars->iFrame );
- printf( "Incorrect return value. " );
+ printf( "Explored all reachable states after completing %d frames. ", 1<<Aig_ManRegNum(pMan) );
}
else if ( RetValue == -1 )
{
@@ -1839,8 +1838,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
}
else
{
- printf( "Incorrect return value. " );
-// printf( "At least one output asserted (out=%d, frame=%d). ", pCex->iPo, pCex->iFrame );
+ printf( "All %d outputs are proved SAT. ", Saig_ManPoNum(pMan) - pMan->nConstrs );
}
}
ABC_PRT( "Time", clock() - clk );
@@ -3044,8 +3042,8 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
}
else
{
- printf( "Simulation of %d frames with %d words did not assert the outputs. ",
- nFrames, nWords );
+// printf( "Simulation of %d frames with %d words did not assert the outputs. ",
+// nFrames, nWords );
}
ABC_PRT( "Time", clock() - clk );
Aig_ManStop( pMan );