diff options
Diffstat (limited to 'src/aig/gia/giaAbsRef.c')
| -rw-r--r-- | src/aig/gia/giaAbsRef.c | 239 |
1 files changed, 235 insertions, 4 deletions
diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c index 5b7bcee2..21a87c33 100644 --- a/src/aig/gia/giaAbsRef.c +++ b/src/aig/gia/giaAbsRef.c @@ -77,6 +77,7 @@ 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) }; @@ -91,6 +92,8 @@ struct Rnm_Man_t_ 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 // internal data Rnm_Obj_t * pObjs; // refinement objects int nObjs; // the number of used objects @@ -98,6 +101,7 @@ struct Rnm_Man_t_ 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 @@ -114,6 +118,17 @@ static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f ) 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; } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -136,6 +151,8 @@ Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia ) p = ABC_CALLOC( Rnm_Man_t, 1 ); p->pGia = pGia; p->vObjs = Vec_IntAlloc( 100 ); + p->vCounts = Vec_StrStart( Gia_ManObjNum(pGia) ); + p->vFanins = Vec_IntAlloc( 100 ); p->nObjsAlloc = 10000; p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc ); if ( p->pGia->vFanout == NULL ) @@ -168,6 +185,8 @@ void Rnm_ManStop( Rnm_Man_t * p, int fProfile ) Gia_ManCleanMark1(p->pGia); Gia_ManStaticFanoutStop(p->pGia); // Gia_ManSetPhase(p->pGia); + Vec_StrFree( p->vCounts ); + Vec_IntFree( p->vFanins ); Vec_IntFree( p->vObjs ); ABC_FREE( p->pObjs ); ABC_FREE( p ); @@ -332,6 +351,11 @@ 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 ) + { + Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1; + p->nVisited++; + } if ( pRnm->fPPi ) { assert( (int)pRnm->Prio > 0 ); @@ -383,7 +407,14 @@ void Rnm_ManJustify_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSe if ( p->fPropFanout ) Rnm_ManJustifyPropFanout_rec( p, pObj, f, vSelect ); else + { pRnm->fVisit = 1; + if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 ) + { + Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1; + p->nVisited++; + } + } if ( pRnm->fPPi ) { assert( (int)pRnm->Prio > 0 ); @@ -507,6 +538,177 @@ void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap /**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.] Description [] @@ -518,8 +720,11 @@ void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap ***********************************************************************/ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose ) { + int fVerify = 0; Vec_Int_t * vSelected = Vec_IntAlloc( 100 ); + Vec_Int_t * vNew; clock_t clk, clk2 = clock(); + int RetValue; p->nCalls++; // Gia_ManCleanValue( p->pGia ); // initialize @@ -542,17 +747,43 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in 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 ); +// assert( RetValue == 0 ); p->timeBwd += clock() - clk; } + + vNew = Ga2_FilterSelected( p, vSelected ); + if ( Vec_IntSize(vNew) > 0 ) + { + Vec_IntFree( vSelected ); + vSelected = vNew; + } + else + { + Vec_IntFree( vNew ); +// printf( "\nBig refinement.\n" ); + } + // clean values Rnm_ManCleanValues( p ); + // verify (empty) refinement - clk = clock(); - Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected ); - Vec_IntUniqify( vSelected ); + if ( fVerify ) + { + clk = clock(); + Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected ); + 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 ); - p->timeVer += clock() - clk; p->timeTotal += clock() - clk2; p->nRefines += Vec_IntSize(vSelected); return vSelected; |