Home
last modified time | relevance | path

Searched refs:nBddVarsMax (Results 1 – 3 of 3) sorted by relevance

/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/fra/
H A DfraSec.c60 p->nBddVarsMax = 150; // the limit on the number of registers in BDD reachability in Fra_SecSetDefaultParams()
572 …bility && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < pParSec->nBddVarsMax ) in Fra_FraigSec()
H A Dfra.h122 int nBddVarsMax; // the state space limit for BDD reachability member
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/abci/
H A Dabc.c24445 pSecPar->nBddVarsMax = atoi(argv[globalUtilOptind]); in Abc_CommandDProve()
24447 if ( pSecPar->nBddVarsMax < 0 ) in Abc_CommandDProve()
24576 …t-V num : the flop count limit for BDD-based reachablity [default = %d]\n", pSecPar->nBddVarsMax ); in Abc_CommandDProve()