1 /**CFile****************************************************************
2
3 FileName [bmcCexTools.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT-based bounded model checking.]
8
9 Synopsis [CEX analysis and optimization toolbox.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: bmcCexTools.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "bmc.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
Bmc_CexBitMask(int iBit)30 static inline word Bmc_CexBitMask( int iBit ) { assert( iBit < 64 ); return ~(((word)1) << iBit); }
Bmc_CexCopySim(Vec_Wrd_t * vSims,int iObjTo,int iObjFrom)31 static inline void Bmc_CexCopySim( Vec_Wrd_t * vSims, int iObjTo, int iObjFrom ) { Vec_WrdWriteEntry( vSims, iObjTo, iObjFrom ); }
Bmc_CexAndSim(Vec_Wrd_t * vSims,int iObjTo,int i,int j)32 static inline void Bmc_CexAndSim( Vec_Wrd_t * vSims, int iObjTo, int i, int j ) { Vec_WrdWriteEntry( vSims, iObjTo, Vec_WrdEntry(vSims, i) & Vec_WrdEntry(vSims, j) ); }
Bmc_CexOrSim(Vec_Wrd_t * vSims,int iObjTo,int i,int j)33 static inline void Bmc_CexOrSim( Vec_Wrd_t * vSims, int iObjTo, int i, int j ) { Vec_WrdWriteEntry( vSims, iObjTo, Vec_WrdEntry(vSims, i) | Vec_WrdEntry(vSims, j) ); }
Bmc_CexSim(Vec_Wrd_t * vSims,int iObj,int i)34 static inline int Bmc_CexSim( Vec_Wrd_t * vSims, int iObj, int i ) { return (Vec_WrdEntry(vSims, iObj) >> i) & 1; }
35
36 ////////////////////////////////////////////////////////////////////////
37 /// FUNCTION DEFINITIONS ///
38 ////////////////////////////////////////////////////////////////////////
39
40 /**Function*************************************************************
41
42 Synopsis []
43
44 Description []
45
46 SideEffects []
47
48 SeeAlso []
49
50 ***********************************************************************/
Bmc_CexBitCount(Abc_Cex_t * p,int nInputs)51 int Bmc_CexBitCount( Abc_Cex_t * p, int nInputs )
52 {
53 int k, Counter = 0, Counter2 = 0;
54 if ( p == NULL )
55 {
56 printf( "The counter example is NULL.\n" );
57 return -1;
58 }
59 for ( k = 0; k < p->nBits; k++ )
60 {
61 Counter += Abc_InfoHasBit(p->pData, k);
62 if ( (k - p->nRegs) % p->nPis < nInputs )
63 Counter2 += Abc_InfoHasBit(p->pData, k);
64 }
65 return Counter2;
66 }
67 /**Function*************************************************************
68
69 Synopsis []
70
71 Description []
72
73 SideEffects []
74
75 SeeAlso []
76
77 ***********************************************************************/
Bmc_CexDumpStats(Gia_Man_t * p,Abc_Cex_t * pCex,Abc_Cex_t * pCexCare,Abc_Cex_t * pCexEss,Abc_Cex_t * pCexMin,abctime clk)78 void Bmc_CexDumpStats( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare, Abc_Cex_t * pCexEss, Abc_Cex_t * pCexMin, abctime clk )
79 {
80 int nInputs = Gia_ManPiNum(p);
81 int nBitsTotal = (pCex->iFrame + 1) * nInputs;
82 int nBitsCare = Bmc_CexBitCount(pCexCare, nInputs);
83 int nBitsDC = nBitsTotal - nBitsCare;
84 int nBitsEss = Bmc_CexBitCount(pCexEss, nInputs);
85 int nBitsOpt = nBitsCare - nBitsEss;
86 int nBitsMin = Bmc_CexBitCount(pCexMin, nInputs);
87
88 FILE * pTable = fopen( "cex/stats.txt", "a+" );
89 fprintf( pTable, "%s ", p->pName );
90 fprintf( pTable, "%d ", nInputs );
91 fprintf( pTable, "%d ", Gia_ManRegNum(p) );
92 fprintf( pTable, "%d ", pCex->iFrame + 1 );
93 fprintf( pTable, "%d ", nBitsTotal );
94 fprintf( pTable, "%.2f ", 100.0 * nBitsDC / nBitsTotal );
95 fprintf( pTable, "%.2f ", 100.0 * nBitsOpt / nBitsTotal );
96 fprintf( pTable, "%.2f ", 100.0 * nBitsEss / nBitsTotal );
97 fprintf( pTable, "%.2f ", 100.0 * nBitsMin / nBitsTotal );
98 fprintf( pTable, "%.2f ", 1.0*clk/(CLOCKS_PER_SEC) );
99 fprintf( pTable, "\n" );
100 fclose( pTable );
101 }
102
103
104 /**Function*************************************************************
105
106 Synopsis []
107
108 Description []
109
110 SideEffects []
111
112 SeeAlso []
113
114 ***********************************************************************/
Bmc_CexDumpAogStats(Gia_Man_t * p,abctime clk)115 void Bmc_CexDumpAogStats( Gia_Man_t * p, abctime clk )
116 {
117 FILE * pTable = fopen( "cex/aig_stats.txt", "a+" );
118 fprintf( pTable, "%s ", p->pName );
119 fprintf( pTable, "%d ", Gia_ManPiNum(p) );
120 fprintf( pTable, "%d ", Gia_ManAndNum(p) );
121 fprintf( pTable, "%d ", Gia_ManLevelNum(p) );
122 fprintf( pTable, "%.2f ", 1.0*clk/(CLOCKS_PER_SEC) );
123 fprintf( pTable, "\n" );
124 fclose( pTable );
125 }
126
127 /**Function*************************************************************
128
129 Synopsis [Performs initialized unrolling till the last frame.]
130
131 Description []
132
133 SideEffects []
134
135 SeeAlso []
136
137 ***********************************************************************/
Bmc_CexPerformUnrolling(Gia_Man_t * p,Abc_Cex_t * pCex)138 Gia_Man_t * Bmc_CexPerformUnrolling( Gia_Man_t * p, Abc_Cex_t * pCex )
139 {
140 Gia_Man_t * pNew, * pTemp;
141 Gia_Obj_t * pObj, * pObjRo, * pObjRi;
142 int i, k;
143 assert( Gia_ManRegNum(p) > 0 );
144 pNew = Gia_ManStart( (pCex->iFrame + 1) * Gia_ManObjNum(p) );
145 pNew->pName = Abc_UtilStrsav( p->pName );
146 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
147 Gia_ManConst0(p)->Value = 0;
148 Gia_ManForEachRi( p, pObj, k )
149 pObj->Value = 0;
150 Gia_ManHashAlloc( pNew );
151 for ( i = 0; i <= pCex->iFrame; i++ )
152 {
153 Gia_ManForEachPi( p, pObj, k )
154 pObj->Value = Gia_ManAppendCi( pNew );
155 Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
156 pObjRo->Value = pObjRi->Value;
157 Gia_ManForEachAnd( p, pObj, k )
158 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
159 Gia_ManForEachCo( p, pObj, k )
160 pObj->Value = Gia_ObjFanin0Copy(pObj);
161 }
162 Gia_ManHashStop( pNew );
163 pObj = Gia_ManPo(p, pCex->iPo);
164 Gia_ManAppendCo( pNew, pObj->Value );
165 // cleanup
166 pNew = Gia_ManCleanup( pTemp = pNew );
167 Gia_ManStop( pTemp );
168 return pNew;
169 }
Bmc_CexPerformUnrollingTest(Gia_Man_t * p,Abc_Cex_t * pCex)170 void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex )
171 {
172 Gia_Man_t * pNew;
173 abctime clk = Abc_Clock();
174 pNew = Bmc_CexPerformUnrolling( p, pCex );
175 Gia_ManPrintStats( pNew, NULL );
176 Gia_AigerWrite( pNew, "unroll.aig", 0, 0, 0 );
177 //Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
178 Gia_ManStop( pNew );
179 printf( "CE-induced network is written into file \"unroll.aig\".\n" );
180 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
181 }
182
183
184 /**Function*************************************************************
185
186 Synopsis [Computes CE-induced network.]
187
188 Description []
189
190 SideEffects []
191
192 SeeAlso []
193
194 ***********************************************************************/
Bmc_CexBuildNetwork(Gia_Man_t * p,Abc_Cex_t * pCex)195 Gia_Man_t * Bmc_CexBuildNetwork( Gia_Man_t * p, Abc_Cex_t * pCex )
196 {
197 Gia_Man_t * pNew, * pTemp;
198 Gia_Obj_t * pObj, * pObjRo, * pObjRi;
199 int fCompl0, fCompl1;
200 int i, k, iBit = pCex->nRegs;
201 // start the manager
202 pNew = Gia_ManStart( 1000 );
203 pNew->pName = Abc_UtilStrsav( "unate" );
204 // set const0
205 Gia_ManConst0(p)->fMark0 = 0;
206 Gia_ManConst0(p)->fMark1 = 1;
207 Gia_ManConst0(p)->Value = ~0;
208 // set init state
209 Gia_ManForEachRi( p, pObj, k )
210 {
211 pObj->fMark0 = 0;
212 pObj->fMark1 = 1;
213 pObj->Value = ~0;
214 }
215 Gia_ManHashAlloc( pNew );
216 for ( i = 0; i <= pCex->iFrame; i++ )
217 {
218 // primary inputs
219 Gia_ManForEachPi( p, pObj, k )
220 {
221 pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ );
222 pObj->fMark1 = 0;
223 pObj->Value = Gia_ManAppendCi(pNew);
224 }
225 // transfer
226 Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
227 {
228 pObjRo->fMark0 = pObjRi->fMark0;
229 pObjRo->fMark1 = pObjRi->fMark1;
230 pObjRo->Value = pObjRi->Value;
231 }
232 // internal nodes
233 Gia_ManForEachAnd( p, pObj, k )
234 {
235 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
236 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
237 pObj->fMark0 = fCompl0 & fCompl1;
238 if ( pObj->fMark0 )
239 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
240 else if ( !fCompl0 && !fCompl1 )
241 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
242 else if ( !fCompl0 )
243 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
244 else if ( !fCompl1 )
245 pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
246 else assert( 0 );
247 pObj->Value = ~0;
248 if ( pObj->fMark1 )
249 continue;
250 if ( pObj->fMark0 )
251 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
252 else if ( !fCompl0 && !fCompl1 )
253 pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
254 else if ( !fCompl0 )
255 pObj->Value = Gia_ObjFanin0(pObj)->Value;
256 else if ( !fCompl1 )
257 pObj->Value = Gia_ObjFanin1(pObj)->Value;
258 else assert( 0 );
259 assert( pObj->Value > 0 );
260 }
261 // combinational outputs
262 Gia_ManForEachCo( p, pObj, k )
263 {
264 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
265 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
266 pObj->Value = Gia_ObjFanin0(pObj)->Value;
267 }
268 }
269 Gia_ManHashStop( pNew );
270 assert( iBit == pCex->nBits );
271 // create primary output
272 pObj = Gia_ManPo(p, pCex->iPo);
273 assert( pObj->fMark0 == 1 );
274 assert( pObj->fMark1 == 0 );
275 assert( pObj->Value > 0 );
276 Gia_ManAppendCo( pNew, pObj->Value );
277 // cleanup
278 pNew = Gia_ManCleanup( pTemp = pNew );
279 Gia_ManStop( pTemp );
280 return pNew;
281 }
Bmc_CexBuildNetworkTest(Gia_Man_t * p,Abc_Cex_t * pCex)282 void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex )
283 {
284 Gia_Man_t * pNew;
285 abctime clk = Abc_Clock();
286 pNew = Bmc_CexBuildNetwork( p, pCex );
287 Gia_ManPrintStats( pNew, NULL );
288 Gia_AigerWrite( pNew, "unate.aig", 0, 0, 0 );
289 //Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
290 Gia_ManStop( pNew );
291 printf( "CE-induced network is written into file \"unate.aig\".\n" );
292 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
293 }
294
295
296 /**Function*************************************************************
297
298 Synopsis [Prints one counter-example.]
299
300 Description []
301
302 SideEffects []
303
304 SeeAlso []
305
306 ***********************************************************************/
Bmc_CexPrint(Abc_Cex_t * pCex,int nRealPis,int fVerbose)307 void Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose )
308 {
309 int i, k, Count, iBit = pCex->nRegs;
310 Abc_CexPrintStatsInputs( pCex, nRealPis );
311 if ( !fVerbose )
312 return;
313
314 for ( i = 0; i <= pCex->iFrame; i++ )
315 {
316 Count = 0;
317 printf( "%3d : ", i );
318 for ( k = 0; k < nRealPis; k++ )
319 {
320 Count += Abc_InfoHasBit(pCex->pData, iBit);
321 printf( "%d", Abc_InfoHasBit(pCex->pData, iBit++) );
322 }
323 printf( " %3d ", Count );
324 Count = 0;
325 for ( ; k < pCex->nPis; k++ )
326 {
327 Count += Abc_InfoHasBit(pCex->pData, iBit);
328 printf( "%d", Abc_InfoHasBit(pCex->pData, iBit++) );
329 }
330 printf( " %3d\n", Count );
331 }
332 assert( iBit == pCex->nBits );
333 }
334
335 /**Function*************************************************************
336
337 Synopsis [Verifies the care set of the counter-example.]
338
339 Description []
340
341 SideEffects []
342
343 SeeAlso []
344
345 ***********************************************************************/
Bmc_CexVerify(Gia_Man_t * p,Abc_Cex_t * pCex,Abc_Cex_t * pCexCare)346 int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
347 {
348 Gia_Obj_t * pObj;
349 int i, k;
350 // assert( pCex->nRegs > 0 );
351 // assert( pCexCare->nRegs == 0 );
352 Gia_ObjTerSimSet0( Gia_ManConst0(p) );
353 Gia_ManForEachRi( p, pObj, k )
354 Gia_ObjTerSimSet0( pObj );
355 for ( i = 0; i <= pCex->iFrame; i++ )
356 {
357 Gia_ManForEachPi( p, pObj, k )
358 {
359 if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
360 Gia_ObjTerSimSetX( pObj );
361 else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
362 Gia_ObjTerSimSet1( pObj );
363 else
364 Gia_ObjTerSimSet0( pObj );
365 }
366 Gia_ManForEachRo( p, pObj, k )
367 Gia_ObjTerSimRo( p, pObj );
368 Gia_ManForEachAnd( p, pObj, k )
369 Gia_ObjTerSimAnd( pObj );
370 Gia_ManForEachCo( p, pObj, k )
371 Gia_ObjTerSimCo( pObj );
372 }
373 pObj = Gia_ManPo( p, pCex->iPo );
374 return Gia_ObjTerSimGet1(pObj);
375 }
376
377 /**Function*************************************************************
378
379 Synopsis [Computes internal states of the CEX.]
380
381 Description []
382
383 SideEffects []
384
385 SeeAlso []
386
387 ***********************************************************************/
Bmc_CexInnerStates(Gia_Man_t * p,Abc_Cex_t * pCex,Abc_Cex_t ** ppCexImpl,int fVerbose)388 Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose )
389 {
390 Abc_Cex_t * pNew, * pNew2;
391 Gia_Obj_t * pObj, * pObjRo, * pObjRi;
392 int fCompl0, fCompl1;
393 int i, k, iBit = 0;
394 assert( pCex->nRegs > 0 );
395 // start the counter-example
396 pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCex->iFrame + 1 );
397 pNew->iFrame = pCex->iFrame;
398 pNew->iPo = pCex->iPo;
399 // start the counter-example
400 pNew2 = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCex->iFrame + 1 );
401 pNew2->iFrame = pCex->iFrame;
402 pNew2->iPo = pCex->iPo;
403 // set initial state
404 Gia_ManCleanMark01(p);
405 // set const0
406 Gia_ManConst0(p)->fMark0 = 0;
407 Gia_ManConst0(p)->fMark1 = 1;
408 // set init state
409 Gia_ManForEachRi( p, pObjRi, k )
410 {
411 pObjRi->fMark0 = 0;
412 pObjRi->fMark1 = 1;
413 }
414 iBit = pCex->nRegs;
415 for ( i = 0; i <= pCex->iFrame; i++ )
416 {
417 Gia_ManForEachPi( p, pObj, k )
418 pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
419 Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
420 {
421 pObjRo->fMark0 = pObjRi->fMark0;
422 pObjRo->fMark1 = pObjRi->fMark1;
423 }
424 Gia_ManForEachCi( p, pObj, k )
425 {
426 if ( pObj->fMark0 )
427 Abc_InfoSetBit( pNew->pData, pNew->nPis * i + k );
428 if ( pObj->fMark1 )
429 Abc_InfoSetBit( pNew2->pData, pNew2->nPis * i + k );
430 }
431 Gia_ManForEachAnd( p, pObj, k )
432 {
433 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
434 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
435 pObj->fMark0 = fCompl0 & fCompl1;
436 if ( pObj->fMark0 )
437 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
438 else if ( !fCompl0 && !fCompl1 )
439 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
440 else if ( !fCompl0 )
441 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
442 else if ( !fCompl1 )
443 pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
444 else assert( 0 );
445 }
446 Gia_ManForEachCo( p, pObj, k )
447 {
448 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
449 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
450 }
451
452 /*
453 // print input/state/output
454 printf( "%3d : ", i );
455 Gia_ManForEachPi( p, pObj, k )
456 printf( "%d", pObj->fMark0 );
457 printf( " " );
458 Gia_ManForEachRo( p, pObj, k )
459 printf( "%d", pObj->fMark0 );
460 printf( " " );
461 Gia_ManForEachPo( p, pObj, k )
462 printf( "%d", pObj->fMark0 );
463 printf( "\n" );
464 */
465 }
466 assert( iBit == pCex->nBits );
467 assert( Gia_ManPo(p, pCex->iPo)->fMark0 == 1 );
468
469 printf( "Inner states: " );
470 Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
471 printf( "Implications: " );
472 Bmc_CexPrint( pNew2, Gia_ManPiNum(p), fVerbose );
473 if ( ppCexImpl )
474 *ppCexImpl = pNew2;
475 else
476 Abc_CexFree( pNew2 );
477 return pNew;
478 }
479
480 /**Function*************************************************************
481
482 Synopsis [Computes care bits of the CEX.]
483
484 Description []
485
486 SideEffects []
487
488 SeeAlso []
489
490 ***********************************************************************/
Bmc_CexCareBits_rec(Gia_Man_t * p,Gia_Obj_t * pObj)491 void Bmc_CexCareBits_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
492 {
493 int fCompl0, fCompl1;
494 if ( Gia_ObjIsConst0(pObj) )
495 return;
496 if ( pObj->fMark1 )
497 return;
498 pObj->fMark1 = 1;
499 if ( Gia_ObjIsCi(pObj) )
500 return;
501 assert( Gia_ObjIsAnd(pObj) );
502 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
503 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
504 if ( pObj->fMark0 )
505 {
506 assert( fCompl0 == 1 && fCompl1 == 1 );
507 Bmc_CexCareBits_rec( p, Gia_ObjFanin0(pObj) );
508 Bmc_CexCareBits_rec( p, Gia_ObjFanin1(pObj) );
509 }
510 else
511 {
512 assert( fCompl0 == 0 || fCompl1 == 0 );
513 if ( fCompl0 == 0 )
514 Bmc_CexCareBits_rec( p, Gia_ObjFanin0(pObj) );
515 if ( fCompl1 == 0 )
516 Bmc_CexCareBits_rec( p, Gia_ObjFanin1(pObj) );
517 }
518 }
Bmc_CexCareBits2_rec(Gia_Man_t * p,Gia_Obj_t * pObj)519 void Bmc_CexCareBits2_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
520 {
521 int fCompl0, fCompl1;
522 if ( Gia_ObjIsConst0(pObj) )
523 return;
524 if ( pObj->fMark1 )
525 return;
526 pObj->fMark1 = 1;
527 if ( Gia_ObjIsCi(pObj) )
528 return;
529 assert( Gia_ObjIsAnd(pObj) );
530 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
531 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
532 if ( pObj->fMark0 )
533 {
534 assert( fCompl0 == 1 && fCompl1 == 1 );
535 Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(pObj) );
536 Bmc_CexCareBits2_rec( p, Gia_ObjFanin1(pObj) );
537 }
538 else
539 {
540 assert( fCompl0 == 0 || fCompl1 == 0 );
541 if ( fCompl0 == 0 )
542 Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(pObj) );
543 /**/
544 else
545 /**/
546 if ( fCompl1 == 0 )
547 Bmc_CexCareBits2_rec( p, Gia_ObjFanin1(pObj) );
548 }
549 }
Bmc_CexCareBits(Gia_Man_t * p,Abc_Cex_t * pCexState,Abc_Cex_t * pCexImpl,Abc_Cex_t * pCexEss,int fFindAll,int fVerbose)550 Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose )
551 {
552 Abc_Cex_t * pNew;
553 Gia_Obj_t * pObj;
554 int fCompl0, fCompl1;
555 int i, k, iBit;
556 assert( pCexState->nRegs == 0 );
557 // start the counter-example
558 pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCexState->iFrame + 1 );
559 pNew->iFrame = pCexState->iFrame;
560 pNew->iPo = pCexState->iPo;
561 // set initial state
562 Gia_ManCleanMark01(p);
563 // set const0
564 Gia_ManConst0(p)->fMark0 = 0;
565 Gia_ManConst0(p)->fMark1 = 1;
566 for ( i = pCexState->iFrame; i >= 0; i-- )
567 {
568 // set correct values
569 iBit = pCexState->nPis * i;
570 Gia_ManForEachCi( p, pObj, k )
571 {
572 pObj->fMark0 = Abc_InfoHasBit(pCexState->pData, iBit+k);
573 pObj->fMark1 = 0;
574 if ( pCexImpl )
575 pObj->fMark1 |= Abc_InfoHasBit(pCexImpl->pData, iBit+k);
576 if ( pCexEss )
577 pObj->fMark1 |= Abc_InfoHasBit(pCexEss->pData, iBit+k);
578 }
579 Gia_ManForEachAnd( p, pObj, k )
580 {
581 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
582 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
583 pObj->fMark0 = fCompl0 & fCompl1;
584 if ( pObj->fMark0 )
585 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
586 else if ( !fCompl0 && !fCompl1 )
587 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
588 else if ( !fCompl0 )
589 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
590 else if ( !fCompl1 )
591 pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
592 else assert( 0 );
593 }
594 Gia_ManForEachCo( p, pObj, k )
595 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
596 // move values from COs to CIs
597 if ( i == pCexState->iFrame )
598 {
599 assert( Gia_ManPo(p, pCexState->iPo)->fMark0 == 1 );
600 if ( fFindAll )
601 Bmc_CexCareBits_rec( p, Gia_ObjFanin0(Gia_ManPo(p, pCexState->iPo)) );
602 else
603 Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(Gia_ManPo(p, pCexState->iPo)) );
604 }
605 else
606 {
607 Gia_ManForEachRi( p, pObj, k )
608 if ( Abc_InfoHasBit(pNew->pData, pNew->nPis * (i+1) + Gia_ManPiNum(p) + k) )
609 {
610 if ( fFindAll )
611 Bmc_CexCareBits_rec( p, Gia_ObjFanin0(pObj) );
612 else
613 Bmc_CexCareBits2_rec( p, Gia_ObjFanin0(pObj) );
614 }
615 }
616 // save the results
617 Gia_ManForEachCi( p, pObj, k )
618 if ( pObj->fMark1 )
619 {
620 pObj->fMark1 = 0;
621 if ( pCexImpl == NULL || !Abc_InfoHasBit(pCexImpl->pData, pNew->nPis * i + k) )
622 Abc_InfoSetBit(pNew->pData, pNew->nPis * i + k);
623 }
624 }
625 if ( pCexEss )
626 printf( "Minimized: " );
627 else
628 printf( "Care bits: " );
629 Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
630 return pNew;
631 }
632
633 /**Function*************************************************************
634
635 Synopsis [Simulates one bit to check whether it is essential.]
636
637 Description []
638
639 SideEffects []
640
641 SeeAlso []
642
643 ***********************************************************************/
Bmc_CexEssentialBitOne(Gia_Man_t * p,Abc_Cex_t * pCexState,int iBit,Abc_Cex_t * pCexPrev,int * pfEqual)644 Abc_Cex_t * Bmc_CexEssentialBitOne( Gia_Man_t * p, Abc_Cex_t * pCexState, int iBit, Abc_Cex_t * pCexPrev, int * pfEqual )
645 {
646 Abc_Cex_t * pNew;
647 Gia_Obj_t * pObj;
648 int i, k, fCompl0, fCompl1;
649 assert( pCexState->nRegs == 0 );
650 assert( iBit < pCexState->nBits );
651 if ( pfEqual )
652 *pfEqual = 0;
653 // start the counter-example
654 pNew = Abc_CexAllocFull( 0, Gia_ManCiNum(p), pCexState->iFrame + 1 );
655 pNew->iFrame = pCexState->iFrame;
656 pNew->iPo = pCexState->iPo;
657 // clean bit
658 Abc_InfoXorBit( pNew->pData, iBit );
659 // simulate the remaining frames
660 Gia_ManConst0(p)->fMark0 = 0;
661 Gia_ManConst0(p)->fMark1 = 1;
662 for ( i = iBit / pCexState->nPis; i <= pCexState->iFrame; i++ )
663 {
664 Gia_ManForEachCi( p, pObj, k )
665 {
666 pObj->fMark0 = Abc_InfoHasBit( pCexState->pData, i * pCexState->nPis + k );
667 pObj->fMark1 = Abc_InfoHasBit( pNew->pData, i * pCexState->nPis + k );
668 }
669 Gia_ManForEachAnd( p, pObj, k )
670 {
671 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
672 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
673 pObj->fMark0 = fCompl0 & fCompl1;
674 if ( pObj->fMark0 )
675 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
676 else if ( !fCompl0 && !fCompl1 )
677 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
678 else if ( !fCompl0 )
679 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
680 else if ( !fCompl1 )
681 pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
682 else assert( 0 );
683 }
684 Gia_ManForEachCo( p, pObj, k )
685 {
686 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
687 pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
688 }
689 if ( i < pCexState->iFrame )
690 {
691 int fChanges = 0;
692 int fEqual = (pCexPrev != NULL);
693 int iBitShift = (i + 1) * pCexState->nPis + Gia_ManPiNum(p);
694 Gia_ManForEachRi( p, pObj, k )
695 {
696 if ( fEqual && pCexPrev && (int)pObj->fMark1 != Abc_InfoHasBit(pCexPrev->pData, iBitShift + k) )
697 fEqual = 0;
698 if ( !pObj->fMark1 )
699 {
700 fChanges = 1;
701 Abc_InfoXorBit( pNew->pData, iBitShift + k );
702 }
703 }
704 if ( !fChanges || fEqual )
705 {
706 if ( pfEqual )
707 *pfEqual = fEqual;
708 Abc_CexFree( pNew );
709 return NULL;
710 }
711 }
712 /*
713 if ( i == 20 )
714 {
715 printf( "Frame %d : ", i );
716 Gia_ManForEachRi( p, pObj, k )
717 printf( "%d", pObj->fMark1 );
718 printf( "\n" );
719 }
720 */
721 }
722 return pNew;
723 }
Bmc_CexEssentialBitTest(Gia_Man_t * p,Abc_Cex_t * pCexState)724 void Bmc_CexEssentialBitTest( Gia_Man_t * p, Abc_Cex_t * pCexState )
725 {
726 Abc_Cex_t * pNew;
727 int b;
728 for ( b = 0; b < pCexState->nBits; b++ )
729 {
730 if ( b % 100 )
731 continue;
732 pNew = Bmc_CexEssentialBitOne( p, pCexState, b, NULL, NULL );
733 Bmc_CexPrint( pNew, Gia_ManPiNum(p), 0 );
734
735 if ( Gia_ManPo(p, pCexState->iPo)->fMark1 )
736 printf( "Not essential\n" );
737 else
738 printf( "Essential\n" );
739
740 Abc_CexFree( pNew );
741 }
742 }
743
744 /**Function*************************************************************
745
746 Synopsis [Computes essential bits of the CEX.]
747
748 Description []
749
750 SideEffects []
751
752 SeeAlso []
753
754 ***********************************************************************/
Bmc_CexEssentialBits(Gia_Man_t * p,Abc_Cex_t * pCexState,Abc_Cex_t * pCexCare,int fVerbose)755 Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexCare, int fVerbose )
756 {
757 Abc_Cex_t * pNew, * pTemp, * pPrev = NULL;
758 int b, fEqual = 0, fPrevStatus = 0;
759 // abctime clk = Abc_Clock();
760 assert( pCexState->nBits == pCexCare->nBits );
761 // start the counter-example
762 pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCexState->iFrame + 1 );
763 pNew->iFrame = pCexState->iFrame;
764 pNew->iPo = pCexState->iPo;
765 // iterate through care-bits
766 for ( b = 0; b < pCexState->nBits; b++ )
767 {
768 // skip don't-care bits
769 if ( !Abc_InfoHasBit(pCexCare->pData, b) )
770 continue;
771
772 // skip state bits
773 if ( b % pCexCare->nPis >= Gia_ManPiNum(p) )
774 {
775 Abc_InfoSetBit( pNew->pData, b );
776 continue;
777 }
778
779 // check if this is an essential bit
780 pTemp = Bmc_CexEssentialBitOne( p, pCexState, b, pPrev, &fEqual );
781 // pTemp = Bmc_CexEssentialBitOne( p, pCexState, b, NULL, &fEqual );
782 if ( pTemp == NULL )
783 {
784 if ( fEqual && fPrevStatus )
785 Abc_InfoSetBit( pNew->pData, b );
786 continue;
787 }
788 // Bmc_CexPrint( pTemp, Gia_ManPiNum(p), fVerbose );
789 Abc_CexFree( pPrev );
790 pPrev = pTemp;
791
792 // record essential bit
793 fPrevStatus = !Gia_ManPo(p, pCexState->iPo)->fMark1;
794 if ( !Gia_ManPo(p, pCexState->iPo)->fMark1 )
795 Abc_InfoSetBit( pNew->pData, b );
796 }
797 Abc_CexFreeP( &pPrev );
798 // Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
799 printf( "Essentials: " );
800 Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
801 return pNew;
802 }
803
804
805 /**Function*************************************************************
806
807 Synopsis [Computes essential bits of the CEX.]
808
809 Description []
810
811 SideEffects []
812
813 SeeAlso []
814
815 ***********************************************************************/
Bmc_CexTest(Gia_Man_t * p,Abc_Cex_t * pCex,int fVerbose)816 void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
817 {
818 abctime clk = Abc_Clock();
819 Abc_Cex_t * pCexImpl = NULL;
820 Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
821 Abc_Cex_t * pCexCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
822 Abc_Cex_t * pCexEss, * pCexMin;
823
824 if ( !Bmc_CexVerify( p, pCex, pCexCare ) )
825 printf( "Counter-example care-set verification has failed.\n" );
826
827 pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose );
828 pCexMin = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose );
829
830 if ( !Bmc_CexVerify( p, pCex, pCexMin ) )
831 printf( "Counter-example min-set verification has failed.\n" );
832
833 // Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, Abc_Clock() - clk );
834
835 Abc_CexFreeP( &pCexStates );
836 Abc_CexFreeP( &pCexImpl );
837 Abc_CexFreeP( &pCexCare );
838 Abc_CexFreeP( &pCexEss );
839 Abc_CexFreeP( &pCexMin );
840
841 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
842 // Bmc_CexBuildNetworkTest( p, pCex );
843 // Bmc_CexPerformUnrollingTest( p, pCex );
844 }
845
846
847
848 /**Function*************************************************************
849
850 Synopsis [Count the number of care bits.]
851
852 Description []
853
854 SideEffects []
855
856 SeeAlso []
857
858 ***********************************************************************/
Gia_ManCountCareBits(Gia_Man_t * p,Vec_Wec_t * vPats)859 void Gia_ManCountCareBits( Gia_Man_t * p, Vec_Wec_t * vPats )
860 {
861 Gia_Obj_t * pObj;
862 int i, k, fCompl0, fCompl1;
863 word Counter = 0;
864 Vec_Int_t * vPat;
865 Vec_WecForEachLevel( vPats, vPat, i )
866 {
867 int Count = 0;
868 assert( Vec_IntSize(vPat) == Gia_ManCiNum(p) );
869
870 // propagate forward
871 Gia_ManConst0(p)->fMark0 = 0;
872 Gia_ManConst0(p)->fMark1 = 0;
873 Gia_ManForEachCi( p, pObj, k )
874 {
875 pObj->fMark0 = Vec_IntEntry(vPat, k);
876 pObj->fMark1 = 0;
877 }
878 Gia_ManForEachAnd( p, pObj, k )
879 {
880 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
881 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
882 pObj->fMark0 = fCompl0 & fCompl1;
883 pObj->fMark1 = 0;
884 }
885 Gia_ManForEachCo( p, pObj, k )
886 {
887 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
888 Gia_ObjFanin0(pObj)->fMark1 = 1;
889 }
890 // propagate backward
891 Gia_ManForEachAndReverse( p, pObj, k )
892 {
893 if ( !pObj->fMark1 )
894 continue;
895 if ( pObj->fMark0 == 0 )
896 {
897 fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
898 fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
899 assert( fCompl0 == 0 || fCompl1 == 0 );
900 if ( fCompl1 == 0 )
901 Gia_ObjFanin1(pObj)->fMark1 = 1;
902 else if ( fCompl0 == 0 )
903 Gia_ObjFanin0(pObj)->fMark1 = 1;
904
905 }
906 else
907 {
908 Gia_ObjFanin0(pObj)->fMark1 = 1;
909 Gia_ObjFanin1(pObj)->fMark1 = 1;
910 }
911 }
912 Gia_ManForEachAnd( p, pObj, k )
913 Count += pObj->fMark1;
914 Counter += Count;
915
916 //printf( "%3d = %8d\n", i, Count );
917 }
918 Counter /= Vec_WecSize(vPats);
919 printf( "Stats over %d patterns: Average care-nodes = %d (%6.2f %%)\n", Vec_WecSize(vPats), (int)Counter, 100.0*(int)Counter/Gia_ManAndNum(p) );
920 }
921
Mnist_ReadImages1_()922 unsigned char * Mnist_ReadImages1_()
923 {
924 int Size = 60000 * 28 * 28 + 16;
925 unsigned char * pData = malloc( Size );
926 FILE * pFile = fopen( "train-images.idx3-ubyte", "rb" );
927 int RetValue = fread( pData, 1, Size, pFile );
928 assert( RetValue == Size );
929 fclose( pFile );
930 return pData;
931 }
Mnist_ReadImages_(int nPats)932 Vec_Wec_t * Mnist_ReadImages_( int nPats )
933 {
934 Vec_Wec_t * vPats = Vec_WecStart( nPats );
935 unsigned char * pL1 = Mnist_ReadImages1_();
936 int i, k, x;
937 for ( i = 0; i < nPats; i++ )
938 for ( x = 0; x < 784; x++ )
939 for ( k = 0; k < 8; k++ )
940 Vec_WecPush( vPats, i, (pL1[16 + i * 784 + x] >> k) & 1 );
941 free( pL1 );
942 return vPats;
943 }
Gia_ManCountCareBitsTest(Gia_Man_t * p)944 void Gia_ManCountCareBitsTest( Gia_Man_t * p )
945 {
946 Vec_Wec_t * vPats = Mnist_ReadImages_( 100 );
947 Gia_ManCountCareBits( p, vPats );
948 Vec_WecFree( vPats );
949 }
950
951
952 ////////////////////////////////////////////////////////////////////////
953 /// END OF FILE ///
954 ////////////////////////////////////////////////////////////////////////
955
956
957 ABC_NAMESPACE_IMPL_END
958
959