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