abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
absRefSelect.c File Reference
#include "abs.h"
#include "absRef.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Rnm_ManPrintSelected (Rnm_Man_t *p, Vec_Int_t *vNewPPis)
 DECLARATIONS ///. More...
 
void Ga2_StructAnalize (Gia_Man_t *p, Vec_Int_t *vFront, Vec_Int_t *vInter, Vec_Int_t *vNewPPis)
 
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)
 

Function Documentation

void Ga2_StructAnalize ( Gia_Man_t *  p,
Vec_Int_t *  vFront,
Vec_Int_t *  vInter,
Vec_Int_t *  vNewPPis 
)

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

Synopsis [Perform structural analysis.]

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file absRefSelect.c.

71 {
72  Vec_Int_t * vFanins;
73  Gia_Obj_t * pObj, * pFanin;
74  int i, k;
75  // clean labels
76  Gia_ManForEachObj( p, pObj, i )
77  pObj->fMark0 = pObj->fMark1 = 0;
78  // label frontier
79  Gia_ManForEachObjVec( vFront, p, pObj, i )
80  pObj->fMark0 = 1, pObj->fMark1 = 0;
81  // label objects
82  Gia_ManForEachObjVec( vInter, p, pObj, i )
83  pObj->fMark1 = 0, pObj->fMark1 = 1;
84  // label selected
85  Gia_ManForEachObjVec( vNewPPis, p, pObj, i )
86  pObj->fMark1 = 1, pObj->fMark1 = 1;
87  // explore selected
88  Gia_ManForEachObjVec( vNewPPis, p, pObj, i )
89  {
90  printf( "Selected PPI %3d : ", i+1 );
91  printf( "%6d ", Gia_ObjId(p, pObj) );
92  printf( "\n" );
93  vFanins = Ga2_ObjLeaves( p, pObj );
94  Gia_ManForEachObjVec( vFanins, p, pFanin, k )
95  {
96  printf( " " );
97  printf( "%6d ", Gia_ObjId(p, pFanin) );
98  if ( pFanin->fMark0 && pFanin->fMark1 )
99  printf( "selected PPI" );
100  else if ( pFanin->fMark0 && !pFanin->fMark1 )
101  printf( "frontier (original PI or PPI)" );
102  else if ( !pFanin->fMark0 && pFanin->fMark1 )
103  printf( "abstracted node" );
104  else if ( !pFanin->fMark0 && !pFanin->fMark1 )
105  printf( "free variable" );
106  printf( "\n" );
107  }
108  }
109 }
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Gia_Obj_t_::fMark1
unsigned fMark1
Definition: gia.h:84
Gia_Obj_t_
Definition: gia.h:75
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
Ga2_ObjLeaves
static Vec_Int_t * Ga2_ObjLeaves(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: abs.h:117
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
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.

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 }
Rnm_Man_t_::vFanins
Vec_Int_t * vFanins
Definition: absRef.h:69
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Rnm_ObjIsJust
static int Rnm_ObjIsJust(Rnm_Man_t *p, Gia_Obj_t *pObj)
Definition: absRef.h:106
Rnm_Man_t_::pGia
Gia_Man_t * pGia
Definition: absRef.h:59
Gia_Obj_t_
Definition: gia.h:75
Rnm_ObjCount
static int Rnm_ObjCount(Rnm_Man_t *p, Gia_Obj_t *pObj)
Definition: absRef.h:102
Rnm_ObjSetCount
static void Rnm_ObjSetCount(Rnm_Man_t *p, Gia_Obj_t *pObj, int c)
Definition: absRef.h:103
Rnm_ObjAddToCount
static int Rnm_ObjAddToCount(Rnm_Man_t *p, Gia_Obj_t *pObj)
Definition: absRef.h:104
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ObjIsRo
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
if
if(last==0)
Definition: sparse_int.h:34
Vec_IntUniqify
static int Vec_IntUniqify(Vec_Int_t *p)
Definition: vecInt.h:1314
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Ga2_ObjLeaves
static Vec_Int_t * Ga2_ObjLeaves(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: abs.h:117
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
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.

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 }
Vec_IntDup
static Vec_Int_t * Vec_IntDup(Vec_Int_t *pVec)
Definition: vecInt.h:214
Rnm_Man_t_::vFanins
Vec_Int_t * vFanins
Definition: absRef.h:69
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Rnm_ObjIsJust
static int Rnm_ObjIsJust(Rnm_Man_t *p, Gia_Obj_t *pObj)
Definition: absRef.h:106
Rnm_Man_t_::pGia
Gia_Man_t * pGia
Definition: absRef.h:59
Gia_Obj_t_
Definition: gia.h:75
Rnm_ObjCount
static int Rnm_ObjCount(Rnm_Man_t *p, Gia_Obj_t *pObj)
Definition: absRef.h:102
Rnm_ObjSetCount
static void Rnm_ObjSetCount(Rnm_Man_t *p, Gia_Obj_t *pObj, int c)
Definition: absRef.h:103
Rnm_ObjAddToCount
static int Rnm_ObjAddToCount(Rnm_Man_t *p, Gia_Obj_t *pObj)
Definition: absRef.h:104
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ObjIsRo
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
Rnm_ManFilterSelected
Vec_Int_t * Rnm_ManFilterSelected(Rnm_Man_t *p, Vec_Int_t *vOldPPis)
Definition: absRefSelect.c:126
if
if(last==0)
Definition: sparse_int.h:34
Vec_IntUniqify
static int Vec_IntUniqify(Vec_Int_t *p)
Definition: vecInt.h:1314
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Ga2_ObjLeaves
static Vec_Int_t * Ga2_ObjLeaves(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: abs.h:117
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_NAMESPACE_IMPL_START void Rnm_ManPrintSelected ( Rnm_Man_t *  p,
Vec_Int_t *  vNewPPis 
)

DECLARATIONS ///.

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

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file absRefSelect.c.

46 {
47  Gia_Obj_t * pObj;
48  int i, Counter = 0;
49  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
50  if ( Gia_ObjIsPi(p->pGia, pObj) )
51  printf( "-" );
52  else if ( Vec_IntFind(vNewPPis, Gia_ObjId(p->pGia, pObj)) >= 0 )// this is PPI
53  printf( "1" ), Counter++;
54  else
55  printf( "0" );
56  printf( " %3d\n", Counter );
57 }
Rnm_Man_t_::pGia
Gia_Man_t * pGia
Definition: absRef.h:59
Vec_IntFind
static int Vec_IntFind(Vec_Int_t *p, int Entry)
Definition: vecInt.h:895
Gia_Obj_t_
Definition: gia.h:75
if
if(last==0)
Definition: sparse_int.h:34
else
else
Definition: sparse_int.h:55
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
Rnm_Man_t_::vMap
Vec_Int_t * vMap
Definition: absRef.h:61
Gia_ObjIsPi
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441