1 /**CFile****************************************************************
2
3 FileName [bmcBmci.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT-based bounded model checking.]
8
9 Synopsis []
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: bmcBmci.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "bmc.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satStore.h"
24 #include "aig/gia/giaAig.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 []
40
41 Description []
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
Cnf_DeriveGiaRemapped(Gia_Man_t * p)48 static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
49 {
50 Cnf_Dat_t * pCnf;
51 Aig_Man_t * pAig = Gia_ManToAigSimple( p );
52 pAig->nRegs = 0;
53 pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
54 Aig_ManStop( pAig );
55 return pCnf;
56 }
57
58 /**Function*************************************************************
59
60 Synopsis []
61
62 Description []
63
64 SideEffects []
65
66 SeeAlso []
67
68 ***********************************************************************/
Cnf_DataLiftGia(Cnf_Dat_t * p,Gia_Man_t * pGia,int nVarsPlus)69 static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPlus )
70 {
71 Gia_Obj_t * pObj;
72 int v;
73 Gia_ManForEachObj( pGia, pObj, v )
74 if ( p->pVarNums[Gia_ObjId(pGia, pObj)] >= 0 )
75 p->pVarNums[Gia_ObjId(pGia, pObj)] += nVarsPlus;
76 for ( v = 0; v < p->nLiterals; v++ )
77 p->pClauses[0][v] += 2*nVarsPlus;
78 }
79
80 /**Function*************************************************************
81
82 Synopsis []
83
84 Description []
85
86 SideEffects []
87
88 SeeAlso []
89
90 ***********************************************************************/
Bmc_BmciUnfold(Gia_Man_t * pNew,Gia_Man_t * p,Vec_Int_t * vFFLits,int fPiReuse)91 void Bmc_BmciUnfold( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vFFLits, int fPiReuse )
92 {
93 Gia_Obj_t * pObj;
94 int i;
95 assert( Gia_ManRegNum(p) == Vec_IntSize(vFFLits) );
96 Gia_ManConst0(p)->Value = 0;
97 Gia_ManForEachRo( p, pObj, i )
98 pObj->Value = Vec_IntEntry(vFFLits, i);
99 Gia_ManForEachPi( p, pObj, i )
100 pObj->Value = fPiReuse ? Gia_ObjToLit(pNew, Gia_ManPi(pNew, Gia_ManPiNum(pNew)-Gia_ManPiNum(p)+i)) : Gia_ManAppendCi(pNew);
101 Gia_ManForEachAnd( p, pObj, i )
102 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
103 Gia_ManForEachRi( p, pObj, i )
104 Vec_IntWriteEntry( vFFLits, i, Gia_ObjFanin0Copy(pObj) );
105 }
106
107 /**Function*************************************************************
108
109 Synopsis []
110
111 Description []
112
113 SideEffects []
114
115 SeeAlso []
116
117 ***********************************************************************/
Bmc_BmciPart_rec(Gia_Man_t * pNew,Vec_Int_t * vSatMap,int iIdNew,Gia_Man_t * pPart,Vec_Int_t * vPartMap,Vec_Int_t * vCopies)118 int Bmc_BmciPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Man_t * pPart, Vec_Int_t * vPartMap, Vec_Int_t * vCopies )
119 {
120 Gia_Obj_t * pObj = Gia_ManObj( pNew, iIdNew );
121 int iLitPart0, iLitPart1, iRes;
122 if ( Vec_IntEntry(vCopies, iIdNew) )
123 return Vec_IntEntry(vCopies, iIdNew);
124 if ( Vec_IntEntry(vSatMap, iIdNew) >= 0 || Gia_ObjIsCi(pObj) )
125 {
126 Vec_IntPush( vPartMap, iIdNew );
127 iRes = Gia_ManAppendCi(pPart);
128 Vec_IntWriteEntry( vCopies, iIdNew, iRes );
129 return iRes;
130 }
131 assert( Gia_ObjIsAnd(pObj) );
132 iLitPart0 = Bmc_BmciPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap, vCopies );
133 iLitPart1 = Bmc_BmciPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap, vCopies );
134 iLitPart0 = Abc_LitNotCond( iLitPart0, Gia_ObjFaninC0(pObj) );
135 iLitPart1 = Abc_LitNotCond( iLitPart1, Gia_ObjFaninC1(pObj) );
136 Vec_IntPush( vPartMap, iIdNew );
137 iRes = Gia_ManAppendAnd( pPart, iLitPart0, iLitPart1 );
138 Vec_IntWriteEntry( vCopies, iIdNew, iRes );
139 return iRes;
140 }
Bmc_BmciPart(Gia_Man_t * pNew,Vec_Int_t * vSatMap,Vec_Int_t * vMiters,Vec_Int_t * vPartMap,Vec_Int_t * vCopies)141 Gia_Man_t * Bmc_BmciPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vMiters, Vec_Int_t * vPartMap, Vec_Int_t * vCopies )
142 {
143 Gia_Man_t * pPart;
144 int i, iLit, iLitPart;
145 Vec_IntFill( vCopies, Gia_ManObjNum(pNew), 0 );
146 Vec_IntFillExtra( vSatMap, Gia_ManObjNum(pNew), -1 );
147 pPart = Gia_ManStart( 1000 );
148 pPart->pName = Abc_UtilStrsav( pNew->pName );
149 Vec_IntClear( vPartMap );
150 Vec_IntPush( vPartMap, 0 );
151 Vec_IntForEachEntry( vMiters, iLit, i )
152 {
153 if ( iLit == -1 )
154 continue;
155 assert( iLit >= 2 );
156 iLitPart = Bmc_BmciPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap, vCopies );
157 Gia_ManAppendCo( pPart, Abc_LitNotCond(iLitPart, Abc_LitIsCompl(iLit)) );
158 Vec_IntPush( vPartMap, -1 );
159 }
160 assert( Gia_ManPoNum(pPart) > 0 );
161 assert( Vec_IntSize(vPartMap) == Gia_ManObjNum(pPart) );
162 return pPart;
163 }
164
165 /**Function*************************************************************
166
167 Synopsis []
168
169 Description []
170
171 SideEffects []
172
173 SeeAlso []
174
175 ***********************************************************************/
Bmc_BmciPerform(Gia_Man_t * p,Vec_Int_t * vInit0,Vec_Int_t * vInit1,int nFrames,int nWords,int nTimeOut,int fVerbose)176 int Bmc_BmciPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int nFrames, int nWords, int nTimeOut, int fVerbose )
177 {
178 int nSatVars = 1;
179 Vec_Int_t * vLits0, * vLits1, * vMiters, * vSatMap, * vPartMap, * vCopies;
180 Gia_Man_t * pNew, * pPart;
181 Gia_Obj_t * pObj;
182 Cnf_Dat_t * pCnf;
183 sat_solver * pSat;
184 int iVar0, iVar1, iLit, iLit0, iLit1;
185 int i, f, status, nChanges, nMiters, RetValue = 1;
186 assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) );
187 assert( Vec_IntSize(vInit1) == Gia_ManRegNum(p) );
188
189 // start the SAT solver
190 pSat = sat_solver_new();
191 sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
192
193 pNew = Gia_ManStart( 10000 );
194 pNew->pName = Abc_UtilStrsav( p->pName );
195 Gia_ManHashAlloc( pNew );
196 Gia_ManConst0(p)->Value = 0;
197
198 vLits0 = Vec_IntAlloc( Gia_ManRegNum(p) );
199 Vec_IntForEachEntry( vInit0, iLit, i )
200 Vec_IntPush( vLits0, iLit < 2 ? iLit : Gia_ManAppendCi(pNew) );
201
202 vLits1 = Vec_IntAlloc( Gia_ManRegNum(p) );
203 Vec_IntForEachEntry( vInit1, iLit, i )
204 Vec_IntPush( vLits1, iLit < 2 ? iLit : Gia_ManAppendCi(pNew) );
205
206 vMiters = Vec_IntAlloc( 1000 );
207 vSatMap = Vec_IntAlloc( 1000 );
208 vPartMap = Vec_IntAlloc( 1000 );
209 vCopies = Vec_IntAlloc( 1000 );
210 for ( f = 0; f < nFrames; f++ )
211 {
212 abctime clk = Abc_Clock();
213 Bmc_BmciUnfold( pNew, p, vLits0, 0 );
214 Bmc_BmciUnfold( pNew, p, vLits1, 1 );
215 assert( Vec_IntSize(vLits0) == Vec_IntSize(vLits1) );
216 nMiters = 0;
217 Vec_IntClear( vMiters );
218 Vec_IntForEachEntryTwo( vLits0, vLits1, iLit0, iLit1, i )
219 if ( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 )
220 Vec_IntPush( vMiters, Gia_ManHashXor(pNew, iLit0, iLit1) ), nMiters++;
221 else
222 Vec_IntPush( vMiters, -1 );
223 assert( Vec_IntSize(vMiters) == Gia_ManRegNum(p) );
224 if ( Vec_IntSum(vMiters) + Vec_IntSize(vLits1) == 0 )
225 {
226 if ( fVerbose )
227 printf( "Reached a fixed point after %d frames. \n", f+1 );
228 break;
229 }
230 // create new part
231 pPart = Bmc_BmciPart( pNew, vSatMap, vMiters, vPartMap, vCopies );
232 pCnf = Cnf_DeriveGiaRemapped( pPart );
233 Cnf_DataLiftGia( pCnf, pPart, nSatVars );
234 nSatVars += pCnf->nVars;
235 sat_solver_setnvars( pSat, nSatVars );
236 for ( i = 0; i < pCnf->nClauses; i++ )
237 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
238 assert( 0 );
239 // stitch the clauses
240 Gia_ManForEachPi( pPart, pObj, i )
241 {
242 iVar0 = pCnf->pVarNums[Gia_ObjId(pPart, pObj)];
243 iVar1 = Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, Gia_ObjId(pPart, pObj)) );
244 if ( iVar1 == -1 )
245 continue;
246 sat_solver_add_buffer( pSat, iVar0, iVar1, 0 );
247 }
248 // transfer variables
249 Gia_ManForEachCand( pPart, pObj, i )
250 if ( pCnf->pVarNums[i] >= 0 )
251 {
252 assert( Gia_ObjIsCi(pObj) || Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, i) ) == -1 );
253 Vec_IntWriteEntry( vSatMap, Vec_IntEntry(vPartMap, i), pCnf->pVarNums[i] );
254 }
255 Cnf_DataFree( pCnf );
256 Gia_ManStop( pPart );
257 // perform runs
258 nChanges = 0;
259 Vec_IntForEachEntry( vMiters, iLit, i )
260 {
261 if ( iLit == -1 )
262 continue;
263 assert( Vec_IntEntry(vSatMap, Abc_Lit2Var(iLit)) > 0 );
264 iLit = Abc_Lit2LitV( Vec_IntArray(vSatMap), iLit );
265 status = sat_solver_solve( pSat, &iLit, &iLit + 1, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
266 if ( status == l_True )
267 {
268 nChanges++;
269 continue;
270 }
271 if ( status == l_Undef )
272 {
273 printf( "Timeout reached after %d seconds. \n", nTimeOut );
274 RetValue = 0;
275 goto cleanup;
276 }
277 assert( status == l_False );
278 iLit0 = Vec_IntEntry( vLits0, i );
279 iLit1 = Vec_IntEntry( vLits1, i );
280 assert( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 );
281 if ( iLit1 >= 2 )
282 Vec_IntWriteEntry( vLits1, i, iLit0 );
283 else
284 Vec_IntWriteEntry( vLits0, i, iLit1 );
285 iLit0 = Vec_IntEntry( vLits0, i );
286 iLit1 = Vec_IntEntry( vLits1, i );
287 assert( iLit0 == iLit1 );
288 }
289 if ( fVerbose )
290 {
291 printf( "Frame %4d : ", f+1 );
292 printf( "Vars =%7d ", nSatVars );
293 printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
294 printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
295 printf( "AIG =%7d ", Gia_ManAndNum(pNew) );
296 printf( "Miters =%5d ", nMiters );
297 printf( "SAT =%5d ", nChanges );
298 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
299 }
300 if ( nChanges == 0 )
301 {
302 printf( "Reached a fixed point after %d frames. \n", f+1 );
303 break;
304 }
305 }
306 cleanup:
307
308 sat_solver_delete( pSat );
309 Gia_ManStopP( &pNew );
310 Vec_IntFree( vLits0 );
311 Vec_IntFree( vLits1 );
312 Vec_IntFree( vMiters );
313 Vec_IntFree( vSatMap );
314 Vec_IntFree( vPartMap );
315 Vec_IntFree( vCopies );
316 return RetValue;
317 }
318
319 /**Function*************************************************************
320
321 Synopsis []
322
323 Description []
324
325 SideEffects []
326
327 SeeAlso []
328
329 ***********************************************************************/
Gia_ManBmciTest(Gia_Man_t * p,Vec_Int_t * vInit,int nFrames,int nWords,int nTimeOut,int fSim,int fVerbose)330 int Gia_ManBmciTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
331 {
332 Vec_Int_t * vInit0 = Vec_IntStart( Gia_ManRegNum(p) );
333 Bmc_BmciPerform( p, vInit, vInit0, nFrames, nWords, nTimeOut, fVerbose );
334 Vec_IntFree( vInit0 );
335 return 1;
336 }
337
338 ////////////////////////////////////////////////////////////////////////
339 /// END OF FILE ///
340 ////////////////////////////////////////////////////////////////////////
341
342
343 ABC_NAMESPACE_IMPL_END
344
345