From ee436f9377201e15f1a8a52acf27e78139841d6c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 16 Sep 2012 13:56:10 -0700 Subject: Changed a few things in the refinement package of &gla. --- src/base/abci/abc.c | 2 +- src/proof/abs/absGla.c | 6 ++- src/proof/abs/absRef.c | 23 +++++---- src/proof/abs/absRefSelect.c | 111 ++++++++++++++++++++++++++++++++++++++----- 4 files changed, 118 insertions(+), 24 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dc86ccb2..254359c2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28364,7 +28364,7 @@ usage: Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin ); Abc_Print( -2, "\t-P num : maximum percentage of added objects before a restart (0<=num<=100) [default = %d]\n", pPars->nRatioMax ); - Abc_Print( -2, "\t-B num : the number of stable frames to dump abstraction or call prover (0<=num<=100) [default = %d]\n", pPars->nFramesNoChangeLim ); + Abc_Print( -2, "\t-B num : the number of stable frames to call prover or dump abstraction [default = %d]\n", pPars->nFramesNoChangeLim ); Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" ); Abc_Print( -2, "\t-f : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" ); Abc_Print( -2, "\t-a : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" ); diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 260a649c..fe024710 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -59,6 +59,7 @@ struct Ga2_Man_t_ int nSatVars; // the number of SAT variables int nCexes; // the number of counter-examples int nObjAdded; // objs added during refinement + int nPdrCalls; // count the number of concurrent calls // hash table int * pTable; int nTable; @@ -463,8 +464,8 @@ void Ga2_ManStop( Ga2_Man_t * p ) sat_solver2_nconflicts(p->pSat), sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); if ( p->pPars->fVerbose ) - Abc_Print( 1, "Hash hits = %d. Hash misses = %d. Hash overs = %d.\n", - p->nHashHit, p->nHashMiss, p->nHashOver ); + Abc_Print( 1, "Hash hits = %d. Hash misses = %d. Hash overs = %d. Concurrent calls = %d.\n", + p->nHashHit, p->nHashMiss, p->nHashOver, p->nPdrCalls ); if( p->pSat ) sat_solver2_delete( p->pSat ); Vec_VecFree( (Vec_Vec_t *)p->vCnfs ); @@ -1794,6 +1795,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) // prove new one Gia_GlaProveAbsracted( pAig, pPars->fVerbose ); iFrameTryToProve = f; + p->nPdrCalls++; } // speak to the bridge if ( Abc_FrameIsBridgeMode() ) diff --git a/src/proof/abs/absRef.c b/src/proof/abs/absRef.c index 64e1f55c..f72d86e2 100644 --- a/src/proof/abs/absRef.c +++ b/src/proof/abs/absRef.c @@ -672,7 +672,7 @@ void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap ***********************************************************************/ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fNewRefinement, int fVerbose ) { - int fVerify = 0; + int fVerify = 1; Vec_Int_t * vGoodPPis, * vNewPPis; clock_t clk, clk2 = clock(); int RetValue; @@ -705,6 +705,16 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in // assert( RetValue == 0 ); p->timeBwd += clock() - clk; } + + // verify (empty) refinement + // (only works when post-processing is not applied) + if ( fVerify ) + { + clk = clock(); + Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vGoodPPis ); + p->timeVer += clock() - clk; + } + // at this point array vGoodPPis contains the set of important PPIs if ( Vec_IntSize(vGoodPPis) > 0 ) // spurious CEX resulting in a non-trivial refinement { @@ -722,17 +732,10 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in } // clean values + // we cannot do this before, because we need to remember what objects + // belong to the abstraction when we do Rnm_ManFilterSelected() Rnm_ManCleanValues( p ); - // verify (empty) refinement - // (only works when post-processing is not applied) - if ( fVerify ) - { - clk = clock(); - Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vGoodPPis ); - p->timeVer += clock() - clk; - } - // Vec_IntReverseOrder( vGoodPPis ); p->timeTotal += clock() - clk2; p->nRefines += Vec_IntSize(vGoodPPis); diff --git a/src/proof/abs/absRefSelect.c b/src/proof/abs/absRefSelect.c index 871eb79b..1832d42c 100644 --- a/src/proof/abs/absRefSelect.c +++ b/src/proof/abs/absRefSelect.c @@ -69,7 +69,7 @@ void Rnm_ManPrintSelected( Rnm_Man_t * p, Vec_Int_t * vNewPPis ) ***********************************************************************/ void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, Vec_Int_t * vNewPPis ) { - Vec_Int_t * vLeaves; + Vec_Int_t * vFanins; Gia_Obj_t * pObj, * pFanin; int i, k; // clean labels @@ -90,8 +90,8 @@ void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, V printf( "Selected PPI %3d : ", i+1 ); printf( "%6d ", Gia_ObjId(p, pObj) ); printf( "\n" ); - vLeaves = Ga2_ObjLeaves( p, pObj ); - Gia_ManForEachObjVec( vLeaves, p, pFanin, k ) + vFanins = Ga2_ObjLeaves( p, pObj ); + Gia_ManForEachObjVec( vFanins, p, pFanin, k ) { printf( " " ); printf( "%6d ", Gia_ObjId(p, pFanin) ); @@ -125,8 +125,8 @@ void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, V ***********************************************************************/ Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis ) { - int fVerbose = 0; - Vec_Int_t * vNewPPis, * vLeaves; + int fVerbose = 0; + Vec_Int_t * vNewPPis, * vFanins; Gia_Obj_t * pObj, * pFanin; int i, k, RetValue, Counters[3] = {0}; @@ -138,8 +138,8 @@ Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis ) Vec_IntClear( p->vFanins ); Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i ) { - vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) + vFanins = Ga2_ObjLeaves( p->pGia, pObj ); + Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k ) if ( Rnm_ObjAddToCount(p, pFanin) == 0 ) // fanin counter is 0 -- save it Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) ); } @@ -160,8 +160,8 @@ Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis ) Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) ); continue; } - vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) + vFanins = Ga2_ObjLeaves( p->pGia, pObj ); + Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k ) { if ( Rnm_ObjIsJust(p, pFanin) || Rnm_ObjCount(p, pFanin) > 1 ) { @@ -206,8 +206,97 @@ Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis ) ***********************************************************************/ Vec_Int_t * Rnm_ManFilterSelectedNew( Rnm_Man_t * p, Vec_Int_t * vOldPPis ) { - Vec_Int_t * vNewPPis; - vNewPPis = Vec_IntDup( vOldPPis ); + static int Counter = 0; + int fVerbose = 0; + Vec_Int_t * vNewPPis, * vFanins, * vFanins2; + Gia_Obj_t * pObj, * pFanin, * pFanin2; + int i, k, k2, RetValue, Counters[3] = {0}; + + // return full set of PPIs once in a while + if ( ++Counter % 9 == 0 ) + return Vec_IntDup( vOldPPis ); + return Rnm_ManFilterSelected( p, vOldPPis ); + + // (0) make sure fanin counters are 0 at the beginning +// Gia_ManForEachObj( p->pGia, pObj, i ) +// assert( Rnm_ObjCount(p, pObj) == 0 ); + + // (1) increment two levels of PPI fanin counters + Vec_IntClear( p->vFanins ); + Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i ) + { + // go through the fanins + vFanins = Ga2_ObjLeaves( p->pGia, pObj ); + Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k ) + { + Rnm_ObjAddToCount(p, pFanin); + if ( Rnm_ObjIsJust(p, pFanin) ) // included in the abstraction + Rnm_ObjAddToCount(p, pFanin); // count it second time! + Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) ); + + // go through the fanins of the fanins + vFanins2 = Ga2_ObjLeaves( p->pGia, pFanin ); + Gia_ManForEachObjVec( vFanins2, p->pGia, pFanin2, k2 ) + { + Rnm_ObjAddToCount(p, pFanin2); + if ( Rnm_ObjIsJust(p, pFanin2) ) // included in the abstraction + Rnm_ObjAddToCount(p, pFanin2); // count it second time! + Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin2) ); + } + } + } + + // (3) select objects with reconvergence, which create potential constraints + // - flop objects - yes + // - objects whose fanin (or fanins' fanin) belongs to the justified area - yes + // - objects whose fanins (or fanins' fanin) overlap - yes + // (these do not guantee reconvergence, but may potentially have it) + // (other objects cannot have reconvergence, even if they are added) + vNewPPis = Vec_IntAlloc( 100 ); + Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i ) + { + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( fVerbose ) + Counters[0]++; + Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) ); + continue; + } + // go through the first fanins + vFanins = Ga2_ObjLeaves( p->pGia, pObj ); + Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k ) + { + if ( Rnm_ObjCount(p, pFanin) > 1 ) + Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) ); + continue; + + // go through the fanins of the fanins + vFanins2 = Ga2_ObjLeaves( p->pGia, pFanin ); + Gia_ManForEachObjVec( vFanins2, p->pGia, pFanin2, k2 ) + { + if ( Rnm_ObjCount(p, pFanin2) > 1 ) + { +// Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pFanin) ); + Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) ); + } + } + } + } + RetValue = Vec_IntUniqify( vNewPPis ); +// assert( RetValue == 0 ); // we will have duplicated entries here! + + // (4) clear fanin counters + // this is important for counters to be correctly set in the future iterations -- see step (0) + Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i ) + Rnm_ObjSetCount( p, pObj, 0 ); + + // visualize + if ( fVerbose ) + printf( "*** Refinement %3d : PI+PPI =%4d. Old =%4d. New =%4d. FF =%4d. Just =%4d. Shared =%4d.\n", + p->nRefId, Vec_IntSize(p->vMap), Vec_IntSize(vOldPPis), Vec_IntSize(vNewPPis), Counters[0], Counters[1], Counters[2] ); + +// Rnm_ManPrintSelected( p, vNewPPis ); +// Ga2_StructAnalize( p->pGia, p->vMap, p->vObjs, vNewPPis ); return vNewPPis; } -- cgit v1.2.3