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
Saig_SynchNot(unsigned w)36 static inline unsigned Saig_SynchNot( unsigned w )
37 {
38 return w^((~(w&(w>>1)))&0x55555555);
39 }
Saig_SynchAnd(unsigned u,unsigned w)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 }
Saig_SynchRandomBinary()44 static inline unsigned Saig_SynchRandomBinary()
45 {
46 return Aig_ManRandom(0) & 0x55555555;
47 }
Saig_SynchRandomTernary()48 static inline unsigned Saig_SynchRandomTernary()
49 {
50 unsigned w = Aig_ManRandom(0);
51 return w^((~w)&(w>>1)&0x55555555);
52 }
Saig_SynchTernary(int v)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 ***********************************************************************/
Saig_SynchSetConstant1(Aig_Man_t * pAig,Vec_Ptr_t * vSimInfo,int nWords)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 ***********************************************************************/
Saig_SynchInitRegsTernary(Aig_Man_t * pAig,Vec_Ptr_t * vSimInfo,int nWords)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 ***********************************************************************/
Saig_SynchInitRegsBinary(Aig_Man_t * pAig,Vec_Ptr_t * vSimInfo,int nWords)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 ***********************************************************************/
Saig_SynchInitPisRandom(Aig_Man_t * pAig,Vec_Ptr_t * vSimInfo,int nWords)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 ***********************************************************************/
Saig_SynchInitPisGiven(Aig_Man_t * pAig,Vec_Ptr_t * vSimInfo,int nWords,char * pValues)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 ***********************************************************************/
Saig_SynchTernarySimulate(Aig_Man_t * pAig,Vec_Ptr_t * vSimInfo,int nWords)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 ***********************************************************************/
Saig_SynchTernaryTransferState(Aig_Man_t * pAig,Vec_Ptr_t * vSimInfo,int nWords)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 ***********************************************************************/
Saig_SynchCountX(Aig_Man_t * pAig,Vec_Ptr_t * vSimInfo,int nWords,int * piPat)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 ***********************************************************************/
Saig_SynchSavePattern(Aig_Man_t * pAig,Vec_Ptr_t * vSimInfo,int nWords,int iPat,Vec_Str_t * vSequence)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 ***********************************************************************/
Saig_SynchSequenceRun(Aig_Man_t * pAig,Vec_Ptr_t * vSimInfo,Vec_Str_t * vSequence,int fTernary)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 ***********************************************************************/
Saig_SynchSequence(Aig_Man_t * pAig,int nWords)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 ***********************************************************************/
Saig_ManDupInitZero(Aig_Man_t * p)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 ***********************************************************************/
Saig_SynchSequenceApply(Aig_Man_t * pAig,int nWords,int fVerbose)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 ***********************************************************************/
Saig_Synchronize(Aig_Man_t * pAig1,Aig_Man_t * pAig2,int nWords,int fVerbose)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
666