1 /**CFile****************************************************************
2
3 FileName [utilCex.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Handling counter-examples.]
8
9 Synopsis [Handling counter-examples.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - Feburary 13, 2011.]
16
17 Revision [$Id: utilCex.c,v 1.00 2011/02/11 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include <stdio.h>
22 #include <string.h>
23 #include <stdlib.h>
24 #include <assert.h>
25
26 #include "misc/vec/vec.h"
27 #include "utilCex.h"
28
29 ABC_NAMESPACE_IMPL_START
30
31 ////////////////////////////////////////////////////////////////////////
32 /// DECLARATIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 ////////////////////////////////////////////////////////////////////////
36 /// FUNCTION DEFINITIONS ///
37 ////////////////////////////////////////////////////////////////////////
38
39
40 /**Function*************************************************************
41
42 Synopsis [Allocates a counter-example.]
43
44 Description []
45
46 SideEffects []
47
48 SeeAlso []
49
50 ***********************************************************************/
Abc_CexAlloc(int nRegs,int nRealPis,int nFrames)51 Abc_Cex_t * Abc_CexAlloc( int nRegs, int nRealPis, int nFrames )
52 {
53 Abc_Cex_t * pCex;
54 int nWords = Abc_BitWordNum( nRegs + nRealPis * nFrames );
55 pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
56 memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
57 pCex->nRegs = nRegs;
58 pCex->nPis = nRealPis;
59 pCex->nBits = nRegs + nRealPis * nFrames;
60 return pCex;
61 }
Abc_CexAllocFull(int nRegs,int nRealPis,int nFrames)62 Abc_Cex_t * Abc_CexAllocFull( int nRegs, int nRealPis, int nFrames )
63 {
64 Abc_Cex_t * pCex;
65 int nWords = Abc_BitWordNum( nRegs + nRealPis * nFrames );
66 pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
67 memset( pCex, 0xFF, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
68 pCex->nRegs = nRegs;
69 pCex->nPis = nRealPis;
70 pCex->nBits = nRegs + nRealPis * nFrames;
71 return pCex;
72 }
73
74 /**Function*************************************************************
75
76 Synopsis [Make the trivial counter-example for the trivially asserted output.]
77
78 Description []
79
80 SideEffects []
81
82 SeeAlso []
83
84 ***********************************************************************/
Abc_CexMakeTriv(int nRegs,int nTruePis,int nTruePos,int iFrameOut)85 Abc_Cex_t * Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int iFrameOut )
86 {
87 Abc_Cex_t * pCex;
88 int iPo, iFrame;
89 assert( nRegs > 0 );
90 iPo = iFrameOut % nTruePos;
91 iFrame = iFrameOut / nTruePos;
92 // allocate the counter example
93 pCex = Abc_CexAlloc( nRegs, nTruePis, iFrame + 1 );
94 pCex->iPo = iPo;
95 pCex->iFrame = iFrame;
96 return pCex;
97 }
98
99 /**Function*************************************************************
100
101 Synopsis [Derives the counter-example.]
102
103 Description []
104
105 SideEffects []
106
107 SeeAlso []
108
109 ***********************************************************************/
Abc_CexCreate(int nRegs,int nPis,int * pArray,int iFrame,int iPo,int fSkipRegs)110 Abc_Cex_t * Abc_CexCreate( int nRegs, int nPis, int * pArray, int iFrame, int iPo, int fSkipRegs )
111 {
112 Abc_Cex_t * pCex;
113 int i;
114 pCex = Abc_CexAlloc( nRegs, nPis, iFrame+1 );
115 pCex->iPo = iPo;
116 pCex->iFrame = iFrame;
117 if ( pArray == NULL )
118 return pCex;
119 if ( fSkipRegs )
120 {
121 for ( i = nRegs; i < pCex->nBits; i++ )
122 if ( pArray[i-nRegs] )
123 Abc_InfoSetBit( pCex->pData, i );
124 }
125 else
126 {
127 for ( i = 0; i < pCex->nBits; i++ )
128 if ( pArray[i] )
129 Abc_InfoSetBit( pCex->pData, i );
130 }
131 return pCex;
132 }
133
134 /**Function*************************************************************
135
136 Synopsis [Make the trivial counter-example for the trivially asserted output.]
137
138 Description []
139
140 SideEffects []
141
142 SeeAlso []
143
144 ***********************************************************************/
Abc_CexDup(Abc_Cex_t * p,int nRegsNew)145 Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew )
146 {
147 Abc_Cex_t * pCex;
148 int i;
149 if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
150 return p;
151 if ( nRegsNew == -1 )
152 nRegsNew = p->nRegs;
153 pCex = Abc_CexAlloc( nRegsNew, p->nPis, p->iFrame+1 );
154 pCex->iPo = p->iPo;
155 pCex->iFrame = p->iFrame;
156 for ( i = p->nRegs; i < p->nBits; i++ )
157 if ( Abc_InfoHasBit(p->pData, i) )
158 Abc_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs );
159 return pCex;
160 }
161
162 /**Function*************************************************************
163
164 Synopsis [Derives CEX from comb model.]
165
166 Description []
167
168 SideEffects []
169
170 SeeAlso []
171
172 ***********************************************************************/
Abc_CexDeriveFromCombModel(int * pModel,int nPis,int nRegs,int iPo)173 Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int iPo )
174 {
175 Abc_Cex_t * pCex;
176 int i;
177 pCex = Abc_CexAlloc( nRegs, nPis, 1 );
178 pCex->iPo = iPo;
179 pCex->iFrame = 0;
180 for ( i = 0; i < nPis; i++ )
181 if ( pModel[i] )
182 pCex->pData[i>>5] |= (1<<(i & 31));
183 return pCex;
184 }
185
186 /**Function*************************************************************
187
188 Synopsis [Derives CEX from comb model.]
189
190 Description []
191
192 SideEffects []
193
194 SeeAlso []
195
196 ***********************************************************************/
Abc_CexMerge(Abc_Cex_t * pCex,Abc_Cex_t * pPart,int iFrBeg,int iFrEnd)197 Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int iFrEnd )
198 {
199 Abc_Cex_t * pNew;
200 int nFramesGain;
201 int i, f, iBit;
202
203 if ( iFrBeg < 0 )
204 { printf( "Starting frame is less than 0.\n" ); return NULL; }
205 if ( iFrEnd < 0 )
206 { printf( "Stopping frame is less than 0.\n" ); return NULL; }
207 if ( iFrBeg > pCex->iFrame )
208 { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
209 if ( iFrEnd > pCex->iFrame )
210 { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
211 if ( iFrBeg > iFrEnd )
212 { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
213 assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
214 assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
215 assert( iFrBeg <= iFrEnd );
216
217 assert( pCex->nPis == pPart->nPis );
218 assert( iFrEnd - iFrBeg + pPart->iPo >= pPart->iFrame );
219
220 nFramesGain = iFrEnd - iFrBeg + pPart->iPo - pPart->iFrame;
221 pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain );
222 pNew->iPo = pCex->iPo;
223 pNew->iFrame = pCex->iFrame - nFramesGain;
224
225 for ( iBit = 0; iBit < pCex->nRegs; iBit++ )
226 if ( Abc_InfoHasBit(pCex->pData, iBit) )
227 Abc_InfoSetBit( pNew->pData, iBit );
228 for ( f = 0; f < iFrBeg; f++ )
229 for ( i = 0; i < pCex->nPis; i++, iBit++ )
230 if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
231 Abc_InfoSetBit( pNew->pData, iBit );
232 for ( f = 0; f < pPart->iFrame; f++ )
233 for ( i = 0; i < pCex->nPis; i++, iBit++ )
234 if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) )
235 Abc_InfoSetBit( pNew->pData, iBit );
236 for ( f = iFrEnd; f <= pCex->iFrame; f++ )
237 for ( i = 0; i < pCex->nPis; i++, iBit++ )
238 if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
239 Abc_InfoSetBit( pNew->pData, iBit );
240 assert( iBit == pNew->nBits );
241
242 return pNew;
243 }
244
245 /**Function*************************************************************
246
247 Synopsis [Prints out the counter-example.]
248
249 Description []
250
251 SideEffects []
252
253 SeeAlso []
254
255 ***********************************************************************/
Abc_CexPrintStats(Abc_Cex_t * p)256 void Abc_CexPrintStats( Abc_Cex_t * p )
257 {
258 int k, Counter = 0;
259 if ( p == NULL )
260 {
261 printf( "The counter example is NULL.\n" );
262 return;
263 }
264 if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
265 {
266 printf( "The counter example is present but not available (pointer has value \"1\").\n" );
267 return;
268 }
269 for ( k = 0; k < p->nBits; k++ )
270 Counter += Abc_InfoHasBit(p->pData, k);
271 printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%)\n",
272 p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits,
273 Counter, 100.0 * Counter / (p->nBits - p->nRegs) );
274 }
Abc_CexPrintStatsInputs(Abc_Cex_t * p,int nRealPis)275 void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nRealPis )
276 {
277 int k, Counter = 0, CounterPi = 0, CounterPpi = 0;
278 if ( p == NULL )
279 {
280 printf( "The counter example is NULL.\n" );
281 return;
282 }
283 if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
284 {
285 printf( "The counter example is present but not available (pointer has value \"1\").\n" );
286 return;
287 }
288 assert( nRealPis <= p->nPis );
289 for ( k = 0; k < p->nBits; k++ )
290 {
291 Counter += Abc_InfoHasBit(p->pData, k);
292 if ( nRealPis == p->nPis )
293 continue;
294 if ( (k - p->nRegs) % p->nPis < nRealPis )
295 CounterPi += Abc_InfoHasBit(p->pData, k);
296 else
297 CounterPpi += Abc_InfoHasBit(p->pData, k);
298 }
299 printf( "CEX: Po =%4d Fr =%4d FF = %d PI = %d Bit =%7d 1 =%8d (%5.2f %%)",
300 p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits,
301 Counter, 100.0 * Counter / ((p->iFrame + 1) * p->nPis ) );
302 if ( nRealPis < p->nPis )
303 {
304 printf( " 1pi =%8d (%5.2f %%) 1ppi =%8d (%5.2f %%)",
305 CounterPi, 100.0 * CounterPi / ((p->iFrame + 1) * nRealPis ),
306 CounterPpi, 100.0 * CounterPpi / ((p->iFrame + 1) * (p->nPis - nRealPis)) );
307 }
308 printf( "\n" );
309 }
310
311 /**Function*************************************************************
312
313 Synopsis [Prints out the counter-example.]
314
315 Description []
316
317 SideEffects []
318
319 SeeAlso []
320
321 ***********************************************************************/
Abc_CexPrint(Abc_Cex_t * p)322 void Abc_CexPrint( Abc_Cex_t * p )
323 {
324 int i, f, k;
325 if ( p == NULL )
326 {
327 printf( "The counter example is NULL.\n" );
328 return;
329 }
330 if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
331 {
332 printf( "The counter example is present but not available (pointer has value \"1\").\n" );
333 return;
334 }
335 Abc_CexPrintStats( p );
336 printf( "State : " );
337 for ( k = 0; k < p->nRegs; k++ )
338 printf( "%d", Abc_InfoHasBit(p->pData, k) );
339 printf( "\n" );
340 for ( f = 0; f <= p->iFrame; f++ )
341 {
342 printf( "Frame %3d : ", f );
343 for ( i = 0; i < p->nPis; i++ )
344 printf( "%d", Abc_InfoHasBit(p->pData, k++) );
345 printf( "\n" );
346 }
347 assert( k == p->nBits );
348 }
349
350 /**Function*************************************************************
351
352 Synopsis [Frees the counter-example.]
353
354 Description []
355
356 SideEffects []
357
358 SeeAlso []
359
360 ***********************************************************************/
Abc_CexFreeP(Abc_Cex_t ** p)361 void Abc_CexFreeP( Abc_Cex_t ** p )
362 {
363 if ( *p == NULL )
364 return;
365 if ( *p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
366 *p = NULL;
367 else
368 ABC_FREE( *p );
369 }
370
371 /**Function*************************************************************
372
373 Synopsis [Frees the counter-example.]
374
375 Description []
376
377 SideEffects []
378
379 SeeAlso []
380
381 ***********************************************************************/
Abc_CexFree(Abc_Cex_t * p)382 void Abc_CexFree( Abc_Cex_t * p )
383 {
384 if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
385 return;
386 ABC_FREE( p );
387 }
388
389
390 /**Function*************************************************************
391
392 Synopsis [Transform CEX after phase abstraction with nFrames frames.]
393
394 Description []
395
396 SideEffects []
397
398 SeeAlso []
399
400 ***********************************************************************/
Abc_CexTransformPhase(Abc_Cex_t * p,int nPisOld,int nPosOld,int nRegsOld)401 Abc_Cex_t * Abc_CexTransformPhase( Abc_Cex_t * p, int nPisOld, int nPosOld, int nRegsOld )
402 {
403 Abc_Cex_t * pCex;
404 int nFrames = p->nPis / nPisOld;
405 int nPosNew = nPosOld * nFrames;
406 assert( p->nPis % nPisOld == 0 );
407 assert( p->iPo < nPosNew );
408 pCex = Abc_CexDup( p, nRegsOld );
409 pCex->nPis = nPisOld;
410 pCex->iPo = -1;
411 pCex->iFrame = (p->iFrame + 1) * nFrames - 1;
412 pCex->nBits = p->nBits;
413 return pCex;
414 }
415
416 /**Function*************************************************************
417
418 Synopsis [Transform CEX after phase temporal decomposition with nFrames frames.]
419
420 Description []
421
422 SideEffects []
423
424 SeeAlso []
425
426 ***********************************************************************/
Abc_CexTransformTempor(Abc_Cex_t * p,int nPisOld,int nPosOld,int nRegsOld)427 Abc_Cex_t * Abc_CexTransformTempor( Abc_Cex_t * p, int nPisOld, int nPosOld, int nRegsOld )
428 {
429 Abc_Cex_t * pCex;
430 int i, k, iBit = nRegsOld, nFrames = p->nPis / nPisOld - 1;
431 assert( p->iFrame > 0 ); // otherwise tempor did not properly check for failures in the prefix
432 assert( p->nPis % nPisOld == 0 );
433 pCex = Abc_CexAlloc( nRegsOld, nPisOld, nFrames + p->iFrame + 1 );
434 pCex->iPo = p->iPo;
435 pCex->iFrame = nFrames + p->iFrame;
436 for ( i = 0; i < nFrames; i++ )
437 for ( k = 0; k < nPisOld; k++, iBit++ )
438 if ( Abc_InfoHasBit(p->pData, p->nRegs + (i+1)*nPisOld + k) )
439 Abc_InfoSetBit( pCex->pData, iBit );
440 for ( i = 0; i <= p->iFrame; i++ )
441 for ( k = 0; k < nPisOld; k++, iBit++ )
442 if ( Abc_InfoHasBit(p->pData, p->nRegs + i*p->nPis + k) )
443 Abc_InfoSetBit( pCex->pData, iBit );
444 assert( iBit == pCex->nBits );
445 return pCex;
446 }
447
448 /**Function*************************************************************
449
450 Synopsis [Transform CEX after "logic; undc; st; zero".]
451
452 Description []
453
454 SideEffects []
455
456 SeeAlso []
457
458 ***********************************************************************/
Abc_CexTransformUndc(Abc_Cex_t * p,char * pInit)459 Abc_Cex_t * Abc_CexTransformUndc( Abc_Cex_t * p, char * pInit )
460 {
461 Abc_Cex_t * pCex;
462 int nFlops = strlen(pInit);
463 int i, f, iBit, iAddPi = 0, nAddPis = 0;
464 // count how many flops got a new PI
465 for ( i = 0; i < nFlops; i++ )
466 nAddPis += (int)(pInit[i] == 'x' || pInit[i] == 'X');
467 // create new CEX
468 pCex = Abc_CexAlloc( nFlops, p->nPis - nAddPis, p->iFrame + 1 );
469 pCex->iPo = p->iPo;
470 pCex->iFrame = p->iFrame;
471 for ( iBit = 0; iBit < nFlops; iBit++ )
472 {
473 if ( pInit[iBit] == '1' || ((pInit[iBit] == 'x' || pInit[iBit] == 'X') && Abc_InfoHasBit(p->pData, p->nRegs + p->nPis - nAddPis + iAddPi)) )
474 Abc_InfoSetBit( pCex->pData, iBit );
475 iAddPi += (int)(pInit[iBit] == 'x' || pInit[iBit] == 'X');
476 }
477 assert( iAddPi == nAddPis );
478 // add timeframes
479 for ( f = 0; f <= p->iFrame; f++ )
480 for ( i = 0; i < pCex->nPis; i++, iBit++ )
481 if ( Abc_InfoHasBit(p->pData, p->nRegs + p->nPis * f + i) )
482 Abc_InfoSetBit( pCex->pData, iBit );
483 assert( iBit == pCex->nBits );
484 return pCex;
485 }
486
487 /**Function*************************************************************
488
489 Synopsis [Derives permuted CEX using permutation of its inputs.]
490
491 Description []
492
493 SideEffects []
494
495 SeeAlso []
496
497 ***********************************************************************/
Abc_CexPermute(Abc_Cex_t * p,Vec_Int_t * vMapOld2New)498 Abc_Cex_t * Abc_CexPermute( Abc_Cex_t * p, Vec_Int_t * vMapOld2New )
499 {
500 Abc_Cex_t * pCex;
501 int i, iNew;
502 assert( Vec_IntSize(vMapOld2New) == p->nPis );
503 pCex = Abc_CexAlloc( p->nRegs, p->nPis, p->iFrame+1 );
504 pCex->iPo = p->iPo;
505 pCex->iFrame = p->iFrame;
506 for ( i = p->nRegs; i < p->nBits; i++ )
507 if ( Abc_InfoHasBit(p->pData, i) )
508 {
509 iNew = p->nRegs + p->nPis * ((i - p->nRegs) / p->nPis) + Vec_IntEntry( vMapOld2New, (i - p->nRegs) % p->nPis );
510 Abc_InfoSetBit( pCex->pData, iNew );
511 }
512 return pCex;
513 }
514
515 /**Function*************************************************************
516
517 Synopsis [Derives permuted CEX using two canonical permutations.]
518
519 Description []
520
521 SideEffects []
522
523 SeeAlso []
524
525 ***********************************************************************/
Abc_CexPermuteTwo(Abc_Cex_t * p,Vec_Int_t * vPermOld,Vec_Int_t * vPermNew)526 Abc_Cex_t * Abc_CexPermuteTwo( Abc_Cex_t * p, Vec_Int_t * vPermOld, Vec_Int_t * vPermNew )
527 {
528 Abc_Cex_t * pCex;
529 Vec_Int_t * vPerm;
530 int i, eOld, eNew;
531 assert( Vec_IntSize(vPermOld) == p->nPis );
532 assert( Vec_IntSize(vPermNew) == p->nPis );
533 vPerm = Vec_IntStartFull( p->nPis );
534 Vec_IntForEachEntryTwo( vPermOld, vPermNew, eOld, eNew, i )
535 Vec_IntWriteEntry( vPerm, eOld, eNew );
536 pCex = Abc_CexPermute( p, vPerm );
537 Vec_IntFree( vPerm );
538 return pCex;
539 }
540
541 /**Function*************************************************************
542
543 Synopsis [Count the number of 1s in the CEX.]
544
545 Description []
546
547 SideEffects []
548
549 SeeAlso []
550
551 ***********************************************************************/
Abc_CexOnes32(unsigned i)552 static inline int Abc_CexOnes32( unsigned i )
553 {
554 i = i - ((i >> 1) & 0x55555555);
555 i = (i & 0x33333333) + ((i >> 2) & 0x33333333);
556 i = ((i + (i >> 4)) & 0x0F0F0F0F);
557 return (i*(0x01010101))>>24;
558 }
Abc_CexCountOnes(Abc_Cex_t * p)559 int Abc_CexCountOnes( Abc_Cex_t * p )
560 {
561 int nWords = Abc_BitWordNum( p->nBits );
562 int i, Count = 0;
563 for ( i = 0; i < nWords; i++ )
564 Count += Abc_CexOnes32( p->pData[i] );
565 return Count;
566 }
567
568 ////////////////////////////////////////////////////////////////////////
569 /// END OF FILE ///
570 ////////////////////////////////////////////////////////////////////////
571
572
573 ABC_NAMESPACE_IMPL_END
574
575