| /**CFile**************************************************************** |
| |
| FileName [sscCore.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [SAT sweeping under constraints.] |
| |
| Synopsis [The core procedures.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 29, 2008.] |
| |
| Revision [$Id: sscCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "sscInt.h" |
| #include "proof/cec/cec.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [This procedure sets default parameters.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ssc_ManSetDefaultParams( Ssc_Pars_t * p ) |
| { |
| memset( p, 0, sizeof(Ssc_Pars_t) ); |
| p->nWords = 1; // the number of simulation words |
| p->nBTLimit = 1000; // conflict limit at a node |
| p->nSatVarMax = 5000; // the max number of SAT variables |
| p->nCallsRecycle = 100; // calls to perform before recycling SAT solver |
| p->fVerbose = 0; // verbose stats |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ssc_ManStop( Ssc_Man_t * p ) |
| { |
| Vec_IntFreeP( &p->vFront ); |
| Vec_IntFreeP( &p->vFanins ); |
| Vec_IntFreeP( &p->vPattern ); |
| Vec_IntFreeP( &p->vDisPairs ); |
| Vec_IntFreeP( &p->vPivot ); |
| Vec_IntFreeP( &p->vId2Var ); |
| Vec_IntFreeP( &p->vVar2Id ); |
| if ( p->pSat ) sat_solver_delete( p->pSat ); |
| Gia_ManStopP( &p->pFraig ); |
| ABC_FREE( p ); |
| } |
| Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars ) |
| { |
| Ssc_Man_t * p; |
| p = ABC_CALLOC( Ssc_Man_t, 1 ); |
| p->pPars = pPars; |
| p->pAig = pAig; |
| p->pCare = pCare; |
| p->pFraig = Gia_ManDupDfs( p->pCare ); |
| assert( Vec_IntSize(&p->pFraig->vHTable) == 0 ); |
| assert( !Gia_ManHasDangling(p->pFraig) ); |
| Gia_ManInvertPos( p->pFraig ); |
| Ssc_ManStartSolver( p ); |
| if ( p->pSat == NULL ) |
| { |
| printf( "Constraints are UNSAT after propagation.\n" ); |
| Ssc_ManStop( p ); |
| return (Ssc_Man_t *)(ABC_PTRINT_T)1; |
| } |
| // p->vPivot = Ssc_GiaFindPivotSim( p->pFraig ); |
| // Vec_IntFreeP( &p->vPivot ); |
| p->vPivot = Ssc_ManFindPivotSat( p ); |
| if ( p->vPivot == (Vec_Int_t *)(ABC_PTRINT_T)1 ) |
| { |
| printf( "Constraints are UNSAT.\n" ); |
| Ssc_ManStop( p ); |
| return (Ssc_Man_t *)(ABC_PTRINT_T)1; |
| } |
| if ( p->vPivot == NULL ) |
| { |
| printf( "Conflict limit is reached while trying to find one SAT assignment.\n" ); |
| Ssc_ManStop( p ); |
| return NULL; |
| } |
| sat_solver_bookmark( p->pSat ); |
| // Vec_IntPrint( p->vPivot ); |
| Gia_ManSetPhasePattern( p->pAig, p->vPivot ); |
| Gia_ManSetPhasePattern( p->pCare, p->vPivot ); |
| if ( Gia_ManCheckCoPhase(p->pCare) ) |
| { |
| printf( "Computed reference pattern violates %d constraints (this is a bug!).\n", Gia_ManCheckCoPhase(p->pCare) ); |
| Ssc_ManStop( p ); |
| return NULL; |
| } |
| // other things |
| p->vDisPairs = Vec_IntAlloc( 100 ); |
| p->vPattern = Vec_IntAlloc( 100 ); |
| p->vFanins = Vec_IntAlloc( 100 ); |
| p->vFront = Vec_IntAlloc( 100 ); |
| Ssc_GiaClassesInit( pAig ); |
| // now it is ready for refinement using simulation |
| return p; |
| } |
| void Ssc_ManPrintStats( Ssc_Man_t * p ) |
| { |
| Abc_Print( 1, "Parameters: SimWords = %d. SatConfs = %d. SatVarMax = %d. CallsRec = %d. Verbose = %d.\n", |
| p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax, p->pPars->nCallsRecycle, p->pPars->fVerbose ); |
| Abc_Print( 1, "SAT calls : Total = %d. Proof = %d. Cex = %d. Undec = %d.\n", |
| p->nSatCalls, p->nSatCallsUnsat, p->nSatCallsSat, p->nSatCallsUndec ); |
| Abc_Print( 1, "SAT solver: Vars = %d. Clauses = %d. Recycles = %d. Sim rounds = %d.\n", |
| sat_solver_nvars(p->pSat), sat_solver_nclauses(p->pSat), p->nRecycles, p->nSimRounds ); |
| |
| p->timeOther = p->timeTotal - p->timeSimInit - p->timeSimSat - p->timeCnfGen - p->timeSatSat - p->timeSatUnsat - p->timeSatUndec; |
| ABC_PRTP( "Initialization ", p->timeSimInit, p->timeTotal ); |
| ABC_PRTP( "SAT simulation ", p->timeSimSat, p->timeTotal ); |
| ABC_PRTP( "CNF generation ", p->timeSimSat, p->timeTotal ); |
| ABC_PRTP( "SAT solving ", p->timeSat-p->timeCnfGen, p->timeTotal ); |
| ABC_PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); |
| ABC_PRTP( " sat ", p->timeSatSat, p->timeTotal ); |
| ABC_PRTP( " undecided ", p->timeSatUndec, p->timeTotal ); |
| ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); |
| ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Refine one class by resimulating one pattern.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ssc_GiaSimulatePatternFraig_rec( Ssc_Man_t * p, int iFraigObj ) |
| { |
| Gia_Obj_t * pObj; |
| int Res0, Res1; |
| if ( Ssc_ObjSatVar(p, iFraigObj) ) |
| return sat_solver_var_value( p->pSat, Ssc_ObjSatVar(p, iFraigObj) ); |
| pObj = Gia_ManObj( p->pFraig, iFraigObj ); |
| assert( Gia_ObjIsAnd(pObj) ); |
| Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId0(pObj, iFraigObj) ); |
| Res1 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId1(pObj, iFraigObj) ); |
| pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj)); |
| return pObj->fMark0; |
| } |
| int Ssc_GiaSimulatePattern_rec( Ssc_Man_t * p, Gia_Obj_t * pObj ) |
| { |
| int Res0, Res1; |
| if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) ) |
| return pObj->fMark0; |
| Gia_ObjSetTravIdCurrent(p->pAig, pObj); |
| if ( ~pObj->Value ) // mapping into FRAIG exists - simulate FRAIG |
| { |
| Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Abc_Lit2Var(pObj->Value) ); |
| pObj->fMark0 = Res0 ^ Abc_LitIsCompl(pObj->Value); |
| } |
| else // mapping into FRAIG does not exist - simulate AIG |
| { |
| Res0 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin0(pObj) ); |
| Res1 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin1(pObj) ); |
| pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj)); |
| } |
| return pObj->fMark0; |
| } |
| int Ssc_GiaResimulateOneClass( Ssc_Man_t * p, int iRepr, int iObj ) |
| { |
| int Ent, RetValue; |
| assert( iRepr == Gia_ObjRepr(p->pAig, iObj) ); |
| assert( Gia_ObjIsHead( p->pAig, iRepr ) ); |
| // set bit-values at the nodes according to the counter-example |
| Gia_ManIncrementTravId( p->pAig ); |
| Gia_ClassForEachObj( p->pAig, iRepr, Ent ) |
| Ssc_GiaSimulatePattern_rec( p, Gia_ManObj(p->pAig, Ent) ); |
| // refine one class using these bit-values |
| RetValue = Ssc_GiaSimClassRefineOneBit( p->pAig, iRepr ); |
| // check that the candidate equivalence is indeed refined |
| assert( iRepr != Gia_ObjRepr(p->pAig, iObj) ); |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Perform verification of conditional sweeping.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ssc_PerformVerification( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC ) |
| { |
| int Status; |
| Cec_ParCec_t ParsCec, * pPars = &ParsCec; |
| // derive the OR of constraint outputs |
| Gia_Man_t * pCond = Gia_ManDupAndOr( pC, Gia_ManPoNum(p0), 1, 0 ); |
| // derive F = F & !OR(c0, c1, c2, ...) |
| Gia_Man_t * p0c = Gia_ManMiter( p0, pCond, 0, 0, 0, 1, 0 ); |
| // derive F = F & !OR(c0, c1, c2, ...) |
| Gia_Man_t * p1c = Gia_ManMiter( p1, pCond, 0, 0, 0, 1, 0 ); |
| // derive dual-output miter |
| Gia_Man_t * pMiter = Gia_ManMiter( p0c, p1c, 0, 1, 0, 0, 0 ); |
| Gia_ManStop( p0c ); |
| Gia_ManStop( p1c ); |
| Gia_ManStop( pCond ); |
| // run equivalence checking |
| Cec_ManCecSetDefaultParams( pPars ); |
| Status = Cec_ManVerify( pMiter, pPars ); |
| Gia_ManStop( pMiter ); |
| // report the results |
| if ( Status == 1 ) |
| printf( "Verification succeeded.\n" ); |
| else if ( Status == 0 ) |
| printf( "Verification failed.\n" ); |
| else if ( Status == -1 ) |
| printf( "Verification undecided.\n" ); |
| else assert( 0 ); |
| return Status; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Ssc_PerformSweepingInt( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars ) |
| { |
| Ssc_Man_t * p; |
| Gia_Man_t * pResult, * pTemp; |
| Gia_Obj_t * pObj, * pRepr; |
| abctime clk, clkTotal = Abc_Clock(); |
| int i, fCompl, nRefined, status; |
| clk = Abc_Clock(); |
| assert( Gia_ManRegNum(pCare) == 0 ); |
| assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) ); |
| assert( Gia_ManIsNormalized(pAig) ); |
| assert( Gia_ManIsNormalized(pCare) ); |
| // reset random numbers |
| Gia_ManRandom( 1 ); |
| // sweeping manager |
| p = Ssc_ManStart( pAig, pCare, pPars ); |
| if ( p == (Ssc_Man_t *)(ABC_PTRINT_T)1 ) // UNSAT |
| return Gia_ManDupZero( pAig ); |
| if ( p == NULL ) // timeout |
| return Gia_ManDup( pAig ); |
| if ( p->pPars->fVerbose ) |
| printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 5), 640 ); |
| // perform simulation |
| while ( 1 ) |
| { |
| // simulate care set |
| Ssc_GiaRandomPiPattern( p->pFraig, 5, NULL ); |
| Ssc_GiaSimRound( p->pFraig ); |
| // transfer care patterns to user's AIG |
| if ( !Ssc_GiaTransferPiPattern( pAig, p->pFraig, p->vPivot ) ) |
| break; |
| // simulate the main AIG |
| Ssc_GiaSimRound( pAig ); |
| nRefined = Ssc_GiaClassesRefine( pAig ); |
| if ( pPars->fVerbose ) |
| Gia_ManEquivPrintClasses( pAig, 0, 0 ); |
| if ( nRefined <= Gia_ManCandNum(pAig) / 100 ) |
| break; |
| } |
| p->timeSimInit += Abc_Clock() - clk; |
| |
| // prepare user's AIG |
| Gia_ManFillValue(pAig); |
| Gia_ManConst0(pAig)->Value = 0; |
| Gia_ManForEachCi( pAig, pObj, i ) |
| pObj->Value = Gia_Obj2Lit( p->pFraig, Gia_ManCi(p->pFraig, i) ); |
| // Gia_ManLevelNum(pAig); |
| // prepare swept AIG (should be done after starting SAT solver in Ssc_ManStart) |
| Gia_ManHashStart( p->pFraig ); |
| // perform sweeping |
| Ssc_GiaResetPiPattern( pAig, pPars->nWords ); |
| Ssc_GiaSavePiPattern( pAig, p->vPivot ); |
| Gia_ManForEachCand( pAig, pObj, i ) |
| { |
| if ( pAig->iPatsPi == 64 * pPars->nWords ) |
| { |
| clk = Abc_Clock(); |
| Ssc_GiaSimRound( pAig ); |
| Ssc_GiaClassesRefine( pAig ); |
| if ( pPars->fVerbose ) |
| Gia_ManEquivPrintClasses( pAig, 0, 0 ); |
| Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs ); |
| Vec_IntClear( p->vDisPairs ); |
| // prepare next patterns |
| Ssc_GiaResetPiPattern( pAig, pPars->nWords ); |
| Ssc_GiaSavePiPattern( pAig, p->vPivot ); |
| p->timeSimSat += Abc_Clock() - clk; |
| //printf( "\n" ); |
| } |
| if ( Gia_ObjIsAnd(pObj) ) |
| pObj->Value = Gia_ManHashAnd( p->pFraig, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| if ( !Gia_ObjHasRepr(pAig, i) ) |
| continue; |
| pRepr = Gia_ObjReprObj(pAig, i); |
| if ( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase ) ) |
| { |
| Gia_ObjSetProved( pAig, i ); |
| continue; |
| } |
| assert( Abc_Lit2Var(pRepr->Value) != Abc_Lit2Var(pObj->Value) ); |
| fCompl = pRepr->fPhase ^ pObj->fPhase ^ Abc_LitIsCompl(pRepr->Value) ^ Abc_LitIsCompl(pObj->Value); |
| |
| // perform SAT call |
| clk = Abc_Clock(); |
| p->nSatCalls++; |
| status = Ssc_ManCheckEquivalence( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl ); |
| if ( status == l_False ) |
| { |
| p->nSatCallsUnsat++; |
| pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase ); |
| Gia_ObjSetProved( pAig, i ); |
| } |
| else if ( status == l_True ) |
| { |
| p->nSatCallsSat++; |
| Ssc_GiaSavePiPattern( pAig, p->vPattern ); |
| Vec_IntPush( p->vDisPairs, Gia_ObjRepr(p->pAig, i) ); |
| Vec_IntPush( p->vDisPairs, i ); |
| // printf( "Try %2d and %2d: ", Gia_ObjRepr(p->pAig, i), i ); |
| // Vec_IntPrint( p->vPattern ); |
| if ( Gia_ObjRepr(p->pAig, i) > 0 ) |
| Ssc_GiaResimulateOneClass( p, Gia_ObjRepr(p->pAig, i), i ); |
| } |
| else if ( status == l_Undef ) |
| p->nSatCallsUndec++; |
| else assert( 0 ); |
| p->timeSat += Abc_Clock() - clk; |
| } |
| if ( pAig->iPatsPi > 1 ) |
| { |
| clk = Abc_Clock(); |
| while ( pAig->iPatsPi < 64 * pPars->nWords ) |
| Ssc_GiaSavePiPattern( pAig, p->vPivot ); |
| Ssc_GiaSimRound( pAig ); |
| Ssc_GiaClassesRefine( pAig ); |
| if ( pPars->fVerbose ) |
| Gia_ManEquivPrintClasses( pAig, 0, 0 ); |
| Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs ); |
| Vec_IntClear( p->vDisPairs ); |
| p->timeSimSat += Abc_Clock() - clk; |
| } |
| // Gia_ManEquivPrintClasses( pAig, 1, 0 ); |
| // Gia_ManPrint( pAig ); |
| |
| // generate the resulting AIG |
| pResult = Gia_ManEquivReduce( pAig, 0, 0, 1, 0 ); |
| if ( pResult == NULL ) |
| { |
| printf( "There is no equivalences.\n" ); |
| ABC_FREE( pAig->pReprs ); |
| ABC_FREE( pAig->pNexts ); |
| pResult = Gia_ManDup( pAig ); |
| } |
| pResult = Gia_ManCleanup( pTemp = pResult ); |
| Gia_ManStop( pTemp ); |
| p->timeTotal = Abc_Clock() - clkTotal; |
| if ( pPars->fVerbose ) |
| Ssc_ManPrintStats( p ); |
| Ssc_ManStop( p ); |
| // count the number of representatives |
| if ( pPars->fVerbose ) |
| { |
| Abc_Print( 1, "Reduction in AIG nodes:%8d ->%8d (%6.2f %%). ", |
| Gia_ManAndNum(pAig), Gia_ManAndNum(pResult), |
| 100.0 - 100.0 * Gia_ManAndNum(pResult) / Gia_ManAndNum(pAig) ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); |
| } |
| return pResult; |
| } |
| Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars ) |
| { |
| Gia_Man_t * pResult = Ssc_PerformSweepingInt( pAig, pCare, pPars ); |
| if ( pPars->fVerify ) |
| Ssc_PerformVerification( pAig, pResult, pCare ); |
| return pResult; |
| } |
| Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars ) |
| { |
| Gia_Man_t * pAig, * pCare, * pResult; |
| int i; |
| if ( pPars->fVerbose ) |
| Abc_Print( 0, "SAT sweeping AIG with %d constraints.\n", p->nConstrs ); |
| if ( p->nConstrs == 0 ) |
| { |
| pAig = Gia_ManDup( p ); |
| pCare = Gia_ManStart( Gia_ManCiNum(p) + 2 ); |
| pCare->pName = Abc_UtilStrsav( "care" ); |
| for ( i = 0; i < Gia_ManCiNum(p); i++ ) |
| Gia_ManAppendCi( pCare ); |
| Gia_ManAppendCo( pCare, 0 ); |
| } |
| else |
| { |
| Vec_Int_t * vOuts = Vec_IntStartNatural( Gia_ManPoNum(p) ); |
| pAig = Gia_ManDupCones( p, Vec_IntArray(vOuts), Gia_ManPoNum(p) - p->nConstrs, 0 ); |
| pCare = Gia_ManDupCones( p, Vec_IntArray(vOuts) + Gia_ManPoNum(p) - p->nConstrs, p->nConstrs, 0 ); |
| Vec_IntFree( vOuts ); |
| } |
| if ( pPars->fVerbose ) |
| { |
| printf( "User AIG: " ); |
| Gia_ManPrintStats( pAig, NULL ); |
| printf( "Care AIG: " ); |
| Gia_ManPrintStats( pCare, NULL ); |
| } |
| |
| pAig = Gia_ManDupLevelized( pResult = pAig ); |
| Gia_ManStop( pResult ); |
| pResult = Ssc_PerformSweeping( pAig, pCare, pPars ); |
| if ( pPars->fAppend ) |
| { |
| Gia_ManDupAppendShare( pResult, pCare ); |
| pResult->nConstrs = Gia_ManPoNum(pCare); |
| } |
| Gia_ManStop( pAig ); |
| Gia_ManStop( pCare ); |
| return pResult; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
