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

Go to the source code of this file.

Functions

void Fsim_ManVerifyFront (Fsim_Man_t *p)
 
void Fsim_ManFront (Fsim_Man_t *p, int fCompressAig)
 FUNCTION DECLARATIONS ///.
 

Function Documentation

◆ Fsim_ManFront()

void Fsim_ManFront ( Fsim_Man_t * p,
int fCompressAig )

FUNCTION DECLARATIONS ///.

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

Synopsis [Determine the frontier.]

Description []

SideEffects []

SeeAlso []

Definition at line 245 of file fsimFront.c.

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}
#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
Cube * p
Definition exorList.c:222
typedefABC_NAMESPACE_HEADER_START struct Fsim_Obj_t_ Fsim_Obj_t
INCLUDES ///.
Definition fsimInt.h:46
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Fsim_ManVerifyFront()

void Fsim_ManVerifyFront ( Fsim_Man_t * p)

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

Synopsis [Verifies the frontier.]

Description []

SideEffects []

SeeAlso []

Definition at line 202 of file fsimFront.c.

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}
#define Fsim_ManForEachObj(p, pObj, i)
Definition fsimInt.h:112