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