abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigSimSeq.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [saigSimSeq.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Sequential AIG package.]
8 
9  Synopsis [Fast sequential AIG simulator.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: saigSimSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "saig.h"
22 #include "proof/ssw/ssw.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 // combinational simulation manager
32 typedef struct Raig_Man_t_ Raig_Man_t;
33 struct Raig_Man_t_
34 {
35  // parameters
36  Aig_Man_t * pAig; // the AIG to be used for simulation
37  int nWords; // the number of words to simulate
38  // AIG representation
39  int nPis; // the number of primary inputs
40  int nPos; // the number of primary outputs
41  int nCis; // the number of combinational inputs
42  int nCos; // the number of combinational outputs
43  int nNodes; // the number of internal nodes
44  int nObjs; // nCis + nNodes + nCos + 2
45  int * pFans0; // fanin0 for all objects
46  int * pFans1; // fanin1 for all objects
47  Vec_Int_t * vCis2Ids; // mapping of CIs into their PI ids
48  Vec_Int_t * vLos; // register outputs
49  Vec_Int_t * vLis; // register inputs
50  // simulation info
51  int * pRefs; // reference counter for each node
52  unsigned * pSims; // simlulation information for each node
53  // recycable memory
54  unsigned * pMems; // allocated simulaton memory
55  int nWordsAlloc; // the number of allocated entries
56  int nMems; // the number of used entries
57  int nMemsMax; // the max number of used entries
58  int MemFree; // next free entry
59 };
60 
61 static inline int Raig_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
62 static inline int Raig_Lit2Var( int Lit ) { return Lit >> 1; }
63 static inline int Raig_LitIsCompl( int Lit ) { return Lit & 1; }
64 static inline int Raig_LitNot( int Lit ) { return Lit ^ 1; }
65 static inline int Raig_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
66 static inline int Raig_LitRegular( int Lit ) { return Lit & ~01; }
67 
68 ////////////////////////////////////////////////////////////////////////
69 /// FUNCTION DEFINITIONS ///
70 ////////////////////////////////////////////////////////////////////////
71 
72 /**Function*************************************************************
73 
74  Synopsis [Find the PO corresponding to the PO driver.]
75 
76  Description []
77 
78  SideEffects []
79 
80  SeeAlso []
81 
82 ***********************************************************************/
83 int Raig_ManFindPo( Aig_Man_t * pAig, int iNode )
84 {
85  Aig_Obj_t * pObj;
86  int i;
87  Saig_ManForEachPo( pAig, pObj, i )
88  if ( pObj->iData == iNode )
89  return i;
90  return -1;
91 }
92 
93 /**Function*************************************************************
94 
95  Synopsis [Creates fast simulation manager.]
96 
97  Description []
98 
99  SideEffects []
100 
101  SeeAlso []
102 
103 ***********************************************************************/
104 int Raig_ManCreate_rec( Raig_Man_t * p, Aig_Obj_t * pObj )
105 {
106  int iFan0, iFan1;
107  assert( !Aig_IsComplement(pObj) );
108  if ( pObj->iData )
109  return pObj->iData;
110  assert( !Aig_ObjIsConst1(pObj) );
111  if ( Aig_ObjIsNode(pObj) )
112  {
113  iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
114  iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj);
115  iFan1 = Raig_ManCreate_rec( p, Aig_ObjFanin1(pObj) );
116  iFan1 = (iFan1 << 1) | Aig_ObjFaninC1(pObj);
117  }
118  else if ( Aig_ObjIsCo(pObj) )
119  {
120  iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
121  iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj);
122  iFan1 = 0;
123  }
124  else
125  {
126  iFan0 = iFan1 = 0;
127  Vec_IntPush( p->vCis2Ids, Aig_ObjCioId(pObj) );
128  }
129  p->pFans0[p->nObjs] = iFan0;
130  p->pFans1[p->nObjs] = iFan1;
131  p->pRefs[p->nObjs] = Aig_ObjRefs(pObj);
132  return pObj->iData = p->nObjs++;
133 }
134 
135 /**Function*************************************************************
136 
137  Synopsis [Creates fast simulation manager.]
138 
139  Description []
140 
141  SideEffects []
142 
143  SeeAlso []
144 
145 ***********************************************************************/
146 Raig_Man_t * Raig_ManCreate( Aig_Man_t * pAig )
147 {
148  Raig_Man_t * p;
149  Aig_Obj_t * pObj;
150  int i, nObjs;
151  Aig_ManCleanData( pAig );
152  p = (Raig_Man_t *)ABC_ALLOC( Raig_Man_t, 1 );
153  memset( p, 0, sizeof(Raig_Man_t) );
154  p->pAig = pAig;
155  p->nPis = Saig_ManPiNum(pAig);
156  p->nPos = Saig_ManPoNum(pAig);
157  p->nCis = Aig_ManCiNum(pAig);
158  p->nCos = Aig_ManCoNum(pAig);
159  p->nNodes = Aig_ManNodeNum(pAig);
160  nObjs = p->nCis + p->nCos + p->nNodes + 2;
161  p->pFans0 = ABC_ALLOC( int, nObjs );
162  p->pFans1 = ABC_ALLOC( int, nObjs );
163  p->pRefs = ABC_ALLOC( int, nObjs );
164  p->pSims = ABC_CALLOC( unsigned, nObjs );
165  p->vCis2Ids = Vec_IntAlloc( Aig_ManCiNum(pAig) );
166  // add objects (0=unused; 1=const1)
167  p->nObjs = 2;
168  pObj = Aig_ManConst1( pAig );
169  pObj->iData = 1;
170  Aig_ManForEachCi( pAig, pObj, i )
171  if ( Aig_ObjRefs(pObj) == 0 )
172  Raig_ManCreate_rec( p, pObj );
173  Aig_ManForEachCo( pAig, pObj, i )
174  Raig_ManCreate_rec( p, pObj );
175  assert( Vec_IntSize(p->vCis2Ids) == Aig_ManCiNum(pAig) );
176  assert( p->nObjs == nObjs );
177  // collect flop outputs
178  p->vLos = Vec_IntAlloc( Aig_ManRegNum(pAig) );
179  Saig_ManForEachLo( pAig, pObj, i )
180  Vec_IntPush( p->vLos, pObj->iData );
181  // collect flop inputs
182  p->vLis = Vec_IntAlloc( Aig_ManRegNum(pAig) );
183  Saig_ManForEachLi( pAig, pObj, i )
184  {
185  Vec_IntPush( p->vLis, pObj->iData );
186  assert( p->pRefs[ pObj->iData ] == 0 );
187  p->pRefs[ pObj->iData ]++;
188  }
189  return p;
190 }
191 
192 /**Function*************************************************************
193 
194  Synopsis [Creates fast simulation manager.]
195 
196  Description []
197 
198  SideEffects []
199 
200  SeeAlso []
201 
202 ***********************************************************************/
203 void Raig_ManDelete( Raig_Man_t * p )
204 {
205  Vec_IntFree( p->vCis2Ids );
206  Vec_IntFree( p->vLos );
207  Vec_IntFree( p->vLis );
208  ABC_FREE( p->pFans0 );
209  ABC_FREE( p->pFans1 );
210  ABC_FREE( p->pRefs );
211  ABC_FREE( p->pSims );
212  ABC_FREE( p->pMems );
213  ABC_FREE( p );
214 }
215 
216 /**Function*************************************************************
217 
218  Synopsis [References simulation info.]
219 
220  Description []
221 
222  SideEffects []
223 
224  SeeAlso []
225 
226 ***********************************************************************/
227 unsigned * Raig_ManSimRef( Raig_Man_t * p, int i )
228 {
229  unsigned * pSim;
230  assert( i > 1 );
231  assert( p->pSims[i] == 0 );
232  if ( p->MemFree == 0 )
233  {
234  unsigned * pPlace, Ent;
235  if ( p->nWordsAlloc == 0 )
236  {
237  assert( p->pMems == NULL );
238  p->nWordsAlloc = (1<<17); // -> 1Mb
239  p->nMems = 1;
240  }
241  p->nWordsAlloc *= 2;
242  p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
243  memset( p->pMems, 0xff, sizeof(unsigned) * (p->nWords + 1) );
244  pPlace = (unsigned *)&p->MemFree;
245  for ( Ent = p->nMems * (p->nWords + 1);
246  Ent + p->nWords + 1 < (unsigned)p->nWordsAlloc;
247  Ent += p->nWords + 1 )
248  {
249  *pPlace = Ent;
250  pPlace = p->pMems + Ent;
251  }
252  *pPlace = 0;
253  }
254  p->pSims[i] = p->MemFree;
255  pSim = p->pMems + p->MemFree;
256  p->MemFree = pSim[0];
257  pSim[0] = p->pRefs[i];
258  p->nMems++;
259  if ( p->nMemsMax < p->nMems )
260  p->nMemsMax = p->nMems;
261  return pSim;
262 }
263 
264 /**Function*************************************************************
265 
266  Synopsis [Dereference simulaton info.]
267 
268  Description []
269 
270  SideEffects []
271 
272  SeeAlso []
273 
274 ***********************************************************************/
275 unsigned * Raig_ManSimDeref( Raig_Man_t * p, int i )
276 {
277  unsigned * pSim;
278  assert( i );
279  if ( i == 1 ) // const 1
280  return p->pMems;
281  assert( p->pSims[i] > 0 );
282  pSim = p->pMems + p->pSims[i];
283  if ( --pSim[0] == 0 )
284  {
285  pSim[0] = p->MemFree;
286  p->MemFree = p->pSims[i];
287  p->pSims[i] = 0;
288  p->nMems--;
289  }
290  return pSim;
291 }
292 
293 /**Function*************************************************************
294 
295  Synopsis [Simulates one round.]
296 
297  Description [Returns the number of PO entry if failed; 0 otherwise.]
298 
299  SideEffects []
300 
301  SeeAlso []
302 
303 ***********************************************************************/
304 int Raig_ManSimulateRound( Raig_Man_t * p, int fMiter, int fFirst, int * piPat )
305 {
306  unsigned * pRes0, * pRes1, * pRes;
307  int i, w, nCis, nCos, iFan0, iFan1, iPioNum;
308  // nove the values to the register outputs
309  Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
310  {
311  if ( iPioNum < p->nPis )
312  continue;
313  pRes = Raig_ManSimRef( p, Vec_IntEntry(p->vLos, iPioNum-p->nPis) );
314  if ( fFirst )
315  memset( pRes + 1, 0, sizeof(unsigned) * p->nWords );
316  else
317  {
318  pRes0 = Raig_ManSimDeref( p, Vec_IntEntry(p->vLis, iPioNum-p->nPis) );
319  for ( w = 1; w <= p->nWords; w++ )
320  pRes[w] = pRes0[w];
321  }
322  // handle unused PIs
323  if ( pRes[0] == 0 )
324  {
325  pRes[0] = 1;
326  Raig_ManSimDeref( p, Vec_IntEntry(p->vLos, iPioNum-p->nPis) );
327  }
328  }
329  // simulate the logic
330  nCis = nCos = 0;
331  for ( i = 2; i < p->nObjs; i++ )
332  {
333  if ( p->pFans0[i] == 0 ) // ci always has zero first fanin
334  {
335  iPioNum = Vec_IntEntry( p->vCis2Ids, nCis );
336  if ( iPioNum < p->nPis )
337  {
338  pRes = Raig_ManSimRef( p, i );
339  for ( w = 1; w <= p->nWords; w++ )
340  pRes[w] = Aig_ManRandom( 0 );
341  // handle unused PIs
342  if ( pRes[0] == 0 )
343  {
344  pRes[0] = 1;
345  Raig_ManSimDeref( p, i );
346  }
347  }
348  else
349  assert( Vec_IntEntry(p->vLos, iPioNum-p->nPis) == i );
350  nCis++;
351  continue;
352  }
353  if ( p->pFans1[i] == 0 ) // co always has non-zero 1st fanin and zero 2nd fanin
354  {
355  pRes0 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans0[i]) );
356  if ( nCos < p->nPos && fMiter )
357  {
358  unsigned Const = Raig_LitIsCompl(p->pFans0[i])? ~0 : 0;
359  for ( w = 1; w <= p->nWords; w++ )
360  if ( pRes0[w] != Const )
361  {
362  *piPat = 32*(w-1) + Aig_WordFindFirstBit( pRes0[w] ^ Const );
363  return i;
364  }
365  }
366  else
367  {
368  pRes = Raig_ManSimRef( p, i );
369  assert( pRes[0] == 1 );
370  if ( Raig_LitIsCompl(p->pFans0[i]) )
371  for ( w = 1; w <= p->nWords; w++ )
372  pRes[w] = ~pRes0[w];
373  else
374  for ( w = 1; w <= p->nWords; w++ )
375  pRes[w] = pRes0[w];
376  }
377  nCos++;
378  continue;
379  }
380  pRes = Raig_ManSimRef( p, i );
381  assert( pRes[0] > 0 );
382  iFan0 = p->pFans0[i];
383  iFan1 = p->pFans1[i];
384  pRes0 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans0[i]) );
385  pRes1 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans1[i]) );
386  if ( Raig_LitIsCompl(iFan0) && Raig_LitIsCompl(iFan1) )
387  for ( w = 1; w <= p->nWords; w++ )
388  pRes[w] = ~(pRes0[w] | pRes1[w]);
389  else if ( Raig_LitIsCompl(iFan0) && !Raig_LitIsCompl(iFan1) )
390  for ( w = 1; w <= p->nWords; w++ )
391  pRes[w] = ~pRes0[w] & pRes1[w];
392  else if ( !Raig_LitIsCompl(iFan0) && Raig_LitIsCompl(iFan1) )
393  for ( w = 1; w <= p->nWords; w++ )
394  pRes[w] = pRes0[w] & ~pRes1[w];
395  else if ( !Raig_LitIsCompl(iFan0) && !Raig_LitIsCompl(iFan1) )
396  for ( w = 1; w <= p->nWords; w++ )
397  pRes[w] = pRes0[w] & pRes1[w];
398  }
399  assert( nCis == p->nCis );
400  assert( nCos == p->nCos );
401  assert( p->nMems == 1 + Vec_IntSize(p->vLis) );
402  return 0;
403 }
404 
405 /**Function*************************************************************
406 
407  Synopsis [Returns the counter-example.]
408 
409  Description []
410 
411  SideEffects []
412 
413  SeeAlso []
414 
415 ***********************************************************************/
416 Abc_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids )
417 {
418  Abc_Cex_t * p;
419  unsigned * pData;
420  int f, i, w, iPioId, Counter;
421  p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
422  p->iFrame = iFrame;
423  p->iPo = iOut;
424  // fill in the binary data
425  Aig_ManRandom( 1 );
426  Counter = p->nRegs;
427  pData = ABC_ALLOC( unsigned, nWords );
428  for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
429  for ( i = 0; i < Aig_ManCiNum(pAig); i++ )
430  {
431  iPioId = Vec_IntEntry( vCis2Ids, i );
432  if ( iPioId >= p->nPis )
433  continue;
434  for ( w = 0; w < nWords; w++ )
435  pData[w] = Aig_ManRandom( 0 );
436  if ( Abc_InfoHasBit( pData, iPat ) )
437  Abc_InfoSetBit( p->pData, Counter + iPioId );
438  }
439  ABC_FREE( pData );
440  return p;
441 }
442 
443 /**Function*************************************************************
444 
445  Synopsis [Returns 1 if the bug is detected, 0 otherwise.]
446 
447  Description []
448 
449  SideEffects []
450 
451  SeeAlso []
452 
453 ***********************************************************************/
454 int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose )
455 {
456  Raig_Man_t * p;
457  Sec_MtrStatus_t Status;
458  int i, iPat, RetValue = 0;
459  abctime clk, clkTotal = Abc_Clock();
460  assert( Aig_ManRegNum(pAig) > 0 );
461  Status = Sec_MiterStatus( pAig );
462  if ( Status.nSat > 0 )
463  {
464  printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut );
465  return 1;
466  }
467  if ( Status.nUndec == 0 )
468  {
469  printf( "Miter is trivially unsatisfiable.\n" );
470  return 0;
471  }
472  Aig_ManRandom( 1 );
473  p = Raig_ManCreate( pAig );
474  p->nWords = nWords;
475  // iterate through objects
476  for ( i = 0; i < nIters; i++ )
477  {
478  clk = Abc_Clock();
479  RetValue = Raig_ManSimulateRound( p, fMiter, i==0, &iPat );
480  if ( fVerbose )
481  {
482  printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, nIters, TimeLimit );
483  printf("Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC);
484  }
485  if ( RetValue > 0 )
486  {
487  int iOut = Raig_ManFindPo(p->pAig, RetValue);
488  assert( pAig->pSeqModel == NULL );
489  pAig->pSeqModel = Raig_ManGenerateCounter( pAig, i, iOut, nWords, iPat, p->vCis2Ids );
490  if ( fVerbose )
491  printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
492  break;
493  }
494  if ( (Abc_Clock() - clk)/CLOCKS_PER_SEC >= TimeLimit )
495  {
496  printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, TimeLimit );
497  break;
498  }
499  }
500  if ( fVerbose )
501  {
502  printf( "Maxcut = %8d. AigMem = %7.2f MB. SimMem = %7.2f MB. ",
503  p->nMemsMax,
504  1.0*(p->nObjs * 16)/(1<<20),
505  1.0*(p->nMemsMax * 4 * (nWords+1))/(1<<20) );
506  ABC_PRT( "Total time", Abc_Clock() - clkTotal );
507  }
508  Raig_ManDelete( p );
509  return RetValue > 0;
510 }
511 
512 ////////////////////////////////////////////////////////////////////////
513 /// END OF FILE ///
514 ////////////////////////////////////////////////////////////////////////
515 
516 
517 ABC_NAMESPACE_IMPL_END
518 
memset
char * memset()
Raig_Man_t_::vLos
Vec_Int_t * vLos
Definition: saigSimSeq.c:48
Raig_Man_t_::nMemsMax
int nMemsMax
Definition: saigSimSeq.c:57
Raig_Man_t_::pSims
unsigned * pSims
Definition: saigSimSeq.c:52
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Raig_Var2Lit
static int Raig_Var2Lit(int Var, int fCompl)
Definition: saigSimSeq.c:61
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
Raig_Man_t_::nObjs
int nObjs
Definition: saigSimSeq.c:44
Raig_LitRegular
static int Raig_LitRegular(int Lit)
Definition: saigSimSeq.c:66
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Raig_LitIsCompl
static int Raig_LitIsCompl(int Lit)
Definition: saigSimSeq.c:63
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Raig_Lit2Var
static int Raig_Lit2Var(int Lit)
Definition: saigSimSeq.c:62
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Raig_Man_t_::nMems
int nMems
Definition: saigSimSeq.c:56
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
nWords
int nWords
Definition: abcNpn.c:127
for
for(p=first;p->value< newval;p=p->next)
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Raig_Man_t_::vLis
Vec_Int_t * vLis
Definition: saigSimSeq.c:49
Raig_ManSimulate
int Raig_ManSimulate(Aig_Man_t *pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose)
Definition: saigSimSeq.c:454
Raig_Man_t
typedefABC_NAMESPACE_IMPL_START struct Raig_Man_t_ Raig_Man_t
DECLARATIONS ///.
Definition: saigSimSeq.c:32
Raig_Man_t_::nPis
int nPis
Definition: saigSimSeq.c:39
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Raig_Man_t_::pFans1
int * pFans1
Definition: saigSimSeq.c:46
Raig_Man_t_::nCis
int nCis
Definition: saigSimSeq.c:41
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Raig_Man_t_::pAig
Aig_Man_t * pAig
Definition: saigSimSeq.c:36
Raig_Man_t_::MemFree
int MemFree
Definition: saigSimSeq.c:58
Raig_ManFindPo
int Raig_ManFindPo(Aig_Man_t *pAig, int iNode)
FUNCTION DEFINITIONS ///.
Definition: saigSimSeq.c:83
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_WordFindFirstBit
static int Aig_WordFindFirstBit(unsigned uWord)
Definition: aig.h:237
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Raig_Man_t_::nWordsAlloc
int nWordsAlloc
Definition: saigSimSeq.c:55
Raig_Man_t_::pMems
unsigned * pMems
Definition: saigSimSeq.c:54
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Raig_Man_t_::pFans0
int * pFans0
Definition: saigSimSeq.c:45
Counter
static int Counter
Definition: extraBddMisc.c:1877
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Sec_MiterStatus
Sec_MtrStatus_t Sec_MiterStatus(Aig_Man_t *p)
DECLARATIONS ///.
Definition: saigMiter.c:46
Raig_Man_t_::nCos
int nCos
Definition: saigSimSeq.c:42
Raig_Man_t_::nNodes
int nNodes
Definition: saigSimSeq.c:43
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Raig_ManCreate_rec
int Raig_ManCreate_rec(Raig_Man_t *p, Aig_Obj_t *pObj)
Definition: saigSimSeq.c:104
Raig_Man_t_::vCis2Ids
Vec_Int_t * vCis2Ids
Definition: saigSimSeq.c:47
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Raig_ManDelete
void Raig_ManDelete(Raig_Man_t *p)
Definition: saigSimSeq.c:203
Raig_Man_t_::nWords
int nWords
Definition: saigSimSeq.c:37
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Raig_ManSimulateRound
int Raig_ManSimulateRound(Raig_Man_t *p, int fMiter, int fFirst, int *piPat)
Definition: saigSimSeq.c:304
Raig_ManSimDeref
unsigned * Raig_ManSimDeref(Raig_Man_t *p, int i)
Definition: saigSimSeq.c:275
Raig_Man_t_::pRefs
int * pRefs
Definition: saigSimSeq.c:51
Aig_Obj_t_::iData
int iData
Definition: aig.h:88
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Raig_LitNot
static int Raig_LitNot(int Lit)
Definition: saigSimSeq.c:64
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Raig_ManCreate
Raig_Man_t * Raig_ManCreate(Aig_Man_t *pAig)
Definition: saigSimSeq.c:146
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Minisat::Var
int Var
Definition: SolverTypes.h:42
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Sec_MtrStatus_t
typedefABC_NAMESPACE_HEADER_START struct Sec_MtrStatus_t_ Sec_MtrStatus_t
INCLUDES ///.
Definition: saig.h:41
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
assert
#define assert(ex)
Definition: util_old.h:213
Raig_Man_t_::nPos
int nPos
Definition: saigSimSeq.c:40
Raig_LitNotCond
static int Raig_LitNotCond(int Lit, int c)
Definition: saigSimSeq.c:65
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Raig_ManSimRef
unsigned * Raig_ManSimRef(Raig_Man_t *p, int i)
Definition: saigSimSeq.c:227
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Raig_ManGenerateCounter
Abc_Cex_t * Raig_ManGenerateCounter(Aig_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t *vCis2Ids)
Definition: saigSimSeq.c:416
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Raig_Man_t_
Definition: saigSimSeq.c:33
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Aig_ObjCioId
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285