1 /**CFile****************************************************************
2
3 FileName [sswRarity.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Inductive prover with constraints.]
8
9 Synopsis [Rarity-driven refinement of equivalence classes.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - September 1, 2008.]
16
17 Revision [$Id: sswRarity.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "sswInt.h"
22 #include "aig/gia/giaAig.h"
23 #include "base/main/main.h"
24 #include "sat/bmc/bmc.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 typedef struct Ssw_RarMan_t_ Ssw_RarMan_t;
34 struct Ssw_RarMan_t_
35 {
36 // parameters
37 Ssw_RarPars_t* pPars;
38 int nGroups; // the number of flop groups
39 int nWordsReg; // the number of words in the registers
40 // internal data
41 Aig_Man_t * pAig; // AIG with equivalence classes
42 Ssw_Cla_t * ppClasses; // equivalence classes
43 Vec_Int_t * vInits; // initial state
44 // simulation data
45 word * pObjData; // simulation info for each obj
46 word * pPatData; // pattern data for each reg
47 // candidates to update
48 Vec_Ptr_t * vUpdConst; // constant 1 candidates
49 Vec_Ptr_t * vUpdClass; // class representatives
50 // rarity data
51 int * pRarity; // occur counts for patterns in groups
52 double * pPatCosts; // pattern costs
53 // best patterns
54 Vec_Int_t * vPatBests; // best patterns
55 int iFailPo; // failed primary output
56 int iFailPat; // failed pattern
57 // counter-examples
58 Vec_Ptr_t * vCexes;
59 };
60
61
Ssw_RarGetBinPat(Ssw_RarMan_t * p,int iBin,int iPat)62 static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
63 {
64 assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize );
65 assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) );
66 return p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat];
67 }
Ssw_RarSetBinPat(Ssw_RarMan_t * p,int iBin,int iPat,int Value)68 static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value )
69 {
70 assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize );
71 assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) );
72 p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat] = Value;
73 }
Ssw_RarAddToBinPat(Ssw_RarMan_t * p,int iBin,int iPat)74 static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
75 {
76 assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize );
77 assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) );
78 p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat]++;
79 }
80
Ssw_RarBitWordNum(int nBits)81 static inline int Ssw_RarBitWordNum( int nBits ) { return (nBits>>6) + ((nBits&63) > 0); }
82
Ssw_RarObjSim(Ssw_RarMan_t * p,int Id)83 static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id ) { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->pPars->nWords * Id; }
Ssw_RarPatSim(Ssw_RarMan_t * p,int Id)84 static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 64 * p->pPars->nWords ); return p->pPatData + p->nWordsReg * Id; }
85
86
87 ////////////////////////////////////////////////////////////////////////
88 /// FUNCTION DEFINITIONS ///
89 ////////////////////////////////////////////////////////////////////////
90
91 /**Function*************************************************************
92
93 Synopsis []
94
95 Description []
96
97 SideEffects []
98
99 SeeAlso []
100
101 ***********************************************************************/
Ssw_RarSetDefaultParams(Ssw_RarPars_t * p)102 void Ssw_RarSetDefaultParams( Ssw_RarPars_t * p )
103 {
104 memset( p, 0, sizeof(Ssw_RarPars_t) );
105 p->nFrames = 20;
106 p->nWords = 50;
107 p->nBinSize = 8;
108 p->nRounds = 0;
109 p->nRestart = 0;
110 p->nRandSeed = 0;
111 p->TimeOut = 0;
112 p->TimeOutGap = 0;
113 p->fSolveAll = 0;
114 p->fDropSatOuts = 0;
115 p->fSetLastState = 0;
116 p->fVerbose = 0;
117 p->fNotVerbose = 0;
118 }
119
120 /**Function*************************************************************
121
122 Synopsis [Prepares random number generator.]
123
124 Description []
125
126 SideEffects []
127
128 SeeAlso []
129
130 ***********************************************************************/
Ssw_RarManPrepareRandom(int nRandSeed)131 void Ssw_RarManPrepareRandom( int nRandSeed )
132 {
133 int i;
134 Aig_ManRandom( 1 );
135 for ( i = 0; i < nRandSeed; i++ )
136 Aig_ManRandom( 0 );
137 }
138
139 /**Function*************************************************************
140
141 Synopsis [Initializes random primary inputs.]
142
143 Description []
144
145 SideEffects []
146
147 SeeAlso []
148
149 ***********************************************************************/
Ssw_RarManAssingRandomPis(Ssw_RarMan_t * p)150 void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p )
151 {
152 word * pSim;
153 Aig_Obj_t * pObj;
154 int w, i;
155 Saig_ManForEachPi( p->pAig, pObj, i )
156 {
157 pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
158 for ( w = 0; w < p->pPars->nWords; w++ )
159 pSim[w] = Aig_ManRandom64(0);
160 // pSim[0] <<= 1;
161 // pSim[0] = (pSim[0] << 2) | 2;
162 pSim[0] = (pSim[0] << 4) | ((i & 1) ? 0xA : 0xC);
163 }
164 }
165
166 /**Function*************************************************************
167
168 Synopsis [Derives the counter-example.]
169
170 Description []
171
172 SideEffects []
173
174 SeeAlso []
175
176 ***********************************************************************/
Ssw_RarDeriveCex(Ssw_RarMan_t * p,int iFrame,int iPo,int iPatFinal,int fVerbose)177 Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFinal, int fVerbose )
178 {
179 Abc_Cex_t * pCex;
180 Aig_Obj_t * pObj;
181 Vec_Int_t * vTrace;
182 word * pSim;
183 int i, r, f, iBit, iPatThis;
184 // compute the pattern sequence
185 iPatThis = iPatFinal;
186 vTrace = Vec_IntStartFull( iFrame / p->pPars->nFrames + 1 );
187 Vec_IntWriteEntry( vTrace, iFrame / p->pPars->nFrames, iPatThis );
188 for ( r = iFrame / p->pPars->nFrames - 1; r >= 0; r-- )
189 {
190 iPatThis = Vec_IntEntry( p->vPatBests, r * p->pPars->nWords + iPatThis / 64 );
191 Vec_IntWriteEntry( vTrace, r, iPatThis );
192 }
193 // create counter-example
194 pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), iFrame+1 );
195 pCex->iFrame = iFrame;
196 pCex->iPo = iPo;
197 // insert the bits
198 iBit = Aig_ManRegNum(p->pAig);
199 for ( f = 0; f <= iFrame; f++ )
200 {
201 Ssw_RarManAssingRandomPis( p );
202 iPatThis = Vec_IntEntry( vTrace, f / p->pPars->nFrames );
203 Saig_ManForEachPi( p->pAig, pObj, i )
204 {
205 pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
206 if ( Abc_InfoHasBit( (unsigned *)pSim, iPatThis ) )
207 Abc_InfoSetBit( pCex->pData, iBit );
208 iBit++;
209 }
210 }
211 Vec_IntFree( vTrace );
212 assert( iBit == pCex->nBits );
213 // verify the counter example
214 if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
215 {
216 Abc_Print( 1, "Ssw_RarDeriveCex(): Counter-example is invalid.\n" );
217 // Abc_CexFree( pCex );
218 // pCex = NULL;
219 }
220 else
221 {
222 // Abc_Print( 1, "Counter-example verification is successful.\n" );
223 }
224 return pCex;
225 }
226
227
228 /**Function*************************************************************
229
230 Synopsis [Transposing 32-bit matrix.]
231
232 Description [Borrowed from "Hacker's Delight", by Henry Warren.]
233
234 SideEffects []
235
236 SeeAlso []
237
238 ***********************************************************************/
transpose32(unsigned A[32])239 void transpose32( unsigned A[32] )
240 {
241 int j, k;
242 unsigned t, m = 0x0000FFFF;
243 for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) )
244 {
245 for ( k = 0; k < 32; k = (k + j + 1) & ~j )
246 {
247 t = (A[k] ^ (A[k+j] >> j)) & m;
248 A[k] = A[k] ^ t;
249 A[k+j] = A[k+j] ^ (t << j);
250 }
251 }
252 }
253
254 /**Function*************************************************************
255
256 Synopsis [Transposing 64-bit matrix.]
257
258 Description []
259
260 SideEffects []
261
262 SeeAlso []
263
264 ***********************************************************************/
transpose64(word A[64])265 void transpose64( word A[64] )
266 {
267 int j, k;
268 word t, m = 0x00000000FFFFFFFF;
269 for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) )
270 {
271 for ( k = 0; k < 64; k = (k + j + 1) & ~j )
272 {
273 t = (A[k] ^ (A[k+j] >> j)) & m;
274 A[k] = A[k] ^ t;
275 A[k+j] = A[k+j] ^ (t << j);
276 }
277 }
278 }
279
280 /**Function*************************************************************
281
282 Synopsis [Transposing 64-bit matrix.]
283
284 Description []
285
286 SideEffects []
287
288 SeeAlso []
289
290 ***********************************************************************/
transpose64Simple(word A[64],word B[64])291 void transpose64Simple( word A[64], word B[64] )
292 {
293 int i, k;
294 for ( i = 0; i < 64; i++ )
295 B[i] = 0;
296 for ( i = 0; i < 64; i++ )
297 for ( k = 0; k < 64; k++ )
298 if ( (A[i] >> k) & 1 )
299 B[k] |= ((word)1 << (63-i));
300 }
301
302 /**Function*************************************************************
303
304 Synopsis [Testing the transposing code.]
305
306 Description []
307
308 SideEffects []
309
310 SeeAlso []
311
312 ***********************************************************************/
TransposeTest()313 void TransposeTest()
314 {
315 word M[64], N[64];
316 int i;
317 abctime clk;
318 Aig_ManRandom64( 1 );
319 // for ( i = 0; i < 64; i++ )
320 // M[i] = Aig_ManRandom64( 0 );
321 for ( i = 0; i < 64; i++ )
322 M[i] = i? (word)0 : ~(word)0;
323 // for ( i = 0; i < 64; i++ )
324 // Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" );
325
326 clk = Abc_Clock();
327 for ( i = 0; i < 100001; i++ )
328 transpose64Simple( M, N );
329 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
330
331 clk = Abc_Clock();
332 for ( i = 0; i < 100001; i++ )
333 transpose64( M );
334 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
335
336 for ( i = 0; i < 64; i++ )
337 if ( M[i] != N[i] )
338 Abc_Print( 1, "Mismatch\n" );
339 /*
340 Abc_Print( 1, "\n" );
341 for ( i = 0; i < 64; i++ )
342 Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" );
343 Abc_Print( 1, "\n" );
344 for ( i = 0; i < 64; i++ )
345 Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), Abc_Print( 1, "\n" );
346 */
347 }
348
349 /**Function*************************************************************
350
351 Synopsis [Transposing pObjData[ nRegs x nWords ] -> pPatData[ nWords x nRegs ].]
352
353 Description []
354
355 SideEffects []
356
357 SeeAlso []
358
359 ***********************************************************************/
Ssw_RarTranspose(Ssw_RarMan_t * p)360 void Ssw_RarTranspose( Ssw_RarMan_t * p )
361 {
362 Aig_Obj_t * pObj;
363 word M[64];
364 int w, r, i;
365 for ( w = 0; w < p->pPars->nWords; w++ )
366 for ( r = 0; r < p->nWordsReg; r++ )
367 {
368 // save input
369 for ( i = 0; i < 64; i++ )
370 {
371 if ( r*64 + 63-i < Aig_ManRegNum(p->pAig) )
372 {
373 pObj = Saig_ManLi( p->pAig, r*64 + 63-i );
374 M[i] = Ssw_RarObjSim( p, Aig_ObjId(pObj) )[w];
375 }
376 else
377 M[i] = 0;
378 }
379 // transpose
380 transpose64( M );
381 // save output
382 for ( i = 0; i < 64; i++ )
383 Ssw_RarPatSim( p, w*64 + 63-i )[r] = M[i];
384 }
385 /*
386 Saig_ManForEachLi( p->pAig, pObj, i )
387 {
388 word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
389 Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->pPars->nWords ); Abc_Print( 1, "\n" );
390 }
391 Abc_Print( 1, "\n" );
392 for ( i = 0; i < p->pPars->nWords*64; i++ )
393 {
394 word * pBitData = Ssw_RarPatSim( p, i );
395 Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); Abc_Print( 1, "\n" );
396 }
397 Abc_Print( 1, "\n" );
398 */
399 }
400
401
402
403
404 /**Function*************************************************************
405
406 Synopsis [Sets random inputs and specialied flop outputs.]
407
408 Description []
409
410 SideEffects []
411
412 SeeAlso []
413
414 ***********************************************************************/
Ssw_RarManInitialize(Ssw_RarMan_t * p,Vec_Int_t * vInit)415 void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
416 {
417 Aig_Obj_t * pObj, * pObjLi;
418 word * pSim, * pSimLi;
419 int w, i;
420 // constant
421 pObj = Aig_ManConst1( p->pAig );
422 pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
423 for ( w = 0; w < p->pPars->nWords; w++ )
424 pSim[w] = ~(word)0;
425 // primary inputs
426 Ssw_RarManAssingRandomPis( p );
427 // flop outputs
428 if ( vInit )
429 {
430 assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->pPars->nWords );
431 Saig_ManForEachLo( p->pAig, pObj, i )
432 {
433 pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
434 for ( w = 0; w < p->pPars->nWords; w++ )
435 pSim[w] = Vec_IntEntry(vInit, w * Saig_ManRegNum(p->pAig) + i) ? ~(word)0 : (word)0;
436 }
437 }
438 else
439 {
440 Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
441 {
442 pSimLi = Ssw_RarObjSim( p, Aig_ObjId(pObjLi) );
443 pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
444 for ( w = 0; w < p->pPars->nWords; w++ )
445 pSim[w] = pSimLi[w];
446 }
447 }
448 }
449
450 /**Function*************************************************************
451
452 Synopsis [Returns 1 if simulation info is composed of all zeros.]
453
454 Description []
455
456 SideEffects []
457
458 SeeAlso []
459
460 ***********************************************************************/
Ssw_RarManPoIsConst0(void * pMan,Aig_Obj_t * pObj)461 int Ssw_RarManPoIsConst0( void * pMan, Aig_Obj_t * pObj )
462 {
463 Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
464 word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
465 int w;
466 for ( w = 0; w < p->pPars->nWords; w++ )
467 if ( pSim[w] )
468 return 0;
469 return 1;
470 }
471
472 /**Function*************************************************************
473
474 Synopsis [Returns 1 if simulation info is composed of all zeros.]
475
476 Description []
477
478 SideEffects []
479
480 SeeAlso []
481
482 ***********************************************************************/
Ssw_RarManObjIsConst(void * pMan,Aig_Obj_t * pObj)483 int Ssw_RarManObjIsConst( void * pMan, Aig_Obj_t * pObj )
484 {
485 Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
486 word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
487 word Flip = pObj->fPhase ? ~(word)0 : 0;
488 int w;
489 for ( w = 0; w < p->pPars->nWords; w++ )
490 if ( pSim[w] ^ Flip )
491 return 0;
492 return 1;
493 }
494
495 /**Function*************************************************************
496
497 Synopsis [Returns 1 if simulation infos are equal.]
498
499 Description []
500
501 SideEffects []
502
503 SeeAlso []
504
505 ***********************************************************************/
Ssw_RarManObjsAreEqual(void * pMan,Aig_Obj_t * pObj0,Aig_Obj_t * pObj1)506 int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
507 {
508 Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
509 word * pSim0 = Ssw_RarObjSim( p, pObj0->Id );
510 word * pSim1 = Ssw_RarObjSim( p, pObj1->Id );
511 word Flip = (pObj0->fPhase != pObj1->fPhase) ? ~(word)0 : 0;
512 int w;
513 for ( w = 0; w < p->pPars->nWords; w++ )
514 if ( pSim0[w] ^ pSim1[w] ^ Flip )
515 return 0;
516 return 1;
517 }
518
519 /**Function*************************************************************
520
521 Synopsis [Computes hash value of the node using its simulation info.]
522
523 Description []
524
525 SideEffects []
526
527 SeeAlso []
528
529 ***********************************************************************/
Ssw_RarManObjHashWord(void * pMan,Aig_Obj_t * pObj)530 unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj )
531 {
532 Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
533 static int s_SPrimes[128] = {
534 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
535 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
536 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
537 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
538 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
539 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
540 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
541 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
542 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
543 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
544 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
545 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
546 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
547 };
548 unsigned * pSims;
549 unsigned uHash;
550 int i;
551 uHash = 0;
552 pSims = (unsigned *)Ssw_RarObjSim( p, pObj->Id );
553 for ( i = 0; i < 2 * p->pPars->nWords; i++ )
554 uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
555 return uHash;
556 }
557
558 /**Function*************************************************************
559
560 Synopsis [Returns 1 if simulation info is composed of all zeros.]
561
562 Description []
563
564 SideEffects []
565
566 SeeAlso []
567
568 ***********************************************************************/
Ssw_RarManObjWhichOne(Ssw_RarMan_t * p,Aig_Obj_t * pObj)569 int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
570 {
571 word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
572 word Flip = 0;//pObj->fPhase ? ~(word)0 : 0; // bug fix!
573 int w, i;
574 for ( w = 0; w < p->pPars->nWords; w++ )
575 if ( pSim[w] ^ Flip )
576 {
577 for ( i = 0; i < 64; i++ )
578 if ( ((pSim[w] ^ Flip) >> i) & 1 )
579 break;
580 assert( i < 64 );
581 return w * 64 + i;
582 }
583 return -1;
584 }
585
586 /**Function*************************************************************
587
588 Synopsis [Check if any of the POs becomes non-constant.]
589
590 Description []
591
592 SideEffects []
593
594 SeeAlso []
595
596 ***********************************************************************/
Ssw_RarManCheckNonConstOutputs(Ssw_RarMan_t * p,int iFrame,abctime Time)597 int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int iFrame, abctime Time )
598 {
599 Aig_Obj_t * pObj;
600 int i;
601 p->iFailPo = -1;
602 p->iFailPat = -1;
603 Saig_ManForEachPo( p->pAig, pObj, i )
604 {
605 if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
606 break;
607 if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
608 continue;
609 if ( Ssw_RarManPoIsConst0(p, pObj) )
610 continue;
611 p->iFailPo = i;
612 p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
613 if ( !p->pPars->fSolveAll )
614 break;
615 // remember the one solved
616 p->pPars->nSolved++;
617 if ( p->vCexes == NULL )
618 p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
619 assert( Vec_PtrEntry(p->vCexes, i) == NULL );
620 Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 );
621 if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(i, NULL) )
622 return 2; // quitting due to callback
623 // print final report
624 if ( !p->pPars->fNotVerbose )
625 {
626 int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
627 Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ",
628 nOutDigits, p->iFailPo, iFrame,
629 nOutDigits, p->pPars->nSolved,
630 nOutDigits, Saig_ManPoNum(p->pAig) );
631 Abc_PrintTime( 1, "Time", Time );
632 }
633 }
634 if ( p->iFailPo >= 0 ) // found CEX
635 return 1;
636 else
637 return 0;
638 }
639
640 /**Function*************************************************************
641
642 Synopsis [Performs one round of simulation.]
643
644 Description []
645
646 SideEffects []
647
648 SeeAlso []
649
650 ***********************************************************************/
Ssw_RarManSimulate(Ssw_RarMan_t * p,Vec_Int_t * vInit,int fUpdate,int fFirst)651 void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int fFirst )
652 {
653 Aig_Obj_t * pObj, * pRepr;
654 word * pSim, * pSim0, * pSim1;
655 word Flip, Flip0, Flip1;
656 int w, i;
657 // initialize
658 Ssw_RarManInitialize( p, vInit );
659 Vec_PtrClear( p->vUpdConst );
660 Vec_PtrClear( p->vUpdClass );
661 Aig_ManIncrementTravId( p->pAig );
662 // check comb inputs
663 if ( fUpdate )
664 Aig_ManForEachCi( p->pAig, pObj, i )
665 {
666 pRepr = Aig_ObjRepr(p->pAig, pObj);
667 if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
668 continue;
669 if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
670 continue;
671 // save for update
672 if ( pRepr == Aig_ManConst1(p->pAig) )
673 Vec_PtrPush( p->vUpdConst, pObj );
674 else
675 {
676 Vec_PtrPush( p->vUpdClass, pRepr );
677 Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
678 }
679 }
680 // simulate
681 Aig_ManForEachNode( p->pAig, pObj, i )
682 {
683 pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
684 pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
685 pSim1 = Ssw_RarObjSim( p, Aig_ObjFaninId1(pObj) );
686 Flip0 = Aig_ObjFaninC0(pObj) ? ~(word)0 : 0;
687 Flip1 = Aig_ObjFaninC1(pObj) ? ~(word)0 : 0;
688 for ( w = 0; w < p->pPars->nWords; w++ )
689 pSim[w] = (Flip0 ^ pSim0[w]) & (Flip1 ^ pSim1[w]);
690
691
692 if ( !fUpdate )
693 continue;
694 // check classes
695 pRepr = Aig_ObjRepr(p->pAig, pObj);
696 if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
697 continue;
698 if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
699 continue;
700 // save for update
701 if ( pRepr == Aig_ManConst1(p->pAig) )
702 Vec_PtrPush( p->vUpdConst, pObj );
703 else
704 {
705 Vec_PtrPush( p->vUpdClass, pRepr );
706 Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
707 }
708 }
709 // transfer to POs
710 Aig_ManForEachCo( p->pAig, pObj, i )
711 {
712 pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
713 pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
714 Flip = Aig_ObjFaninC0(pObj) ? ~(word)0 : 0;
715 for ( w = 0; w < p->pPars->nWords; w++ )
716 pSim[w] = Flip ^ pSim0[w];
717 }
718 // refine classes
719 if ( fUpdate )
720 {
721 if ( fFirst )
722 {
723 Vec_Ptr_t * vCands = Vec_PtrAlloc( 1000 );
724 Aig_ManForEachObj( p->pAig, pObj, i )
725 if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
726 Vec_PtrPush( vCands, pObj );
727 assert( Vec_PtrSize(vCands) == Ssw_ClassesCand1Num(p->ppClasses) );
728 Ssw_ClassesPrepareRehash( p->ppClasses, vCands, 0 );
729 Vec_PtrFree( vCands );
730 }
731 else
732 {
733 Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 );
734 Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 );
735 }
736 }
737 }
738
739
740 /**Function*************************************************************
741
742 Synopsis []
743
744 Description []
745
746 SideEffects []
747
748 SeeAlso []
749
750 ***********************************************************************/
Ssw_RarManStart(Aig_Man_t * pAig,Ssw_RarPars_t * pPars)751 static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
752 {
753 Ssw_RarMan_t * p;
754 // if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
755 // return NULL;
756 p = ABC_CALLOC( Ssw_RarMan_t, 1 );
757 p->pAig = pAig;
758 p->pPars = pPars;
759 p->nGroups = Aig_ManRegNum(pAig) / pPars->nBinSize;
760 p->pRarity = ABC_CALLOC( int, (1 << pPars->nBinSize) * p->nGroups );
761 p->pPatCosts = ABC_CALLOC( double, p->pPars->nWords * 64 );
762 p->nWordsReg = Ssw_RarBitWordNum( Aig_ManRegNum(pAig) );
763 p->pObjData = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->pPars->nWords );
764 p->pPatData = ABC_ALLOC( word, 64 * p->pPars->nWords * p->nWordsReg );
765 p->vUpdConst = Vec_PtrAlloc( 100 );
766 p->vUpdClass = Vec_PtrAlloc( 100 );
767 p->vPatBests = Vec_IntAlloc( 100 );
768 return p;
769 }
770
771 /**Function*************************************************************
772
773 Synopsis []
774
775 Description []
776
777 SideEffects []
778
779 SeeAlso []
780
781 ***********************************************************************/
Ssw_RarManStop(Ssw_RarMan_t * p)782 static void Ssw_RarManStop( Ssw_RarMan_t * p )
783 {
784 // Vec_PtrFreeP( &p->vCexes );
785 if ( p->vCexes )
786 {
787 assert( p->pAig->vSeqModelVec == NULL );
788 p->pAig->vSeqModelVec = p->vCexes;
789 p->vCexes = NULL;
790 }
791 if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
792 Vec_IntFreeP( &p->vInits );
793 Vec_IntFreeP( &p->vPatBests );
794 Vec_PtrFreeP( &p->vUpdConst );
795 Vec_PtrFreeP( &p->vUpdClass );
796 ABC_FREE( p->pObjData );
797 ABC_FREE( p->pPatData );
798 ABC_FREE( p->pPatCosts );
799 ABC_FREE( p->pRarity );
800 ABC_FREE( p );
801 }
802
803 /**Function*************************************************************
804
805 Synopsis [Select best patterns.]
806
807 Description []
808
809 SideEffects []
810
811 SeeAlso []
812
813 ***********************************************************************/
Ssw_RarTransferPatterns(Ssw_RarMan_t * p,Vec_Int_t * vInits)814 static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
815 {
816 // Aig_Obj_t * pObj;
817 unsigned char * pData;
818 unsigned * pPattern;
819 int i, k, Value;
820
821 // more data from regs to pats
822 Ssw_RarTranspose( p );
823
824 // update counters
825 for ( k = 0; k < p->pPars->nWords * 64; k++ )
826 {
827 pData = (unsigned char *)Ssw_RarPatSim( p, k );
828 for ( i = 0; i < p->nGroups; i++ )
829 Ssw_RarAddToBinPat( p, i, pData[i] );
830 }
831
832 // for each pattern
833 for ( k = 0; k < p->pPars->nWords * 64; k++ )
834 {
835 pData = (unsigned char *)Ssw_RarPatSim( p, k );
836 // find the cost of its values
837 p->pPatCosts[k] = 0.0;
838 for ( i = 0; i < p->nGroups; i++ )
839 {
840 Value = Ssw_RarGetBinPat( p, i, pData[i] );
841 assert( Value > 0 );
842 p->pPatCosts[k] += 1.0/(Value*Value);
843 }
844 // print the result
845 //Abc_Print( 1, "%3d : %9.6f\n", k, p->pPatCosts[k] );
846 }
847
848 // choose as many as there are words
849 Vec_IntClear( vInits );
850 for ( i = 0; i < p->pPars->nWords; i++ )
851 {
852 // select the best
853 int iPatBest = -1;
854 double iCostBest = -ABC_INFINITY;
855 for ( k = 0; k < p->pPars->nWords * 64; k++ )
856 if ( iCostBest < p->pPatCosts[k] )
857 {
858 iCostBest = p->pPatCosts[k];
859 iPatBest = k;
860 }
861 // remove from costs
862 assert( iPatBest >= 0 );
863 p->pPatCosts[iPatBest] = -ABC_INFINITY;
864 // set the flops
865 pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest );
866 for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ )
867 Vec_IntPush( vInits, Abc_InfoHasBit(pPattern, k) );
868 //Abc_Print( 1, "Best pattern %5d\n", iPatBest );
869 Vec_IntPush( p->vPatBests, iPatBest );
870 }
871 assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->pPars->nWords );
872 }
873
874
875 /**Function*************************************************************
876
877 Synopsis [Performs fraiging for one node.]
878
879 Description [Returns the fraiged node.]
880
881 SideEffects []
882
883 SeeAlso []
884
885 ***********************************************************************/
Ssw_RarFindStartingState(Aig_Man_t * pAig,Abc_Cex_t * pCex)886 static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
887 {
888 Vec_Int_t * vInit;
889 Aig_Obj_t * pObj, * pObjLi;
890 int f, i, iBit;
891 // assign register outputs
892 Saig_ManForEachLi( pAig, pObj, i )
893 pObj->fMarkB = Abc_InfoHasBit( pCex->pData, i );
894 // simulate the timeframes
895 iBit = pCex->nRegs;
896 for ( f = 0; f <= pCex->iFrame; f++ )
897 {
898 // set the PI simulation information
899 Aig_ManConst1(pAig)->fMarkB = 1;
900 Saig_ManForEachPi( pAig, pObj, i )
901 pObj->fMarkB = Abc_InfoHasBit( pCex->pData, iBit++ );
902 Saig_ManForEachLiLo( pAig, pObjLi, pObj, i )
903 pObj->fMarkB = pObjLi->fMarkB;
904 // simulate internal nodes
905 Aig_ManForEachNode( pAig, pObj, i )
906 pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
907 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
908 // assign the COs
909 Aig_ManForEachCo( pAig, pObj, i )
910 pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
911 }
912 assert( iBit == pCex->nBits );
913 // check that the output failed as expected -- cannot check because it is not an SRM!
914 // pObj = Aig_ManCo( pAig, pCex->iPo );
915 // if ( pObj->fMarkB != 1 )
916 // Abc_Print( 1, "The counter-example does not refine the output.\n" );
917 // record the new pattern
918 vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) );
919 Saig_ManForEachLo( pAig, pObj, i )
920 {
921 //Abc_Print( 1, "%d", pObj->fMarkB );
922 Vec_IntPush( vInit, pObj->fMarkB );
923 }
924 //Abc_Print( 1, "\n" );
925 Aig_ManCleanMarkB( pAig );
926 return vInit;
927 }
928
929
930 /**Function*************************************************************
931
932 Synopsis []
933
934 Description []
935
936 SideEffects []
937
938 SeeAlso []
939
940 ***********************************************************************/
Ssw_RarCheckTrivial(Aig_Man_t * pAig,int fVerbose)941 int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose )
942 {
943 Aig_Obj_t * pObj;
944 int i;
945 Saig_ManForEachPo( pAig, pObj, i )
946 {
947 if ( pAig->nConstrs && i >= Saig_ManPoNum(pAig) - pAig->nConstrs )
948 return 0;
949 if ( pObj->fPhase )
950 {
951 ABC_FREE( pAig->pSeqModel );
952 pAig->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), 1 );
953 pAig->pSeqModel->iPo = i;
954 if ( fVerbose )
955 Abc_Print( 1, "Output %d is trivally SAT in frame 0. \n", i );
956 return 1;
957 }
958 }
959 return 0;
960 }
961
962 /**Function*************************************************************
963
964 Synopsis [Perform sequential simulation.]
965
966 Description []
967
968 SideEffects []
969
970 SeeAlso []
971
972 ***********************************************************************/
Ssw_RarSimulate(Aig_Man_t * pAig,Ssw_RarPars_t * pPars)973 int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
974 {
975 int fTryBmc = 0;
976 int fMiter = 1;
977 Ssw_RarMan_t * p;
978 int r, f = -1;
979 abctime clk, clkTotal = Abc_Clock();
980 abctime nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
981 abctime timeLastSolved = 0;
982 int nNumRestart = 0;
983 int nSavedSeed = pPars->nRandSeed;
984 int RetValue = -1;
985 int iFrameFail = -1;
986 assert( Aig_ManRegNum(pAig) > 0 );
987 assert( Aig_ManConstrNum(pAig) == 0 );
988 ABC_FREE( pAig->pSeqModel );
989 // consider the case of empty AIG
990 // if ( Aig_ManNodeNum(pAig) == 0 )
991 // return -1;
992 // check trivially SAT miters
993 // if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) )
994 // return 0;
995 if ( pPars->fVerbose )
996 Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d restart, %d seed, and %d sec timeout.\n",
997 pPars->nWords, pPars->nFrames, pPars->nRounds, pPars->nRestart, pPars->nRandSeed, pPars->TimeOut );
998 // reset random numbers
999 Ssw_RarManPrepareRandom( nSavedSeed );
1000
1001 // create manager
1002 p = Ssw_RarManStart( pAig, pPars );
1003 p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * pPars->nWords );
1004
1005 // perform simulation rounds
1006 pPars->nSolved = 0;
1007 timeLastSolved = Abc_Clock();
1008 for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
1009 {
1010 clk = Abc_Clock();
1011 if ( fTryBmc )
1012 {
1013 Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits );
1014 Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0, 0 );
1015 // if ( pNewAig->pSeqModel != NULL )
1016 // Abc_Print( 1, "BMC has found a counter-example in frame %d.\n", iFrameFail );
1017 Aig_ManStop( pNewAig );
1018 }
1019 // simulate
1020 for ( f = 0; f < pPars->nFrames; f++ )
1021 {
1022 Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
1023 if ( fMiter )
1024 {
1025 int Status = Ssw_RarManCheckNonConstOutputs(p, r * p->pPars->nFrames + f, Abc_Clock() - clkTotal);
1026 if ( Status == 2 )
1027 {
1028 Abc_Print( 1, "Quitting due to callback on fail.\n" );
1029 goto finish;
1030 }
1031 if ( Status == 1 ) // found CEX
1032 {
1033 RetValue = 0;
1034 if ( !pPars->fSolveAll )
1035 {
1036 if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
1037 // Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
1038 Ssw_RarManPrepareRandom( nSavedSeed );
1039 if ( pPars->fVerbose )
1040 Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
1041 pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, pPars->fVerbose );
1042 // print final report
1043 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
1044 Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
1045 goto finish;
1046 }
1047 timeLastSolved = Abc_Clock();
1048 }
1049 // else - did not find a counter example
1050 }
1051 // check timeout
1052 if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
1053 {
1054 if ( !pPars->fSilent )
1055 {
1056 if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
1057 Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved );
1058 Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut );
1059 }
1060 goto finish;
1061 }
1062 if ( pPars->TimeOutGap && timeLastSolved && Abc_Clock() > timeLastSolved + pPars->TimeOutGap * CLOCKS_PER_SEC )
1063 {
1064 if ( !pPars->fSilent )
1065 {
1066 if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
1067 Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved );
1068 Abc_Print( 1, "Reached gap timeout (%d sec).\n", pPars->TimeOutGap );
1069 }
1070 goto finish;
1071 }
1072 // check if all outputs are solved by now
1073 if ( pPars->fSolveAll && p->vCexes && Vec_PtrCountZero(p->vCexes) == 0 )
1074 goto finish;
1075 }
1076 // get initialization patterns
1077 if ( pPars->nRestart && r == pPars->nRestart )
1078 {
1079 r = -1;
1080 nSavedSeed = (nSavedSeed + 1) % 1000;
1081 Ssw_RarManPrepareRandom( nSavedSeed );
1082 Vec_IntFill( p->vInits, Aig_ManRegNum(pAig) * pPars->nWords, 0 );
1083 nNumRestart++;
1084 Vec_IntClear( p->vPatBests );
1085 // clean rarity info
1086 // memset( p->pRarity, 0, sizeof(int) * (1 << nBinSize) * p->nGroups );
1087 }
1088 else
1089 Ssw_RarTransferPatterns( p, p->vInits );
1090 // printout
1091 if ( pPars->fVerbose )
1092 {
1093 if ( pPars->fSolveAll )
1094 {
1095 Abc_Print( 1, "Starts =%6d ", nNumRestart );
1096 Abc_Print( 1, "Rounds =%6d ", nNumRestart * pPars->nRestart + ((r==-1)?0:r) );
1097 Abc_Print( 1, "Frames =%6d ", (nNumRestart * pPars->nRestart + r) * pPars->nFrames );
1098 Abc_Print( 1, "CEX =%6d (%6.2f %%) ", pPars->nSolved, 100.0*pPars->nSolved/Saig_ManPoNum(p->pAig) );
1099 Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
1100 }
1101 else
1102 Abc_Print( 1, "." );
1103 }
1104
1105 }
1106 finish:
1107 if ( pPars->fSetLastState && p->vInits )
1108 {
1109 assert( Vec_IntSize(p->vInits) % Aig_ManRegNum(pAig) == 0 );
1110 Vec_IntShrink( p->vInits, Aig_ManRegNum(pAig) );
1111 pAig->pData = p->vInits; p->vInits = NULL;
1112 }
1113 if ( pPars->nSolved )
1114 {
1115 /*
1116 if ( !pPars->fSilent )
1117 {
1118 if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
1119 Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved, Saig_ManPoNum(p->pAig) );
1120 Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
1121 }
1122 */
1123 }
1124 else if ( r == pPars->nRounds && f == pPars->nFrames )
1125 {
1126 if ( !pPars->fSilent )
1127 {
1128 if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
1129 Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
1130 Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
1131 }
1132 }
1133 // cleanup
1134 Ssw_RarManStop( p );
1135 return RetValue;
1136 }
1137
1138
1139 /**Function*************************************************************
1140
1141 Synopsis [Derive random flop permutation.]
1142
1143 Description []
1144
1145 SideEffects []
1146
1147 SeeAlso []
1148
1149 ***********************************************************************/
Ssw_RarRandomPermFlop(int nFlops,int nUnused)1150 Vec_Int_t * Ssw_RarRandomPermFlop( int nFlops, int nUnused )
1151 {
1152 Vec_Int_t * vPerm;
1153 int i, k, * pArray;
1154 srand( 1 );
1155 printf( "Generating random permutation of %d flops.\n", nFlops );
1156 vPerm = Vec_IntStartNatural( nFlops );
1157 pArray = Vec_IntArray( vPerm );
1158 for ( i = 0; i < nFlops; i++ )
1159 {
1160 k = rand() % nFlops;
1161 ABC_SWAP( int, pArray[i], pArray[k] );
1162 }
1163 printf( "Randomly adding %d unused flops.\n", nUnused );
1164 for ( i = 0; i < nUnused; i++ )
1165 {
1166 k = rand() % Vec_IntSize(vPerm);
1167 Vec_IntPush( vPerm, -1 );
1168 pArray = Vec_IntArray( vPerm );
1169 ABC_SWAP( int, pArray[Vec_IntSize(vPerm)-1], pArray[k] );
1170 }
1171 // Vec_IntPrint(vPerm);
1172 return vPerm;
1173 }
1174
1175 /**Function*************************************************************
1176
1177 Synopsis [Perform sequential simulation.]
1178
1179 Description []
1180
1181 SideEffects []
1182
1183 SeeAlso []
1184
1185 ***********************************************************************/
Ssw_RarSimulateGia(Gia_Man_t * p,Ssw_RarPars_t * pPars)1186 int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars )
1187 {
1188 Aig_Man_t * pAig;
1189 int RetValue;
1190 if ( pPars->fUseFfGrouping )
1191 {
1192 Vec_Int_t * vPerm = Ssw_RarRandomPermFlop( Gia_ManRegNum(p), 10 );
1193 Gia_Man_t * pTemp = Gia_ManDupPermFlopGap( p, vPerm );
1194 Vec_IntFree( vPerm );
1195 pAig = Gia_ManToAigSimple( pTemp );
1196 Gia_ManStop( pTemp );
1197 }
1198 else
1199 pAig = Gia_ManToAigSimple( p );
1200 RetValue = Ssw_RarSimulate( pAig, pPars );
1201 // save counter-example
1202 Abc_CexFree( p->pCexSeq );
1203 p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
1204 Aig_ManStop( pAig );
1205 return RetValue;
1206 }
1207
1208 /**Function*************************************************************
1209
1210 Synopsis [Filter equivalence classes of nodes.]
1211
1212 Description []
1213
1214 SideEffects []
1215
1216 SeeAlso []
1217
1218 ***********************************************************************/
Ssw_RarSignalFilter(Aig_Man_t * pAig,Ssw_RarPars_t * pPars)1219 int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
1220 {
1221 Ssw_RarMan_t * p;
1222 int r, f = -1, i, k;
1223 abctime clkTotal = Abc_Clock();
1224 abctime nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
1225 int nNumRestart = 0;
1226 int nSavedSeed = pPars->nRandSeed;
1227 int RetValue = -1;
1228 assert( Aig_ManRegNum(pAig) > 0 );
1229 assert( Aig_ManConstrNum(pAig) == 0 );
1230 // consider the case of empty AIG
1231 if ( Aig_ManNodeNum(pAig) == 0 )
1232 return -1;
1233 // check trivially SAT miters
1234 if ( pPars->fMiter && Ssw_RarCheckTrivial( pAig, 1 ) )
1235 return 0;
1236 if ( pPars->fVerbose )
1237 Abc_Print( 1, "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
1238 pPars->nWords, pPars->nFrames, pPars->nRounds, pPars->nRandSeed, pPars->TimeOut );
1239 // reset random numbers
1240 Ssw_RarManPrepareRandom( nSavedSeed );
1241
1242 // create manager
1243 p = Ssw_RarManStart( pAig, pPars );
1244 // compute starting state if needed
1245 assert( p->vInits == NULL );
1246 if ( pPars->pCex )
1247 {
1248 p->vInits = Ssw_RarFindStartingState( pAig, pPars->pCex );
1249 Abc_Print( 1, "Beginning simulation from the state derived using the counter-example.\n" );
1250 }
1251 else
1252 p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) );
1253 // duplicate the array
1254 for ( i = 1; i < pPars->nWords; i++ )
1255 for ( k = 0; k < Aig_ManRegNum(pAig); k++ )
1256 Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) );
1257 assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * pPars->nWords );
1258
1259 // create trivial equivalence classes with all nodes being candidates for constant 1
1260 if ( pAig->pReprs == NULL )
1261 p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchOnly, 0 );
1262 else
1263 p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
1264 Ssw_ClassesSetData( p->ppClasses, p, Ssw_RarManObjHashWord, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual );
1265 // print the stats
1266 if ( pPars->fVerbose )
1267 {
1268 Abc_Print( 1, "Initial : " );
1269 Ssw_ClassesPrint( p->ppClasses, 0 );
1270 }
1271 // refine classes using BMC
1272 for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
1273 {
1274 // start filtering equivalence classes
1275 if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
1276 {
1277 Abc_Print( 1, "All equivalences are refined away.\n" );
1278 break;
1279 }
1280 // simulate
1281 for ( f = 0; f < pPars->nFrames; f++ )
1282 {
1283 Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
1284 if ( pPars->fMiter && Ssw_RarManCheckNonConstOutputs(p, -1, 0) )
1285 {
1286 if ( !pPars->fVerbose )
1287 Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
1288 // Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * pPars->nFrames, (r+1) * pPars->nFrames );
1289 if ( pPars->fVerbose )
1290 Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
1291 Ssw_RarManPrepareRandom( nSavedSeed );
1292 Abc_CexFree( pAig->pSeqModel );
1293 pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, 1 );
1294 // print final report
1295 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
1296 Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
1297 RetValue = 0;
1298 goto finish;
1299 }
1300 // check timeout
1301 if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
1302 {
1303 if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
1304 Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
1305 Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut );
1306 goto finish;
1307 }
1308 }
1309 // get initialization patterns
1310 if ( pPars->pCex == NULL && pPars->nRestart && r == pPars->nRestart )
1311 {
1312 r = -1;
1313 nSavedSeed = (nSavedSeed + 1) % 1000;
1314 Ssw_RarManPrepareRandom( nSavedSeed );
1315 Vec_IntFill( p->vInits, Aig_ManRegNum(pAig) * pPars->nWords, 0 );
1316 nNumRestart++;
1317 Vec_IntClear( p->vPatBests );
1318 // clean rarity info
1319 // memset( p->pRarity, 0, sizeof(int) * (1 << nBinSize) * p->nGroups );
1320 }
1321 else
1322 Ssw_RarTransferPatterns( p, p->vInits );
1323 // printout
1324 if ( pPars->fVerbose )
1325 {
1326 Abc_Print( 1, "Round %3d: ", r );
1327 Ssw_ClassesPrint( p->ppClasses, 0 );
1328 }
1329 else
1330 {
1331 Abc_Print( 1, "." );
1332 }
1333 }
1334 finish:
1335 // report
1336 if ( r == pPars->nRounds && f == pPars->nFrames )
1337 {
1338 if ( !pPars->fVerbose )
1339 Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
1340 Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
1341 Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
1342 }
1343 // cleanup
1344 Ssw_RarManStop( p );
1345 return RetValue;
1346 }
1347
1348 /**Function*************************************************************
1349
1350 Synopsis [Filter equivalence classes of nodes.]
1351
1352 Description []
1353
1354 SideEffects []
1355
1356 SeeAlso []
1357
1358 ***********************************************************************/
Ssw_RarSignalFilterGia(Gia_Man_t * p,Ssw_RarPars_t * pPars)1359 int Ssw_RarSignalFilterGia( Gia_Man_t * p, Ssw_RarPars_t * pPars )
1360 {
1361 Aig_Man_t * pAig;
1362 int RetValue;
1363 pAig = Gia_ManToAigSimple( p );
1364 if ( p->pReprs != NULL )
1365 {
1366 Gia_ManReprToAigRepr2( pAig, p );
1367 ABC_FREE( p->pReprs );
1368 ABC_FREE( p->pNexts );
1369 }
1370 RetValue = Ssw_RarSignalFilter( pAig, pPars );
1371 Gia_ManReprFromAigRepr( pAig, p );
1372 // save counter-example
1373 Abc_CexFree( p->pCexSeq );
1374 p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
1375 Aig_ManStop( pAig );
1376 return RetValue;
1377 }
1378
1379
1380 ////////////////////////////////////////////////////////////////////////
1381 /// END OF FILE ///
1382 ////////////////////////////////////////////////////////////////////////
1383
1384
1385 ABC_NAMESPACE_IMPL_END
1386