abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigSynch.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [saigSynch.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Sequential AIG package.]
8 
9  Synopsis [Computation of synchronizing sequence.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: saigSynch.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 // 0 1 x
31 // 00 01 11
32 // 0 00 00 00 00
33 // 1 01 00 01 11
34 // x 11 00 11 11
35 
36 static inline unsigned Saig_SynchNot( unsigned w )
37 {
38  return w^((~(w&(w>>1)))&0x55555555);
39 }
40 static inline unsigned Saig_SynchAnd( unsigned u, unsigned w )
41 {
42  return (u&w)|((((u&(u>>1)&w&~(w>>1))|(w&(w>>1)&u&~(u>>1)))&0x55555555)<<1);
43 }
44 static inline unsigned Saig_SynchRandomBinary()
45 {
46  return Aig_ManRandom(0) & 0x55555555;
47 }
48 static inline unsigned Saig_SynchRandomTernary()
49 {
50  unsigned w = Aig_ManRandom(0);
51  return w^((~w)&(w>>1)&0x55555555);
52 }
53 static inline unsigned Saig_SynchTernary( int v )
54 {
55  assert( v == 0 || v == 1 || v == 3 );
56  return v? ((v==1)? 0x55555555 : 0xffffffff) : 0;
57 }
58 
59 
60 ////////////////////////////////////////////////////////////////////////
61 /// FUNCTION DEFINITIONS ///
62 ////////////////////////////////////////////////////////////////////////
63 
64 /**Function*************************************************************
65 
66  Synopsis [Initializes registers to the ternary state.]
67 
68  Description []
69 
70  SideEffects []
71 
72  SeeAlso []
73 
74 ***********************************************************************/
75 void Saig_SynchSetConstant1( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
76 {
77  Aig_Obj_t * pObj;
78  unsigned * pSim;
79  int w;
80  pObj = Aig_ManConst1( pAig );
81  pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
82  for ( w = 0; w < nWords; w++ )
83  pSim[w] = 0x55555555;
84 }
85 
86 /**Function*************************************************************
87 
88  Synopsis [Initializes registers to the ternary state.]
89 
90  Description []
91 
92  SideEffects []
93 
94  SeeAlso []
95 
96 ***********************************************************************/
97 void Saig_SynchInitRegsTernary( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
98 {
99  Aig_Obj_t * pObj;
100  unsigned * pSim;
101  int i, w;
102  Saig_ManForEachLo( pAig, pObj, i )
103  {
104  pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
105  for ( w = 0; w < nWords; w++ )
106  pSim[w] = 0xffffffff;
107  }
108 }
109 
110 /**Function*************************************************************
111 
112  Synopsis [Initializes registers to the given binary state.]
113 
114  Description [The binary state is stored in pObj->fMarkA.]
115 
116  SideEffects []
117 
118  SeeAlso []
119 
120 ***********************************************************************/
121 void Saig_SynchInitRegsBinary( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
122 {
123  Aig_Obj_t * pObj;
124  unsigned * pSim;
125  int i, w;
126  Saig_ManForEachLo( pAig, pObj, i )
127  {
128  pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
129  for ( w = 0; w < nWords; w++ )
130  pSim[w] = Saig_SynchTernary( pObj->fMarkA );
131  }
132 }
133 
134 /**Function*************************************************************
135 
136  Synopsis [Initializes random binary primary inputs.]
137 
138  Description []
139 
140  SideEffects []
141 
142  SeeAlso []
143 
144 ***********************************************************************/
145 void Saig_SynchInitPisRandom( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
146 {
147  Aig_Obj_t * pObj;
148  unsigned * pSim;
149  int i, w;
150  Saig_ManForEachPi( pAig, pObj, i )
151  {
152  pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
153  for ( w = 0; w < nWords; w++ )
154  pSim[w] = Saig_SynchRandomBinary();
155  }
156 }
157 
158 /**Function*************************************************************
159 
160  Synopsis [Initializes random binary primary inputs.]
161 
162  Description []
163 
164  SideEffects []
165 
166  SeeAlso []
167 
168 ***********************************************************************/
169 void Saig_SynchInitPisGiven( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, char * pValues )
170 {
171  Aig_Obj_t * pObj;
172  unsigned * pSim;
173  int i, w;
174  Saig_ManForEachPi( pAig, pObj, i )
175  {
176  pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
177  for ( w = 0; w < nWords; w++ )
178  pSim[w] = Saig_SynchTernary( pValues[i] );
179  }
180 }
181 
182 /**Function*************************************************************
183 
184  Synopsis [Performs ternary simulation of the nodes.]
185 
186  Description []
187 
188  SideEffects []
189 
190  SeeAlso []
191 
192 ***********************************************************************/
193 void Saig_SynchTernarySimulate( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
194 {
195  Aig_Obj_t * pObj;
196  unsigned * pSim0, * pSim1, * pSim;
197  int i, w;
198  // simulate nodes
199  Aig_ManForEachNode( pAig, pObj, i )
200  {
201  pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
202  pSim0 = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjFaninId0(pObj) );
203  pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjFaninId1(pObj) );
204  if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
205  {
206  for ( w = 0; w < nWords; w++ )
207  pSim[w] = Saig_SynchAnd( Saig_SynchNot(pSim0[w]), Saig_SynchNot(pSim1[w]) );
208  }
209  else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
210  {
211  for ( w = 0; w < nWords; w++ )
212  pSim[w] = Saig_SynchAnd( pSim0[w], Saig_SynchNot(pSim1[w]) );
213  }
214  else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
215  {
216  for ( w = 0; w < nWords; w++ )
217  pSim[w] = Saig_SynchAnd( Saig_SynchNot(pSim0[w]), pSim1[w] );
218  }
219  else // if ( !Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
220  {
221  for ( w = 0; w < nWords; w++ )
222  pSim[w] = Saig_SynchAnd( pSim0[w], pSim1[w] );
223  }
224  }
225  // transfer values to register inputs
226  Saig_ManForEachLi( pAig, pObj, i )
227  {
228  pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
229  pSim0 = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjFaninId0(pObj) );
230  if ( Aig_ObjFaninC0(pObj) )
231  {
232  for ( w = 0; w < nWords; w++ )
233  pSim[w] = Saig_SynchNot( pSim0[w] );
234  }
235  else
236  {
237  for ( w = 0; w < nWords; w++ )
238  pSim[w] = pSim0[w];
239  }
240  }
241 }
242 
243 /**Function*************************************************************
244 
245  Synopsis [Performs ternary simulation of the nodes.]
246 
247  Description []
248 
249  SideEffects []
250 
251  SeeAlso []
252 
253 ***********************************************************************/
254 void Saig_SynchTernaryTransferState( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords )
255 {
256  Aig_Obj_t * pObjLi, * pObjLo;
257  unsigned * pSim0, * pSim1;
258  int i, w;
259  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
260  {
261  pSim0 = (unsigned *)Vec_PtrEntry( vSimInfo, pObjLi->Id );
262  pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, pObjLo->Id );
263  for ( w = 0; w < nWords; w++ )
264  pSim1[w] = pSim0[w];
265  }
266 }
267 
268 /**Function*************************************************************
269 
270  Synopsis [Returns the number of Xs in the smallest ternary pattern.]
271 
272  Description [Returns the number of this pattern.]
273 
274  SideEffects []
275 
276  SeeAlso []
277 
278 ***********************************************************************/
279 int Saig_SynchCountX( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, int * piPat )
280 {
281  Aig_Obj_t * pObj;
282  unsigned * pSim;
283  int * pCounters, i, w, b;
284  int iPatBest, iTernMin;
285  // count the number of ternary values in each pattern
286  pCounters = ABC_CALLOC( int, nWords * 16 );
287  Saig_ManForEachLi( pAig, pObj, i )
288  {
289  pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
290  for ( w = 0; w < nWords; w++ )
291  for ( b = 0; b < 16; b++ )
292  if ( ((pSim[w] >> (b << 1)) & 3) == 3 )
293  pCounters[16 * w + b]++;
294  }
295  // get the best pattern
296  iPatBest = -1;
297  iTernMin = 1 + Saig_ManRegNum(pAig);
298  for ( b = 0; b < 16 * nWords; b++ )
299  if ( iTernMin > pCounters[b] )
300  {
301  iTernMin = pCounters[b];
302  iPatBest = b;
303  if ( iTernMin == 0 )
304  break;
305  }
306  ABC_FREE( pCounters );
307  *piPat = iPatBest;
308  return iTernMin;
309 }
310 
311 /**Function*************************************************************
312 
313  Synopsis [Saves the best pattern found and initializes the registers.]
314 
315  Description []
316 
317  SideEffects []
318 
319  SeeAlso []
320 
321 ***********************************************************************/
322 int Saig_SynchSavePattern( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, int iPat, Vec_Str_t * vSequence )
323 {
324  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
325  unsigned * pSim;
326  int Counter, Value, i, w;
327  assert( iPat < 16 * nWords );
328  Saig_ManForEachPi( pAig, pObj, i )
329  {
330  pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
331  Value = (pSim[iPat>>4] >> ((iPat&0xf) << 1)) & 3;
332  Vec_StrPush( vSequence, (char)Value );
333 // printf( "%d ", Value );
334  }
335 // printf( "\n" );
336  Counter = 0;
337  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
338  {
339  pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObjLi->Id );
340  Value = (pSim[iPat>>4] >> ((iPat&0xf) << 1)) & 3;
341  Counter += (Value == 3);
342  // save patern in the same register
343  pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObjLo->Id );
344  for ( w = 0; w < nWords; w++ )
345  pSim[w] = Saig_SynchTernary( Value );
346  }
347  return Counter;
348 }
349 
350 /**Function*************************************************************
351 
352  Synopsis [Implement synchronizing sequence.]
353 
354  Description []
355 
356  SideEffects []
357 
358  SeeAlso []
359 
360 ***********************************************************************/
361 int Saig_SynchSequenceRun( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, Vec_Str_t * vSequence, int fTernary )
362 {
363  unsigned * pSim;
364  Aig_Obj_t * pObj;
365  int Counter, nIters, Value, i;
366  assert( Vec_StrSize(vSequence) % Saig_ManPiNum(pAig) == 0 );
367  nIters = Vec_StrSize(vSequence) / Saig_ManPiNum(pAig);
368  Saig_SynchSetConstant1( pAig, vSimInfo, 1 );
369  if ( fTernary )
370  Saig_SynchInitRegsTernary( pAig, vSimInfo, 1 );
371  else
372  Saig_SynchInitRegsBinary( pAig, vSimInfo, 1 );
373  for ( i = 0; i < nIters; i++ )
374  {
375  Saig_SynchInitPisGiven( pAig, vSimInfo, 1, Vec_StrArray(vSequence) + i * Saig_ManPiNum(pAig) );
376  Saig_SynchTernarySimulate( pAig, vSimInfo, 1 );
377  Saig_SynchTernaryTransferState( pAig, vSimInfo, 1 );
378  }
379  // save the resulting state in the registers
380  Counter = 0;
381  Saig_ManForEachLo( pAig, pObj, i )
382  {
383  pSim = (unsigned *)Vec_PtrEntry( vSimInfo, pObj->Id );
384  Value = pSim[0] & 3;
385  assert( Value != 2 );
386  Counter += (Value == 3);
387  pObj->fMarkA = Value;
388  }
389  return Counter;
390 }
391 
392 /**Function*************************************************************
393 
394  Synopsis [Determines synchronizing sequence using ternary simulation.]
395 
396  Description []
397 
398  SideEffects []
399 
400  SeeAlso []
401 
402 ***********************************************************************/
403 Vec_Str_t * Saig_SynchSequence( Aig_Man_t * pAig, int nWords )
404 {
405  int nStepsMax = 100; // the maximum number of simulation steps
406  int nTriesMax = 100; // the maximum number of attempts at each step
407  int fVerify = 1; // verify the resulting pattern
408  Vec_Str_t * vSequence;
409  Vec_Ptr_t * vSimInfo;
410  int nTerPrev, nTerCur = 0, nTerCur2;
411  int iPatBest, RetValue, s, t;
412  assert( Saig_ManRegNum(pAig) > 0 );
413  // reset random numbers
414  Aig_ManRandom( 1 );
415  // start the sequence
416  vSequence = Vec_StrAlloc( 20 * Saig_ManRegNum(pAig) );
417  // create sim info and init registers
418  vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords );
419  Saig_SynchSetConstant1( pAig, vSimInfo, nWords );
420  // iterate over the timeframes
421  nTerPrev = Saig_ManRegNum(pAig);
422  Saig_SynchInitRegsTernary( pAig, vSimInfo, nWords );
423  for ( s = 0; s < nStepsMax && nTerPrev > 0; s++ )
424  {
425  for ( t = 0; t < nTriesMax; t++ )
426  {
427  Saig_SynchInitPisRandom( pAig, vSimInfo, nWords );
428  Saig_SynchTernarySimulate( pAig, vSimInfo, nWords );
429  nTerCur = Saig_SynchCountX( pAig, vSimInfo, nWords, &iPatBest );
430  if ( nTerCur < nTerPrev )
431  break;
432  }
433  if ( t == nTriesMax )
434  break;
435  nTerCur2 = Saig_SynchSavePattern( pAig, vSimInfo, nWords, iPatBest, vSequence );
436  assert( nTerCur == nTerCur2 );
437  nTerPrev = nTerCur;
438  }
439  if ( nTerPrev > 0 )
440  {
441  printf( "Count not initialize %d registers.\n", nTerPrev );
442  Vec_PtrFree( vSimInfo );
443  Vec_StrFree( vSequence );
444  return NULL;
445  }
446  // verify that the sequence is correct
447  if ( fVerify )
448  {
449  RetValue = Saig_SynchSequenceRun( pAig, vSimInfo, vSequence, 1 );
450  assert( RetValue == 0 );
451  Aig_ManCleanMarkA( pAig );
452  }
453  Vec_PtrFree( vSimInfo );
454  return vSequence;
455 }
456 
457 /**Function*************************************************************
458 
459  Synopsis [Duplicates the AIG to have constant-0 initial state.]
460 
461  Description []
462 
463  SideEffects []
464 
465  SeeAlso []
466 
467 ***********************************************************************/
468 Aig_Man_t * Saig_ManDupInitZero( Aig_Man_t * p )
469 {
470  Aig_Man_t * pNew;
471  Aig_Obj_t * pObj;
472  int i;
473  pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
474  pNew->pName = Abc_UtilStrsav( p->pName );
475  Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
476  Saig_ManForEachPi( p, pObj, i )
477  pObj->pData = Aig_ObjCreateCi( pNew );
478  Saig_ManForEachLo( p, pObj, i )
479  pObj->pData = Aig_NotCond( Aig_ObjCreateCi( pNew ), pObj->fMarkA );
480  Aig_ManForEachNode( p, pObj, i )
481  pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
482  Saig_ManForEachPo( p, pObj, i )
483  pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
484  Saig_ManForEachLi( p, pObj, i )
485  pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), pObj->fMarkA ) );
486  Aig_ManSetRegNum( pNew, Saig_ManRegNum(p) );
487  assert( Aig_ManNodeNum(pNew) == Aig_ManNodeNum(p) );
488  return pNew;
489 }
490 
491 /**Function*************************************************************
492 
493  Synopsis [Determines synchronizing sequence using ternary simulation.]
494 
495  Description []
496 
497  SideEffects []
498 
499  SeeAlso []
500 
501 ***********************************************************************/
502 Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose )
503 {
504  Aig_Man_t * pAigZero;
505  Vec_Str_t * vSequence;
506  Vec_Ptr_t * vSimInfo;
507  int RetValue;
508  abctime clk;
509 
510 clk = Abc_Clock();
511  // derive synchronization sequence
512  vSequence = Saig_SynchSequence( pAig, nWords );
513  if ( vSequence == NULL )
514  printf( "Design 1: Synchronizing sequence is not found. " );
515  else if ( fVerbose )
516  printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSequence) / Saig_ManPiNum(pAig) );
517  if ( fVerbose )
518  {
519  ABC_PRT( "Time", Abc_Clock() - clk );
520  }
521  else
522  printf( "\n" );
523  if ( vSequence == NULL )
524  {
525  printf( "Quitting synchronization.\n" );
526  return NULL;
527  }
528 
529  // apply synchronization sequence
530  vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), 1 );
531  RetValue = Saig_SynchSequenceRun( pAig, vSimInfo, vSequence, 1 );
532  assert( RetValue == 0 );
533  // duplicate
534  pAigZero = Saig_ManDupInitZero( pAig );
535  // cleanup
536  Vec_PtrFree( vSimInfo );
537  Vec_StrFree( vSequence );
538  Aig_ManCleanMarkA( pAig );
539  return pAigZero;
540 }
541 
542 /**Function*************************************************************
543 
544  Synopsis [Creates SEC miter for two designs without initial state.]
545 
546  Description [The designs (pAig1 and pAig2) are assumed to have ternary
547  initial state. Determines synchronizing sequences using ternary simulation.
548  Simulates the sequences on both designs to come up with equivalent binary
549  initial states. Create seq miter for the designs starting in these states.]
550 
551  SideEffects []
552 
553  SeeAlso []
554 
555 ***********************************************************************/
556 Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, int fVerbose )
557 {
558  Aig_Man_t * pAig1z, * pAig2z, * pMiter;
559  Vec_Str_t * vSeq1, * vSeq2;
560  Vec_Ptr_t * vSimInfo;
561  int RetValue;
562  abctime clk;
563 /*
564  {
565  unsigned u = Saig_SynchRandomTernary();
566  unsigned w = Saig_SynchRandomTernary();
567  unsigned x = Saig_SynchNot( u );
568  unsigned y = Saig_SynchNot( w );
569  unsigned z = Saig_SynchAnd( x, y );
570 
571  Extra_PrintBinary( stdout, &u, 32 ); printf( "\n" );
572  Extra_PrintBinary( stdout, &w, 32 ); printf( "\n" ); printf( "\n" );
573  Extra_PrintBinary( stdout, &x, 32 ); printf( "\n" );
574  Extra_PrintBinary( stdout, &y, 32 ); printf( "\n" ); printf( "\n" );
575  Extra_PrintBinary( stdout, &z, 32 ); printf( "\n" );
576  }
577 */
578  // report statistics
579  if ( fVerbose )
580  {
581  printf( "Design 1: " );
582  Aig_ManPrintStats( pAig1 );
583  printf( "Design 2: " );
584  Aig_ManPrintStats( pAig2 );
585  }
586 
587  // synchronize the first design
588  clk = Abc_Clock();
589  vSeq1 = Saig_SynchSequence( pAig1, nWords );
590  if ( vSeq1 == NULL )
591  printf( "Design 1: Synchronizing sequence is not found. " );
592  else if ( fVerbose )
593  printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSeq1) / Saig_ManPiNum(pAig1) );
594  if ( fVerbose )
595  {
596  ABC_PRT( "Time", Abc_Clock() - clk );
597  }
598  else
599  printf( "\n" );
600 
601  // synchronize the first design
602  clk = Abc_Clock();
603  vSeq2 = Saig_SynchSequence( pAig2, nWords );
604  if ( vSeq2 == NULL )
605  printf( "Design 2: Synchronizing sequence is not found. " );
606  else if ( fVerbose )
607  printf( "Design 2: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSeq2) / Saig_ManPiNum(pAig2) );
608  if ( fVerbose )
609  {
610  ABC_PRT( "Time", Abc_Clock() - clk );
611  }
612  else
613  printf( "\n" );
614 
615  // quit if one of the designs cannot be synchronized
616  if ( vSeq1 == NULL || vSeq2 == NULL )
617  {
618  printf( "Quitting synchronization.\n" );
619  if ( vSeq1 ) Vec_StrFree( vSeq1 );
620  if ( vSeq2 ) Vec_StrFree( vSeq2 );
621  return NULL;
622  }
623  clk = Abc_Clock();
624  vSimInfo = Vec_PtrAllocSimInfo( Abc_MaxInt( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 );
625 
626  // process Design 1
627  RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq1, 1 );
628  assert( RetValue == 0 );
629  RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq2, 0 );
630  assert( RetValue == 0 );
631 
632  // process Design 2
633  RetValue = Saig_SynchSequenceRun( pAig2, vSimInfo, vSeq2, 1 );
634  assert( RetValue == 0 );
635 
636  // duplicate designs
637  pAig1z = Saig_ManDupInitZero( pAig1 );
638  pAig2z = Saig_ManDupInitZero( pAig2 );
639  pMiter = Saig_ManCreateMiter( pAig1z, pAig2z, 0 );
640  Aig_ManCleanup( pMiter );
641  Aig_ManStop( pAig1z );
642  Aig_ManStop( pAig2z );
643 
644  // cleanup
645  Vec_PtrFree( vSimInfo );
646  Vec_StrFree( vSeq1 );
647  Vec_StrFree( vSeq2 );
648  Aig_ManCleanMarkA( pAig1 );
649  Aig_ManCleanMarkA( pAig2 );
650 
651  if ( fVerbose )
652  {
653  printf( "Miter of the synchronized designs is constructed. " );
654  ABC_PRT( "Time", Abc_Clock() - clk );
655  }
656  return pMiter;
657 }
658 
659 ////////////////////////////////////////////////////////////////////////
660 /// END OF FILE ///
661 ////////////////////////////////////////////////////////////////////////
662 
663 
664 ABC_NAMESPACE_IMPL_END
665 
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Saig_SynchTernarySimulate
void Saig_SynchTernarySimulate(Aig_Man_t *pAig, Vec_Ptr_t *vSimInfo, int nWords)
Definition: saigSynch.c:193
Aig_ObjFaninId0
static int Aig_ObjFaninId0(Aig_Obj_t *pObj)
Definition: aig.h:304
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
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Vec_StrArray
static char * Vec_StrArray(Vec_Str_t *p)
Definition: vecStr.h:272
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Saig_SynchSetConstant1
void Saig_SynchSetConstant1(Aig_Man_t *pAig, Vec_Ptr_t *vSimInfo, int nWords)
FUNCTION DEFINITIONS ///.
Definition: saigSynch.c:75
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Saig_SynchInitRegsBinary
void Saig_SynchInitRegsBinary(Aig_Man_t *pAig, Vec_Ptr_t *vSimInfo, int nWords)
Definition: saigSynch.c:121
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
Saig_SynchInitPisRandom
void Saig_SynchInitPisRandom(Aig_Man_t *pAig, Vec_Ptr_t *vSimInfo, int nWords)
Definition: saigSynch.c:145
Saig_SynchSequence
Vec_Str_t * Saig_SynchSequence(Aig_Man_t *pAig, int nWords)
Definition: saigSynch.c:403
Saig_SynchTernary
static unsigned Saig_SynchTernary(int v)
Definition: saigSynch.c:53
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition: aig.h:79
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Vec_StrAlloc
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
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_StrPush
static void Vec_StrPush(Vec_Str_t *p, char Entry)
Definition: vecStr.h:535
nWords
int nWords
Definition: abcNpn.c:127
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Saig_ManDupInitZero
Aig_Man_t * Saig_ManDupInitZero(Aig_Man_t *p)
Definition: saigSynch.c:468
Saig_SynchTernaryTransferState
void Saig_SynchTernaryTransferState(Aig_Man_t *pAig, Vec_Ptr_t *vSimInfo, int nWords)
Definition: saigSynch.c:254
Saig_SynchInitPisGiven
void Saig_SynchInitPisGiven(Aig_Man_t *pAig, Vec_Ptr_t *vSimInfo, int nWords, char *pValues)
Definition: saigSynch.c:169
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Saig_Synchronize
Aig_Man_t * Saig_Synchronize(Aig_Man_t *pAig1, Aig_Man_t *pAig2, int nWords, int fVerbose)
Definition: saigSynch.c:556
Saig_ManCreateMiter
Aig_Man_t * Saig_ManCreateMiter(Aig_Man_t *p1, Aig_Man_t *p2, int Oper)
Definition: saigMiter.c:100
Saig_SynchRandomBinary
static unsigned Saig_SynchRandomBinary()
Definition: saigSynch.c:44
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Vec_StrFree
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_ObjChild1Copy
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Aig_Obj_t_
Definition: aig.h:69
Saig_SynchCountX
int Saig_SynchCountX(Aig_Man_t *pAig, Vec_Ptr_t *vSimInfo, int nWords, int *piPat)
Definition: saigSynch.c:279
Counter
static int Counter
Definition: extraBddMisc.c:1877
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Aig_ObjChild0Copy
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
Saig_SynchSequenceRun
int Saig_SynchSequenceRun(Aig_Man_t *pAig, Vec_Ptr_t *vSimInfo, Vec_Str_t *vSequence, int fTernary)
Definition: saigSynch.c:361
Saig_SynchSequenceApply
Aig_Man_t * Saig_SynchSequenceApply(Aig_Man_t *pAig, int nWords, int fVerbose)
Definition: saigSynch.c:502
Saig_SynchInitRegsTernary
void Saig_SynchInitRegsTernary(Aig_Man_t *pAig, Vec_Ptr_t *vSimInfo, int nWords)
Definition: saigSynch.c:97
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
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
Saig_SynchRandomTernary
static unsigned Saig_SynchRandomTernary()
Definition: saigSynch.c:48
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Vec_StrSize
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Vec_Str_t_
Definition: bblif.c:47
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition: aigUtil.c:148
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
assert
#define assert(ex)
Definition: util_old.h:213
Saig_SynchNot
static ABC_NAMESPACE_IMPL_START unsigned Saig_SynchNot(unsigned w)
DECLARATIONS ///.
Definition: saigSynch.c:36
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Saig_SynchAnd
static unsigned Saig_SynchAnd(unsigned u, unsigned w)
Definition: saigSynch.c:40
Vec_PtrAllocSimInfo
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
Saig_SynchSavePattern
int Saig_SynchSavePattern(Aig_Man_t *pAig, Vec_Ptr_t *vSimInfo, int nWords, int iPat, Vec_Str_t *vSequence)
Definition: saigSynch.c:322