abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
sswSim.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [sswSim.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Inductive prover with constraints.]
8 
9  Synopsis [Sequential simulator used by the inductive prover.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - September 1, 2008.]
16 
17  Revision [$Id: sswSim.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sswInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 // simulation manager
31 struct Ssw_Sml_t_
32 {
33  Aig_Man_t * pAig; // the original AIG manager
34  int nPref; // the number of timeframes in the prefix
35  int nFrames; // the number of timeframes
36  int nWordsFrame; // the number of words in each timeframe
37  int nWordsTotal; // the total number of words at a node
38  int nWordsPref; // the number of word in the prefix
39  int fNonConstOut; // have seen a non-const-0 output during simulation
40  int nSimRounds; // statistics
41  abctime timeSim; // statistics
42  unsigned pData[0]; // simulation data for the nodes
43 };
44 
45 static inline unsigned * Ssw_ObjSim( Ssw_Sml_t * p, int Id ) { return p->pData + p->nWordsTotal * Id; }
46 static inline unsigned Ssw_ObjRandomSim() { return Aig_ManRandom(0); }
47 
48 ////////////////////////////////////////////////////////////////////////
49 /// FUNCTION DEFINITIONS ///
50 ////////////////////////////////////////////////////////////////////////
51 
52 /**Function*************************************************************
53 
54  Synopsis [Computes hash value of the node using its simulation info.]
55 
56  Description []
57 
58  SideEffects []
59 
60  SeeAlso []
61 
62 ***********************************************************************/
63 unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
64 {
65  static int s_SPrimes[128] = {
66  1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
67  1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
68  2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
69  2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
70  3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
71  3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
72  4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
73  4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
74  5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
75  6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
76  6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
77  7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
78  8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
79  };
80  unsigned * pSims;
81  unsigned uHash;
82  int i;
83 // assert( p->nWordsTotal <= 128 );
84  uHash = 0;
85  pSims = Ssw_ObjSim(p, pObj->Id);
86  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
87  uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
88  return uHash;
89 }
90 
91 /**Function*************************************************************
92 
93  Synopsis [Returns 1 if simulation info is composed of all zeros.]
94 
95  Description []
96 
97  SideEffects []
98 
99  SeeAlso []
100 
101 ***********************************************************************/
102 int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
103 {
104  unsigned * pSims;
105  int i;
106  pSims = Ssw_ObjSim(p, pObj->Id);
107  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
108  if ( pSims[i] )
109  return 0;
110  return 1;
111 }
112 
113 /**Function*************************************************************
114 
115  Synopsis [Returns 1 if simulation infos are equal.]
116 
117  Description []
118 
119  SideEffects []
120 
121  SeeAlso []
122 
123 ***********************************************************************/
124 int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
125 {
126  unsigned * pSims0, * pSims1;
127  int i;
128  pSims0 = Ssw_ObjSim(p, pObj0->Id);
129  pSims1 = Ssw_ObjSim(p, pObj1->Id);
130  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
131  if ( pSims0[i] != pSims1[i] )
132  return 0;
133  return 1;
134 }
135 
136 /**Function*************************************************************
137 
138  Synopsis [Returns 1 if the node appears to be constant 1 candidate.]
139 
140  Description []
141 
142  SideEffects []
143 
144  SeeAlso []
145 
146 ***********************************************************************/
147 int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj )
148 {
149  return pObj->fPhase == pObj->fMarkB;
150 }
151 
152 /**Function*************************************************************
153 
154  Synopsis [Returns 1 if the nodes appear equal.]
155 
156  Description []
157 
158  SideEffects []
159 
160  SeeAlso []
161 
162 ***********************************************************************/
163 int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
164 {
165  return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
166 }
167 
168 
169 /**Function*************************************************************
170 
171  Synopsis [Counts the number of 1s in the XOR of simulation data.]
172 
173  Description []
174 
175  SideEffects []
176 
177  SeeAlso []
178 
179 ***********************************************************************/
180 int Ssw_SmlNodeNotEquWeight( Ssw_Sml_t * p, int Left, int Right )
181 {
182  unsigned * pSimL, * pSimR;
183  int k, Counter = 0;
184  pSimL = Ssw_ObjSim( p, Left );
185  pSimR = Ssw_ObjSim( p, Right );
186  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
187  Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
188  return Counter;
189 }
190 
191 /**Function*************************************************************
192 
193  Synopsis [Checks implication.]
194 
195  Description []
196 
197  SideEffects []
198 
199  SeeAlso []
200 
201 ***********************************************************************/
202 int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand )
203 {
204  unsigned * pSimLi, * pSimLo, * pSimCand;
205  int k;
206  assert( pObjLo->fPhase == 0 );
207  // pObjLi->fPhase may be 1, but the LI simulation data is not complemented!
208  pSimCand = Ssw_ObjSim( p, Aig_Regular(pCand)->Id );
209  pSimLi = Ssw_ObjSim( p, pObjLi->Id );
210  pSimLo = Ssw_ObjSim( p, pObjLo->Id );
211  if ( Aig_Regular(pCand)->fPhase ^ Aig_IsComplement(pCand) )
212  {
213  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
214  if ( ~pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) )
215  return 0;
216  }
217  else
218  {
219  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
220  if ( pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) )
221  return 0;
222  }
223  return 1;
224 }
225 
226 /**Function*************************************************************
227 
228  Synopsis [Counts the number of 1s in the implication.]
229 
230  Description []
231 
232  SideEffects []
233 
234  SeeAlso []
235 
236 ***********************************************************************/
237 int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand )
238 {
239  unsigned * pSimLi, * pSimLo, * pSimCand;
240  int k, Counter = 0;
241  assert( pObjLo->fPhase == 0 );
242  // pObjLi->fPhase may be 1, but the LI simulation data is not complemented!
243  pSimCand = Ssw_ObjSim( p, Aig_Regular(pCand)->Id );
244  pSimLi = Ssw_ObjSim( p, pObjLi->Id );
245  pSimLo = Ssw_ObjSim( p, pObjLo->Id );
246  if ( Aig_Regular(pCand)->fPhase ^ Aig_IsComplement(pCand) )
247  {
248  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
249  Counter += Aig_WordCountOnes(~pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k]));
250  }
251  else
252  {
253  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
254  Counter += Aig_WordCountOnes(pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k]));
255  }
256  return Counter;
257 }
258 
259 /**Function*************************************************************
260 
261  Synopsis [Counts the number of 1s in the implication.]
262 
263  Description []
264 
265  SideEffects []
266 
267  SeeAlso []
268 
269 ***********************************************************************/
270 int Ssw_SmlCountEqual( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo )
271 {
272  unsigned * pSimLi, * pSimLo;
273  int k, Counter = 0;
274  assert( pObjLo->fPhase == 0 );
275  // pObjLi->fPhase may be 1, but the LI simulation data is not complemented!
276  pSimLi = Ssw_ObjSim( p, pObjLi->Id );
277  pSimLo = Ssw_ObjSim( p, pObjLo->Id );
278  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
279  Counter += Aig_WordCountOnes( ~(pSimLi[k] ^ pSimLo[k]) );
280  return Counter;
281 }
282 
283 /**Function*************************************************************
284 
285  Synopsis [Returns 1 if simulation info is composed of all zeros.]
286 
287  Description []
288 
289  SideEffects []
290 
291  SeeAlso []
292 
293 ***********************************************************************/
294 int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj )
295 {
296  unsigned * pSims;
297  int i;
298  pSims = Ssw_ObjSim(p, pObj->Id);
299  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
300  if ( pSims[i] )
301  return 0;
302  return 1;
303 }
304 
305 /**Function*************************************************************
306 
307  Synopsis [Returns 1 if simulation info is composed of all zeros.]
308 
309  Description []
310 
311  SideEffects []
312 
313  SeeAlso []
314 
315 ***********************************************************************/
316 int Ssw_SmlNodeIsZeroFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f )
317 {
318  unsigned * pSims = Ssw_ObjSim(p, pObj->Id);
319  return pSims[f] == 0;
320 }
321 
322 /**Function*************************************************************
323 
324  Synopsis [Counts the number of one's in the pattern of the object.]
325 
326  Description []
327 
328  SideEffects []
329 
330  SeeAlso []
331 
332 ***********************************************************************/
333 int Ssw_SmlNodeCountOnesReal( Ssw_Sml_t * p, Aig_Obj_t * pObj )
334 {
335  unsigned * pSims;
336  int i, Counter = 0;
337  pSims = Ssw_ObjSim(p, Aig_Regular(pObj)->Id);
338  if ( Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) )
339  {
340  for ( i = 0; i < p->nWordsTotal; i++ )
341  Counter += Aig_WordCountOnes( ~pSims[i] );
342  }
343  else
344  {
345  for ( i = 0; i < p->nWordsTotal; i++ )
346  Counter += Aig_WordCountOnes( pSims[i] );
347  }
348  return Counter;
349 }
350 
351 /**Function*************************************************************
352 
353  Synopsis [Counts the number of one's in the pattern of the objects.]
354 
355  Description []
356 
357  SideEffects []
358 
359  SeeAlso []
360 
361 ***********************************************************************/
362 int Ssw_SmlNodeCountOnesRealVec( Ssw_Sml_t * p, Vec_Ptr_t * vObjs )
363 {
364  Aig_Obj_t * pObj;
365  unsigned * pSims, uWord;
366  int i, k, Counter = 0;
367  if ( Vec_PtrSize(vObjs) == 0 )
368  return 0;
369  for ( i = 0; i < p->nWordsTotal; i++ )
370  {
371  uWord = 0;
372  Vec_PtrForEachEntry( Aig_Obj_t *, vObjs, pObj, k )
373  {
374  pSims = Ssw_ObjSim(p, Aig_Regular(pObj)->Id);
375  if ( Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) )
376  uWord |= ~pSims[i];
377  else
378  uWord |= pSims[i];
379  }
380  Counter += Aig_WordCountOnes( uWord );
381  }
382  return Counter;
383 }
384 
385 
386 
387 /**Function*************************************************************
388 
389  Synopsis [Generated const 0 pattern.]
390 
391  Description []
392 
393  SideEffects []
394 
395  SeeAlso []
396 
397 ***********************************************************************/
398 void Ssw_SmlSavePattern0( Ssw_Man_t * p, int fInit )
399 {
400  memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
401 }
402 
403 /**Function*************************************************************
404 
405  Synopsis [[Generated const 1 pattern.]
406 
407  Description []
408 
409  SideEffects []
410 
411  SeeAlso []
412 
413 ***********************************************************************/
414 void Ssw_SmlSavePattern1( Ssw_Man_t * p, int fInit )
415 {
416  Aig_Obj_t * pObj;
417  int i, k, nTruePis;
418  memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
419  if ( !fInit )
420  return;
421  // clear the state bits to correspond to all-0 initial state
422  nTruePis = Saig_ManPiNum(p->pAig);
423  k = 0;
424  Saig_ManForEachLo( p->pAig, pObj, i )
425  Abc_InfoXorBit( p->pPatWords, nTruePis * p->nFrames + k++ );
426 }
427 
428 
429 /**Function*************************************************************
430 
431  Synopsis [Creates the counter-example from the successful pattern.]
432 
433  Description []
434 
435  SideEffects []
436 
437  SeeAlso []
438 
439 ***********************************************************************/
440 int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo )
441 {
442  Aig_Obj_t * pFanin, * pObjPi;
443  unsigned * pSims;
444  int i, k, BestPat, * pModel;
445  // find the word of the pattern
446  pFanin = Aig_ObjFanin0(pObjPo);
447  pSims = Ssw_ObjSim(p, pFanin->Id);
448  for ( i = 0; i < p->nWordsTotal; i++ )
449  if ( pSims[i] )
450  break;
451  assert( i < p->nWordsTotal );
452  // find the bit of the pattern
453  for ( k = 0; k < 32; k++ )
454  if ( pSims[i] & (1 << k) )
455  break;
456  assert( k < 32 );
457  // determine the best pattern
458  BestPat = i * 32 + k;
459  // fill in the counter-example data
460  pModel = ABC_ALLOC( int, Aig_ManCiNum(p->pAig)+1 );
461  Aig_ManForEachCi( p->pAig, pObjPi, i )
462  {
463  pModel[i] = Abc_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat);
464 // Abc_Print( 1, "%d", pModel[i] );
465  }
466  pModel[Aig_ManCiNum(p->pAig)] = pObjPo->Id;
467 // Abc_Print( 1, "\n" );
468  return pModel;
469 }
470 
471 /**Function*************************************************************
472 
473  Synopsis [Returns 1 if the one of the output is already non-constant 0.]
474 
475  Description []
476 
477  SideEffects []
478 
479  SeeAlso []
480 
481 ***********************************************************************/
482 int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
483 {
484  Aig_Obj_t * pObj;
485  int i;
486  // make sure the reference simulation pattern does not detect the bug
487  pObj = Aig_ManCo( p->pAig, 0 );
488  assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) );
489  Aig_ManForEachCo( p->pAig, pObj, i )
490  {
491  if ( !Ssw_SmlObjIsConstWord( p, Aig_ObjFanin0(pObj) ) )
492  {
493  // create the counter-example from this pattern
494  return Ssw_SmlCheckOutputSavePattern( p, pObj );
495  }
496  }
497  return NULL;
498 }
499 
500 
501 
502 /**Function*************************************************************
503 
504  Synopsis [Assigns random patterns to the PI node.]
505 
506  Description []
507 
508  SideEffects []
509 
510  SeeAlso []
511 
512 ***********************************************************************/
513 void Ssw_SmlAssignRandom( Ssw_Sml_t * p, Aig_Obj_t * pObj )
514 {
515  unsigned * pSims;
516  int i, f;
517  assert( Aig_ObjIsCi(pObj) );
518  pSims = Ssw_ObjSim( p, pObj->Id );
519  for ( i = 0; i < p->nWordsTotal; i++ )
520  pSims[i] = Ssw_ObjRandomSim();
521  // set the first bit 0 in each frame
522  assert( p->nWordsFrame * p->nFrames == p->nWordsTotal );
523  for ( f = 0; f < p->nFrames; f++ )
524  pSims[p->nWordsFrame*f] <<= 1;
525 }
526 
527 /**Function*************************************************************
528 
529  Synopsis [Assigns random patterns to the PI node.]
530 
531  Description []
532 
533  SideEffects []
534 
535  SeeAlso []
536 
537 ***********************************************************************/
538 void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
539 {
540  unsigned * pSims;
541  int i;
542  assert( iFrame < p->nFrames );
543  assert( Aig_ObjIsCi(pObj) );
544  pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
545  for ( i = 0; i < p->nWordsFrame; i++ )
546  pSims[i] = Ssw_ObjRandomSim();
547 }
548 
549 /**Function*************************************************************
550 
551  Synopsis [Assigns constant patterns to the PI node.]
552 
553  Description []
554 
555  SideEffects []
556 
557  SeeAlso []
558 
559 ***********************************************************************/
560 void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
561 {
562  unsigned * pSims;
563  int i;
564  assert( iFrame < p->nFrames );
565  assert( Aig_ObjIsCi(pObj) );
566  pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
567  for ( i = 0; i < p->nWordsFrame; i++ )
568  pSims[i] = fConst1? ~(unsigned)0 : 0;
569 }
570 
571 /**Function*************************************************************
572 
573  Synopsis [Assigns constant patterns to the PI node.]
574 
575  Description []
576 
577  SideEffects []
578 
579  SeeAlso []
580 
581 ***********************************************************************/
582 void Ssw_SmlObjAssignConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame, int iWord )
583 {
584  unsigned * pSims;
585  assert( iFrame < p->nFrames );
586  assert( iWord < p->nWordsFrame );
587  assert( Aig_ObjIsCi(pObj) );
588  pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
589  pSims[iWord] = fConst1? ~(unsigned)0 : 0;
590 }
591 
592 /**Function*************************************************************
593 
594  Synopsis [Assigns constant patterns to the PI node.]
595 
596  Description []
597 
598  SideEffects []
599 
600  SeeAlso []
601 
602 ***********************************************************************/
603 void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame )
604 {
605  unsigned * pSims;
606  assert( iFrame < p->nFrames );
607  assert( Aig_ObjIsCi(pObj) );
608  pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
609  pSims[iWord] = Word;
610 }
611 
612 /**Function*************************************************************
613 
614  Synopsis [Assings distance-1 simulation info for the PIs.]
615 
616  Description []
617 
618  SideEffects []
619 
620  SeeAlso []
621 
622 ***********************************************************************/
623 void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
624 {
625  Aig_Obj_t * pObj;
626  int f, i, k, Limit, nTruePis;
627  assert( p->nFrames > 0 );
628  if ( p->nFrames == 1 )
629  {
630  // copy the PI info
631  Aig_ManForEachCi( p->pAig, pObj, i )
632  Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
633  // flip one bit
634  Limit = Abc_MinInt( Aig_ManCiNum(p->pAig), p->nWordsTotal * 32 - 1 );
635  for ( i = 0; i < Limit; i++ )
636  Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig,i)->Id ), i+1 );
637  }
638  else
639  {
640  int fUseDist1 = 0;
641 
642  // copy the PI info for each frame
643  nTruePis = Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig);
644  for ( f = 0; f < p->nFrames; f++ )
645  Saig_ManForEachPi( p->pAig, pObj, i )
646  Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f );
647  // copy the latch info
648  k = 0;
649  Saig_ManForEachLo( p->pAig, pObj, i )
650  Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
651 // assert( p->pFrames == NULL || nTruePis * p->nFrames + k == Aig_ManCiNum(p->pFrames) );
652 
653  // flip one bit of the last frame
654  if ( fUseDist1 ) //&& p->nFrames == 2 )
655  {
656  Limit = Abc_MinInt( nTruePis, p->nWordsFrame * 32 - 1 );
657  for ( i = 0; i < Limit; i++ )
658  Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
659  }
660  }
661 }
662 
663 /**Function*************************************************************
664 
665  Synopsis [Assings distance-1 simulation info for the PIs.]
666 
667  Description []
668 
669  SideEffects []
670 
671  SeeAlso []
672 
673 ***********************************************************************/
674 void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
675 {
676  Aig_Obj_t * pObj;
677  int f, i, Limit;
678  assert( p->nFrames > 0 );
679 
680  // copy the pattern into the primary inputs
681  Aig_ManForEachCi( p->pAig, pObj, i )
682  Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
683 
684  // set distance one PIs for the first frame
685  Limit = Abc_MinInt( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 );
686  for ( i = 0; i < Limit; i++ )
687  Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ), i+1 );
688 
689  // create random info for the remaining timeframes
690  for ( f = 1; f < p->nFrames; f++ )
691  Saig_ManForEachPi( p->pAig, pObj, i )
692  Ssw_SmlAssignRandomFrame( p, pObj, f );
693 }
694 
695 /**Function*************************************************************
696 
697  Synopsis [Simulates one node.]
698 
699  Description []
700 
701  SideEffects []
702 
703  SeeAlso []
704 
705 ***********************************************************************/
706 void Ssw_SmlNodeSimulate( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
707 {
708  unsigned * pSims, * pSims0, * pSims1;
709  int fCompl, fCompl0, fCompl1, i;
710  assert( iFrame < p->nFrames );
711  assert( !Aig_IsComplement(pObj) );
712  assert( Aig_ObjIsNode(pObj) );
713  assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
714  // get hold of the simulation information
715  pSims = Ssw_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
716  pSims0 = Ssw_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
717  pSims1 = Ssw_ObjSim(p, Aig_ObjFanin1(pObj)->Id) + p->nWordsFrame * iFrame;
718  // get complemented attributes of the children using their random info
719  fCompl = pObj->fPhase;
720  fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
721  fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj));
722  // simulate
723  if ( fCompl0 && fCompl1 )
724  {
725  if ( fCompl )
726  for ( i = 0; i < p->nWordsFrame; i++ )
727  pSims[i] = (pSims0[i] | pSims1[i]);
728  else
729  for ( i = 0; i < p->nWordsFrame; i++ )
730  pSims[i] = ~(pSims0[i] | pSims1[i]);
731  }
732  else if ( fCompl0 && !fCompl1 )
733  {
734  if ( fCompl )
735  for ( i = 0; i < p->nWordsFrame; i++ )
736  pSims[i] = (pSims0[i] | ~pSims1[i]);
737  else
738  for ( i = 0; i < p->nWordsFrame; i++ )
739  pSims[i] = (~pSims0[i] & pSims1[i]);
740  }
741  else if ( !fCompl0 && fCompl1 )
742  {
743  if ( fCompl )
744  for ( i = 0; i < p->nWordsFrame; i++ )
745  pSims[i] = (~pSims0[i] | pSims1[i]);
746  else
747  for ( i = 0; i < p->nWordsFrame; i++ )
748  pSims[i] = (pSims0[i] & ~pSims1[i]);
749  }
750  else // if ( !fCompl0 && !fCompl1 )
751  {
752  if ( fCompl )
753  for ( i = 0; i < p->nWordsFrame; i++ )
754  pSims[i] = ~(pSims0[i] & pSims1[i]);
755  else
756  for ( i = 0; i < p->nWordsFrame; i++ )
757  pSims[i] = (pSims0[i] & pSims1[i]);
758  }
759 }
760 
761 /**Function*************************************************************
762 
763  Synopsis [Simulates one node.]
764 
765  Description []
766 
767  SideEffects []
768 
769  SeeAlso []
770 
771 ***********************************************************************/
772 int Ssw_SmlNodesCompareInFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 )
773 {
774  unsigned * pSims0, * pSims1;
775  int i;
776  assert( iFrame0 < p->nFrames );
777  assert( iFrame1 < p->nFrames );
778  assert( !Aig_IsComplement(pObj0) );
779  assert( !Aig_IsComplement(pObj1) );
780  assert( iFrame0 == 0 || p->nWordsFrame < p->nWordsTotal );
781  assert( iFrame1 == 0 || p->nWordsFrame < p->nWordsTotal );
782  // get hold of the simulation information
783  pSims0 = Ssw_ObjSim(p, pObj0->Id) + p->nWordsFrame * iFrame0;
784  pSims1 = Ssw_ObjSim(p, pObj1->Id) + p->nWordsFrame * iFrame1;
785  // compare
786  for ( i = 0; i < p->nWordsFrame; i++ )
787  if ( pSims0[i] != pSims1[i] )
788  return 0;
789  return 1;
790 }
791 
792 /**Function*************************************************************
793 
794  Synopsis [Simulates one node.]
795 
796  Description []
797 
798  SideEffects []
799 
800  SeeAlso []
801 
802 ***********************************************************************/
803 void Ssw_SmlNodeCopyFanin( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
804 {
805  unsigned * pSims, * pSims0;
806  int fCompl, fCompl0, i;
807  assert( iFrame < p->nFrames );
808  assert( !Aig_IsComplement(pObj) );
809  assert( Aig_ObjIsCo(pObj) );
810  assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
811  // get hold of the simulation information
812  pSims = Ssw_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
813  pSims0 = Ssw_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
814  // get complemented attributes of the children using their random info
815  fCompl = pObj->fPhase;
816  fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
817  // copy information as it is
818  if ( fCompl0 )
819  for ( i = 0; i < p->nWordsFrame; i++ )
820  pSims[i] = ~pSims0[i];
821  else
822  for ( i = 0; i < p->nWordsFrame; i++ )
823  pSims[i] = pSims0[i];
824 }
825 
826 /**Function*************************************************************
827 
828  Synopsis [Simulates one node.]
829 
830  Description []
831 
832  SideEffects []
833 
834  SeeAlso []
835 
836 ***********************************************************************/
837 void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame )
838 {
839  unsigned * pSims0, * pSims1;
840  int i;
841  assert( iFrame < p->nFrames );
842  assert( !Aig_IsComplement(pOut) );
843  assert( !Aig_IsComplement(pIn) );
844  assert( Aig_ObjIsCo(pOut) );
845  assert( Aig_ObjIsCi(pIn) );
846  assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
847  // get hold of the simulation information
848  pSims0 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame;
849  pSims1 = Ssw_ObjSim(p, pIn->Id) + p->nWordsFrame * (iFrame+1);
850  // copy information as it is
851  for ( i = 0; i < p->nWordsFrame; i++ )
852  pSims1[i] = pSims0[i];
853 }
854 
855 /**Function*************************************************************
856 
857  Synopsis [Simulates one node.]
858 
859  Description []
860 
861  SideEffects []
862 
863  SeeAlso []
864 
865 ***********************************************************************/
866 void Ssw_SmlNodeTransferFirst( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn )
867 {
868  unsigned * pSims0, * pSims1;
869  int i;
870  assert( !Aig_IsComplement(pOut) );
871  assert( !Aig_IsComplement(pIn) );
872  assert( Aig_ObjIsCo(pOut) );
873  assert( Aig_ObjIsCi(pIn) );
874  assert( p->nWordsFrame < p->nWordsTotal );
875  // get hold of the simulation information
876  pSims0 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * (p->nFrames-1);
877  pSims1 = Ssw_ObjSim(p, pIn->Id);
878  // copy information as it is
879  for ( i = 0; i < p->nWordsFrame; i++ )
880  pSims1[i] = pSims0[i];
881 }
882 
883 
884 /**Function*************************************************************
885 
886  Synopsis [Assings random simulation info for the PIs.]
887 
888  Description []
889 
890  SideEffects []
891 
892  SeeAlso []
893 
894 ***********************************************************************/
895 void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
896 {
897  Aig_Obj_t * pObj;
898  int i;
899  if ( fInit )
900  {
901  assert( Aig_ManRegNum(p->pAig) > 0 );
902  assert( Aig_ManRegNum(p->pAig) <= Aig_ManCiNum(p->pAig) );
903  // assign random info for primary inputs
904  Saig_ManForEachPi( p->pAig, pObj, i )
905  Ssw_SmlAssignRandom( p, pObj );
906  // assign the initial state for the latches
907  Saig_ManForEachLo( p->pAig, pObj, i )
908  Ssw_SmlObjAssignConst( p, pObj, 0, 0 );
909  }
910  else
911  {
912  Aig_ManForEachCi( p->pAig, pObj, i )
913  Ssw_SmlAssignRandom( p, pObj );
914  }
915 }
916 
917 /**Function*************************************************************
918 
919  Synopsis [Assings random simulation info for the PIs.]
920 
921  Description []
922 
923  SideEffects []
924 
925  SeeAlso []
926 
927 ***********************************************************************/
928 void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit )
929 {
930  Aig_Obj_t * pObj;
931  int Entry, i, nRegs;
932  nRegs = Aig_ManRegNum(p->pAig);
933  assert( nRegs > 0 );
934  assert( nRegs <= Aig_ManCiNum(p->pAig) );
935  assert( Vec_IntSize(vInit) == nRegs * p->nWordsFrame );
936  // assign random info for primary inputs
937  Saig_ManForEachPi( p->pAig, pObj, i )
938  Ssw_SmlAssignRandom( p, pObj );
939  // assign the initial state for the latches
940  Vec_IntForEachEntry( vInit, Entry, i )
941  Ssw_SmlObjAssignConstWord( p, Saig_ManLo(p->pAig, i % nRegs), Entry, 0, i / nRegs );
942 }
943 
944 /**Function*************************************************************
945 
946  Synopsis [Assings random simulation info for the PIs.]
947 
948  Description []
949 
950  SideEffects []
951 
952  SeeAlso []
953 
954 ***********************************************************************/
955 void Ssw_SmlReinitialize( Ssw_Sml_t * p )
956 {
957  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
958  int i;
959  assert( Aig_ManRegNum(p->pAig) > 0 );
960  assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
961  // assign random info for primary inputs
962  Saig_ManForEachPi( p->pAig, pObj, i )
963  Ssw_SmlAssignRandom( p, pObj );
964  // copy simulation info into the inputs
965  Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
966  Ssw_SmlNodeTransferFirst( p, pObjLi, pObjLo );
967 }
968 
969 /**Function*************************************************************
970 
971  Synopsis [Check if any of the POs becomes non-constant.]
972 
973  Description []
974 
975  SideEffects []
976 
977  SeeAlso []
978 
979 ***********************************************************************/
980 int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p )
981 {
982  Aig_Obj_t * pObj;
983  int i;
984  Saig_ManForEachPo( p->pAig, pObj, i )
985  {
986  if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
987  return 0;
988  if ( !Ssw_SmlNodeIsZero(p, pObj) )
989  return 1;
990  }
991  return 0;
992 }
993 
994 /**Function*************************************************************
995 
996  Synopsis [Simulates AIG manager.]
997 
998  Description [Assumes that the PI simulation info is attached.]
999 
1000  SideEffects []
1001 
1002  SeeAlso []
1003 
1004 ***********************************************************************/
1005 void Ssw_SmlSimulateOne( Ssw_Sml_t * p )
1006 {
1007  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
1008  int f, i;
1009  abctime clk;
1010 clk = Abc_Clock();
1011  for ( f = 0; f < p->nFrames; f++ )
1012  {
1013  // simulate the nodes
1014  Aig_ManForEachNode( p->pAig, pObj, i )
1015  Ssw_SmlNodeSimulate( p, pObj, f );
1016  // copy simulation info into outputs
1017  Saig_ManForEachPo( p->pAig, pObj, i )
1018  Ssw_SmlNodeCopyFanin( p, pObj, f );
1019  // copy simulation info into outputs
1020  Saig_ManForEachLi( p->pAig, pObj, i )
1021  Ssw_SmlNodeCopyFanin( p, pObj, f );
1022  // quit if this is the last timeframe
1023  if ( f == p->nFrames - 1 )
1024  break;
1025  // copy simulation info into the inputs
1026  Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
1027  Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
1028  }
1029 p->timeSim += Abc_Clock() - clk;
1030 p->nSimRounds++;
1031 }
1032 
1033 /**Function*************************************************************
1034 
1035  Synopsis [Converts simulation information to be not normallized.]
1036 
1037  Description []
1038 
1039  SideEffects []
1040 
1041  SeeAlso []
1042 
1043 ***********************************************************************/
1044 void Ssw_SmlUnnormalize( Ssw_Sml_t * p )
1045 {
1046  Aig_Obj_t * pObj;
1047  unsigned * pSims;
1048  int i, k;
1049  // convert constant 1
1050  pSims = Ssw_ObjSim( p, 0 );
1051  for ( i = 0; i < p->nWordsFrame; i++ )
1052  pSims[i] = ~pSims[i];
1053  // convert internal nodes
1054  Aig_ManForEachNode( p->pAig, pObj, k )
1055  {
1056  if ( pObj->fPhase == 0 )
1057  continue;
1058  pSims = Ssw_ObjSim( p, pObj->Id );
1059  for ( i = 0; i < p->nWordsFrame; i++ )
1060  pSims[i] = ~pSims[i];
1061  }
1062  // PIs/POs are always stored in their natural state
1063 }
1064 
1065 /**Function*************************************************************
1066 
1067  Synopsis [Simulates AIG manager.]
1068 
1069  Description [Assumes that the PI simulation info is attached.]
1070 
1071  SideEffects []
1072 
1073  SeeAlso []
1074 
1075 ***********************************************************************/
1076 void Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pVisited, int nVisCounter )
1077 {
1078 // if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
1079 // return;
1080 // Aig_ObjSetTravIdCurrent(p->pAig, pObj);
1081  if ( pVisited[p->nFrames*pObj->Id+f] == nVisCounter )
1082  return;
1083  pVisited[p->nFrames*pObj->Id+f] = nVisCounter;
1084  if ( Saig_ObjIsPi( p->pAig, pObj ) || Aig_ObjIsConst1(pObj) )
1085  return;
1086  if ( Saig_ObjIsLo( p->pAig, pObj ) )
1087  {
1088  if ( f == 0 )
1089  return;
1090  Ssw_SmlSimulateOneDyn_rec( p, Saig_ObjLoToLi(p->pAig, pObj), f-1, pVisited, nVisCounter );
1091  Ssw_SmlNodeTransferNext( p, Saig_ObjLoToLi(p->pAig, pObj), pObj, f-1 );
1092  return;
1093  }
1094  if ( Saig_ObjIsLi( p->pAig, pObj ) )
1095  {
1096  Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin0(pObj), f, pVisited, nVisCounter );
1097  Ssw_SmlNodeCopyFanin( p, pObj, f );
1098  return;
1099  }
1100  assert( Aig_ObjIsNode(pObj) );
1101  Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin0(pObj), f, pVisited, nVisCounter );
1102  Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin1(pObj), f, pVisited, nVisCounter );
1103  Ssw_SmlNodeSimulate( p, pObj, f );
1104 }
1105 
1106 /**Function*************************************************************
1107 
1108  Synopsis [Simulates AIG manager.]
1109 
1110  Description [Assumes that the PI simulation info is attached.]
1111 
1112  SideEffects []
1113 
1114  SeeAlso []
1115 
1116 ***********************************************************************/
1117 void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p )
1118 {
1119  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
1120  int i;
1121  abctime clk;
1122 clk = Abc_Clock();
1123  // simulate the nodes
1124  Aig_ManForEachNode( p->pAig, pObj, i )
1125  Ssw_SmlNodeSimulate( p, pObj, 0 );
1126  // copy simulation info into outputs
1127  Saig_ManForEachLi( p->pAig, pObj, i )
1128  Ssw_SmlNodeCopyFanin( p, pObj, 0 );
1129  // copy simulation info into the inputs
1130  Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
1131  Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, 0 );
1132 p->timeSim += Abc_Clock() - clk;
1133 p->nSimRounds++;
1134 }
1135 
1136 
1137 /**Function*************************************************************
1138 
1139  Synopsis [Allocates simulation manager.]
1140 
1141  Description []
1142 
1143  SideEffects []
1144 
1145  SeeAlso []
1146 
1147 ***********************************************************************/
1148 Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
1149 {
1150  Ssw_Sml_t * p;
1151  p = (Ssw_Sml_t *)ABC_ALLOC( char, sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
1152  memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
1153  p->pAig = pAig;
1154  p->nPref = nPref;
1155  p->nFrames = nPref + nFrames;
1156  p->nWordsFrame = nWordsFrame;
1157  p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
1158  p->nWordsPref = nPref * nWordsFrame;
1159  return p;
1160 }
1161 
1162 /**Function*************************************************************
1163 
1164  Synopsis [Allocates simulation manager.]
1165 
1166  Description []
1167 
1168  SideEffects []
1169 
1170  SeeAlso []
1171 
1172 ***********************************************************************/
1173 void Ssw_SmlClean( Ssw_Sml_t * p )
1174 {
1175  memset( p->pData, 0, sizeof(unsigned) * Aig_ManObjNumMax(p->pAig) * p->nWordsTotal );
1176 }
1177 
1178 /**Function*************************************************************
1179 
1180  Synopsis [Get simulation data.]
1181 
1182  Description []
1183 
1184  SideEffects []
1185 
1186  SeeAlso []
1187 
1188 ***********************************************************************/
1189 Vec_Ptr_t * Ssw_SmlSimDataPointers( Ssw_Sml_t * p )
1190 {
1191  Vec_Ptr_t * vSimInfo;
1192  Aig_Obj_t * pObj;
1193  int i;
1194  vSimInfo = Vec_PtrStart( Aig_ManObjNumMax(p->pAig) );
1195  Aig_ManForEachObj( p->pAig, pObj, i )
1196  Vec_PtrWriteEntry( vSimInfo, i, Ssw_ObjSim(p, i) );
1197  return vSimInfo;
1198 }
1199 
1200 /**Function*************************************************************
1201 
1202  Synopsis [Deallocates simulation manager.]
1203 
1204  Description []
1205 
1206  SideEffects []
1207 
1208  SeeAlso []
1209 
1210 ***********************************************************************/
1211 void Ssw_SmlStop( Ssw_Sml_t * p )
1212 {
1213  ABC_FREE( p );
1214 }
1215 
1216 
1217 /**Function*************************************************************
1218 
1219  Synopsis [Performs simulation of the uninitialized circuit.]
1220 
1221  Description []
1222 
1223  SideEffects []
1224 
1225  SeeAlso []
1226 
1227 ***********************************************************************/
1228 Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords )
1229 {
1230  Ssw_Sml_t * p;
1231  p = Ssw_SmlStart( pAig, 0, 1, nWords );
1232  Ssw_SmlInitialize( p, 0 );
1233  Ssw_SmlSimulateOne( p );
1234  return p;
1235 }
1236 
1237 /**Function*************************************************************
1238 
1239  Synopsis [Performs simulation of the initialized circuit.]
1240 
1241  Description []
1242 
1243  SideEffects []
1244 
1245  SeeAlso []
1246 
1247 ***********************************************************************/
1248 Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords )
1249 {
1250  Ssw_Sml_t * p;
1251  p = Ssw_SmlStart( pAig, nPref, nFrames, nWords );
1252  Ssw_SmlInitialize( p, 1 );
1253  Ssw_SmlSimulateOne( p );
1254  p->fNonConstOut = Ssw_SmlCheckNonConstOutputs( p );
1255  return p;
1256 }
1257 
1258 /**Function*************************************************************
1259 
1260  Synopsis [Performs next round of sequential simulation.]
1261 
1262  Description []
1263 
1264  SideEffects []
1265 
1266  SeeAlso []
1267 
1268 ***********************************************************************/
1269 void Ssw_SmlResimulateSeq( Ssw_Sml_t * p )
1270 {
1271  Ssw_SmlReinitialize( p );
1272  Ssw_SmlSimulateOne( p );
1273  p->fNonConstOut = Ssw_SmlCheckNonConstOutputs( p );
1274 }
1275 
1276 
1277 /**Function*************************************************************
1278 
1279  Synopsis [Returns the number of frames simulated in the manager.]
1280 
1281  Description []
1282 
1283  SideEffects []
1284 
1285  SeeAlso []
1286 
1287 ***********************************************************************/
1288 int Ssw_SmlNumFrames( Ssw_Sml_t * p )
1289 {
1290  return p->nFrames;
1291 }
1292 
1293 /**Function*************************************************************
1294 
1295  Synopsis [Returns the total number of simulation words.]
1296 
1297  Description []
1298 
1299  SideEffects []
1300 
1301  SeeAlso []
1302 
1303 ***********************************************************************/
1304 int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p )
1305 {
1306  return p->nWordsTotal;
1307 }
1308 
1309 /**Function*************************************************************
1310 
1311  Synopsis [Returns the pointer to the simulation info of the node.]
1312 
1313  Description [The simulation info is normalized unless procedure
1314  Ssw_SmlUnnormalize() is called in advance.]
1315 
1316  SideEffects []
1317 
1318  SeeAlso []
1319 
1320 ***********************************************************************/
1321 unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj )
1322 {
1323  assert( !Aig_IsComplement(pObj) );
1324  return Ssw_ObjSim( p, pObj->Id );
1325 }
1326 
1327 /**Function*************************************************************
1328 
1329  Synopsis [Creates sequential counter-example from the simulation info.]
1330 
1331  Description []
1332 
1333  SideEffects []
1334 
1335  SeeAlso []
1336 
1337 ***********************************************************************/
1338 Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
1339 {
1340  Abc_Cex_t * pCex;
1341  Aig_Obj_t * pObj;
1342  unsigned * pSims;
1343  int iPo, iFrame, iBit, i, k;
1344 
1345  // make sure the simulation manager has it
1346  assert( p->fNonConstOut );
1347 
1348  // find the first output that failed
1349  iPo = -1;
1350  iBit = -1;
1351  iFrame = -1;
1352  Saig_ManForEachPo( p->pAig, pObj, iPo )
1353  {
1354  if ( Ssw_SmlNodeIsZero(p, pObj) )
1355  continue;
1356  pSims = Ssw_ObjSim( p, pObj->Id );
1357  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
1358  if ( pSims[i] )
1359  {
1360  iFrame = i / p->nWordsFrame;
1361  iBit = 32 * (i % p->nWordsFrame) + Aig_WordFindFirstBit( pSims[i] );
1362  break;
1363  }
1364  break;
1365  }
1366  assert( iPo < Aig_ManCoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
1367  assert( iFrame < p->nFrames );
1368  assert( iBit < 32 * p->nWordsFrame );
1369 
1370  // allocate the counter example
1371  pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
1372  pCex->iPo = iPo;
1373  pCex->iFrame = iFrame;
1374 
1375  // copy the bit data
1376  Saig_ManForEachLo( p->pAig, pObj, k )
1377  {
1378  pSims = Ssw_ObjSim( p, pObj->Id );
1379  if ( Abc_InfoHasBit( pSims, iBit ) )
1380  Abc_InfoSetBit( pCex->pData, k );
1381  }
1382  for ( i = 0; i <= iFrame; i++ )
1383  {
1384  Saig_ManForEachPi( p->pAig, pObj, k )
1385  {
1386  pSims = Ssw_ObjSim( p, pObj->Id );
1387  if ( Abc_InfoHasBit( pSims, 32 * p->nWordsFrame * i + iBit ) )
1388  Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * i + k );
1389  }
1390  }
1391  // verify the counter example
1392  if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
1393  {
1394  Abc_Print( 1, "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" );
1395  Abc_CexFree( pCex );
1396  pCex = NULL;
1397  }
1398  return pCex;
1399 }
1400 
1401 ////////////////////////////////////////////////////////////////////////
1402 /// END OF FILE ///
1403 ////////////////////////////////////////////////////////////////////////
1404 
1405 
1406 ABC_NAMESPACE_IMPL_END
memset
char * memset()
Ssw_SmlReinitialize
void Ssw_SmlReinitialize(Ssw_Sml_t *p)
Definition: sswSim.c:955
Vec_PtrStart
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
Ssw_Sml_t_::nWordsPref
int nWordsPref
Definition: sswSim.c:38
Ssw_SmlNodeTransferFirst
void Ssw_SmlNodeTransferFirst(Ssw_Sml_t *p, Aig_Obj_t *pOut, Aig_Obj_t *pIn)
Definition: sswSim.c:866
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Ssw_SmlSimulateOne
void Ssw_SmlSimulateOne(Ssw_Sml_t *p)
Definition: sswSim.c:1005
Ssw_Sml_t_::pData
unsigned pData[0]
Definition: sswSim.c:42
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Ssw_SmlAssignDist1Plus
void Ssw_SmlAssignDist1Plus(Ssw_Sml_t *p, unsigned *pPat)
Definition: sswSim.c:674
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
Ssw_SmlClean
void Ssw_SmlClean(Ssw_Sml_t *p)
Definition: sswSim.c:1173
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
Ssw_SmlSimulateOneDyn_rec
void Ssw_SmlSimulateOneDyn_rec(Ssw_Sml_t *p, Aig_Obj_t *pObj, int f, int *pVisited, int nVisCounter)
Definition: sswSim.c:1076
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Ssw_SmlAssignDist1
void Ssw_SmlAssignDist1(Ssw_Sml_t *p, unsigned *pPat)
Definition: sswSim.c:623
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Saig_ManVerifyCex
int Saig_ManVerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:279
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition: aig.h:80
Ssw_SmlObjAssignConstWord
void Ssw_SmlObjAssignConstWord(Ssw_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame, int iWord)
Definition: sswSim.c:582
Saig_ManLo
static Aig_Obj_t * Saig_ManLo(Aig_Man_t *p, int i)
Definition: saig.h:79
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
Ssw_SmlAssignRandom
void Ssw_SmlAssignRandom(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:513
Ssw_SmlObjSetWord
void Ssw_SmlObjSetWord(Ssw_Sml_t *p, Aig_Obj_t *pObj, unsigned Word, int iWord, int iFrame)
Definition: sswSim.c:603
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Ssw_SmlSavePattern0
void Ssw_SmlSavePattern0(Ssw_Man_t *p, int fInit)
Definition: sswSim.c:398
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
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Ssw_SmlObjsAreEqualBit
int Ssw_SmlObjsAreEqualBit(void *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition: sswSim.c:163
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Ssw_SmlSimulateSeq
Ssw_Sml_t * Ssw_SmlSimulateSeq(Aig_Man_t *pAig, int nPref, int nFrames, int nWords)
Definition: sswSim.c:1248
Ssw_SmlNodeTransferNext
void Ssw_SmlNodeTransferNext(Ssw_Sml_t *p, Aig_Obj_t *pOut, Aig_Obj_t *pIn, int iFrame)
Definition: sswSim.c:837
Ssw_Sml_t_::nSimRounds
int nSimRounds
Definition: sswSim.c:40
Ssw_SmlCheckOutput
int * Ssw_SmlCheckOutput(Ssw_Sml_t *p)
Definition: sswSim.c:482
Ssw_SmlResimulateSeq
void Ssw_SmlResimulateSeq(Ssw_Sml_t *p)
Definition: sswSim.c:1269
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Ssw_Man_t
typedefABC_NAMESPACE_HEADER_START struct Ssw_Man_t_ Ssw_Man_t
INCLUDES ///.
Definition: sswInt.h:47
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
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
Ssw_SmlObjAssignConst
void Ssw_SmlObjAssignConst(Ssw_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame)
Definition: sswSim.c:560
nWords
int nWords
Definition: abcNpn.c:127
Ssw_SmlNodeIsZeroFrame
int Ssw_SmlNodeIsZeroFrame(Ssw_Sml_t *p, Aig_Obj_t *pObj, int f)
Definition: sswSim.c:316
Saig_ObjIsLi
static int Saig_ObjIsLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:85
Ssw_SmlObjIsConstWord
int Ssw_SmlObjIsConstWord(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:102
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
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
Ssw_SmlSimulateOneFrame
void Ssw_SmlSimulateOneFrame(Ssw_Sml_t *p)
Definition: sswSim.c:1117
Aig_WordCountOnes
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
Ssw_SmlNodeIsZero
int Ssw_SmlNodeIsZero(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:294
Ssw_SmlSimInfo
unsigned * Ssw_SmlSimInfo(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:1321
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Ssw_SmlNodeNotEquWeight
int Ssw_SmlNodeNotEquWeight(Ssw_Sml_t *p, int Left, int Right)
Definition: sswSim.c:180
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
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
Ssw_Sml_t_::nPref
int nPref
Definition: sswSim.c:34
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Ssw_SmlObjIsConstBit
int Ssw_SmlObjIsConstBit(void *p, Aig_Obj_t *pObj)
Definition: sswSim.c:147
Aig_ObjChild1
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
Ssw_SmlCheckXorImplication
int Ssw_SmlCheckXorImplication(Ssw_Sml_t *p, Aig_Obj_t *pObjLi, Aig_Obj_t *pObjLo, Aig_Obj_t *pCand)
DECLARATIONS ///.
Definition: sswSim.c:202
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Ssw_Sml_t_::fNonConstOut
int fNonConstOut
Definition: sswSim.c:39
Aig_ObjPhaseReal
static int Aig_ObjPhaseReal(Aig_Obj_t *pObj)
Definition: aig.h:299
Aig_Obj_t_
Definition: aig.h:69
Counter
static int Counter
Definition: extraBddMisc.c:1877
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Ssw_SmlCountXorImplication
int Ssw_SmlCountXorImplication(Ssw_Sml_t *p, Aig_Obj_t *pObjLi, Aig_Obj_t *pObjLo, Aig_Obj_t *pCand)
Definition: sswSim.c:237
Ssw_SmlSimDataPointers
Vec_Ptr_t * Ssw_SmlSimDataPointers(Ssw_Sml_t *p)
Definition: sswSim.c:1189
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Ssw_SmlNumFrames
int Ssw_SmlNumFrames(Ssw_Sml_t *p)
Definition: sswSim.c:1288
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Ssw_SmlStart
Ssw_Sml_t * Ssw_SmlStart(Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
Definition: sswSim.c:1148
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
Ssw_SmlObjHashWord
unsigned Ssw_SmlObjHashWord(Ssw_Sml_t *p, Aig_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition: sswSim.c:63
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Ssw_SmlNumWordsTotal
int Ssw_SmlNumWordsTotal(Ssw_Sml_t *p)
Definition: sswSim.c:1304
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Ssw_SmlCheckNonConstOutputs
int Ssw_SmlCheckNonConstOutputs(Ssw_Sml_t *p)
Definition: sswSim.c:980
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Ssw_SmlNodeSimulate
void Ssw_SmlNodeSimulate(Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: sswSim.c:706
Ssw_SmlCheckOutputSavePattern
int * Ssw_SmlCheckOutputSavePattern(Ssw_Sml_t *p, Aig_Obj_t *pObjPo)
Definition: sswSim.c:440
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Ssw_SmlSavePattern1
void Ssw_SmlSavePattern1(Ssw_Man_t *p, int fInit)
Definition: sswSim.c:414
Ssw_SmlAssignRandomFrame
void Ssw_SmlAssignRandomFrame(Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: sswSim.c:538
Ssw_SmlNodesCompareInFrame
int Ssw_SmlNodesCompareInFrame(Ssw_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1, int iFrame0, int iFrame1)
Definition: sswSim.c:772
Ssw_ObjRandomSim
static unsigned Ssw_ObjRandomSim()
Definition: sswSim.c:46
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Ssw_SmlCountEqual
int Ssw_SmlCountEqual(Ssw_Sml_t *p, Aig_Obj_t *pObjLi, Aig_Obj_t *pObjLo)
Definition: sswSim.c:270
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Ssw_SmlUnnormalize
void Ssw_SmlUnnormalize(Ssw_Sml_t *p)
Definition: sswSim.c:1044
Ssw_Sml_t_::nFrames
int nFrames
Definition: sswSim.c:35
Ssw_Sml_t_::timeSim
abctime timeSim
Definition: sswSim.c:41
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Ssw_SmlNodeCountOnesRealVec
int Ssw_SmlNodeCountOnesRealVec(Ssw_Sml_t *p, Vec_Ptr_t *vObjs)
Definition: sswSim.c:362
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
Ssw_SmlGetCounterExample
Abc_Cex_t * Ssw_SmlGetCounterExample(Ssw_Sml_t *p)
Definition: sswSim.c:1338
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Ssw_SmlStop
void Ssw_SmlStop(Ssw_Sml_t *p)
Definition: sswSim.c:1211
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Ssw_SmlSimulateComb
Ssw_Sml_t * Ssw_SmlSimulateComb(Aig_Man_t *pAig, int nWords)
Definition: sswSim.c:1228
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Ssw_SmlNodeCopyFanin
void Ssw_SmlNodeCopyFanin(Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: sswSim.c:803
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Ssw_SmlInitialize
void Ssw_SmlInitialize(Ssw_Sml_t *p, int fInit)
Definition: sswSim.c:895
Ssw_SmlObjsAreEqualWord
int Ssw_SmlObjsAreEqualWord(Ssw_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition: sswSim.c:124
Ssw_Sml_t_
DECLARATIONS ///.
Definition: sswSim.c:31
Ssw_SmlInitializeSpecial
void Ssw_SmlInitializeSpecial(Ssw_Sml_t *p, Vec_Int_t *vInit)
Definition: sswSim.c:928
Ssw_SmlNodeCountOnesReal
int Ssw_SmlNodeCountOnesReal(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:333
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91