| /**CFile**************************************************************** |
| |
| FileName [saigGlaPba.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Sequential AIG package.] |
| |
| Synopsis [Gate level abstraction.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: saigGlaPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "saig.h" |
| #include "sat/bsat/satSolver.h" |
| #include "sat/bsat/satStore.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| typedef struct Aig_Gla2Man_t_ Aig_Gla2Man_t; |
| struct Aig_Gla2Man_t_ |
| { |
| // user data |
| Aig_Man_t * pAig; |
| int nStart; |
| int nFramesMax; |
| int fVerbose; |
| // unrolling |
| Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID |
| Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID) |
| Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID |
| // clause mapping |
| Vec_Int_t * vCla2Obj; // maps clause into its root object |
| Vec_Int_t * vCla2Fra; // maps clause into its frame |
| Vec_Int_t * vVec2Use; // maps vec ID into its used frames (nFrames per vec ID) |
| // SAT solver |
| sat_solver * pSat; |
| // statistics |
| clock_t timePre; |
| clock_t timeSat; |
| clock_t timeTotal; |
| }; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Adds constant to the solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Aig_Gla2AddConst( sat_solver * pSat, int iVar, int fCompl ) |
| { |
| lit Lit = toLitCond( iVar, fCompl ); |
| if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) ) |
| return 0; |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Adds buffer to the solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Aig_Gla2AddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) |
| { |
| lit Lits[2]; |
| |
| Lits[0] = toLitCond( iVar0, 0 ); |
| Lits[1] = toLitCond( iVar1, !fCompl ); |
| if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) |
| return 0; |
| |
| Lits[0] = toLitCond( iVar0, 1 ); |
| Lits[1] = toLitCond( iVar1, fCompl ); |
| if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) |
| return 0; |
| |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Adds buffer to the solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Aig_Gla2AddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ) |
| { |
| lit Lits[3]; |
| |
| Lits[0] = toLitCond( iVar, 1 ); |
| Lits[1] = toLitCond( iVar0, fCompl0 ); |
| if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) |
| return 0; |
| |
| Lits[0] = toLitCond( iVar, 1 ); |
| Lits[1] = toLitCond( iVar1, fCompl1 ); |
| if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) |
| return 0; |
| |
| Lits[0] = toLitCond( iVar, 0 ); |
| Lits[1] = toLitCond( iVar0, !fCompl0 ); |
| Lits[2] = toLitCond( iVar1, !fCompl1 ); |
| if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) ) |
| return 0; |
| |
| return 1; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Finds existing SAT variable or creates a new one.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Aig_Gla2FetchVar( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int k ) |
| { |
| int i, iVecId, iSatVar; |
| assert( k < p->nFramesMax ); |
| iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) ); |
| if ( iVecId == 0 ) |
| { |
| iVecId = Vec_IntSize( p->vVec2Var ) / p->nFramesMax; |
| for ( i = 0; i < p->nFramesMax; i++ ) |
| Vec_IntPush( p->vVec2Var, 0 ); |
| Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId ); |
| } |
| iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFramesMax + k ); |
| if ( iSatVar == 0 ) |
| { |
| iSatVar = Vec_IntSize( p->vVar2Inf ) / 2; |
| Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) ); |
| Vec_IntPush( p->vVar2Inf, k ); |
| Vec_IntWriteEntry( p->vVec2Var, iVecId * p->nFramesMax + k, iSatVar ); |
| } |
| return iSatVar; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Assigns variables to the AIG nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Aig_Gla2AssignVars_rec( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int f ) |
| { |
| int nVars = Vec_IntSize(p->vVar2Inf); |
| Aig_Gla2FetchVar( p, pObj, f ); |
| if ( nVars == Vec_IntSize(p->vVar2Inf) ) |
| return; |
| if ( Aig_ObjIsConst1(pObj) ) |
| return; |
| if ( Saig_ObjIsPo( p->pAig, pObj ) ) |
| { |
| Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f ); |
| return; |
| } |
| if ( Aig_ObjIsCi( pObj ) ) |
| { |
| if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 ) |
| Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 ); |
| return; |
| } |
| assert( Aig_ObjIsNode(pObj) ); |
| Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f ); |
| Aig_Gla2AssignVars_rec( p, Aig_ObjFanin1(pObj), f ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates SAT solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p ) |
| { |
| Vec_Int_t * vPoLits; |
| Aig_Obj_t * pObj; |
| int i, f, ObjId, nVars, RetValue = 1; |
| |
| // assign variables |
| for ( f = p->nFramesMax - 1; f >= 0; f-- ) |
| // for ( f = 0; f < p->nFramesMax; f++ ) |
| Aig_Gla2AssignVars_rec( p, Aig_ManCo(p->pAig, 0), f ); |
| |
| // create SAT solver |
| p->pSat = sat_solver_new(); |
| sat_solver_store_alloc( p->pSat ); |
| sat_solver_setnvars( p->pSat, Vec_IntSize(p->vVar2Inf)/2 ); |
| |
| // add clauses |
| nVars = Vec_IntSize( p->vVar2Inf ); |
| Vec_IntForEachEntryDouble( p->vVar2Inf, ObjId, f, i ) |
| { |
| if ( ObjId == -1 ) |
| continue; |
| pObj = Aig_ManObj( p->pAig, ObjId ); |
| if ( Aig_ObjIsNode(pObj) ) |
| { |
| RetValue &= Aig_Gla2AddNode( p->pSat, Aig_Gla2FetchVar(p, pObj, f), |
| Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f), |
| Aig_Gla2FetchVar(p, Aig_ObjFanin1(pObj), f), |
| Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) ); |
| Vec_IntPush( p->vCla2Obj, ObjId ); |
| Vec_IntPush( p->vCla2Obj, ObjId ); |
| Vec_IntPush( p->vCla2Obj, ObjId ); |
| |
| Vec_IntPush( p->vCla2Fra, f ); |
| Vec_IntPush( p->vCla2Fra, f ); |
| Vec_IntPush( p->vCla2Fra, f ); |
| } |
| else if ( Saig_ObjIsLo(p->pAig, pObj) ) |
| { |
| if ( f == 0 ) |
| { |
| RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 1 ); |
| Vec_IntPush( p->vCla2Obj, ObjId ); |
| |
| Vec_IntPush( p->vCla2Fra, f ); |
| } |
| else |
| { |
| Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj); |
| RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f), |
| Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObjLi), f-1), |
| Aig_ObjFaninC0(pObjLi) ); |
| Vec_IntPush( p->vCla2Obj, ObjId ); |
| Vec_IntPush( p->vCla2Obj, ObjId ); |
| |
| Vec_IntPush( p->vCla2Fra, f ); |
| Vec_IntPush( p->vCla2Fra, f ); |
| } |
| } |
| else if ( Saig_ObjIsPo(p->pAig, pObj) ) |
| { |
| RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f), |
| Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f), |
| Aig_ObjFaninC0(pObj) ); |
| Vec_IntPush( p->vCla2Obj, ObjId ); |
| Vec_IntPush( p->vCla2Obj, ObjId ); |
| |
| Vec_IntPush( p->vCla2Fra, f ); |
| Vec_IntPush( p->vCla2Fra, f ); |
| } |
| else if ( Aig_ObjIsConst1(pObj) ) |
| { |
| RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 0 ); |
| Vec_IntPush( p->vCla2Obj, ObjId ); |
| |
| Vec_IntPush( p->vCla2Fra, f ); |
| } |
| else assert( Saig_ObjIsPi(p->pAig, pObj) ); |
| } |
| |
| // add output clause |
| vPoLits = Vec_IntAlloc( p->nFramesMax ); |
| for ( f = p->nStart; f < p->nFramesMax; f++ ) |
| Vec_IntPush( vPoLits, 2 * Aig_Gla2FetchVar(p, Aig_ManCo(p->pAig, 0), f) ); |
| RetValue &= sat_solver_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ); |
| Vec_IntFree( vPoLits ); |
| Vec_IntPush( p->vCla2Obj, 0 ); |
| Vec_IntPush( p->vCla2Fra, 0 ); |
| assert( Vec_IntSize(p->vCla2Fra) == Vec_IntSize(p->vCla2Obj) ); |
| |
| assert( nVars == Vec_IntSize(p->vVar2Inf) ); |
| assert( ((Sto_Man_t *)p->pSat->pStore)->nClauses == Vec_IntSize(p->vCla2Obj) ); |
| // Sto_ManDumpClauses( ((Sto_Man_t *)p->pSat->pStore), "temp_sto.cnf" ); |
| sat_solver_store_mark_roots( p->pSat ); |
| |
| if ( p->fVerbose ) |
| printf( "The resulting SAT problem contains %d variables and %d clauses.\n", |
| p->pSat->size, p->pSat->stats.clauses ); |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nStart, int nFramesMax, int fVerbose ) |
| { |
| Aig_Gla2Man_t * p; |
| int i; |
| |
| p = ABC_CALLOC( Aig_Gla2Man_t, 1 ); |
| p->pAig = pAig; |
| |
| p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) ); |
| p->vVec2Var = Vec_IntAlloc( 1 << 20 ); |
| p->vVar2Inf = Vec_IntAlloc( 1 << 20 ); |
| p->vCla2Obj = Vec_IntAlloc( 1 << 20 ); |
| p->vCla2Fra = Vec_IntAlloc( 1 << 20 ); |
| |
| // skip first vector ID |
| p->nStart = nStart; |
| p->nFramesMax = nFramesMax; |
| p->fVerbose = fVerbose; |
| for ( i = 0; i < p->nFramesMax; i++ ) |
| Vec_IntPush( p->vVec2Var, -1 ); |
| |
| // skip first SAT variable |
| Vec_IntPush( p->vVar2Inf, -1 ); |
| Vec_IntPush( p->vVar2Inf, -1 ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Aig_Gla2ManStop( Aig_Gla2Man_t * p ) |
| { |
| Vec_IntFreeP( &p->vObj2Vec ); |
| Vec_IntFreeP( &p->vVec2Var ); |
| Vec_IntFreeP( &p->vVar2Inf ); |
| Vec_IntFreeP( &p->vCla2Obj ); |
| Vec_IntFreeP( &p->vCla2Fra ); |
| Vec_IntFreeP( &p->vVec2Use ); |
| |
| if ( p->pSat ) |
| sat_solver_delete( p->pSat ); |
| ABC_FREE( p ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Finds the set of clauses involved in the UNSAT core.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose, int * piRetValue ) |
| { |
| Vec_Int_t * vCore; |
| void * pSatCnf; |
| Intp_Man_t * pManProof; |
| int RetValue; |
| clock_t clk = clock(); |
| if ( piRetValue ) |
| *piRetValue = -1; |
| // solve the problem |
| RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); |
| if ( RetValue == l_Undef ) |
| { |
| printf( "Conflict limit is reached.\n" ); |
| return NULL; |
| } |
| if ( RetValue == l_True ) |
| { |
| printf( "The BMC problem is SAT.\n" ); |
| if ( piRetValue ) |
| *piRetValue = 0; |
| return NULL; |
| } |
| if ( fVerbose ) |
| { |
| printf( "SAT solver returned UNSAT after %7d conflicts. ", (int)pSat->stats.conflicts ); |
| Abc_PrintTime( 1, "Time", clock() - clk ); |
| } |
| assert( RetValue == l_False ); |
| pSatCnf = sat_solver_store_release( pSat ); |
| // derive the UNSAT core |
| clk = clock(); |
| pManProof = Intp_ManAlloc(); |
| vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0, 0 ); |
| Intp_ManFree( pManProof ); |
| if ( fVerbose ) |
| { |
| printf( "SAT core contains %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver_nclauses(pSat) ); |
| Abc_PrintTime( 1, "Time", clock() - clk ); |
| } |
| Sto_ManFree( (Sto_Man_t *)pSatCnf ); |
| return vCore; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects abstracted objects.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore ) |
| { |
| Vec_Int_t * vResult; |
| Aig_Obj_t * pObj; |
| int i, ClaId, iVecId; |
| // p->vVec2Use = Vec_IntStart( Vec_IntSize(p->vVec2Var) ); |
| |
| vResult = Vec_IntStart( Aig_ManObjNumMax(p->pAig) ); |
| Vec_IntWriteEntry( vResult, 0, 1 ); // add const1 |
| Vec_IntForEachEntry( vCore, ClaId, i ) |
| { |
| pObj = Aig_ManObj( p->pAig, Vec_IntEntry(p->vCla2Obj, ClaId) ); |
| if ( Saig_ObjIsPi(p->pAig, pObj) || Saig_ObjIsPo(p->pAig, pObj) || Aig_ObjIsConst1(pObj) ) |
| continue; |
| assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) ); |
| Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 ); |
| /* |
| // add flop inputs with multiple fanouts |
| if ( Saig_ObjIsLo(p->pAig, pObj) ) |
| { |
| Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj); |
| if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObjLi)) ) |
| // if ( Aig_ObjRefs( Aig_ObjFanin0(pObjLi) ) > 1 ) |
| Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObjLi), 1 ); |
| } |
| else |
| { |
| if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObj)) ) |
| Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObj), 1 ); |
| if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin1(pObj)) ) |
| Vec_IntWriteEntry( vResult, Aig_ObjFaninId1(pObj), 1 ); |
| } |
| */ |
| if ( p->vVec2Use ) |
| { |
| iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) ); |
| Vec_IntWriteEntry( p->vVec2Use, iVecId * p->nFramesMax + Vec_IntEntry(p->vCla2Fra, ClaId), 1 ); |
| } |
| } |
| // printf( "Number of entries %d\n", Vec_IntCountPositive(vResult) ); |
| |
| // count the number of objects in each frame |
| if ( p->vVec2Use ) |
| { |
| Vec_Int_t * vCounts = Vec_IntStart( p->nFramesMax ); |
| int v, f, Entry, nVecIds = Vec_IntSize(p->vVec2Use) / p->nFramesMax; |
| for ( f = 0; f < p->nFramesMax; f++ ) |
| for ( v = 0; v < nVecIds; v++ ) |
| if ( Vec_IntEntry( p->vVec2Use, v * p->nFramesMax + f ) ) |
| Vec_IntAddToEntry( vCounts, f, 1 ); |
| Vec_IntForEachEntry( vCounts, Entry, f ) |
| printf( "%d ", Entry ); |
| printf( "\n" ); |
| Vec_IntFree( vCounts ); |
| } |
| return vResult; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs gate-level localization abstraction.] |
| |
| Description [Returns array of objects included in the abstraction. This array |
| may contain only const1, flop outputs, and internal nodes, that is, objects |
| that should have clauses added to the SAT solver.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose ) |
| { |
| Aig_Gla2Man_t * p; |
| Vec_Int_t * vCore, * vResult; |
| clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0; |
| clock_t clk, clk2 = clock(); |
| assert( Saig_ManPoNum(pAig) == 1 ); |
| |
| if ( fVerbose ) |
| { |
| if ( TimeLimit ) |
| printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit ); |
| else |
| printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax ); |
| } |
| |
| // start the solver |
| clk = clock(); |
| p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose ); |
| if ( !Aig_Gla2CreateSatSolver( p ) ) |
| { |
| printf( "Error! SAT solver became UNSAT.\n" ); |
| Aig_Gla2ManStop( p ); |
| return NULL; |
| } |
| sat_solver_set_random( p->pSat, fSkipRand ); |
| p->timePre += clock() - clk; |
| |
| // set runtime limit |
| if ( TimeLimit ) |
| sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); |
| |
| // compute UNSAT core |
| clk = clock(); |
| vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL ); |
| if ( vCore == NULL ) |
| { |
| Aig_Gla2ManStop( p ); |
| return NULL; |
| } |
| p->timeSat += clock() - clk; |
| p->timeTotal += clock() - clk2; |
| |
| // print stats |
| if ( fVerbose ) |
| { |
| ABC_PRTP( "Pre ", p->timePre, p->timeTotal ); |
| ABC_PRTP( "Sat ", p->timeSat, p->timeTotal ); |
| ABC_PRTP( "Total ", p->timeTotal, p->timeTotal ); |
| } |
| |
| // prepare return value |
| vResult = Aig_Gla2ManCollect( p, vCore ); |
| Vec_IntFree( vCore ); |
| Aig_Gla2ManStop( p ); |
| return vResult; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
