ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
absRefSelect.c File Reference
#include "abs.h"
#include "absRef.h"
Include dependency graph for absRefSelect.c:

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 ///.
 
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

◆ Ga2_StructAnalize()

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
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
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Gia_Obj_t_::fMark1
unsigned fMark1
Definition gia.h:86
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81

◆ Rnm_ManFilterSelected()

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}
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 )

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_ManPrintSelected()

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}