ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
absRef.h File Reference
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  Rnm_Obj_t_
 
struct  Rnm_Man_t_
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct Rnm_Obj_t_ Rnm_Obj_t
 INCLUDES ///.
 
typedef struct Rnm_Man_t_ Rnm_Man_t
 

Functions

Rnm_Man_t * Rnm_ManStart (Gia_Man_t *pGia)
 FUNCTION DECLARATIONS ///.
 
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

◆ Rnm_Man_t

typedef struct Rnm_Man_t_ Rnm_Man_t

Definition at line 55 of file absRef.h.

◆ Rnm_Obj_t

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

◆ Rnm_ManFilterSelected()

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

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.

127{
128 int fVerbose = 0;
129 Vec_Int_t * vNewPPis, * vFanins;
130 Gia_Obj_t * pObj, * pFanin;
131 int i, k, RetValue, Counters[3] = {0};
132
133 // (0) make sure fanin counters are 0 at the beginning
134// Gia_ManForEachObj( p->pGia, pObj, i )
135// assert( Rnm_ObjCount(p, pObj) == 0 );
136
137 // (1) increment PPI fanin counters
138 Vec_IntClear( p->vFanins );
139 Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
140 {
141 vFanins = Ga2_ObjLeaves( p->pGia, pObj );
142 Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
143 if ( Rnm_ObjAddToCount(p, pFanin) == 0 ) // fanin counter is 0 -- save it
144 Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) );
145 }
146
147 // (3) select objects with reconvergence, which create potential constraints
148 // - flop objects
149 // - objects whose fanin belongs to the justified area
150 // - objects whose fanins overlap
151 // (these do not guantee reconvergence, but may potentially have it)
152 // (other objects cannot have reconvergence, even if they are added)
153 vNewPPis = Vec_IntAlloc( 100 );
154 Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
155 {
156 if ( Gia_ObjIsRo(p->pGia, pObj) )
157 {
158 if ( fVerbose )
159 Counters[0]++;
160 Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
161 continue;
162 }
163 vFanins = Ga2_ObjLeaves( p->pGia, pObj );
164 Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
165 {
166 if ( Rnm_ObjIsJust(p, pFanin) || Rnm_ObjCount(p, pFanin) > 1 )
167 {
168 if ( fVerbose )
169 Counters[1] += Rnm_ObjIsJust(p, pFanin);
170 if ( fVerbose )
171 Counters[2] += (Rnm_ObjCount(p, pFanin) > 1);
172 Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
173 break;
174 }
175 }
176 }
177 RetValue = Vec_IntUniqify( vNewPPis );
178 assert( RetValue == 0 );
179
180 // (4) clear fanin counters
181 // this is important for counters to be correctly set in the future iterations -- see step (0)
182 Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
183 Rnm_ObjSetCount( p, pObj, 0 );
184
185 // visualize
186 if ( fVerbose )
187 printf( "*** Refinement %3d : PI+PPI =%4d. Old =%4d. New =%4d. FF =%4d. Just =%4d. Shared =%4d.\n",
188 p->nRefId, Vec_IntSize(p->vMap), Vec_IntSize(vOldPPis), Vec_IntSize(vNewPPis), Counters[0], Counters[1], Counters[2] );
189
190// Rnm_ManPrintSelected( p, vNewPPis );
191// Ga2_StructAnalize( p->pGia, p->vMap, p->vObjs, vNewPPis );
192 return vNewPPis;
193}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
p
Cube * p
Definition exorList.c:222
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
assert
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Rnm_ManFilterSelectedNew()

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

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

Synopsis [Improved postprocessing the set of PPIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 207 of file absRefSelect.c.

208{
209 static int Counter = 0;
210 int fVerbose = 0;
211 Vec_Int_t * vNewPPis, * vFanins, * vFanins2;
212 Gia_Obj_t * pObj, * pFanin, * pFanin2;
213 int i, k, k2, RetValue, Counters[3] = {0};
214
215 // return full set of PPIs once in a while
216 if ( ++Counter % 9 == 0 )
217 return Vec_IntDup( vOldPPis );
218 return Rnm_ManFilterSelected( p, vOldPPis );
219
220 // (0) make sure fanin counters are 0 at the beginning
221// Gia_ManForEachObj( p->pGia, pObj, i )
222// assert( Rnm_ObjCount(p, pObj) == 0 );
223
224 // (1) increment two levels of PPI fanin counters
225 Vec_IntClear( p->vFanins );
226 Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
227 {
228 // go through the fanins
229 vFanins = Ga2_ObjLeaves( p->pGia, pObj );
230 Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
231 {
232 Rnm_ObjAddToCount(p, pFanin);
233 if ( Rnm_ObjIsJust(p, pFanin) ) // included in the abstraction
234 Rnm_ObjAddToCount(p, pFanin); // count it second time!
235 Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) );
236
237 // go through the fanins of the fanins
238 vFanins2 = Ga2_ObjLeaves( p->pGia, pFanin );
239 Gia_ManForEachObjVec( vFanins2, p->pGia, pFanin2, k2 )
240 {
241 Rnm_ObjAddToCount(p, pFanin2);
242 if ( Rnm_ObjIsJust(p, pFanin2) ) // included in the abstraction
243 Rnm_ObjAddToCount(p, pFanin2); // count it second time!
244 Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin2) );
245 }
246 }
247 }
248
249 // (3) select objects with reconvergence, which create potential constraints
250 // - flop objects - yes
251 // - objects whose fanin (or fanins' fanin) belongs to the justified area - yes
252 // - objects whose fanins (or fanins' fanin) overlap - yes
253 // (these do not guantee reconvergence, but may potentially have it)
254 // (other objects cannot have reconvergence, even if they are added)
255 vNewPPis = Vec_IntAlloc( 100 );
256 Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
257 {
258 if ( Gia_ObjIsRo(p->pGia, pObj) )
259 {
260 if ( fVerbose )
261 Counters[0]++;
262 Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
263 continue;
264 }
265 // go through the first fanins
266 vFanins = Ga2_ObjLeaves( p->pGia, pObj );
267 Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
268 {
269 if ( Rnm_ObjCount(p, pFanin) > 1 )
270 Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
271 continue;
272
273 // go through the fanins of the fanins
274 vFanins2 = Ga2_ObjLeaves( p->pGia, pFanin );
275 Gia_ManForEachObjVec( vFanins2, p->pGia, pFanin2, k2 )
276 {
277 if ( Rnm_ObjCount(p, pFanin2) > 1 )
278 {
279// Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pFanin) );
280 Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
281 }
282 }
283 }
284 }
285 RetValue = Vec_IntUniqify( vNewPPis );
286// assert( RetValue == 0 ); // we will have duplicated entries here!
287
288 // (4) clear fanin counters
289 // this is important for counters to be correctly set in the future iterations -- see step (0)
290 Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
291 Rnm_ObjSetCount( p, pObj, 0 );
292
293 // visualize
294 if ( fVerbose )
295 printf( "*** Refinement %3d : PI+PPI =%4d. Old =%4d. New =%4d. FF =%4d. Just =%4d. Shared =%4d.\n",
296 p->nRefId, Vec_IntSize(p->vMap), Vec_IntSize(vOldPPis), Vec_IntSize(vNewPPis), Counters[0], Counters[1], Counters[2] );
297
298// Rnm_ManPrintSelected( p, vNewPPis );
299// Ga2_StructAnalize( p->pGia, p->vMap, p->vObjs, vNewPPis );
300 return vNewPPis;
301}
Rnm_ManFilterSelected
Vec_Int_t * Rnm_ManFilterSelected(Rnm_Man_t *p, Vec_Int_t *vOldPPis)
Definition absRefSelect.c:126
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Rnm_ManMemoryUsage()

double Rnm_ManMemoryUsage ( Rnm_Man_t * p)
extern

Definition at line 317 of file absRef.c.

318{
319 return (double)(sizeof(Rnm_Man_t) + sizeof(Rnm_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs));
320}
Rnm_Obj_t
typedefABC_NAMESPACE_HEADER_START struct Rnm_Obj_t_ Rnm_Obj_t
INCLUDES ///.
Definition absRef.h:45
Rnm_Man_t
struct Rnm_Man_t_ Rnm_Man_t
Definition absRef.h:55
Here is the caller graph for this function:

◆ Rnm_ManRefine()

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 673 of file absRef.c.

674{
675 int fVerify = 1;
676 Vec_Int_t * vGoodPPis, * vNewPPis;
677 abctime clk, clk2 = Abc_Clock();
678 int RetValue;
679 p->nCalls++;
680// Gia_ManCleanValue( p->pGia );
681 // initialize
682 p->pCex = pCex;
683 p->vMap = vMap;
684 p->fPropFanout = fPropFanout;
685 p->fVerbose = fVerbose;
686 // collects used objects
687 Rnm_ManCollect( p );
688 // initialize datastructure
689 p->nObjsFrame = 1 + Vec_IntSize(vMap) + Vec_IntSize(p->vObjs);
690 p->nObjs = p->nObjsFrame * (pCex->iFrame + 1);
691 if ( p->nObjs > p->nObjsAlloc )
692 p->pObjs = ABC_REALLOC( Rnm_Obj_t, p->pObjs, (p->nObjsAlloc = p->nObjs + 10000) );
693 memset( p->pObjs, 0, sizeof(Rnm_Obj_t) * p->nObjs );
694 // propagate priorities
695 clk = Abc_Clock();
696 vGoodPPis = Vec_IntAlloc( 100 );
697 if ( Rnm_ManSensitize( p ) ) // the CEX is not a true CEX
698 {
699 p->timeFwd += Abc_Clock() - clk;
700 // select refinement
701 clk = Abc_Clock();
702 p->nVisited = 0;
703 Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vGoodPPis );
704 RetValue = Vec_IntUniqify( vGoodPPis );
705// assert( RetValue == 0 );
706 p->timeBwd += Abc_Clock() - clk;
707 }
708
709 // verify (empty) refinement
710 // (only works when post-processing is not applied)
711 if ( fVerify )
712 {
713 clk = Abc_Clock();
714 Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vGoodPPis );
715 p->timeVer += Abc_Clock() - clk;
716 }
717
718 // at this point array vGoodPPis contains the set of important PPIs
719 if ( Vec_IntSize(vGoodPPis) > 0 ) // spurious CEX resulting in a non-trivial refinement
720 {
721 // filter selected set
722 if ( !fNewRefinement ) // default
723 vNewPPis = Rnm_ManFilterSelected( p, vGoodPPis );
724 else // this is enabled when &gla is called with -r (&gla -r)
725 vNewPPis = Rnm_ManFilterSelectedNew( p, vGoodPPis );
726
727 // replace the PPI array if necessary
728 if ( Vec_IntSize(vNewPPis) > 0 ) // something to select, replace current refinement
729 Vec_IntFree( vGoodPPis ), vGoodPPis = vNewPPis;
730 else // if there is nothing to select, do not change the current refinement array
731 Vec_IntFree( vNewPPis );
732 }
733
734 // clean values
735 // we cannot do this before, because we need to remember what objects
736 // belong to the abstraction when we do Rnm_ManFilterSelected()
737 Rnm_ManCleanValues( p );
738
739// Vec_IntReverseOrder( vGoodPPis );
740 p->timeTotal += Abc_Clock() - clk2;
741 p->nRefines += Vec_IntSize(vGoodPPis);
742 return vGoodPPis;
743}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
Rnm_ManJustify_rec
void Rnm_ManJustify_rec(Rnm_Man_t *p, Gia_Obj_t *pObj, int f, Vec_Int_t *vSelect)
Definition absRef.c:524
Rnm_ManVerifyUsingTerSim
void Rnm_ManVerifyUsingTerSim(Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vMap, Vec_Int_t *vObjs, Vec_Int_t *vRes)
Definition absRef.c:619
Rnm_ManCleanValues
void Rnm_ManCleanValues(Rnm_Man_t *p)
Definition absRef.c:375
Rnm_ManSensitize
int Rnm_ManSensitize(Rnm_Man_t *p)
Definition absRef.c:396
Rnm_ManCollect
void Rnm_ManCollect(Rnm_Man_t *p)
Definition absRef.c:351
Rnm_ManFilterSelectedNew
Vec_Int_t * Rnm_ManFilterSelectedNew(Rnm_Man_t *p, Vec_Int_t *vOldPPis)
Definition absRefSelect.c:207
Rnm_ManFilterSelected
Vec_Int_t * Rnm_ManFilterSelected(Rnm_Man_t *p, Vec_Int_t *vOldPPis)
Definition absRefSelect.c:126
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Rnm_ManStart()

Rnm_Man_t * Rnm_ManStart ( Gia_Man_t * pGia)
extern

FUNCTION DECLARATIONS ///.

FUNCTION DECLARATIONS ///.

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

Synopsis [Creates a new manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 264 of file absRef.c.

265{
266 Rnm_Man_t * p;
267 assert( Gia_ManPoNum(pGia) == 1 );
268 p = ABC_CALLOC( Rnm_Man_t, 1 );
269 p->pGia = pGia;
270 p->vObjs = Vec_IntAlloc( 100 );
271 p->vCounts = Vec_StrStart( Gia_ManObjNum(pGia) );
272 p->vFanins = Vec_IntAlloc( 1000 );
273// p->vSatVars = Vec_IntAlloc( 0 );
274// p->vSat2Ids = Vec_IntAlloc( 1000 );
275// p->vIsopMem = Vec_IntAlloc( 0 );
276 p->nObjsAlloc = 10000;
277 p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc );
278 if ( p->pGia->vFanout == NULL )
279 Gia_ManStaticFanoutStart( p->pGia );
280 Gia_ManCleanValue(pGia);
281 Gia_ManCleanMark0(pGia);
282 Gia_ManCleanMark1(pGia);
283 return p;
284}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
Gia_ManStaticFanoutStart
void Gia_ManStaticFanoutStart(Gia_Man_t *p)
Definition giaFanout.c:238
Gia_ManCleanValue
void Gia_ManCleanValue(Gia_Man_t *p)
Definition giaUtil.c:351
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition giaUtil.c:256
Gia_ManCleanMark1
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition giaUtil.c:313
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Rnm_ManStop()

void Rnm_ManStop ( Rnm_Man_t * p,
int fProfile )
extern

Definition at line 285 of file absRef.c.

286{
287 if ( !p ) return;
288 // print runtime statistics
289 if ( fProfile && p->nCalls )
290 {
291 double MemGia = sizeof(Gia_Man_t) + sizeof(Gia_Obj_t) * p->pGia->nObjsAlloc + sizeof(int) * p->pGia->nTravIdsAlloc;
292 double MemOther = sizeof(Rnm_Man_t) + sizeof(Rnm_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs);
293 abctime timeOther = p->timeTotal - p->timeFwd - p->timeBwd - p->timeVer;
294 printf( "Abstraction refinement runtime statistics:\n" );
295 ABC_PRTP( "Sensetization", p->timeFwd, p->timeTotal );
296 ABC_PRTP( "Justification", p->timeBwd, p->timeTotal );
297 ABC_PRTP( "Verification ", p->timeVer, p->timeTotal );
298 ABC_PRTP( "Other ", timeOther, p->timeTotal );
299 ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
300 printf( "Total calls = %d. Average refine = %.1f. GIA mem = %.3f MB. Other mem = %.3f MB.\n",
301 p->nCalls, 1.0*p->nRefines/p->nCalls, MemGia/(1<<20), MemOther/(1<<20) );
302 }
303
304 Gia_ManCleanMark0(p->pGia);
305 Gia_ManCleanMark1(p->pGia);
306 Gia_ManStaticFanoutStop(p->pGia);
307// Gia_ManSetPhase(p->pGia);
308// Vec_IntFree( p->vIsopMem );
309// Vec_IntFree( p->vSatVars );
310// Vec_IntFree( p->vSat2Ids );
311 Vec_StrFree( p->vCounts );
312 Vec_IntFree( p->vFanins );
313 Vec_IntFree( p->vObjs );
314 ABC_FREE( p->pObjs );
315 ABC_FREE( p );
316}
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Gia_ManStaticFanoutStop
void Gia_ManStaticFanoutStop(Gia_Man_t *p)
Definition giaFanout.c:393
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
timeOther
abctime timeOther
Definition llb3Image.c:82
Here is the call graph for this function:
Here is the caller graph for this function: