ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
saigSimFast.c
Go to the documentation of this file.
1
20
21#include "saig.h"
22
23#include "base/main/main.h"
24
26
27
31
32// the AIG manager
33typedef struct Faig_Man_t_ Faig_Man_t;
35{
36 // parameters
37 int nPis;
38 int nPos;
39 int nCis;
40 int nCos;
41 int nFfs;
42 int nNos;
43 // offsets
44 int nPis1;
45 int nCis1;
48 int nObjs;
49 // allocated data
50 int nWords;
51 int pObjs[0];
52};
53
54static inline int Faig_CheckIdPi( Faig_Man_t * p, int i ) { return i >= 1 && i < p->nPis1; }
55static inline int Faig_CheckIdLo( Faig_Man_t * p, int i ) { return i >= p->nPis1 && i < p->nCis1; }
56static inline int Faig_CheckIdNo( Faig_Man_t * p, int i ) { return i >= p->nCis1 && i < p->nCisNos1; }
57static inline int Faig_CheckIdPo( Faig_Man_t * p, int i ) { return i >= p->nCisNos1 && i < p->nCisNosPos1; }
58static inline int Faig_CheckIdLi( Faig_Man_t * p, int i ) { return i >= p->nCisNosPos1 && i < p->nObjs; }
59static inline int Faig_CheckIdCo( Faig_Man_t * p, int i ) { return i >= p->nCisNos1 && i < p->nObjs; }
60static inline int Faig_CheckIdObj( Faig_Man_t * p, int i ) { return i >= 0 && i < p->nObjs; }
61
62static inline int Faig_ObjIdToNumPi( Faig_Man_t * p, int i ) { assert( Faig_CheckIdPi(p,i) ); return i - 1; }
63static inline int Faig_ObjIdToNumLo( Faig_Man_t * p, int i ) { assert( Faig_CheckIdLo(p,i) ); return i - p->nPis1; }
64static inline int Faig_ObjIdToNumNo( Faig_Man_t * p, int i ) { assert( Faig_CheckIdNo(p,i) ); return i - p->nCis1; }
65static inline int Faig_ObjIdToNumPo( Faig_Man_t * p, int i ) { assert( Faig_CheckIdPo(p,i) ); return i - p->nCisNos1; }
66static inline int Faig_ObjIdToNumLi( Faig_Man_t * p, int i ) { assert( Faig_CheckIdLi(p,i) ); return i - p->nCisNosPos1; }
67static inline int Faig_ObjIdToNumCo( Faig_Man_t * p, int i ) { assert( Faig_CheckIdCo(p,i) ); return i - p->nCisNos1; }
68
69static inline int Faig_ObjLoToLi( Faig_Man_t * p, int i ) { assert( Faig_CheckIdLo(p,i) ); return p->nObjs - (p->nCis1 - i); }
70static inline int Faig_ObjLiToLo( Faig_Man_t * p, int i ) { assert( Faig_CheckIdLi(p,i) ); return p->nCis1 - (p->nObjs - i); }
71
72static inline int Faig_NodeChild0( Faig_Man_t * p, int n ) { return p->pObjs[n<<1]; }
73static inline int Faig_NodeChild1( Faig_Man_t * p, int n ) { return p->pObjs[(n<<1)+1]; }
74static inline int Faig_CoChild0( Faig_Man_t * p, int n ) { return p->pObjs[(p->nNos<<1)+n]; }
75static inline int Faig_ObjFaninC( int iFan ) { return iFan & 1; }
76static inline int Faig_ObjFanin( int iFan ) { return iFan >> 1; }
77
81
94{
95 return Aig_ManObjNumMax(pAig) ==
96 1 + Aig_ManCiNum(pAig) + Aig_ManNodeNum(pAig) + Aig_ManCoNum(pAig);
97}
98
111{
112 Faig_Man_t * p;
113 int nWords;
114// assert( Faig_ManIsCorrect(pAig) );
115 nWords = 2 * Aig_ManNodeNum(pAig) + Aig_ManCoNum(pAig);
116 p = (Faig_Man_t *)ABC_ALLOC( char, sizeof(Faig_Man_t) + sizeof(int) * nWords );
117//printf( "Allocating %7.2f MB.\n", 1.0 * (sizeof(Faig_Man_t) + sizeof(int) * nWords)/(1<<20) );
118 memset( p, 0, sizeof(Faig_Man_t) );
119 p->nPis = Aig_ManCiNum(pAig) - Aig_ManRegNum(pAig);
120 p->nPos = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig);
121 p->nCis = Aig_ManCiNum(pAig);
122 p->nCos = Aig_ManCoNum(pAig);
123 p->nFfs = Aig_ManRegNum(pAig);
124 p->nNos = Aig_ManNodeNum(pAig);
125 // offsets
126 p->nPis1 = p->nPis + 1;
127 p->nCis1 = p->nCis + 1;
128 p->nCisNos1 = p->nCis + p->nNos + 1;
129 p->nCisNosPos1 = p->nCis + p->nNos + p->nPos + 1;
130 p->nObjs = p->nCis + p->nNos + p->nCos + 1;
131 p->nWords = nWords;
132 return p;
133}
134
147{
148 Faig_Man_t * p;
149 Aig_Obj_t * pObj;
150 int i, iWord = 0;
151 p = Faig_ManAlloc( pAig );
152 Aig_ManForEachNode( pAig, pObj, i )
153 {
154 p->pObjs[iWord++] = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj);
155 p->pObjs[iWord++] = (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj);
156 }
157 Aig_ManForEachCo( pAig, pObj, i )
158 p->pObjs[iWord++] = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj);
159 assert( iWord == p->nWords );
160 return p;
161}
162
174static inline unsigned Faig_SimulateNode( Faig_Man_t * p, int Id, unsigned * pSimInfo )
175{
176 int n = Faig_ObjIdToNumNo( p, Id );
177 int iFan0 = Faig_NodeChild0( p, n );
178 int iFan1 = Faig_NodeChild1( p, n );
179 if ( Faig_ObjFaninC(iFan0) && Faig_ObjFaninC(iFan1) )
180 return ~(pSimInfo[Faig_ObjFanin(iFan0)] | pSimInfo[Faig_ObjFanin(iFan1)]);
181 if ( Faig_ObjFaninC(iFan0) && !Faig_ObjFaninC(iFan1) )
182 return (~pSimInfo[Faig_ObjFanin(iFan0)] & pSimInfo[Faig_ObjFanin(iFan1)]);
183 if ( !Faig_ObjFaninC(iFan0) && Faig_ObjFaninC(iFan1) )
184 return (pSimInfo[Faig_ObjFanin(iFan0)] & ~pSimInfo[Faig_ObjFanin(iFan1)]);
185 // if ( !Faig_ObjFaninC(iFan0) && !Faig_ObjFaninC(iFan1) )
186 return (pSimInfo[Faig_ObjFanin(iFan0)] & pSimInfo[Faig_ObjFanin(iFan1)]);
187}
188
200static inline unsigned Faig_SimulateCo( Faig_Man_t * p, int Id, unsigned * pSimInfo )
201{
202 int n = Faig_ObjIdToNumCo( p, Id );
203 int iFan0 = Faig_CoChild0( p, n );
204 if ( Faig_ObjFaninC(iFan0) )
205 return ~pSimInfo[Faig_ObjFanin(iFan0)];
206 // if ( !Faig_ObjFaninC(iFan0) )
207 return pSimInfo[Faig_ObjFanin(iFan0)];
208}
209
221static inline unsigned Faig_SimulateRandomShift( unsigned uOld )
222{
223 return (uOld << 16) | ((uOld ^ Aig_ManRandom(0)) & 0xffff);
224}
225
237static inline unsigned Faig_SimulateTransferShift( unsigned uOld, unsigned uNew )
238{
239 return (uOld << 16) | (uNew & 0xffff);
240}
241
253int * Faig_ManSimulateFrames( Faig_Man_t * p, int nFrames, int nPref, int fTrans )
254{
255 int * pNumOnes = ABC_CALLOC( int, p->nObjs );
256 unsigned * pSimInfo = ABC_ALLOC( unsigned, p->nObjs );
257 int f, i;
258//printf( "Allocating %7.2f MB.\n", 1.0 * 4 * p->nObjs/(1<<20) );
259//printf( "Allocating %7.2f MB.\n", 1.0 * 4 * p->nObjs/(1<<20) );
260 // set constant 1
261 pSimInfo[0] = ~0;
262 for ( f = 0; f < nFrames; f++ )
263 {
264 if ( fTrans )
265 {
266 for ( i = 1; i < p->nPis1; i++ )
267 pSimInfo[i] = f? Faig_SimulateRandomShift( pSimInfo[i] ) : Aig_ManRandom( 0 );
268 for ( ; i < p->nCis1; i++ )
269 pSimInfo[i] = f? Faig_SimulateTransferShift( pSimInfo[i], pSimInfo[Faig_ObjLoToLi(p,i)] ) : 0;
270 }
271 else
272 {
273 for ( i = 1; i < p->nPis1; i++ )
274 pSimInfo[i] = Aig_ManRandom( 0 );
275 for ( ; i < p->nCis1; i++ )
276 pSimInfo[i] = f? pSimInfo[Faig_ObjLoToLi(p,i)] : 0;
277 }
278 for ( ; i < p->nCisNos1; i++ )
279 pSimInfo[i] = Faig_SimulateNode( p, i, pSimInfo );
280 for ( ; i < p->nObjs; i++ )
281 pSimInfo[i] = Faig_SimulateCo( p, i, pSimInfo );
282 if ( f < nPref )
283 continue;
284 if ( fTrans )
285 {
286 for ( i = 0; i < p->nObjs; i++ )
287 pNumOnes[i] += Aig_WordCountOnes( (pSimInfo[i] ^ (pSimInfo[i] >> 16)) & 0xffff );
288 }
289 else
290 {
291 for ( i = 0; i < p->nObjs; i++ )
292 pNumOnes[i] += Aig_WordCountOnes( pSimInfo[i] );
293 }
294 }
295 ABC_FREE( pSimInfo );
296 return pNumOnes;
297}
298
310float Faig_ManComputeSwitching( int nOnes, int nSimWords )
311{
312 int nTotal = 32 * nSimWords;
313 return (float)2.0 * nOnes / nTotal * (nTotal - nOnes) / nTotal;
314}
315
327float Faig_ManComputeProbOne( int nOnes, int nSimWords )
328{
329 int nTotal = 32 * nSimWords;
330 return (float)nOnes / nTotal;
331}
332
344Vec_Int_t * Faig_ManComputeSwitchProbs4( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
345{
346 int fTrans = 1;
347 Faig_Man_t * pAig;
348 Vec_Int_t * vSwitching;
349 int * pProbs;
350 float * pSwitching;
351 int nFramesReal;
352 abctime clk;//, clkTotal = Abc_Clock();
353 if ( fProbOne )
354 fTrans = 0;
355 vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) );
356 pSwitching = (float *)vSwitching->pArray;
357clk = Abc_Clock();
358 pAig = Faig_ManCreate( p );
359//ABC_PRT( "\nCreation ", Abc_Clock() - clk );
360 Aig_ManRandom( 1 );
361 // get the number of frames to simulate
362 // if the parameter "seqsimframes" is defined, use it
363 // otherwise, use the given number of frames "nFrames"
364 nFramesReal = nFrames;
365 if ( Abc_FrameReadFlag("seqsimframes") )
366 nFramesReal = atoi( Abc_FrameReadFlag("seqsimframes") );
367 if ( nFramesReal <= nPref )
368 {
369 printf( "The total number of frames (%d) should exceed prefix (%d).\n", nFramesReal, nPref );
370 printf( "Setting the total number of frames to be %d.\n", nFrames );
371 nFramesReal = nFrames;
372 }
373//printf( "Simulating %d frames.\n", nFramesReal );
374clk = Abc_Clock();
375 pProbs = Faig_ManSimulateFrames( pAig, nFramesReal, nPref, fTrans );
376//ABC_PRT( "Simulation", Abc_Clock() - clk );
377clk = Abc_Clock();
378 if ( fTrans )
379 {
380 Aig_Obj_t * pObj;
381 int i, Counter = 0;
382 pObj = Aig_ManConst1(p);
383 pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], (nFramesReal - nPref)/2 );
384 Aig_ManForEachCi( p, pObj, i )
385 pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], (nFramesReal - nPref)/2 );
386 Aig_ManForEachNode( p, pObj, i )
387 pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], (nFramesReal - nPref)/2 );
388 Aig_ManForEachCo( p, pObj, i )
389 pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], (nFramesReal - nPref)/2 );
390 assert( Counter == pAig->nObjs );
391 }
392 else if ( fProbOne )
393 {
394 Aig_Obj_t * pObj;
395 int i, Counter = 0;
396 pObj = Aig_ManConst1(p);
397 pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], nFramesReal - nPref );
398 Aig_ManForEachCi( p, pObj, i )
399 pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], nFramesReal - nPref );
400 Aig_ManForEachNode( p, pObj, i )
401 pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], nFramesReal - nPref );
402 Aig_ManForEachCo( p, pObj, i )
403 pSwitching[pObj->Id] = Faig_ManComputeProbOne( pProbs[Counter++], nFramesReal - nPref );
404 assert( Counter == pAig->nObjs );
405 }
406 else
407 {
408 Aig_Obj_t * pObj;
409 int i, Counter = 0;
410 pObj = Aig_ManConst1(p);
411 pSwitching[pObj->Id] = Faig_ManComputeSwitching( pProbs[Counter++], nFramesReal - nPref );
412 Aig_ManForEachCi( p, pObj, i )
413 pSwitching[pObj->Id] = Faig_ManComputeSwitching( pProbs[Counter++], nFramesReal - nPref );
414 Aig_ManForEachNode( p, pObj, i )
415 pSwitching[pObj->Id] = Faig_ManComputeSwitching( pProbs[Counter++], nFramesReal - nPref );
416 Aig_ManForEachCo( p, pObj, i )
417 pSwitching[pObj->Id] = Faig_ManComputeSwitching( pProbs[Counter++], nFramesReal - nPref );
418 assert( Counter == pAig->nObjs );
419 }
420 ABC_FREE( pProbs );
421 ABC_FREE( pAig );
422//ABC_PRT( "Switch ", Abc_Clock() - clk );
423//ABC_PRT( "TOTAL ", Abc_Clock() - clkTotal );
424 return vSwitching;
425}
426
438Vec_Int_t * Saig_ManComputeSwitchProb3s( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
439{
440// return Faig_ManComputeSwitchProbs( p, nFrames, nPref, fProbOne );
441 return NULL;
442}
443
444
448
449
451
int nWords
Definition abcNpn.c:127
ABC_INT64_T abctime
Definition abc_global.h:332
#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
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
unsigned Aig_ManRandom(int fReset)
Definition aigUtil.c:1170
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
ABC_DLL char * Abc_FrameReadFlag(char *pFlag)
Definition mainFrame.c:69
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
int * Faig_ManSimulateFrames(Faig_Man_t *p, int nFrames, int nPref, int fTrans)
Vec_Int_t * Saig_ManComputeSwitchProb3s(Aig_Man_t *p, int nFrames, int nPref, int fProbOne)
float Faig_ManComputeSwitching(int nOnes, int nSimWords)
typedefABC_NAMESPACE_IMPL_START struct Faig_Man_t_ Faig_Man_t
DECLARATIONS ///.
Definition saigSimFast.c:33
float Faig_ManComputeProbOne(int nOnes, int nSimWords)
int Faig_ManIsCorrect(Aig_Man_t *pAig)
FUNCTION DEFINITIONS ///.
Definition saigSimFast.c:93
Faig_Man_t * Faig_ManAlloc(Aig_Man_t *pAig)
Vec_Int_t * Faig_ManComputeSwitchProbs4(Aig_Man_t *p, int nFrames, int nPref, int fProbOne)
Faig_Man_t * Faig_ManCreate(Aig_Man_t *pAig)
int Id
Definition aig.h:85
int pObjs[0]
Definition saigSimFast.c:51
#define assert(ex)
Definition util_old.h:213
char * memset()