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