abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaSim.c
Go to the documentation of this file.
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 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static inline unsigned * Gia_SimData( Gia_ManSim_t * p, int i ) { return p->pDataSim + i * p->nWords; }
31 static inline unsigned * Gia_SimDataCi( Gia_ManSim_t * p, int i ) { return p->pDataSimCis + i * p->nWords; }
32 static inline unsigned * Gia_SimDataCo( Gia_ManSim_t * p, int i ) { return p->pDataSimCos + i * p->nWords; }
33 
34 unsigned * Gia_SimDataExt( Gia_ManSim_t * p, int i ) { return Gia_SimData(p, i); }
35 unsigned * Gia_SimDataCiExt( Gia_ManSim_t * p, int i ) { return Gia_SimDataCi(p, i); }
36 unsigned * Gia_SimDataCoExt( Gia_ManSim_t * p, int i ) { return Gia_SimDataCo(p, i); }
37 
38 ////////////////////////////////////////////////////////////////////////
39 /// FUNCTION DEFINITIONS ///
40 ////////////////////////////////////////////////////////////////////////
41 
42 
43 /**Function*************************************************************
44 
45  Synopsis []
46 
47  Description []
48 
49  SideEffects []
50 
51  SeeAlso []
52 
53 ***********************************************************************/
54 void Gia_ManSimCollect_rec( Gia_Man_t * pGia, Gia_Obj_t * pObj, Vec_Int_t * vVec )
55 {
56  Vec_IntPush( vVec, Gia_ObjToLit(pGia, pObj) );
57  if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) )
58  return;
59  assert( Gia_ObjIsAnd(pObj) );
60  Gia_ManSimCollect_rec( pGia, Gia_ObjChild0(pObj), vVec );
61  Gia_ManSimCollect_rec( pGia, Gia_ObjChild1(pObj), vVec );
62 }
63 
64 /**Function*************************************************************
65 
66  Synopsis [Derives signal implications.]
67 
68  Description []
69 
70  SideEffects []
71 
72  SeeAlso []
73 
74 ***********************************************************************/
75 void Gia_ManSimCollect( Gia_Man_t * pGia, Gia_Obj_t * pObj, Vec_Int_t * vVec )
76 {
77  Vec_IntClear( vVec );
78  Gia_ManSimCollect_rec( pGia, pObj, vVec );
79  Vec_IntUniqify( vVec );
80 }
81 
82 /**Function*************************************************************
83 
84  Synopsis [Finds signals, which reset flops to have constant values.]
85 
86  Description []
87 
88  SideEffects []
89 
90  SeeAlso []
91 
92 ***********************************************************************/
93 Vec_Int_t * Gia_ManSimDeriveResets( Gia_Man_t * pGia )
94 {
95  int nImpLimit = 5;
96  Vec_Int_t * vResult;
97  Vec_Int_t * vCountLits, * vSuperGate;
98  Gia_Obj_t * pObj;
99  int i, k, Lit, Count;
100  int Counter0 = 0, Counter1 = 0;
101  int CounterPi0 = 0, CounterPi1 = 0;
102  abctime clk = Abc_Clock();
103 
104  // create reset counters for each literal
105  vCountLits = Vec_IntStart( 2 * Gia_ManObjNum(pGia) );
106 
107  // collect implications for each flop input driver
108  vSuperGate = Vec_IntAlloc( 1000 );
109  Gia_ManForEachRi( pGia, pObj, i )
110  {
111  if ( Gia_ObjFaninId0p(pGia, pObj) == 0 )
112  continue;
113  Vec_IntAddToEntry( vCountLits, Gia_ObjToLit(pGia, Gia_ObjChild0(pObj)), 1 );
114  Gia_ManSimCollect( pGia, Gia_ObjFanin0(pObj), vSuperGate );
115  Vec_IntForEachEntry( vSuperGate, Lit, k )
116  Vec_IntAddToEntry( vCountLits, Lit, 1 );
117  }
118  Vec_IntFree( vSuperGate );
119 
120  // label signals whose counter if more than the limit
121  vResult = Vec_IntStartFull( Gia_ManObjNum(pGia) );
122  Vec_IntForEachEntry( vCountLits, Count, Lit )
123  {
124  if ( Count < nImpLimit )
125  continue;
126  pObj = Gia_ManObj( pGia, Abc_Lit2Var(Lit) );
127  if ( Abc_LitIsCompl(Lit) ) // const 0
128  {
129 // Ssm_ObjSetLogic0( pObj );
130  Vec_IntWriteEntry( vResult, Abc_Lit2Var(Lit), 0 );
131  CounterPi0 += Gia_ObjIsPi(pGia, pObj);
132  Counter0++;
133  }
134  else
135  {
136 // Ssm_ObjSetLogic1( pObj );
137  Vec_IntWriteEntry( vResult, Abc_Lit2Var(Lit), 1 );
138  CounterPi1 += Gia_ObjIsPi(pGia, pObj);
139  Counter1++;
140  }
141 // if ( Gia_ObjIsPi(pGia, pObj) )
142 // printf( "%d ", Count );
143  }
144 // printf( "\n" );
145  Vec_IntFree( vCountLits );
146 
147  printf( "Logic0 = %d (%d). Logic1 = %d (%d). ", Counter0, CounterPi0, Counter1, CounterPi1 );
148  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
149  return vResult;
150 }
151 
152 
153 /**Function*************************************************************
154 
155  Synopsis [This procedure sets default parameters.]
156 
157  Description []
158 
159  SideEffects []
160 
161  SeeAlso []
162 
163 ***********************************************************************/
164 void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p )
165 {
166  memset( p, 0, sizeof(Gia_ParSim_t) );
167  // user-controlled parameters
168  p->nWords = 8; // the number of machine words
169  p->nIters = 32; // the number of timeframes
170  p->RandSeed = 0; // the seed to generate random numbers
171  p->TimeLimit = 60; // time limit in seconds
172  p->fCheckMiter = 0; // check if miter outputs are non-zero
173  p->fVerbose = 0; // enables verbose output
174  p->iOutFail = -1; // index of the failed output
175 }
176 
177 /**Function*************************************************************
178 
179  Synopsis []
180 
181  Description []
182 
183  SideEffects []
184 
185  SeeAlso []
186 
187 ***********************************************************************/
188 void Gia_ManSimDelete( Gia_ManSim_t * p )
189 {
190  Vec_IntFreeP( &p->vConsts );
191  Vec_IntFreeP( &p->vCis2Ids );
192  Gia_ManStopP( &p->pAig );
193  ABC_FREE( p->pDataSim );
194  ABC_FREE( p->pDataSimCis );
195  ABC_FREE( p->pDataSimCos );
196  ABC_FREE( p );
197 }
198 
199 /**Function*************************************************************
200 
201  Synopsis [Creates fast simulation manager.]
202 
203  Description []
204 
205  SideEffects []
206 
207  SeeAlso []
208 
209 ***********************************************************************/
210 Gia_ManSim_t * Gia_ManSimCreate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
211 {
212  Gia_ManSim_t * p;
213  int Entry, i;
214  p = ABC_ALLOC( Gia_ManSim_t, 1 );
215  memset( p, 0, sizeof(Gia_ManSim_t) );
216  // look for reset signals
217  if ( pPars->fVerbose )
218  p->vConsts = Gia_ManSimDeriveResets( pAig );
219  // derive the frontier
220  p->pAig = Gia_ManFront( pAig );
221  p->pPars = pPars;
222  p->nWords = pPars->nWords;
223  p->pDataSim = ABC_ALLOC( unsigned, p->nWords * p->pAig->nFront );
224  p->pDataSimCis = ABC_ALLOC( unsigned, p->nWords * Gia_ManCiNum(p->pAig) );
225  p->pDataSimCos = ABC_ALLOC( unsigned, p->nWords * Gia_ManCoNum(p->pAig) );
226  if ( !p->pDataSim || !p->pDataSimCis || !p->pDataSimCos )
227  {
228  Abc_Print( 1, "Simulator could not allocate %.2f GB for simulation info.\n",
229  4.0 * p->nWords * (p->pAig->nFront + Gia_ManCiNum(p->pAig) + Gia_ManCoNum(p->pAig)) / (1<<30) );
230  Gia_ManSimDelete( p );
231  return NULL;
232  }
233  p->vCis2Ids = Vec_IntAlloc( Gia_ManCiNum(p->pAig) );
234  Vec_IntForEachEntry( pAig->vCis, Entry, i )
235  Vec_IntPush( p->vCis2Ids, i ); // do we need p->vCis2Ids?
236  if ( pPars->fVerbose )
237  Abc_Print( 1, "AIG = %7.2f MB. Front mem = %7.2f MB. Other mem = %7.2f MB.\n",
238  12.0*Gia_ManObjNum(p->pAig)/(1<<20),
239  4.0*p->nWords*p->pAig->nFront/(1<<20),
240  4.0*p->nWords*(Gia_ManCiNum(p->pAig) + Gia_ManCoNum(p->pAig))/(1<<20) );
241 
242  return p;
243 }
244 
245 /**Function*************************************************************
246 
247  Synopsis []
248 
249  Description []
250 
251  SideEffects []
252 
253  SeeAlso []
254 
255 ***********************************************************************/
256 static inline void Gia_ManSimInfoRandom( Gia_ManSim_t * p, unsigned * pInfo )
257 {
258  int w;
259  for ( w = p->nWords-1; w >= 0; w-- )
260  pInfo[w] = Gia_ManRandom( 0 );
261 }
262 
263 /**Function*************************************************************
264 
265  Synopsis []
266 
267  Description []
268 
269  SideEffects []
270 
271  SeeAlso []
272 
273 ***********************************************************************/
274 static inline void Gia_ManSimInfoZero( Gia_ManSim_t * p, unsigned * pInfo )
275 {
276  int w;
277  for ( w = p->nWords-1; w >= 0; w-- )
278  pInfo[w] = 0;
279 }
280 
281 /**Function*************************************************************
282 
283  Synopsis [Returns index of the first pattern that failed.]
284 
285  Description []
286 
287  SideEffects []
288 
289  SeeAlso []
290 
291 ***********************************************************************/
292 static inline int Gia_ManSimInfoIsZero( Gia_ManSim_t * p, unsigned * pInfo )
293 {
294  int w;
295  for ( w = 0; w < p->nWords; w++ )
296  if ( pInfo[w] )
297  return 32*w + Gia_WordFindFirstBit( pInfo[w] );
298  return -1;
299 }
300 
301 /**Function*************************************************************
302 
303  Synopsis []
304 
305  Description []
306 
307  SideEffects []
308 
309  SeeAlso []
310 
311 ***********************************************************************/
312 static inline void Gia_ManSimInfoOne( Gia_ManSim_t * p, unsigned * pInfo )
313 {
314  int w;
315  for ( w = p->nWords-1; w >= 0; w-- )
316  pInfo[w] = ~0;
317 }
318 
319 /**Function*************************************************************
320 
321  Synopsis []
322 
323  Description []
324 
325  SideEffects []
326 
327  SeeAlso []
328 
329 ***********************************************************************/
330 static inline void Gia_ManSimInfoCopy( Gia_ManSim_t * p, unsigned * pInfo, unsigned * pInfo0 )
331 {
332  int w;
333  for ( w = p->nWords-1; w >= 0; w-- )
334  pInfo[w] = pInfo0[w];
335 }
336 
337 /**Function*************************************************************
338 
339  Synopsis []
340 
341  Description []
342 
343  SideEffects []
344 
345  SeeAlso []
346 
347 ***********************************************************************/
348 static inline void Gia_ManSimulateCi( Gia_ManSim_t * p, Gia_Obj_t * pObj, int iCi )
349 {
350  unsigned * pInfo = Gia_SimData( p, Gia_ObjValue(pObj) );
351  unsigned * pInfo0 = Gia_SimDataCi( p, iCi );
352  int w;
353  for ( w = p->nWords-1; w >= 0; w-- )
354  pInfo[w] = pInfo0[w];
355 }
356 
357 /**Function*************************************************************
358 
359  Synopsis []
360 
361  Description []
362 
363  SideEffects []
364 
365  SeeAlso []
366 
367 ***********************************************************************/
368 static inline void Gia_ManSimulateCo( Gia_ManSim_t * p, int iCo, Gia_Obj_t * pObj )
369 {
370  unsigned * pInfo = Gia_SimDataCo( p, iCo );
371  unsigned * pInfo0 = Gia_SimData( p, Gia_ObjDiff0(pObj) );
372  int w;
373  if ( Gia_ObjFaninC0(pObj) )
374  for ( w = p->nWords-1; w >= 0; w-- )
375  pInfo[w] = ~pInfo0[w];
376  else
377  for ( w = p->nWords-1; w >= 0; w-- )
378  pInfo[w] = pInfo0[w];
379 }
380 
381 /**Function*************************************************************
382 
383  Synopsis []
384 
385  Description []
386 
387  SideEffects []
388 
389  SeeAlso []
390 
391 ***********************************************************************/
392 static inline void Gia_ManSimulateNode( Gia_ManSim_t * p, Gia_Obj_t * pObj )
393 {
394  unsigned * pInfo = Gia_SimData( p, Gia_ObjValue(pObj) );
395  unsigned * pInfo0 = Gia_SimData( p, Gia_ObjDiff0(pObj) );
396  unsigned * pInfo1 = Gia_SimData( p, Gia_ObjDiff1(pObj) );
397  int w;
398  if ( Gia_ObjFaninC0(pObj) )
399  {
400  if ( Gia_ObjFaninC1(pObj) )
401  for ( w = p->nWords-1; w >= 0; w-- )
402  pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
403  else
404  for ( w = p->nWords-1; w >= 0; w-- )
405  pInfo[w] = ~pInfo0[w] & pInfo1[w];
406  }
407  else
408  {
409  if ( Gia_ObjFaninC1(pObj) )
410  for ( w = p->nWords-1; w >= 0; w-- )
411  pInfo[w] = pInfo0[w] & ~pInfo1[w];
412  else
413  for ( w = p->nWords-1; w >= 0; w-- )
414  pInfo[w] = pInfo0[w] & pInfo1[w];
415  }
416 }
417 
418 /**Function*************************************************************
419 
420  Synopsis []
421 
422  Description []
423 
424  SideEffects []
425 
426  SeeAlso []
427 
428 ***********************************************************************/
429 void Gia_ManSimInfoInit( Gia_ManSim_t * p )
430 {
431  int iPioNum, i;
432  Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
433  {
434  if ( iPioNum < Gia_ManPiNum(p->pAig) )
435  Gia_ManSimInfoRandom( p, Gia_SimDataCi(p, i) );
436  else
437  Gia_ManSimInfoZero( p, Gia_SimDataCi(p, i) );
438  }
439 }
440 
441 /**Function*************************************************************
442 
443  Synopsis []
444 
445  Description []
446 
447  SideEffects []
448 
449  SeeAlso []
450 
451 ***********************************************************************/
452 void Gia_ManSimInfoTransfer( Gia_ManSim_t * p )
453 {
454  int iPioNum, i;
455  Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
456  {
457  if ( iPioNum < Gia_ManPiNum(p->pAig) )
458  Gia_ManSimInfoRandom( p, Gia_SimDataCi(p, i) );
459  else
460  Gia_ManSimInfoCopy( p, Gia_SimDataCi(p, i), Gia_SimDataCo(p, Gia_ManPoNum(p->pAig)+iPioNum-Gia_ManPiNum(p->pAig)) );
461  }
462 }
463 
464 /**Function*************************************************************
465 
466  Synopsis []
467 
468  Description []
469 
470  SideEffects []
471 
472  SeeAlso []
473 
474 ***********************************************************************/
475 void Gia_ManSimulateRound( Gia_ManSim_t * p )
476 {
477  Gia_Obj_t * pObj;
478  int i, iCis = 0, iCos = 0;
479  assert( p->pAig->nFront > 0 );
480  assert( Gia_ManConst0(p->pAig)->Value == 0 );
481  Gia_ManSimInfoZero( p, Gia_SimData(p, 0) );
482  Gia_ManForEachObj1( p->pAig, pObj, i )
483  {
484  if ( Gia_ObjIsAndOrConst0(pObj) )
485  {
486  assert( Gia_ObjValue(pObj) < p->pAig->nFront );
487  Gia_ManSimulateNode( p, pObj );
488  }
489  else if ( Gia_ObjIsCo(pObj) )
490  {
491  assert( Gia_ObjValue(pObj) == GIA_NONE );
492  Gia_ManSimulateCo( p, iCos++, pObj );
493  }
494  else // if ( Gia_ObjIsCi(pObj) )
495  {
496  assert( Gia_ObjValue(pObj) < p->pAig->nFront );
497  Gia_ManSimulateCi( p, pObj, iCis++ );
498  }
499  }
500  assert( Gia_ManCiNum(p->pAig) == iCis );
501  assert( Gia_ManCoNum(p->pAig) == iCos );
502 }
503 
504 /**Function*************************************************************
505 
506  Synopsis [Returns index of the PO and pattern that failed it.]
507 
508  Description []
509 
510  SideEffects []
511 
512  SeeAlso []
513 
514 ***********************************************************************/
515 static inline int Gia_ManCheckPos( Gia_ManSim_t * p, int * piPo, int * piPat )
516 {
517  int i, iPat;
518  for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
519  {
520  iPat = Gia_ManSimInfoIsZero( p, Gia_SimDataCo(p, i) );
521  if ( iPat >= 0 )
522  {
523  *piPo = i;
524  *piPat = iPat;
525  return 1;
526  }
527  }
528  return 0;
529 }
530 
531 /**Function*************************************************************
532 
533  Synopsis [Returns the counter-example.]
534 
535  Description []
536 
537  SideEffects []
538 
539  SeeAlso []
540 
541 ***********************************************************************/
542 Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids )
543 {
544  Abc_Cex_t * p;
545  unsigned * pData;
546  int f, i, w, iPioId, Counter;
547  p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
548  p->iFrame = iFrame;
549  p->iPo = iOut;
550  // fill in the binary data
551  Counter = p->nRegs;
552  pData = ABC_ALLOC( unsigned, nWords );
553  for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
554  for ( i = 0; i < Gia_ManPiNum(pAig); i++ )
555  {
556  iPioId = Vec_IntEntry( vCis2Ids, i );
557  if ( iPioId >= p->nPis )
558  continue;
559  for ( w = nWords-1; w >= 0; w-- )
560  pData[w] = Gia_ManRandom( 0 );
561  if ( Abc_InfoHasBit( pData, iPat ) )
562  Abc_InfoSetBit( p->pData, Counter + iPioId );
563  }
564  ABC_FREE( pData );
565  return p;
566 }
567 
568 /**Function*************************************************************
569 
570  Synopsis []
571 
572  Description []
573 
574  SideEffects []
575 
576  SeeAlso []
577 
578 ***********************************************************************/
579 void Gia_ManResetRandom( Gia_ParSim_t * pPars )
580 {
581  int i;
582  Gia_ManRandom( 1 );
583  for ( i = 0; i < pPars->RandSeed; i++ )
584  Gia_ManRandom( 0 );
585 }
586 
587 /**Function*************************************************************
588 
589  Synopsis []
590 
591  Description []
592 
593  SideEffects []
594 
595  SeeAlso []
596 
597 ***********************************************************************/
598 int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
599 {
600  extern int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
601  Gia_ManSim_t * p;
602  abctime clkTotal = Abc_Clock();
603  int i, iOut, iPat, RetValue = 0;
604  abctime nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
605  if ( pAig->pReprs && pAig->pNexts )
606  return Gia_ManSimSimulateEquiv( pAig, pPars );
607  ABC_FREE( pAig->pCexSeq );
608  p = Gia_ManSimCreate( pAig, pPars );
609  Gia_ManResetRandom( pPars );
610  Gia_ManSimInfoInit( p );
611  for ( i = 0; i < pPars->nIters; i++ )
612  {
613  Gia_ManSimulateRound( p );
614  if ( pPars->fVerbose )
615  {
616  Abc_Print( 1, "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
617  Abc_Print( 1, "Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC );
618  }
619  if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
620  {
621  Gia_ManResetRandom( pPars );
622  pPars->iOutFail = iOut;
623  pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
624  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", iOut, pAig->pName, i );
625  if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
626  {
627 // Abc_Print( 1, "\n" );
628  Abc_Print( 1, "\nGenerated counter-example is INVALID. " );
629 // Abc_Print( 1, "\n" );
630  }
631  else
632  {
633 // Abc_Print( 1, "\n" );
634 // if ( pPars->fVerbose )
635 // Abc_Print( 1, "\nGenerated counter-example is verified correctly. " );
636 // Abc_Print( 1, "\n" );
637  }
638  RetValue = 1;
639  break;
640  }
641  if ( Abc_Clock() > nTimeToStop )
642  {
643  i++;
644  break;
645  }
646  if ( i < pPars->nIters - 1 )
647  Gia_ManSimInfoTransfer( p );
648  }
649  Gia_ManSimDelete( p );
650  if ( pAig->pCexSeq == NULL )
651  Abc_Print( 1, "No bug detected after simulating %d frames with %d words. ", i, pPars->nWords );
652  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
653  return RetValue;
654 }
655 
656 /**Function*************************************************************
657 
658  Synopsis []
659 
660  Description []
661 
662  SideEffects []
663 
664  SeeAlso []
665 
666 ***********************************************************************/
667 Vec_Int_t * Gia_ManSimReadFile( char * pFileIn )
668 {
669  int c;
670  Vec_Int_t * vPat;
671  FILE * pFile = fopen( pFileIn, "rb" );
672  if ( pFile == NULL )
673  {
674  printf( "Cannot open input file.\n" );
675  return NULL;
676  }
677  vPat = Vec_IntAlloc( 1000 );
678  while ( (c = fgetc(pFile)) != EOF )
679  if ( c == '0' || c == '1' )
680  Vec_IntPush( vPat, c - '0' );
681  fclose( pFile );
682  return vPat;
683 }
684 int Gia_ManSimWriteFile( char * pFileOut, Vec_Int_t * vPat, int nOuts )
685 {
686  int c, i;
687  FILE * pFile = fopen( pFileOut, "wb" );
688  if ( pFile == NULL )
689  {
690  printf( "Cannot open output file.\n" );
691  return 0;
692  }
693  assert( Vec_IntSize(vPat) % nOuts == 0 );
694  Vec_IntForEachEntry( vPat, c, i )
695  {
696  fputc( '0' + c, pFile );
697  if ( i % nOuts == nOuts - 1 )
698  fputc( '\n', pFile );
699  }
700  fclose( pFile );
701  return 1;
702 }
703 Vec_Int_t * Gia_ManSimSimulateOne( Gia_Man_t * p, Vec_Int_t * vPat )
704 {
705  Vec_Int_t * vPatOut;
706  Gia_Obj_t * pObj, * pObjRo;
707  int i, k, f;
708  assert( Vec_IntSize(vPat) % Gia_ManPiNum(p) == 0 );
709  Gia_ManConst0(p)->fMark1 = 0;
710  Gia_ManForEachRo( p, pObj, i )
711  pObj->fMark1 = 0;
712  vPatOut = Vec_IntAlloc( 1000 );
713  for ( k = f = 0; f < Vec_IntSize(vPat) / Gia_ManPiNum(p); f++ )
714  {
715  Gia_ManForEachPi( p, pObj, i )
716  pObj->fMark1 = Vec_IntEntry( vPat, k++ );
717  Gia_ManForEachAnd( p, pObj, i )
718  pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
719  Gia_ManForEachCo( p, pObj, i )
720  pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj));
721  Gia_ManForEachPo( p, pObj, i )
722  Vec_IntPush( vPatOut, pObj->fMark1 );
723  Gia_ManForEachRiRo( p, pObj, pObjRo, i )
724  pObjRo->fMark1 = pObj->fMark1;
725  }
726  assert( k == Vec_IntSize(vPat) );
727  Gia_ManForEachObj( p, pObj, i )
728  pObj->fMark1 = 0;
729  return vPatOut;
730 }
731 void Gia_ManSimSimulatePattern( Gia_Man_t * p, char * pFileIn, char * pFileOut )
732 {
733  Vec_Int_t * vPat, * vPatOut;
734  vPat = Gia_ManSimReadFile( pFileIn );
735  if ( vPat == NULL )
736  return;
737  if ( Vec_IntSize(vPat) % Gia_ManPiNum(p) )
738  {
739  printf( "The number of 0s and 1s in the input file (%d) does not evenly divide by the number of primary inputs (%d).\n",
740  Vec_IntSize(vPat), Gia_ManPiNum(p) );
741  Vec_IntFree( vPat );
742  return;
743  }
744  vPatOut = Gia_ManSimSimulateOne( p, vPat );
745  if ( Gia_ManSimWriteFile( pFileOut, vPatOut, Gia_ManPoNum(p) ) )
746  printf( "Output patterns are written into file \"%s\".\n", pFileOut );
747  Vec_IntFree( vPat );
748  Vec_IntFree( vPatOut );
749 }
750 
751 ////////////////////////////////////////////////////////////////////////
752 /// END OF FILE ///
753 ////////////////////////////////////////////////////////////////////////
754 
755 
756 ABC_NAMESPACE_IMPL_END
757 
memset
char * memset()
Gia_ObjToLit
static int Gia_ObjToLit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:497
Gia_ObjChild0
static Gia_Obj_t * Gia_ObjChild0(Gia_Obj_t *pObj)
Definition: gia.h:457
Gia_ManSim_t_::vConsts
Vec_Int_t * vConsts
Definition: gia.h:257
Gia_ManSim_t_::vCis2Ids
Vec_Int_t * vCis2Ids
Definition: gia.h:256
Gia_ManSimulateNode
static void Gia_ManSimulateNode(Gia_ManSim_t *p, Gia_Obj_t *pObj)
Definition: giaSim.c:392
Gia_ParSim_t_::nWords
int nWords
Definition: gia.h:241
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition: giaCex.c:44
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Gia_ManSimSimulatePattern
void Gia_ManSimSimulatePattern(Gia_Man_t *p, char *pFileIn, char *pFileOut)
Definition: giaSim.c:731
Gia_Man_t_::nFront
int nFront
Definition: gia.h:119
Gia_ObjDiff1
static int Gia_ObjDiff1(Gia_Obj_t *pObj)
Definition: gia.h:450
Gia_ManSimInfoOne
static void Gia_ManSimInfoOne(Gia_ManSim_t *p, unsigned *pInfo)
Definition: giaSim.c:312
Gia_WordFindFirstBit
static int Gia_WordFindFirstBit(unsigned uWord)
Definition: gia.h:321
Gia_ObjValue
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Gia_ManSimulateCi
static void Gia_ManSimulateCi(Gia_ManSim_t *p, Gia_Obj_t *pObj, int iCi)
Definition: giaSim.c:348
Gia_ParSim_t_::RandSeed
int RandSeed
Definition: gia.h:243
Gia_Obj_t_::fMark1
unsigned fMark1
Definition: gia.h:84
Gia_ManSim_t_::nWords
int nWords
Definition: gia.h:255
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Gia_ManSimSimulateOne
Vec_Int_t * Gia_ManSimSimulateOne(Gia_Man_t *p, Vec_Int_t *vPat)
Definition: giaSim.c:703
Gia_ManSimInfoInit
void Gia_ManSimInfoInit(Gia_ManSim_t *p)
Definition: giaSim.c:429
Gia_ManSimSetDefaultParams
void Gia_ManSimSetDefaultParams(Gia_ParSim_t *p)
Definition: giaSim.c:164
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
nWords
int nWords
Definition: abcNpn.c:127
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Gia_Obj_t_
Definition: gia.h:75
Gia_ParSim_t_::fVerbose
int fVerbose
Definition: gia.h:246
Gia_ManSim_t_::pDataSimCis
unsigned * pDataSimCis
Definition: gia.h:260
Gia_ManCheckPos
static int Gia_ManCheckPos(Gia_ManSim_t *p, int *piPo, int *piPat)
Definition: giaSim.c:515
Gia_ManStopP
void Gia_ManStopP(Gia_Man_t **p)
Definition: giaMan.c:177
Gia_ManSimCollect_rec
void Gia_ManSimCollect_rec(Gia_Man_t *pGia, Gia_Obj_t *pObj, Vec_Int_t *vVec)
FUNCTION DEFINITIONS ///.
Definition: giaSim.c:54
Gia_ManSimInfoIsZero
static int Gia_ManSimInfoIsZero(Gia_ManSim_t *p, unsigned *pInfo)
Definition: giaSim.c:292
Gia_ManSimDelete
void Gia_ManSimDelete(Gia_ManSim_t *p)
Definition: giaSim.c:188
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
Gia_ObjChild1
static Gia_Obj_t * Gia_ObjChild1(Gia_Obj_t *pObj)
Definition: gia.h:458
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Gia_SimDataCo
static unsigned * Gia_SimDataCo(Gia_ManSim_t *p, int i)
Definition: giaSim.c:32
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Gia_ManSimInfoTransfer
void Gia_ManSimInfoTransfer(Gia_ManSim_t *p)
Definition: giaSim.c:452
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Gia_ManSimulateCo
static void Gia_ManSimulateCo(Gia_ManSim_t *p, int iCo, Gia_Obj_t *pObj)
Definition: giaSim.c:368
Gia_ManGenerateCounter
Abc_Cex_t * Gia_ManGenerateCounter(Gia_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t *vCis2Ids)
Definition: giaSim.c:542
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ParSim_t_::fCheckMiter
int fCheckMiter
Definition: gia.h:245
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
Gia_ManSimCreate
Gia_ManSim_t * Gia_ManSimCreate(Gia_Man_t *pAig, Gia_ParSim_t *pPars)
Definition: giaSim.c:210
Gia_ManSim_t_::pAig
Gia_Man_t * pAig
Definition: gia.h:253
Gia_ParSim_t_
Definition: gia.h:238
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_SimDataCiExt
unsigned * Gia_SimDataCiExt(Gia_ManSim_t *p, int i)
Definition: giaSim.c:35
Gia_ManSimCollect
void Gia_ManSimCollect(Gia_Man_t *pGia, Gia_Obj_t *pObj, Vec_Int_t *vVec)
Definition: giaSim.c:75
Gia_ManFront
Gia_Man_t * Gia_ManFront(Gia_Man_t *p)
Definition: giaFront.c:147
Gia_ManSim_t_::pDataSimCos
unsigned * pDataSimCos
Definition: gia.h:261
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Gia_ManSimInfoRandom
static void Gia_ManSimInfoRandom(Gia_ManSim_t *p, unsigned *pInfo)
Definition: giaSim.c:256
Gia_ManSim_t_::pDataSim
unsigned * pDataSim
Definition: gia.h:259
Gia_ManSimInfoZero
static void Gia_ManSimInfoZero(Gia_ManSim_t *p, unsigned *pInfo)
Definition: giaSim.c:274
Gia_ObjIsAndOrConst0
static int Gia_ObjIsAndOrConst0(Gia_Obj_t *pObj)
Definition: gia.h:419
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Vec_IntUniqify
static int Vec_IntUniqify(Vec_Int_t *p)
Definition: vecInt.h:1314
Gia_ParSim_t_::nIters
int nIters
Definition: gia.h:242
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Counter
static int Counter
Definition: extraBddMisc.c:1877
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Gia_ObjDiff0
static int Gia_ObjDiff0(Gia_Obj_t *pObj)
Definition: gia.h:449
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Gia_Man_t_::vCis
Vec_Int_t * vCis
Definition: gia.h:108
Gia_ManSim_t_::pPars
Gia_ParSim_t * pPars
Definition: gia.h:254
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_ManSim_t_
Definition: gia.h:251
Gia_ManSimWriteFile
int Gia_ManSimWriteFile(char *pFileOut, Vec_Int_t *vPat, int nOuts)
Definition: giaSim.c:684
Gia_IsComplement
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_SimDataExt
unsigned * Gia_SimDataExt(Gia_ManSim_t *p, int i)
Definition: giaSim.c:34
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
GIA_NONE
#define GIA_NONE
INCLUDES ///.
Definition: gia.h:44
Gia_ManResetRandom
void Gia_ManResetRandom(Gia_ParSim_t *pPars)
Definition: giaSim.c:579
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Gia_ManSimulateRound
void Gia_ManSimulateRound(Gia_ManSim_t *p)
Definition: giaSim.c:475
Gia_ObjFaninId0p
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Gia_ManSimInfoCopy
static void Gia_ManSimInfoCopy(Gia_ManSim_t *p, unsigned *pInfo, unsigned *pInfo0)
Definition: giaSim.c:330
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Gia_SimData
static ABC_NAMESPACE_IMPL_START unsigned * Gia_SimData(Gia_ManSim_t *p, int i)
DECLARATIONS ///.
Definition: giaSim.c:30
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
assert
#define assert(ex)
Definition: util_old.h:213
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
Gia_ParSim_t_::iOutFail
int iOutFail
Definition: gia.h:247
Gia_ManSimDeriveResets
Vec_Int_t * Gia_ManSimDeriveResets(Gia_Man_t *pGia)
Definition: giaSim.c:93
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_SimDataCi
static unsigned * Gia_SimDataCi(Gia_ManSim_t *p, int i)
Definition: giaSim.c:31
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Gia_ManSimSimulateEquiv
int Gia_ManSimSimulateEquiv(Gia_Man_t *pAig, Gia_ParSim_t *pPars)
Definition: giaSim2.c:638
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_SimDataCoExt
unsigned * Gia_SimDataCoExt(Gia_ManSim_t *p, int i)
Definition: giaSim.c:36
Gia_ManSimSimulate
int Gia_ManSimSimulate(Gia_Man_t *pAig, Gia_ParSim_t *pPars)
Definition: giaSim.c:598
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ObjIsPi
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_Man_t_::pCexSeq
Abc_Cex_t * pCexSeq
Definition: gia.h:136
Gia_ManSimReadFile
Vec_Int_t * Gia_ManSimReadFile(char *pFileIn)
Definition: giaSim.c:667
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Gia_ParSim_t_::TimeLimit
int TimeLimit
Definition: gia.h:244