| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/abci/ |
| H A D | abcReach.c | 141 …tk_t * pNtk, DdNode ** pbParts, DdNode * bInitial, DdNode * bOutput, int nBddMax, int nIterMax, in… in Abc_NtkComputeReachable() argument
189 if ( nBddSize > nBddMax ) in Abc_NtkComputeReachable()
235 if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax ) in Abc_NtkComputeReachable()
244 if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax ) in Abc_NtkComputeReachable()
261 void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReor… in Abc_NtkVerifyUsingBdds() argument
274 dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, 0, fVerbose ); in Abc_NtkVerifyUsingBdds()
277 printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax ); in Abc_NtkVerifyUsingBdds()
298 …bReached = Abc_NtkComputeReachable( dd, pNtk, pbParts, bInitial, bOutput, nBddMax, nIterMax, fPart… in Abc_NtkVerifyUsingBdds()
|
| H A D | abc.c | 11397 pPars->nBddMax = atoi(argv[globalUtilOptind]); in Abc_CommandReach()
11399 if ( pPars->nBddMax < 0 ) in Abc_CommandReach()
24458 if ( pSecPar->nBddMax < 0 ) in Abc_CommandDProve()
40920 pPars->nBddMax = atoi(argv[globalUtilOptind]); in Abc_CommandAbc9ReachM()
40922 if ( pPars->nBddMax < 0 ) in Abc_CommandAbc9ReachM()
41100 pPars->nBddMax = atoi(argv[globalUtilOptind]); in Abc_CommandAbc9ReachP()
41102 if ( pPars->nBddMax < 0 ) in Abc_CommandAbc9ReachP()
41239 pPars->nBddMax = atoi(argv[globalUtilOptind]); in Abc_CommandAbc9ReachN()
41241 if ( pPars->nBddMax < 0 ) in Abc_CommandAbc9ReachN()
41359 pPars->nBddMax = 100; in Abc_CommandAbc9ReachY()
[all …]
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/bdd/bbr/ |
| H A D | bbrReach.c | 53 p->nBddMax = 50000; in Bbr_ManSetDefaultParams()
261 …RegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->nBddMax, pPars->fVerbose … in Aig_ManComputeReachable()
328 if ( nBddSize > pPars->nBddMax ) in Aig_ManComputeReachable()
402 if ( nIters > pPars->nIterMax || nBddSize > pPars->nBddMax ) in Aig_ManComputeReachable()
420 assert(nIters >= pPars->nIterMax || nBddSize >= pPars->nBddMax); in Aig_ManComputeReachable()
451 dd = Aig_ManComputeGlobalBdds( p, pPars->nBddMax, 1, pPars->fReorder, pPars->fVerbose ); in Aig_ManVerifyUsingBdds_int()
455 … printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", pPars->nBddMax ); in Aig_ManVerifyUsingBdds_int()
|
| H A D | bbrImage.c | 55 int nBddMax; // the number of node to stop member
121 int nVars, Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax );
171 …int nVars, DdNode ** pbVars, int nBddMax, int fVerbose ) // the NS and parameter variables (not … in Bbr_bddImageStart() argument
189 while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop, nBddMax ) ); in Bbr_bddImageStart()
218 pTree->nBddMax = nBddMax; in Bbr_bddImageStart()
705 if ( dd->keys-dd->dead > (unsigned)pTree->nBddMax ) in Bbr_bddImageCompute_rec()
723 int nVars, Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax ) in Bbr_BuildTreeNode() argument
830 if ( dd->keys-dd->dead > (unsigned)nBddMax ) in Bbr_BuildTreeNode()
|
| H A D | bbr.h | 62 int nVars, DdNode ** pbVars, int nBddMax, int fVerbose );
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/bdd/llb/ |
| H A D | llb.h | 44 int nBddMax; // maximum BDD size member
|
| H A D | llb4Cluster.c | 390 … * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose ) in Llb_Nonlin4Cluster() argument
406 vGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, nBddMax ); in Llb_Nonlin4Cluster()
|
| H A D | llb1Core.c | 49 p->nBddMax = 10000000; in Llb_ManSetDefaultParams()
|
| H A D | llb1Reach.c | 781 if ( nBddSize > p->pPars->nBddMax ) in Llb_ManReachability()
868 if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax ) in Llb_ManReachability()
875 if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax ) in Llb_ManReachability()
|
| H A D | llb3Nonlin.c | 665 if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax ) in Llb_NonlinReachability()
672 if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax ) in Llb_NonlinReachability()
|
| H A D | llb4Nonlin.c | 954 …Llb4_Nonlin4Sweep( p->pAig, pPars->nBddMax, pPars->nClusterMax, &p->dd, &p->vOrder, &p->vRoots, pP… in Llb_MnxStart()
1122 pPars->nBddMax = 100; in Llb_ReachableStates()
|
| H A D | llb2Flow.c | 1301 p->nBddMax = 1000000; in Llb_BddSetDefaultParams()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/fra/ |
| H A D | fraSec.c | 61 p->nBddMax = 50000; // the limit on the number of BDD nodes in Fra_SecSetDefaultParams()
577 pPars->nBddMax = pParSec->nBddMax; in Fra_FraigSec()
|
| H A D | fra.h | 123 int nBddMax; // the max number of BDD nodes member
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/saig/ |
| H A D | saig.h | 57 int nBddMax; member
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/abs/ |
| H A D | absOldRef.c | 193 pPars->nBddMax = 1000000; in Saig_ManCexRefine()
|