abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraSim.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [fraSim.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [New FRAIG package.]
8 
9  Synopsis []
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 30, 2007.]
16 
17  Revision [$Id: fraSim.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "fra.h"
22 #include "aig/saig/saig.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37  Synopsis [Computes hash value of the node using its simulation info.]
38 
39  Description []
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize )
47 {
48  Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
49  static int s_FPrimes[128] = {
50  1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
51  1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
52  2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
53  2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
54  3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
55  3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
56  4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
57  4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
58  5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
59  6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
60  6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
61  7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
62  8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
63  };
64  unsigned * pSims;
65  unsigned uHash;
66  int i;
67 // assert( p->pSml->nWordsTotal <= 128 );
68  uHash = 0;
69  pSims = Fra_ObjSim(p->pSml, pObj->Id);
70  for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
71  uHash ^= pSims[i] * s_FPrimes[i & 0x7F];
72  return uHash % nTableSize;
73 }
74 
75 /**Function*************************************************************
76 
77  Synopsis [Returns 1 if simulation info is composed of all zeros.]
78 
79  Description []
80 
81  SideEffects []
82 
83  SeeAlso []
84 
85 ***********************************************************************/
86 int Fra_SmlNodeIsConst( Aig_Obj_t * pObj )
87 {
88  Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
89  unsigned * pSims;
90  int i;
91  pSims = Fra_ObjSim(p->pSml, pObj->Id);
92  for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
93  if ( pSims[i] )
94  return 0;
95  return 1;
96 }
97 
98 /**Function*************************************************************
99 
100  Synopsis [Returns 1 if simulation infos are equal.]
101 
102  Description []
103 
104  SideEffects []
105 
106  SeeAlso []
107 
108 ***********************************************************************/
109 int Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
110 {
111  Fra_Man_t * p = (Fra_Man_t *)pObj0->pData;
112  unsigned * pSims0, * pSims1;
113  int i;
114  pSims0 = Fra_ObjSim(p->pSml, pObj0->Id);
115  pSims1 = Fra_ObjSim(p->pSml, pObj1->Id);
116  for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
117  if ( pSims0[i] != pSims1[i] )
118  return 0;
119  return 1;
120 }
121 
122 /**Function*************************************************************
123 
124  Synopsis [Counts the number of 1s in the XOR of simulation data.]
125 
126  Description []
127 
128  SideEffects []
129 
130  SeeAlso []
131 
132 ***********************************************************************/
133 int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right )
134 {
135  unsigned * pSimL, * pSimR;
136  int k, Counter = 0;
137  pSimL = Fra_ObjSim( p, Left );
138  pSimR = Fra_ObjSim( p, Right );
139  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
140  Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
141  return Counter;
142 }
143 
144 /**Function*************************************************************
145 
146  Synopsis [Returns 1 if simulation info is composed of all zeros.]
147 
148  Description []
149 
150  SideEffects []
151 
152  SeeAlso []
153 
154 ***********************************************************************/
155 int Fra_SmlNodeIsZero( Fra_Sml_t * p, Aig_Obj_t * pObj )
156 {
157  unsigned * pSims;
158  int i;
159  pSims = Fra_ObjSim(p, pObj->Id);
160  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
161  if ( pSims[i] )
162  return 0;
163  return 1;
164 }
165 
166 /**Function*************************************************************
167 
168  Synopsis [Counts the number of one's in the patten of the output.]
169 
170  Description []
171 
172  SideEffects []
173 
174  SeeAlso []
175 
176 ***********************************************************************/
177 int Fra_SmlNodeCountOnes( Fra_Sml_t * p, Aig_Obj_t * pObj )
178 {
179  unsigned * pSims;
180  int i, Counter = 0;
181  pSims = Fra_ObjSim(p, pObj->Id);
182  for ( i = 0; i < p->nWordsTotal; i++ )
183  Counter += Aig_WordCountOnes( pSims[i] );
184  return Counter;
185 }
186 
187 
188 
189 /**Function*************************************************************
190 
191  Synopsis [Generated const 0 pattern.]
192 
193  Description []
194 
195  SideEffects []
196 
197  SeeAlso []
198 
199 ***********************************************************************/
200 void Fra_SmlSavePattern0( Fra_Man_t * p, int fInit )
201 {
202  memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
203 }
204 
205 /**Function*************************************************************
206 
207  Synopsis [[Generated const 1 pattern.]
208 
209  Description []
210 
211  SideEffects []
212 
213  SeeAlso []
214 
215 ***********************************************************************/
216 void Fra_SmlSavePattern1( Fra_Man_t * p, int fInit )
217 {
218  Aig_Obj_t * pObj;
219  int i, k, nTruePis;
220  memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
221  if ( !fInit )
222  return;
223  // clear the state bits to correspond to all-0 initial state
224  nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
225  k = 0;
226  Aig_ManForEachLoSeq( p->pManAig, pObj, i )
227  Abc_InfoXorBit( p->pPatWords, nTruePis * p->nFramesAll + k++ );
228 }
229 
230 /**Function*************************************************************
231 
232  Synopsis [Copy pattern from the solver into the internal storage.]
233 
234  Description []
235 
236  SideEffects []
237 
238  SeeAlso []
239 
240 ***********************************************************************/
241 void Fra_SmlSavePattern( Fra_Man_t * p )
242 {
243  Aig_Obj_t * pObj;
244  int i;
245  memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
246  Aig_ManForEachCi( p->pManFraig, pObj, i )
247 // if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
248  if ( sat_solver_var_value(p->pSat, Fra_ObjSatNum(pObj)) )
249  Abc_InfoSetBit( p->pPatWords, i );
250 
251  if ( p->vCex )
252  {
253  Vec_IntClear( p->vCex );
254  for ( i = 0; i < Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
255  Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) );
256  for ( i = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManCiNum(p->pManFraig); i++ )
257  Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) );
258  }
259 
260 /*
261  printf( "Pattern: " );
262  Aig_ManForEachCi( p->pManFraig, pObj, i )
263  printf( "%d", Abc_InfoHasBit( p->pPatWords, i ) );
264  printf( "\n" );
265 */
266 }
267 
268 
269 
270 /**Function*************************************************************
271 
272  Synopsis [Creates the counter-example from the successful pattern.]
273 
274  Description []
275 
276  SideEffects []
277 
278  SeeAlso []
279 
280 ***********************************************************************/
281 void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObjPo )
282 {
283  Aig_Obj_t * pFanin, * pObjPi;
284  unsigned * pSims;
285  int i, k, BestPat, * pModel;
286  // find the word of the pattern
287  pFanin = Aig_ObjFanin0(pObjPo);
288  pSims = Fra_ObjSim(p->pSml, pFanin->Id);
289  for ( i = 0; i < p->pSml->nWordsTotal; i++ )
290  if ( pSims[i] )
291  break;
292  assert( i < p->pSml->nWordsTotal );
293  // find the bit of the pattern
294  for ( k = 0; k < 32; k++ )
295  if ( pSims[i] & (1 << k) )
296  break;
297  assert( k < 32 );
298  // determine the best pattern
299  BestPat = i * 32 + k;
300  // fill in the counter-example data
301  pModel = ABC_ALLOC( int, Aig_ManCiNum(p->pManFraig)+1 );
302  Aig_ManForEachCi( p->pManAig, pObjPi, i )
303  {
304  pModel[i] = Abc_InfoHasBit(Fra_ObjSim(p->pSml, pObjPi->Id), BestPat);
305 // printf( "%d", pModel[i] );
306  }
307  pModel[Aig_ManCiNum(p->pManAig)] = pObjPo->Id;
308 // printf( "\n" );
309  // set the model
310  assert( p->pManFraig->pData == NULL );
311  p->pManFraig->pData = pModel;
312  return;
313 }
314 
315 /**Function*************************************************************
316 
317  Synopsis [Returns 1 if the one of the output is already non-constant 0.]
318 
319  Description []
320 
321  SideEffects []
322 
323  SeeAlso []
324 
325 ***********************************************************************/
326 int Fra_SmlCheckOutput( Fra_Man_t * p )
327 {
328  Aig_Obj_t * pObj;
329  int i;
330  // make sure the reference simulation pattern does not detect the bug
331  pObj = Aig_ManCo( p->pManAig, 0 );
332  assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) );
333  Aig_ManForEachCo( p->pManAig, pObj, i )
334  {
335  if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) )
336  {
337  // create the counter-example from this pattern
338  Fra_SmlCheckOutputSavePattern( p, pObj );
339  return 1;
340  }
341  }
342  return 0;
343 }
344 
345 
346 
347 /**Function*************************************************************
348 
349  Synopsis [Assigns random patterns to the PI node.]
350 
351  Description []
352 
353  SideEffects []
354 
355  SeeAlso []
356 
357 ***********************************************************************/
358 void Fra_SmlAssignRandom( Fra_Sml_t * p, Aig_Obj_t * pObj )
359 {
360  unsigned * pSims;
361  int i;
362  assert( Aig_ObjIsCi(pObj) );
363  pSims = Fra_ObjSim( p, pObj->Id );
364  for ( i = 0; i < p->nWordsTotal; i++ )
365  pSims[i] = Fra_ObjRandomSim();
366 }
367 
368 /**Function*************************************************************
369 
370  Synopsis [Assigns constant patterns to the PI node.]
371 
372  Description []
373 
374  SideEffects []
375 
376  SeeAlso []
377 
378 ***********************************************************************/
379 void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
380 {
381  unsigned * pSims;
382  int i;
383  assert( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) );
384  pSims = Fra_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
385  for ( i = 0; i < p->nWordsFrame; i++ )
386  pSims[i] = fConst1? ~(unsigned)0 : 0;
387 }
388 
389 /**Function*************************************************************
390 
391  Synopsis [Assings random simulation info for the PIs.]
392 
393  Description []
394 
395  SideEffects []
396 
397  SeeAlso []
398 
399 ***********************************************************************/
400 void Fra_SmlInitialize( Fra_Sml_t * p, int fInit )
401 {
402  Aig_Obj_t * pObj;
403  int i;
404  if ( fInit )
405  {
406  assert( Aig_ManRegNum(p->pAig) > 0 );
407  assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
408  // assign random info for primary inputs
409  Aig_ManForEachPiSeq( p->pAig, pObj, i )
410  Fra_SmlAssignRandom( p, pObj );
411  // assign the initial state for the latches
412  Aig_ManForEachLoSeq( p->pAig, pObj, i )
413  Fra_SmlAssignConst( p, pObj, 0, 0 );
414  }
415  else
416  {
417  Aig_ManForEachCi( p->pAig, pObj, i )
418  Fra_SmlAssignRandom( p, pObj );
419  }
420 }
421 
422 /**Function*************************************************************
423 
424  Synopsis [Assings distance-1 simulation info for the PIs.]
425 
426  Description []
427 
428  SideEffects []
429 
430  SeeAlso []
431 
432 ***********************************************************************/
433 void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
434 {
435  Aig_Obj_t * pObj;
436  int f, i, k, Limit, nTruePis;
437  assert( p->nFrames > 0 );
438  if ( p->nFrames == 1 )
439  {
440  // copy the PI info
441  Aig_ManForEachCi( p->pAig, pObj, i )
442  Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
443  // flip one bit
444  Limit = Abc_MinInt( Aig_ManCiNum(p->pAig), p->nWordsTotal * 32 - 1 );
445  for ( i = 0; i < Limit; i++ )
446  Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManCi(p->pAig,i)->Id ), i+1 );
447  }
448  else
449  {
450  int fUseDist1 = 0;
451 
452  // copy the PI info for each frame
453  nTruePis = Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig);
454  for ( f = 0; f < p->nFrames; f++ )
455  Aig_ManForEachPiSeq( p->pAig, pObj, i )
456  Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f );
457  // copy the latch info
458  k = 0;
459  Aig_ManForEachLoSeq( p->pAig, pObj, i )
460  Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
461 // assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManCiNum(p->pManFraig) );
462 
463  // flip one bit of the last frame
464  if ( fUseDist1 ) //&& p->nFrames == 2 )
465  {
466  Limit = Abc_MinInt( nTruePis, p->nWordsFrame * 32 - 1 );
467  for ( i = 0; i < Limit; i++ )
468  Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
469  }
470  }
471 }
472 
473 
474 /**Function*************************************************************
475 
476  Synopsis [Simulates one node.]
477 
478  Description []
479 
480  SideEffects []
481 
482  SeeAlso []
483 
484 ***********************************************************************/
485 void Fra_SmlNodeSimulate( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
486 {
487  unsigned * pSims, * pSims0, * pSims1;
488  int fCompl, fCompl0, fCompl1, i;
489  assert( !Aig_IsComplement(pObj) );
490  assert( Aig_ObjIsNode(pObj) );
491  assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
492  // get hold of the simulation information
493  pSims = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
494  pSims0 = Fra_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
495  pSims1 = Fra_ObjSim(p, Aig_ObjFanin1(pObj)->Id) + p->nWordsFrame * iFrame;
496  // get complemented attributes of the children using their random info
497  fCompl = pObj->fPhase;
498  fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
499  fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj));
500  // simulate
501  if ( fCompl0 && fCompl1 )
502  {
503  if ( fCompl )
504  for ( i = 0; i < p->nWordsFrame; i++ )
505  pSims[i] = (pSims0[i] | pSims1[i]);
506  else
507  for ( i = 0; i < p->nWordsFrame; i++ )
508  pSims[i] = ~(pSims0[i] | pSims1[i]);
509  }
510  else if ( fCompl0 && !fCompl1 )
511  {
512  if ( fCompl )
513  for ( i = 0; i < p->nWordsFrame; i++ )
514  pSims[i] = (pSims0[i] | ~pSims1[i]);
515  else
516  for ( i = 0; i < p->nWordsFrame; i++ )
517  pSims[i] = (~pSims0[i] & pSims1[i]);
518  }
519  else if ( !fCompl0 && fCompl1 )
520  {
521  if ( fCompl )
522  for ( i = 0; i < p->nWordsFrame; i++ )
523  pSims[i] = (~pSims0[i] | pSims1[i]);
524  else
525  for ( i = 0; i < p->nWordsFrame; i++ )
526  pSims[i] = (pSims0[i] & ~pSims1[i]);
527  }
528  else // if ( !fCompl0 && !fCompl1 )
529  {
530  if ( fCompl )
531  for ( i = 0; i < p->nWordsFrame; i++ )
532  pSims[i] = ~(pSims0[i] & pSims1[i]);
533  else
534  for ( i = 0; i < p->nWordsFrame; i++ )
535  pSims[i] = (pSims0[i] & pSims1[i]);
536  }
537 }
538 
539 /**Function*************************************************************
540 
541  Synopsis [Simulates one node.]
542 
543  Description []
544 
545  SideEffects []
546 
547  SeeAlso []
548 
549 ***********************************************************************/
550 int Fra_SmlNodesCompareInFrame( Fra_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 )
551 {
552  unsigned * pSims0, * pSims1;
553  int i;
554  assert( !Aig_IsComplement(pObj0) );
555  assert( !Aig_IsComplement(pObj1) );
556  assert( iFrame0 == 0 || p->nWordsFrame < p->nWordsTotal );
557  assert( iFrame1 == 0 || p->nWordsFrame < p->nWordsTotal );
558  // get hold of the simulation information
559  pSims0 = Fra_ObjSim(p, pObj0->Id) + p->nWordsFrame * iFrame0;
560  pSims1 = Fra_ObjSim(p, pObj1->Id) + p->nWordsFrame * iFrame1;
561  // compare
562  for ( i = 0; i < p->nWordsFrame; i++ )
563  if ( pSims0[i] != pSims1[i] )
564  return 0;
565  return 1;
566 }
567 
568 /**Function*************************************************************
569 
570  Synopsis [Simulates one node.]
571 
572  Description []
573 
574  SideEffects []
575 
576  SeeAlso []
577 
578 ***********************************************************************/
579 void Fra_SmlNodeCopyFanin( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
580 {
581  unsigned * pSims, * pSims0;
582  int fCompl, fCompl0, i;
583  assert( !Aig_IsComplement(pObj) );
584  assert( Aig_ObjIsCo(pObj) );
585  assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
586  // get hold of the simulation information
587  pSims = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
588  pSims0 = Fra_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
589  // get complemented attributes of the children using their random info
590  fCompl = pObj->fPhase;
591  fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
592  // copy information as it is
593 // if ( Aig_ObjFaninC0(pObj) )
594  if ( fCompl0 )
595  for ( i = 0; i < p->nWordsFrame; i++ )
596  pSims[i] = ~pSims0[i];
597  else
598  for ( i = 0; i < p->nWordsFrame; i++ )
599  pSims[i] = pSims0[i];
600 }
601 
602 /**Function*************************************************************
603 
604  Synopsis [Simulates one node.]
605 
606  Description []
607 
608  SideEffects []
609 
610  SeeAlso []
611 
612 ***********************************************************************/
613 void Fra_SmlNodeTransferNext( Fra_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame )
614 {
615  unsigned * pSims0, * pSims1;
616  int i;
617  assert( !Aig_IsComplement(pOut) );
618  assert( !Aig_IsComplement(pIn) );
619  assert( Aig_ObjIsCo(pOut) );
620  assert( Aig_ObjIsCi(pIn) );
621  assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
622  // get hold of the simulation information
623  pSims0 = Fra_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame;
624  pSims1 = Fra_ObjSim(p, pIn->Id) + p->nWordsFrame * (iFrame+1);
625  // copy information as it is
626  for ( i = 0; i < p->nWordsFrame; i++ )
627  pSims1[i] = pSims0[i];
628 }
629 
630 
631 /**Function*************************************************************
632 
633  Synopsis [Check if any of the POs becomes non-constant.]
634 
635  Description []
636 
637  SideEffects []
638 
639  SeeAlso []
640 
641 ***********************************************************************/
642 int Fra_SmlCheckNonConstOutputs( Fra_Sml_t * p )
643 {
644  Aig_Obj_t * pObj;
645  int i;
646  Aig_ManForEachPoSeq( p->pAig, pObj, i )
647  if ( !Fra_SmlNodeIsZero(p, pObj) )
648  return 1;
649  return 0;
650 }
651 
652 /**Function*************************************************************
653 
654  Synopsis [Simulates AIG manager.]
655 
656  Description [Assumes that the PI simulation info is attached.]
657 
658  SideEffects []
659 
660  SeeAlso []
661 
662 ***********************************************************************/
663 void Fra_SmlSimulateOne( Fra_Sml_t * p )
664 {
665  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
666  int f, i;
667  abctime clk;
668 clk = Abc_Clock();
669  for ( f = 0; f < p->nFrames; f++ )
670  {
671  // simulate the nodes
672  Aig_ManForEachNode( p->pAig, pObj, i )
673  Fra_SmlNodeSimulate( p, pObj, f );
674  // copy simulation info into outputs
675  Aig_ManForEachPoSeq( p->pAig, pObj, i )
676  Fra_SmlNodeCopyFanin( p, pObj, f );
677  // quit if this is the last timeframe
678  if ( f == p->nFrames - 1 )
679  break;
680  // copy simulation info into outputs
681  Aig_ManForEachLiSeq( p->pAig, pObj, i )
682  Fra_SmlNodeCopyFanin( p, pObj, f );
683  // copy simulation info into the inputs
684  Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
685  Fra_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
686  }
687 p->timeSim += Abc_Clock() - clk;
688 p->nSimRounds++;
689 }
690 
691 
692 /**Function*************************************************************
693 
694  Synopsis [Resimulates fraiging manager after finding a counter-example.]
695 
696  Description []
697 
698  SideEffects []
699 
700  SeeAlso []
701 
702 ***********************************************************************/
703 void Fra_SmlResimulate( Fra_Man_t * p )
704 {
705  int nChanges;
706  abctime clk;
707  Fra_SmlAssignDist1( p->pSml, p->pPatWords );
708  Fra_SmlSimulateOne( p->pSml );
709 // if ( p->pPars->fPatScores )
710 // Fra_CleanPatScores( p );
711  if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
712  return;
713 clk = Abc_Clock();
714  nChanges = Fra_ClassesRefine( p->pCla );
715  nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
716  if ( p->pCla->vImps )
717  nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
718  if ( p->vOneHots )
719  nChanges += Fra_OneHotRefineUsingCex( p, p->vOneHots );
720 p->timeRef += Abc_Clock() - clk;
721  if ( !p->pPars->nFramesK && nChanges < 1 )
722  printf( "Error: A counter-example did not refine classes!\n" );
723 // assert( nChanges >= 1 );
724 //printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
725 }
726 
727 /**Function*************************************************************
728 
729  Synopsis [Performs simulation of the manager.]
730 
731  Description []
732 
733  SideEffects []
734 
735  SeeAlso []
736 
737 ***********************************************************************/
738 void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
739 {
740  int fVerbose = 0;
741  int nChanges, nClasses;
742  abctime clk;
743  assert( !fInit || Aig_ManRegNum(p->pManAig) );
744  // start the classes
745  Fra_SmlInitialize( p->pSml, fInit );
746  Fra_SmlSimulateOne( p->pSml );
747  if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
748  return;
749  Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 );
750 // Fra_ClassesPrint( p->pCla, 0 );
751 if ( fVerbose )
752 printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
753 
754 //return;
755 
756  // refine classes by walking 0/1 patterns
757  Fra_SmlSavePattern0( p, fInit );
758  Fra_SmlAssignDist1( p->pSml, p->pPatWords );
759  Fra_SmlSimulateOne( p->pSml );
760  if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
761  return;
762 clk = Abc_Clock();
763  nChanges = Fra_ClassesRefine( p->pCla );
764  nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
765 p->timeRef += Abc_Clock() - clk;
766 if ( fVerbose )
767 printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
768  Fra_SmlSavePattern1( p, fInit );
769  Fra_SmlAssignDist1( p->pSml, p->pPatWords );
770  Fra_SmlSimulateOne( p->pSml );
771  if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
772  return;
773 clk = Abc_Clock();
774  nChanges = Fra_ClassesRefine( p->pCla );
775  nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
776 p->timeRef += Abc_Clock() - clk;
777 
778 if ( fVerbose )
779 printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
780  // refine classes by random simulation
781  do {
782  Fra_SmlInitialize( p->pSml, fInit );
783  Fra_SmlSimulateOne( p->pSml );
784  nClasses = Vec_PtrSize(p->pCla->vClasses);
785  if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
786  return;
787 clk = Abc_Clock();
788  nChanges = Fra_ClassesRefine( p->pCla );
789  nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
790 p->timeRef += Abc_Clock() - clk;
791 if ( fVerbose )
792 printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
793  } while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
794 
795 // if ( p->pPars->fVerbose )
796 // printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n",
797 // Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
798 // Fra_ClassesPrint( p->pCla, 0 );
799 }
800 
801 
802 /**Function*************************************************************
803 
804  Synopsis [Allocates simulation manager.]
805 
806  Description []
807 
808  SideEffects []
809 
810  SeeAlso []
811 
812 ***********************************************************************/
813 Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
814 {
815  Fra_Sml_t * p;
816  p = (Fra_Sml_t *)ABC_ALLOC( char, sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
817  memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
818  p->pAig = pAig;
819  p->nPref = nPref;
820  p->nFrames = nPref + nFrames;
821  p->nWordsFrame = nWordsFrame;
822  p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
823  p->nWordsPref = nPref * nWordsFrame;
824  // constant 1 is initialized to 0 because we store values modulus phase (pObj->fPhase)
825  return p;
826 }
827 
828 /**Function*************************************************************
829 
830  Synopsis [Deallocates simulation manager.]
831 
832  Description []
833 
834  SideEffects []
835 
836  SeeAlso []
837 
838 ***********************************************************************/
839 void Fra_SmlStop( Fra_Sml_t * p )
840 {
841  ABC_FREE( p );
842 }
843 
844 
845 /**Function*************************************************************
846 
847  Synopsis [Performs simulation of the uninitialized circuit.]
848 
849  Description []
850 
851  SideEffects []
852 
853  SeeAlso []
854 
855 ***********************************************************************/
856 Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords, int fCheckMiter )
857 {
858  Fra_Sml_t * p;
859  p = Fra_SmlStart( pAig, 0, 1, nWords );
860  Fra_SmlInitialize( p, 0 );
861  Fra_SmlSimulateOne( p );
862  if ( fCheckMiter )
863  p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
864  return p;
865 }
866 
867 /**Function*************************************************************
868 
869  Synopsis [Reads simulation patterns from file.]
870 
871  Description [Each pattern contains the given number (nInputs) of binary digits.
872  No other symbols (except spaces and line endings) are allowed in the file.]
873 
874  SideEffects []
875 
876  SeeAlso []
877 
878 ***********************************************************************/
879 Vec_Str_t * Fra_SmlSimulateReadFile( char * pFileName )
880 {
881  Vec_Str_t * vRes;
882  FILE * pFile;
883  int c;
884  pFile = fopen( pFileName, "rb" );
885  if ( pFile == NULL )
886  {
887  printf( "Cannot open file \"%s\" with simulation patterns.\n", pFileName );
888  return NULL;
889  }
890  vRes = Vec_StrAlloc( 1000 );
891  while ( (c = fgetc(pFile)) != EOF )
892  {
893  if ( c == '0' || c == '1' )
894  Vec_StrPush( vRes, (char)(c - '0') );
895  else if ( c != ' ' && c != '\r' && c != '\n' && c != '\t' )
896  {
897  printf( "File \"%s\" contains symbol (%c) other than \'0\' or \'1\'.\n", pFileName, (char)c );
898  Vec_StrFreeP( &vRes );
899  break;
900  }
901  }
902  fclose( pFile );
903  return vRes;
904 }
905 
906 /**Function*************************************************************
907 
908  Synopsis [Assigns simulation patters derived from file.]
909 
910  Description []
911 
912  SideEffects []
913 
914  SeeAlso []
915 
916 ***********************************************************************/
917 void Fra_SmlInitializeGiven( Fra_Sml_t * p, Vec_Str_t * vSimInfo )
918 {
919  Aig_Obj_t * pObj;
920  unsigned * pSims;
921  int i, k, nPats = Vec_StrSize(vSimInfo) / Aig_ManCiNum(p->pAig);
922  int nPatsPadded = p->nWordsTotal * 32;
923  assert( Aig_ManRegNum(p->pAig) == 0 );
924  assert( Vec_StrSize(vSimInfo) % Aig_ManCiNum(p->pAig) == 0 );
925  assert( nPats <= nPatsPadded );
926  Aig_ManForEachCi( p->pAig, pObj, i )
927  {
928  pSims = Fra_ObjSim( p, pObj->Id );
929  // clean data
930  for ( k = 0; k < p->nWordsTotal; k++ )
931  pSims[k] = 0;
932  // load patterns
933  for ( k = 0; k < nPats; k++ )
934  if ( Vec_StrEntry(vSimInfo, k * Aig_ManCiNum(p->pAig) + i) )
935  Abc_InfoSetBit( pSims, k );
936  // pad the remaining bits with the value of the last pattern
937  for ( ; k < nPatsPadded; k++ )
938  if ( Vec_StrEntry(vSimInfo, (nPats-1) * Aig_ManCiNum(p->pAig) + i) )
939  Abc_InfoSetBit( pSims, k );
940  }
941 }
942 
943 /**Function*************************************************************
944 
945  Synopsis [Prints output values.]
946 
947  Description []
948 
949  SideEffects []
950 
951  SeeAlso []
952 
953 ***********************************************************************/
954 void Fra_SmlPrintOutputs( Fra_Sml_t * p, int nPatterns )
955 {
956  Aig_Obj_t * pObj;
957  unsigned * pSims;
958  int i, k;
959  for ( k = 0; k < nPatterns; k++ )
960  {
961  Aig_ManForEachCo( p->pAig, pObj, i )
962  {
963  pSims = Fra_ObjSim( p, pObj->Id );
964  printf( "%d", Abc_InfoHasBit( pSims, k ) );
965  }
966  printf( "\n" ); ;
967  }
968 }
969 
970 /**Function*************************************************************
971 
972  Synopsis [Assigns simulation patters derived from file.]
973 
974  Description []
975 
976  SideEffects []
977 
978  SeeAlso []
979 
980 ***********************************************************************/
981 Fra_Sml_t * Fra_SmlSimulateCombGiven( Aig_Man_t * pAig, char * pFileName, int fCheckMiter, int fVerbose )
982 {
983  Vec_Str_t * vSimInfo;
984  Fra_Sml_t * p;
985  int nPatterns;
986  assert( Aig_ManRegNum(pAig) == 0 );
987  // read comb patterns from file
988  vSimInfo = Fra_SmlSimulateReadFile( pFileName );
989  if ( vSimInfo == NULL )
990  return NULL;
991  if ( Vec_StrSize(vSimInfo) % Aig_ManCiNum(pAig) != 0 )
992  {
993  printf( "File \"%s\": The number of binary digits (%d) is not divisible by the number of primary inputs (%d).\n",
994  pFileName, Vec_StrSize(vSimInfo), Aig_ManCiNum(pAig) );
995  Vec_StrFree( vSimInfo );
996  return NULL;
997  }
998  p = Fra_SmlStart( pAig, 0, 1, Abc_BitWordNum(Vec_StrSize(vSimInfo) / Aig_ManCiNum(pAig)) );
999  Fra_SmlInitializeGiven( p, vSimInfo );
1000  nPatterns = Vec_StrSize(vSimInfo) / Aig_ManCiNum(pAig);
1001  Vec_StrFree( vSimInfo );
1002  Fra_SmlSimulateOne( p );
1003  if ( fCheckMiter )
1004  p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
1005  if ( fVerbose )
1006  Fra_SmlPrintOutputs( p, nPatterns );
1007  return p;
1008 }
1009 
1010 /**Function*************************************************************
1011 
1012  Synopsis [Performs simulation of the initialized circuit.]
1013 
1014  Description []
1015 
1016  SideEffects []
1017 
1018  SeeAlso []
1019 
1020 ***********************************************************************/
1021 Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter )
1022 {
1023  Fra_Sml_t * p;
1024  p = Fra_SmlStart( pAig, nPref, nFrames, nWords );
1025  Fra_SmlInitialize( p, 1 );
1026  Fra_SmlSimulateOne( p );
1027  if ( fCheckMiter )
1028  p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
1029  return p;
1030 }
1031 
1032 /**Function*************************************************************
1033 
1034  Synopsis [Creates sequential counter-example from the simulation info.]
1035 
1036  Description []
1037 
1038  SideEffects []
1039 
1040  SeeAlso []
1041 
1042 ***********************************************************************/
1043 Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
1044 {
1045  Abc_Cex_t * pCex;
1046  Aig_Obj_t * pObj;
1047  unsigned * pSims;
1048  int iPo, iFrame, iBit, i, k;
1049 
1050  // make sure the simulation manager has it
1051  assert( p->fNonConstOut );
1052 
1053  // find the first output that failed
1054  iPo = -1;
1055  iBit = -1;
1056  iFrame = -1;
1057  Aig_ManForEachPoSeq( p->pAig, pObj, iPo )
1058  {
1059  if ( Fra_SmlNodeIsZero(p, pObj) )
1060  continue;
1061  pSims = Fra_ObjSim( p, pObj->Id );
1062  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
1063  if ( pSims[i] )
1064  {
1065  iFrame = i / p->nWordsFrame;
1066  iBit = 32 * (i % p->nWordsFrame) + Aig_WordFindFirstBit( pSims[i] );
1067  break;
1068  }
1069  break;
1070  }
1071  assert( iPo < Aig_ManCoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
1072  assert( iFrame < p->nFrames );
1073  assert( iBit < 32 * p->nWordsFrame );
1074 
1075  // allocate the counter example
1076  pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
1077  pCex->iPo = iPo;
1078  pCex->iFrame = iFrame;
1079 
1080  // copy the bit data
1081  Aig_ManForEachLoSeq( p->pAig, pObj, k )
1082  {
1083  pSims = Fra_ObjSim( p, pObj->Id );
1084  if ( Abc_InfoHasBit( pSims, iBit ) )
1085  Abc_InfoSetBit( pCex->pData, k );
1086  }
1087  for ( i = 0; i <= iFrame; i++ )
1088  {
1089  Aig_ManForEachPiSeq( p->pAig, pObj, k )
1090  {
1091  pSims = Fra_ObjSim( p, pObj->Id );
1092  if ( Abc_InfoHasBit( pSims, 32 * p->nWordsFrame * i + iBit ) )
1093  Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * i + k );
1094  }
1095  }
1096  // verify the counter example
1097  if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
1098  {
1099  printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
1100  Abc_CexFree( pCex );
1101  pCex = NULL;
1102  }
1103  return pCex;
1104 }
1105 
1106 /**Function*************************************************************
1107 
1108  Synopsis [Generates seq counter-example from the combinational one.]
1109 
1110  Description []
1111 
1112  SideEffects []
1113 
1114  SeeAlso []
1115 
1116 ***********************************************************************/
1117 Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel )
1118 {
1119  Abc_Cex_t * pCex;
1120  Aig_Obj_t * pObj;
1121  int i, nFrames, nTruePis, nTruePos, iPo, iFrame;
1122  // get the number of frames
1123  assert( Aig_ManRegNum(pAig) > 0 );
1124  assert( Aig_ManRegNum(pFrames) == 0 );
1125  nTruePis = Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig);
1126  nTruePos = Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig);
1127  nFrames = Aig_ManCiNum(pFrames) / nTruePis;
1128  assert( nTruePis * nFrames == Aig_ManCiNum(pFrames) );
1129  assert( nTruePos * nFrames == Aig_ManCoNum(pFrames) );
1130  // find the PO that failed
1131  iPo = -1;
1132  iFrame = -1;
1133  Aig_ManForEachCo( pFrames, pObj, i )
1134  if ( pObj->Id == pModel[Aig_ManCiNum(pFrames)] )
1135  {
1136  iPo = i % nTruePos;
1137  iFrame = i / nTruePos;
1138  break;
1139  }
1140  assert( iPo >= 0 );
1141  // allocate the counter example
1142  pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
1143  pCex->iPo = iPo;
1144  pCex->iFrame = iFrame;
1145 
1146  // copy the bit data
1147  for ( i = 0; i < Aig_ManCiNum(pFrames); i++ )
1148  {
1149  if ( pModel[i] )
1150  Abc_InfoSetBit( pCex->pData, pCex->nRegs + i );
1151  if ( pCex->nRegs + i == pCex->nBits - 1 )
1152  break;
1153  }
1154 
1155  // verify the counter example
1156  if ( !Saig_ManVerifyCex( pAig, pCex ) )
1157  {
1158  printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
1159  Abc_CexFree( pCex );
1160  pCex = NULL;
1161  }
1162  return pCex;
1163 
1164 }
1165 
1166 
1167 ////////////////////////////////////////////////////////////////////////
1168 /// END OF FILE ///
1169 ////////////////////////////////////////////////////////////////////////
1170 
1171 
1172 ABC_NAMESPACE_IMPL_END
1173 
memset
char * memset()
Fra_Sml_t_::fNonConstOut
int fNonConstOut
Definition: fra.h:179
Fra_SmlInitialize
void Fra_SmlInitialize(Fra_Sml_t *p, int fInit)
Definition: fraSim.c:400
Fra_ImpRefineUsingCex
int Fra_ImpRefineUsingCex(Fra_Man_t *p, Vec_Int_t *vImps)
Definition: fraImp.c:575
Fra_SmlNodeCountOnes
int Fra_SmlNodeCountOnes(Fra_Sml_t *p, Aig_Obj_t *pObj)
Definition: fraSim.c:177
Fra_ClassesRefine1
int Fra_ClassesRefine1(Fra_Cla_t *p, int fRefineNewClass, int *pSkipped)
Definition: fraClass.c:527
Fra_SmlSavePattern
void Fra_SmlSavePattern(Fra_Man_t *p)
Definition: fraSim.c:241
Fra_SmlNodeNotEquWeight
int Fra_SmlNodeNotEquWeight(Fra_Sml_t *p, int Left, int Right)
Definition: fraSim.c:133
Fra_SmlSimulate
void Fra_SmlSimulate(Fra_Man_t *p, int fInit)
Definition: fraSim.c:738
Fra_Sml_t_::nFrames
int nFrames
Definition: fra.h:175
Fra_SmlSimulateComb
Fra_Sml_t * Fra_SmlSimulateComb(Aig_Man_t *pAig, int nWords, int fCheckMiter)
Definition: fraSim.c:856
Fra_Man_t_::pManAig
Aig_Man_t * pManAig
Definition: fra.h:191
Fra_SmlAssignRandom
void Fra_SmlAssignRandom(Fra_Sml_t *p, Aig_Obj_t *pObj)
Definition: fraSim.c:358
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Fra_SmlNodeSimulate
void Fra_SmlNodeSimulate(Fra_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: fraSim.c:485
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fra_Sml_t_::pAig
Aig_Man_t * pAig
Definition: fra.h:173
Fra_SmlAssignConst
void Fra_SmlAssignConst(Fra_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame)
Definition: fraSim.c:379
Fra_Sml_t_::timeSim
int timeSim
Definition: fra.h:181
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
Fra_SmlNodesCompareInFrame
int Fra_SmlNodesCompareInFrame(Fra_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1, int iFrame0, int iFrame1)
Definition: fraSim.c:550
Fra_Man_t_::pCla
Fra_Cla_t * pCla
Definition: fra.h:198
Fra_Cla_t_::vClasses
Vec_Ptr_t * vClasses
Definition: fra.h:154
Saig_ManVerifyCex
int Saig_ManVerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:279
Fra_Man_t_::pPars
Fra_Par_t * pPars
Definition: fra.h:189
Fra_ClassesCountLits
int Fra_ClassesCountLits(Fra_Cla_t *p)
Definition: fraClass.c:164
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Fra_Man_t_::pSat
sat_solver * pSat
Definition: fra.h:210
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
Fra_SmlSimulateCombGiven
Fra_Sml_t * Fra_SmlSimulateCombGiven(Aig_Man_t *pAig, char *pFileName, int fCheckMiter, int fVerbose)
Definition: fraSim.c:981
Fra_Man_t_::pSml
Fra_Sml_t * pSml
Definition: fra.h:200
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Fra_Man_t_::vOneHots
Vec_Int_t * vOneHots
Definition: fra.h:208
Fra_SmlNodeIsConst
int Fra_SmlNodeIsConst(Aig_Obj_t *pObj)
Definition: fraSim.c:86
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Vec_StrAlloc
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
Fra_Sml_t_::nWordsTotal
int nWordsTotal
Definition: fra.h:177
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Vec_StrPush
static void Vec_StrPush(Vec_Str_t *p, char Entry)
Definition: vecStr.h:535
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Fra_SmlSimulateOne
void Fra_SmlSimulateOne(Fra_Sml_t *p)
Definition: fraSim.c:663
nWords
int nWords
Definition: abcNpn.c:127
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Fra_Man_t_::nFramesAll
int nFramesAll
Definition: fra.h:194
Fra_SmlInitializeGiven
void Fra_SmlInitializeGiven(Fra_Sml_t *p, Vec_Str_t *vSimInfo)
Definition: fraSim.c:917
Fra_SmlNodeHash
ABC_NAMESPACE_IMPL_START int Fra_SmlNodeHash(Aig_Obj_t *pObj, int nTableSize)
DECLARATIONS ///.
Definition: fraSim.c:46
Fra_ObjSim
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
Fra_Man_t_::pPatWords
unsigned * pPatWords
Definition: fra.h:205
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Fra_ClassesPrepare
void Fra_ClassesPrepare(Fra_Cla_t *p, int fLatchCorr, int nMaxLevs)
Definition: fraClass.c:276
Fra_SmlCopyCounterExample
Abc_Cex_t * Fra_SmlCopyCounterExample(Aig_Man_t *pAig, Aig_Man_t *pFrames, int *pModel)
Definition: fraSim.c:1117
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Fra_Man_t_::pManFraig
Aig_Man_t * pManFraig
Definition: fra.h:192
Fra_SmlCheckNonConstOutputs
int Fra_SmlCheckNonConstOutputs(Fra_Sml_t *p)
Definition: fraSim.c:642
Aig_WordCountOnes
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
Fra_Sml_t_
Definition: fra.h:171
Vec_StrEntry
static char Vec_StrEntry(Vec_Str_t *p, int i)
Definition: vecStr.h:336
Fra_SmlSimulateReadFile
Vec_Str_t * Fra_SmlSimulateReadFile(char *pFileName)
Definition: fraSim.c:879
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Fra_SmlGetCounterExample
Abc_Cex_t * Fra_SmlGetCounterExample(Fra_Sml_t *p)
Definition: fraSim.c:1043
Fra_ObjRandomSim
static unsigned Fra_ObjRandomSim()
Definition: fra.h:258
Vec_StrFree
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
Aig_ManForEachLiLoSeq
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition: aig.h:450
Fra_SmlCheckOutput
int Fra_SmlCheckOutput(Fra_Man_t *p)
Definition: fraSim.c:326
Aig_WordFindFirstBit
static int Aig_WordFindFirstBit(unsigned uWord)
Definition: aig.h:237
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Fra_Man_t_::vCex
Vec_Int_t * vCex
Definition: fra.h:206
Aig_ObjChild1
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Fra_SmlSimulateSeq
Fra_Sml_t * Fra_SmlSimulateSeq(Aig_Man_t *pAig, int nPref, int nFrames, int nWords, int fCheckMiter)
Definition: fraSim.c:1021
Fra_OneHotRefineUsingCex
int Fra_OneHotRefineUsingCex(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition: fraHot.c:266
Aig_ObjPhaseReal
static int Aig_ObjPhaseReal(Aig_Obj_t *pObj)
Definition: aig.h:299
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Fra_SmlCheckOutputSavePattern
void Fra_SmlCheckOutputSavePattern(Fra_Man_t *p, Aig_Obj_t *pObjPo)
Definition: fraSim.c:281
Counter
static int Counter
Definition: extraBddMisc.c:1877
Fra_Sml_t_::nWordsFrame
int nWordsFrame
Definition: fra.h:176
Fra_SmlResimulate
void Fra_SmlResimulate(Fra_Man_t *p)
Definition: fraSim.c:703
Fra_SmlNodeCopyFanin
void Fra_SmlNodeCopyFanin(Fra_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: fraSim.c:579
Fra_SmlNodesAreEqual
int Fra_SmlNodesAreEqual(Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition: fraSim.c:109
Fra_SmlPrintOutputs
void Fra_SmlPrintOutputs(Fra_Sml_t *p, int nPatterns)
Definition: fraSim.c:954
Fra_Man_t_::timeRef
abctime timeRef
Definition: fra.h:247
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Fra_SmlAssignDist1
void Fra_SmlAssignDist1(Fra_Sml_t *p, unsigned *pPat)
Definition: fraSim.c:433
Fra_Cla_t_::vImps
Vec_Int_t * vImps
Definition: fra.h:163
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Fra_Sml_t_::nSimRounds
int nSimRounds
Definition: fra.h:180
Vec_StrSize
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Vec_Str_t_
Definition: bblif.c:47
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Fra_ClassesRefine
int Fra_ClassesRefine(Fra_Cla_t *p)
Definition: fraClass.c:493
Fra_Man_t_::nPatWords
int nPatWords
Definition: fra.h:204
Aig_ManForEachLoSeq
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
Fra_Man_t_
Definition: fra.h:186
Fra_SmlStop
void Fra_SmlStop(Fra_Sml_t *p)
Definition: fraSim.c:839
Fra_ObjSatNum
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ManForEachLiSeq
#define Aig_ManForEachLiSeq(p, pObj, i)
Definition: aig.h:447
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Fra_SmlNodeTransferNext
void Fra_SmlNodeTransferNext(Fra_Sml_t *p, Aig_Obj_t *pOut, Aig_Obj_t *pIn, int iFrame)
Definition: fraSim.c:613
Fra_Sml_t_::nWordsPref
int nWordsPref
Definition: fra.h:178
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
Aig_ManForEachPoSeq
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition: aig.h:444
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Fra_SmlSavePattern1
void Fra_SmlSavePattern1(Fra_Man_t *p, int fInit)
Definition: fraSim.c:216
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Fra_SmlStart
Fra_Sml_t * Fra_SmlStart(Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
Definition: fraSim.c:813
Aig_ManForEachPiSeq
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition: aig.h:438
Vec_StrFreeP
static void Vec_StrFreeP(Vec_Str_t **p)
Definition: vecStr.h:233
Fra_SmlNodeIsZero
int Fra_SmlNodeIsZero(Fra_Sml_t *p, Aig_Obj_t *pObj)
Definition: fraSim.c:155
Fra_Sml_t_::nPref
int nPref
Definition: fra.h:174
Fra_SmlSavePattern0
void Fra_SmlSavePattern0(Fra_Man_t *p, int fInit)
Definition: fraSim.c:200