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
Ssw_ObjSim(Ssw_Sml_t * p,int Id)45 static inline unsigned * Ssw_ObjSim( Ssw_Sml_t * p, int Id ) { return p->pData + p->nWordsTotal * Id; }
Ssw_ObjRandomSim()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 ***********************************************************************/
Ssw_SmlObjHashWord(Ssw_Sml_t * p,Aig_Obj_t * pObj)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 ***********************************************************************/
Ssw_SmlObjIsConstWord(Ssw_Sml_t * p,Aig_Obj_t * pObj)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 ***********************************************************************/
Ssw_SmlObjsAreEqualWord(Ssw_Sml_t * p,Aig_Obj_t * pObj0,Aig_Obj_t * pObj1)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 ***********************************************************************/
Ssw_SmlObjIsConstBit(void * p,Aig_Obj_t * pObj)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 ***********************************************************************/
Ssw_SmlObjsAreEqualBit(void * p,Aig_Obj_t * pObj0,Aig_Obj_t * pObj1)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 ***********************************************************************/
Ssw_SmlNodeNotEquWeight(Ssw_Sml_t * p,int Left,int Right)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 ***********************************************************************/
Ssw_SmlCheckXorImplication(Ssw_Sml_t * p,Aig_Obj_t * pObjLi,Aig_Obj_t * pObjLo,Aig_Obj_t * pCand)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 ***********************************************************************/
Ssw_SmlCountXorImplication(Ssw_Sml_t * p,Aig_Obj_t * pObjLi,Aig_Obj_t * pObjLo,Aig_Obj_t * pCand)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 ***********************************************************************/
Ssw_SmlCountEqual(Ssw_Sml_t * p,Aig_Obj_t * pObjLi,Aig_Obj_t * pObjLo)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 ***********************************************************************/
Ssw_SmlNodeIsZero(Ssw_Sml_t * p,Aig_Obj_t * pObj)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 ***********************************************************************/
Ssw_SmlNodeIsZeroFrame(Ssw_Sml_t * p,Aig_Obj_t * pObj,int f)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 ***********************************************************************/
Ssw_SmlNodeCountOnesReal(Ssw_Sml_t * p,Aig_Obj_t * pObj)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 ***********************************************************************/
Ssw_SmlNodeCountOnesRealVec(Ssw_Sml_t * p,Vec_Ptr_t * vObjs)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 ***********************************************************************/
Ssw_SmlSavePattern0(Ssw_Man_t * p,int fInit)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 ***********************************************************************/
Ssw_SmlSavePattern1(Ssw_Man_t * p,int fInit)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 ***********************************************************************/
Ssw_SmlCheckOutputSavePattern(Ssw_Sml_t * p,Aig_Obj_t * pObjPo)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 ***********************************************************************/
Ssw_SmlCheckOutput(Ssw_Sml_t * p)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 ***********************************************************************/
Ssw_SmlAssignRandom(Ssw_Sml_t * p,Aig_Obj_t * pObj)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 ***********************************************************************/
Ssw_SmlAssignRandomFrame(Ssw_Sml_t * p,Aig_Obj_t * pObj,int iFrame)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 ***********************************************************************/
Ssw_SmlObjAssignConst(Ssw_Sml_t * p,Aig_Obj_t * pObj,int fConst1,int iFrame)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 ***********************************************************************/
Ssw_SmlObjAssignConstWord(Ssw_Sml_t * p,Aig_Obj_t * pObj,int fConst1,int iFrame,int iWord)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 ***********************************************************************/
Ssw_SmlObjSetWord(Ssw_Sml_t * p,Aig_Obj_t * pObj,unsigned Word,int iWord,int iFrame)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 ***********************************************************************/
Ssw_SmlAssignDist1(Ssw_Sml_t * p,unsigned * pPat)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 ***********************************************************************/
Ssw_SmlAssignDist1Plus(Ssw_Sml_t * p,unsigned * pPat)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 ***********************************************************************/
Ssw_SmlNodeSimulate(Ssw_Sml_t * p,Aig_Obj_t * pObj,int iFrame)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 ***********************************************************************/
Ssw_SmlNodesCompareInFrame(Ssw_Sml_t * p,Aig_Obj_t * pObj0,Aig_Obj_t * pObj1,int iFrame0,int iFrame1)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 ***********************************************************************/
Ssw_SmlNodeCopyFanin(Ssw_Sml_t * p,Aig_Obj_t * pObj,int iFrame)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 ***********************************************************************/
Ssw_SmlNodeTransferNext(Ssw_Sml_t * p,Aig_Obj_t * pOut,Aig_Obj_t * pIn,int iFrame)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 ***********************************************************************/
Ssw_SmlNodeTransferFirst(Ssw_Sml_t * p,Aig_Obj_t * pOut,Aig_Obj_t * pIn)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 ***********************************************************************/
Ssw_SmlInitialize(Ssw_Sml_t * p,int fInit)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 ***********************************************************************/
Ssw_SmlInitializeSpecial(Ssw_Sml_t * p,Vec_Int_t * vInit)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 ***********************************************************************/
Ssw_SmlReinitialize(Ssw_Sml_t * p)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 ***********************************************************************/
Ssw_SmlCheckNonConstOutputs(Ssw_Sml_t * p)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 ***********************************************************************/
Ssw_SmlSimulateOne(Ssw_Sml_t * p)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 ***********************************************************************/
Ssw_SmlUnnormalize(Ssw_Sml_t * p)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 ***********************************************************************/
Ssw_SmlSimulateOneDyn_rec(Ssw_Sml_t * p,Aig_Obj_t * pObj,int f,int * pVisited,int nVisCounter)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 ***********************************************************************/
Ssw_SmlSimulateOneFrame(Ssw_Sml_t * p)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 ***********************************************************************/
Ssw_SmlStart(Aig_Man_t * pAig,int nPref,int nFrames,int nWordsFrame)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 ***********************************************************************/
Ssw_SmlClean(Ssw_Sml_t * p)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 ***********************************************************************/
Ssw_SmlSimDataPointers(Ssw_Sml_t * p)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 ***********************************************************************/
Ssw_SmlStop(Ssw_Sml_t * p)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 ***********************************************************************/
Ssw_SmlSimulateComb(Aig_Man_t * pAig,int nWords)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 ***********************************************************************/
Ssw_SmlSimulateSeq(Aig_Man_t * pAig,int nPref,int nFrames,int nWords)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 ***********************************************************************/
Ssw_SmlResimulateSeq(Ssw_Sml_t * p)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 ***********************************************************************/
Ssw_SmlNumFrames(Ssw_Sml_t * p)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 ***********************************************************************/
Ssw_SmlNumWordsTotal(Ssw_Sml_t * p)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 ***********************************************************************/
Ssw_SmlSimInfo(Ssw_Sml_t * p,Aig_Obj_t * pObj)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 ***********************************************************************/
Ssw_SmlGetCounterExample(Ssw_Sml_t * p)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
1407