From f74fb87dae78ecc87dd8f4929c5ca3d00701d47b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 8 Feb 2011 12:45:28 -0800 Subject: Improved timeout in &reachp. --- src/aig/llb/llb2Core.c | 122 +++++++++++++++++++++++++++++++++++++++-------- src/aig/llb/llb2Driver.c | 14 +++++- src/aig/llb/llb2Image.c | 43 +++++++++++++---- src/aig/llb/llbInt.h | 4 +- 4 files changed, 150 insertions(+), 33 deletions(-) (limited to 'src/aig/llb') diff --git a/src/aig/llb/llb2Core.c b/src/aig/llb/llb2Core.c index 45add7e9..7fa361b9 100644 --- a/src/aig/llb/llb2Core.c +++ b/src/aig/llb/llb2Core.c @@ -207,22 +207,35 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ int * pGlo2Loc = p->pPars->fBackward? Vec_IntArray( p->vGlo2Ns ) : Vec_IntArray( p->vGlo2Cs ); DdNode * bCurrent, * bReached, * bNext, * bTemp; int clk2, clk = clock(), nIters, nBddSize, iOutFail = -1; - +/* // compute time to stop if ( p->pPars->TimeLimit ) p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC; else p->pPars->TimeTarget = 0; +*/ + + if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit ); + return -1; + } + + // set the stop time parameter + p->dd->TimeStop = p->pPars->TimeTarget; + p->ddG->TimeStop = p->pPars->TimeTarget; + p->ddR->TimeStop = p->pPars->TimeTarget; // compute initial states if ( p->pPars->fBackward ) { // create init state in the global manager - bTemp = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeLimit ); + bTemp = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget ); if ( bTemp == NULL ) { if ( !p->pPars->fSilent ) - printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit ); + printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit ); return -1; } Cudd_Ref( bTemp ); @@ -238,11 +251,11 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ else { // create bad state in the ring manager - p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeLimit ); + p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget ); if ( p->ddR->bFunc == NULL ) { if ( !p->pPars->fSilent ) - printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit ); + printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit ); return -1; } if ( p->ddR->bFunc == NULL ) @@ -263,7 +276,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget ) { if ( !p->pPars->fSilent ) - printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit ); + printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit ); p->pPars->iFrame = nIters - 1; Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; @@ -300,7 +313,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ if ( bNext == NULL ) { if ( !p->pPars->fSilent ) - printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit ); + printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit ); p->pPars->iFrame = nIters - 1; Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; @@ -311,10 +324,23 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ //Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" ); // remap these states into the global manager - bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo ); Cudd_Ref( bNext ); - Cudd_RecursiveDeref( p->dd, bTemp ); - nBddSize = Cudd_DagSize(bNext); +// bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo ); Cudd_Ref( bNext ); +// Cudd_RecursiveDeref( p->dd, bTemp ); + bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pLoc2Glo, p->pPars->TimeTarget ); + if ( bNext == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit ); + p->pPars->iFrame = nIters - 1; + Cudd_RecursiveDeref( p->dd, bTemp ); + Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; + return -1; + } + Cudd_Ref( bNext ); + Cudd_RecursiveDeref( p->dd, bTemp ); + + nBddSize = Cudd_DagSize(bNext); // check if there are any new states if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states { @@ -324,8 +350,22 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ // get the new states bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); + // remap these states into the current state vars - bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc ); Cudd_Ref( bCurrent ); +// bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc ); Cudd_Ref( bCurrent ); +// Cudd_RecursiveDeref( p->ddG, bTemp ); + + bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc, p->pPars->TimeTarget ); + if ( bCurrent == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n", p->pPars->TimeLimit ); + p->pPars->iFrame = nIters - 1; + Cudd_RecursiveDeref( p->ddG, bTemp ); + Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; + return -1; + } + Cudd_Ref( bCurrent ); Cudd_RecursiveDeref( p->ddG, bTemp ); // add to the reached states @@ -449,7 +489,7 @@ int Llb_CoreReachability( Llb_Img_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t * vVarsNs ) +Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t * vVarsNs, int TimeTarget ) { DdManager * dd; Vec_Ptr_t * vDdMans; @@ -459,9 +499,22 @@ Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t Vec_PtrForEachEntryReverse( Vec_Ptr_t *, vResult, vLower, i ) { if ( i < Vec_PtrSize(vResult) - 1 ) - dd = Llb_ImgPartition( p, vLower, vUpper ); + dd = Llb_ImgPartition( p, vLower, vUpper, TimeTarget ); else - dd = Llb_DriverLastPartition( p, vVarsNs ); + dd = Llb_DriverLastPartition( p, vVarsNs, TimeTarget ); + if ( dd == NULL ) + { + Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i ) + { + if ( dd == NULL ) + continue; + if ( dd->bFunc ) + Cudd_RecursiveDeref( dd, dd->bFunc ); + Extra_StopManager( dd ); + } + Vec_PtrFree( vDdMans ); + return NULL; + } Vec_PtrWriteEntry( vDdMans, i, dd ); vUpper = vLower; } @@ -557,6 +610,7 @@ void Llb_CoreStop( Llb_Img_t * p ) DdManager * dd; DdNode * bTemp; int i; + if ( p->vDdMans ) Vec_PtrForEachEntry( DdManager *, p->vDdMans, dd, i ) { if ( dd->bFunc ) @@ -565,7 +619,7 @@ void Llb_CoreStop( Llb_Img_t * p ) Cudd_RecursiveDeref( dd, dd->bFunc2 ); Extra_StopManager( dd ); } - Vec_PtrFree( p->vDdMans ); + Vec_PtrFreeP( &p->vDdMans ); if ( p->ddR->bFunc ) Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc ); Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i ) @@ -595,14 +649,21 @@ void Llb_CoreStop( Llb_Img_t * p ) SeeAlso [] ***********************************************************************/ -int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult ) +int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, int TimeTarget ) { int RetValue; Llb_Img_t * p; // printf( "\n" ); // pPars->fVerbose = 1; p = Llb_CoreStart( pInit, pAig, pPars ); - p->vDdMans = Llb_CoreConstructAll( pAig, vResult, p->vVarsNs ); + p->vDdMans = Llb_CoreConstructAll( pAig, vResult, p->vVarsNs, TimeTarget ); + if ( p->vDdMans == NULL ) + { + if ( !pPars->fSilent ) + printf( "Reached timeout (%d seconds) while deriving the partitions.\n", pPars->TimeLimit ); + Llb_CoreStop( p ); + return -1; + } RetValue = Llb_CoreReachability( p ); Llb_CoreStop( p ); return RetValue; @@ -625,6 +686,13 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) Vec_Ptr_t * vResult; Aig_Man_t * p; int RetValue = -1; + int clk = clock(); + + // compute time to stop + if ( pPars->TimeLimit ) + pPars->TimeTarget = clock() + pPars->TimeLimit * CLOCKS_PER_SEC; + else + pPars->TimeTarget = 0; p = Aig_ManDupFlopsOnly( pAig ); //Aig_ManShow( p, 0, NULL ); @@ -635,13 +703,29 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) Aig_ManFanoutStart( p ); vResult = Llb_ManComputeCuts( p, pPars->nPartValue, pPars->fVerbose, pPars->fVeryVerbose ); + + if ( pPars->TimeLimit && clock() >= pPars->TimeTarget ) + { + if ( !pPars->fSilent ) + printf( "Reached timeout (%d seconds) after partitioning.\n", pPars->TimeLimit ); + + Vec_VecFree( (Vec_Vec_t *)vResult ); + Aig_ManFanoutStop( p ); + Aig_ManCleanMarkAB( p ); + Aig_ManStop( p ); + return RetValue; + } + if ( !pPars->fSkipReach ) - RetValue = Llb_CoreExperiment( pAig, p, pPars, vResult ); - Vec_VecFree( (Vec_Vec_t *)vResult ); + RetValue = Llb_CoreExperiment( pAig, p, pPars, vResult, pPars->TimeTarget ); + Vec_VecFree( (Vec_Vec_t *)vResult ); Aig_ManFanoutStop( p ); Aig_ManCleanMarkAB( p ); Aig_ManStop( p ); + + if ( RetValue == -1 ) + Abc_PrintTime( 1, "Total runtime of the min-cut-based reachability engine", clock() - clk ); return RetValue; } diff --git a/src/aig/llb/llb2Driver.c b/src/aig/llb/llb2Driver.c index 0115e51e..aab65317 100644 --- a/src/aig/llb/llb2Driver.c +++ b/src/aig/llb/llb2Driver.c @@ -157,7 +157,7 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager SeeAlso [] ***********************************************************************/ -DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs ) +DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int TimeTarget ) { int fVerbose = 1; DdManager * dd; @@ -166,6 +166,7 @@ DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs ) int i; dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + dd->TimeStop = TimeTarget; bRes = Cudd_ReadOne(dd); Cudd_Ref( bRes ); // mark the duplicated flop inputs @@ -179,7 +180,15 @@ DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs ) bVar2 = Cudd_ReadOne(dd); bVar2 = Cudd_NotCond( bVar2, Aig_ObjFaninC0(pObj) ); bProd = Cudd_bddXnor( dd, bVar1, bVar2 ); Cudd_Ref( bProd ); - bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes ); +// bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes ); + bRes = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bProd ); + return NULL; + } + Cudd_Ref( bRes ); Cudd_RecursiveDeref( dd, bTemp ); Cudd_RecursiveDeref( dd, bProd ); } @@ -196,6 +205,7 @@ DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs ) // Cudd_RecursiveDeref( dd, bRes ); // Extra_StopManager( dd ); dd->bFunc = bRes; + dd->TimeStop = 0; return dd; } diff --git a/src/aig/llb/llb2Image.c b/src/aig/llb/llb2Image.c index afe99051..78ff9da1 100644 --- a/src/aig/llb/llb2Image.c +++ b/src/aig/llb/llb2Image.c @@ -179,7 +179,7 @@ void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pv SeeAlso [] ***********************************************************************/ -DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper ) +DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, int TimeTarget ) { Vec_Ptr_t * vNodes, * vRange; Aig_Obj_t * pObj; @@ -189,6 +189,7 @@ DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUp dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + dd->TimeStop = TimeTarget; Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i ) pObj->pData = Cudd_bddIthVar( dd, Aig_ObjId(pObj) ); @@ -198,7 +199,15 @@ DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUp { bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); - pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData ); +// pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData ); + pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeTarget ); + if ( pObj->pData == NULL ) + { + Cudd_Quit( dd ); + Vec_PtrFree( vNodes ); + return NULL; + } + Cudd_Ref( (DdNode *)pObj->pData ); } vRange = Llb_ManCutRange( p, vLower, vUpper ); @@ -207,7 +216,16 @@ DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUp { assert( Aig_ObjIsNode(pObj) ); bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData ); Cudd_Ref( bProd ); - bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes ); +// bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes ); + bRes = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget ); + if ( bRes == NULL ) + { + Cudd_Quit( dd ); + Vec_PtrFree( vRange ); + Vec_PtrFree( vNodes ); + return NULL; + } + Cudd_Ref( bRes ); Cudd_RecursiveDeref( dd, bTemp ); Cudd_RecursiveDeref( dd, bProd ); } @@ -220,6 +238,7 @@ DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUp // Cudd_RecursiveDeref( dd, bRes ); // Extra_StopManager( dd ); dd->bFunc = bRes; + dd->TimeStop = 0; return dd; } @@ -373,7 +392,17 @@ if ( fVerbose ) printf( "Pt0 =%6d. Pt1 =%6d. ", Cudd_DagSize(ddPart->bFunc), Cudd_DagSize(bGroup) ); // perform partial product bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant1, i+1), dd ); Cudd_Ref( bCube ); - bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube ); Cudd_Ref( bImage ); +// bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube ); + bImage = Extra_bddAndAbstractTime( dd, bTemp = bImage, bGroup, bCube, TimeTarget ); + if ( bImage == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bCube ); + Cudd_RecursiveDeref( dd, bGroup ); + return NULL; + } + Cudd_Ref( bImage ); + if ( fVerbose ) printf( "Im0 =%6d. Im1 =%6d. ", Cudd_DagSize(bTemp), Cudd_DagSize(bImage) ); //printf("\n"); Extra_bddPrintSupport(dd, bImage); printf("\n"); @@ -384,12 +413,6 @@ printf( "Im0 =%6d. Im1 =%6d. ", Cudd_DagSize(bTemp), Cudd_DagSize(bImage) ); // Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); // Abc_Print( 1, "Reo =%6d. ", Cudd_DagSize(bImage) ); - // chech runtime - if ( TimeTarget && clock() >= TimeTarget ) - { - Cudd_RecursiveDeref( dd, bImage ); - return NULL; - } if ( fVerbose ) printf( "Supp =%3d. ", Cudd_SupportSize(dd, bImage) ); if ( fVerbose ) diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h index 1294438e..3ee1f5c2 100644 --- a/src/aig/llb/llbInt.h +++ b/src/aig/llb/llbInt.h @@ -155,11 +155,11 @@ extern Vec_Int_t * Llb_DriverCountRefs( Aig_Man_t * p ); extern Vec_Int_t * Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs ); extern Vec_Int_t * Llb_DriverCollectCs( Aig_Man_t * pAig ); extern DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager * dd ); -extern DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs ); +extern DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int TimeTarget ); /*=== llb2Image.c ======================================================*/ extern Vec_Ptr_t * Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vStart, Vec_Int_t * vStop, int fAddPis, int fVerbose ); extern void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose ); -extern DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper ); +extern DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, int TimeTarget ); extern void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQuant0, int fVerbose ); extern void Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans ); extern DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit, -- cgit v1.2.3