diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-05-11 20:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-05-11 20:01:00 -0700 |
commit | 47036e1e44fb5f4e1948cdc26ab10254ccaa161d (patch) | |
tree | 93ad0800fd9f38ea6a2732e0cf3a68412734efc5 /src/aig | |
parent | 582cf0b923e0a461c2efdb4ecde9bfdb0716a328 (diff) | |
download | abc-47036e1e44fb5f4e1948cdc26ab10254ccaa161d.tar.gz abc-47036e1e44fb5f4e1948cdc26ab10254ccaa161d.tar.bz2 abc-47036e1e44fb5f4e1948cdc26ab10254ccaa161d.zip |
Version abc80511_2
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/fra/fra.h | 5 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 17 | ||||
-rw-r--r-- | src/aig/fra/fraLcr.c | 15 | ||||
-rw-r--r-- | src/aig/fra/fraSec.c | 91 | ||||
-rw-r--r-- | src/aig/ntl/ntlFraig.c | 2 | ||||
-rw-r--r-- | src/aig/saig/saigInter.c | 2 |
6 files changed, 120 insertions, 12 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 7311d414..f7ad40dd 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -104,6 +104,7 @@ struct Fra_Ssw_t_ int fUse1Hot; // use one-hotness constraints int fVerbose; // enable verbose output int nIters; // the number of iterations performed + float TimeLimit; // the runtime budget for this call }; // FRAIG equivalence classes @@ -312,7 +313,7 @@ extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars /*=== fraIndVer.c =====================================================*/ extern int Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits ); /*=== fraLcr.c ========================================================*/ -extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter ); +extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); @@ -328,7 +329,7 @@ extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ); extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); /*=== fraSec.c ========================================================*/ -extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ); +extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit ); /*=== fraSim.c ========================================================*/ extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ); extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ); diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index b29fa946..99b62856 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -336,9 +336,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams ) Fra_Par_t Pars, * pPars = &Pars; Aig_Obj_t * pObj; Cnf_Dat_t * pCnf; - Aig_Man_t * pManAigNew; + Aig_Man_t * pManAigNew = NULL; int nNodesBeg, nRegsBeg; int nIter, i, clk = clock(), clk2; + int TimeToStop = (pParams->TimeLimit == 0.0)? 0 : clock() + (int)(pParams->TimeLimit * CLOCKS_PER_SEC); if ( Aig_ManNodeNum(pManAig) == 0 ) { @@ -419,6 +420,12 @@ PRT( "Time", clock() - clk ); if ( pPars->fUseImps ) p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr ); + if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop ) + { + printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" ); + goto finish; + } + // perform BMC (for the min number of frames) Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement //Fra_ClassesPrint( p->pCla, 1 ); @@ -442,6 +449,13 @@ PRT( "Time", clock() - clk ); int nLitsOld = Fra_ClassesCountLits(p->pCla); int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0; int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0; + + if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop ) + { + printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" ); + goto finish; + } + // mark the classes as non-refined p->pCla->fRefinement = 0; // derive non-init K-timeframes while implementing e-classes @@ -592,6 +606,7 @@ p->timeTotal = clock() - clk; p->nNodesEnd = Aig_ManNodeNum(pManAigNew); p->nRegsEnd = Aig_ManRegNum(pManAigNew); // free the manager +finish: Fra_ManStop( p ); // check the output // if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 ) diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c index 145bafae..0f5cc207 100644 --- a/src/aig/fra/fraLcr.c +++ b/src/aig/fra/fraLcr.c @@ -526,7 +526,7 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter ) +Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit ) { int nPartSize = 200; int fReprSelect = 0; @@ -536,6 +536,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC Aig_Man_t * pAigPart, * pAigNew = NULL; Vec_Int_t * vPart; int i, nIter, timeSim, clk = clock(), clk2, clk3; + int TimeToStop = (TimeLimit == 0.0)? 0 : clock() + (int)(TimeLimit * CLOCKS_PER_SEC); if ( Aig_ManNodeNum(pAig) == 0 ) { if ( pnIter ) *pnIter = 0; @@ -609,6 +610,15 @@ p->timePart += clock() - clk2; Vec_PtrClear( p->vFraigs ); Vec_PtrForEachEntry( p->vParts, vPart, i ) { + if ( TimeLimit != 0.0 && clock() > TimeToStop ) + { + Vec_PtrForEachEntry( p->vFraigs, pAigPart, i ) + Aig_ManStop( pAigPart ); + Aig_ManCleanMarkA( pAig ); + Aig_ManCleanMarkB( pAig ); + printf( "Fra_FraigLatchCorrespondence(): Runtime limit exceeded.\n" ); + goto finish; + } clk2 = clock(); pAigPart = Fra_LcrCreatePart( p, vPart ); p->timeTrav += clock() - clk2; @@ -649,7 +659,6 @@ clk2 = clock(); p->timePart += clock() - clk2; } } - free( pTemp ); p->nIters = nIter; // move the classes into representatives and reduce AIG @@ -667,6 +676,8 @@ p->timeTotal = clock() - clk; p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); p->nNodesEnd = Aig_ManNodeNum(pAigNew); p->nRegsEnd = Aig_ManRegNum(pAigNew); +finish: + free( pTemp ); Lcr_ManFree( p ); if ( pnIter ) *pnIter = nIter; return pAigNew; diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 9a500680..5146344c 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -40,13 +40,14 @@ SeeAlso [] ***********************************************************************/ -int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ) +int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit ) { Fra_Ssw_t Pars, * pPars = &Pars; Fra_Sml_t * pSml; Aig_Man_t * pNew, * pTemp; int nFrames, RetValue, nIter, clk, clkTotal = clock(); int fLatchCorr = 0; + float TimeLeft = 0.0; // try the miter before solving pNew = Aig_ManDup( p ); @@ -119,7 +120,24 @@ clk = clock(); pNew = Aig_ManDupOrdered( pTemp = pNew ); // pNew = Aig_ManDupDfs( pTemp = pNew ); Aig_ManStop( pTemp ); - pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter ); + if ( TimeLimit ) + { + TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); + TimeLeft = AIG_MAX( TimeLeft, 0.0 ); + if ( TimeLeft == 0.0 ) + { + printf( "Runtime limit exceeded.\n" ); + RetValue = -1; + goto finish; + } + } + pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter, TimeLeft ); + if ( pNew == NULL ) + { + pNew = pTemp; + RetValue = -1; + goto finish; + } p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL; Aig_ManStop( pTemp ); if ( pNew == NULL ) @@ -138,6 +156,18 @@ PRT( "Time", clock() - clk ); } } + if ( TimeLimit ) + { + TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); + TimeLeft = AIG_MAX( TimeLeft, 0.0 ); + if ( TimeLeft == 0.0 ) + { + printf( "Runtime limit exceeded.\n" ); + RetValue = -1; + goto finish; + } + } + // perform fraiging if ( fFraiging ) { @@ -159,6 +189,18 @@ PRT( "Time", clock() - clk ); if ( RetValue >= 0 ) goto finish; + if ( TimeLimit ) + { + TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); + TimeLeft = AIG_MAX( TimeLeft, 0.0 ); + if ( TimeLeft == 0.0 ) + { + printf( "Runtime limit exceeded.\n" ); + RetValue = -1; + goto finish; + } + } + // perform min-area retiming if ( fRetimeRegs && pNew->nRegs ) { @@ -184,9 +226,28 @@ PRT( "Time", clock() - clk ); if ( RetValue == -1 ) for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 ) { + if ( TimeLimit ) + { + TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); + TimeLeft = AIG_MAX( TimeLeft, 0.0 ); + if ( TimeLeft == 0.0 ) + { + printf( "Runtime limit exceeded.\n" ); + RetValue = -1; + goto finish; + } + } + clk = clock(); pPars->nFramesK = nFrames; + pPars->TimeLimit = TimeLeft; pNew = Fra_FraigInduction( pTemp = pNew, pPars ); + if ( pNew == NULL ) + { + pNew = pTemp; + RetValue = -1; + goto finish; + } Aig_ManStop( pTemp ); RetValue = Fra_FraigMiterStatus( pNew ); if ( fVerbose ) @@ -264,11 +325,33 @@ PRT( "Time", clock() - clkTotal ); // get the miter status RetValue = Fra_FraigMiterStatus( pNew ); + // try interplation +clk = clock(); + if ( RetValue == -1 && Aig_ManRegNum(pNew) > 0 ) + { + extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth ); + int Depth; + pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); + RetValue = Saig_Interpolate( pNew, 10000, 0, 1, 0, &Depth ); + if ( fVerbose ) + { + if ( RetValue == 1 ) + printf( "Property proved using interpolation. " ); + else if ( RetValue == 0 ) + printf( "Property DISPROVED with cex at depth %d using interpolation. ", Depth ); + else if ( RetValue == -1 ) + printf( "Property UNDECIDED after interpolation. " ); + else + assert( 0 ); +PRT( "Time", clock() - clk ); + } + } + // try reachability analysis - if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 ) + if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 && Aig_ManRegNum(pNew) > 0 ) { extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ); - assert( Aig_ManRegNum(pNew) > 0 ); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 ); diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index a723c981..1b135212 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -347,7 +347,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose ) // perform SCL for the given design pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p)); - pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL ); + pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 ); Aig_ManStop( pTemp ); // finalize the transformation diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c index ffd32206..c3bb0875 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -519,8 +519,6 @@ int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTrans p->pAigTrans = Saig_ManTransformed( pAig ); else p->pAigTrans = Saig_ManDuplicated( pAig ); -// p->pAigTrans = Dar_ManRwsat( pAigTemp = p->pAigTrans, 1, 0 ); -// Aig_ManStop( pAigTemp ); // derive CNF for the transformed AIG clk = clock(); p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) ); |