1 /**CFile****************************************************************
2
3 FileName [sswPairs.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Inductive prover with constraints.]
8
9 Synopsis [Calls to the SAT solver.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - September 1, 2008.]
16
17 Revision [$Id: sswPairs.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "sswInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Reports the status of the miter.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Ssw_MiterStatus(Aig_Man_t * p,int fVerbose)45 int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose )
46 {
47 Aig_Obj_t * pObj, * pChild;
48 int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
49 // if ( p->pData )
50 // return 0;
51 Saig_ManForEachPo( p, pObj, i )
52 {
53 pChild = Aig_ObjChild0(pObj);
54 // check if the output is constant 0
55 if ( pChild == Aig_ManConst0(p) )
56 {
57 CountConst0++;
58 continue;
59 }
60 // check if the output is constant 1
61 if ( pChild == Aig_ManConst1(p) )
62 {
63 CountNonConst0++;
64 continue;
65 }
66 // check if the output is a primary input
67 if ( p->nRegs == 0 && Aig_ObjIsCi(Aig_Regular(pChild)) )
68 {
69 CountNonConst0++;
70 continue;
71 }
72 // check if the output can be not constant 0
73 if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
74 {
75 CountNonConst0++;
76 continue;
77 }
78 CountUndecided++;
79 }
80
81 if ( fVerbose )
82 {
83 Abc_Print( 1, "Miter has %d outputs. ", Saig_ManPoNum(p) );
84 Abc_Print( 1, "Const0 = %d. ", CountConst0 );
85 Abc_Print( 1, "NonConst0 = %d. ", CountNonConst0 );
86 Abc_Print( 1, "Undecided = %d. ", CountUndecided );
87 Abc_Print( 1, "\n" );
88 }
89
90 if ( CountNonConst0 )
91 return 0;
92 if ( CountUndecided )
93 return -1;
94 return 1;
95 }
96
97 /**Function*************************************************************
98
99 Synopsis [Transfer equivalent pairs to the miter.]
100
101 Description []
102
103 SideEffects []
104
105 SeeAlso []
106
107 ***********************************************************************/
Ssw_TransferSignalPairs(Aig_Man_t * pMiter,Aig_Man_t * pAig1,Aig_Man_t * pAig2,Vec_Int_t * vIds1,Vec_Int_t * vIds2)108 Vec_Int_t * Ssw_TransferSignalPairs( Aig_Man_t * pMiter, Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2 )
109 {
110 Vec_Int_t * vIds;
111 Aig_Obj_t * pObj1, * pObj2;
112 Aig_Obj_t * pObj1m, * pObj2m;
113 int i;
114 vIds = Vec_IntAlloc( 2 * Vec_IntSize(vIds1) );
115 for ( i = 0; i < Vec_IntSize(vIds1); i++ )
116 {
117 pObj1 = Aig_ManObj( pAig1, Vec_IntEntry(vIds1, i) );
118 pObj2 = Aig_ManObj( pAig2, Vec_IntEntry(vIds2, i) );
119 pObj1m = Aig_Regular((Aig_Obj_t *)pObj1->pData);
120 pObj2m = Aig_Regular((Aig_Obj_t *)pObj2->pData);
121 assert( pObj1m && pObj2m );
122 if ( pObj1m == pObj2m )
123 continue;
124 if ( pObj1m->Id < pObj2m->Id )
125 {
126 Vec_IntPush( vIds, pObj1m->Id );
127 Vec_IntPush( vIds, pObj2m->Id );
128 }
129 else
130 {
131 Vec_IntPush( vIds, pObj2m->Id );
132 Vec_IntPush( vIds, pObj1m->Id );
133 }
134 }
135 return vIds;
136 }
137
138 /**Function*************************************************************
139
140 Synopsis [Transform pairs into class representation.]
141
142 Description []
143
144 SideEffects []
145
146 SeeAlso []
147
148 ***********************************************************************/
Ssw_TransformPairsIntoTempClasses(Vec_Int_t * vPairs,int nObjNumMax)149 Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumMax )
150 {
151 Vec_Int_t ** pvClasses; // vector of classes
152 int * pReprs; // mapping nodes into their representatives
153 int Entry, idObj, idRepr, idReprObj, idReprRepr, i;
154 // allocate data-structures
155 pvClasses = ABC_CALLOC( Vec_Int_t *, nObjNumMax );
156 pReprs = ABC_ALLOC( int, nObjNumMax );
157 for ( i = 0; i < nObjNumMax; i++ )
158 pReprs[i] = -1;
159 // consider pairs
160 for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
161 {
162 // get both objects
163 idRepr = Vec_IntEntry( vPairs, i );
164 idObj = Vec_IntEntry( vPairs, i+1 );
165 assert( idObj > 0 );
166 assert( (pReprs[idRepr] == -1) || (pvClasses[pReprs[idRepr]] != NULL) );
167 assert( (pReprs[idObj] == -1) || (pvClasses[pReprs[idObj] ] != NULL) );
168 // get representatives of both objects
169 idReprRepr = pReprs[idRepr];
170 idReprObj = pReprs[idObj];
171 // check different situations
172 if ( idReprRepr == -1 && idReprObj == -1 )
173 { // they do not have classes
174 // create a class
175 pvClasses[idRepr] = Vec_IntAlloc( 4 );
176 Vec_IntPush( pvClasses[idRepr], idRepr );
177 Vec_IntPush( pvClasses[idRepr], idObj );
178 pReprs[ idRepr ] = idRepr;
179 pReprs[ idObj ] = idRepr;
180 }
181 else if ( idReprRepr >= 0 && idReprObj == -1 )
182 { // representative has a class
183 // add iObj to the same class
184 Vec_IntPushUniqueOrder( pvClasses[idReprRepr], idObj );
185 pReprs[ idObj ] = idReprRepr;
186 }
187 else if ( idReprRepr == -1 && idReprObj >= 0 )
188 { // object has a class
189 assert( idReprObj != idRepr );
190 if ( idReprObj < idRepr )
191 { // add idRepr to the same class
192 Vec_IntPushUniqueOrder( pvClasses[idReprObj], idRepr );
193 pReprs[ idRepr ] = idReprObj;
194 }
195 else // if ( idReprObj > idRepr )
196 { // make idRepr new representative
197 Vec_IntPushFirst( pvClasses[idReprObj], idRepr );
198 pvClasses[idRepr] = pvClasses[idReprObj];
199 pvClasses[idReprObj] = NULL;
200 // set correct representatives of each node
201 Vec_IntForEachEntry( pvClasses[idRepr], Entry, i )
202 pReprs[ Entry ] = idRepr;
203 }
204 }
205 else // if ( idReprRepr >= 0 && idReprObj >= 0 )
206 { // both have classes
207 if ( idReprRepr == idReprObj )
208 { // the classes are the same
209 // nothing to do
210 }
211 else
212 { // the classes are different
213 // find the repr of the new class
214 if ( idReprRepr < idReprObj )
215 {
216 Vec_IntForEachEntry( pvClasses[idReprObj], Entry, i )
217 {
218 Vec_IntPushUniqueOrder( pvClasses[idReprRepr], Entry );
219 pReprs[ Entry ] = idReprRepr;
220 }
221 Vec_IntFree( pvClasses[idReprObj] );
222 pvClasses[idReprObj] = NULL;
223 }
224 else // if ( idReprRepr > idReprObj )
225 {
226 Vec_IntForEachEntry( pvClasses[idReprRepr], Entry, i )
227 {
228 Vec_IntPushUniqueOrder( pvClasses[idReprObj], Entry );
229 pReprs[ Entry ] = idReprObj;
230 }
231 Vec_IntFree( pvClasses[idReprRepr] );
232 pvClasses[idReprRepr] = NULL;
233 }
234 }
235 }
236 }
237 ABC_FREE( pReprs );
238 return pvClasses;
239 }
240
241 /**Function*************************************************************
242
243 Synopsis []
244
245 Description []
246
247 SideEffects []
248
249 SeeAlso []
250
251 ***********************************************************************/
Ssw_FreeTempClasses(Vec_Int_t ** pvClasses,int nObjNumMax)252 void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax )
253 {
254 int i;
255 for ( i = 0; i < nObjNumMax; i++ )
256 if ( pvClasses[i] )
257 Vec_IntFree( pvClasses[i] );
258 ABC_FREE( pvClasses );
259 }
260
261 /**Function*************************************************************
262
263 Synopsis [Performs signal correspondence for the miter of two AIGs with node pairs defined.]
264
265 Description []
266
267 SideEffects []
268
269 SeeAlso []
270
271 ***********************************************************************/
Ssw_SignalCorrespondenceWithPairs(Aig_Man_t * pAig1,Aig_Man_t * pAig2,Vec_Int_t * vIds1,Vec_Int_t * vIds2,Ssw_Pars_t * pPars)272 Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars )
273 {
274 Ssw_Man_t * p;
275 Aig_Man_t * pAigNew, * pMiter;
276 Ssw_Pars_t Pars;
277 Vec_Int_t * vPairs;
278 Vec_Int_t ** pvClasses;
279 assert( Vec_IntSize(vIds1) == Vec_IntSize(vIds2) );
280 // create sequential miter
281 pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
282 Aig_ManCleanup( pMiter );
283 // transfer information to the miter
284 vPairs = Ssw_TransferSignalPairs( pMiter, pAig1, pAig2, vIds1, vIds2 );
285 // create representation of the classes
286 pvClasses = Ssw_TransformPairsIntoTempClasses( vPairs, Aig_ManObjNumMax(pMiter) );
287 Vec_IntFree( vPairs );
288 // if parameters are not given, create them
289 if ( pPars == NULL )
290 Ssw_ManSetDefaultParams( pPars = &Pars );
291 // start the induction manager
292 p = Ssw_ManCreate( pMiter, pPars );
293 // create equivalence classes using these IDs
294 p->ppClasses = Ssw_ClassesPreparePairs( pMiter, pvClasses );
295 p->pSml = Ssw_SmlStart( pMiter, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
296 Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
297 // perform refinement of classes
298 pAigNew = Ssw_SignalCorrespondenceRefine( p );
299 // cleanup
300 Ssw_FreeTempClasses( pvClasses, Aig_ManObjNumMax(pMiter) );
301 Ssw_ManStop( p );
302 Aig_ManStop( pMiter );
303 return pAigNew;
304 }
305
306 /**Function*************************************************************
307
308 Synopsis [Runs inductive SEC for the miter of two AIGs with node pairs defined.]
309
310 Description []
311
312 SideEffects []
313
314 SeeAlso []
315
316 ***********************************************************************/
Ssw_SignalCorrespondeceTestPairs(Aig_Man_t * pAig)317 Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
318 {
319 Aig_Man_t * pAigNew, * pAigRes;
320 Ssw_Pars_t Pars, * pPars = &Pars;
321 Vec_Int_t * vIds1, * vIds2;
322 Aig_Obj_t * pObj, * pRepr;
323 int RetValue, i;
324 abctime clk = Abc_Clock();
325 Ssw_ManSetDefaultParams( pPars );
326 pPars->fVerbose = 1;
327 pAigNew = Ssw_SignalCorrespondence( pAig, pPars );
328 // record pairs of equivalent nodes
329 vIds1 = Vec_IntAlloc( Aig_ManObjNumMax(pAig) );
330 vIds2 = Vec_IntAlloc( Aig_ManObjNumMax(pAig) );
331 Aig_ManForEachObj( pAig, pObj, i )
332 {
333 pRepr = Aig_Regular((Aig_Obj_t *)pObj->pData);
334 if ( pRepr == NULL )
335 continue;
336 if ( Aig_ManObj(pAigNew, pRepr->Id) == NULL )
337 continue;
338 /*
339 if ( Aig_ObjIsNode(pObj) )
340 Abc_Print( 1, "n " );
341 else if ( Saig_ObjIsPi(pAig, pObj) )
342 Abc_Print( 1, "pi " );
343 else if ( Saig_ObjIsLo(pAig, pObj) )
344 Abc_Print( 1, "lo " );
345 */
346 Vec_IntPush( vIds1, Aig_ObjId(pObj) );
347 Vec_IntPush( vIds2, Aig_ObjId(pRepr) );
348 }
349 Abc_Print( 1, "Recorded %d pairs (before: %d after: %d).\n", Vec_IntSize(vIds1), Aig_ManObjNumMax(pAig), Aig_ManObjNumMax(pAigNew) );
350 // try the new AIGs
351 pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig, pAigNew, vIds1, vIds2, pPars );
352 Vec_IntFree( vIds1 );
353 Vec_IntFree( vIds2 );
354 // report the results
355 RetValue = Ssw_MiterStatus( pAigRes, 1 );
356 if ( RetValue == 1 )
357 Abc_Print( 1, "Verification successful. " );
358 else if ( RetValue == 0 )
359 Abc_Print( 1, "Verification failed with the counter-example. " );
360 else
361 Abc_Print( 1, "Verification UNDECIDED. Remaining registers %d (total %d). ",
362 Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig) + Aig_ManRegNum(pAigNew) );
363 ABC_PRT( "Time", Abc_Clock() - clk );
364 // cleanup
365 Aig_ManStop( pAigNew );
366 return pAigRes;
367 }
368
369 /**Function*************************************************************
370
371 Synopsis [Runs inductive SEC for the miter of two AIGs with node pairs defined.]
372
373 Description []
374
375 SideEffects []
376
377 SeeAlso []
378
379 ***********************************************************************/
Ssw_SecWithPairs(Aig_Man_t * pAig1,Aig_Man_t * pAig2,Vec_Int_t * vIds1,Vec_Int_t * vIds2,Ssw_Pars_t * pPars)380 int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars )
381 {
382 Aig_Man_t * pAigRes;
383 int RetValue;
384 abctime clk = Abc_Clock();
385 assert( vIds1 != NULL && vIds2 != NULL );
386 // try the new AIGs
387 Abc_Print( 1, "Performing specialized verification with node pairs.\n" );
388 pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig1, pAig2, vIds1, vIds2, pPars );
389 // report the results
390 RetValue = Ssw_MiterStatus( pAigRes, 1 );
391 if ( RetValue == 1 )
392 Abc_Print( 1, "Verification successful. " );
393 else if ( RetValue == 0 )
394 Abc_Print( 1, "Verification failed with a counter-example. " );
395 else
396 Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
397 Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
398 ABC_PRT( "Time", Abc_Clock() - clk );
399 // cleanup
400 Aig_ManStop( pAigRes );
401 return RetValue;
402 }
403
404 /**Function*************************************************************
405
406 Synopsis [Runs inductive SEC for the miter of two AIGs.]
407
408 Description []
409
410 SideEffects []
411
412 SeeAlso []
413
414 ***********************************************************************/
Ssw_SecGeneral(Aig_Man_t * pAig1,Aig_Man_t * pAig2,Ssw_Pars_t * pPars)415 int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
416 {
417 Aig_Man_t * pAigRes, * pMiter;
418 int RetValue;
419 abctime clk = Abc_Clock();
420 // try the new AIGs
421 Abc_Print( 1, "Performing general verification without node pairs.\n" );
422 pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
423 Aig_ManCleanup( pMiter );
424 pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
425 Aig_ManStop( pMiter );
426 // report the results
427 RetValue = Ssw_MiterStatus( pAigRes, 1 );
428 if ( RetValue == 1 )
429 Abc_Print( 1, "Verification successful. " );
430 else if ( RetValue == 0 )
431 Abc_Print( 1, "Verification failed with a counter-example. " );
432 else
433 Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
434 Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
435 ABC_PRT( "Time", Abc_Clock() - clk );
436 // cleanup
437 Aig_ManStop( pAigRes );
438 return RetValue;
439 }
440
441 /**Function*************************************************************
442
443 Synopsis [Runs inductive SEC for the miter of two AIGs.]
444
445 Description []
446
447 SideEffects []
448
449 SeeAlso []
450
451 ***********************************************************************/
Ssw_SecGeneralMiter(Aig_Man_t * pMiter,Ssw_Pars_t * pPars)452 int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
453 {
454 Aig_Man_t * pAigRes;
455 int RetValue;
456 abctime clk = Abc_Clock();
457 // try the new AIGs
458 // Abc_Print( 1, "Performing general verification without node pairs.\n" );
459 pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
460 // report the results
461 RetValue = Ssw_MiterStatus( pAigRes, 1 );
462 if ( RetValue == 1 )
463 Abc_Print( 1, "Verification successful. " );
464 else if ( RetValue == 0 )
465 Abc_Print( 1, "Verification failed with a counter-example. " );
466 else
467 Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
468 Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) );
469 ABC_PRT( "Time", Abc_Clock() - clk );
470 // cleanup
471 Aig_ManStop( pAigRes );
472 return RetValue;
473 }
474
475 ////////////////////////////////////////////////////////////////////////
476 /// END OF FILE ///
477 ////////////////////////////////////////////////////////////////////////
478
479
480 ABC_NAMESPACE_IMPL_END
481