ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
fsimFront.c
Go to the documentation of this file.
1
20
21#include "fsimInt.h"
22
24
25
29
33
45static inline void Fsim_ManStoreNum( Fsim_Man_t * p, int Num )
46{
47 unsigned x = (unsigned)Num;
48 assert( Num >= 0 );
49 while ( x & ~0x7f )
50 {
51 *p->pDataCur++ = (x & 0x7f) | 0x80;
52 x >>= 7;
53 }
54 *p->pDataCur++ = x;
55 assert( p->pDataCur - p->pDataAig < p->nDataAig );
56}
57
69static inline int Fsim_ManRestoreNum( Fsim_Man_t * p )
70{
71 int ch, i, x = 0;
72 for ( i = 0; (ch = *p->pDataCur++) & 0x80; i++ )
73 x |= (ch & 0x7f) << (7 * i);
74 assert( p->pDataCur - p->pDataAig < p->nDataAig );
75 return x | (ch << (7 * i));
76}
77
89static inline void Fsim_ManStoreObj( Fsim_Man_t * p, Fsim_Obj_t * pObj )
90{
91 if ( p->pDataAig2 )
92 {
93 *p->pDataCur2++ = pObj->iNode;
94 *p->pDataCur2++ = pObj->iFan0;
95 *p->pDataCur2++ = pObj->iFan1;
96 return;
97 }
98 if ( pObj->iFan0 && pObj->iFan1 ) // and
99 {
100 assert( pObj->iNode );
101 assert( pObj->iNode >= p->iNodePrev );
102 assert( (pObj->iNode << 1) > pObj->iFan0 );
103 assert( pObj->iFan0 > pObj->iFan1 );
104 Fsim_ManStoreNum( p, ((pObj->iNode - p->iNodePrev) << 2) | 3 );
105 Fsim_ManStoreNum( p, (pObj->iNode << 1) - pObj->iFan0 );
106 Fsim_ManStoreNum( p, pObj->iFan0 - pObj->iFan1 );
107 p->iNodePrev = pObj->iNode;
108 }
109 else if ( !pObj->iFan0 && !pObj->iFan1 ) // ci
110 {
111 assert( pObj->iNode );
112 assert( pObj->iNode >= p->iNodePrev );
113 Fsim_ManStoreNum( p, ((pObj->iNode - p->iNodePrev) << 2) | 1 );
114 p->iNodePrev = pObj->iNode;
115 }
116 else // if ( !pObj->iFan0 && pObj->iFan1 ) // co
117 {
118 assert( pObj->iNode == 0 );
119 assert( pObj->iFan0 != 0 );
120 assert( pObj->iFan1 == 0 );
121 assert( ((p->iNodePrev << 1) | 1) >= pObj->iFan0 );
122 Fsim_ManStoreNum( p, (((p->iNodePrev << 1) | 1) - pObj->iFan0) << 1 );
123 }
124}
125
137static inline int Fsim_ManRestoreObj( Fsim_Man_t * p, Fsim_Obj_t * pObj )
138{
139 int iValue = Fsim_ManRestoreNum( p );
140 if ( (iValue & 3) == 3 ) // and
141 {
142 pObj->iNode = (iValue >> 2) + p->iNodePrev;
143 pObj->iFan0 = (pObj->iNode << 1) - Fsim_ManRestoreNum( p );
144 pObj->iFan1 = pObj->iFan0 - Fsim_ManRestoreNum( p );
145 p->iNodePrev = pObj->iNode;
146 }
147 else if ( (iValue & 3) == 1 ) // ci
148 {
149 pObj->iNode = (iValue >> 2) + p->iNodePrev;
150 pObj->iFan0 = 0;
151 pObj->iFan1 = 0;
152 p->iNodePrev = pObj->iNode;
153 }
154 else // if ( (iValue & 1) == 0 ) // co
155 {
156 pObj->iNode = 0;
157 pObj->iFan0 = ((p->iNodePrev << 1) | 1) - (iValue >> 1);
158 pObj->iFan1 = 0;
159 }
160 return 1;
161}
162
174static inline int Fsim_ManFrontFindNext( Fsim_Man_t * p, char * pFront )
175{
176 assert( p->iNumber < (1 << 30) - p->nFront );
177 while ( 1 )
178 {
179 if ( p->iNumber % p->nFront == 0 )
180 p->iNumber++;
181 if ( pFront[p->iNumber % p->nFront] == 0 )
182 {
183 pFront[p->iNumber % p->nFront] = 1;
184 return p->iNumber;
185 }
186 p->iNumber++;
187 }
188 return -1;
189}
190
203{
204 Fsim_Obj_t * pObj;
205 int * pFans0, * pFans1; // representation of fanins
206 int * pFrontToId; // mapping of nodes into frontier variables
207 int i, iVar0, iVar1;
208 pFans0 = ABC_ALLOC( int, p->nObjs );
209 pFans1 = ABC_ALLOC( int, p->nObjs );
210 pFans0[0] = pFans1[0] = 0;
211 pFans0[1] = pFans1[1] = 0;
212 pFrontToId = ABC_CALLOC( int, p->nFront );
213 if ( Aig_ObjRefs(Aig_ManConst1(p->pAig)) )
214 pFrontToId[1] = 1;
215 Fsim_ManForEachObj( p, pObj, i )
216 {
217 if ( pObj->iNode )
218 pFrontToId[pObj->iNode % p->nFront] = i;
219 iVar0 = Fsim_Lit2Var(pObj->iFan0);
220 iVar1 = Fsim_Lit2Var(pObj->iFan1);
221 pFans0[i] = Fsim_Var2Lit(pFrontToId[iVar0 % p->nFront], Fsim_LitIsCompl(pObj->iFan0));
222 pFans1[i] = Fsim_Var2Lit(pFrontToId[iVar1 % p->nFront], Fsim_LitIsCompl(pObj->iFan1));
223 }
224 for ( i = 0; i < p->nObjs; i++ )
225 {
226 assert( pFans0[i] == p->pFans0[i] );
227 assert( pFans1[i] == p->pFans1[i] );
228 }
229 ABC_FREE( pFrontToId );
230 ABC_FREE( pFans0 );
231 ABC_FREE( pFans1 );
232}
233
245void Fsim_ManFront( Fsim_Man_t * p, int fCompressAig )
246{
247 Fsim_Obj_t Obj, * pObj = &Obj;
248 char * pFront; // places used for the frontier
249 int * pIdToFront; // mapping of nodes into frontier places
250 int i, iVar0, iVar1, nCrossCut = 0, nCrossCutMax = 0;
251 // start the frontier
252 pFront = ABC_CALLOC( char, p->nFront );
253 pIdToFront = ABC_ALLOC( int, p->nObjs );
254 pIdToFront[0] = -1;
255 pIdToFront[1] = -1;
256 // add constant node
257 p->iNumber = 1;
258 if ( p->pRefs[1] )
259 {
260 pIdToFront[1] = Fsim_ManFrontFindNext( p, pFront );
261 nCrossCut = 1;
262 }
263 // allocate room for data
264 if ( fCompressAig )
265 {
266 p->nDataAig = p->nObjs * 6;
267 p->pDataAig = ABC_ALLOC( unsigned char, p->nDataAig );
268 p->pDataCur = p->pDataAig;
269 p->iNodePrev = 0;
270 }
271 else
272 {
273 p->pDataAig2 = ABC_ALLOC( int, 3 * p->nObjs );
274 p->pDataCur2 = p->pDataAig2 + 6;
275 }
276 // iterate through the objects
277 for ( i = 2; i < p->nObjs; i++ )
278 {
279 if ( p->pFans0[i] == 0 ) // ci
280 {
281 // store node
282 pIdToFront[i] = Fsim_ManFrontFindNext( p, pFront );
283 pObj->iNode = pIdToFront[i];
284 pObj->iFan0 = 0;
285 pObj->iFan1 = 0;
286 Fsim_ManStoreObj( p, pObj );
287 // handle CIs without fanout
288 if ( p->pRefs[i] == 0 )
289 {
290 pFront[pIdToFront[i] % p->nFront] = 0;
291 pIdToFront[i] = -1;
292 }
293 }
294 else if ( p->pFans1[i] == 0 ) // co
295 {
296 assert( p->pRefs[i] == 0 );
297 // get the fanin
298 iVar0 = Fsim_Lit2Var(p->pFans0[i]);
299 assert( pIdToFront[iVar0] > 0 );
300 // store node
301 pObj->iNode = 0;
302 pObj->iFan0 = Fsim_Var2Lit(pIdToFront[iVar0], Fsim_LitIsCompl(p->pFans0[i]));
303 pObj->iFan1 = 0;
304 Fsim_ManStoreObj( p, pObj );
305 // deref the fanin
306 if ( --p->pRefs[iVar0] == 0 )
307 {
308 pFront[pIdToFront[iVar0] % p->nFront] = 0;
309 pIdToFront[iVar0] = -1;
310 nCrossCut--;
311 }
312 }
313 else
314 {
315 // get the fanins
316 iVar0 = Fsim_Lit2Var(p->pFans0[i]);
317 assert( pIdToFront[iVar0] > 0 );
318 iVar1 = Fsim_Lit2Var(p->pFans1[i]);
319 assert( pIdToFront[iVar1] > 0 );
320 // store node
321 pIdToFront[i] = Fsim_ManFrontFindNext( p, pFront );
322 pObj->iNode = pIdToFront[i];
323 pObj->iFan0 = Fsim_Var2Lit(pIdToFront[iVar0], Fsim_LitIsCompl(p->pFans0[i]));
324 pObj->iFan1 = Fsim_Var2Lit(pIdToFront[iVar1], Fsim_LitIsCompl(p->pFans1[i]));
325 Fsim_ManStoreObj( p, pObj );
326 // deref the fanins
327 if ( --p->pRefs[iVar0] == 0 )
328 {
329 pFront[pIdToFront[iVar0] % p->nFront] = 0;
330 pIdToFront[iVar0] = -1;
331 nCrossCut--;
332 }
333 if ( --p->pRefs[iVar1] == 0 )
334 {
335 pFront[pIdToFront[iVar1] % p->nFront] = 0;
336 pIdToFront[iVar1] = -1;
337 nCrossCut--;
338 }
339 // handle nodes without fanout (choice nodes)
340 if ( p->pRefs[i] == 0 )
341 {
342 pFront[pIdToFront[i] % p->nFront] = 0;
343 pIdToFront[i] = -1;
344 }
345 }
346 if ( p->pRefs[i] )
347 if ( nCrossCutMax < ++nCrossCut )
348 nCrossCutMax = nCrossCut;
349 }
350 assert( p->pDataAig2 == NULL || p->pDataCur2 - p->pDataAig2 == (3 * p->nObjs) );
351 assert( nCrossCut == 0 );
352 assert( nCrossCutMax == p->nCrossCutMax );
353 for ( i = 0; i < p->nFront; i++ )
354 assert( pFront[i] == 0 );
355 ABC_FREE( pFront );
356 ABC_FREE( pIdToFront );
357// Fsim_ManVerifyFront( p );
358 ABC_FREE( p->pFans0 );
359 ABC_FREE( p->pFans1 );
360 ABC_FREE( p->pRefs );
361}
362
366
367
369
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Cube * p
Definition exorList.c:222
void Fsim_ManFront(Fsim_Man_t *p, int fCompressAig)
FUNCTION DECLARATIONS ///.
Definition fsimFront.c:245
void Fsim_ManVerifyFront(Fsim_Man_t *p)
Definition fsimFront.c:202
#define Fsim_ManForEachObj(p, pObj, i)
Definition fsimInt.h:112
typedefABC_NAMESPACE_HEADER_START struct Fsim_Obj_t_ Fsim_Obj_t
INCLUDES ///.
Definition fsimInt.h:46
typedefABC_NAMESPACE_HEADER_START struct Fsim_Man_t_ Fsim_Man_t
INCLUDES ///.
Definition fsim.h:42
#define assert(ex)
Definition util_old.h:213