From 5953beb2da3e9ee4bcc2fc03487cb8c8ef36877c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 16 Sep 2012 09:54:19 -0700 Subject: Restructured the code to post-process object used during refinement in &gla. --- src/base/abci/abc.c | 19 +- src/proof/abs/abs.h | 9 + src/proof/abs/absDup.c | 4 +- src/proof/abs/absGla.c | 10 +- src/proof/abs/absGlaOld.c | 2 +- src/proof/abs/absRef.c | 329 ++-------------- src/proof/abs/absRef.h | 74 +++- src/proof/abs/absRef2.c | 916 ------------------------------------------- src/proof/abs/absRef2.h | 67 ---- src/proof/abs/absRefJ.c | 916 +++++++++++++++++++++++++++++++++++++++++++ src/proof/abs/absRefJ.h | 67 ++++ src/proof/abs/absRefSelect.c | 220 +++++++++++ src/proof/abs/module.make | 2 +- 13 files changed, 1332 insertions(+), 1303 deletions(-) delete mode 100644 src/proof/abs/absRef2.c delete mode 100644 src/proof/abs/absRef2.h create mode 100644 src/proof/abs/absRefJ.c create mode 100644 src/proof/abs/absRefJ.h create mode 100644 src/proof/abs/absRefSelect.c (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c2b44921..dc86ccb2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28143,10 +28143,10 @@ usage: int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abs_Par_t Pars, * pPars = &Pars; - int c, fStartVta = 0, fNewAlgo = 1; + int c, fNewAlgo = 1; Abs_ParSetDefaults( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPBAtrfkadmnscbpqwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPBAtfardmnscbpqwvh" ) ) != EOF ) { switch ( c ) { @@ -28272,18 +28272,15 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': pPars->fUseTermVars ^= 1; break; - case 'r': - pPars->fUseRollback ^= 1; - break; case 'f': pPars->fPropFanout ^= 1; break; - case 'k': - fStartVta ^= 1; - break; case 'a': pPars->fAddLayer ^= 1; break; + case 'r': + pPars->fNewRefine ^= 1; + break; case 'd': pPars->fDumpVabs ^= 1; break; @@ -28350,13 +28347,13 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fNewAlgo ) pAbc->Status = Gia_ManPerformGla( pAbc->pGia, pPars ); else - pAbc->Status = Gia_ManPerformGlaOld( pAbc->pGia, pPars, fStartVta ); + pAbc->Status = Gia_ManPerformGlaOld( pAbc->pGia, pPars, 0 ); pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; 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-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 ); @@ -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-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-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-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-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" ); diff --git a/src/proof/abs/abs.h b/src/proof/abs/abs.h index e7ab9e7d..11eda38c 100644 --- a/src/proof/abs/abs.h +++ b/src/proof/abs/abs.h @@ -61,6 +61,7 @@ struct Abs_Par_t_ int fUseRollback; // use rollback to the starting number of frames int fPropFanout; // propagate fanout implications int fAddLayer; // refinement strategy by adding layers + int fNewRefine; // uses new refinement heuristics int fUseSkip; // skip proving intermediate timeframes int fUseSimple; // use simple CNF construction int fSkipHash; // skip hashing CNF while unrolling @@ -81,6 +82,13 @@ struct Abs_Par_t_ /// 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 /// //////////////////////////////////////////////////////////////////////// @@ -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_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ); + /*=== 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 Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ); diff --git a/src/proof/abs/absDup.c b/src/proof/abs/absDup.c index 247137bd..94215575 100644 --- a/src/proof/abs/absDup.c +++ b/src/proof/abs/absDup.c @@ -53,7 +53,7 @@ void Gia_ManDupAbsFlops_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) /**Function************************************************************* - Synopsis [Performs abstraction of the AIG to preserve the included flops.] + Synopsis [Extractes a flop-level abstraction given a flop map.] Description [] @@ -207,7 +207,7 @@ void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) /**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) that are included in the abstraction; 0, otherwise.] diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 76b6c231..260a649c 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -78,13 +78,6 @@ struct Ga2_Man_t_ 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 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 ) } Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap ); // 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) ); Abc_CexFree( pCex ); if ( Vec_IntSize(vVec) == 0 ) @@ -1644,6 +1637,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) // perform refinement clk2 = clock(); + Rnm_ManSetRefId( p->pRnm, c ); vPPis = Ga2_ManRefine( p ); p->timeCex += clock() - clk2; if ( vPPis == NULL ) diff --git a/src/proof/abs/absGlaOld.c b/src/proof/abs/absGlaOld.c index 5ee69739..4ab956f7 100644 --- a/src/proof/abs/absGlaOld.c +++ b/src/proof/abs/absGlaOld.c @@ -503,7 +503,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p ) Gia_Obj_t * pObj; int i; 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 ); if ( Vec_IntSize(vVec) == 0 ) { diff --git a/src/proof/abs/absRef.c b/src/proof/abs/absRef.c index 3aea96ee..64e1f55c 100644 --- a/src/proof/abs/absRef.c +++ b/src/proof/abs/absRef.c @@ -73,80 +73,20 @@ ABC_NAMESPACE_IMPL_START /// 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 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); } - +*/ 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 ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +#if 0 + /**Function************************************************************* Synopsis [Performs UNSAT-core-based refinement.] @@ -308,6 +248,7 @@ Vec_Int_t * Rnm_ManRefineUnsatCore( Rnm_Man_t * p, Vec_Int_t * vPPIs ) return vCoreFinal; } +#endif /**Function************************************************************* @@ -329,9 +270,9 @@ Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia ) p->vObjs = Vec_IntAlloc( 100 ); p->vCounts = Vec_StrStart( Gia_ManObjNum(pGia) ); p->vFanins = Vec_IntAlloc( 1000 ); - p->vSatVars = Vec_IntAlloc( 0 ); - p->vSat2Ids = Vec_IntAlloc( 1000 ); - p->vIsopMem = Vec_IntAlloc( 0 ); +// p->vSatVars = Vec_IntAlloc( 0 ); +// p->vSat2Ids = Vec_IntAlloc( 1000 ); +// p->vIsopMem = Vec_IntAlloc( 0 ); p->nObjsAlloc = 10000; p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc ); if ( p->pGia->vFanout == NULL ) @@ -364,9 +305,9 @@ void Rnm_ManStop( Rnm_Man_t * p, int fProfile ) Gia_ManCleanMark1(p->pGia); Gia_ManStaticFanoutStop(p->pGia); // Gia_ManSetPhase(p->pGia); - Vec_IntFree( p->vIsopMem ); - Vec_IntFree( p->vSatVars ); - Vec_IntFree( p->vSat2Ids ); +// Vec_IntFree( p->vIsopMem ); +// Vec_IntFree( p->vSatVars ); +// Vec_IntFree( p->vSat2Ids ); Vec_StrFree( p->vCounts ); Vec_IntFree( p->vFanins ); Vec_IntFree( p->vObjs ); @@ -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); assert( pRnm->fVisit == 0 ); 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++; } 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 else { 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++; } } @@ -718,177 +659,6 @@ void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap Abc_Print( 1, "\nRefinement verification has failed!!!\n" ); } -/**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.] @@ -900,12 +670,10 @@ Vec_Int_t * Ga2_FilterSelected( Rnm_Man_t * p, Vec_Int_t * vSelect ) 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 fPostProcess = 1; - Vec_Int_t * vSelected = Vec_IntAlloc( 100 ); - Vec_Int_t * vNew; + Vec_Int_t * vGoodPPis, * vNewPPis; clock_t clk, clk2 = clock(); int RetValue; p->nCalls++; @@ -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 ); // propagate priorities clk = clock(); + vGoodPPis = Vec_IntAlloc( 100 ); if ( Rnm_ManSensitize( p ) ) // the CEX is not a true CEX { p->timeFwd += clock() - clk; // select refinement clk = clock(); p->nVisited = 0; - Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vSelected ); - RetValue = Vec_IntUniqify( vSelected ); + Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vGoodPPis ); + RetValue = Vec_IntUniqify( vGoodPPis ); // assert( RetValue == 0 ); p->timeBwd += clock() - clk; } - - if ( fPostProcess ) - { - vNew = Ga2_FilterSelected( p, vSelected ); - if ( Vec_IntSize(vNew) > 0 ) - { - Vec_IntFree( vSelected ); - vSelected = vNew; - } - else - { - Vec_IntFree( vNew ); - // printf( "\nBig refinement.\n" ); - } - } - else + // at this point array vGoodPPis contains the set of important PPIs + if ( Vec_IntSize(vGoodPPis) > 0 ) // spurious CEX resulting in a non-trivial refinement { -/* - vNew = Rnm_ManRefineUnsatCore( p, vSelected ); - if ( Vec_IntSize(vNew) > 0 ) - { - Vec_IntFree( vSelected ); - vSelected = vNew; -// Vec_IntFree( vNew ); - } - else - { - Vec_IntFree( vNew ); - // printf( "\nBig refinement.\n" ); - } -*/ + // filter selected set + if ( !fNewRefinement ) // default + vNewPPis = Rnm_ManFilterSelected( p, vGoodPPis ); + else // this is enabled when &gla is called with -r (&gla -r) + vNewPPis = Rnm_ManFilterSelectedNew( p, vGoodPPis ); + + // replace the PPI array if necessary + if ( Vec_IntSize(vNewPPis) > 0 ) // something to select, replace current refinement + Vec_IntFree( vGoodPPis ), vGoodPPis = vNewPPis; + else // if there is nothing to select, do not change the current refinement array + Vec_IntFree( vNewPPis ); } // clean values 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, vSelected ); + Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vGoodPPis ); p->timeVer += clock() - clk; } -// printf( "\nOriginal (%d): \n", Vec_IntSize(p->vMap) ); -// 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 ); +// Vec_IntReverseOrder( vGoodPPis ); p->timeTotal += clock() - clk2; - p->nRefines += Vec_IntSize(vSelected); - return vSelected; + p->nRefines += Vec_IntSize(vGoodPPis); + return vGoodPPis; } //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/abs/absRef.h b/src/proof/abs/absRef.h index ca46c776..9bae40a3 100644 --- a/src/proof/abs/absRef.h +++ b/src/proof/abs/absRef.h @@ -37,28 +37,90 @@ ABC_NAMESPACE_HEADER_START /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// -typedef struct Rnm_Man_t_ Rnm_Man_t; // refinement manager //////////////////////////////////////////////////////////////////////// /// 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 /// //////////////////////////////////////////////////////////////////////// -/*=== giaAbsRef.c ===========================================================*/ +/*=== absRef.c ===========================================================*/ extern Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia ); extern void Rnm_ManStop( Rnm_Man_t * p, int fProfile ); 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 - - #endif //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/abs/absRef2.c b/src/proof/abs/absRef2.c deleted file mode 100644 index 7fb26e5a..00000000 --- a/src/proof/abs/absRef2.c +++ /dev/null @@ -1,916 +0,0 @@ -/**CFile**************************************************************** - - FileName [absRef2.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Abstraction package.] - - Synopsis [Refinement manager.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: absRef2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abs.h" -#include "absRef2.h" - -ABC_NAMESPACE_IMPL_START - -/* - Description of the refinement manager - - This refinement manager should be - * started by calling Rf2_ManStart() - this procedure takes one argument, the user's seq miter as a GIA manager - - the manager should have only one property output - - this manager should not change while the refinement manager is alive - - it cannot be used by external applications for any purpose - - when the refinement manager stop, GIA manager is the same as at the beginning - - in the meantime, it will have some data-structures attached to its nodes... - * stopped by calling Rf2_ManStop() - * between starting and stopping, refinements are obtained by calling Rf2_ManRefine() - - Procedure Rf2_ManRefine() takes the following arguments: - * the refinement manager previously started by Rf2_ManStart() - * counter-example (CEX) obtained by abstracting some logic of GIA - * mapping (vMap) of inputs of the CEX into the object IDs of the GIA manager - - only PI, flop outputs, and internal AND nodes can be used in vMap - - the ordering of objects in vMap is not important - - however, the index of a non-PI object in vMap is used as its priority - (the smaller the index, the more likely this non-PI object apears in a refinement) - - only the logic between PO and the objects listed in vMap is traversed by the manager - (as a result, GIA can be arbitrarily large, but only objects used in the abstraction - and the pseudo-PI, that is, objects in the cut, will be visited by the manager) - * flag fPropFanout defines whether value propagation is done through the fanout - - it this flag is enabled, theoretically refinement should be better (the result smaller) - * flag fVerbose may print some statistics - - The refinement manager returns a minimal-size array of integer IDs of GIA objects - which should be added to the abstraction to possibly prevent the given counter-example - - only flop output and internal AND nodes from vMap may appear in the resulting array - - if the resulting array is empty, the CEX is a true CEX - (in other words, non-PI objects are not needed to set the PO value to 1) - - Verification of the selected refinement is performed by - - initializing all PI objects in vMap to value 0 or 1 they have in the CEX - - initializing all remaining objects in vMap to value X - - initializing objects used in the refiment to value 0 or 1 they have in the CEX - - simulating through as many timeframes as required by the CEX - - if the PO value in the last frame is 1, the refinement is correct - (however, the minimality of the refinement is not currently checked) - -*/ - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Rf2_Obj_t_ Rf2_Obj_t; // refinement object -struct Rf2_Obj_t_ -{ - unsigned Value : 1; // binary value - unsigned fVisit : 1; // visited object - unsigned fPPi : 1; // PPI object - unsigned Prio : 24; // priority (0 - highest) -}; - -struct Rf2_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_Int_t * vFanins; // fanins of the PPI nodes - Vec_Int_t * pvVecs; // vectors of integers for each object - Vec_Vec_t * vGrp2Ppi; // for each node, the set of PPIs to include - int nMapWords; - // internal data - Rf2_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 - // 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 Rf2_Obj_t * Rf2_ManObj( Rf2_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 Vec_Int_t * Rf2_ObjVec( Rf2_Man_t * p, Gia_Obj_t * pObj ) -{ - return p->pvVecs + Gia_ObjId(p->pGia, pObj); -} - - -static inline unsigned * Rf2_ObjA( Rf2_Man_t * p, Gia_Obj_t * pObj ) -{ - return (unsigned *)Vec_IntArray(Rf2_ObjVec(p, pObj)); -} -static inline unsigned * Rf2_ObjN( Rf2_Man_t * p, Gia_Obj_t * pObj ) -{ - return (unsigned *)Vec_IntArray(Rf2_ObjVec(p, pObj)) + p->nMapWords; -} -static inline void Rf2_ObjClear( Rf2_Man_t * p, Gia_Obj_t * pObj ) -{ - Vec_IntFill( Rf2_ObjVec(p, pObj), 2*p->nMapWords, 0 ); -} -static inline void Rf2_ObjStart( Rf2_Man_t * p, Gia_Obj_t * pObj, int i ) -{ - Vec_Int_t * vVec = Rf2_ObjVec(p, pObj); - int w; - Vec_IntClear( vVec ); - for ( w = 0; w < p->nMapWords; w++ ) - Vec_IntPush( vVec, 0 ); - for ( w = 0; w < p->nMapWords; w++ ) - Vec_IntPush( vVec, ~0 ); - Abc_InfoSetBit( Rf2_ObjA(p, pObj), i ); - Abc_InfoXorBit( Rf2_ObjN(p, pObj), i ); -} -static inline void Rf2_ObjCopy( Rf2_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) -{ - assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 2*p->nMapWords ); - memcpy( Rf2_ObjA(p, pObj), Rf2_ObjA(p, pFanin), sizeof(unsigned) * 2 * p->nMapWords ); -} -static inline void Rf2_ObjDeriveAnd( Rf2_Man_t * p, Gia_Obj_t * pObj, int One ) -{ - unsigned * pInfo, * pInfo0, * pInfo1; - int i; - assert( Gia_ObjIsAnd(pObj) ); - assert( One == (int)pObj->fMark0 ); - assert( One == (int)(Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) ); - assert( One == (int)(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) ); - assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 2*p->nMapWords ); - - pInfo = Rf2_ObjA( p, pObj ); - pInfo0 = Rf2_ObjA( p, Gia_ObjFanin0(pObj) ); - pInfo1 = Rf2_ObjA( p, Gia_ObjFanin1(pObj) ); - for ( i = 0; i < p->nMapWords; i++ ) - pInfo[i] = One ? (pInfo0[i] & pInfo1[i]) : (pInfo0[i] | pInfo1[i]); - - pInfo = Rf2_ObjN( p, pObj ); - pInfo0 = Rf2_ObjN( p, Gia_ObjFanin0(pObj) ); - pInfo1 = Rf2_ObjN( p, Gia_ObjFanin1(pObj) ); - for ( i = 0; i < p->nMapWords; i++ ) - pInfo[i] = One ? (pInfo0[i] | pInfo1[i]) : (pInfo0[i] & pInfo1[i]); -} -static inline void Rf2_ObjPrint( Rf2_Man_t * p, Gia_Obj_t * pRoot ) -{ - Gia_Obj_t * pObj; - unsigned * pInfo; - int i; - pInfo = Rf2_ObjA( p, pRoot ); - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - if ( !Gia_ObjIsPi(p->pGia, pObj) ) - printf( "%d", Abc_InfoHasBit(pInfo, i) ); - printf( "\n" ); - pInfo = Rf2_ObjN( p, pRoot ); - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - if ( !Gia_ObjIsPi(p->pGia, pObj) ) - printf( "%d", !Abc_InfoHasBit(pInfo, i) ); - printf( "\n" ); - -} - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Creates a new manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Rf2_Man_t * Rf2_ManStart( Gia_Man_t * pGia ) -{ - Rf2_Man_t * p; - assert( Gia_ManPoNum(pGia) == 1 ); - p = ABC_CALLOC( Rf2_Man_t, 1 ); - p->pGia = pGia; - p->vObjs = Vec_IntAlloc( 1000 ); - p->vFanins = Vec_IntAlloc( 1000 ); - p->pvVecs = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(pGia) ); - p->vGrp2Ppi = Vec_VecStart( 100 ); - Gia_ManCleanMark0(pGia); - Gia_ManCleanMark1(pGia); - return p; -} -void Rf2_ManStop( Rf2_Man_t * p, int fProfile ) -{ - if ( !p ) return; - // print runtime statistics - if ( fProfile && p->nCalls ) - { - double MemGia = sizeof(Gia_Man_t) + sizeof(Gia_Obj_t) * p->pGia->nObjsAlloc + sizeof(int) * p->pGia->nTravIdsAlloc; - double MemOther = sizeof(Rf2_Man_t) + sizeof(Rf2_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs); - clock_t timeOther = p->timeTotal - p->timeFwd - p->timeBwd - p->timeVer; - printf( "Abstraction refinement runtime statistics:\n" ); - ABC_PRTP( "Sensetization", p->timeFwd, p->timeTotal ); - ABC_PRTP( "Justification", p->timeBwd, p->timeTotal ); - ABC_PRTP( "Verification ", p->timeVer, p->timeTotal ); - ABC_PRTP( "Other ", timeOther, p->timeTotal ); - ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); - printf( "Total calls = %d. Average refine = %.1f. GIA mem = %.3f MB. Other mem = %.3f MB.\n", - p->nCalls, 1.0*p->nRefines/p->nCalls, MemGia/(1<<20), MemOther/(1<<20) ); - } - Vec_IntFree( p->vObjs ); - Vec_IntFree( p->vFanins ); - Vec_VecFree( p->vGrp2Ppi ); - ABC_FREE( p->pvVecs ); - ABC_FREE( p ); -} -double Rf2_ManMemoryUsage( Rf2_Man_t * p ) -{ - return (double)(sizeof(Rf2_Man_t) + sizeof(Vec_Int_t) * Gia_ManObjNum(p->pGia)); -} - - -/**Function************************************************************* - - Synopsis [Collect internal objects to be used in value propagation.] - - Description [Resulting array vObjs contains RO, AND, PO/RI in a topo order.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Rf2_ManCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjs ) -{ - if ( Gia_ObjIsTravIdCurrent(p, pObj) ) - return; - Gia_ObjSetTravIdCurrent(p, pObj); - if ( Gia_ObjIsCo(pObj) ) - Rf2_ManCollect_rec( p, Gia_ObjFanin0(pObj), vObjs ); - else if ( Gia_ObjIsAnd(pObj) ) - { - Rf2_ManCollect_rec( p, Gia_ObjFanin0(pObj), vObjs ); - Rf2_ManCollect_rec( p, Gia_ObjFanin1(pObj), vObjs ); - } - else if ( !Gia_ObjIsRo(p, pObj) ) - assert( 0 ); - Vec_IntPush( vObjs, Gia_ObjId(p, pObj) ); -} -void Rf2_ManCollect( Rf2_Man_t * p ) -{ - Gia_Obj_t * pObj = NULL; - int i; - // mark const/PIs/PPIs - Gia_ManIncrementTravId( p->pGia ); - Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) ); - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - { - assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); - Gia_ObjSetTravIdCurrent( p->pGia, pObj ); - } - // collect objects - Vec_IntClear( p->vObjs ); - Rf2_ManCollect_rec( p->pGia, Gia_ManPo(p->pGia, 0), p->vObjs ); - Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) - if ( Gia_ObjIsRo(p->pGia, pObj) ) - Rf2_ManCollect_rec( p->pGia, Gia_ObjRoToRi(p->pGia, pObj), p->vObjs ); - // the last object should be a CO - assert( Gia_ObjIsCo(pObj) ); -} - -/**Function************************************************************* - - Synopsis [Performs sensitization analysis.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Rf2_ManSensitize( Rf2_Man_t * p ) -{ - Rf2_Obj_t * pRnm, * pRnm0, * pRnm1; - Gia_Obj_t * pObj; - int f, i, iBit = p->pCex->nRegs; - // const0 is initialized automatically in all timeframes - for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis ) - { - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - { - assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); - pRnm = Rf2_ManObj( p, pObj, f ); - pRnm->Value = Abc_InfoHasBit( p->pCex->pData, iBit + i ); - if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI - { - assert( pObj->Value > 0 ); - pRnm->Prio = pObj->Value; - pRnm->fPPi = 1; - } - } - Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) - { - assert( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) ); - pRnm = Rf2_ManObj( p, pObj, f ); - assert( !pRnm->fPPi ); - if ( Gia_ObjIsRo(p->pGia, pObj) ) - { - if ( f == 0 ) - continue; - pRnm0 = Rf2_ManObj( p, Gia_ObjRoToRi(p->pGia, pObj), f-1 ); - pRnm->Value = pRnm0->Value; - pRnm->Prio = pRnm0->Prio; - continue; - } - if ( Gia_ObjIsCo(pObj) ) - { - pRnm0 = Rf2_ManObj( p, Gia_ObjFanin0(pObj), f ); - pRnm->Value = (pRnm0->Value ^ Gia_ObjFaninC0(pObj)); - pRnm->Prio = pRnm0->Prio; - continue; - } - assert( Gia_ObjIsAnd(pObj) ); - pRnm0 = Rf2_ManObj( p, Gia_ObjFanin0(pObj), f ); - pRnm1 = Rf2_ManObj( p, Gia_ObjFanin1(pObj), f ); - pRnm->Value = (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) & (pRnm1->Value ^ Gia_ObjFaninC1(pObj)); - if ( pRnm->Value == 1 ) - pRnm->Prio = Abc_MaxInt( pRnm0->Prio, pRnm1->Prio ); - else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRnm1->Value ^ Gia_ObjFaninC1(pObj)) == 0 ) - pRnm->Prio = Abc_MinInt( pRnm0->Prio, pRnm1->Prio ); // choice - else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 ) - pRnm->Prio = pRnm0->Prio; - else - pRnm->Prio = pRnm1->Prio; - } - } - assert( iBit == p->pCex->nBits ); - pRnm = Rf2_ManObj( p, Gia_ManPo(p->pGia, 0), p->pCex->iFrame ); - if ( pRnm->Value != 1 ) - printf( "Output value is incorrect.\n" ); - return pRnm->Prio; -} - - - -/**Function************************************************************* - - Synopsis [Performs refinement.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Rf2_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, Vec_Int_t * vObjs, Vec_Int_t * vRes ) -{ - Gia_Obj_t * pObj; - int i, f, iBit = pCex->nRegs; - Gia_ObjTerSimSet0( Gia_ManConst0(p) ); - for ( f = 0; f <= pCex->iFrame; f++, iBit += pCex->nPis ) - { - Gia_ManForEachObjVec( vMap, p, pObj, i ) - { - pObj->Value = Abc_InfoHasBit( pCex->pData, iBit + i ); - if ( !Gia_ObjIsPi(p, pObj) ) - Gia_ObjTerSimSetX( pObj ); - else if ( pObj->Value ) - Gia_ObjTerSimSet1( pObj ); - else - Gia_ObjTerSimSet0( pObj ); - } - Gia_ManForEachObjVec( vRes, p, pObj, i ) // vRes is subset of vMap - { - if ( pObj->Value ) - Gia_ObjTerSimSet1( pObj ); - else - Gia_ObjTerSimSet0( pObj ); - } - Gia_ManForEachObjVec( vObjs, p, pObj, i ) - { - if ( Gia_ObjIsCo(pObj) ) - Gia_ObjTerSimCo( pObj ); - else if ( Gia_ObjIsAnd(pObj) ) - Gia_ObjTerSimAnd( pObj ); - else if ( f == 0 ) - Gia_ObjTerSimSet0( pObj ); - else - Gia_ObjTerSimRo( p, pObj ); - } - } - Gia_ManForEachObjVec( vMap, p, pObj, i ) - pObj->Value = 0; - pObj = Gia_ManPo( p, 0 ); - if ( !Gia_ObjTerSimGet1(pObj) ) - Abc_Print( 1, "\nRefinement verification has failed!!!\n" ); -} - -/**Function************************************************************* - - Synopsis [Computes the refinement for a given counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Rf2_ManGatherFanins_rec( Rf2_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vFanins, int Depth, int RootId, int fFirst ) -{ - if ( Gia_ObjIsTravIdCurrent(p->pGia, pObj) ) - return; - Gia_ObjSetTravIdCurrent(p->pGia, pObj); - if ( pObj->fPhase && !fFirst ) - { - Vec_Int_t * vVec = Rf2_ObjVec( p, pObj ); -// if ( Vec_IntEntry( vVec, 0 ) == 0 ) -// return; - if ( Vec_IntSize(vVec) == 0 ) - Vec_IntPush( vFanins, Gia_ObjId(p->pGia, pObj) ); - Vec_IntPushUnique( vVec, RootId ); - if ( Depth == 0 ) - return; - } - if ( Gia_ObjIsPi(p->pGia, pObj) || Gia_ObjIsConst0(pObj) ) - return; - if ( Gia_ObjIsRo(p->pGia, pObj) ) - { - assert( pObj->fPhase ); - pObj = Gia_ObjRoToRi(p->pGia, pObj); - Rf2_ManGatherFanins_rec( p, Gia_ObjFanin0(pObj), vFanins, Depth - 1, RootId, 0 ); - } - else if ( Gia_ObjIsAnd(pObj) ) - { - Rf2_ManGatherFanins_rec( p, Gia_ObjFanin0(pObj), vFanins, Depth - pObj->fPhase, RootId, 0 ); - Rf2_ManGatherFanins_rec( p, Gia_ObjFanin1(pObj), vFanins, Depth - pObj->fPhase, RootId, 0 ); - } - else assert( 0 ); -} -void Rf2_ManGatherFanins( Rf2_Man_t * p, int Depth ) -{ - Vec_Int_t * vUsed; - Vec_Int_t * vVec; - Gia_Obj_t * pObj; - int i, k, Entry; - // mark PPIs - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - { - vVec = Rf2_ObjVec( p, pObj ); - assert( Vec_IntSize(vVec) == 0 ); - Vec_IntPush( vVec, 0 ); - } - // collect internal - Vec_IntClear( p->vFanins ); - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - { - if ( Gia_ObjIsPi(p->pGia, pObj) ) - continue; - Gia_ManIncrementTravId( p->pGia ); - Rf2_ManGatherFanins_rec( p, pObj, p->vFanins, Depth, i, 1 ); - } - - vUsed = Vec_IntStart( Vec_IntSize(p->vMap) ); - - // evaluate collected - printf( "\nMap (%d): ", Vec_IntSize(p->vMap) ); - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - { - vVec = Rf2_ObjVec( p, pObj ); - if ( Vec_IntSize(vVec) > 1 ) - printf( "%d=%d ", i, Vec_IntSize(vVec) - 1 ); - Vec_IntForEachEntryStart( vVec, Entry, k, 1 ) - Vec_IntAddToEntry( vUsed, Entry, 1 ); - Vec_IntClear( vVec ); - } - printf( "\n" ); - // evaluate internal - printf( "Int (%d): ", Vec_IntSize(p->vFanins) ); - Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i ) - { - vVec = Rf2_ObjVec( p, pObj ); - if ( Vec_IntSize(vVec) > 1 ) - printf( "%d=%d ", i, Vec_IntSize(vVec) ); - if ( Vec_IntSize(vVec) > 1 ) - Vec_IntForEachEntry( vVec, Entry, k ) - Vec_IntAddToEntry( vUsed, Entry, 1 ); - Vec_IntClear( vVec ); - } - printf( "\n" ); - // evaluate PPIs - Vec_IntForEachEntry( vUsed, Entry, k ) - printf( "%d ", Entry ); - printf( "\n" ); - - Vec_IntFree( vUsed ); -} - - -/**Function************************************************************* - - Synopsis [Sort, make dup- and containment-free, and filter.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Rf2_ManCountPpis( Rf2_Man_t * p ) -{ - 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 - Counter++; - return Counter; -} - -/**Function************************************************************* - - Synopsis [Sort, make dup- and containment-free, and filter.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Rf2_ManPrintVector( Vec_Int_t * p, int Num ) -{ - int i, k, Entry; - Vec_IntForEachEntry( p, Entry, i ) - { - for ( k = 0; k < Num; k++ ) - printf( "%c", '0' + ((Entry>>k) & 1) ); - printf( "\n" ); - } -} - -/**Function************************************************************* - - Synopsis [Sort, make dup- and containment-free, and filter.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Rf2_ManProcessVector( Vec_Int_t * p, int Limit ) -{ -// int Start = Vec_IntSize(p); - int Start = 0; - int i, j, k, Entry, Entry2; -// printf( "%d", Vec_IntSize(p) ); - if ( Start > 5 ) - { - printf( "Before: \n" ); - Rf2_ManPrintVector( p, 31 ); - } - - k = 0; - Vec_IntForEachEntry( p, Entry, i ) - if ( Gia_WordCountOnes((unsigned)Entry) <= Limit ) - Vec_IntWriteEntry( p, k++, Entry ); - Vec_IntShrink( p, k ); - Vec_IntSort( p, 0 ); - k = 0; - Vec_IntForEachEntry( p, Entry, i ) - { - Vec_IntForEachEntryStop( p, Entry2, j, i ) - if ( (Entry2 & Entry) == Entry2 ) // Entry2 is a subset of Entry - break; - if ( j == i ) // Entry is not contained in any Entry2 - Vec_IntWriteEntry( p, k++, Entry ); - } - Vec_IntShrink( p, k ); -// printf( "->%d ", Vec_IntSize(p) ); - if ( Start > 5 ) - { - printf( "After: \n" ); - Rf2_ManPrintVector( p, 31 ); - k = 0; - } -} - -/**Function************************************************************* - - Synopsis [Assigns a unique justifification ID for each PPI.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Rf2_ManAssignJustIds( Rf2_Man_t * p ) -{ - Gia_Obj_t * pObj; - int nPpis = Rf2_ManCountPpis( p ); - int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0); - int i, k = 0; - Vec_VecClear( p->vGrp2Ppi ); - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI - Vec_VecPushInt( p->vGrp2Ppi, (k++ / nGroupSize), i ); - printf( "Considering %d PPIs combined into %d groups of size %d.\n", k, (k-1)/nGroupSize+1, nGroupSize ); - return (k-1)/nGroupSize+1; -} - -/**Function************************************************************* - - Synopsis [Sort, make dup- and containment-free, and filter.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Rf2_ManPrintVectorSpecial( Rf2_Man_t * p, Vec_Int_t * vVec ) -{ - Gia_Obj_t * pObj; - int nPpis = Rf2_ManCountPpis( p ); - int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0); - int s, i, k, Entry, Counter; - - Vec_IntForEachEntry( vVec, Entry, s ) - { - k = 0; - Counter = 0; - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - { - if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI - { - if ( (Entry >> (k++ / nGroupSize)) & 1 ) - printf( "1" ), Counter++; - else - printf( "0" ); - } - else - printf( "-" ); - } - printf( " %3d \n", Counter ); - } -} - -/**Function************************************************************* - - Synopsis [Performs justification propagation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit ) -{ - Vec_Int_t * vVec, * vVec0, * vVec1; - Gia_Obj_t * pObj; - int f, i, k, j, Entry, Entry2, iBit = p->pCex->nRegs; - // init constant - pObj = Gia_ManConst0(p->pGia); - pObj->fMark0 = 0; - Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 ); - // iterate through the timeframes - for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis ) - { - // initialize frontier values and init justification sets - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - { - assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); - pObj->fMark0 = Abc_InfoHasBit( p->pCex->pData, iBit + i ); - Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 ); - } - // assign justification sets for PPis - Vec_VecForEachLevelInt( p->vGrp2Ppi, vVec, i ) - Vec_IntForEachEntry( vVec, Entry, k ) - { - assert( i < 31 ); - pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vMap, Entry) ); - assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 1 ); - Vec_IntAddToEntry( Rf2_ObjVec(p, pObj), 0, (1 << i) ); - } - // propagate internal nodes - Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) - { - pObj->fMark0 = 0; - vVec = Rf2_ObjVec(p, pObj); - Vec_IntClear( vVec ); - if ( Gia_ObjIsRo(p->pGia, pObj) ) - { - if ( f == 0 ) - { - Vec_IntPush( vVec, 0 ); - continue; - } - pObj->fMark0 = Gia_ObjRoToRi(p->pGia, pObj)->fMark0; - vVec0 = Rf2_ObjVec( p, Gia_ObjRoToRi(p->pGia, pObj) ); - Vec_IntAppend( vVec, vVec0 ); - continue; - } - if ( Gia_ObjIsCo(pObj) ) - { - pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)); - vVec0 = Rf2_ObjVec( p, Gia_ObjFanin0(pObj) ); - Vec_IntAppend( vVec, vVec0 ); - continue; - } - assert( Gia_ObjIsAnd(pObj) ); - vVec0 = Rf2_ObjVec(p, Gia_ObjFanin0(pObj)); - vVec1 = Rf2_ObjVec(p, Gia_ObjFanin1(pObj)); - pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); - if ( pObj->fMark0 == 1 ) - { - Vec_IntForEachEntry( vVec0, Entry, k ) - Vec_IntForEachEntry( vVec1, Entry2, j ) - Vec_IntPush( vVec, Entry | Entry2 ); - Rf2_ManProcessVector( vVec, Limit ); - } - else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 ) - { - Vec_IntAppend( vVec, vVec0 ); - Vec_IntAppend( vVec, vVec1 ); - Rf2_ManProcessVector( vVec, Limit ); - } - else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 ) - Vec_IntAppend( vVec, vVec0 ); - else - Vec_IntAppend( vVec, vVec1 ); - } - } - assert( iBit == p->pCex->nBits ); - if ( Gia_ManPo(p->pGia, 0)->fMark0 != 1 ) - printf( "Output value is incorrect.\n" ); - return Rf2_ObjVec(p, Gia_ManPo(p->pGia, 0)); -} - -/**Function************************************************************* - - Synopsis [Performs justification propagation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Rf2_ManBounds( Rf2_Man_t * p ) -{ - Gia_Obj_t * pObj; - int f, i, iBit = p->pCex->nRegs; - // init constant - pObj = Gia_ManConst0(p->pGia); - pObj->fMark0 = 0; - Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) ); - // iterate through the timeframes - for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis ) - { - // initialize frontier values and init justification sets - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - { - assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); - pObj->fMark0 = Abc_InfoHasBit( p->pCex->pData, iBit + i ); - Rf2_ObjStart( p, pObj, i ); - } - // propagate internal nodes - Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) - { - pObj->fMark0 = 0; - Rf2_ObjClear( p, pObj ); - if ( Gia_ObjIsRo(p->pGia, pObj) ) - { - if ( f == 0 ) - { - Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + i ); - continue; - } - pObj->fMark0 = Gia_ObjRoToRi(p->pGia, pObj)->fMark0; - Rf2_ObjCopy( p, pObj, Gia_ObjRoToRi(p->pGia, pObj) ); - continue; - } - if ( Gia_ObjIsCo(pObj) ) - { - pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)); - Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) ); - continue; - } - assert( Gia_ObjIsAnd(pObj) ); - pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); - if ( pObj->fMark0 == 1 ) - Rf2_ObjDeriveAnd( p, pObj, 1 ); - else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 ) - Rf2_ObjDeriveAnd( p, pObj, 0 ); - else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 ) - Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) ); - else - Rf2_ObjCopy( p, pObj, Gia_ObjFanin1(pObj) ); - } - } - assert( iBit == p->pCex->nBits ); - if ( Gia_ManPo(p->pGia, 0)->fMark0 != 1 ) - printf( "Output value is incorrect.\n" ); - - printf( "Bounds: \n" ); - Rf2_ObjPrint( p, Gia_ManPo(p->pGia, 0) ); -} - -/**Function************************************************************* - - Synopsis [Computes the refinement for a given counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose ) -{ - Vec_Int_t * vJusts; -// Vec_Int_t * vSelected = Vec_IntAlloc( 100 ); - Vec_Int_t * vSelected = NULL; - clock_t clk, clk2 = clock(); - int nGroups; - p->nCalls++; - // initialize - p->pCex = pCex; - p->vMap = vMap; - p->fPropFanout = fPropFanout; - p->fVerbose = fVerbose; - // collects used objects - Rf2_ManCollect( p ); - // collect reconvergence points -// Rf2_ManGatherFanins( p, 2 ); - // propagate justification IDs - nGroups = Rf2_ManAssignJustIds( p ); - vJusts = Rf2_ManPropagate( p, 32 ); - -// printf( "\n" ); -// Rf2_ManPrintVector( vJusts, nGroups ); - Rf2_ManPrintVectorSpecial( p, vJusts ); - if ( Vec_IntSize(vJusts) == 0 ) - { - printf( "Empty set of justifying subsets.\n" ); - return NULL; - } - -// p->nMapWords = Abc_BitWordNum( Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) + 1 ); // Map + Flops + Const -// Rf2_ManBounds( p ); - - // select the result -// Abc_PrintTime( 1, "Time", clock() - clk2 ); - - // verify (empty) refinement - clk = clock(); -// Rf2_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected ); -// Vec_IntUniqify( vSelected ); -// Vec_IntReverseOrder( vSelected ); - p->timeVer += clock() - clk; - p->timeTotal += clock() - clk2; -// p->nRefines += Vec_IntSize(vSelected); - return vSelected; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/abs/absRef2.h b/src/proof/abs/absRef2.h deleted file mode 100644 index df7774c0..00000000 --- a/src/proof/abs/absRef2.h +++ /dev/null @@ -1,67 +0,0 @@ -/**CFile**************************************************************** - - FileName [absRef2.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Abstraction package.] - - Synopsis [Refinement manager.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: absRef2.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef ABC__proof_abs__AbsRef2_h -#define ABC__proof_abs__AbsRef2_h - - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -ABC_NAMESPACE_HEADER_START - - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Rf2_Man_t_ Rf2_Man_t; // refinement manager - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== giaAbsRef.c ===========================================================*/ -extern Rf2_Man_t * Rf2_ManStart( Gia_Man_t * pGia ); -extern void Rf2_ManStop( Rf2_Man_t * p, int fProfile ); -extern double Rf2_ManMemoryUsage( Rf2_Man_t * p ); -extern Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose ); - - - -ABC_NAMESPACE_HEADER_END - - - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/proof/abs/absRefJ.c b/src/proof/abs/absRefJ.c new file mode 100644 index 00000000..aa5ea7bb --- /dev/null +++ b/src/proof/abs/absRefJ.c @@ -0,0 +1,916 @@ +/**CFile**************************************************************** + + FileName [absRef2.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Abstraction package.] + + Synopsis [Refinement manager to compute all justifying subsets.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: absRef2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abs.h" +#include "absRef2.h" + +ABC_NAMESPACE_IMPL_START + +/* + Description of the refinement manager + + This refinement manager should be + * started by calling Rf2_ManStart() + this procedure takes one argument, the user's seq miter as a GIA manager + - the manager should have only one property output + - this manager should not change while the refinement manager is alive + - it cannot be used by external applications for any purpose + - when the refinement manager stop, GIA manager is the same as at the beginning + - in the meantime, it will have some data-structures attached to its nodes... + * stopped by calling Rf2_ManStop() + * between starting and stopping, refinements are obtained by calling Rf2_ManRefine() + + Procedure Rf2_ManRefine() takes the following arguments: + * the refinement manager previously started by Rf2_ManStart() + * counter-example (CEX) obtained by abstracting some logic of GIA + * mapping (vMap) of inputs of the CEX into the object IDs of the GIA manager + - only PI, flop outputs, and internal AND nodes can be used in vMap + - the ordering of objects in vMap is not important + - however, the index of a non-PI object in vMap is used as its priority + (the smaller the index, the more likely this non-PI object apears in a refinement) + - only the logic between PO and the objects listed in vMap is traversed by the manager + (as a result, GIA can be arbitrarily large, but only objects used in the abstraction + and the pseudo-PI, that is, objects in the cut, will be visited by the manager) + * flag fPropFanout defines whether value propagation is done through the fanout + - it this flag is enabled, theoretically refinement should be better (the result smaller) + * flag fVerbose may print some statistics + + The refinement manager returns a minimal-size array of integer IDs of GIA objects + which should be added to the abstraction to possibly prevent the given counter-example + - only flop output and internal AND nodes from vMap may appear in the resulting array + - if the resulting array is empty, the CEX is a true CEX + (in other words, non-PI objects are not needed to set the PO value to 1) + + Verification of the selected refinement is performed by + - initializing all PI objects in vMap to value 0 or 1 they have in the CEX + - initializing all remaining objects in vMap to value X + - initializing objects used in the refiment to value 0 or 1 they have in the CEX + - simulating through as many timeframes as required by the CEX + - if the PO value in the last frame is 1, the refinement is correct + (however, the minimality of the refinement is not currently checked) + +*/ + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Rf2_Obj_t_ Rf2_Obj_t; // refinement object +struct Rf2_Obj_t_ +{ + unsigned Value : 1; // binary value + unsigned fVisit : 1; // visited object + unsigned fPPi : 1; // PPI object + unsigned Prio : 24; // priority (0 - highest) +}; + +struct Rf2_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_Int_t * vFanins; // fanins of the PPI nodes + Vec_Int_t * pvVecs; // vectors of integers for each object + Vec_Vec_t * vGrp2Ppi; // for each node, the set of PPIs to include + int nMapWords; + // internal data + Rf2_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 + // 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 Rf2_Obj_t * Rf2_ManObj( Rf2_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 Vec_Int_t * Rf2_ObjVec( Rf2_Man_t * p, Gia_Obj_t * pObj ) +{ + return p->pvVecs + Gia_ObjId(p->pGia, pObj); +} + + +static inline unsigned * Rf2_ObjA( Rf2_Man_t * p, Gia_Obj_t * pObj ) +{ + return (unsigned *)Vec_IntArray(Rf2_ObjVec(p, pObj)); +} +static inline unsigned * Rf2_ObjN( Rf2_Man_t * p, Gia_Obj_t * pObj ) +{ + return (unsigned *)Vec_IntArray(Rf2_ObjVec(p, pObj)) + p->nMapWords; +} +static inline void Rf2_ObjClear( Rf2_Man_t * p, Gia_Obj_t * pObj ) +{ + Vec_IntFill( Rf2_ObjVec(p, pObj), 2*p->nMapWords, 0 ); +} +static inline void Rf2_ObjStart( Rf2_Man_t * p, Gia_Obj_t * pObj, int i ) +{ + Vec_Int_t * vVec = Rf2_ObjVec(p, pObj); + int w; + Vec_IntClear( vVec ); + for ( w = 0; w < p->nMapWords; w++ ) + Vec_IntPush( vVec, 0 ); + for ( w = 0; w < p->nMapWords; w++ ) + Vec_IntPush( vVec, ~0 ); + Abc_InfoSetBit( Rf2_ObjA(p, pObj), i ); + Abc_InfoXorBit( Rf2_ObjN(p, pObj), i ); +} +static inline void Rf2_ObjCopy( Rf2_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) +{ + assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 2*p->nMapWords ); + memcpy( Rf2_ObjA(p, pObj), Rf2_ObjA(p, pFanin), sizeof(unsigned) * 2 * p->nMapWords ); +} +static inline void Rf2_ObjDeriveAnd( Rf2_Man_t * p, Gia_Obj_t * pObj, int One ) +{ + unsigned * pInfo, * pInfo0, * pInfo1; + int i; + assert( Gia_ObjIsAnd(pObj) ); + assert( One == (int)pObj->fMark0 ); + assert( One == (int)(Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) ); + assert( One == (int)(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) ); + assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 2*p->nMapWords ); + + pInfo = Rf2_ObjA( p, pObj ); + pInfo0 = Rf2_ObjA( p, Gia_ObjFanin0(pObj) ); + pInfo1 = Rf2_ObjA( p, Gia_ObjFanin1(pObj) ); + for ( i = 0; i < p->nMapWords; i++ ) + pInfo[i] = One ? (pInfo0[i] & pInfo1[i]) : (pInfo0[i] | pInfo1[i]); + + pInfo = Rf2_ObjN( p, pObj ); + pInfo0 = Rf2_ObjN( p, Gia_ObjFanin0(pObj) ); + pInfo1 = Rf2_ObjN( p, Gia_ObjFanin1(pObj) ); + for ( i = 0; i < p->nMapWords; i++ ) + pInfo[i] = One ? (pInfo0[i] | pInfo1[i]) : (pInfo0[i] & pInfo1[i]); +} +static inline void Rf2_ObjPrint( Rf2_Man_t * p, Gia_Obj_t * pRoot ) +{ + Gia_Obj_t * pObj; + unsigned * pInfo; + int i; + pInfo = Rf2_ObjA( p, pRoot ); + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + if ( !Gia_ObjIsPi(p->pGia, pObj) ) + printf( "%d", Abc_InfoHasBit(pInfo, i) ); + printf( "\n" ); + pInfo = Rf2_ObjN( p, pRoot ); + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + if ( !Gia_ObjIsPi(p->pGia, pObj) ) + printf( "%d", !Abc_InfoHasBit(pInfo, i) ); + printf( "\n" ); + +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates a new manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Rf2_Man_t * Rf2_ManStart( Gia_Man_t * pGia ) +{ + Rf2_Man_t * p; + assert( Gia_ManPoNum(pGia) == 1 ); + p = ABC_CALLOC( Rf2_Man_t, 1 ); + p->pGia = pGia; + p->vObjs = Vec_IntAlloc( 1000 ); + p->vFanins = Vec_IntAlloc( 1000 ); + p->pvVecs = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(pGia) ); + p->vGrp2Ppi = Vec_VecStart( 100 ); + Gia_ManCleanMark0(pGia); + Gia_ManCleanMark1(pGia); + return p; +} +void Rf2_ManStop( Rf2_Man_t * p, int fProfile ) +{ + if ( !p ) return; + // print runtime statistics + if ( fProfile && p->nCalls ) + { + double MemGia = sizeof(Gia_Man_t) + sizeof(Gia_Obj_t) * p->pGia->nObjsAlloc + sizeof(int) * p->pGia->nTravIdsAlloc; + double MemOther = sizeof(Rf2_Man_t) + sizeof(Rf2_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs); + clock_t timeOther = p->timeTotal - p->timeFwd - p->timeBwd - p->timeVer; + printf( "Abstraction refinement runtime statistics:\n" ); + ABC_PRTP( "Sensetization", p->timeFwd, p->timeTotal ); + ABC_PRTP( "Justification", p->timeBwd, p->timeTotal ); + ABC_PRTP( "Verification ", p->timeVer, p->timeTotal ); + ABC_PRTP( "Other ", timeOther, p->timeTotal ); + ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + printf( "Total calls = %d. Average refine = %.1f. GIA mem = %.3f MB. Other mem = %.3f MB.\n", + p->nCalls, 1.0*p->nRefines/p->nCalls, MemGia/(1<<20), MemOther/(1<<20) ); + } + Vec_IntFree( p->vObjs ); + Vec_IntFree( p->vFanins ); + Vec_VecFree( p->vGrp2Ppi ); + ABC_FREE( p->pvVecs ); + ABC_FREE( p ); +} +double Rf2_ManMemoryUsage( Rf2_Man_t * p ) +{ + return (double)(sizeof(Rf2_Man_t) + sizeof(Vec_Int_t) * Gia_ManObjNum(p->pGia)); +} + + +/**Function************************************************************* + + Synopsis [Collect internal objects to be used in value propagation.] + + Description [Resulting array vObjs contains RO, AND, PO/RI in a topo order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rf2_ManCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjs ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( Gia_ObjIsCo(pObj) ) + Rf2_ManCollect_rec( p, Gia_ObjFanin0(pObj), vObjs ); + else if ( Gia_ObjIsAnd(pObj) ) + { + Rf2_ManCollect_rec( p, Gia_ObjFanin0(pObj), vObjs ); + Rf2_ManCollect_rec( p, Gia_ObjFanin1(pObj), vObjs ); + } + else if ( !Gia_ObjIsRo(p, pObj) ) + assert( 0 ); + Vec_IntPush( vObjs, Gia_ObjId(p, pObj) ); +} +void Rf2_ManCollect( Rf2_Man_t * p ) +{ + Gia_Obj_t * pObj = NULL; + int i; + // mark const/PIs/PPIs + Gia_ManIncrementTravId( p->pGia ); + Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) ); + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + { + assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); + Gia_ObjSetTravIdCurrent( p->pGia, pObj ); + } + // collect objects + Vec_IntClear( p->vObjs ); + Rf2_ManCollect_rec( p->pGia, Gia_ManPo(p->pGia, 0), p->vObjs ); + Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) + if ( Gia_ObjIsRo(p->pGia, pObj) ) + Rf2_ManCollect_rec( p->pGia, Gia_ObjRoToRi(p->pGia, pObj), p->vObjs ); + // the last object should be a CO + assert( Gia_ObjIsCo(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Performs sensitization analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rf2_ManSensitize( Rf2_Man_t * p ) +{ + Rf2_Obj_t * pRnm, * pRnm0, * pRnm1; + Gia_Obj_t * pObj; + int f, i, iBit = p->pCex->nRegs; + // const0 is initialized automatically in all timeframes + for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis ) + { + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + { + assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); + pRnm = Rf2_ManObj( p, pObj, f ); + pRnm->Value = Abc_InfoHasBit( p->pCex->pData, iBit + i ); + if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI + { + assert( pObj->Value > 0 ); + pRnm->Prio = pObj->Value; + pRnm->fPPi = 1; + } + } + Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) + { + assert( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) ); + pRnm = Rf2_ManObj( p, pObj, f ); + assert( !pRnm->fPPi ); + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( f == 0 ) + continue; + pRnm0 = Rf2_ManObj( p, Gia_ObjRoToRi(p->pGia, pObj), f-1 ); + pRnm->Value = pRnm0->Value; + pRnm->Prio = pRnm0->Prio; + continue; + } + if ( Gia_ObjIsCo(pObj) ) + { + pRnm0 = Rf2_ManObj( p, Gia_ObjFanin0(pObj), f ); + pRnm->Value = (pRnm0->Value ^ Gia_ObjFaninC0(pObj)); + pRnm->Prio = pRnm0->Prio; + continue; + } + assert( Gia_ObjIsAnd(pObj) ); + pRnm0 = Rf2_ManObj( p, Gia_ObjFanin0(pObj), f ); + pRnm1 = Rf2_ManObj( p, Gia_ObjFanin1(pObj), f ); + pRnm->Value = (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) & (pRnm1->Value ^ Gia_ObjFaninC1(pObj)); + if ( pRnm->Value == 1 ) + pRnm->Prio = Abc_MaxInt( pRnm0->Prio, pRnm1->Prio ); + else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRnm1->Value ^ Gia_ObjFaninC1(pObj)) == 0 ) + pRnm->Prio = Abc_MinInt( pRnm0->Prio, pRnm1->Prio ); // choice + else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 ) + pRnm->Prio = pRnm0->Prio; + else + pRnm->Prio = pRnm1->Prio; + } + } + assert( iBit == p->pCex->nBits ); + pRnm = Rf2_ManObj( p, Gia_ManPo(p->pGia, 0), p->pCex->iFrame ); + if ( pRnm->Value != 1 ) + printf( "Output value is incorrect.\n" ); + return pRnm->Prio; +} + + + +/**Function************************************************************* + + Synopsis [Performs refinement.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rf2_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, Vec_Int_t * vObjs, Vec_Int_t * vRes ) +{ + Gia_Obj_t * pObj; + int i, f, iBit = pCex->nRegs; + Gia_ObjTerSimSet0( Gia_ManConst0(p) ); + for ( f = 0; f <= pCex->iFrame; f++, iBit += pCex->nPis ) + { + Gia_ManForEachObjVec( vMap, p, pObj, i ) + { + pObj->Value = Abc_InfoHasBit( pCex->pData, iBit + i ); + if ( !Gia_ObjIsPi(p, pObj) ) + Gia_ObjTerSimSetX( pObj ); + else if ( pObj->Value ) + Gia_ObjTerSimSet1( pObj ); + else + Gia_ObjTerSimSet0( pObj ); + } + Gia_ManForEachObjVec( vRes, p, pObj, i ) // vRes is subset of vMap + { + if ( pObj->Value ) + Gia_ObjTerSimSet1( pObj ); + else + Gia_ObjTerSimSet0( pObj ); + } + Gia_ManForEachObjVec( vObjs, p, pObj, i ) + { + if ( Gia_ObjIsCo(pObj) ) + Gia_ObjTerSimCo( pObj ); + else if ( Gia_ObjIsAnd(pObj) ) + Gia_ObjTerSimAnd( pObj ); + else if ( f == 0 ) + Gia_ObjTerSimSet0( pObj ); + else + Gia_ObjTerSimRo( p, pObj ); + } + } + Gia_ManForEachObjVec( vMap, p, pObj, i ) + pObj->Value = 0; + pObj = Gia_ManPo( p, 0 ); + if ( !Gia_ObjTerSimGet1(pObj) ) + Abc_Print( 1, "\nRefinement verification has failed!!!\n" ); +} + +/**Function************************************************************* + + Synopsis [Computes the refinement for a given counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rf2_ManGatherFanins_rec( Rf2_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vFanins, int Depth, int RootId, int fFirst ) +{ + if ( Gia_ObjIsTravIdCurrent(p->pGia, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p->pGia, pObj); + if ( pObj->fPhase && !fFirst ) + { + Vec_Int_t * vVec = Rf2_ObjVec( p, pObj ); +// if ( Vec_IntEntry( vVec, 0 ) == 0 ) +// return; + if ( Vec_IntSize(vVec) == 0 ) + Vec_IntPush( vFanins, Gia_ObjId(p->pGia, pObj) ); + Vec_IntPushUnique( vVec, RootId ); + if ( Depth == 0 ) + return; + } + if ( Gia_ObjIsPi(p->pGia, pObj) || Gia_ObjIsConst0(pObj) ) + return; + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + assert( pObj->fPhase ); + pObj = Gia_ObjRoToRi(p->pGia, pObj); + Rf2_ManGatherFanins_rec( p, Gia_ObjFanin0(pObj), vFanins, Depth - 1, RootId, 0 ); + } + else if ( Gia_ObjIsAnd(pObj) ) + { + Rf2_ManGatherFanins_rec( p, Gia_ObjFanin0(pObj), vFanins, Depth - pObj->fPhase, RootId, 0 ); + Rf2_ManGatherFanins_rec( p, Gia_ObjFanin1(pObj), vFanins, Depth - pObj->fPhase, RootId, 0 ); + } + else assert( 0 ); +} +void Rf2_ManGatherFanins( Rf2_Man_t * p, int Depth ) +{ + Vec_Int_t * vUsed; + Vec_Int_t * vVec; + Gia_Obj_t * pObj; + int i, k, Entry; + // mark PPIs + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + { + vVec = Rf2_ObjVec( p, pObj ); + assert( Vec_IntSize(vVec) == 0 ); + Vec_IntPush( vVec, 0 ); + } + // collect internal + Vec_IntClear( p->vFanins ); + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + { + if ( Gia_ObjIsPi(p->pGia, pObj) ) + continue; + Gia_ManIncrementTravId( p->pGia ); + Rf2_ManGatherFanins_rec( p, pObj, p->vFanins, Depth, i, 1 ); + } + + vUsed = Vec_IntStart( Vec_IntSize(p->vMap) ); + + // evaluate collected + printf( "\nMap (%d): ", Vec_IntSize(p->vMap) ); + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + { + vVec = Rf2_ObjVec( p, pObj ); + if ( Vec_IntSize(vVec) > 1 ) + printf( "%d=%d ", i, Vec_IntSize(vVec) - 1 ); + Vec_IntForEachEntryStart( vVec, Entry, k, 1 ) + Vec_IntAddToEntry( vUsed, Entry, 1 ); + Vec_IntClear( vVec ); + } + printf( "\n" ); + // evaluate internal + printf( "Int (%d): ", Vec_IntSize(p->vFanins) ); + Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i ) + { + vVec = Rf2_ObjVec( p, pObj ); + if ( Vec_IntSize(vVec) > 1 ) + printf( "%d=%d ", i, Vec_IntSize(vVec) ); + if ( Vec_IntSize(vVec) > 1 ) + Vec_IntForEachEntry( vVec, Entry, k ) + Vec_IntAddToEntry( vUsed, Entry, 1 ); + Vec_IntClear( vVec ); + } + printf( "\n" ); + // evaluate PPIs + Vec_IntForEachEntry( vUsed, Entry, k ) + printf( "%d ", Entry ); + printf( "\n" ); + + Vec_IntFree( vUsed ); +} + + +/**Function************************************************************* + + Synopsis [Sort, make dup- and containment-free, and filter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Rf2_ManCountPpis( Rf2_Man_t * p ) +{ + 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 + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Sort, make dup- and containment-free, and filter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Rf2_ManPrintVector( Vec_Int_t * p, int Num ) +{ + int i, k, Entry; + Vec_IntForEachEntry( p, Entry, i ) + { + for ( k = 0; k < Num; k++ ) + printf( "%c", '0' + ((Entry>>k) & 1) ); + printf( "\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Sort, make dup- and containment-free, and filter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Rf2_ManProcessVector( Vec_Int_t * p, int Limit ) +{ +// int Start = Vec_IntSize(p); + int Start = 0; + int i, j, k, Entry, Entry2; +// printf( "%d", Vec_IntSize(p) ); + if ( Start > 5 ) + { + printf( "Before: \n" ); + Rf2_ManPrintVector( p, 31 ); + } + + k = 0; + Vec_IntForEachEntry( p, Entry, i ) + if ( Gia_WordCountOnes((unsigned)Entry) <= Limit ) + Vec_IntWriteEntry( p, k++, Entry ); + Vec_IntShrink( p, k ); + Vec_IntSort( p, 0 ); + k = 0; + Vec_IntForEachEntry( p, Entry, i ) + { + Vec_IntForEachEntryStop( p, Entry2, j, i ) + if ( (Entry2 & Entry) == Entry2 ) // Entry2 is a subset of Entry + break; + if ( j == i ) // Entry is not contained in any Entry2 + Vec_IntWriteEntry( p, k++, Entry ); + } + Vec_IntShrink( p, k ); +// printf( "->%d ", Vec_IntSize(p) ); + if ( Start > 5 ) + { + printf( "After: \n" ); + Rf2_ManPrintVector( p, 31 ); + k = 0; + } +} + +/**Function************************************************************* + + Synopsis [Assigns a unique justifification ID for each PPI.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rf2_ManAssignJustIds( Rf2_Man_t * p ) +{ + Gia_Obj_t * pObj; + int nPpis = Rf2_ManCountPpis( p ); + int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0); + int i, k = 0; + Vec_VecClear( p->vGrp2Ppi ); + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI + Vec_VecPushInt( p->vGrp2Ppi, (k++ / nGroupSize), i ); + printf( "Considering %d PPIs combined into %d groups of size %d.\n", k, (k-1)/nGroupSize+1, nGroupSize ); + return (k-1)/nGroupSize+1; +} + +/**Function************************************************************* + + Synopsis [Sort, make dup- and containment-free, and filter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Rf2_ManPrintVectorSpecial( Rf2_Man_t * p, Vec_Int_t * vVec ) +{ + Gia_Obj_t * pObj; + int nPpis = Rf2_ManCountPpis( p ); + int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0); + int s, i, k, Entry, Counter; + + Vec_IntForEachEntry( vVec, Entry, s ) + { + k = 0; + Counter = 0; + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + { + if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI + { + if ( (Entry >> (k++ / nGroupSize)) & 1 ) + printf( "1" ), Counter++; + else + printf( "0" ); + } + else + printf( "-" ); + } + printf( " %3d \n", Counter ); + } +} + +/**Function************************************************************* + + Synopsis [Performs justification propagation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit ) +{ + Vec_Int_t * vVec, * vVec0, * vVec1; + Gia_Obj_t * pObj; + int f, i, k, j, Entry, Entry2, iBit = p->pCex->nRegs; + // init constant + pObj = Gia_ManConst0(p->pGia); + pObj->fMark0 = 0; + Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 ); + // iterate through the timeframes + for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis ) + { + // initialize frontier values and init justification sets + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + { + assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); + pObj->fMark0 = Abc_InfoHasBit( p->pCex->pData, iBit + i ); + Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 ); + } + // assign justification sets for PPis + Vec_VecForEachLevelInt( p->vGrp2Ppi, vVec, i ) + Vec_IntForEachEntry( vVec, Entry, k ) + { + assert( i < 31 ); + pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vMap, Entry) ); + assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 1 ); + Vec_IntAddToEntry( Rf2_ObjVec(p, pObj), 0, (1 << i) ); + } + // propagate internal nodes + Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) + { + pObj->fMark0 = 0; + vVec = Rf2_ObjVec(p, pObj); + Vec_IntClear( vVec ); + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( f == 0 ) + { + Vec_IntPush( vVec, 0 ); + continue; + } + pObj->fMark0 = Gia_ObjRoToRi(p->pGia, pObj)->fMark0; + vVec0 = Rf2_ObjVec( p, Gia_ObjRoToRi(p->pGia, pObj) ); + Vec_IntAppend( vVec, vVec0 ); + continue; + } + if ( Gia_ObjIsCo(pObj) ) + { + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)); + vVec0 = Rf2_ObjVec( p, Gia_ObjFanin0(pObj) ); + Vec_IntAppend( vVec, vVec0 ); + continue; + } + assert( Gia_ObjIsAnd(pObj) ); + vVec0 = Rf2_ObjVec(p, Gia_ObjFanin0(pObj)); + vVec1 = Rf2_ObjVec(p, Gia_ObjFanin1(pObj)); + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + if ( pObj->fMark0 == 1 ) + { + Vec_IntForEachEntry( vVec0, Entry, k ) + Vec_IntForEachEntry( vVec1, Entry2, j ) + Vec_IntPush( vVec, Entry | Entry2 ); + Rf2_ManProcessVector( vVec, Limit ); + } + else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 ) + { + Vec_IntAppend( vVec, vVec0 ); + Vec_IntAppend( vVec, vVec1 ); + Rf2_ManProcessVector( vVec, Limit ); + } + else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 ) + Vec_IntAppend( vVec, vVec0 ); + else + Vec_IntAppend( vVec, vVec1 ); + } + } + assert( iBit == p->pCex->nBits ); + if ( Gia_ManPo(p->pGia, 0)->fMark0 != 1 ) + printf( "Output value is incorrect.\n" ); + return Rf2_ObjVec(p, Gia_ManPo(p->pGia, 0)); +} + +/**Function************************************************************* + + Synopsis [Performs justification propagation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Rf2_ManBounds( Rf2_Man_t * p ) +{ + Gia_Obj_t * pObj; + int f, i, iBit = p->pCex->nRegs; + // init constant + pObj = Gia_ManConst0(p->pGia); + pObj->fMark0 = 0; + Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) ); + // iterate through the timeframes + for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis ) + { + // initialize frontier values and init justification sets + Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) + { + assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); + pObj->fMark0 = Abc_InfoHasBit( p->pCex->pData, iBit + i ); + Rf2_ObjStart( p, pObj, i ); + } + // propagate internal nodes + Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) + { + pObj->fMark0 = 0; + Rf2_ObjClear( p, pObj ); + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( f == 0 ) + { + Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + i ); + continue; + } + pObj->fMark0 = Gia_ObjRoToRi(p->pGia, pObj)->fMark0; + Rf2_ObjCopy( p, pObj, Gia_ObjRoToRi(p->pGia, pObj) ); + continue; + } + if ( Gia_ObjIsCo(pObj) ) + { + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)); + Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) ); + continue; + } + assert( Gia_ObjIsAnd(pObj) ); + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + if ( pObj->fMark0 == 1 ) + Rf2_ObjDeriveAnd( p, pObj, 1 ); + else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 ) + Rf2_ObjDeriveAnd( p, pObj, 0 ); + else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 ) + Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) ); + else + Rf2_ObjCopy( p, pObj, Gia_ObjFanin1(pObj) ); + } + } + assert( iBit == p->pCex->nBits ); + if ( Gia_ManPo(p->pGia, 0)->fMark0 != 1 ) + printf( "Output value is incorrect.\n" ); + + printf( "Bounds: \n" ); + Rf2_ObjPrint( p, Gia_ManPo(p->pGia, 0) ); +} + +/**Function************************************************************* + + Synopsis [Computes the refinement for a given counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose ) +{ + Vec_Int_t * vJusts; +// Vec_Int_t * vSelected = Vec_IntAlloc( 100 ); + Vec_Int_t * vSelected = NULL; + clock_t clk, clk2 = clock(); + int nGroups; + p->nCalls++; + // initialize + p->pCex = pCex; + p->vMap = vMap; + p->fPropFanout = fPropFanout; + p->fVerbose = fVerbose; + // collects used objects + Rf2_ManCollect( p ); + // collect reconvergence points +// Rf2_ManGatherFanins( p, 2 ); + // propagate justification IDs + nGroups = Rf2_ManAssignJustIds( p ); + vJusts = Rf2_ManPropagate( p, 32 ); + +// printf( "\n" ); +// Rf2_ManPrintVector( vJusts, nGroups ); + Rf2_ManPrintVectorSpecial( p, vJusts ); + if ( Vec_IntSize(vJusts) == 0 ) + { + printf( "Empty set of justifying subsets.\n" ); + return NULL; + } + +// p->nMapWords = Abc_BitWordNum( Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) + 1 ); // Map + Flops + Const +// Rf2_ManBounds( p ); + + // select the result +// Abc_PrintTime( 1, "Time", clock() - clk2 ); + + // verify (empty) refinement + clk = clock(); +// Rf2_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected ); +// Vec_IntUniqify( vSelected ); +// Vec_IntReverseOrder( vSelected ); + p->timeVer += clock() - clk; + p->timeTotal += clock() - clk2; +// p->nRefines += Vec_IntSize(vSelected); + return vSelected; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/abs/absRefJ.h b/src/proof/abs/absRefJ.h new file mode 100644 index 00000000..0c56d2dd --- /dev/null +++ b/src/proof/abs/absRefJ.h @@ -0,0 +1,67 @@ +/**CFile**************************************************************** + + FileName [absRef2.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Abstraction package.] + + Synopsis [Refinement manager to compute all justifying subsets.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: absRef2.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__proof_abs__AbsRef2_h +#define ABC__proof_abs__AbsRef2_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Rf2_Man_t_ Rf2_Man_t; // refinement manager + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== giaAbsRef.c ===========================================================*/ +extern Rf2_Man_t * Rf2_ManStart( Gia_Man_t * pGia ); +extern void Rf2_ManStop( Rf2_Man_t * p, int fProfile ); +extern double Rf2_ManMemoryUsage( Rf2_Man_t * p ); +extern Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose ); + + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/proof/abs/absRefSelect.c b/src/proof/abs/absRefSelect.c new file mode 100644 index 00000000..871eb79b --- /dev/null +++ b/src/proof/abs/absRefSelect.c @@ -0,0 +1,220 @@ +/**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 + diff --git a/src/proof/abs/module.make b/src/proof/abs/module.make index 4e652afd..4dd463e2 100644 --- a/src/proof/abs/module.make +++ b/src/proof/abs/module.make @@ -10,6 +10,6 @@ SRC += src/proof/abs/abs.c \ src/proof/abs/absOut.c \ src/proof/abs/absPth.c \ src/proof/abs/absRef.c \ - src/proof/abs/absRef2.c \ + src/proof/abs/absRefSelect.c \ src/proof/abs/absVta.c \ src/proof/abs/absUtil.c -- cgit v1.2.3