diff options
Diffstat (limited to 'src/proof/abs/absRefSelect.c')
| -rw-r--r-- | src/proof/abs/absRefSelect.c | 220 |
1 files changed, 220 insertions, 0 deletions
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 + |