diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-04-11 09:22:03 +0900 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-04-11 09:22:03 +0900 |
commit | 96c622b3bc61584580e28b6b9ba5c8de2a9a1e2b (patch) | |
tree | 9946f530ff0ebf64bee3e14caf1c189334ca605b /src | |
parent | dff6e2ab3162b33b309d20a8c8bde07e6a5590ac (diff) | |
download | abc-96c622b3bc61584580e28b6b9ba5c8de2a9a1e2b.tar.gz abc-96c622b3bc61584580e28b6b9ba5c8de2a9a1e2b.tar.bz2 abc-96c622b3bc61584580e28b6b9ba5c8de2a9a1e2b.zip |
Making BDD computation more robust by using dynamic resource limit.
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abcNtbdd.c | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index 9eedfde6..508d1741 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -367,7 +367,7 @@ void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInter DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose ) { DdNode * bFunc, * bFunc0, * bFunc1, * bFuncC; - int fDetectMuxes = 1; + int fDetectMuxes = 0; assert( !Abc_ObjIsComplement(pNode) ); if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax ) { @@ -438,7 +438,10 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize bFunc0 = Cudd_NotCond( bFunc0, (int)Abc_ObjFaninC0(pNode) ); bFunc1 = Cudd_NotCond( bFunc1, (int)Abc_ObjFaninC1(pNode) ); // get the final result - bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); + bFunc = Cudd_bddAndLimit( dd, bFunc0, bFunc1, nBddSizeMax ); + if ( bFunc == NULL ) + return NULL; + Cudd_Ref( bFunc ); Cudd_RecursiveDeref( dd, bFunc0 ); Cudd_RecursiveDeref( dd, bFunc1 ); // add the number of used nodes |