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