Skip to content

A
abc
Commit 5953beb2 by Alan Mishchenko
Options

Restructured the code to post-process object used during refinement in &gla.

parent 5a4f1fe4
Showing with 351 additions and 330 deletions
abclib.dsp
...@@ -4367,14 +4367,6 @@ SOURCE=.\src\proof\abs\absRef.h ...@@ -4367,14 +4367,6 @@ SOURCE=.\src\proof\abs\absRef.h
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\proof\abs\absRef2.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absRef2.h
# End Source File
# Begin Source File
SOURCE=.\src\proof\abs\absUtil.c SOURCE=.\src\proof\abs\absUtil.c
# End Source File # End Source File
# Begin Source File # Begin Source File
......
src/base/abci/abc.c
...@@ -28143,10 +28143,10 @@ usage: ...@@ -28143,10 +28143,10 @@ usage:
int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
Abs_Par_t Pars, * pPars = &Pars; Abs_Par_t Pars, * pPars = &Pars;
int c, fStartVta = 0, fNewAlgo = 1; int c, fNewAlgo = 1;
Abs_ParSetDefaults( pPars ); Abs_ParSetDefaults( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPBAtrfkadmnscbpqwvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPBAtfardmnscbpqwvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -28272,18 +28272,15 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -28272,18 +28272,15 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't': case 't':
pPars->fUseTermVars ^= 1; pPars->fUseTermVars ^= 1;
break; break;
case 'r':
pPars->fUseRollback ^= 1;
break;
case 'f': case 'f':
pPars->fPropFanout ^= 1; pPars->fPropFanout ^= 1;
break; break;
case 'k':
fStartVta ^= 1;
break;
case 'a': case 'a':
pPars->fAddLayer ^= 1; pPars->fAddLayer ^= 1;
break; break;
case 'r':
pPars->fNewRefine ^= 1;
break;
case 'd': case 'd':
pPars->fDumpVabs ^= 1; pPars->fDumpVabs ^= 1;
break; break;
...@@ -28350,13 +28347,13 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -28350,13 +28347,13 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fNewAlgo ) if ( fNewAlgo )
pAbc->Status = Gia_ManPerformGla( pAbc->pGia, pPars ); pAbc->Status = Gia_ManPerformGla( pAbc->pGia, pPars );
else else
pAbc->Status = Gia_ManPerformGlaOld( pAbc->pGia, pPars, fStartVta ); pAbc->Status = Gia_ManPerformGlaOld( pAbc->pGia, pPars, 0 );
pAbc->nFrames = pPars->iFrame; pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &gla [-FSCLDETRPB num] [-A file] [-fkadmnscbpqwvh]\n" ); Abc_Print( -2, "usage: &gla [-FSCLDETRPB num] [-A file] [-fardmnscbpqwvh]\n" );
Abc_Print( -2, "\t fixed-time-frame gate-level proof- and cex-based abstraction\n" ); Abc_Print( -2, "\t fixed-time-frame gate-level proof- and cex-based abstraction\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart ); Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
...@@ -28370,8 +28367,8 @@ usage: ...@@ -28370,8 +28367,8 @@ usage:
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 dump abstraction or call prover (0<=num<=100) [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-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-f : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" );
Abc_Print( -2, "\t-k : toggle using VTA to kick start GLA for starting frames [default = %s]\n", fStartVta? "yes": "no" );
Abc_Print( -2, "\t-a : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" ); Abc_Print( -2, "\t-a : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using improved refinement heuristics [default = %s]\n", pPars->fNewRefine? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
Abc_Print( -2, "\t-m : toggle dumping abstraction map into a file [default = %s]\n", pPars->fDumpMabs? "yes": "no" ); Abc_Print( -2, "\t-m : toggle dumping abstraction map into a file [default = %s]\n", pPars->fDumpMabs? "yes": "no" );
Abc_Print( -2, "\t-n : toggle using new algorithms [default = %s]\n", fNewAlgo? "yes": "no" ); Abc_Print( -2, "\t-n : toggle using new algorithms [default = %s]\n", fNewAlgo? "yes": "no" );
......
src/proof/abs/abs.h
...@@ -61,6 +61,7 @@ struct Abs_Par_t_ ...@@ -61,6 +61,7 @@ struct Abs_Par_t_
int fUseRollback; // use rollback to the starting number of frames int fUseRollback; // use rollback to the starting number of frames
int fPropFanout; // propagate fanout implications int fPropFanout; // propagate fanout implications
int fAddLayer; // refinement strategy by adding layers int fAddLayer; // refinement strategy by adding layers
int fNewRefine; // uses new refinement heuristics
int fUseSkip; // skip proving intermediate timeframes int fUseSkip; // skip proving intermediate timeframes
int fUseSimple; // use simple CNF construction int fUseSimple; // use simple CNF construction
int fSkipHash; // skip hashing CNF while unrolling int fSkipHash; // skip hashing CNF while unrolling
...@@ -81,6 +82,13 @@ struct Abs_Par_t_ ...@@ -81,6 +82,13 @@ struct Abs_Par_t_
/// MACRO DEFINITIONS /// /// MACRO DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); }
static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); }
static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); }
static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); }
static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); }
static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS /// /// FUNCTION DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -114,6 +122,7 @@ extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla ); ...@@ -114,6 +122,7 @@ extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
extern int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla ); extern int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla );
extern int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ); extern int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla );
/*=== absOldCex.c ==========================================================*/ /*=== absOldCex.c ==========================================================*/
extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect ); extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ); extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
......
src/proof/abs/absDup.c
...@@ -53,7 +53,7 @@ void Gia_ManDupAbsFlops_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) ...@@ -53,7 +53,7 @@ void Gia_ManDupAbsFlops_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs abstraction of the AIG to preserve the included flops.] Synopsis [Extractes a flop-level abstraction given a flop map.]
Description [] Description []
...@@ -207,7 +207,7 @@ void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) ...@@ -207,7 +207,7 @@ void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs abstraction of the AIG to preserve the included gates.] Synopsis [Extractes a gate-level abstraction given a gate map.]
Description [The array contains 1 for those objects (const, RO, AND) Description [The array contains 1 for those objects (const, RO, AND)
that are included in the abstraction; 0, otherwise.] that are included in the abstraction; 0, otherwise.]
......
src/proof/abs/absGla.c
...@@ -78,13 +78,6 @@ struct Ga2_Man_t_ ...@@ -78,13 +78,6 @@ struct Ga2_Man_t_
clock_t timeOther; clock_t timeOther;
}; };
static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); }
static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); }
static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); }
static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); }
static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); }
static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; }
static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); } static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); }
static inline void Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i); } static inline void Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i); }
...@@ -1329,7 +1322,7 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p ) ...@@ -1329,7 +1322,7 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
} }
Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap ); Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap );
// Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 ); // Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 );
vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1, 1 ); vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, p->pPars->fNewRefine, 1 );
// printf( "Refinement %d\n", Vec_IntSize(vVec) ); // printf( "Refinement %d\n", Vec_IntSize(vVec) );
Abc_CexFree( pCex ); Abc_CexFree( pCex );
if ( Vec_IntSize(vVec) == 0 ) if ( Vec_IntSize(vVec) == 0 )
...@@ -1644,6 +1637,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) ...@@ -1644,6 +1637,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
// perform refinement // perform refinement
clk2 = clock(); clk2 = clock();
Rnm_ManSetRefId( p->pRnm, c );
vPPis = Ga2_ManRefine( p ); vPPis = Ga2_ManRefine( p );
p->timeCex += clock() - clk2; p->timeCex += clock() - clk2;
if ( vPPis == NULL ) if ( vPPis == NULL )
......
src/proof/abs/absGlaOld.c
...@@ -503,7 +503,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p ) ...@@ -503,7 +503,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int i; int i;
Gia_GlaPrepareCexAndMap( p, &pCex, &vMap ); Gia_GlaPrepareCexAndMap( p, &pCex, &vMap );
vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 0, 1 ); vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, p->pPars->fNewRefine, 1 );
Abc_CexFree( pCex ); Abc_CexFree( pCex );
if ( Vec_IntSize(vVec) == 0 ) if ( Vec_IntSize(vVec) == 0 )
{ {
......
src/proof/abs/absRef.c
...@@ -73,80 +73,20 @@ ABC_NAMESPACE_IMPL_START ...@@ -73,80 +73,20 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
typedef struct Rnm_Obj_t_ Rnm_Obj_t; // refinement object /*
struct Rnm_Obj_t_
{
unsigned Value : 1; // binary value
unsigned fVisit : 1; // visited object
unsigned fVisit0 : 1; // visited object
unsigned fPPi : 1; // PPI object
unsigned Prio : 24; // priority (0 - highest)
};
struct Rnm_Man_t_
{
// user data
Gia_Man_t * pGia; // working AIG manager (it is completely owned by this package)
Abc_Cex_t * pCex; // counter-example
Vec_Int_t * vMap; // mapping of CEX inputs into objects (PI + PPI, in any order)
int fPropFanout; // propagate fanouts
int fVerbose; // verbose flag
// traversing data
Vec_Int_t * vObjs; // internal objects used in value propagation
Vec_Str_t * vCounts; // fanin counters
Vec_Int_t * vFanins; // fanins
// SAT solver
sat_solver2 * pSat; // incremental SAT solver
Vec_Int_t * vSatVars; // SAT variables
Vec_Int_t * vSat2Ids; // mapping of SAT variables into object IDs
Vec_Int_t * vIsopMem; // memory for ISOP computation
// internal data
Rnm_Obj_t * pObjs; // refinement objects
int nObjs; // the number of used objects
int nObjsAlloc; // the number of allocated objects
int nObjsFrame; // the number of used objects in each frame
int nCalls; // total number of calls
int nRefines; // total refined objects
int nVisited; // visited during justification
// statistics
clock_t timeFwd; // forward propagation
clock_t timeBwd; // backward propagation
clock_t timeVer; // ternary simulation
clock_t timeTotal; // other time
};
// accessing the refinement object
static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f )
{
assert( Gia_ObjIsConst0(pObj) || pObj->Value );
assert( (int)pObj->Value < p->nObjsFrame );
assert( f >= 0 && f <= p->pCex->iFrame );
return p->pObjs + f * p->nObjsFrame + pObj->Value;
}
static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); }
static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); }
static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); }
static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); }
static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); }
static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; }
static inline int Rnm_ObjCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_StrEntry( p->vCounts, Gia_ObjId(p->pGia, pObj) ); }
static inline void Rnm_ObjSetCount( Rnm_Man_t * p, Gia_Obj_t * pObj, int c ) { Vec_StrWriteEntry( p->vCounts, Gia_ObjId(p->pGia, pObj), (char)c ); }
static inline int Rnm_ObjAddToCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { int c = Rnm_ObjCount(p, pObj); if ( c < 16 ) Rnm_ObjSetCount(p, pObj, c+1); return c; }
static inline int Rnm_ObjSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry( p->vSatVars, Gia_ObjId(p->pGia, pObj) ); } static inline int Rnm_ObjSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry( p->vSatVars, Gia_ObjId(p->pGia, pObj) ); }
static inline void Rnm_ObjSetSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj, int c) { Vec_IntWriteEntry( p->vSatVars, Gia_ObjId(p->pGia, pObj), c ); } static inline void Rnm_ObjSetSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj, int c) { Vec_IntWriteEntry( p->vSatVars, Gia_ObjId(p->pGia, pObj), c ); }
static inline int Rnm_ObjFindOrAddSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj) { if ( Rnm_ObjSatVar(p, pObj) == 0 ) { Rnm_ObjSetSatVar(p, pObj, Vec_IntSize(p->vSat2Ids)); Vec_IntPush(p->vSat2Ids, Gia_ObjId(p->pGia, pObj)); }; return 2*Rnm_ObjSatVar(p, pObj); } static inline int Rnm_ObjFindOrAddSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj) { if ( Rnm_ObjSatVar(p, pObj) == 0 ) { Rnm_ObjSetSatVar(p, pObj, Vec_IntSize(p->vSat2Ids)); Vec_IntPush(p->vSat2Ids, Gia_ObjId(p->pGia, pObj)); }; return 2*Rnm_ObjSatVar(p, pObj); }
*/
extern void Ga2_ManCnfAddStatic( sat_solver2 * pSat, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int * pLits, int iLitOut, int ProofId ); extern void Ga2_ManCnfAddStatic( sat_solver2 * pSat, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int * pLits, int iLitOut, int ProofId );
extern Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover ); extern Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
#if 0
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs UNSAT-core-based refinement.] Synopsis [Performs UNSAT-core-based refinement.]
...@@ -308,6 +248,7 @@ Vec_Int_t * Rnm_ManRefineUnsatCore( Rnm_Man_t * p, Vec_Int_t * vPPIs ) ...@@ -308,6 +248,7 @@ Vec_Int_t * Rnm_ManRefineUnsatCore( Rnm_Man_t * p, Vec_Int_t * vPPIs )
return vCoreFinal; return vCoreFinal;
} }
#endif
/**Function************************************************************* /**Function*************************************************************
...@@ -329,9 +270,9 @@ Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia ) ...@@ -329,9 +270,9 @@ Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia )
p->vObjs = Vec_IntAlloc( 100 ); p->vObjs = Vec_IntAlloc( 100 );
p->vCounts = Vec_StrStart( Gia_ManObjNum(pGia) ); p->vCounts = Vec_StrStart( Gia_ManObjNum(pGia) );
p->vFanins = Vec_IntAlloc( 1000 ); p->vFanins = Vec_IntAlloc( 1000 );
p->vSatVars = Vec_IntAlloc( 0 ); // p->vSatVars = Vec_IntAlloc( 0 );
p->vSat2Ids = Vec_IntAlloc( 1000 ); // p->vSat2Ids = Vec_IntAlloc( 1000 );
p->vIsopMem = Vec_IntAlloc( 0 ); // p->vIsopMem = Vec_IntAlloc( 0 );
p->nObjsAlloc = 10000; p->nObjsAlloc = 10000;
p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc ); p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc );
if ( p->pGia->vFanout == NULL ) if ( p->pGia->vFanout == NULL )
...@@ -364,9 +305,9 @@ void Rnm_ManStop( Rnm_Man_t * p, int fProfile ) ...@@ -364,9 +305,9 @@ void Rnm_ManStop( Rnm_Man_t * p, int fProfile )
Gia_ManCleanMark1(p->pGia); Gia_ManCleanMark1(p->pGia);
Gia_ManStaticFanoutStop(p->pGia); Gia_ManStaticFanoutStop(p->pGia);
// Gia_ManSetPhase(p->pGia); // Gia_ManSetPhase(p->pGia);
Vec_IntFree( p->vIsopMem ); // Vec_IntFree( p->vIsopMem );
Vec_IntFree( p->vSatVars ); // Vec_IntFree( p->vSatVars );
Vec_IntFree( p->vSat2Ids ); // Vec_IntFree( p->vSat2Ids );
Vec_StrFree( p->vCounts ); Vec_StrFree( p->vCounts );
Vec_IntFree( p->vFanins ); Vec_IntFree( p->vFanins );
Vec_IntFree( p->vObjs ); Vec_IntFree( p->vObjs );
...@@ -533,9 +474,9 @@ void Rnm_ManJustifyPropFanout_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_I ...@@ -533,9 +474,9 @@ void Rnm_ManJustifyPropFanout_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_I
int i, k;//, Id = Gia_ObjId(p->pGia, pObj); int i, k;//, Id = Gia_ObjId(p->pGia, pObj);
assert( pRnm->fVisit == 0 ); assert( pRnm->fVisit == 0 );
pRnm->fVisit = 1; pRnm->fVisit = 1;
if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 ) if ( Rnm_ManObj( p, pObj, 0 )->fVisitJ == 0 )
{ {
Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1; Rnm_ManObj( p, pObj, 0 )->fVisitJ = 1;
p->nVisited++; p->nVisited++;
} }
if ( pRnm->fPPi ) if ( pRnm->fPPi )
...@@ -591,9 +532,9 @@ void Rnm_ManJustify_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSe ...@@ -591,9 +532,9 @@ void Rnm_ManJustify_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSe
else else
{ {
pRnm->fVisit = 1; pRnm->fVisit = 1;
if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 ) if ( Rnm_ManObj( p, pObj, 0 )->fVisitJ == 0 )
{ {
Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1; Rnm_ManObj( p, pObj, 0 )->fVisitJ = 1;
p->nVisited++; p->nVisited++;
} }
} }
...@@ -720,177 +661,6 @@ void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap ...@@ -720,177 +661,6 @@ void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap
/**Function************************************************************* /**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Rnm_ManPrintSelected( Rnm_Man_t * p, Vec_Int_t * vSelected )
{
Gia_Obj_t * pObj;
int i, Counter = 0;
Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
{
if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
{
if ( Vec_IntFind(vSelected, Gia_ObjId(p->pGia, pObj)) >= 0 )
printf( "1" ), Counter++;
else
printf( "0" );
}
else
printf( "-" );
}
printf( " %3d\n", Counter );
}
/**Function*************************************************************
Synopsis [Perform structural analysis.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, Vec_Int_t * vSelect )
{
Vec_Int_t * vLeaves;
Gia_Obj_t * pObj, * pFanin;
int i, k;
// clean labels
Gia_ManForEachObj( p, pObj, i )
pObj->fMark0 = pObj->fMark1 = 0;
// label frontier
Gia_ManForEachObjVec( vFront, p, pObj, i )
pObj->fMark0 = 1, pObj->fMark1 = 0;
// label objects
Gia_ManForEachObjVec( vInter, p, pObj, i )
pObj->fMark1 = 0, pObj->fMark1 = 1;
// label selected
Gia_ManForEachObjVec( vSelect, p, pObj, i )
pObj->fMark1 = 1, pObj->fMark1 = 1;
// explore selected
printf( "\n" );
Gia_ManForEachObjVec( vSelect, p, pObj, i )
{
printf( "Selected %6d : ", Gia_ObjId(p, pObj) );
printf( "\n" );
vLeaves = Ga2_ObjLeaves( p, pObj );
Gia_ManForEachObjVec( vLeaves, p, pFanin, k )
{
printf( " " );
printf( "%6d ", Gia_ObjId(p, pFanin) );
if ( pFanin->fMark0 && pFanin->fMark1 )
printf( "select" );
else if ( pFanin->fMark0 && !pFanin->fMark1 )
printf( "front" );
else if ( !pFanin->fMark0 && pFanin->fMark1 )
printf( "internal" );
else if ( !pFanin->fMark0 && !pFanin->fMark1 )
printf( "new" );
printf( "\n" );
}
}
}
/**Function*************************************************************
Synopsis [Finds essential objects.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Ga2_FilterSelected( Rnm_Man_t * p, Vec_Int_t * vSelect )
{
Vec_Int_t * vNew, * vLeaves;
Gia_Obj_t * pObj, * pFanin;
int i, k, RetValue;//, Counters[3] = {0};
/*
// check that selected are not visited
Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i )
assert( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 1 );
Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
if ( Vec_IntFind(vSelect, Gia_ObjId(p->pGia, pObj)) == -1 )
assert( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 );
*/
// verify
// Gia_ManForEachObj( p->pGia, pObj, i )
// assert( Rnm_ObjCount(p, pObj) == 0 );
// increment fanin counters
Vec_IntClear( p->vFanins );
Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i )
{
vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
if ( Rnm_ObjAddToCount(p, pFanin) == 0 )
Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) );
}
// find selected objects, which create potential constraints
// - flop objects
// - objects whose fanin belongs to the justified area
// - objects whose fanins overlap
// (these do not guantee reconvergence, but may potentially have it)
// (other objects cannot have reconvergence, even if they are added)
vNew = Vec_IntAlloc( 100 );
Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i )
{
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
Vec_IntPush( vNew, Gia_ObjId(p->pGia, pObj) );
continue;
}
vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
{
if ( Gia_ObjIsConst0(pFanin)
|| (pFanin->Value && Rnm_ManObj(p, pFanin, 0)->fVisit0 == 1)
|| Rnm_ObjCount(p, pFanin) > 1
)
{
Vec_IntPush( vNew, Gia_ObjId(p->pGia, pObj) );
break;
}
}
// Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
// {
// Counters[1] += (pFanin->Value && Rnm_ManObj( p, pFanin, 0 )->fVisit0 == 1);
// Counters[2] += (Rnm_ObjCount(p, pFanin) > 1);
// }
}
RetValue = Vec_IntUniqify( vNew );
assert( RetValue == 0 );
// printf( "\n*** Select = %5d. New = %5d. Flops = %5d. Visited = %5d. Fanins = %5d.\n",
// Vec_IntSize(vSelect), Vec_IntSize(vNew), Counters[0], Counters[1], Counters[2] );
// clear fanin counters
Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
Rnm_ObjSetCount( p, pObj, 0 );
return vNew;
}
/**Function*************************************************************
Synopsis [Computes the refinement for a given counter-example.] Synopsis [Computes the refinement for a given counter-example.]
Description [] Description []
...@@ -900,12 +670,10 @@ Vec_Int_t * Ga2_FilterSelected( Rnm_Man_t * p, Vec_Int_t * vSelect ) ...@@ -900,12 +670,10 @@ Vec_Int_t * Ga2_FilterSelected( Rnm_Man_t * p, Vec_Int_t * vSelect )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fPostProcess, int fVerbose ) 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 = 0;
// int fPostProcess = 1; Vec_Int_t * vGoodPPis, * vNewPPis;
Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
Vec_Int_t * vNew;
clock_t clk, clk2 = clock(); clock_t clk, clk2 = clock();
int RetValue; int RetValue;
p->nCalls++; p->nCalls++;
...@@ -925,71 +693,50 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in ...@@ -925,71 +693,50 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
memset( p->pObjs, 0, sizeof(Rnm_Obj_t) * p->nObjs ); memset( p->pObjs, 0, sizeof(Rnm_Obj_t) * p->nObjs );
// propagate priorities // propagate priorities
clk = clock(); clk = clock();
vGoodPPis = Vec_IntAlloc( 100 );
if ( Rnm_ManSensitize( p ) ) // the CEX is not a true CEX if ( Rnm_ManSensitize( p ) ) // the CEX is not a true CEX
{ {
p->timeFwd += clock() - clk; p->timeFwd += clock() - clk;
// select refinement // select refinement
clk = clock(); clk = clock();
p->nVisited = 0; p->nVisited = 0;
Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vSelected ); Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vGoodPPis );
RetValue = Vec_IntUniqify( vSelected ); RetValue = Vec_IntUniqify( vGoodPPis );
// assert( RetValue == 0 ); // assert( RetValue == 0 );
p->timeBwd += clock() - clk; p->timeBwd += clock() - clk;
} }
// at this point array vGoodPPis contains the set of important PPIs
if ( fPostProcess ) if ( Vec_IntSize(vGoodPPis) > 0 ) // spurious CEX resulting in a non-trivial refinement
{
vNew = Ga2_FilterSelected( p, vSelected );
if ( Vec_IntSize(vNew) > 0 )
{
Vec_IntFree( vSelected );
vSelected = vNew;
}
else
{
Vec_IntFree( vNew );
// printf( "\nBig refinement.\n" );
}
}
else
{ {
/* // filter selected set
vNew = Rnm_ManRefineUnsatCore( p, vSelected ); if ( !fNewRefinement ) // default
if ( Vec_IntSize(vNew) > 0 ) vNewPPis = Rnm_ManFilterSelected( p, vGoodPPis );
{ else // this is enabled when &gla is called with -r (&gla -r)
Vec_IntFree( vSelected ); vNewPPis = Rnm_ManFilterSelectedNew( p, vGoodPPis );
vSelected = vNew;
// Vec_IntFree( vNew ); // replace the PPI array if necessary
} if ( Vec_IntSize(vNewPPis) > 0 ) // something to select, replace current refinement
else Vec_IntFree( vGoodPPis ), vGoodPPis = vNewPPis;
{ else // if there is nothing to select, do not change the current refinement array
Vec_IntFree( vNew ); Vec_IntFree( vNewPPis );
// printf( "\nBig refinement.\n" );
}
*/
} }
// clean values // clean values
Rnm_ManCleanValues( p ); Rnm_ManCleanValues( p );
// verify (empty) refinement // verify (empty) refinement
// (only works when post-processing is not applied)
if ( fVerify ) if ( fVerify )
{ {
clk = clock(); clk = clock();
Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected ); Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vGoodPPis );
p->timeVer += clock() - clk; p->timeVer += clock() - clk;
} }
// printf( "\nOriginal (%d): \n", Vec_IntSize(p->vMap) ); // Vec_IntReverseOrder( vGoodPPis );
// Rnm_ManPrintSelected( p, vSelected );
// Ga2_StructAnalize( p->pGia, vMap, p->vObjs, vSelected );
// printf( "\nObjects = %5d. Visited = %5d.\n", Vec_IntSize(p->vObjs), p->nVisited );
// Vec_IntReverseOrder( vSelected );
p->timeTotal += clock() - clk2; p->timeTotal += clock() - clk2;
p->nRefines += Vec_IntSize(vSelected); p->nRefines += Vec_IntSize(vGoodPPis);
return vSelected; return vGoodPPis;
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/proof/abs/absRef.h
...@@ -37,28 +37,90 @@ ABC_NAMESPACE_HEADER_START ...@@ -37,28 +37,90 @@ ABC_NAMESPACE_HEADER_START
/// BASIC TYPES /// /// BASIC TYPES ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
typedef struct Rnm_Man_t_ Rnm_Man_t; // refinement manager
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS /// /// MACRO DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
typedef struct Rnm_Obj_t_ Rnm_Obj_t; // refinement object
struct Rnm_Obj_t_
{
unsigned Value : 1; // binary value
unsigned fVisit : 1; // visited object
unsigned fVisitJ : 1; // justified visited object
unsigned fPPi : 1; // PPI object
unsigned Prio : 24; // priority (0 - highest)
};
typedef struct Rnm_Man_t_ Rnm_Man_t; // refinement manager
struct Rnm_Man_t_
{
// user data
Gia_Man_t * pGia; // working AIG manager (it is completely owned by this package)
Abc_Cex_t * pCex; // counter-example
Vec_Int_t * vMap; // mapping of CEX inputs into objects (PI + PPI, in any order)
int fPropFanout; // propagate fanouts
int fVerbose; // verbose flag
int nRefId; // refinement ID
// traversing data
Vec_Int_t * vObjs; // internal objects used in value propagation
// filtering of selected objects
Vec_Str_t * vCounts; // fanin counters
Vec_Int_t * vFanins; // fanins
/*
// SAT solver
sat_solver2 * pSat; // incremental SAT solver
Vec_Int_t * vSatVars; // SAT variables
Vec_Int_t * vSat2Ids; // mapping of SAT variables into object IDs
Vec_Int_t * vIsopMem; // memory for ISOP computation
*/
// internal data
Rnm_Obj_t * pObjs; // refinement objects
int nObjs; // the number of used objects
int nObjsAlloc; // the number of allocated objects
int nObjsFrame; // the number of used objects in each frame
int nCalls; // total number of calls
int nRefines; // total refined objects
int nVisited; // visited during justification
// statistics
clock_t timeFwd; // forward propagation
clock_t timeBwd; // backward propagation
clock_t timeVer; // ternary simulation
clock_t timeTotal; // other time
};
// accessing the refinement object
static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f )
{
assert( Gia_ObjIsConst0(pObj) || pObj->Value );
assert( (int)pObj->Value < p->nObjsFrame );
assert( f >= 0 && f <= p->pCex->iFrame );
return p->pObjs + f * p->nObjsFrame + pObj->Value;
}
static inline void Rnm_ManSetRefId( Rnm_Man_t * p, int RefId ) { p->nRefId = RefId; }
static inline int Rnm_ObjCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_StrEntry( p->vCounts, Gia_ObjId(p->pGia, pObj) ); }
static inline void Rnm_ObjSetCount( Rnm_Man_t * p, Gia_Obj_t * pObj, int c ) { Vec_StrWriteEntry( p->vCounts, Gia_ObjId(p->pGia, pObj), (char)c ); }
static inline int Rnm_ObjAddToCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { int c = Rnm_ObjCount(p, pObj); if ( c < 16 ) Rnm_ObjSetCount(p, pObj, c+1); return c; }
static inline int Rnm_ObjIsJust( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsConst0(pObj) || (pObj->Value && Rnm_ManObj(p, pObj, 0)->fVisitJ); }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS /// /// FUNCTION DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/*=== giaAbsRef.c ===========================================================*/ /*=== absRef.c ===========================================================*/
extern Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia ); extern Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia );
extern void Rnm_ManStop( Rnm_Man_t * p, int fProfile ); extern void Rnm_ManStop( Rnm_Man_t * p, int fProfile );
extern double Rnm_ManMemoryUsage( Rnm_Man_t * p ); extern double Rnm_ManMemoryUsage( Rnm_Man_t * p );
extern Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fPostProcess, int fVerbose ); extern Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fNewRefinement, int fVerbose );
/*=== absRefSelected.c ===========================================================*/
extern Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis );
extern Vec_Int_t * Rnm_ManFilterSelectedNew( Rnm_Man_t * p, Vec_Int_t * vOldPPis );
ABC_NAMESPACE_HEADER_END ABC_NAMESPACE_HEADER_END
#endif #endif
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/proof/abs/absRef2.c → src/proof/abs/absRefJ.c
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
PackageName [Abstraction package.] PackageName [Abstraction package.]
Synopsis [Refinement manager.] Synopsis [Refinement manager to compute all justifying subsets.]
Author [Alan Mishchenko] Author [Alan Mishchenko]
......
src/proof/abs/absRef2.h → src/proof/abs/absRefJ.h
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
PackageName [Abstraction package.] PackageName [Abstraction package.]
Synopsis [Refinement manager.] Synopsis [Refinement manager to compute all justifying subsets.]
Author [Alan Mishchenko] Author [Alan Mishchenko]
......
src/proof/abs/absRefSelect.c 0 → 100644
/**CFile****************************************************************
FileName [absRefSelect.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Abstraction package.]
Synopsis [Post-processes the set of selected refinement objects.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: absRefSelect.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abs.h"
#include "absRef.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Rnm_ManPrintSelected( Rnm_Man_t * p, Vec_Int_t * vNewPPis )
{
Gia_Obj_t * pObj;
int i, Counter = 0;
Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
if ( Gia_ObjIsPi(p->pGia, pObj) )
printf( "-" );
else if ( Vec_IntFind(vNewPPis, Gia_ObjId(p->pGia, pObj)) >= 0 )// this is PPI
printf( "1" ), Counter++;
else
printf( "0" );
printf( " %3d\n", Counter );
}
/**Function*************************************************************
Synopsis [Perform structural analysis.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, Vec_Int_t * vNewPPis )
{
Vec_Int_t * vLeaves;
Gia_Obj_t * pObj, * pFanin;
int i, k;
// clean labels
Gia_ManForEachObj( p, pObj, i )
pObj->fMark0 = pObj->fMark1 = 0;
// label frontier
Gia_ManForEachObjVec( vFront, p, pObj, i )
pObj->fMark0 = 1, pObj->fMark1 = 0;
// label objects
Gia_ManForEachObjVec( vInter, p, pObj, i )
pObj->fMark1 = 0, pObj->fMark1 = 1;
// label selected
Gia_ManForEachObjVec( vNewPPis, p, pObj, i )
pObj->fMark1 = 1, pObj->fMark1 = 1;
// explore selected
Gia_ManForEachObjVec( vNewPPis, p, pObj, i )
{
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 )
{
printf( " " );
printf( "%6d ", Gia_ObjId(p, pFanin) );
if ( pFanin->fMark0 && pFanin->fMark1 )
printf( "selected PPI" );
else if ( pFanin->fMark0 && !pFanin->fMark1 )
printf( "frontier (original PI or PPI)" );
else if ( !pFanin->fMark0 && pFanin->fMark1 )
printf( "abstracted node" );
else if ( !pFanin->fMark0 && !pFanin->fMark1 )
printf( "free variable" );
printf( "\n" );
}
}
}
/**Function*************************************************************
Synopsis [Postprocessing the set of PPIs using structural analysis.]
Description [The following sets are used:
The set of all PI+PPI is in p->vMap.
The set of all abstracted objects is in p->vObjs;
The set of important PPIs is in vOldPPis.
The new set of selected PPIs is in vNewPPis.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
{
int fVerbose = 0;
Vec_Int_t * vNewPPis, * vLeaves;
Gia_Obj_t * pObj, * pFanin;
int i, k, RetValue, Counters[3] = {0};
// (0) make sure fanin counters are 0 at the beginning
// Gia_ManForEachObj( p->pGia, pObj, i )
// assert( Rnm_ObjCount(p, pObj) == 0 );
// (1) increment PPI fanin counters
Vec_IntClear( p->vFanins );
Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
{
vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
Gia_ManForEachObjVec( vLeaves, 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) );
}
// (3) select objects with reconvergence, which create potential constraints
// - flop objects
// - objects whose fanin belongs to the justified area
// - objects whose fanins overlap
// (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;
}
vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
{
if ( Rnm_ObjIsJust(p, pFanin) || Rnm_ObjCount(p, pFanin) > 1 )
{
if ( fVerbose )
Counters[1] += Rnm_ObjIsJust(p, pFanin);
if ( fVerbose )
Counters[2] += (Rnm_ObjCount(p, pFanin) > 1);
Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
break;
}
}
}
RetValue = Vec_IntUniqify( vNewPPis );
assert( RetValue == 0 );
// (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;
}
/**Function*************************************************************
Synopsis [Improved postprocessing the set of PPIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Rnm_ManFilterSelectedNew( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
{
Vec_Int_t * vNewPPis;
vNewPPis = Vec_IntDup( vOldPPis );
return vNewPPis;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/proof/abs/module.make
...@@ -10,6 +10,6 @@ SRC += src/proof/abs/abs.c \ ...@@ -10,6 +10,6 @@ SRC += src/proof/abs/abs.c \
src/proof/abs/absOut.c \ src/proof/abs/absOut.c \
src/proof/abs/absPth.c \ src/proof/abs/absPth.c \
src/proof/abs/absRef.c \ src/proof/abs/absRef.c \
src/proof/abs/absRef2.c \ src/proof/abs/absRefSelect.c \
src/proof/abs/absVta.c \ src/proof/abs/absVta.c \
src/proof/abs/absUtil.c src/proof/abs/absUtil.c
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