abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigSimMv.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [saigSimMv.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Sequential AIG package.]
8 
9  Synopsis [Multi-valued simulation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: saigSimMv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "saig.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 #define SAIG_DIFF_VALUES 8
31 #define SAIG_UNDEF_VALUE 0x1ffffffe //536870910
32 
33 // old AIG
34 typedef struct Saig_MvObj_t_ Saig_MvObj_t;
35 struct Saig_MvObj_t_
36 {
37  int iFan0;
38  int iFan1;
39  unsigned Type : 3;
40  unsigned Value : 29;
41 };
42 
43 // new AIG
44 typedef struct Saig_MvAnd_t_ Saig_MvAnd_t;
45 struct Saig_MvAnd_t_
46 {
47  int iFan0;
48  int iFan1;
49  int iNext;
50 };
51 
52 // simulation manager
53 typedef struct Saig_MvMan_t_ Saig_MvMan_t;
54 struct Saig_MvMan_t_
55 {
56  // user data
57  Aig_Man_t * pAig; // original AIG
58  // parameters
59  int nStatesMax; // maximum number of states
60  int nLevelsMax; // maximum number of levels
61  int nValuesMax; // maximum number of values
62  int nFlops; // number of flops
63  // compacted AIG
64  Saig_MvObj_t * pAigOld; // AIG objects
65  Vec_Ptr_t * vFlops; // collected flops
66  Vec_Int_t * vXFlops; // flops that had at least one X-value
67  Vec_Ptr_t * vTired; // collected flops
68  unsigned * pTStates; // hash table for states
69  int nTStatesSize; // hash table size
70  Aig_MmFixed_t * pMemStates; // memory for states
71  Vec_Ptr_t * vStates; // reached states
72  int * pRegsUndef; // count the number of undef values
73  int ** pRegsValues; // write the first different values
74  int * nRegsValues; // count the number of different values
75  int nRUndefs; // the number of undef registers
76  int nRValues[SAIG_DIFF_VALUES+1]; // the number of registers with given values
77  // internal AIG
78  Saig_MvAnd_t * pAigNew; // AIG nodes
79  int nObjsAlloc; // the number of objects allocated
80  int nObjs; // the number of objects
81  int nPis; // the number of primary inputs
82  int * pTNodes; // hash table
83  int nTNodesSize; // hash table size
84  unsigned char * pLevels; // levels of AIG nodes
85 };
86 
87 static inline int Saig_MvObjFaninC0( Saig_MvObj_t * pObj ) { return pObj->iFan0 & 1; }
88 static inline int Saig_MvObjFaninC1( Saig_MvObj_t * pObj ) { return pObj->iFan1 & 1; }
89 static inline int Saig_MvObjFanin0( Saig_MvObj_t * pObj ) { return pObj->iFan0 >> 1; }
90 static inline int Saig_MvObjFanin1( Saig_MvObj_t * pObj ) { return pObj->iFan1 >> 1; }
91 
92 static inline int Saig_MvConst0() { return 1; }
93 static inline int Saig_MvConst1() { return 0; }
94 static inline int Saig_MvConst( int c ) { return !c; }
95 static inline int Saig_MvUndef() { return SAIG_UNDEF_VALUE; }
96 
97 static inline int Saig_MvIsConst0( int iNode ) { return iNode == 1; }
98 static inline int Saig_MvIsConst1( int iNode ) { return iNode == 0; }
99 static inline int Saig_MvIsConst( int iNode ) { return iNode < 2; }
100 static inline int Saig_MvIsUndef( int iNode ) { return iNode == SAIG_UNDEF_VALUE; }
101 
102 static inline int Saig_MvRegular( int iNode ) { return (iNode & ~01); }
103 static inline int Saig_MvNot( int iNode ) { return (iNode ^ 01); }
104 static inline int Saig_MvNotCond( int iNode, int c ) { return (iNode ^ (c)); }
105 static inline int Saig_MvIsComplement( int iNode ) { return (int)(iNode & 01); }
106 
107 static inline int Saig_MvLit2Var( int iNode ) { return (iNode >> 1); }
108 static inline int Saig_MvVar2Lit( int iVar ) { return (iVar << 1); }
109 static inline int Saig_MvLev( Saig_MvMan_t * p, int iNode ) { return p->pLevels[iNode >> 1]; }
110 
111 // iterator over compacted objects
112 #define Saig_MvManForEachObj( pAig, pEntry ) \
113  for ( pEntry = pAig; pEntry->Type != AIG_OBJ_VOID; pEntry++ )
114 
115 ////////////////////////////////////////////////////////////////////////
116 /// FUNCTION DEFINITIONS ///
117 ////////////////////////////////////////////////////////////////////////
118 
119 /**Function*************************************************************
120 
121  Synopsis [Creates reduced manager.]
122 
123  Description []
124 
125  SideEffects []
126 
127  SeeAlso []
128 
129 ***********************************************************************/
130 Saig_MvObj_t * Saig_ManCreateReducedAig( Aig_Man_t * p, Vec_Ptr_t ** pvFlops )
131 {
132  Saig_MvObj_t * pAig, * pEntry;
133  Aig_Obj_t * pObj;
134  int i;
135  *pvFlops = Vec_PtrAlloc( Aig_ManRegNum(p) );
136  pAig = ABC_CALLOC( Saig_MvObj_t, Aig_ManObjNumMax(p)+1 );
137  Aig_ManForEachObj( p, pObj, i )
138  {
139  pEntry = pAig + i;
140  pEntry->Type = pObj->Type;
141  if ( Aig_ObjIsCi(pObj) || i == 0 )
142  {
143  if ( Saig_ObjIsLo(p, pObj) )
144  {
145  pEntry->iFan0 = (Saig_ObjLoToLi(p, pObj)->Id << 1);
146  pEntry->iFan1 = -1;
147  Vec_PtrPush( *pvFlops, pEntry );
148  }
149  continue;
150  }
151  pEntry->iFan0 = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj);
152  if ( Aig_ObjIsCo(pObj) )
153  continue;
154  assert( Aig_ObjIsNode(pObj) );
155  pEntry->iFan1 = (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj);
156  }
157  pEntry = pAig + Aig_ManObjNumMax(p);
158  pEntry->Type = AIG_OBJ_VOID;
159  return pAig;
160 }
161 
162 /**Function*************************************************************
163 
164  Synopsis [Creates a new node.]
165 
166  Description []
167 
168  SideEffects []
169 
170  SeeAlso []
171 
172 ***********************************************************************/
173 static inline int Saig_MvCreateObj( Saig_MvMan_t * p, int iFan0, int iFan1 )
174 {
175  Saig_MvAnd_t * pNode;
176  if ( p->nObjs == p->nObjsAlloc )
177  {
178  p->pAigNew = ABC_REALLOC( Saig_MvAnd_t, p->pAigNew, 2*p->nObjsAlloc );
179  p->pLevels = ABC_REALLOC( unsigned char, p->pLevels, 2*p->nObjsAlloc );
180  p->nObjsAlloc *= 2;
181  }
182  pNode = p->pAigNew + p->nObjs;
183  pNode->iFan0 = iFan0;
184  pNode->iFan1 = iFan1;
185  pNode->iNext = 0;
186  if ( iFan0 || iFan1 )
187  p->pLevels[p->nObjs] = 1 + Abc_MaxInt( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) );
188  else
189  p->pLevels[p->nObjs] = 0, p->nPis++;
190  return p->nObjs++;
191 }
192 
193 /**Function*************************************************************
194 
195  Synopsis [Creates multi-valued simulation manager.]
196 
197  Description []
198 
199  SideEffects []
200 
201  SeeAlso []
202 
203 ***********************************************************************/
204 Saig_MvMan_t * Saig_MvManStart( Aig_Man_t * pAig, int nFramesSatur )
205 {
206  Saig_MvMan_t * p;
207  int i;
208  assert( Aig_ManRegNum(pAig) > 0 );
209  p = (Saig_MvMan_t *)ABC_ALLOC( Saig_MvMan_t, 1 );
210  memset( p, 0, sizeof(Saig_MvMan_t) );
211  // set parameters
212  p->pAig = pAig;
213  p->nStatesMax = 2 * nFramesSatur + 100;
214  p->nLevelsMax = 4;
215  p->nValuesMax = SAIG_DIFF_VALUES;
216  p->nFlops = Aig_ManRegNum(pAig);
217  // compacted AIG
218  p->pAigOld = Saig_ManCreateReducedAig( pAig, &p->vFlops );
219  p->nTStatesSize = Abc_PrimeCudd( p->nStatesMax );
220  p->pTStates = ABC_CALLOC( unsigned, p->nTStatesSize );
221  p->pMemStates = Aig_MmFixedStart( sizeof(int) * (p->nFlops+1), p->nStatesMax );
222  p->vStates = Vec_PtrAlloc( p->nStatesMax );
223  Vec_PtrPush( p->vStates, NULL );
224  p->pRegsUndef = ABC_CALLOC( int, p->nFlops );
225  p->pRegsValues = ABC_ALLOC( int *, p->nFlops );
226  p->pRegsValues[0] = ABC_ALLOC( int, p->nValuesMax * p->nFlops );
227  for ( i = 1; i < p->nFlops; i++ )
228  p->pRegsValues[i] = p->pRegsValues[i-1] + p->nValuesMax;
229  p->nRegsValues = ABC_CALLOC( int, p->nFlops );
230  p->vTired = Vec_PtrAlloc( 100 );
231  // internal AIG
232  p->nObjsAlloc = 1000000;
233  p->pAigNew = ABC_ALLOC( Saig_MvAnd_t, p->nObjsAlloc );
234  p->nTNodesSize = Abc_PrimeCudd( p->nObjsAlloc / 3 );
235  p->pTNodes = ABC_CALLOC( int, p->nTNodesSize );
236  p->pLevels = ABC_ALLOC( unsigned char, p->nObjsAlloc );
237  Saig_MvCreateObj( p, 0, 0 );
238  return p;
239 }
240 
241 /**Function*************************************************************
242 
243  Synopsis [Destroys multi-valued simulation manager.]
244 
245  Description []
246 
247  SideEffects []
248 
249  SeeAlso []
250 
251 ***********************************************************************/
252 void Saig_MvManStop( Saig_MvMan_t * p )
253 {
254  Aig_MmFixedStop( p->pMemStates, 0 );
255  Vec_PtrFree( p->vStates );
256  Vec_IntFreeP( &p->vXFlops );
257  Vec_PtrFree( p->vFlops );
258  Vec_PtrFree( p->vTired );
259  ABC_FREE( p->pRegsValues[0] );
260  ABC_FREE( p->pRegsValues );
261  ABC_FREE( p->nRegsValues );
262  ABC_FREE( p->pRegsUndef );
263  ABC_FREE( p->pAigOld );
264  ABC_FREE( p->pTStates );
265  ABC_FREE( p->pAigNew );
266  ABC_FREE( p->pTNodes );
267  ABC_FREE( p->pLevels );
268  ABC_FREE( p );
269 }
270 
271 /**Function*************************************************************
272 
273  Synopsis [Hashing the node.]
274 
275  Description []
276 
277  SideEffects []
278 
279  SeeAlso []
280 
281 ***********************************************************************/
282 static inline int Saig_MvHash( int iFan0, int iFan1, int TableSize )
283 {
284  unsigned Key = 0;
285  assert( iFan0 < iFan1 );
286  Key ^= Saig_MvLit2Var(iFan0) * 7937;
287  Key ^= Saig_MvLit2Var(iFan1) * 2971;
288  Key ^= Saig_MvIsComplement(iFan0) * 911;
289  Key ^= Saig_MvIsComplement(iFan1) * 353;
290  return (int)(Key % TableSize);
291 }
292 
293 /**Function*************************************************************
294 
295  Synopsis [Returns the place where this node is stored (or should be stored).]
296 
297  Description []
298 
299  SideEffects []
300 
301  SeeAlso []
302 
303 ***********************************************************************/
304 static inline int * Saig_MvTableFind( Saig_MvMan_t * p, int iFan0, int iFan1 )
305 {
306  Saig_MvAnd_t * pEntry;
307  int * pPlace = p->pTNodes + Saig_MvHash( iFan0, iFan1, p->nTNodesSize );
308  for ( pEntry = (*pPlace)? p->pAigNew + *pPlace : NULL; pEntry;
309  pPlace = &pEntry->iNext, pEntry = (*pPlace)? p->pAigNew + *pPlace : NULL )
310  if ( pEntry->iFan0 == iFan0 && pEntry->iFan1 == iFan1 )
311  break;
312  return pPlace;
313 }
314 
315 /**Function*************************************************************
316 
317  Synopsis [Performs an AND-operation.]
318 
319  Description []
320 
321  SideEffects []
322 
323  SeeAlso []
324 
325 ***********************************************************************/
326 static inline int Saig_MvAnd( Saig_MvMan_t * p, int iFan0, int iFan1, int fFirst )
327 {
328  if ( iFan0 == iFan1 )
329  return iFan0;
330  if ( iFan0 == Saig_MvNot(iFan1) )
331  return Saig_MvConst0();
332  if ( Saig_MvIsConst(iFan0) )
333  return Saig_MvIsConst1(iFan0) ? iFan1 : Saig_MvConst0();
334  if ( Saig_MvIsConst(iFan1) )
335  return Saig_MvIsConst1(iFan1) ? iFan0 : Saig_MvConst0();
336  if ( Saig_MvIsUndef(iFan0) || Saig_MvIsUndef(iFan1) )
337  return Saig_MvUndef();
338 // if ( Saig_MvLev(p, iFan0) >= p->nLevelsMax || Saig_MvLev(p, iFan1) >= p->nLevelsMax )
339 // return Saig_MvUndef();
340 
341  // go undef after the first frame
342  if ( !fFirst )
343  return Saig_MvUndef();
344 
345  if ( iFan0 > iFan1 )
346  {
347  int Temp = iFan0;
348  iFan0 = iFan1;
349  iFan1 = Temp;
350  }
351  {
352  int * pPlace;
353  pPlace = Saig_MvTableFind( p, iFan0, iFan1 );
354  if ( *pPlace == 0 )
355  {
356  if ( pPlace >= (int*)p->pAigNew && pPlace < (int*)(p->pAigNew + p->nObjsAlloc) )
357  {
358  int iPlace = pPlace - (int*)p->pAigNew;
359  int iNode = Saig_MvCreateObj( p, iFan0, iFan1 );
360  ((int*)p->pAigNew)[iPlace] = iNode;
361  return Saig_MvVar2Lit( iNode );
362  }
363  else
364  *pPlace = Saig_MvCreateObj( p, iFan0, iFan1 );
365  }
366  return Saig_MvVar2Lit( *pPlace );
367  }
368 }
369 
370 /**Function*************************************************************
371 
372  Synopsis [Propagates one edge.]
373 
374  Description []
375 
376  SideEffects []
377 
378  SeeAlso []
379 
380 ***********************************************************************/
381 static inline int Saig_MvSimulateValue0( Saig_MvObj_t * pAig, Saig_MvObj_t * pObj )
382 {
383  Saig_MvObj_t * pObj0 = pAig + Saig_MvObjFanin0(pObj);
384  if ( Saig_MvIsUndef( pObj0->Value ) )
385  return Saig_MvUndef();
386  return Saig_MvNotCond( pObj0->Value, Saig_MvObjFaninC0(pObj) );
387 }
388 static inline int Saig_MvSimulateValue1( Saig_MvObj_t * pAig, Saig_MvObj_t * pObj )
389 {
390  Saig_MvObj_t * pObj1 = pAig + Saig_MvObjFanin1(pObj);
391  if ( Saig_MvIsUndef( pObj1->Value ) )
392  return Saig_MvUndef();
393  return Saig_MvNotCond( pObj1->Value, Saig_MvObjFaninC1(pObj) );
394 }
395 
396 /**Function*************************************************************
397 
398  Synopsis [Prints MV state.]
399 
400  Description []
401 
402  SideEffects []
403 
404  SeeAlso []
405 
406 ***********************************************************************/
407 void Saig_MvPrintState( int Iter, Saig_MvMan_t * p )
408 {
409  Saig_MvObj_t * pEntry;
410  int i;
411  printf( "%3d : ", Iter );
412  Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
413  {
414  if ( pEntry->Value == SAIG_UNDEF_VALUE )
415  printf( " *" );
416  else
417  printf( "%5d", pEntry->Value );
418  }
419  printf( "\n" );
420 }
421 
422 /**Function*************************************************************
423 
424  Synopsis [Performs one iteration of simulation.]
425 
426  Description []
427 
428  SideEffects []
429 
430  SeeAlso []
431 
432 ***********************************************************************/
433 void Saig_MvSimulateFrame( Saig_MvMan_t * p, int fFirst, int fVerbose )
434 {
435  Saig_MvObj_t * pEntry;
436  int i;
437  Saig_MvManForEachObj( p->pAigOld, pEntry )
438  {
439  if ( pEntry->Type == AIG_OBJ_AND )
440  {
441  pEntry->Value = Saig_MvAnd( p,
442  Saig_MvSimulateValue0(p->pAigOld, pEntry),
443  Saig_MvSimulateValue1(p->pAigOld, pEntry), fFirst );
444  }
445  else if ( pEntry->Type == AIG_OBJ_CO )
446  pEntry->Value = Saig_MvSimulateValue0(p->pAigOld, pEntry);
447  else if ( pEntry->Type == AIG_OBJ_CI )
448  {
449  if ( pEntry->iFan1 == 0 ) // true PI
450  {
451  if ( fFirst )
452  pEntry->Value = Saig_MvVar2Lit( Saig_MvCreateObj( p, 0, 0 ) );
453  else
454  pEntry->Value = SAIG_UNDEF_VALUE;
455  }
456 // else if ( fFirst ) // register output
457 // pEntry->Value = Saig_MvConst0();
458 // else
459 // pEntry->Value = Saig_MvSimulateValue0(p->pAigOld, pEntry);
460  }
461  else if ( pEntry->Type == AIG_OBJ_CONST1 )
462  pEntry->Value = Saig_MvConst1();
463  else if ( pEntry->Type != AIG_OBJ_NONE )
464  assert( 0 );
465  }
466  // transfer to registers
467  Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
468  pEntry->Value = Saig_MvSimulateValue0( p->pAigOld, pEntry );
469 }
470 
471 
472 /**Function*************************************************************
473 
474  Synopsis [Computes hash value of the node using its simulation info.]
475 
476  Description []
477 
478  SideEffects []
479 
480  SeeAlso []
481 
482 ***********************************************************************/
483 int Saig_MvSimHash( unsigned * pState, int nFlops, int TableSize )
484 {
485  static int s_SPrimes[16] = {
486  1610612741,
487  805306457,
488  402653189,
489  201326611,
490  100663319,
491  50331653,
492  25165843,
493  12582917,
494  6291469,
495  3145739,
496  1572869,
497  786433,
498  393241,
499  196613,
500  98317,
501  49157
502  };
503  unsigned uHash = 0;
504  int i;
505  for ( i = 0; i < nFlops; i++ )
506  uHash ^= pState[i] * s_SPrimes[i & 0xF];
507  return (int)(uHash % TableSize);
508 }
509 
510 /**Function*************************************************************
511 
512  Synopsis [Returns the place where this state is stored (or should be stored).]
513 
514  Description []
515 
516  SideEffects []
517 
518  SeeAlso []
519 
520 ***********************************************************************/
521 static inline unsigned * Saig_MvSimTableFind( Saig_MvMan_t * p, unsigned * pState )
522 {
523  unsigned * pEntry;
524  unsigned * pPlace = p->pTStates + Saig_MvSimHash( pState+1, p->nFlops, p->nTStatesSize );
525  for ( pEntry = (*pPlace)? (unsigned *)Vec_PtrEntry(p->vStates, *pPlace) : NULL; pEntry;
526  pPlace = pEntry, pEntry = (*pPlace)? (unsigned *)Vec_PtrEntry(p->vStates, *pPlace) : NULL )
527  if ( memcmp( pEntry+1, pState+1, sizeof(int)*p->nFlops ) == 0 )
528  break;
529  return pPlace;
530 }
531 
532 /**Function*************************************************************
533 
534  Synopsis [Saves current state.]
535 
536  Description [Returns -1 if there is no fixed point.]
537 
538  SideEffects []
539 
540  SeeAlso []
541 
542 ***********************************************************************/
543 int Saig_MvSaveState( Saig_MvMan_t * p )
544 {
545  Saig_MvObj_t * pEntry;
546  unsigned * pState, * pPlace;
547  int i;
548  pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMemStates );
549  pState[0] = 0;
550  Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
551  pState[i+1] = pEntry->Value;
552  pPlace = Saig_MvSimTableFind( p, pState );
553  if ( *pPlace )
554  return *pPlace;
555  *pPlace = Vec_PtrSize( p->vStates );
556  Vec_PtrPush( p->vStates, pState );
557  return -1;
558 }
559 
560 /**Function*************************************************************
561 
562  Synopsis [Performs multi-valued simulation.]
563 
564  Description []
565 
566  SideEffects []
567 
568  SeeAlso []
569 
570 ***********************************************************************/
571 void Saig_MvManPostProcess( Saig_MvMan_t * p, int iState )
572 {
573  Saig_MvObj_t * pEntry;
574  unsigned * pState;
575  int i, k, j, nTotal = 0, iFlop;
576  Vec_Int_t * vUniques = Vec_IntAlloc( 100 );
577  Vec_Int_t * vCounter = Vec_IntAlloc( 100 );
578  // count registers that never became undef
579  Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
580  if ( p->pRegsUndef[i] == 0 )
581  nTotal++;
582  printf( "The number of registers that never became undef = %d. (Total = %d.)\n", nTotal, p->nFlops );
583  Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
584  {
585  if ( p->pRegsUndef[i] )
586  continue;
587  Vec_IntForEachEntry( vUniques, iFlop, k )
588  {
589  Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, j, 1 )
590  if ( pState[iFlop+1] != pState[i+1] )
591  break;
592  if ( j == Vec_PtrSize(p->vStates) )
593  {
594  Vec_IntAddToEntry( vCounter, k, 1 );
595  break;
596  }
597  }
598  if ( k == Vec_IntSize(vUniques) )
599  {
600  Vec_IntPush( vUniques, i );
601  Vec_IntPush( vCounter, 1 );
602  }
603  }
604  Vec_IntForEachEntry( vUniques, iFlop, i )
605  {
606  printf( "FLOP %5d : (%3d) ", iFlop, Vec_IntEntry(vCounter,i) );
607 /*
608  for ( k = 0; k < p->nRegsValues[iFlop]; k++ )
609  if ( p->pRegsValues[iFlop][k] == SAIG_UNDEF_VALUE )
610  printf( "* " );
611  else
612  printf( "%d ", p->pRegsValues[iFlop][k] );
613  printf( "\n" );
614 */
615  Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, k, 1 )
616  {
617  if ( k == iState+1 )
618  printf( " # " );
619  if ( pState[iFlop+1] == SAIG_UNDEF_VALUE )
620  printf( "*" );
621  else
622  printf( "%d", pState[iFlop+1] );
623  }
624  printf( "\n" );
625 // if ( ++Counter == 10 )
626 // break;
627  }
628 
629  Vec_IntFree( vUniques );
630  Vec_IntFree( vCounter );
631 }
632 
633 /**Function*************************************************************
634 
635  Synopsis [Performs multi-valued simulation.]
636 
637  Description []
638 
639  SideEffects []
640 
641  SeeAlso []
642 
643 ***********************************************************************/
644 Vec_Int_t * Saig_MvManFindXFlops( Saig_MvMan_t * p )
645 {
646  Vec_Int_t * vXFlops;
647  unsigned * pState;
648  int i, k;
649  vXFlops = Vec_IntStart( p->nFlops );
650  Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, i, 1 )
651  {
652  for ( k = 0; k < p->nFlops; k++ )
653  if ( Saig_MvIsUndef(pState[k+1]) )
654  Vec_IntWriteEntry( vXFlops, k, 1 );
655  }
656  return vXFlops;
657 }
658 
659 /**Function*************************************************************
660 
661  Synopsis [Checks if the flop is an oscilator.]
662 
663  Description []
664 
665  SideEffects []
666 
667  SeeAlso []
668 
669 ***********************************************************************/
670 int Saig_MvManCheckOscilator( Saig_MvMan_t * p, int iFlop )
671 {
672  Vec_Int_t * vValues;
673  unsigned * pState;
674  int k, Per, Entry;
675  // collect values of this flop
676  vValues = Vec_IntAlloc( 100 );
677  Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, k, 1 )
678  {
679  Vec_IntPush( vValues, pState[iFlop+1] );
680 //printf( "%d ", pState[iFlop+1] );
681  }
682 //printf( "\n" );
683  assert( Saig_MvIsConst0( Vec_IntEntry(vValues,0) ) );
684  // look for constants
685  for ( Per = 0; Per < Vec_IntSize(vValues)/2; Per++ )
686  {
687  // find the first non-const0
688  Vec_IntForEachEntryStart( vValues, Entry, Per, Per )
689  if ( !Saig_MvIsConst0(Entry) )
690  break;
691  if ( Per == Vec_IntSize(vValues) )
692  break;
693  // find the first const0
694  Vec_IntForEachEntryStart( vValues, Entry, Per, Per )
695  if ( Saig_MvIsConst0(Entry) )
696  break;
697  if ( Per == Vec_IntSize(vValues) )
698  break;
699  // try to determine period
700  assert( Saig_MvIsConst0( Vec_IntEntry(vValues,Per) ) );
701  for ( k = Per; k < Vec_IntSize(vValues); k++ )
702  if ( Vec_IntEntry(vValues, k-Per) != Vec_IntEntry(vValues, k) )
703  break;
704  if ( k < Vec_IntSize(vValues) )
705  continue;
706  Vec_IntFree( vValues );
707 //printf( "Period = %d\n", Per );
708  return Per;
709  }
710  Vec_IntFree( vValues );
711  return 0;
712 }
713 
714 /**Function*************************************************************
715 
716  Synopsis [Returns const0 and binary flops.]
717 
718  Description []
719 
720  SideEffects []
721 
722  SeeAlso []
723 
724 ***********************************************************************/
725 Vec_Int_t * Saig_MvManFindConstBinaryFlops( Saig_MvMan_t * p, Vec_Int_t ** pvBinary )
726 {
727  unsigned * pState;
728  Vec_Int_t * vBinary, * vConst0;
729  int i, k, fConst0;
730  // detect constant flops
731  vConst0 = Vec_IntAlloc( p->nFlops );
732  vBinary = Vec_IntAlloc( p->nFlops );
733  for ( k = 0; k < p->nFlops; k++ )
734  {
735  // check if this flop is constant 0 in all states
736  fConst0 = 1;
737  Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, i, 1 )
738  {
739  if ( !Saig_MvIsConst0(pState[k+1]) )
740  fConst0 = 0;
741  if ( Saig_MvIsUndef(pState[k+1]) )
742  break;
743  }
744  if ( i < Vec_PtrSize(p->vStates) )
745  continue;
746  // the flop is binary-valued
747  if ( fConst0 )
748  Vec_IntPush( vConst0, k );
749  else
750  Vec_IntPush( vBinary, k );
751  }
752  *pvBinary = vBinary;
753  return vConst0;
754 }
755 
756 /**Function*************************************************************
757 
758  Synopsis [Find oscilators.]
759 
760  Description []
761 
762  SideEffects []
763 
764  SeeAlso []
765 
766 ***********************************************************************/
767 Vec_Int_t * Saig_MvManFindOscilators( Saig_MvMan_t * p, Vec_Int_t ** pvConst0 )
768 {
769  Vec_Int_t * vBinary, * vOscils;
770  int Entry, i;
771  // detect constant flops
772  *pvConst0 = Saig_MvManFindConstBinaryFlops( p, &vBinary );
773  // check binary flops
774  vOscils = Vec_IntAlloc( 100 );
775  Vec_IntForEachEntry( vBinary, Entry, i )
776  if ( Saig_MvManCheckOscilator( p, Entry ) )
777  Vec_IntPush( vOscils, Entry );
778  Vec_IntFree( vBinary );
779  return vOscils;
780 }
781 
782 /**Function*************************************************************
783 
784  Synopsis [Find constants and oscilators.]
785 
786  Description []
787 
788  SideEffects []
789 
790  SeeAlso []
791 
792 ***********************************************************************/
793 Vec_Int_t * Saig_MvManCreateNextSkip( Saig_MvMan_t * p )
794 {
795  Vec_Int_t * vConst0, * vOscils, * vXFlops;
796  int i, Entry;
797  vOscils = Saig_MvManFindOscilators( p, &vConst0 );
798 //printf( "Found %d constants and %d oscilators.\n", Vec_IntSize(vConst0), Vec_IntSize(vOscils) );
799  vXFlops = Vec_IntAlloc( p->nFlops );
800  Vec_IntFill( vXFlops, p->nFlops, 1 );
801  Vec_IntForEachEntry( vConst0, Entry, i )
802  Vec_IntWriteEntry( vXFlops, Entry, 0 );
803  Vec_IntForEachEntry( vOscils, Entry, i )
804  Vec_IntWriteEntry( vXFlops, Entry, 0 );
805  Vec_IntFree( vOscils );
806  Vec_IntFree( vConst0 );
807  return vXFlops;
808 }
809 
810 /**Function*************************************************************
811 
812  Synopsis [Finds equivalent flops.]
813 
814  Description []
815 
816  SideEffects []
817 
818  SeeAlso []
819 
820 ***********************************************************************/
821 Vec_Ptr_t * Saig_MvManDeriveMap( Saig_MvMan_t * p, int fVerbose )
822 {
823  Vec_Int_t * vConst0, * vBinValued;
824  Vec_Ptr_t * vMap = NULL;
825  Aig_Obj_t * pObj;
826  unsigned * pState;
827  int i, k, j, FlopK, FlopJ;
828  int Counter1 = 0, Counter2 = 0;
829  // prepare CI map
830  vMap = Vec_PtrAlloc( Aig_ManCiNum(p->pAig) );
831  Aig_ManForEachCi( p->pAig, pObj, i )
832  Vec_PtrPush( vMap, pObj );
833  // detect constant flops
834  vConst0 = Saig_MvManFindConstBinaryFlops( p, &vBinValued );
835  // set constants
836  Vec_IntForEachEntry( vConst0, FlopK, k )
837  {
838  Vec_PtrWriteEntry( vMap, Saig_ManPiNum(p->pAig) + FlopK, Aig_ManConst0(p->pAig) );
839  Counter1++;
840  }
841  Vec_IntFree( vConst0 );
842 
843  // detect equivalent (non-ternary flops)
844  Vec_IntForEachEntry( vBinValued, FlopK, k )
845  if ( FlopK >= 0 )
846  Vec_IntForEachEntryStart( vBinValued, FlopJ, j, k+1 )
847  if ( FlopJ >= 0 )
848  {
849  // check if they are equal
850  Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, i, 1 )
851  if ( pState[FlopK+1] != pState[FlopJ+1] )
852  break;
853  if ( i < Vec_PtrSize(p->vStates) )
854  continue;
855  // set the equivalence
856  Vec_PtrWriteEntry( vMap, Saig_ManPiNum(p->pAig) + FlopJ, Saig_ManLo(p->pAig, FlopK) );
857  Vec_IntWriteEntry( vBinValued, j, -1 );
858  Counter2++;
859  }
860  if ( fVerbose )
861  printf( "Detected %d const0 flops and %d pairs of equiv binary flops.\n", Counter1, Counter2 );
862  Vec_IntFree( vBinValued );
863  if ( Counter1 == 0 && Counter2 == 0 )
864  Vec_PtrFreeP( &vMap );
865  return vMap;
866 }
867 
868 /**Function*************************************************************
869 
870  Synopsis [Performs multi-valued simulation.]
871 
872  Description []
873 
874  SideEffects []
875 
876  SeeAlso []
877 
878 ***********************************************************************/
879 Vec_Ptr_t * Saig_MvManSimulate( Aig_Man_t * pAig, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose )
880 {
881  Vec_Ptr_t * vMap;
882  Saig_MvMan_t * p;
883  Saig_MvObj_t * pEntry;
884  int f, i, iState;
885  abctime clk = Abc_Clock();
886  assert( nFramesSymb >= 1 && nFramesSymb <= nFramesSatur );
887 
888  // start manager
889  p = Saig_MvManStart( pAig, nFramesSatur );
890 if ( fVerbose )
891 ABC_PRT( "Constructing the problem", Abc_Clock() - clk );
892 
893  // initialize registers
894  Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
895  pEntry->Value = Saig_MvConst0();
896  Saig_MvSaveState( p );
897  if ( fVeryVerbose )
898  Saig_MvPrintState( 0, p );
899  // simulate until convergence
900  clk = Abc_Clock();
901  for ( f = 0; ; f++ )
902  {
903  if ( f == nFramesSatur )
904  {
905  if ( fVerbose )
906  printf( "Begining to saturate simulation after %d frames\n", f );
907  // find all flops that have at least one X value in the past and set them to X forever
908  p->vXFlops = Saig_MvManFindXFlops( p );
909  }
910  if ( f == 2 * nFramesSatur )
911  {
912  if ( fVerbose )
913  printf( "Agressively saturating simulation after %d frames\n", f );
914  Vec_IntFree( p->vXFlops );
915  p->vXFlops = Saig_MvManCreateNextSkip( p );
916  }
917  // retire some flops
918  if ( p->vXFlops )
919  {
920  Vec_PtrForEachEntry( Saig_MvObj_t *, p->vFlops, pEntry, i )
921  if ( Vec_IntEntry( p->vXFlops, i ) )
922  pEntry->Value = SAIG_UNDEF_VALUE;
923  }
924  // simulate timeframe
925  Saig_MvSimulateFrame( p, (int)(f < nFramesSymb), fVerbose );
926  // save and print state
927  iState = Saig_MvSaveState( p );
928  if ( fVeryVerbose )
929  Saig_MvPrintState( f+1, p );
930  if ( iState >= 0 )
931  {
932  if ( fVerbose )
933  printf( "Converged after %d frames with lasso in state %d. Cycle = %d.\n", f+1, iState-1, f+2-iState );
934 // printf( "Total number of PIs = %d. AND nodes = %d.\n", p->nPis, p->nObjs - p->nPis );
935  break;
936  }
937  }
938 // printf( "Coverged after %d frames.\n", f );
939 if ( fVerbose )
940 ABC_PRT( "Multi-valued simulation", Abc_Clock() - clk );
941  // implement equivalences
942 // Saig_MvManPostProcess( p, iState-1 );
943  vMap = Saig_MvManDeriveMap( p, fVerbose );
944  Saig_MvManStop( p );
945 // return Aig_ManDupSimple( pAig );
946  return vMap;
947 }
948 
949 
950 ////////////////////////////////////////////////////////////////////////
951 /// END OF FILE ///
952 ////////////////////////////////////////////////////////////////////////
953 
954 
955 ABC_NAMESPACE_IMPL_END
956 
memset
char * memset()
Saig_MvLev
static int Saig_MvLev(Saig_MvMan_t *p, int iNode)
Definition: saigSimMv.c:109
Saig_MvManFindOscilators
Vec_Int_t * Saig_MvManFindOscilators(Saig_MvMan_t *p, Vec_Int_t **pvConst0)
Definition: saigSimMv.c:767
Saig_MvMan_t_::pAig
Aig_Man_t * pAig
Definition: saigSimMv.c:57
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Aig_ObjFaninId0
static int Aig_ObjFaninId0(Aig_Obj_t *pObj)
Definition: aig.h:304
Saig_MvUndef
static int Saig_MvUndef()
Definition: saigSimMv.c:95
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
Saig_MvMan_t_::nValuesMax
int nValuesMax
Definition: saigSimMv.c:61
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
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
Saig_MvMan_t_::pRegsUndef
int * pRegsUndef
Definition: saigSimMv.c:72
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Saig_MvSimHash
int Saig_MvSimHash(unsigned *pState, int nFlops, int TableSize)
Definition: saigSimMv.c:483
AIG_OBJ_CO
Definition: aig.h:61
Aig_Obj_t_::Type
unsigned int Type
Definition: aig.h:77
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
Saig_MvMan_t_::nObjs
int nObjs
Definition: saigSimMv.c:80
Saig_MvMan_t_::nPis
int nPis
Definition: saigSimMv.c:81
Saig_ManLo
static Aig_Obj_t * Saig_ManLo(Aig_Man_t *p, int i)
Definition: saig.h:79
Aig_MmFixedStop
void Aig_MmFixedStop(Aig_MmFixed_t *p, int fVerbose)
Definition: aigMem.c:132
Saig_MvMan_t_::pRegsValues
int ** pRegsValues
Definition: saigSimMv.c:73
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Saig_ManCreateReducedAig
Saig_MvObj_t * Saig_ManCreateReducedAig(Aig_Man_t *p, Vec_Ptr_t **pvFlops)
FUNCTION DEFINITIONS ///.
Definition: saigSimMv.c:130
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ManConst0
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
Saig_MvMan_t_::nRValues
int nRValues[SAIG_DIFF_VALUES+1]
Definition: saigSimMv.c:76
Saig_MvConst0
static int Saig_MvConst0()
Definition: saigSimMv.c:92
Saig_MvManFindXFlops
Vec_Int_t * Saig_MvManFindXFlops(Saig_MvMan_t *p)
Definition: saigSimMv.c:644
Saig_MvCreateObj
static int Saig_MvCreateObj(Saig_MvMan_t *p, int iFan0, int iFan1)
Definition: saigSimMv.c:173
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Saig_MvManCheckOscilator
int Saig_MvManCheckOscilator(Saig_MvMan_t *p, int iFlop)
Definition: saigSimMv.c:670
Saig_MvMan_t_::pAigOld
Saig_MvObj_t * pAigOld
Definition: saigSimMv.c:64
Saig_MvMan_t_::pTStates
unsigned * pTStates
Definition: saigSimMv.c:68
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Aig_ObjFaninId1
static int Aig_ObjFaninId1(Aig_Obj_t *pObj)
Definition: aig.h:305
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_MmFixedStart
Aig_MmFixed_t * Aig_MmFixedStart(int nEntrySize, int nEntriesMax)
FUNCTION DEFINITIONS ///.
Definition: aigMem.c:96
Saig_MvPrintState
void Saig_MvPrintState(int Iter, Saig_MvMan_t *p)
Definition: saigSimMv.c:407
Saig_MvVar2Lit
static int Saig_MvVar2Lit(int iVar)
Definition: saigSimMv.c:108
Saig_MvTableFind
static int * Saig_MvTableFind(Saig_MvMan_t *p, int iFan0, int iFan1)
Definition: saigSimMv.c:304
Saig_MvManCreateNextSkip
Vec_Int_t * Saig_MvManCreateNextSkip(Saig_MvMan_t *p)
Definition: saigSimMv.c:793
Aig_MmFixed_t_
DECLARATIONS ///.
Definition: aigMem.c:30
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Saig_MvObjFanin0
static int Saig_MvObjFanin0(Saig_MvObj_t *pObj)
Definition: saigSimMv.c:89
Saig_MvObj_t_::Value
unsigned Value
Definition: saigSimMv.c:40
Saig_MvSimulateFrame
void Saig_MvSimulateFrame(Saig_MvMan_t *p, int fFirst, int fVerbose)
Definition: saigSimMv.c:433
Saig_MvManFindConstBinaryFlops
Vec_Int_t * Saig_MvManFindConstBinaryFlops(Saig_MvMan_t *p, Vec_Int_t **pvBinary)
Definition: saigSimMv.c:725
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Saig_MvObjFanin1
static int Saig_MvObjFanin1(Saig_MvObj_t *pObj)
Definition: saigSimMv.c:90
Saig_MvMan_t_::nRUndefs
int nRUndefs
Definition: saigSimMv.c:75
Saig_MvObjFaninC1
static int Saig_MvObjFaninC1(Saig_MvObj_t *pObj)
Definition: saigSimMv.c:88
Saig_MvMan_t_::nFlops
int nFlops
Definition: saigSimMv.c:62
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Saig_MvObj_t_
Definition: saigSimMv.c:35
Saig_MvIsConst1
static int Saig_MvIsConst1(int iNode)
Definition: saigSimMv.c:98
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
Saig_MvObjFaninC0
static int Saig_MvObjFaninC0(Saig_MvObj_t *pObj)
Definition: saigSimMv.c:87
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
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
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Saig_MvMan_t_::nTStatesSize
int nTStatesSize
Definition: saigSimMv.c:69
memcmp
int memcmp()
Saig_MvSimulateValue0
static int Saig_MvSimulateValue0(Saig_MvObj_t *pAig, Saig_MvObj_t *pObj)
Definition: saigSimMv.c:381
Aig_MmFixedEntryFetch
char * Aig_MmFixedEntryFetch(Aig_MmFixed_t *p)
Definition: aigMem.c:161
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Saig_MvMan_t_::nLevelsMax
int nLevelsMax
Definition: saigSimMv.c:60
Saig_MvLit2Var
static int Saig_MvLit2Var(int iNode)
Definition: saigSimMv.c:107
SAIG_UNDEF_VALUE
#define SAIG_UNDEF_VALUE
Definition: saigSimMv.c:31
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Saig_MvManStart
Saig_MvMan_t * Saig_MvManStart(Aig_Man_t *pAig, int nFramesSatur)
Definition: saigSimMv.c:204
Saig_MvConst1
static int Saig_MvConst1()
Definition: saigSimMv.c:93
Saig_MvMan_t_::pLevels
unsigned char * pLevels
Definition: saigSimMv.c:84
Saig_MvManSimulate
Vec_Ptr_t * Saig_MvManSimulate(Aig_Man_t *pAig, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose)
Definition: saigSimMv.c:879
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Saig_MvMan_t_::vStates
Vec_Ptr_t * vStates
Definition: saigSimMv.c:71
Saig_MvNotCond
static int Saig_MvNotCond(int iNode, int c)
Definition: saigSimMv.c:104
Saig_MvMan_t_::pTNodes
int * pTNodes
Definition: saigSimMv.c:82
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Saig_MvIsConst
static int Saig_MvIsConst(int iNode)
Definition: saigSimMv.c:99
Saig_MvManStop
void Saig_MvManStop(Saig_MvMan_t *p)
Definition: saigSimMv.c:252
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Saig_MvAnd
static int Saig_MvAnd(Saig_MvMan_t *p, int iFan0, int iFan1, int fFirst)
Definition: saigSimMv.c:326
Saig_MvHash
static int Saig_MvHash(int iFan0, int iFan1, int TableSize)
Definition: saigSimMv.c:282
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Saig_MvMan_t_::vTired
Vec_Ptr_t * vTired
Definition: saigSimMv.c:67
Saig_MvAnd_t_::iFan0
int iFan0
Definition: saigSimMv.c:47
Saig_MvIsUndef
static int Saig_MvIsUndef(int iNode)
Definition: saigSimMv.c:100
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Saig_MvMan_t_::nStatesMax
int nStatesMax
Definition: saigSimMv.c:59
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Saig_MvSimTableFind
static unsigned * Saig_MvSimTableFind(Saig_MvMan_t *p, unsigned *pState)
Definition: saigSimMv.c:521
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Saig_MvMan_t_::nRegsValues
int * nRegsValues
Definition: saigSimMv.c:74
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Saig_MvMan_t_::nTNodesSize
int nTNodesSize
Definition: saigSimMv.c:83
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Saig_MvObj_t_::iFan0
int iFan0
Definition: saigSimMv.c:37
Saig_MvAnd_t_::iNext
int iNext
Definition: saigSimMv.c:49
Saig_MvObj_t_::Type
unsigned Type
Definition: saigSimMv.c:39
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Saig_MvRegular
static int Saig_MvRegular(int iNode)
Definition: saigSimMv.c:102
Saig_MvMan_t_::pMemStates
Aig_MmFixed_t * pMemStates
Definition: saigSimMv.c:70
Vec_PtrFreeP
static void Vec_PtrFreeP(Vec_Ptr_t **p)
Definition: vecPtr.h:240
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
SAIG_DIFF_VALUES
#define SAIG_DIFF_VALUES
DECLARATIONS ///.
Definition: saigSimMv.c:30
Saig_MvManPostProcess
void Saig_MvManPostProcess(Saig_MvMan_t *p, int iState)
Definition: saigSimMv.c:571
Saig_MvAnd_t_::iFan1
int iFan1
Definition: saigSimMv.c:48
AIG_OBJ_CI
Definition: aig.h:60
assert
#define assert(ex)
Definition: util_old.h:213
Saig_MvConst
static int Saig_MvConst(int c)
Definition: saigSimMv.c:94
Saig_MvMan_t_::vXFlops
Vec_Int_t * vXFlops
Definition: saigSimMv.c:66
Saig_MvManForEachObj
#define Saig_MvManForEachObj(pAig, pEntry)
Definition: saigSimMv.c:112
Saig_MvAnd_t_
Definition: saigSimMv.c:45
Saig_MvIsConst0
static int Saig_MvIsConst0(int iNode)
Definition: saigSimMv.c:97
Saig_MvSaveState
int Saig_MvSaveState(Saig_MvMan_t *p)
Definition: saigSimMv.c:543
Saig_MvObj_t_::iFan1
int iFan1
Definition: saigSimMv.c:38
Saig_MvSimulateValue1
static int Saig_MvSimulateValue1(Saig_MvObj_t *pAig, Saig_MvObj_t *pObj)
Definition: saigSimMv.c:388
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Saig_MvMan_t_
Definition: saigSimMv.c:54
Saig_MvMan_t_::pAigNew
Saig_MvAnd_t * pAigNew
Definition: saigSimMv.c:78
Saig_MvMan_t_::vFlops
Vec_Ptr_t * vFlops
Definition: saigSimMv.c:65
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Saig_MvManDeriveMap
Vec_Ptr_t * Saig_MvManDeriveMap(Saig_MvMan_t *p, int fVerbose)
Definition: saigSimMv.c:821
Saig_MvNot
static int Saig_MvNot(int iNode)
Definition: saigSimMv.c:103
nTotal
int nTotal
DECLARATIONS ///.
Definition: cutTruth.c:37
Saig_MvIsComplement
static int Saig_MvIsComplement(int iNode)
Definition: saigSimMv.c:105
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Saig_MvMan_t_::nObjsAlloc
int nObjsAlloc
Definition: saigSimMv.c:79