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