ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
absRefSelect.c
Go to the documentation of this file.
1
20
21#include "abs.h"
22#include "absRef.h"
23
25
29
33
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}
58
70void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, Vec_Int_t * vNewPPis )
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}
110
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}
194
195
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}
302
306
307
309
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Vec_Int_t * Rnm_ManFilterSelectedNew(Rnm_Man_t *p, Vec_Int_t *vOldPPis)
ABC_NAMESPACE_IMPL_START void Rnm_ManPrintSelected(Rnm_Man_t *p, Vec_Int_t *vNewPPis)
DECLARATIONS ///.
Vec_Int_t * Rnm_ManFilterSelected(Rnm_Man_t *p, Vec_Int_t *vOldPPis)
void Ga2_StructAnalize(Gia_Man_t *p, Vec_Int_t *vFront, Vec_Int_t *vInter, Vec_Int_t *vNewPPis)
struct Rnm_Man_t_ Rnm_Man_t
Definition absRef.h:55
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
unsigned fMark1
Definition gia.h:86
unsigned fMark0
Definition gia.h:81
#define assert(ex)
Definition util_old.h:213