Skip to content

A
abc
Commit ee436f93 by Alan Mishchenko
Options

Changed a few things in the refinement package of &gla.

parent 33cd4dea
Showing with 118 additions and 24 deletions
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" );
......
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() )
......
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);
......
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;
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment