diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-18 14:38:02 +0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-18 14:38:02 +0700 |
commit | b71b5bbc233492321566551b7b5a69d99beaa297 (patch) | |
tree | 7f9035b43eea4ebd860a401ce5cdbdd08e12c586 /src/aig/saig | |
parent | 48ae2c448f66b9d4462472a5bc62924730612535 (diff) | |
download | abc-b71b5bbc233492321566551b7b5a69d99beaa297.tar.gz abc-b71b5bbc233492321566551b7b5a69d99beaa297.tar.bz2 abc-b71b5bbc233492321566551b7b5a69d99beaa297.zip |
Bug fix in CBA and PBA.
Diffstat (limited to 'src/aig/saig')
-rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
-rw-r--r-- | src/aig/saig/saigAbsCba.c | 5 | ||||
-rw-r--r-- | src/aig/saig/saigAbsPba.c | 19 | ||||
-rw-r--r-- | src/aig/saig/saigAbsStart.c | 4 |
4 files changed, 18 insertions, 12 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 505fd6ee..fa68bf95 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -135,7 +135,7 @@ extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t extern Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ); extern Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars ); /*=== sswAbsPba.c ==========================================================*/ -extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose, int * piFrame ); +extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame ); /*=== sswAbsStart.c ==========================================================*/ extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ); extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ); diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c index 02d01852..f79cbf09 100644 --- a/src/aig/saig/saigAbsCba.c +++ b/src/aig/saig/saigAbsCba.c @@ -609,7 +609,7 @@ ABC_PRT( "Time", clock() - clk ); ***********************************************************************/ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * pPars ) -{ +{ Vec_Int_t * vAbsFfsToAdd; int RetValue, clk = clock(); // assert( pAbs->nRegs > 0 ); @@ -617,6 +617,7 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p RetValue = Saig_ManBmcScalable( pAbs, pPars ); if ( RetValue == -1 ) // time out - nothing to add { + printf( "Resource limit is reached during BMC.\n" ); assert( pAbs->pSeqModel == NULL ); return Vec_IntAlloc( 0 ); } @@ -631,7 +632,7 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p } if ( pPars->fVerbose ) { - printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vAbsFfsToAdd) ); + printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) ); Abc_PrintTime( 1, "Time", clock() - clk ); } return vAbsFfsToAdd; diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c index edc9b6fd..e3c49142 100644 --- a/src/aig/saig/saigAbsPba.c +++ b/src/aig/saig/saigAbsPba.c @@ -72,7 +72,7 @@ void Saig_ManUnrollForPba_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * v SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pvPiVarMap ) +Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec_Int_t ** pvPiVarMap ) { Aig_Man_t * pFrames; // unrolled timeframes Vec_Vec_t * vFrameCos; // the list of COs per frame @@ -80,6 +80,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pv Vec_Int_t * vRoots, * vObjs; Aig_Obj_t * pObj, * pObjNew; int i, f; + assert( nStart <= nFrames ); // collect COs and Objs visited in each frame vFrameCos = Vec_VecStart( nFrames ); vFrameObjs = Vec_VecStart( nFrames ); @@ -130,8 +131,11 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pv assert( 0 ); } // create output - Saig_ManForEachPo( pAig, pObj, i ) - pObjNew = Aig_Or( pFrames, pObjNew, pObj->pData ); + if ( f >= nStart ) + { + Saig_ManForEachPo( pAig, pObj, i ) + pObjNew = Aig_Or( pFrames, pObjNew, pObj->pData ); + } // transfer if ( f == nFrames - 1 ) break; @@ -243,7 +247,7 @@ Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose, int * piFrame ) +Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame ) { Vec_Int_t * vFlops = NULL, * vMapVar2FF, * vAssumps, * vPiVarMap; Aig_Man_t * pFrames; @@ -252,10 +256,11 @@ Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int n Aig_Obj_t * pObj; int nCoreLits, * pCoreLits; int i, iVar, RetValue, clk; - +if ( fVerbose ) +printf( "Performing abstraction with starting frame %d and total number of frames %d.\n", nStart, nFrames ); // create SAT solver clk = clock(); - pFrames = Saig_ManUnrollForPba( pAig, nFrames, &vPiVarMap ); + pFrames = Saig_ManUnrollForPba( pAig, nStart, nFrames, &vPiVarMap ); if ( fVerbose ) Aig_ManPrintStats( pFrames ); // pCnf = Cnf_DeriveSimple( pFrames, 0 ); @@ -306,7 +311,7 @@ Abc_PrintTime( 1, "Solving", clock() - clk ); } if ( fVerbose ) { - printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vAbsFfsToAdd) ); + printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAig)+Vec_IntSize(vAbsFfsToAdd) ); Abc_PrintTime( 1, "Time", clock() - clk ); } vFlops = vAbsFfsToAdd; diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c index ec933512..5f7042c8 100644 --- a/src/aig/saig/saigAbsStart.c +++ b/src/aig/saig/saigAbsStart.c @@ -139,7 +139,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo } // vFlopsNew contains PI numbers that should be kept in pAbs if ( fVerbose ) - printf( "Adding %d registers to the abstraction.\n\n", Vec_IntSize(vFlopsNew) ); + printf( "Adding %d registers to the abstraction (total = %d).\n\n", Vec_IntSize(vFlopsNew), Aig_ManRegNum(pAbs)+Vec_IntSize(vFlopsNew) ); // add to the abstraction Vec_IntForEachEntry( vFlopsNew, Entry, i ) { @@ -195,7 +195,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, } if ( fVerbose ) { - printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vFlopsNew) ); + printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vFlopsNew), Aig_ManRegNum(p)+Vec_IntSize(vFlopsNew) ); Abc_PrintTime( 1, "Time", clock() - clk ); } // vFlopsNew contains PI number that should be kept in pAbs |