1 /**CFile****************************************************************
2
3 FileName [sscCore.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT sweeping under constraints.]
8
9 Synopsis [The core procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 29, 2008.]
16
17 Revision [$Id: sscCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "sscInt.h"
22 #include "proof/cec/cec.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 [This procedure sets default parameters.]
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Ssc_ManSetDefaultParams(Ssc_Pars_t * p)46 void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
47 {
48 memset( p, 0, sizeof(Ssc_Pars_t) );
49 p->nWords = 1; // the number of simulation words
50 p->nBTLimit = 1000; // conflict limit at a node
51 p->nSatVarMax = 5000; // the max number of SAT variables
52 p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
53 p->fVerbose = 0; // verbose stats
54 }
55
56 /**Function*************************************************************
57
58 Synopsis []
59
60 Description []
61
62 SideEffects []
63
64 SeeAlso []
65
66 ***********************************************************************/
Ssc_ManStop(Ssc_Man_t * p)67 void Ssc_ManStop( Ssc_Man_t * p )
68 {
69 Vec_IntFreeP( &p->vFront );
70 Vec_IntFreeP( &p->vFanins );
71 Vec_IntFreeP( &p->vPattern );
72 Vec_IntFreeP( &p->vDisPairs );
73 Vec_IntFreeP( &p->vPivot );
74 Vec_IntFreeP( &p->vId2Var );
75 Vec_IntFreeP( &p->vVar2Id );
76 if ( p->pSat ) sat_solver_delete( p->pSat );
77 Gia_ManStopP( &p->pFraig );
78 ABC_FREE( p );
79 }
Ssc_ManStart(Gia_Man_t * pAig,Gia_Man_t * pCare,Ssc_Pars_t * pPars)80 Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
81 {
82 Ssc_Man_t * p;
83 p = ABC_CALLOC( Ssc_Man_t, 1 );
84 p->pPars = pPars;
85 p->pAig = pAig;
86 p->pCare = pCare;
87 p->pFraig = Gia_ManDupDfs( p->pCare );
88 assert( Vec_IntSize(&p->pFraig->vHTable) == 0 );
89 assert( !Gia_ManHasDangling(p->pFraig) );
90 Gia_ManInvertPos( p->pFraig );
91 Ssc_ManStartSolver( p );
92 if ( p->pSat == NULL )
93 {
94 printf( "Constraints are UNSAT after propagation.\n" );
95 Ssc_ManStop( p );
96 return (Ssc_Man_t *)(ABC_PTRINT_T)1;
97 }
98 // p->vPivot = Ssc_GiaFindPivotSim( p->pFraig );
99 // Vec_IntFreeP( &p->vPivot );
100 p->vPivot = Ssc_ManFindPivotSat( p );
101 if ( p->vPivot == (Vec_Int_t *)(ABC_PTRINT_T)1 )
102 {
103 printf( "Constraints are UNSAT.\n" );
104 Ssc_ManStop( p );
105 return (Ssc_Man_t *)(ABC_PTRINT_T)1;
106 }
107 if ( p->vPivot == NULL )
108 {
109 printf( "Conflict limit is reached while trying to find one SAT assignment.\n" );
110 Ssc_ManStop( p );
111 return NULL;
112 }
113 sat_solver_bookmark( p->pSat );
114 // Vec_IntPrint( p->vPivot );
115 Gia_ManSetPhasePattern( p->pAig, p->vPivot );
116 Gia_ManSetPhasePattern( p->pCare, p->vPivot );
117 if ( Gia_ManCheckCoPhase(p->pCare) )
118 {
119 printf( "Computed reference pattern violates %d constraints (this is a bug!).\n", Gia_ManCheckCoPhase(p->pCare) );
120 Ssc_ManStop( p );
121 return NULL;
122 }
123 // other things
124 p->vDisPairs = Vec_IntAlloc( 100 );
125 p->vPattern = Vec_IntAlloc( 100 );
126 p->vFanins = Vec_IntAlloc( 100 );
127 p->vFront = Vec_IntAlloc( 100 );
128 Ssc_GiaClassesInit( pAig );
129 // now it is ready for refinement using simulation
130 return p;
131 }
Ssc_ManPrintStats(Ssc_Man_t * p)132 void Ssc_ManPrintStats( Ssc_Man_t * p )
133 {
134 Abc_Print( 1, "Parameters: SimWords = %d. SatConfs = %d. SatVarMax = %d. CallsRec = %d. Verbose = %d.\n",
135 p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax, p->pPars->nCallsRecycle, p->pPars->fVerbose );
136 Abc_Print( 1, "SAT calls : Total = %d. Proof = %d. Cex = %d. Undec = %d.\n",
137 p->nSatCalls, p->nSatCallsUnsat, p->nSatCallsSat, p->nSatCallsUndec );
138 Abc_Print( 1, "SAT solver: Vars = %d. Clauses = %d. Recycles = %d. Sim rounds = %d.\n",
139 sat_solver_nvars(p->pSat), sat_solver_nclauses(p->pSat), p->nRecycles, p->nSimRounds );
140
141 p->timeOther = p->timeTotal - p->timeSimInit - p->timeSimSat - p->timeCnfGen - p->timeSatSat - p->timeSatUnsat - p->timeSatUndec;
142 ABC_PRTP( "Initialization ", p->timeSimInit, p->timeTotal );
143 ABC_PRTP( "SAT simulation ", p->timeSimSat, p->timeTotal );
144 ABC_PRTP( "CNF generation ", p->timeSimSat, p->timeTotal );
145 ABC_PRTP( "SAT solving ", p->timeSat-p->timeCnfGen, p->timeTotal );
146 ABC_PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
147 ABC_PRTP( " sat ", p->timeSatSat, p->timeTotal );
148 ABC_PRTP( " undecided ", p->timeSatUndec, p->timeTotal );
149 ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
150 ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
151 }
152
153 /**Function*************************************************************
154
155 Synopsis [Refine one class by resimulating one pattern.]
156
157 Description []
158
159 SideEffects []
160
161 SeeAlso []
162
163 ***********************************************************************/
Ssc_GiaSimulatePatternFraig_rec(Ssc_Man_t * p,int iFraigObj)164 int Ssc_GiaSimulatePatternFraig_rec( Ssc_Man_t * p, int iFraigObj )
165 {
166 Gia_Obj_t * pObj;
167 int Res0, Res1;
168 if ( Ssc_ObjSatVar(p, iFraigObj) )
169 return sat_solver_var_value( p->pSat, Ssc_ObjSatVar(p, iFraigObj) );
170 pObj = Gia_ManObj( p->pFraig, iFraigObj );
171 assert( Gia_ObjIsAnd(pObj) );
172 Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId0(pObj, iFraigObj) );
173 Res1 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId1(pObj, iFraigObj) );
174 pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj));
175 return pObj->fMark0;
176 }
Ssc_GiaSimulatePattern_rec(Ssc_Man_t * p,Gia_Obj_t * pObj)177 int Ssc_GiaSimulatePattern_rec( Ssc_Man_t * p, Gia_Obj_t * pObj )
178 {
179 int Res0, Res1;
180 if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) )
181 return pObj->fMark0;
182 Gia_ObjSetTravIdCurrent(p->pAig, pObj);
183 if ( ~pObj->Value ) // mapping into FRAIG exists - simulate FRAIG
184 {
185 Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Abc_Lit2Var(pObj->Value) );
186 pObj->fMark0 = Res0 ^ Abc_LitIsCompl(pObj->Value);
187 }
188 else // mapping into FRAIG does not exist - simulate AIG
189 {
190 Res0 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin0(pObj) );
191 Res1 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin1(pObj) );
192 pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj));
193 }
194 return pObj->fMark0;
195 }
Ssc_GiaResimulateOneClass(Ssc_Man_t * p,int iRepr,int iObj)196 int Ssc_GiaResimulateOneClass( Ssc_Man_t * p, int iRepr, int iObj )
197 {
198 int Ent, RetValue;
199 assert( iRepr == Gia_ObjRepr(p->pAig, iObj) );
200 assert( Gia_ObjIsHead( p->pAig, iRepr ) );
201 // set bit-values at the nodes according to the counter-example
202 Gia_ManIncrementTravId( p->pAig );
203 Gia_ClassForEachObj( p->pAig, iRepr, Ent )
204 Ssc_GiaSimulatePattern_rec( p, Gia_ManObj(p->pAig, Ent) );
205 // refine one class using these bit-values
206 RetValue = Ssc_GiaSimClassRefineOneBit( p->pAig, iRepr );
207 // check that the candidate equivalence is indeed refined
208 assert( iRepr != Gia_ObjRepr(p->pAig, iObj) );
209 return RetValue;
210 }
211
212 /**Function*************************************************************
213
214 Synopsis [Perform verification of conditional sweeping.]
215
216 Description []
217
218 SideEffects []
219
220 SeeAlso []
221
222 ***********************************************************************/
Ssc_PerformVerification(Gia_Man_t * p0,Gia_Man_t * p1,Gia_Man_t * pC)223 int Ssc_PerformVerification( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC )
224 {
225 int Status;
226 Cec_ParCec_t ParsCec, * pPars = &ParsCec;
227 // derive the OR of constraint outputs
228 Gia_Man_t * pCond = Gia_ManDupAndOr( pC, Gia_ManPoNum(p0), 1, 0 );
229 // derive F = F & !OR(c0, c1, c2, ...)
230 Gia_Man_t * p0c = Gia_ManMiter( p0, pCond, 0, 0, 0, 1, 0 );
231 // derive F = F & !OR(c0, c1, c2, ...)
232 Gia_Man_t * p1c = Gia_ManMiter( p1, pCond, 0, 0, 0, 1, 0 );
233 // derive dual-output miter
234 Gia_Man_t * pMiter = Gia_ManMiter( p0c, p1c, 0, 1, 0, 0, 0 );
235 Gia_ManStop( p0c );
236 Gia_ManStop( p1c );
237 Gia_ManStop( pCond );
238 // run equivalence checking
239 Cec_ManCecSetDefaultParams( pPars );
240 Status = Cec_ManVerify( pMiter, pPars );
241 Gia_ManStop( pMiter );
242 // report the results
243 if ( Status == 1 )
244 printf( "Verification succeeded.\n" );
245 else if ( Status == 0 )
246 printf( "Verification failed.\n" );
247 else if ( Status == -1 )
248 printf( "Verification undecided.\n" );
249 else assert( 0 );
250 return Status;
251 }
252
253 /**Function*************************************************************
254
255 Synopsis []
256
257 Description []
258
259 SideEffects []
260
261 SeeAlso []
262
263 ***********************************************************************/
Ssc_PerformSweepingInt(Gia_Man_t * pAig,Gia_Man_t * pCare,Ssc_Pars_t * pPars)264 Gia_Man_t * Ssc_PerformSweepingInt( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
265 {
266 Ssc_Man_t * p;
267 Gia_Man_t * pResult, * pTemp;
268 Gia_Obj_t * pObj, * pRepr;
269 abctime clk, clkTotal = Abc_Clock();
270 int i, fCompl, nRefined, status;
271 clk = Abc_Clock();
272 assert( Gia_ManRegNum(pCare) == 0 );
273 assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) );
274 assert( Gia_ManIsNormalized(pAig) );
275 assert( Gia_ManIsNormalized(pCare) );
276 // reset random numbers
277 Gia_ManRandom( 1 );
278 // sweeping manager
279 p = Ssc_ManStart( pAig, pCare, pPars );
280 if ( p == (Ssc_Man_t *)(ABC_PTRINT_T)1 ) // UNSAT
281 return Gia_ManDupZero( pAig );
282 if ( p == NULL ) // timeout
283 return Gia_ManDup( pAig );
284 if ( p->pPars->fVerbose )
285 printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 5), 640 );
286 // perform simulation
287 while ( 1 )
288 {
289 // simulate care set
290 Ssc_GiaRandomPiPattern( p->pFraig, 5, NULL );
291 Ssc_GiaSimRound( p->pFraig );
292 // transfer care patterns to user's AIG
293 if ( !Ssc_GiaTransferPiPattern( pAig, p->pFraig, p->vPivot ) )
294 break;
295 // simulate the main AIG
296 Ssc_GiaSimRound( pAig );
297 nRefined = Ssc_GiaClassesRefine( pAig );
298 if ( pPars->fVerbose )
299 Gia_ManEquivPrintClasses( pAig, 0, 0 );
300 if ( nRefined <= Gia_ManCandNum(pAig) / 100 )
301 break;
302 }
303 p->timeSimInit += Abc_Clock() - clk;
304
305 // prepare user's AIG
306 Gia_ManFillValue(pAig);
307 Gia_ManConst0(pAig)->Value = 0;
308 Gia_ManForEachCi( pAig, pObj, i )
309 pObj->Value = Gia_Obj2Lit( p->pFraig, Gia_ManCi(p->pFraig, i) );
310 // Gia_ManLevelNum(pAig);
311 // prepare swept AIG (should be done after starting SAT solver in Ssc_ManStart)
312 Gia_ManHashStart( p->pFraig );
313 // perform sweeping
314 Ssc_GiaResetPiPattern( pAig, pPars->nWords );
315 Ssc_GiaSavePiPattern( pAig, p->vPivot );
316 Gia_ManForEachCand( pAig, pObj, i )
317 {
318 if ( pAig->iPatsPi == 64 * pPars->nWords )
319 {
320 clk = Abc_Clock();
321 Ssc_GiaSimRound( pAig );
322 Ssc_GiaClassesRefine( pAig );
323 if ( pPars->fVerbose )
324 Gia_ManEquivPrintClasses( pAig, 0, 0 );
325 Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
326 Vec_IntClear( p->vDisPairs );
327 // prepare next patterns
328 Ssc_GiaResetPiPattern( pAig, pPars->nWords );
329 Ssc_GiaSavePiPattern( pAig, p->vPivot );
330 p->timeSimSat += Abc_Clock() - clk;
331 //printf( "\n" );
332 }
333 if ( Gia_ObjIsAnd(pObj) )
334 pObj->Value = Gia_ManHashAnd( p->pFraig, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
335 if ( !Gia_ObjHasRepr(pAig, i) )
336 continue;
337 pRepr = Gia_ObjReprObj(pAig, i);
338 if ( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase ) )
339 {
340 Gia_ObjSetProved( pAig, i );
341 continue;
342 }
343 assert( Abc_Lit2Var(pRepr->Value) != Abc_Lit2Var(pObj->Value) );
344 fCompl = pRepr->fPhase ^ pObj->fPhase ^ Abc_LitIsCompl(pRepr->Value) ^ Abc_LitIsCompl(pObj->Value);
345
346 // perform SAT call
347 clk = Abc_Clock();
348 p->nSatCalls++;
349 status = Ssc_ManCheckEquivalence( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl );
350 if ( status == l_False )
351 {
352 p->nSatCallsUnsat++;
353 pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
354 Gia_ObjSetProved( pAig, i );
355 }
356 else if ( status == l_True )
357 {
358 p->nSatCallsSat++;
359 Ssc_GiaSavePiPattern( pAig, p->vPattern );
360 Vec_IntPush( p->vDisPairs, Gia_ObjRepr(p->pAig, i) );
361 Vec_IntPush( p->vDisPairs, i );
362 // printf( "Try %2d and %2d: ", Gia_ObjRepr(p->pAig, i), i );
363 // Vec_IntPrint( p->vPattern );
364 if ( Gia_ObjRepr(p->pAig, i) > 0 )
365 Ssc_GiaResimulateOneClass( p, Gia_ObjRepr(p->pAig, i), i );
366 }
367 else if ( status == l_Undef )
368 p->nSatCallsUndec++;
369 else assert( 0 );
370 p->timeSat += Abc_Clock() - clk;
371 }
372 if ( pAig->iPatsPi > 1 )
373 {
374 clk = Abc_Clock();
375 while ( pAig->iPatsPi < 64 * pPars->nWords )
376 Ssc_GiaSavePiPattern( pAig, p->vPivot );
377 Ssc_GiaSimRound( pAig );
378 Ssc_GiaClassesRefine( pAig );
379 if ( pPars->fVerbose )
380 Gia_ManEquivPrintClasses( pAig, 0, 0 );
381 Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
382 Vec_IntClear( p->vDisPairs );
383 p->timeSimSat += Abc_Clock() - clk;
384 }
385 // Gia_ManEquivPrintClasses( pAig, 1, 0 );
386 // Gia_ManPrint( pAig );
387
388 // generate the resulting AIG
389 pResult = Gia_ManEquivReduce( pAig, 0, 0, 1, 0 );
390 if ( pResult == NULL )
391 {
392 printf( "There is no equivalences.\n" );
393 ABC_FREE( pAig->pReprs );
394 ABC_FREE( pAig->pNexts );
395 pResult = Gia_ManDup( pAig );
396 }
397 pResult = Gia_ManCleanup( pTemp = pResult );
398 Gia_ManStop( pTemp );
399 p->timeTotal = Abc_Clock() - clkTotal;
400 if ( pPars->fVerbose )
401 Ssc_ManPrintStats( p );
402 Ssc_ManStop( p );
403 // count the number of representatives
404 if ( pPars->fVerbose )
405 {
406 Abc_Print( 1, "Reduction in AIG nodes:%8d ->%8d (%6.2f %%). ",
407 Gia_ManAndNum(pAig), Gia_ManAndNum(pResult),
408 100.0 - 100.0 * Gia_ManAndNum(pResult) / Gia_ManAndNum(pAig) );
409 Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
410 }
411 return pResult;
412 }
Ssc_PerformSweeping(Gia_Man_t * pAig,Gia_Man_t * pCare,Ssc_Pars_t * pPars)413 Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
414 {
415 Gia_Man_t * pResult = Ssc_PerformSweepingInt( pAig, pCare, pPars );
416 if ( pPars->fVerify )
417 Ssc_PerformVerification( pAig, pResult, pCare );
418 return pResult;
419 }
Ssc_PerformSweepingConstr(Gia_Man_t * p,Ssc_Pars_t * pPars)420 Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
421 {
422 Gia_Man_t * pAig, * pCare, * pResult;
423 int i;
424 if ( pPars->fVerbose )
425 Abc_Print( 0, "SAT sweeping AIG with %d constraints.\n", p->nConstrs );
426 if ( p->nConstrs == 0 )
427 {
428 pAig = Gia_ManDup( p );
429 pCare = Gia_ManStart( Gia_ManCiNum(p) + 2 );
430 pCare->pName = Abc_UtilStrsav( "care" );
431 for ( i = 0; i < Gia_ManCiNum(p); i++ )
432 Gia_ManAppendCi( pCare );
433 Gia_ManAppendCo( pCare, 0 );
434 }
435 else
436 {
437 Vec_Int_t * vOuts = Vec_IntStartNatural( Gia_ManPoNum(p) );
438 pAig = Gia_ManDupCones( p, Vec_IntArray(vOuts), Gia_ManPoNum(p) - p->nConstrs, 0 );
439 pCare = Gia_ManDupCones( p, Vec_IntArray(vOuts) + Gia_ManPoNum(p) - p->nConstrs, p->nConstrs, 0 );
440 Vec_IntFree( vOuts );
441 }
442 if ( pPars->fVerbose )
443 {
444 printf( "User AIG: " );
445 Gia_ManPrintStats( pAig, NULL );
446 printf( "Care AIG: " );
447 Gia_ManPrintStats( pCare, NULL );
448 }
449
450 pAig = Gia_ManDupLevelized( pResult = pAig );
451 Gia_ManStop( pResult );
452 pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
453 if ( pPars->fAppend )
454 {
455 Gia_ManDupAppendShare( pResult, pCare );
456 pResult->nConstrs = Gia_ManPoNum(pCare);
457 }
458 Gia_ManStop( pAig );
459 Gia_ManStop( pCare );
460 return pResult;
461 }
462
463 ////////////////////////////////////////////////////////////////////////
464 /// END OF FILE ///
465 ////////////////////////////////////////////////////////////////////////
466
467
468 ABC_NAMESPACE_IMPL_END
469
470