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