1 /**CFile****************************************************************
2
3 FileName [sswSemi.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Inductive prover with constraints.]
8
9 Synopsis [Semiformal for equivalence classes.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - September 1, 2008.]
16
17 Revision [$Id: sswSemi.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 typedef struct Ssw_Sem_t_ Ssw_Sem_t; // BMC manager
31
32 struct Ssw_Sem_t_
33 {
34 // parameters
35 int nConfMaxStart; // the starting conflict limit
36 int nConfMax; // the intermediate conflict limit
37 int nFramesSweep; // the number of frames to sweep
38 int fVerbose; // prints output statistics
39 // equivalences considered
40 Ssw_Man_t * pMan; // SAT sweeping manager
41 Vec_Ptr_t * vTargets; // the nodes that are watched
42 // storage for patterns
43 int nPatternsAlloc; // the max number of interesting states
44 int nPatterns; // the number of patterns
45 Vec_Ptr_t * vPatterns; // storage for the interesting states
46 Vec_Int_t * vHistory; // what state and how many steps
47 };
48
49 ////////////////////////////////////////////////////////////////////////
50 /// FUNCTION DEFINITIONS ///
51 ////////////////////////////////////////////////////////////////////////
52
53 /**Function*************************************************************
54
55 Synopsis []
56
57 Description []
58
59 SideEffects []
60
61 SeeAlso []
62
63 ***********************************************************************/
Ssw_SemManStart(Ssw_Man_t * pMan,int nConfMax,int fVerbose)64 Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
65 {
66 Ssw_Sem_t * p;
67 Aig_Obj_t * pObj;
68 int i;
69 // create interpolation manager
70 p = ABC_ALLOC( Ssw_Sem_t, 1 );
71 memset( p, 0, sizeof(Ssw_Sem_t) );
72 p->nConfMaxStart = nConfMax;
73 p->nConfMax = nConfMax;
74 p->nFramesSweep = Abc_MaxInt( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
75 p->fVerbose = fVerbose;
76 // equivalences considered
77 p->pMan = pMan;
78 p->vTargets = Vec_PtrAlloc( Saig_ManPoNum(p->pMan->pAig) );
79 Saig_ManForEachPo( p->pMan->pAig, pObj, i )
80 Vec_PtrPush( p->vTargets, Aig_ObjFanin0(pObj) );
81 // storage for patterns
82 p->nPatternsAlloc = 512;
83 p->nPatterns = 1;
84 p->vPatterns = Vec_PtrAllocSimInfo( Aig_ManRegNum(p->pMan->pAig), Abc_BitWordNum(p->nPatternsAlloc) );
85 Vec_PtrCleanSimInfo( p->vPatterns, 0, Abc_BitWordNum(p->nPatternsAlloc) );
86 p->vHistory = Vec_IntAlloc( 100 );
87 Vec_IntPush( p->vHistory, 0 );
88 // update arrays of the manager
89 assert( 0 );
90 /*
91 ABC_FREE( p->pMan->pNodeToFrames );
92 Vec_IntFree( p->pMan->vSatVars );
93 p->pMan->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep );
94 p->pMan->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) );
95 */
96 return p;
97 }
98
99 /**Function*************************************************************
100
101 Synopsis []
102
103 Description []
104
105 SideEffects []
106
107 SeeAlso []
108
109 ***********************************************************************/
Ssw_SemManStop(Ssw_Sem_t * p)110 void Ssw_SemManStop( Ssw_Sem_t * p )
111 {
112 Vec_PtrFree( p->vTargets );
113 Vec_PtrFree( p->vPatterns );
114 Vec_IntFree( p->vHistory );
115 ABC_FREE( p );
116 }
117
118 /**Function*************************************************************
119
120 Synopsis []
121
122 Description []
123
124 SideEffects []
125
126 SeeAlso []
127
128 ***********************************************************************/
Ssw_SemCheckTargets(Ssw_Sem_t * p)129 int Ssw_SemCheckTargets( Ssw_Sem_t * p )
130 {
131 Aig_Obj_t * pObj;
132 int i;
133 Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
134 if ( !Ssw_ObjIsConst1Cand(p->pMan->pAig, pObj) )
135 return 1;
136 return 0;
137 }
138
139 /**Function*************************************************************
140
141 Synopsis []
142
143 Description []
144
145 SideEffects []
146
147 SeeAlso []
148
149 ***********************************************************************/
Ssw_ManFilterBmcSavePattern(Ssw_Sem_t * p)150 void Ssw_ManFilterBmcSavePattern( Ssw_Sem_t * p )
151 {
152 unsigned * pInfo;
153 Aig_Obj_t * pObj;
154 int i;
155 if ( p->nPatterns >= p->nPatternsAlloc )
156 return;
157 Saig_ManForEachLo( p->pMan->pAig, pObj, i )
158 {
159 pInfo = (unsigned *)Vec_PtrEntry( p->vPatterns, i );
160 if ( Abc_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) )
161 Abc_InfoSetBit( pInfo, p->nPatterns );
162 }
163 p->nPatterns++;
164 }
165
166 /**Function*************************************************************
167
168 Synopsis [Performs fraiging for the internal nodes.]
169
170 Description []
171
172 SideEffects []
173
174 SeeAlso []
175
176 ***********************************************************************/
Ssw_ManFilterBmc(Ssw_Sem_t * pBmc,int iPat,int fCheckTargets)177 int Ssw_ManFilterBmc( Ssw_Sem_t * pBmc, int iPat, int fCheckTargets )
178 {
179 Ssw_Man_t * p = pBmc->pMan;
180 Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
181 unsigned * pInfo;
182 int i, f, RetValue, fFirst = 0;
183 abctime clk;
184 clk = Abc_Clock();
185
186 // start initialized timeframes
187 p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 );
188 Saig_ManForEachLo( p->pAig, pObj, i )
189 {
190 pInfo = (unsigned *)Vec_PtrEntry( pBmc->vPatterns, i );
191 pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Abc_InfoHasBit(pInfo, iPat) );
192 Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
193 }
194
195 // sweep internal nodes
196 RetValue = pBmc->nFramesSweep;
197 for ( f = 0; f < pBmc->nFramesSweep; f++ )
198 {
199 // map constants and PIs
200 Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
201 Saig_ManForEachPi( p->pAig, pObj, i )
202 Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
203 // sweep internal nodes
204 Aig_ManForEachNode( p->pAig, pObj, i )
205 {
206 pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
207 Ssw_ObjSetFrame( p, pObj, f, pObjNew );
208 if ( Ssw_ManSweepNode( p, pObj, f, 1, NULL ) )
209 {
210 Ssw_ManFilterBmcSavePattern( pBmc );
211 if ( fFirst == 0 )
212 {
213 fFirst = 1;
214 pBmc->nConfMax *= 10;
215 }
216 }
217 if ( f > 0 && p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
218 {
219 RetValue = -1;
220 break;
221 }
222 }
223 // quit if this is the last timeframe
224 if ( p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
225 {
226 RetValue += f + 1;
227 break;
228 }
229 if ( fCheckTargets && Ssw_SemCheckTargets( pBmc ) )
230 break;
231 // transfer latch input to the latch outputs
232 // build logic cones for register outputs
233 Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
234 {
235 pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
236 Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
237 Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );
238 }
239 //Abc_Print( 1, "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
240 }
241 if ( fFirst )
242 pBmc->nConfMax /= 10;
243
244 // cleanup
245 Ssw_ClassesCheck( p->ppClasses );
246 p->timeBmc += Abc_Clock() - clk;
247 return RetValue;
248 }
249
250 /**Function*************************************************************
251
252 Synopsis [Returns 1 if one of the targets has failed.]
253
254 Description []
255
256 SideEffects []
257
258 SeeAlso []
259
260 ***********************************************************************/
Ssw_FilterUsingSemi(Ssw_Man_t * pMan,int fCheckTargets,int nConfMax,int fVerbose)261 int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose )
262 {
263 Ssw_Sem_t * p;
264 int RetValue, Frames, Iter;
265 abctime clk = Abc_Clock();
266 p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
267 if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
268 {
269 assert( 0 );
270 Ssw_SemManStop( p );
271 return 1;
272 }
273 if ( fVerbose )
274 {
275 Abc_Print( 1, "AIG : C = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n",
276 Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
277 Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
278 }
279 RetValue = 0;
280 for ( Iter = 0; Iter < p->nPatterns; Iter++ )
281 {
282 clk = Abc_Clock();
283 pMan->pMSat = Ssw_SatStart( 0 );
284 Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
285 if ( fVerbose )
286 {
287 Abc_Print( 1, "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
288 Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
289 Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
290 p->pMan->nSatFailsReal? "f" : " " );
291 ABC_PRT( "T", Abc_Clock() - clk );
292 }
293 Ssw_ManCleanup( p->pMan );
294 if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
295 {
296 Abc_Print( 1, "Target is hit!!!\n" );
297 RetValue = 1;
298 }
299 if ( p->nPatterns >= p->nPatternsAlloc )
300 break;
301 }
302 Ssw_SemManStop( p );
303
304 pMan->nStrangers = 0;
305 pMan->nSatCalls = 0;
306 pMan->nSatProof = 0;
307 pMan->nSatFailsReal = 0;
308 pMan->nSatCallsUnsat = 0;
309 pMan->nSatCallsSat = 0;
310 pMan->timeSimSat = 0;
311 pMan->timeSat = 0;
312 pMan->timeSatSat = 0;
313 pMan->timeSatUnsat = 0;
314 pMan->timeSatUndec = 0;
315 return RetValue;
316 }
317
318 ////////////////////////////////////////////////////////////////////////
319 /// END OF FILE ///
320 ////////////////////////////////////////////////////////////////////////
321
322
323 ABC_NAMESPACE_IMPL_END
324