1 /**CFile****************************************************************
2
3 FileName [giaSim.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Fast sequential 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: giaSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22 #include "misc/util/utilTruth.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
Gia_SimData(Gia_ManSim_t * p,int i)31 static inline unsigned * Gia_SimData( Gia_ManSim_t * p, int i ) { return p->pDataSim + i * p->nWords; }
Gia_SimDataCi(Gia_ManSim_t * p,int i)32 static inline unsigned * Gia_SimDataCi( Gia_ManSim_t * p, int i ) { return p->pDataSimCis + i * p->nWords; }
Gia_SimDataCo(Gia_ManSim_t * p,int i)33 static inline unsigned * Gia_SimDataCo( Gia_ManSim_t * p, int i ) { return p->pDataSimCos + i * p->nWords; }
34
Gia_SimDataExt(Gia_ManSim_t * p,int i)35 unsigned * Gia_SimDataExt( Gia_ManSim_t * p, int i ) { return Gia_SimData(p, i); }
Gia_SimDataCiExt(Gia_ManSim_t * p,int i)36 unsigned * Gia_SimDataCiExt( Gia_ManSim_t * p, int i ) { return Gia_SimDataCi(p, i); }
Gia_SimDataCoExt(Gia_ManSim_t * p,int i)37 unsigned * Gia_SimDataCoExt( Gia_ManSim_t * p, int i ) { return Gia_SimDataCo(p, i); }
38
39 ////////////////////////////////////////////////////////////////////////
40 /// FUNCTION DEFINITIONS ///
41 ////////////////////////////////////////////////////////////////////////
42
43
44 /**Function*************************************************************
45
46 Synopsis []
47
48 Description []
49
50 SideEffects []
51
52 SeeAlso []
53
54 ***********************************************************************/
Gia_ManSimCollect_rec(Gia_Man_t * pGia,Gia_Obj_t * pObj,Vec_Int_t * vVec)55 void Gia_ManSimCollect_rec( Gia_Man_t * pGia, Gia_Obj_t * pObj, Vec_Int_t * vVec )
56 {
57 Vec_IntPush( vVec, Gia_ObjToLit(pGia, pObj) );
58 if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) )
59 return;
60 assert( Gia_ObjIsAnd(pObj) );
61 Gia_ManSimCollect_rec( pGia, Gia_ObjChild0(pObj), vVec );
62 Gia_ManSimCollect_rec( pGia, Gia_ObjChild1(pObj), vVec );
63 }
64
65 /**Function*************************************************************
66
67 Synopsis [Derives signal implications.]
68
69 Description []
70
71 SideEffects []
72
73 SeeAlso []
74
75 ***********************************************************************/
Gia_ManSimCollect(Gia_Man_t * pGia,Gia_Obj_t * pObj,Vec_Int_t * vVec)76 void Gia_ManSimCollect( Gia_Man_t * pGia, Gia_Obj_t * pObj, Vec_Int_t * vVec )
77 {
78 Vec_IntClear( vVec );
79 Gia_ManSimCollect_rec( pGia, pObj, vVec );
80 Vec_IntUniqify( vVec );
81 }
82
83 /**Function*************************************************************
84
85 Synopsis [Finds signals, which reset flops to have constant values.]
86
87 Description []
88
89 SideEffects []
90
91 SeeAlso []
92
93 ***********************************************************************/
Gia_ManSimDeriveResets(Gia_Man_t * pGia)94 Vec_Int_t * Gia_ManSimDeriveResets( Gia_Man_t * pGia )
95 {
96 int nImpLimit = 5;
97 Vec_Int_t * vResult;
98 Vec_Int_t * vCountLits, * vSuperGate;
99 Gia_Obj_t * pObj;
100 int i, k, Lit, Count;
101 int Counter0 = 0, Counter1 = 0;
102 int CounterPi0 = 0, CounterPi1 = 0;
103 abctime clk = Abc_Clock();
104
105 // create reset counters for each literal
106 vCountLits = Vec_IntStart( 2 * Gia_ManObjNum(pGia) );
107
108 // collect implications for each flop input driver
109 vSuperGate = Vec_IntAlloc( 1000 );
110 Gia_ManForEachRi( pGia, pObj, i )
111 {
112 if ( Gia_ObjFaninId0p(pGia, pObj) == 0 )
113 continue;
114 Vec_IntAddToEntry( vCountLits, Gia_ObjToLit(pGia, Gia_ObjChild0(pObj)), 1 );
115 Gia_ManSimCollect( pGia, Gia_ObjFanin0(pObj), vSuperGate );
116 Vec_IntForEachEntry( vSuperGate, Lit, k )
117 Vec_IntAddToEntry( vCountLits, Lit, 1 );
118 }
119 Vec_IntFree( vSuperGate );
120
121 // label signals whose counter if more than the limit
122 vResult = Vec_IntStartFull( Gia_ManObjNum(pGia) );
123 Vec_IntForEachEntry( vCountLits, Count, Lit )
124 {
125 if ( Count < nImpLimit )
126 continue;
127 pObj = Gia_ManObj( pGia, Abc_Lit2Var(Lit) );
128 if ( Abc_LitIsCompl(Lit) ) // const 0
129 {
130 // Ssm_ObjSetLogic0( pObj );
131 Vec_IntWriteEntry( vResult, Abc_Lit2Var(Lit), 0 );
132 CounterPi0 += Gia_ObjIsPi(pGia, pObj);
133 Counter0++;
134 }
135 else
136 {
137 // Ssm_ObjSetLogic1( pObj );
138 Vec_IntWriteEntry( vResult, Abc_Lit2Var(Lit), 1 );
139 CounterPi1 += Gia_ObjIsPi(pGia, pObj);
140 Counter1++;
141 }
142 // if ( Gia_ObjIsPi(pGia, pObj) )
143 // printf( "%d ", Count );
144 }
145 // printf( "\n" );
146 Vec_IntFree( vCountLits );
147
148 printf( "Logic0 = %d (%d). Logic1 = %d (%d). ", Counter0, CounterPi0, Counter1, CounterPi1 );
149 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
150 return vResult;
151 }
152
153
154 /**Function*************************************************************
155
156 Synopsis [This procedure sets default parameters.]
157
158 Description []
159
160 SideEffects []
161
162 SeeAlso []
163
164 ***********************************************************************/
Gia_ManSimSetDefaultParams(Gia_ParSim_t * p)165 void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p )
166 {
167 memset( p, 0, sizeof(Gia_ParSim_t) );
168 // user-controlled parameters
169 p->nWords = 8; // the number of machine words
170 p->nIters = 32; // the number of timeframes
171 p->RandSeed = 0; // the seed to generate random numbers
172 p->TimeLimit = 60; // time limit in seconds
173 p->fCheckMiter = 0; // check if miter outputs are non-zero
174 p->fVerbose = 0; // enables verbose output
175 p->iOutFail = -1; // index of the failed output
176 }
177
178 /**Function*************************************************************
179
180 Synopsis []
181
182 Description []
183
184 SideEffects []
185
186 SeeAlso []
187
188 ***********************************************************************/
Gia_ManSimDelete(Gia_ManSim_t * p)189 void Gia_ManSimDelete( Gia_ManSim_t * p )
190 {
191 Vec_IntFreeP( &p->vConsts );
192 Vec_IntFreeP( &p->vCis2Ids );
193 Gia_ManStopP( &p->pAig );
194 ABC_FREE( p->pDataSim );
195 ABC_FREE( p->pDataSimCis );
196 ABC_FREE( p->pDataSimCos );
197 ABC_FREE( p );
198 }
199
200 /**Function*************************************************************
201
202 Synopsis [Creates fast simulation manager.]
203
204 Description []
205
206 SideEffects []
207
208 SeeAlso []
209
210 ***********************************************************************/
Gia_ManSimCreate(Gia_Man_t * pAig,Gia_ParSim_t * pPars)211 Gia_ManSim_t * Gia_ManSimCreate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
212 {
213 Gia_ManSim_t * p;
214 int Entry, i;
215 p = ABC_ALLOC( Gia_ManSim_t, 1 );
216 memset( p, 0, sizeof(Gia_ManSim_t) );
217 // look for reset signals
218 if ( pPars->fVerbose )
219 p->vConsts = Gia_ManSimDeriveResets( pAig );
220 // derive the frontier
221 p->pAig = Gia_ManFront( pAig );
222 p->pPars = pPars;
223 p->nWords = pPars->nWords;
224 p->pDataSim = ABC_ALLOC( unsigned, p->nWords * p->pAig->nFront );
225 p->pDataSimCis = ABC_ALLOC( unsigned, p->nWords * Gia_ManCiNum(p->pAig) );
226 p->pDataSimCos = ABC_ALLOC( unsigned, p->nWords * Gia_ManCoNum(p->pAig) );
227 if ( !p->pDataSim || !p->pDataSimCis || !p->pDataSimCos )
228 {
229 Abc_Print( 1, "Simulator could not allocate %.2f GB for simulation info.\n",
230 4.0 * p->nWords * (p->pAig->nFront + Gia_ManCiNum(p->pAig) + Gia_ManCoNum(p->pAig)) / (1<<30) );
231 Gia_ManSimDelete( p );
232 return NULL;
233 }
234 p->vCis2Ids = Vec_IntAlloc( Gia_ManCiNum(p->pAig) );
235 Vec_IntForEachEntry( pAig->vCis, Entry, i )
236 Vec_IntPush( p->vCis2Ids, i ); // do we need p->vCis2Ids?
237 if ( pPars->fVerbose )
238 Abc_Print( 1, "AIG = %7.2f MB. Front mem = %7.2f MB. Other mem = %7.2f MB.\n",
239 12.0*Gia_ManObjNum(p->pAig)/(1<<20),
240 4.0*p->nWords*p->pAig->nFront/(1<<20),
241 4.0*p->nWords*(Gia_ManCiNum(p->pAig) + Gia_ManCoNum(p->pAig))/(1<<20) );
242
243 return p;
244 }
245
246 /**Function*************************************************************
247
248 Synopsis []
249
250 Description []
251
252 SideEffects []
253
254 SeeAlso []
255
256 ***********************************************************************/
Gia_ManSimInfoRandom(Gia_ManSim_t * p,unsigned * pInfo)257 static inline void Gia_ManSimInfoRandom( Gia_ManSim_t * p, unsigned * pInfo )
258 {
259 int w;
260 for ( w = p->nWords-1; w >= 0; w-- )
261 pInfo[w] = Gia_ManRandom( 0 );
262 }
263
264 /**Function*************************************************************
265
266 Synopsis []
267
268 Description []
269
270 SideEffects []
271
272 SeeAlso []
273
274 ***********************************************************************/
Gia_ManSimInfoZero(Gia_ManSim_t * p,unsigned * pInfo)275 static inline void Gia_ManSimInfoZero( Gia_ManSim_t * p, unsigned * pInfo )
276 {
277 int w;
278 for ( w = p->nWords-1; w >= 0; w-- )
279 pInfo[w] = 0;
280 }
281
282 /**Function*************************************************************
283
284 Synopsis [Returns index of the first pattern that failed.]
285
286 Description []
287
288 SideEffects []
289
290 SeeAlso []
291
292 ***********************************************************************/
Gia_ManSimInfoIsZero(Gia_ManSim_t * p,unsigned * pInfo)293 static inline int Gia_ManSimInfoIsZero( Gia_ManSim_t * p, unsigned * pInfo )
294 {
295 int w;
296 for ( w = 0; w < p->nWords; w++ )
297 if ( pInfo[w] )
298 return 32*w + Gia_WordFindFirstBit( pInfo[w] );
299 return -1;
300 }
301
302 /**Function*************************************************************
303
304 Synopsis []
305
306 Description []
307
308 SideEffects []
309
310 SeeAlso []
311
312 ***********************************************************************/
Gia_ManSimInfoOne(Gia_ManSim_t * p,unsigned * pInfo)313 static inline void Gia_ManSimInfoOne( Gia_ManSim_t * p, unsigned * pInfo )
314 {
315 int w;
316 for ( w = p->nWords-1; w >= 0; w-- )
317 pInfo[w] = ~0;
318 }
319
320 /**Function*************************************************************
321
322 Synopsis []
323
324 Description []
325
326 SideEffects []
327
328 SeeAlso []
329
330 ***********************************************************************/
Gia_ManSimInfoCopy(Gia_ManSim_t * p,unsigned * pInfo,unsigned * pInfo0)331 static inline void Gia_ManSimInfoCopy( Gia_ManSim_t * p, unsigned * pInfo, unsigned * pInfo0 )
332 {
333 int w;
334 for ( w = p->nWords-1; w >= 0; w-- )
335 pInfo[w] = pInfo0[w];
336 }
337
338 /**Function*************************************************************
339
340 Synopsis []
341
342 Description []
343
344 SideEffects []
345
346 SeeAlso []
347
348 ***********************************************************************/
Gia_ManSimulateCi(Gia_ManSim_t * p,Gia_Obj_t * pObj,int iCi)349 static inline void Gia_ManSimulateCi( Gia_ManSim_t * p, Gia_Obj_t * pObj, int iCi )
350 {
351 unsigned * pInfo = Gia_SimData( p, Gia_ObjValue(pObj) );
352 unsigned * pInfo0 = Gia_SimDataCi( p, iCi );
353 int w;
354 for ( w = p->nWords-1; w >= 0; w-- )
355 pInfo[w] = pInfo0[w];
356 }
357
358 /**Function*************************************************************
359
360 Synopsis []
361
362 Description []
363
364 SideEffects []
365
366 SeeAlso []
367
368 ***********************************************************************/
Gia_ManSimulateCo(Gia_ManSim_t * p,int iCo,Gia_Obj_t * pObj)369 static inline void Gia_ManSimulateCo( Gia_ManSim_t * p, int iCo, Gia_Obj_t * pObj )
370 {
371 unsigned * pInfo = Gia_SimDataCo( p, iCo );
372 unsigned * pInfo0 = Gia_SimData( p, Gia_ObjDiff0(pObj) );
373 int w;
374 if ( Gia_ObjFaninC0(pObj) )
375 for ( w = p->nWords-1; w >= 0; w-- )
376 pInfo[w] = ~pInfo0[w];
377 else
378 for ( w = p->nWords-1; w >= 0; w-- )
379 pInfo[w] = pInfo0[w];
380 }
381
382 /**Function*************************************************************
383
384 Synopsis []
385
386 Description []
387
388 SideEffects []
389
390 SeeAlso []
391
392 ***********************************************************************/
Gia_ManSimulateNode(Gia_ManSim_t * p,Gia_Obj_t * pObj)393 static inline void Gia_ManSimulateNode( Gia_ManSim_t * p, Gia_Obj_t * pObj )
394 {
395 unsigned * pInfo = Gia_SimData( p, Gia_ObjValue(pObj) );
396 unsigned * pInfo0 = Gia_SimData( p, Gia_ObjDiff0(pObj) );
397 unsigned * pInfo1 = Gia_SimData( p, Gia_ObjDiff1(pObj) );
398 int w;
399 if ( Gia_ObjFaninC0(pObj) )
400 {
401 if ( Gia_ObjFaninC1(pObj) )
402 for ( w = p->nWords-1; w >= 0; w-- )
403 pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
404 else
405 for ( w = p->nWords-1; w >= 0; w-- )
406 pInfo[w] = ~pInfo0[w] & pInfo1[w];
407 }
408 else
409 {
410 if ( Gia_ObjFaninC1(pObj) )
411 for ( w = p->nWords-1; w >= 0; w-- )
412 pInfo[w] = pInfo0[w] & ~pInfo1[w];
413 else
414 for ( w = p->nWords-1; w >= 0; w-- )
415 pInfo[w] = pInfo0[w] & pInfo1[w];
416 }
417 }
418
419 /**Function*************************************************************
420
421 Synopsis []
422
423 Description []
424
425 SideEffects []
426
427 SeeAlso []
428
429 ***********************************************************************/
Gia_ManSimInfoInit(Gia_ManSim_t * p)430 void Gia_ManSimInfoInit( Gia_ManSim_t * p )
431 {
432 int iPioNum, i;
433 Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
434 {
435 if ( iPioNum < Gia_ManPiNum(p->pAig) )
436 Gia_ManSimInfoRandom( p, Gia_SimDataCi(p, i) );
437 else
438 Gia_ManSimInfoZero( p, Gia_SimDataCi(p, i) );
439 }
440 }
441
442 /**Function*************************************************************
443
444 Synopsis []
445
446 Description []
447
448 SideEffects []
449
450 SeeAlso []
451
452 ***********************************************************************/
Gia_ManSimInfoTransfer(Gia_ManSim_t * p)453 void Gia_ManSimInfoTransfer( Gia_ManSim_t * p )
454 {
455 int iPioNum, i;
456 Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
457 {
458 if ( iPioNum < Gia_ManPiNum(p->pAig) )
459 Gia_ManSimInfoRandom( p, Gia_SimDataCi(p, i) );
460 else
461 Gia_ManSimInfoCopy( p, Gia_SimDataCi(p, i), Gia_SimDataCo(p, Gia_ManPoNum(p->pAig)+iPioNum-Gia_ManPiNum(p->pAig)) );
462 }
463 }
464
465 /**Function*************************************************************
466
467 Synopsis []
468
469 Description []
470
471 SideEffects []
472
473 SeeAlso []
474
475 ***********************************************************************/
Gia_ManSimulateRound(Gia_ManSim_t * p)476 void Gia_ManSimulateRound( Gia_ManSim_t * p )
477 {
478 Gia_Obj_t * pObj;
479 int i, iCis = 0, iCos = 0;
480 assert( p->pAig->nFront > 0 );
481 assert( Gia_ManConst0(p->pAig)->Value == 0 );
482 Gia_ManSimInfoZero( p, Gia_SimData(p, 0) );
483 Gia_ManForEachObj1( p->pAig, pObj, i )
484 {
485 if ( Gia_ObjIsAndOrConst0(pObj) )
486 {
487 assert( Gia_ObjValue(pObj) < p->pAig->nFront );
488 Gia_ManSimulateNode( p, pObj );
489 }
490 else if ( Gia_ObjIsCo(pObj) )
491 {
492 assert( Gia_ObjValue(pObj) == GIA_NONE );
493 Gia_ManSimulateCo( p, iCos++, pObj );
494 }
495 else // if ( Gia_ObjIsCi(pObj) )
496 {
497 assert( Gia_ObjValue(pObj) < p->pAig->nFront );
498 Gia_ManSimulateCi( p, pObj, iCis++ );
499 }
500 }
501 assert( Gia_ManCiNum(p->pAig) == iCis );
502 assert( Gia_ManCoNum(p->pAig) == iCos );
503 }
504
505 /**Function*************************************************************
506
507 Synopsis [Returns index of the PO and pattern that failed it.]
508
509 Description []
510
511 SideEffects []
512
513 SeeAlso []
514
515 ***********************************************************************/
Gia_ManCheckPos(Gia_ManSim_t * p,int * piPo,int * piPat)516 static inline int Gia_ManCheckPos( Gia_ManSim_t * p, int * piPo, int * piPat )
517 {
518 int i, iPat;
519 for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
520 {
521 iPat = Gia_ManSimInfoIsZero( p, Gia_SimDataCo(p, i) );
522 if ( iPat >= 0 )
523 {
524 *piPo = i;
525 *piPat = iPat;
526 return 1;
527 }
528 }
529 return 0;
530 }
531
532 /**Function*************************************************************
533
534 Synopsis [Returns the counter-example.]
535
536 Description []
537
538 SideEffects []
539
540 SeeAlso []
541
542 ***********************************************************************/
Gia_ManGenerateCounter(Gia_Man_t * pAig,int iFrame,int iOut,int nWords,int iPat,Vec_Int_t * vCis2Ids)543 Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids )
544 {
545 Abc_Cex_t * p;
546 unsigned * pData;
547 int f, i, w, iPioId, Counter;
548 p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
549 p->iFrame = iFrame;
550 p->iPo = iOut;
551 // fill in the binary data
552 Counter = p->nRegs;
553 pData = ABC_ALLOC( unsigned, nWords );
554 for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
555 for ( i = 0; i < Gia_ManPiNum(pAig); i++ )
556 {
557 iPioId = Vec_IntEntry( vCis2Ids, i );
558 if ( iPioId >= p->nPis )
559 continue;
560 for ( w = nWords-1; w >= 0; w-- )
561 pData[w] = Gia_ManRandom( 0 );
562 if ( Abc_InfoHasBit( pData, iPat ) )
563 Abc_InfoSetBit( p->pData, Counter + iPioId );
564 }
565 ABC_FREE( pData );
566 return p;
567 }
568
569 /**Function*************************************************************
570
571 Synopsis []
572
573 Description []
574
575 SideEffects []
576
577 SeeAlso []
578
579 ***********************************************************************/
Gia_ManResetRandom(Gia_ParSim_t * pPars)580 void Gia_ManResetRandom( Gia_ParSim_t * pPars )
581 {
582 int i;
583 Gia_ManRandom( 1 );
584 for ( i = 0; i < pPars->RandSeed; i++ )
585 Gia_ManRandom( 0 );
586 }
587
588 /**Function*************************************************************
589
590 Synopsis []
591
592 Description []
593
594 SideEffects []
595
596 SeeAlso []
597
598 ***********************************************************************/
Gia_ManSimSimulate(Gia_Man_t * pAig,Gia_ParSim_t * pPars)599 int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
600 {
601 extern int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
602 Gia_ManSim_t * p;
603 abctime clkTotal = Abc_Clock();
604 int i, iOut, iPat, RetValue = 0;
605 abctime nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
606 if ( pAig->pReprs && pAig->pNexts )
607 return Gia_ManSimSimulateEquiv( pAig, pPars );
608 ABC_FREE( pAig->pCexSeq );
609 p = Gia_ManSimCreate( pAig, pPars );
610 Gia_ManResetRandom( pPars );
611 Gia_ManSimInfoInit( p );
612 for ( i = 0; i < pPars->nIters; i++ )
613 {
614 Gia_ManSimulateRound( p );
615 if ( pPars->fVerbose )
616 {
617 Abc_Print( 1, "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
618 Abc_Print( 1, "Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC );
619 }
620 if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
621 {
622 Gia_ManResetRandom( pPars );
623 pPars->iOutFail = iOut;
624 pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
625 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", iOut, pAig->pName, i );
626 if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
627 {
628 // Abc_Print( 1, "\n" );
629 Abc_Print( 1, "\nGenerated counter-example is INVALID. " );
630 // Abc_Print( 1, "\n" );
631 }
632 else
633 {
634 // Abc_Print( 1, "\n" );
635 // if ( pPars->fVerbose )
636 // Abc_Print( 1, "\nGenerated counter-example is verified correctly. " );
637 // Abc_Print( 1, "\n" );
638 }
639 RetValue = 1;
640 break;
641 }
642 if ( Abc_Clock() > nTimeToStop )
643 {
644 i++;
645 break;
646 }
647 if ( i < pPars->nIters - 1 )
648 Gia_ManSimInfoTransfer( p );
649 }
650 Gia_ManSimDelete( p );
651 if ( pAig->pCexSeq == NULL )
652 Abc_Print( 1, "No bug detected after simulating %d frames with %d words. ", i, pPars->nWords );
653 Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
654 return RetValue;
655 }
656
657 /**Function*************************************************************
658
659 Synopsis []
660
661 Description []
662
663 SideEffects []
664
665 SeeAlso []
666
667 ***********************************************************************/
Gia_ManSimReadFile(char * pFileIn)668 Vec_Int_t * Gia_ManSimReadFile( char * pFileIn )
669 {
670 int c;
671 Vec_Int_t * vPat;
672 FILE * pFile = fopen( pFileIn, "rb" );
673 if ( pFile == NULL )
674 {
675 printf( "Cannot open input file.\n" );
676 return NULL;
677 }
678 vPat = Vec_IntAlloc( 1000 );
679 while ( (c = fgetc(pFile)) != EOF )
680 if ( c == '0' || c == '1' )
681 Vec_IntPush( vPat, c - '0' );
682 fclose( pFile );
683 return vPat;
684 }
Gia_ManSimWriteFile(char * pFileOut,Vec_Int_t * vPat,int nOuts)685 int Gia_ManSimWriteFile( char * pFileOut, Vec_Int_t * vPat, int nOuts )
686 {
687 int c, i;
688 FILE * pFile = fopen( pFileOut, "wb" );
689 if ( pFile == NULL )
690 {
691 printf( "Cannot open output file.\n" );
692 return 0;
693 }
694 assert( Vec_IntSize(vPat) % nOuts == 0 );
695 Vec_IntForEachEntry( vPat, c, i )
696 {
697 fputc( '0' + c, pFile );
698 if ( i % nOuts == nOuts - 1 )
699 fputc( '\n', pFile );
700 }
701 fclose( pFile );
702 return 1;
703 }
Gia_ManSimSimulateOne(Gia_Man_t * p,Vec_Int_t * vPat)704 Vec_Int_t * Gia_ManSimSimulateOne( Gia_Man_t * p, Vec_Int_t * vPat )
705 {
706 Vec_Int_t * vPatOut;
707 Gia_Obj_t * pObj, * pObjRo;
708 int i, k, f;
709 assert( Vec_IntSize(vPat) % Gia_ManPiNum(p) == 0 );
710 Gia_ManConst0(p)->fMark1 = 0;
711 Gia_ManForEachRo( p, pObj, i )
712 pObj->fMark1 = 0;
713 vPatOut = Vec_IntAlloc( 1000 );
714 for ( k = f = 0; f < Vec_IntSize(vPat) / Gia_ManPiNum(p); f++ )
715 {
716 Gia_ManForEachPi( p, pObj, i )
717 pObj->fMark1 = Vec_IntEntry( vPat, k++ );
718 Gia_ManForEachAnd( p, pObj, i )
719 pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
720 Gia_ManForEachCo( p, pObj, i )
721 pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj));
722 Gia_ManForEachPo( p, pObj, i )
723 Vec_IntPush( vPatOut, pObj->fMark1 );
724 Gia_ManForEachRiRo( p, pObj, pObjRo, i )
725 pObjRo->fMark1 = pObj->fMark1;
726 }
727 assert( k == Vec_IntSize(vPat) );
728 Gia_ManForEachObj( p, pObj, i )
729 pObj->fMark1 = 0;
730 return vPatOut;
731 }
Gia_ManSimSimulatePattern(Gia_Man_t * p,char * pFileIn,char * pFileOut)732 void Gia_ManSimSimulatePattern( Gia_Man_t * p, char * pFileIn, char * pFileOut )
733 {
734 Vec_Int_t * vPat, * vPatOut;
735 vPat = Gia_ManSimReadFile( pFileIn );
736 if ( vPat == NULL )
737 return;
738 if ( Vec_IntSize(vPat) % Gia_ManPiNum(p) )
739 {
740 printf( "The number of 0s and 1s in the input file (%d) does not evenly divide by the number of primary inputs (%d).\n",
741 Vec_IntSize(vPat), Gia_ManPiNum(p) );
742 Vec_IntFree( vPat );
743 return;
744 }
745 vPatOut = Gia_ManSimSimulateOne( p, vPat );
746 if ( Gia_ManSimWriteFile( pFileOut, vPatOut, Gia_ManPoNum(p) ) )
747 printf( "Output patterns are written into file \"%s\".\n", pFileOut );
748 Vec_IntFree( vPat );
749 Vec_IntFree( vPatOut );
750 }
751
752
753 /**Function*************************************************************
754
755 Synopsis [Bit-parallel simulation during AIG construction.]
756
757 Description []
758
759 SideEffects []
760
761 SeeAlso []
762
763 ***********************************************************************/
Gia_ManBuiltInDataPi(Gia_Man_t * p,int iCiId)764 static inline word * Gia_ManBuiltInDataPi( Gia_Man_t * p, int iCiId )
765 {
766 return Vec_WrdEntryP( p->vSimsPi, p->nSimWords * iCiId );
767 }
Gia_ManBuiltInData(Gia_Man_t * p,int iObj)768 static inline word * Gia_ManBuiltInData( Gia_Man_t * p, int iObj )
769 {
770 return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj );
771 }
Gia_ManBuiltInDataPrint(Gia_Man_t * p,int iObj)772 static inline void Gia_ManBuiltInDataPrint( Gia_Man_t * p, int iObj )
773 {
774 // printf( "Obj %6d : ", iObj ); Extra_PrintBinary( stdout, Gia_ManBuiltInData(p, iObj), p->nSimWords * 64 ); printf( "\n" );
775 }
Gia_ManBuiltInSimStart(Gia_Man_t * p,int nWords,int nObjs)776 void Gia_ManBuiltInSimStart( Gia_Man_t * p, int nWords, int nObjs )
777 {
778 int i, k;
779 assert( !p->fBuiltInSim );
780 assert( Gia_ManAndNum(p) == 0 );
781 p->fBuiltInSim = 1;
782 p->iPatsPi = 0;
783 p->iPastPiMax = 0;
784 p->nSimWords = nWords;
785 p->nSimWordsMax = 8;
786 Gia_ManRandomW( 1 );
787 // init PI care info
788 p->vSimsPi = Vec_WrdAlloc( p->nSimWords * Gia_ManCiNum(p) );
789 Vec_WrdFill( p->vSimsPi, p->nSimWords * Gia_ManCiNum(p), 0 );
790 // init object sim info
791 p->vSims = Vec_WrdAlloc( p->nSimWords * nObjs );
792 Vec_WrdFill( p->vSims, p->nSimWords, 0 );
793 for ( i = 0; i < Gia_ManCiNum(p); i++ )
794 for ( k = 0; k < p->nSimWords; k++ )
795 Vec_WrdPush( p->vSims, Gia_ManRandomW(0) );
796 }
Gia_ManBuiltInSimPerformInt(Gia_Man_t * p,int iObj)797 void Gia_ManBuiltInSimPerformInt( Gia_Man_t * p, int iObj )
798 {
799 Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); int w;
800 word * pInfo = Gia_ManBuiltInData( p, iObj );
801 word * pInfo0 = Gia_ManBuiltInData( p, Gia_ObjFaninId0(pObj, iObj) );
802 word * pInfo1 = Gia_ManBuiltInData( p, Gia_ObjFaninId1(pObj, iObj) );
803 assert( p->fBuiltInSim || p->fIncrSim );
804 if ( Gia_ObjFaninC0(pObj) )
805 {
806 if ( Gia_ObjFaninC1(pObj) )
807 for ( w = 0; w < p->nSimWords; w++ )
808 pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
809 else
810 for ( w = 0; w < p->nSimWords; w++ )
811 pInfo[w] = ~pInfo0[w] & pInfo1[w];
812 }
813 else
814 {
815 if ( Gia_ObjFaninC1(pObj) )
816 for ( w = 0; w < p->nSimWords; w++ )
817 pInfo[w] = pInfo0[w] & ~pInfo1[w];
818 else
819 for ( w = 0; w < p->nSimWords; w++ )
820 pInfo[w] = pInfo0[w] & pInfo1[w];
821 }
822 assert( Vec_WrdSize(p->vSims) == Gia_ManObjNum(p) * p->nSimWords );
823 }
Gia_ManBuiltInSimPerform(Gia_Man_t * p,int iObj)824 void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj )
825 {
826 int w;
827 for ( w = 0; w < p->nSimWords; w++ )
828 Vec_WrdPush( p->vSims, 0 );
829 Gia_ManBuiltInSimPerformInt( p, iObj );
830 }
831
Gia_ManBuiltInSimResimulateCone_rec(Gia_Man_t * p,int iObj)832 void Gia_ManBuiltInSimResimulateCone_rec( Gia_Man_t * p, int iObj )
833 {
834 Gia_Obj_t * pObj;
835 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
836 return;
837 Gia_ObjSetTravIdCurrentId(p, iObj);
838 pObj = Gia_ManObj( p, iObj );
839 if ( Gia_ObjIsCi(pObj) )
840 return;
841 assert( Gia_ObjIsAnd(pObj) );
842 Gia_ManBuiltInSimResimulateCone_rec( p, Gia_ObjFaninId0(pObj, iObj) );
843 Gia_ManBuiltInSimResimulateCone_rec( p, Gia_ObjFaninId1(pObj, iObj) );
844 Gia_ManBuiltInSimPerformInt( p, iObj );
845 }
Gia_ManBuiltInSimResimulateCone(Gia_Man_t * p,int iLit0,int iLit1)846 void Gia_ManBuiltInSimResimulateCone( Gia_Man_t * p, int iLit0, int iLit1 )
847 {
848 Gia_ManIncrementTravId( p );
849 Gia_ManBuiltInSimResimulateCone_rec( p, Abc_Lit2Var(iLit0) );
850 Gia_ManBuiltInSimResimulateCone_rec( p, Abc_Lit2Var(iLit1) );
851 }
Gia_ManBuiltInSimResimulate(Gia_Man_t * p)852 void Gia_ManBuiltInSimResimulate( Gia_Man_t * p )
853 {
854 Gia_Obj_t * pObj; int iObj;
855 Gia_ManForEachAnd( p, pObj, iObj )
856 Gia_ManBuiltInSimPerformInt( p, iObj );
857 }
858
Gia_ManBuiltInSimCheckOver(Gia_Man_t * p,int iLit0,int iLit1)859 int Gia_ManBuiltInSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 )
860 {
861 word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) );
862 word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w;
863 assert( p->fBuiltInSim || p->fIncrSim );
864
865 // printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) );
866 // Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" );
867 // Extra_PrintBinary( stdout, pInfo1, 64*p->nSimWords ); printf( "\n" );
868 // printf( "\n" );
869
870 if ( Abc_LitIsCompl(iLit0) )
871 {
872 if ( Abc_LitIsCompl(iLit1) )
873 {
874 for ( w = 0; w < p->nSimWords; w++ )
875 if ( ~pInfo0[w] & ~pInfo1[w] )
876 return 1;
877 }
878 else
879 {
880 for ( w = 0; w < p->nSimWords; w++ )
881 if ( ~pInfo0[w] & pInfo1[w] )
882 return 1;
883 }
884 }
885 else
886 {
887 if ( Abc_LitIsCompl(iLit1) )
888 {
889 for ( w = 0; w < p->nSimWords; w++ )
890 if ( pInfo0[w] & ~pInfo1[w] )
891 return 1;
892 }
893 else
894 {
895 for ( w = 0; w < p->nSimWords; w++ )
896 if ( pInfo0[w] & pInfo1[w] )
897 return 1;
898 }
899 }
900 return 0;
901 }
Gia_ManBuiltInSimCheckEqual(Gia_Man_t * p,int iLit0,int iLit1)902 int Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
903 {
904 word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) );
905 word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w;
906 assert( p->fBuiltInSim || p->fIncrSim );
907
908 // printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) );
909 // Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" );
910 // Extra_PrintBinary( stdout, pInfo1, 64*p->nSimWords ); printf( "\n" );
911 // printf( "\n" );
912
913 if ( Abc_LitIsCompl(iLit0) )
914 {
915 if ( Abc_LitIsCompl(iLit1) )
916 {
917 for ( w = 0; w < p->nSimWords; w++ )
918 if ( ~pInfo0[w] != ~pInfo1[w] )
919 return 0;
920 }
921 else
922 {
923 for ( w = 0; w < p->nSimWords; w++ )
924 if ( ~pInfo0[w] != pInfo1[w] )
925 return 0;
926 }
927 }
928 else
929 {
930 if ( Abc_LitIsCompl(iLit1) )
931 {
932 for ( w = 0; w < p->nSimWords; w++ )
933 if ( pInfo0[w] != ~pInfo1[w] )
934 return 0;
935 }
936 else
937 {
938 for ( w = 0; w < p->nSimWords; w++ )
939 if ( pInfo0[w] != pInfo1[w] )
940 return 0;
941 }
942 }
943 return 1;
944 }
945
Gia_ManBuiltInSimPack(Gia_Man_t * p,Vec_Int_t * vPat)946 int Gia_ManBuiltInSimPack( Gia_Man_t * p, Vec_Int_t * vPat )
947 {
948 int i, k, iLit;
949 assert( Vec_IntSize(vPat) > 0 );
950 //printf( "%d ", Vec_IntSize(vPat) );
951 for ( i = 0; i < p->iPatsPi; i++ )
952 {
953 Vec_IntForEachEntry( vPat, iLit, k )
954 if ( Abc_TtGetBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), i) &&
955 Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), i) == Abc_LitIsCompl(iLit) )
956 break;
957 if ( k == Vec_IntSize(vPat) )
958 return i; // success
959 }
960 return -1; // failure
961 }
962 // adds PI pattern to storage; the pattern comes in terms of CiIds
Gia_ManBuiltInSimAddPat(Gia_Man_t * p,Vec_Int_t * vPat)963 int Gia_ManBuiltInSimAddPat( Gia_Man_t * p, Vec_Int_t * vPat )
964 {
965 int Period = 0xF;
966 int fOverflow = p->iPatsPi == 64 * p->nSimWords && p->nSimWords == p->nSimWordsMax;
967 int k, iLit, iPat = Gia_ManBuiltInSimPack( p, vPat );
968 if ( iPat == -1 )
969 {
970 if ( fOverflow )
971 {
972 if ( (p->iPastPiMax & Period) == 0 )
973 Gia_ManBuiltInSimResimulate( p );
974 iPat = p->iPastPiMax;
975 //if ( p->iPastPiMax == 64 * p->nSimWordsMax - 1 )
976 // printf( "Completed the cycle.\n" );
977 p->iPastPiMax = p->iPastPiMax == 64 * p->nSimWordsMax - 1 ? 0 : p->iPastPiMax + 1;
978 }
979 else
980 {
981 if ( p->iPatsPi && (p->iPatsPi & Period) == 0 )
982 Gia_ManBuiltInSimResimulate( p );
983 if ( p->iPatsPi == 64 * p->nSimWords )
984 {
985 Vec_Wrd_t * vTemp = Vec_WrdAlloc( 2 * Vec_WrdSize(p->vSims) );
986 word Data; int w, Count = 0, iObj = 0;
987 Vec_WrdForEachEntry( p->vSims, Data, w )
988 {
989 Vec_WrdPush( vTemp, Data );
990 if ( ++Count == p->nSimWords )
991 {
992 Gia_Obj_t * pObj = Gia_ManObj(p, iObj++);
993 if ( Gia_ObjIsCi(pObj) )
994 Vec_WrdPush( vTemp, Gia_ManRandomW(0) ); // Vec_WrdPush( vTemp, 0 );
995 else if ( Gia_ObjIsAnd(pObj) )
996 Vec_WrdPush( vTemp, pObj->fPhase ? ~(word)0 : 0 );
997 else
998 Vec_WrdPush( vTemp, 0 );
999 Count = 0;
1000 }
1001 }
1002 assert( iObj == Gia_ManObjNum(p) );
1003 Vec_WrdFree( p->vSims );
1004 p->vSims = vTemp;
1005
1006 vTemp = Vec_WrdAlloc( 2 * Vec_WrdSize(p->vSimsPi) );
1007 Count = 0;
1008 Vec_WrdForEachEntry( p->vSimsPi, Data, w )
1009 {
1010 Vec_WrdPush( vTemp, Data );
1011 if ( ++Count == p->nSimWords )
1012 {
1013 Vec_WrdPush( vTemp, 0 );
1014 Count = 0;
1015 }
1016 }
1017 Vec_WrdFree( p->vSimsPi );
1018 p->vSimsPi = vTemp;
1019
1020 // update the word count
1021 p->nSimWords++;
1022 assert( Vec_WrdSize(p->vSims) == p->nSimWords * Gia_ManObjNum(p) );
1023 assert( Vec_WrdSize(p->vSimsPi) == p->nSimWords * Gia_ManCiNum(p) );
1024 //printf( "Resizing to %d words.\n", p->nSimWords );
1025 }
1026 iPat = p->iPatsPi++;
1027 }
1028 }
1029 assert( iPat >= 0 && iPat < p->iPatsPi );
1030 // add literals
1031 if ( fOverflow )
1032 {
1033 int iVar;
1034 Vec_IntForEachEntry( &p->vSuppVars, iVar, k )
1035 if ( Abc_TtGetBit(Gia_ManBuiltInDataPi(p, iVar), iPat) )
1036 Abc_TtXorBit(Gia_ManBuiltInDataPi(p, iVar), iPat);
1037 Vec_IntForEachEntry( vPat, iLit, k )
1038 {
1039 if ( Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat) == Abc_LitIsCompl(iLit) )
1040 Abc_TtXorBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat);
1041 Abc_TtXorBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), iPat);
1042 }
1043 }
1044 else
1045 {
1046 Vec_IntForEachEntry( vPat, iLit, k )
1047 {
1048 if ( Abc_TtGetBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), iPat) )
1049 assert( Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat) != Abc_LitIsCompl(iLit) );
1050 else
1051 {
1052 if ( Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat) == Abc_LitIsCompl(iLit) )
1053 Abc_TtXorBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat);
1054 Abc_TtXorBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), iPat);
1055 }
1056 }
1057 }
1058 return 1;
1059 }
1060
1061 /**Function*************************************************************
1062
1063 Synopsis [Finds a satisfying assignment.]
1064
1065 Description [Returns 1 if a sat assignment is found; 0 otherwise.]
1066
1067 SideEffects []
1068
1069 SeeAlso []
1070
1071 ***********************************************************************/
Gia_ManObjCheckSat_rec(Gia_Man_t * p,int iLit,Vec_Int_t * vObjs)1072 int Gia_ManObjCheckSat_rec( Gia_Man_t * p, int iLit, Vec_Int_t * vObjs )
1073 {
1074 int iObj = Abc_Lit2Var(iLit);
1075 Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
1076 if ( pObj->fMark0 )
1077 return pObj->fMark1 == (unsigned)Abc_LitIsCompl(iLit);
1078 pObj->fMark0 = 1;
1079 pObj->fMark1 = Abc_LitIsCompl(iLit);
1080 Vec_IntPush( vObjs, iObj );
1081 if ( Gia_ObjIsAnd(pObj) )
1082 {
1083 if ( pObj->fMark1 == 0 ) // node value is 1
1084 {
1085 if ( !Gia_ManObjCheckSat_rec( p, Gia_ObjFaninLit0(pObj, iObj), vObjs ) ) return 0;
1086 if ( !Gia_ManObjCheckSat_rec( p, Gia_ObjFaninLit1(pObj, iObj), vObjs ) ) return 0;
1087 }
1088 else
1089 {
1090 if ( !Gia_ManObjCheckSat_rec( p, Abc_LitNot(Gia_ObjFaninLit0(pObj, iObj)), vObjs ) ) return 0;
1091 }
1092 }
1093 return 1;
1094 }
Gia_ManObjCheckOverlap1(Gia_Man_t * p,int iLit0,int iLit1,Vec_Int_t * vObjs)1095 int Gia_ManObjCheckOverlap1( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs )
1096 {
1097 Gia_Obj_t * pObj;
1098 int i, Res0, Res1 = 0;
1099 // Gia_ManForEachObj( p, pObj, i )
1100 // assert( pObj->fMark0 == 0 && pObj->fMark1 == 0 );
1101 Vec_IntClear( vObjs );
1102 Res0 = Gia_ManObjCheckSat_rec( p, iLit0, vObjs );
1103 if ( Res0 )
1104 Res1 = Gia_ManObjCheckSat_rec( p, iLit1, vObjs );
1105 Gia_ManForEachObjVec( vObjs, p, pObj, i )
1106 pObj->fMark0 = pObj->fMark1 = 0;
1107 return Res0 && Res1;
1108 }
Gia_ManObjCheckOverlap(Gia_Man_t * p,int iLit0,int iLit1,Vec_Int_t * vObjs)1109 int Gia_ManObjCheckOverlap( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs )
1110 {
1111 if ( Gia_ManObjCheckOverlap1( p, iLit0, iLit1, vObjs ) )
1112 return 1;
1113 return Gia_ManObjCheckOverlap1( p, iLit1, iLit0, vObjs );
1114 }
1115
1116
1117
1118
1119
1120 /**Function*************************************************************
1121
1122 Synopsis [Bit-parallel simulation during AIG construction.]
1123
1124 Description []
1125
1126 SideEffects []
1127
1128 SeeAlso []
1129
1130 ***********************************************************************/
Gia_ManIncrSimUpdate(Gia_Man_t * p)1131 void Gia_ManIncrSimUpdate( Gia_Man_t * p )
1132 {
1133 int i, k;
1134 // extend timestamp info
1135 assert( Vec_IntSize(p->vTimeStamps) <= Gia_ManObjNum(p) );
1136 Vec_IntFillExtra( p->vTimeStamps, Gia_ManObjNum(p), 0 );
1137 // extend simulation info
1138 assert( Vec_WrdSize(p->vSims) <= Gia_ManObjNum(p) * p->nSimWords );
1139 Vec_WrdFillExtra( p->vSims, Gia_ManObjNum(p) * p->nSimWords, 0 );
1140 // extend PI info
1141 assert( p->iNextPi <= Gia_ManCiNum(p) );
1142 for ( i = p->iNextPi; i < Gia_ManCiNum(p); i++ )
1143 {
1144 word * pSims = Gia_ManBuiltInData( p, Gia_ManCiIdToId(p, i) );
1145 for ( k = 0; k < p->nSimWords; k++ )
1146 pSims[k] = Gia_ManRandomW(0);
1147 }
1148 p->iNextPi = Gia_ManCiNum(p);
1149 }
Gia_ManIncrSimStart(Gia_Man_t * p,int nWords,int nObjs)1150 void Gia_ManIncrSimStart( Gia_Man_t * p, int nWords, int nObjs )
1151 {
1152 assert( !p->fIncrSim );
1153 p->fIncrSim = 1;
1154 p->iPatsPi = 0;
1155 p->nSimWords = nWords;
1156 // init time stamps
1157 p->iTimeStamp = 1;
1158 p->vTimeStamps = Vec_IntAlloc( p->nSimWords );
1159 // init object sim info
1160 p->iNextPi = 0;
1161 p->vSims = Vec_WrdAlloc( p->nSimWords * nObjs );
1162 Gia_ManRandomW( 1 );
1163 }
Gia_ManIncrSimStop(Gia_Man_t * p)1164 void Gia_ManIncrSimStop( Gia_Man_t * p )
1165 {
1166 assert( p->fIncrSim );
1167 p->fIncrSim = 0;
1168 p->iPatsPi = 0;
1169 p->nSimWords = 0;
1170 p->iTimeStamp = 1;
1171 Vec_IntFreeP( &p->vTimeStamps );
1172 Vec_WrdFreeP( &p->vSims );
1173 }
Gia_ManIncrSimSet(Gia_Man_t * p,Vec_Int_t * vObjLits)1174 void Gia_ManIncrSimSet( Gia_Man_t * p, Vec_Int_t * vObjLits )
1175 {
1176 int i, iLit;
1177 assert( Vec_IntSize(vObjLits) > 0 );
1178 p->iTimeStamp++;
1179 Vec_IntForEachEntry( vObjLits, iLit, i )
1180 {
1181 word * pSims = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit) );
1182 if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) )
1183 continue;
1184 //assert( Vec_IntEntry(p->vTimeStamps, Abc_Lit2Var(iLit)) == p->iTimeStamp-1 );
1185 Vec_IntWriteEntry(p->vTimeStamps, Abc_Lit2Var(iLit), p->iTimeStamp);
1186 if ( Abc_TtGetBit(pSims, p->iPatsPi) == Abc_LitIsCompl(iLit) )
1187 Abc_TtXorBit(pSims, p->iPatsPi);
1188 }
1189 p->iPatsPi = (p->iPatsPi == p->nSimWords * 64 - 1) ? 0 : p->iPatsPi + 1;
1190 }
Gia_ManIncrSimCone_rec(Gia_Man_t * p,int iObj)1191 void Gia_ManIncrSimCone_rec( Gia_Man_t * p, int iObj )
1192 {
1193 Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
1194 if ( Gia_ObjIsCi(pObj) )
1195 return;
1196 if ( Vec_IntEntry(p->vTimeStamps, iObj) == p->iTimeStamp )
1197 return;
1198 assert( Vec_IntEntry(p->vTimeStamps, iObj) < p->iTimeStamp );
1199 Vec_IntWriteEntry( p->vTimeStamps, iObj, p->iTimeStamp );
1200 assert( Gia_ObjIsAnd(pObj) );
1201 Gia_ManIncrSimCone_rec( p, Gia_ObjFaninId0(pObj, iObj) );
1202 Gia_ManIncrSimCone_rec( p, Gia_ObjFaninId1(pObj, iObj) );
1203 Gia_ManBuiltInSimPerformInt( p, iObj );
1204 }
Gia_ManIncrSimCheckOver(Gia_Man_t * p,int iLit0,int iLit1)1205 int Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 )
1206 {
1207 assert( iLit0 > 1 && iLit1 > 1 );
1208 Gia_ManIncrSimUpdate( p );
1209 Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) );
1210 Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) );
1211 // return 0; // disable
1212 return Gia_ManBuiltInSimCheckOver( p, iLit0, iLit1 );
1213 }
Gia_ManIncrSimCheckEqual(Gia_Man_t * p,int iLit0,int iLit1)1214 int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
1215 {
1216 assert( iLit0 > 1 && iLit1 > 1 );
1217 Gia_ManIncrSimUpdate( p );
1218 Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) );
1219 Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) );
1220 // return 1; // disable
1221 return Gia_ManBuiltInSimCheckEqual( p, iLit0, iLit1 );
1222 }
1223
1224
1225
1226 ////////////////////////////////////////////////////////////////////////
1227 /// END OF FILE ///
1228 ////////////////////////////////////////////////////////////////////////
1229
1230
1231 ABC_NAMESPACE_IMPL_END
1232
1233