1 /**CFile****************************************************************
2 
3   FileName    [bmcChain.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [SAT-based bounded model checking.]
8 
9   Synopsis    [Implementation of chain BMC.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 20, 2005.]
16 
17   Revision    [$Id: bmcChain.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "bmc.h"
22 #include "aig/gia/giaAig.h"
23 #include "sat/cnf/cnf.h"
24 #include "sat/bsat/satSolver.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 ///                        DECLARATIONS                              ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 ////////////////////////////////////////////////////////////////////////
34 ///                     FUNCTION DEFINITIONS                         ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 /**Function*************************************************************
38 
39   Synopsis    [Find the first failure.]
40 
41   Description []
42 
43   SideEffects []
44 
45   SeeAlso     []
46 
47 ***********************************************************************/
Bmc_ChainFailOneOutput(Gia_Man_t * p,int nFrameMax,int nConfMax,int fVerbose,int fVeryVerbose)48 Abc_Cex_t * Bmc_ChainFailOneOutput( Gia_Man_t * p, int nFrameMax, int nConfMax, int fVerbose, int fVeryVerbose )
49 {
50     int RetValue;
51     Abc_Cex_t * pCex = NULL;
52     Aig_Man_t * pAig = Gia_ManToAigSimple( p );
53     Saig_ParBmc_t Pars, * pPars = &Pars;
54     Saig_ParBmcSetDefaultParams( pPars );
55     pPars->nFramesMax = nFrameMax;
56     pPars->nConfLimit = nConfMax;
57     pPars->fVerbose   = fVeryVerbose;
58     RetValue = Saig_ManBmcScalable( pAig, pPars );
59     if ( RetValue == 0 ) // SAT
60     {
61         pCex = pAig->pSeqModel, pAig->pSeqModel = NULL;
62         if ( fVeryVerbose )
63             Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n", pCex->iPo, p->pName, pCex->iFrame );
64     }
65     else if ( fVeryVerbose )
66         Abc_Print( 1, "No output asserted in %d frames. Resource limit reached.\n", pPars->iFrame+2 );
67     Aig_ManStop( pAig );
68     return pCex;
69 }
70 
71 /**Function*************************************************************
72 
73   Synopsis    [Move GIA into the failing state.]
74 
75   Description []
76 
77   SideEffects []
78 
79   SeeAlso     []
80 
81 ***********************************************************************/
Gia_ManDupWithInit(Gia_Man_t * p)82 Gia_Man_t * Gia_ManDupWithInit( Gia_Man_t * p )
83 {
84     Gia_Man_t * pNew;
85     Gia_Obj_t * pObj;
86     int i;
87     pNew = Gia_ManStart( Gia_ManObjNum(p) );
88     pNew->pName = Abc_UtilStrsav( p->pName );
89     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
90     Gia_ManConst0(p)->Value = 0;
91     Gia_ManForEachObj1( p, pObj, i )
92     {
93         if ( Gia_ObjIsAnd(pObj) )
94             pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
95         else if ( Gia_ObjIsCi(pObj) )
96         {
97             pObj->Value = Gia_ManAppendCi( pNew );
98             pObj->Value = Abc_LitNotCond( pObj->Value, pObj->fMark0 );
99         }
100         else if ( Gia_ObjIsCo(pObj) )
101         {
102             pObj->Value = Gia_ObjFanin0Copy(pObj);
103             pObj->Value = Abc_LitNotCond( pObj->Value, pObj->fMark0 );
104             pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
105         }
106     }
107     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
108     return pNew;
109 }
Gia_ManVerifyCexAndMove(Gia_Man_t * pGia,Abc_Cex_t * p)110 Gia_Man_t * Gia_ManVerifyCexAndMove( Gia_Man_t * pGia, Abc_Cex_t * p )
111 {
112     Gia_Man_t * pNew;
113     Gia_Obj_t * pObj, * pObjRi, * pObjRo;
114     int RetValue, i, k, iBit = 0;
115     Gia_ManCleanMark0(pGia);
116     Gia_ManForEachRo( pGia, pObj, i )
117         pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
118     for ( i = 0; i <= p->iFrame; i++ )
119     {
120         Gia_ManForEachPi( pGia, pObj, k )
121             pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
122         Gia_ManForEachAnd( pGia, pObj, k )
123             pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
124                            (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
125         Gia_ManForEachCo( pGia, pObj, k )
126             pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
127         if ( i == p->iFrame )
128             break;
129         Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k )
130             pObjRo->fMark0 = pObjRi->fMark0;
131     }
132     assert( iBit == p->nBits );
133     RetValue = Gia_ManPo(pGia, p->iPo)->fMark0;
134     assert( RetValue );
135     // set PI/PO values to zero and transfer RO values to RI
136     Gia_ManForEachPi( pGia, pObj, k )
137         pObj->fMark0 = 0;
138     Gia_ManForEachPo( pGia, pObj, k )
139         pObj->fMark0 = 0;
140     Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k )
141         pObjRi->fMark0 = pObjRo->fMark0;
142     // duplicate assuming CI/CO marks are set correctly
143     pNew = Gia_ManDupWithInit( pGia );
144     Gia_ManCleanMark0(pGia);
145     return pNew;
146 }
147 
148 /**Function*************************************************************
149 
150   Synopsis    [Find what outputs fail in this state.]
151 
152   Description []
153 
154   SideEffects []
155 
156   SeeAlso     []
157 
158 ***********************************************************************/
Gia_ManDupPosAndPropagateInit(Gia_Man_t * p)159 Gia_Man_t * Gia_ManDupPosAndPropagateInit( Gia_Man_t * p )
160 {
161     Gia_Man_t * pNew, * pTemp;
162     Gia_Obj_t * pObj;  int i;
163     pNew = Gia_ManStart( Gia_ManObjNum(p) );
164     pNew->pName = Abc_UtilStrsav( p->pName );
165     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
166     Gia_ManConst0(p)->Value = 0;
167     Gia_ManHashAlloc( pNew );
168     Gia_ManForEachObj1( p, pObj, i )
169     {
170         if ( Gia_ObjIsAnd(pObj) )
171             pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
172         else if ( Gia_ObjIsPi(p, pObj) )
173             pObj->Value = Gia_ManAppendCi( pNew );
174         else if ( Gia_ObjIsCi(pObj) )
175             pObj->Value = 0;
176         else if ( Gia_ObjIsPo(p, pObj) )
177             Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
178     }
179     Gia_ManHashStop( pNew );
180     assert( Gia_ManPiNum(p) == Gia_ManPiNum(pNew) );
181     assert( Gia_ManPoNum(p) == Gia_ManPoNum(pNew) );
182     pNew = Gia_ManCleanup( pTemp = pNew );
183     Gia_ManStop( pTemp );
184     return pNew;
185 }
Gia_ManDeriveSatSolver(Gia_Man_t * p,Vec_Int_t * vSatIds)186 sat_solver * Gia_ManDeriveSatSolver( Gia_Man_t * p, Vec_Int_t * vSatIds )
187 {
188     sat_solver * pSat;
189     Aig_Man_t * pAig = Gia_ManToAigSimple( p );
190 //    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
191     Cnf_Dat_t * pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
192     // save SAT vars for the primary inputs
193     if ( vSatIds )
194     {
195         Aig_Obj_t * pObj; int i;
196         Vec_IntClear( vSatIds );
197         Aig_ManForEachCi( pAig, pObj, i )
198             Vec_IntPush( vSatIds, pCnf->pVarNums[ Aig_ObjId(pObj) ] );
199         assert( Vec_IntSize(vSatIds) == Gia_ManPiNum(p) );
200     }
201     Aig_ManStop( pAig );
202     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
203     Cnf_DataFree( pCnf );
204     assert( p->nRegs == 0 );
205     return pSat;
206 }
Bmc_ChainFindFailedOutputs(Gia_Man_t * p,Vec_Ptr_t * vCexes)207 Vec_Int_t * Bmc_ChainFindFailedOutputs( Gia_Man_t * p, Vec_Ptr_t * vCexes )
208 {
209     Vec_Int_t * vOutputs;
210     Vec_Int_t * vSatIds;
211     Gia_Man_t * pInit;
212     Gia_Obj_t * pObj;
213     sat_solver * pSat;
214     int i, j, Lit, status = 0;
215     // derive output logic cones
216     pInit = Gia_ManDupPosAndPropagateInit( p );
217     // derive SAT solver and test
218     vSatIds = Vec_IntAlloc( Gia_ManPiNum(p) );
219     pSat = Gia_ManDeriveSatSolver( pInit, vSatIds );
220     vOutputs = Vec_IntAlloc( 100 );
221     Gia_ManForEachPo( pInit, pObj, i )
222     {
223         if ( Gia_ObjFaninLit0p(pInit, pObj) == 0 )
224             continue;
225         Lit = Abc_Var2Lit( i+1, 0 );
226         status = sat_solver_solve( pSat, &Lit, &Lit + 1, 0, 0, 0, 0 );
227         if ( status == l_True )
228         {
229             // save the index of solved output
230             Vec_IntPush( vOutputs, i );
231             // create CEX for this output
232             if ( vCexes )
233             {
234                 Abc_Cex_t * pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), 1 );
235                 pCex->iFrame = 0;
236                 pCex->iPo = i;
237                 for ( j = 0; j < Gia_ManPiNum(p); j++ )
238                     if ( sat_solver_var_value( pSat, Vec_IntEntry(vSatIds, j) ) )
239                         Abc_InfoSetBit( pCex->pData, Gia_ManRegNum(p) + j );
240                 Vec_PtrPush( vCexes, pCex );
241             }
242         }
243     }
244     Gia_ManStop( pInit );
245     sat_solver_delete( pSat );
246     Vec_IntFree( vSatIds );
247     return vOutputs;
248 }
249 
250 /**Function*************************************************************
251 
252   Synopsis    [Cleanup AIG by removing COs replacing failed out by const0.]
253 
254   Description []
255 
256   SideEffects []
257 
258   SeeAlso     []
259 
260 ***********************************************************************/
Gia_ObjMakePoConst0(Gia_Man_t * p,Gia_Obj_t * pObj)261 static inline void Gia_ObjMakePoConst0( Gia_Man_t * p, Gia_Obj_t * pObj )
262 {
263     assert( Gia_ObjIsCo(pObj) );
264     pObj->iDiff0 = Gia_ObjId( p, pObj );
265     pObj->fCompl0 = 0;
266 }
Gia_ManCountNonConst0(Gia_Man_t * p)267 int Gia_ManCountNonConst0( Gia_Man_t * p )
268 {
269     Gia_Obj_t * pObj;
270     int i, Count = 0;
271     Gia_ManForEachPo( p, pObj, i )
272         Count += (Gia_ObjFaninLit0p(p, pObj) != 0);
273     return Count;
274 }
Bmc_ChainCleanup(Gia_Man_t * p,Vec_Int_t * vOutputs)275 Gia_Man_t * Bmc_ChainCleanup( Gia_Man_t * p, Vec_Int_t * vOutputs )
276 {
277     int i, iOut;
278     Vec_IntForEachEntry( vOutputs, iOut, i )
279     {
280         Gia_Obj_t * pObj = Gia_ManPo( p, iOut );
281         assert( Gia_ObjFaninLit0p(p, pObj) != 0 );
282         Gia_ObjMakePoConst0( p, pObj );
283         assert( Gia_ObjFaninLit0p(p, pObj) == 0 );
284     }
285     return Gia_ManCleanup( p );
286 }
287 
288 /**Function*************************************************************
289 
290   Synopsis    []
291 
292   Description []
293 
294   SideEffects []
295 
296   SeeAlso     []
297 
298 ***********************************************************************/
Bmc_ChainTest(Gia_Man_t * p,int nFrameMax,int nConfMax,int fVerbose,int fVeryVerbose,Vec_Ptr_t ** pvCexes)299 int Bmc_ChainTest( Gia_Man_t * p, int nFrameMax, int nConfMax, int fVerbose, int fVeryVerbose, Vec_Ptr_t ** pvCexes )
300 {
301     int Iter, IterMax = 10000;
302     Gia_Man_t * pTemp, * pNew = Gia_ManDup(p);
303     Abc_Cex_t * pCex = NULL;
304     Vec_Int_t * vOutputs;
305     abctime clk2, clk = Abc_Clock();
306     abctime clkBmc = 0;
307     abctime clkMov = 0;
308     abctime clkSat = 0;
309     abctime clkCln = 0;
310     abctime clkSwp = 0;
311     int DepthTotal = 0;
312     if ( pvCexes )
313         *pvCexes = Vec_PtrAlloc( 1000 );
314     for ( Iter = 0; Iter < IterMax; Iter++ )
315     {
316         if ( Gia_ManPoNum(pNew) == 0 )
317         {
318             if ( fVerbose )
319                 printf( "Finished all POs.\n" );
320             break;
321         }
322         // run BMC till the first failure
323         clk2 = Abc_Clock();
324         pCex = Bmc_ChainFailOneOutput( pNew, nFrameMax, nConfMax, fVerbose, fVeryVerbose );
325         clkBmc += Abc_Clock() - clk2;
326         if ( pCex == NULL )
327         {
328             if ( fVerbose )
329                 printf( "BMC could not detect a failed output in %d frames with %d conflicts.\n", nFrameMax, nConfMax );
330             break;
331         }
332         assert( !Iter || pCex->iFrame > 0 );
333         // move the AIG to the failure state
334         clk2 = Abc_Clock();
335         pNew = Gia_ManVerifyCexAndMove( pTemp = pNew, pCex );
336         Gia_ManStop( pTemp );
337         DepthTotal += pCex->iFrame;
338         clkMov += Abc_Clock() - clk2;
339         // find outputs that fail in this state
340         clk2 = Abc_Clock();
341         vOutputs = Bmc_ChainFindFailedOutputs( pNew, pvCexes ? *pvCexes : NULL );
342         assert( Vec_IntFind(vOutputs, pCex->iPo) >= 0 );
343         // save the counter-example
344         if ( pvCexes )
345             Vec_PtrPush( *pvCexes, pCex );
346         else
347             Abc_CexFree( pCex );
348         clkSat += Abc_Clock() - clk2;
349         // remove them from the AIG
350         clk2 = Abc_Clock();
351         pNew = Bmc_ChainCleanup( pTemp = pNew, vOutputs );
352         Gia_ManStop( pTemp );
353         clkCln += Abc_Clock() - clk2;
354         // perform sequential cleanup
355         clk2 = Abc_Clock();
356 //        pNew = Gia_ManSeqStructSweep( pTemp = pNew, 0, 1, 0 );
357 //        Gia_ManStop( pTemp );
358         clkSwp += Abc_Clock() - clk2;
359         // printout
360         if ( fVerbose )
361         {
362             int nNonConst = Gia_ManCountNonConst0(pNew);
363             printf( "Iter %4d : ",    Iter+1 );
364             printf( "Depth =%5d  ",   DepthTotal );
365             printf( "FailPo =%5d  ",  Vec_IntSize(vOutputs) );
366             printf( "UndecPo =%5d ",  nNonConst );
367             printf( "(%6.2f %%)  ",   100.0 * nNonConst / Gia_ManPoNum(pNew) );
368             printf( "AIG =%8d  ",     Gia_ManAndNum(pNew) );
369             Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
370         }
371         Vec_IntFree( vOutputs );
372     }
373     printf( "Completed a CEX chain with %d segments, %d frames, and %d failed POs (out of %d). ",
374         Iter, DepthTotal, Gia_ManPoNum(pNew) - Gia_ManCountNonConst0(pNew), Gia_ManPoNum(pNew) );
375     if ( fVerbose )
376     {
377     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
378     Abc_PrintTimeP( 1, "BMC  ", clkBmc, Abc_Clock() - clk );
379     Abc_PrintTimeP( 1, "Init ", clkMov, Abc_Clock() - clk );
380     Abc_PrintTimeP( 1, "SAT  ", clkSat, Abc_Clock() - clk );
381     Abc_PrintTimeP( 1, "Clean", clkCln, Abc_Clock() - clk );
382 //    Abc_PrintTimeP( 1, "Sweep", clkSwp, Abc_Clock() - clk );
383     }
384     Gia_ManStop( pNew );
385     if ( pvCexes )
386         printf( "Total number of CEXes collected = %d.\n", Vec_PtrSize(*pvCexes) );
387     return 0;
388 }
389 
390 ////////////////////////////////////////////////////////////////////////
391 ///                       END OF FILE                                ///
392 ////////////////////////////////////////////////////////////////////////
393 
394 
395 ABC_NAMESPACE_IMPL_END
396 
397