Data Structures
struct	Rnm_Obj_t_

struct	Rnm_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Rnm_Obj_t_	Rnm_Obj_t
	INCLUDES ///. More...

typedef struct Rnm_Man_t_	Rnm_Man_t

Functions
static Rnm_Obj_t *	Rnm_ManObj (Rnm_Man_t p, Gia_Obj_t pObj, int f)

static void	Rnm_ManSetRefId (Rnm_Man_t *p, int RefId)

static int	Rnm_ObjCount (Rnm_Man_t p, Gia_Obj_t pObj)

static void	Rnm_ObjSetCount (Rnm_Man_t p, Gia_Obj_t pObj, int c)

static int	Rnm_ObjAddToCount (Rnm_Man_t p, Gia_Obj_t pObj)

static int	Rnm_ObjIsJust (Rnm_Man_t p, Gia_Obj_t pObj)

Rnm_Man_t *	Rnm_ManStart (Gia_Man_t *pGia)
	FUNCTION DECLARATIONS ///. More...

void	Rnm_ManStop (Rnm_Man_t *p, int fProfile)

double	Rnm_ManMemoryUsage (Rnm_Man_t *p)

Vec_Int_t *	Rnm_ManRefine (Rnm_Man_t p, Abc_Cex_t pCex, Vec_Int_t *vMap, int fPropFanout, int fNewRefinement, int fVerbose)

Vec_Int_t *	Rnm_ManFilterSelected (Rnm_Man_t p, Vec_Int_t vOldPPis)

Vec_Int_t *	Rnm_ManFilterSelectedNew (Rnm_Man_t p, Vec_Int_t vOldPPis)

Typedef Documentation

typedef struct Rnm_Man_t_ Rnm_Man_t

Definition at line 55 of file absRef.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Rnm_Obj_t_ Rnm_Obj_t

INCLUDES ///.

CFile****************************************************************

FileName [absRef.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:: absRef.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///MACRO DEFINITIONS ///

Definition at line 45 of file absRef.h.

Function Documentation

Vec_Int_t* Rnm_ManFilterSelected	(	Rnm_Man_t *	p,
		Vec_Int_t *	vOldPPis
	)

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 []

Definition at line 126 of file absRefSelect.c.

 {
     int fVerbose = 0;
     Vec_Int_t * vNewPPis, * vFanins;
     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 )
     {
         vFanins = Ga2_ObjLeaves( p->pGia, pObj );
         Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
             if ( Rnm_ObjAddToCount(p, pFanin) == 0 ) // fanin counter is 0 -- save it
                 Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) );
     }
 
     // (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;
         }
         vFanins = Ga2_ObjLeaves( p->pGia, pObj );
         Gia_ManForEachObjVec( vFanins, 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;
 }

Vec_Int_t* Rnm_ManFilterSelectedNew	(	Rnm_Man_t *	p,
		Vec_Int_t *	vOldPPis
	)

Function*************************************************************

Synopsis [Improved postprocessing the set of PPIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 207 of file absRefSelect.c.

 {
     static int Counter = 0;
     int fVerbose = 0;
     Vec_Int_t * vNewPPis, * vFanins, * vFanins2;
     Gia_Obj_t * pObj, * pFanin, * pFanin2;
     int i, k, k2, RetValue, Counters[3] = {0};
 
     // return full set of PPIs once in a while
     if ( ++Counter % 9 == 0 )
         return Vec_IntDup( vOldPPis );
     return Rnm_ManFilterSelected( p, vOldPPis );
 
     // (0) make sure fanin counters are 0 at the beginning
 //    Gia_ManForEachObj( p->pGia, pObj, i )
 //        assert( Rnm_ObjCount(p, pObj) == 0 );
 
     // (1) increment two levels of PPI fanin counters
     Vec_IntClear( p->vFanins );
     Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
     {
         // go through the fanins
         vFanins = Ga2_ObjLeaves( p->pGia, pObj );
         Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
         {
             Rnm_ObjAddToCount(p, pFanin);
             if ( Rnm_ObjIsJust(p, pFanin) )   // included in the abstraction
                 Rnm_ObjAddToCount(p, pFanin); // count it second time!
             Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) );
 
             // go through the fanins of the fanins
             vFanins2 = Ga2_ObjLeaves( p->pGia, pFanin );
             Gia_ManForEachObjVec( vFanins2, p->pGia, pFanin2, k2 )
             {
                 Rnm_ObjAddToCount(p, pFanin2);
                 if ( Rnm_ObjIsJust(p, pFanin2) )   // included in the abstraction
                     Rnm_ObjAddToCount(p, pFanin2); // count it second time!
                 Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin2) );
             }
         }
     }
 
     // (3) select objects with reconvergence, which create potential constraints
     // - flop objects - yes
     // - objects whose fanin (or fanins' fanin) belongs to the justified area - yes
     // - objects whose fanins (or fanins' fanin) overlap - yes
     // (these do not guantee reconvergence, but may potentially have it)
     // (other objects cannot have reconvergence, even if they are added)
     vNewPPis = Vec_IntAlloc( 100 );
     Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
     {
         if ( Gia_ObjIsRo(p->pGia, pObj) )
         {
             if ( fVerbose )
                 Counters[0]++;
             Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
             continue;
         } 
         // go through the first fanins
         vFanins = Ga2_ObjLeaves( p->pGia, pObj );
         Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
         {
             if ( Rnm_ObjCount(p, pFanin) > 1 )
                 Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
             continue;
 
             // go through the fanins of the fanins
             vFanins2 = Ga2_ObjLeaves( p->pGia, pFanin );
             Gia_ManForEachObjVec( vFanins2, p->pGia, pFanin2, k2 )
             {
                 if ( Rnm_ObjCount(p, pFanin2) > 1 )
                 {
 //                    Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pFanin) );
                     Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
                 }
             }
         }
     }
     RetValue = Vec_IntUniqify( vNewPPis );
 //    assert( RetValue == 0 ); // we will have duplicated entries here!
 
     // (4) clear fanin counters
     // this is important for counters to be correctly set in the future iterations -- see step (0)
     Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
         Rnm_ObjSetCount( p, pObj, 0 );
 
     // visualize
     if ( fVerbose )
         printf( "*** Refinement %3d : PI+PPI =%4d. Old =%4d. New =%4d.   FF =%4d. Just =%4d. Shared =%4d.\n", 
             p->nRefId, Vec_IntSize(p->vMap), Vec_IntSize(vOldPPis), Vec_IntSize(vNewPPis), Counters[0], Counters[1], Counters[2] );
 
 //    Rnm_ManPrintSelected( p, vNewPPis );
 //    Ga2_StructAnalize( p->pGia, p->vMap, p->vObjs, vNewPPis );
     return vNewPPis;
 }

double Rnm_ManMemoryUsage ( Rnm_Man_t * p )

Definition at line 317 of file absRef.c.

 {
     return (double)(sizeof(Rnm_Man_t) + sizeof(Rnm_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs));
 }

static Rnm_Obj_t* Rnm_ManObj	(	Rnm_Man_t *	p,
		Gia_Obj_t *	pObj,
		int	f
	)

inlinestatic

Definition at line 93 of file absRef.h.

 { 
     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;  
 }

Vec_Int_t* Rnm_ManRefine	(	Rnm_Man_t *	p,
		Abc_Cex_t *	pCex,
		Vec_Int_t *	vMap,
		int	fPropFanout,
		int	fNewRefinement,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Computes the refinement for a given counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 673 of file absRef.c.

 {
     int fVerify = 1;
     Vec_Int_t * vGoodPPis, * vNewPPis;
     abctime clk, clk2 = Abc_Clock();
     int RetValue;
     p->nCalls++;
 //    Gia_ManCleanValue( p->pGia );
     // initialize
     p->pCex = pCex;
     p->vMap = vMap;
     p->fPropFanout = fPropFanout;
     p->fVerbose    = fVerbose;
     // collects used objects
     Rnm_ManCollect( p );
     // initialize datastructure
     p->nObjsFrame = 1 + Vec_IntSize(vMap) + Vec_IntSize(p->vObjs);
     p->nObjs = p->nObjsFrame * (pCex->iFrame + 1);
     if ( p->nObjs > p->nObjsAlloc )
         p->pObjs = ABC_REALLOC( Rnm_Obj_t, p->pObjs, (p->nObjsAlloc = p->nObjs + 10000) );
     memset( p->pObjs, 0, sizeof(Rnm_Obj_t) * p->nObjs );
     // propagate priorities
     clk = Abc_Clock();
     vGoodPPis = Vec_IntAlloc( 100 );
     if ( Rnm_ManSensitize( p ) ) // the CEX is not a true CEX
     {
         p->timeFwd += Abc_Clock() - clk;
         // select refinement
         clk = Abc_Clock();
         p->nVisited = 0;
         Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vGoodPPis );
         RetValue = Vec_IntUniqify( vGoodPPis );
 //        assert( RetValue == 0 );
         p->timeBwd += Abc_Clock() - clk;
     }
 
     // verify (empty) refinement
     // (only works when post-processing is not applied)
     if ( fVerify )
     {
         clk = Abc_Clock();
         Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vGoodPPis );
         p->timeVer += Abc_Clock() - clk;
     }
 
     // at this point array vGoodPPis contains the set of important PPIs
     if ( Vec_IntSize(vGoodPPis) > 0 ) // spurious CEX resulting in a non-trivial refinement 
     {
         // 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
     // we cannot do this before, because we need to remember what objects
     // belong to the abstraction when we do Rnm_ManFilterSelected()
     Rnm_ManCleanValues( p );
 
 //    Vec_IntReverseOrder( vGoodPPis );
     p->timeTotal += Abc_Clock() - clk2;
     p->nRefines += Vec_IntSize(vGoodPPis);
     return vGoodPPis;
 }

static void Rnm_ManSetRefId	(	Rnm_Man_t *	p,
		int	RefId
	)

inlinestatic

Definition at line 100 of file absRef.h.

100 { p->nRefId = RefId; }

Rnm_Man_t_::nRefId

int nRefId

Definition: absRef.h:64

Rnm_Man_t* Rnm_ManStart ( Gia_Man_t * pGia )

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis [Creates a new manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 264 of file absRef.c.

 {
     Rnm_Man_t * p;
     assert( Gia_ManPoNum(pGia) == 1 );
     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( 1000 );
 //    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 )
         Gia_ManStaticFanoutStart( p->pGia );
     Gia_ManCleanValue(pGia);
     Gia_ManCleanMark0(pGia);
     Gia_ManCleanMark1(pGia);
     return p;
 }

void Rnm_ManStop	(	Rnm_Man_t *	p,
		int	fProfile
	)

Definition at line 285 of file absRef.c.

 {
     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(Rnm_Man_t) + sizeof(Rnm_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs);
         abctime 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) );
     }
 
     Gia_ManCleanMark0(p->pGia);
     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_StrFree( p->vCounts );
     Vec_IntFree( p->vFanins );
     Vec_IntFree( p->vObjs );
     ABC_FREE( p->pObjs );
     ABC_FREE( p );
 }