1 /**CFile****************************************************************
2 
3   FileName    [sswLcorr.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Inductive prover with constraints.]
8 
9   Synopsis    [Latch correspondence.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - September 1, 2008.]
16 
17   Revision    [$Id: sswLcorr.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sswInt.h"
22 //#include "bar.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 ///                        DECLARATIONS                              ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 ////////////////////////////////////////////////////////////////////////
32 ///                     FUNCTION DEFINITIONS                         ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37   Synopsis    [Tranfers simulation information from FRAIG to AIG.]
38 
39   Description []
40 
41   SideEffects []
42 
43   SeeAlso     []
44 
45 ***********************************************************************/
Ssw_ManSweepTransfer(Ssw_Man_t * p)46 void Ssw_ManSweepTransfer( Ssw_Man_t * p )
47 {
48     Aig_Obj_t * pObj, * pObjFraig;
49     unsigned * pInfo;
50     int i;
51     // transfer simulation information
52     Aig_ManForEachCi( p->pAig, pObj, i )
53     {
54         pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
55         if ( pObjFraig == Aig_ManConst0(p->pFrames) )
56         {
57             Ssw_SmlObjAssignConst( p->pSml, pObj, 0, 0 );
58             continue;
59         }
60         assert( !Aig_IsComplement(pObjFraig) );
61         assert( Aig_ObjIsCi(pObjFraig) );
62         pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) );
63         Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
64     }
65 }
66 
67 /**Function*************************************************************
68 
69   Synopsis    [Performs one round of simulation with counter-examples.]
70 
71   Description []
72 
73   SideEffects []
74 
75   SeeAlso     []
76 
77 ***********************************************************************/
Ssw_ManSweepResimulate(Ssw_Man_t * p)78 int Ssw_ManSweepResimulate( Ssw_Man_t * p )
79 {
80     int RetValue1, RetValue2;
81     abctime clk = Abc_Clock();
82     // transfer PI simulation information from storage
83     Ssw_ManSweepTransfer( p );
84     // simulate internal nodes
85     Ssw_SmlSimulateOneFrame( p->pSml );
86     // check equivalence classes
87     RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
88     RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
89     // prepare simulation info for the next round
90     Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
91     p->nPatterns = 0;
92     p->nSimRounds++;
93 p->timeSimSat += Abc_Clock() - clk;
94     return RetValue1 > 0 || RetValue2 > 0;
95 }
96 
97 /**Function*************************************************************
98 
99   Synopsis    [Saves one counter-example into internal storage.]
100 
101   Description []
102 
103   SideEffects []
104 
105   SeeAlso     []
106 
107 ***********************************************************************/
Ssw_SmlAddPattern(Ssw_Man_t * p,Aig_Obj_t * pRepr,Aig_Obj_t * pCand)108 void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand )
109 {
110     Aig_Obj_t * pObj;
111     unsigned * pInfo;
112     int i, nVarNum, Value;
113     Vec_PtrForEachEntry( Aig_Obj_t *, p->pMSat->vUsedPis, pObj, i )
114     {
115         nVarNum = Ssw_ObjSatNum( p->pMSat, pObj );
116         assert( nVarNum > 0 );
117         Value = sat_solver_var_value( p->pMSat->pSat, nVarNum );
118         if ( Value == 0 )
119             continue;
120         pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObj) );
121         Abc_InfoSetBit( pInfo, p->nPatterns );
122     }
123 }
124 
125 /**Function*************************************************************
126 
127   Synopsis    [Builds fraiged logic cone of the node.]
128 
129   Description []
130 
131   SideEffects []
132 
133   SeeAlso     []
134 
135 ***********************************************************************/
Ssw_ManBuildCone_rec(Ssw_Man_t * p,Aig_Obj_t * pObj)136 void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
137 {
138     Aig_Obj_t * pObjNew;
139     assert( !Aig_IsComplement(pObj) );
140     if ( Ssw_ObjFrame( p, pObj, 0 ) )
141         return;
142     assert( Aig_ObjIsNode(pObj) );
143     Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObj) );
144     Ssw_ManBuildCone_rec( p, Aig_ObjFanin1(pObj) );
145     pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
146     Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
147 }
148 
149 /**Function*************************************************************
150 
151   Synopsis    [Recycles the SAT solver.]
152 
153   Description []
154 
155   SideEffects []
156 
157   SeeAlso     []
158 
159 ***********************************************************************/
Ssw_ManSweepLatchOne(Ssw_Man_t * p,Aig_Obj_t * pObjRepr,Aig_Obj_t * pObj)160 void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj )
161 {
162     Aig_Obj_t * pObjFraig, * pObjReprFraig, * pObjLi;
163     int RetValue;
164     abctime clk;
165     assert( Aig_ObjIsCi(pObj) );
166     assert( Aig_ObjIsCi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
167     // check if it makes sense to skip some calls
168     if ( p->nCallsCount > 100 && p->nCallsUnsat < p->nCallsSat )
169     {
170         if ( ++p->nCallsDelta < 0 )
171             return;
172     }
173     p->nCallsDelta = 0;
174 clk = Abc_Clock();
175     // get the fraiged node
176     pObjLi = Saig_ObjLoToLi( p->pAig, pObj );
177     Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
178     pObjFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
179     // get the fraiged representative
180     if ( Aig_ObjIsCi(pObjRepr) )
181     {
182         pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr );
183         Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
184         pObjReprFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
185     }
186     else
187         pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, 0 );
188 p->timeReduce += Abc_Clock() - clk;
189     // if the fraiged nodes are the same, return
190     if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
191         return;
192     p->nRecycleCalls++;
193     p->nCallsCount++;
194 
195     // check equivalence of the two nodes
196     if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
197     {
198         p->nPatterns++;
199         p->nStrangers++;
200         p->fRefined = 1;
201     }
202     else
203     {
204         RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
205         if ( RetValue == 1 )  // proved equivalence
206         {
207             p->nCallsUnsat++;
208             return;
209         }
210         if ( RetValue == -1 ) // timed out
211         {
212             Ssw_ClassesRemoveNode( p->ppClasses, pObj );
213             p->nCallsUnsat++;
214             p->fRefined = 1;
215             return;
216         }
217         else // disproved equivalence
218         {
219             Ssw_SmlAddPattern( p, pObjRepr, pObj );
220             p->nPatterns++;
221             p->nCallsSat++;
222             p->fRefined = 1;
223         }
224     }
225 }
226 
227 /**Function*************************************************************
228 
229   Synopsis    [Performs one iteration of sweeping latches.]
230 
231   Description []
232 
233   SideEffects []
234 
235   SeeAlso     []
236 
237 ***********************************************************************/
Ssw_ManSweepLatch(Ssw_Man_t * p)238 int Ssw_ManSweepLatch( Ssw_Man_t * p )
239 {
240 //    Bar_Progress_t * pProgress = NULL;
241     Vec_Ptr_t * vClass;
242     Aig_Obj_t * pObj, * pRepr, * pTemp;
243     int i, k;
244 
245     // start the timeframe
246     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) );
247     // map constants and PIs
248     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) );
249     Saig_ManForEachPi( p->pAig, pObj, i )
250         Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(p->pFrames) );
251 
252     // implement equivalence classes
253     Saig_ManForEachLo( p->pAig, pObj, i )
254     {
255         pRepr = Aig_ObjRepr( p->pAig, pObj );
256         if ( pRepr == NULL )
257         {
258             pTemp = Aig_ObjCreateCi(p->pFrames);
259             pTemp->pData = pObj;
260         }
261         else
262             pTemp = Aig_NotCond( Ssw_ObjFrame(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase );
263         Ssw_ObjSetFrame( p, pObj, 0, pTemp );
264     }
265     Aig_ManSetCioIds( p->pFrames );
266 
267     // prepare simulation info
268     assert( p->vSimInfo == NULL );
269     p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 );
270     Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
271 
272     // go through the registers
273 //    if ( p->pPars->fVerbose )
274 //        pProgress = Bar_ProgressStart( stdout, Aig_ManRegNum(p->pAig) );
275     vClass = Vec_PtrAlloc( 100 );
276     p->fRefined = 0;
277     p->nCallsCount = p->nCallsSat = p->nCallsUnsat = 0;
278     Saig_ManForEachLo( p->pAig, pObj, i )
279     {
280 //        if ( p->pPars->fVerbose )
281 //            Bar_ProgressUpdate( pProgress, i, NULL );
282         // consider the case of constant candidate
283         if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
284             Ssw_ManSweepLatchOne( p, Aig_ManConst1(p->pAig), pObj );
285         else
286         {
287             // consider the case of equivalence class
288             Ssw_ClassesCollectClass( p->ppClasses, pObj, vClass );
289             if ( Vec_PtrSize(vClass) == 0 )
290                 continue;
291             // try to prove equivalences in this class
292             Vec_PtrForEachEntry( Aig_Obj_t *, vClass, pTemp, k )
293                 if ( Aig_ObjRepr(p->pAig, pTemp) == pObj )
294                 {
295                     Ssw_ManSweepLatchOne( p, pObj, pTemp );
296                     if ( p->nPatterns == 32 )
297                         break;
298                 }
299         }
300         // resimulate
301         if ( p->nPatterns == 32 )
302             Ssw_ManSweepResimulate( p );
303         // attempt recycling the SAT solver
304         if ( p->pPars->nSatVarMax &&
305              p->pMSat->nSatVars > p->pPars->nSatVarMax &&
306              p->nRecycleCalls > p->pPars->nRecycleCalls )
307         {
308             p->nVarsMax  = Abc_MaxInt( p->nVarsMax,  p->pMSat->nSatVars );
309             p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
310             Ssw_SatStop( p->pMSat );
311             p->pMSat = Ssw_SatStart( 0 );
312             p->nRecycles++;
313             p->nRecycleCalls = 0;
314         }
315     }
316 //    ABC_PRT( "reduce", p->timeReduce );
317 //    Aig_TableProfile( p->pFrames );
318 //    Abc_Print( 1, "And gates = %d\n", Aig_ManNodeNum(p->pFrames) );
319     // resimulate
320     if ( p->nPatterns > 0 )
321         Ssw_ManSweepResimulate( p );
322     // cleanup
323     Vec_PtrFree( vClass );
324 //    if ( p->pPars->fVerbose )
325 //        Bar_ProgressStop( pProgress );
326 
327     // cleanup
328 //    Ssw_ClassesCheck( p->ppClasses );
329     return p->fRefined;
330 }
331 
332 ////////////////////////////////////////////////////////////////////////
333 ///                       END OF FILE                                ///
334 ////////////////////////////////////////////////////////////////////////
335 
336 
337 ABC_NAMESPACE_IMPL_END
338