diff options
Diffstat (limited to 'src/aig/saig/saigPba.c')
| -rw-r--r-- | src/aig/saig/saigPba.c | 752 |
1 files changed, 0 insertions, 752 deletions
diff --git a/src/aig/saig/saigPba.c b/src/aig/saig/saigPba.c deleted file mode 100644 index 65b39fc0..00000000 --- a/src/aig/saig/saigPba.c +++ /dev/null @@ -1,752 +0,0 @@ -/**CFile**************************************************************** - - FileName [saigPba.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Sequential AIG package.] - - Synopsis [Proof-based abstraction.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: saigPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "saig.h" - -#include "cnf.h" -#include "satSolver.h" -#include "satStore.h" -#include "ssw.h" -#include "ioa.h" -#include "fra.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static inline char Saig_AbsVisited( Vec_Str_t * p, int nObjs, Aig_Obj_t * pObj, int i ) { return Vec_StrGetEntry( p, nObjs*i+pObj->Id ); } -static inline void Saig_AbsSetVisited( Vec_Str_t * p, int nObjs, Aig_Obj_t * pObj, int i ) { Vec_StrSetEntry( p, nObjs*i+pObj->Id, (char)1 ); } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**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, clk = clock(); - *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" ); - *piRetValue = 0; - return NULL; - } - if ( fVerbose ) - { - printf( "SAT solver returned UNSAT after %d conflicts. ", pSat->stats.conflicts ); - ABC_PRT( "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 ); - Intp_ManFree( pManProof ); - Sto_ManFree( (Sto_Man_t *)pSatCnf ); - if ( fVerbose ) - { - printf( "SAT core contains %d clauses (out of %d). ", Vec_IntSize(vCore), pSat->stats.clauses ); - ABC_PRT( "Time", clock() - clk ); - } - return vCore; -} - - -/**Function************************************************************* - - Synopsis [Mark visited nodes recursively.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_AbsMarkVisited_rec( Aig_Man_t * p, Vec_Str_t * vObj2Visit, Aig_Obj_t * pObj, int i ) -{ - if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, i ) ) - return 1; - Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, i ); - if ( Saig_ObjIsPi( p, pObj ) ) - return 1; - if ( Saig_ObjIsLo( p, pObj ) ) - { - if ( i == 0 ) - return 1; - return Saig_AbsMarkVisited_rec( p, vObj2Visit, Saig_ObjLoToLi(p, pObj), i-1 ); - } - if ( Aig_ObjIsPo( pObj ) ) - return Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i ); - Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i ); - Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin1(pObj), i ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Mark visited nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Str_t * Saig_AbsMarkVisited( Aig_Man_t * p, int nFramesMax ) -{ - Vec_Str_t * vObj2Visit; - Aig_Obj_t * pObj; - int i, f; - vObj2Visit = Vec_StrStart( Aig_ManObjNumMax(p) * nFramesMax ); -// Saig_ManForEachLo( p, pObj, i ) -// Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, 0 ); - for ( f = 0; f < nFramesMax; f++ ) - { - Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), Aig_ManConst1(p), f ); - Saig_ManForEachPo( p, pObj, i ) - Saig_AbsMarkVisited_rec( p, vObj2Visit, pObj, f ); - } - return vObj2Visit; -} - -/**Function************************************************************* - - Synopsis [Performs the actual construction of the output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Obj_t * Saig_AbsCreateFrames_rec( Aig_Man_t * pFrame, Aig_Obj_t * pObj ) -{ - if ( pObj->pData ) - return (Aig_Obj_t *)pObj->pData; - assert( Aig_ObjIsNode(pObj) ); - Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) ); - Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin1(pObj) ); - return (Aig_Obj_t *)(pObj->pData = Aig_And( pFrame, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) )); -} - -/**Function************************************************************* - - Synopsis [Derives a vector of AIG managers, one for each frame.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Saig_AbsCreateFrames( Aig_Man_t * p, int nFramesMax, int fVerbose ) -{ - Vec_Ptr_t * vFrames, * vLoObjs, * vLiObjs; - Vec_Str_t * vObj2Visit; - Aig_Man_t * pFrame; - Aig_Obj_t * pObj; - int f, i; - vObj2Visit = Saig_AbsMarkVisited( p, nFramesMax ); - vFrames = Vec_PtrAlloc( nFramesMax ); - vLoObjs = Vec_PtrAlloc( 100 ); - vLiObjs = Vec_PtrAlloc( 100 ); - for ( f = 0; f < nFramesMax; f++ ) - { - Aig_ManCleanData( p ); - pFrame = Aig_ManStart( 1000 ); - Aig_ManConst1(p)->pData = Aig_ManConst1(pFrame); - // create PIs - Vec_PtrClear( vLoObjs ); - Vec_PtrClear( vLiObjs ); - Aig_ManForEachPi( p, pObj, i ) - { - if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) ) - { - pObj->pData = Aig_ObjCreatePi(pFrame); - if ( i >= Saig_ManPiNum(p) ) - Vec_PtrPush( vLoObjs, pObj ); - } - } - // remember the number of (implicit) registers in this frame - pFrame->nAsserts = Vec_PtrSize(vLoObjs); - // create POs - Aig_ManForEachPo( p, pObj, i ) - { - if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) ) - { - Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) ); - pObj->pData = Aig_ObjCreatePo( pFrame, Aig_ObjChild0Copy(pObj) ); - if ( i >= Saig_ManPoNum(p) ) - Vec_PtrPush( vLiObjs, pObj ); - } - } -// Vec_PtrPush( vFrames, Cnf_Derive(pFrame, Aig_ManPoNum(pFrame)) ); - Vec_PtrPush( vFrames, Cnf_DeriveSimple(pFrame, Aig_ManPoNum(pFrame)) ); - // set the new PIs to point to the corresponding registers - Aig_ManCleanData( pFrame ); - Vec_PtrForEachEntry( Aig_Obj_t *, vLoObjs, pObj, i ) - ((Aig_Obj_t *)pObj->pData)->pData = pObj; - Vec_PtrForEachEntry( Aig_Obj_t *, vLiObjs, pObj, i ) - ((Aig_Obj_t *)pObj->pData)->pData = pObj; - if ( fVerbose ) - printf( "%3d : PI =%8d. PO =%8d. Flop =%8d. Node =%8d.\n", - f, Aig_ManPiNum(pFrame), Aig_ManPoNum(pFrame), pFrame->nAsserts, Aig_ManNodeNum(pFrame) ); - } - Vec_PtrFree( vLoObjs ); - Vec_PtrFree( vLiObjs ); - Vec_StrFree( vObj2Visit ); - return vFrames; -} - -/**Function************************************************************* - - Synopsis [Derives a vector of AIG managers, one for each frame.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -sat_solver * Saig_AbsCreateSolverDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames ) -{ - sat_solver * pSat; - Cnf_Dat_t * pCnf, * pCnfPrev; - Vec_Int_t * vPoLits; - Aig_Obj_t * pObjPo, * pObjLi, * pObjLo; - int f, i, Lit, Lits[2], iVarOld, iVarNew, nSatVars, nRegisters; - // start array of output literals - vPoLits = Vec_IntAlloc( 100 ); - // count the number of CNF variables - nSatVars = 0; - Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f ) - nSatVars += pCnf->nVars; - - // create the SAT solver - pSat = sat_solver_new(); - sat_solver_store_alloc( pSat ); - sat_solver_setnvars( pSat, nSatVars ); - - // add clauses for the timeframes - nSatVars = 0; -// Vec_PtrForEachEntryReverse( Cnf_Dat_t *, vFrames, pCnf, f ) - Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f ) - { - // lift clauses of this CNF - Cnf_DataLift( pCnf, nSatVars ); - nSatVars += pCnf->nVars; - // copy clauses into the manager - for ( i = 0; i < pCnf->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) - { - printf( "The BMC problem is trivially UNSAT.\n" ); - sat_solver_delete( pSat ); - Vec_IntFree( vPoLits ); - return NULL; - } - } - // remember output literal - Aig_ManForEachPo( pCnf->pMan, pObjPo, i ) - { - if ( i == Saig_ManPoNum(p) ) - break; - Vec_IntPush( vPoLits, toLit(pCnf->pVarNums[pObjPo->Id]) ); - } - } - - // add auxiliary clauses (output, connectors, initial) - // add output clause - if ( !sat_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) ) - { - printf( "SAT solver is not created correctly.\n" ); - assert( 0 ); - } - Vec_IntFree( vPoLits ); - - // add connecting clauses - pCnfPrev = (Cnf_Dat_t *)Vec_PtrEntry( vFrames, 0 ); - Vec_PtrForEachEntryStart( Cnf_Dat_t *, vFrames, pCnf, f, 1 ) - { - nRegisters = pCnf->pMan->nAsserts; - assert( nRegisters <= Aig_ManPoNum(pCnfPrev->pMan) ); - assert( nRegisters <= Aig_ManPiNum(pCnf->pMan) ); - for ( i = 0; i < nRegisters; i++ ) - { - pObjLi = Aig_ManPo( pCnfPrev->pMan, Aig_ManPoNum(pCnfPrev->pMan) - nRegisters + i ); - pObjLo = Aig_ManPi( pCnf->pMan, Aig_ManPiNum(pCnf->pMan) - nRegisters + i ); - // get variable numbers - iVarOld = pCnfPrev->pVarNums[pObjLi->Id]; - iVarNew = pCnf->pVarNums[pObjLo->Id]; - // add clauses connecting existing variables - Lits[0] = toLitCond( iVarOld, 0 ); - Lits[1] = toLitCond( iVarNew, 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - Lits[0] = toLitCond( iVarOld, 1 ); - Lits[1] = toLitCond( iVarNew, 0 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - } - pCnfPrev = pCnf; - } - // add unit clauses - pCnf = (Cnf_Dat_t *)Vec_PtrEntry( vFrames, 0 ); - nRegisters = pCnf->pMan->nAsserts; - for ( i = 0; i < nRegisters; i++ ) - { - pObjLo = Aig_ManPi( pCnf->pMan, Aig_ManPiNum(pCnf->pMan) - nRegisters + i ); - assert( pCnf->pVarNums[pObjLo->Id] >= 0 ); - Lit = toLitCond( pCnf->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) - assert( 0 ); - } - sat_solver_store_mark_roots( pSat ); - return pSat; -} - - -/**Function************************************************************* - - Synopsis [Creates SAT solver for BMC.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -sat_solver * Saig_AbsCreateSolver( Cnf_Dat_t * pCnf, int nFrames ) -{ - sat_solver * pSat; - Vec_Int_t * vPoLits; - Aig_Obj_t * pObjPo, * pObjLi, * pObjLo; - int f, i, Lit, Lits[2], iVarOld, iVarNew; - // start array of output literals - vPoLits = Vec_IntAlloc( nFrames * Saig_ManPoNum(pCnf->pMan) ); - // create the SAT solver - pSat = sat_solver_new(); - sat_solver_store_alloc( pSat ); - sat_solver_setnvars( pSat, pCnf->nVars * nFrames ); - - // add clauses for the timeframes - for ( f = 0; f < nFrames; f++ ) - { - for ( i = 0; i < pCnf->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) - { - printf( "The BMC problem is trivially UNSAT.\n" ); - sat_solver_delete( pSat ); - Vec_IntFree( vPoLits ); - return NULL; - } - } - // remember output literal - Saig_ManForEachPo( pCnf->pMan, pObjPo, i ) - Vec_IntPush( vPoLits, toLit(pCnf->pVarNums[pObjPo->Id]) ); - // lift CNF to the next frame - Cnf_DataLift( pCnf, pCnf->nVars ); - } - // put CNF back to the original level - Cnf_DataLift( pCnf, - pCnf->nVars * nFrames ); - - // add auxiliary clauses (output, connectors, initial) - // add output clause - if ( !sat_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) ) - assert( 0 ); - Vec_IntFree( vPoLits ); - // add connecting clauses - for ( f = 0; f < nFrames; f++ ) - { - // connect to the previous timeframe - if ( f > 0 ) - { - Saig_ManForEachLiLo( pCnf->pMan, pObjLi, pObjLo, i ) - { - iVarOld = pCnf->pVarNums[pObjLi->Id] - pCnf->nVars; - iVarNew = pCnf->pVarNums[pObjLo->Id]; - // add clauses connecting existing variables - Lits[0] = toLitCond( iVarOld, 0 ); - Lits[1] = toLitCond( iVarNew, 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - Lits[0] = toLitCond( iVarOld, 1 ); - Lits[1] = toLitCond( iVarNew, 0 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - } - } - // lift CNF to the next frame - Cnf_DataLift( pCnf, pCnf->nVars ); - } - // put CNF back to the original level - Cnf_DataLift( pCnf, - pCnf->nVars * nFrames ); - // add unit clauses - Saig_ManForEachLo( pCnf->pMan, pObjLo, i ) - { - assert( pCnf->pVarNums[pObjLo->Id] >= 0 ); - Lit = toLitCond( pCnf->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) - assert( 0 ); - } - sat_solver_store_mark_roots( pSat ); - return pSat; -} - -/**Function************************************************************* - - Synopsis [Performs proof-based abstraction using BMC of the given depth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_AbsCollectRegistersDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames, Vec_Int_t * vCore ) -{ - Aig_Obj_t * pObj; - Cnf_Dat_t * pCnf; - Vec_Int_t * vFlops; - int * pVars, * pFlops; - int i, f, iClause, iReg, * piLit, nSatVars, nSatClauses; - // count the number of CNF variables - nSatVars = 0; - Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f ) - nSatVars += pCnf->nVars; - // mark register variables - pVars = ABC_ALLOC( int, nSatVars ); - for ( i = 0; i < nSatVars; i++ ) - pVars[i] = -1; - Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f ) - { - Aig_ManForEachPi( pCnf->pMan, pObj, i ) - { - assert( pCnf->pVarNums[pObj->Id] >= 0 ); - assert( pCnf->pVarNums[pObj->Id] < nSatVars ); - if ( pObj->pData == NULL ) - continue; - iReg = Aig_ObjPioNum((Aig_Obj_t *)pObj->pData) - Saig_ManPiNum(p); - assert( iReg >= 0 && iReg < Aig_ManRegNum(p) ); - pVars[ pCnf->pVarNums[pObj->Id] ] = iReg; - } - Aig_ManForEachPo( pCnf->pMan, pObj, i ) - { - assert( pCnf->pVarNums[pObj->Id] >= 0 ); - assert( pCnf->pVarNums[pObj->Id] < nSatVars ); - if ( pObj->pData == NULL ) - continue; - iReg = Aig_ObjPioNum((Aig_Obj_t *)pObj->pData) - Saig_ManPoNum(p); - assert( iReg >= 0 && iReg < Aig_ManRegNum(p) ); - pVars[ pCnf->pVarNums[pObj->Id] ] = iReg; - } - } - // mark used registers - pFlops = ABC_CALLOC( int, Aig_ManRegNum(p) ); - Vec_IntForEachEntry( vCore, iClause, i ) - { - nSatClauses = 0; - Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f ) - { - if ( iClause < nSatClauses + pCnf->nClauses ) - break; - nSatClauses += pCnf->nClauses; - } - if ( f == Vec_PtrSize(vFrames) ) - continue; - iClause = iClause - nSatClauses; - assert( iClause >= 0 ); - assert( iClause < pCnf->nClauses ); - // consider the clause - for ( piLit = pCnf->pClauses[iClause]; piLit < pCnf->pClauses[iClause+1]; piLit++ ) - { - iReg = pVars[ lit_var(*piLit) ]; - if ( iReg >= 0 ) - pFlops[iReg] = 1; - } - } - // collect registers - vFlops = Vec_IntAlloc( Aig_ManRegNum(p) ); - for ( i = 0; i < Aig_ManRegNum(p); i++ ) - if ( pFlops[i] ) - Vec_IntPush( vFlops, i ); - ABC_FREE( pFlops ); - ABC_FREE( pVars ); - return vFlops; -} - -/**Function************************************************************* - - Synopsis [Performs proof-based abstraction using BMC of the given depth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * vCore ) -{ - Aig_Obj_t * pObj; - Vec_Int_t * vFlops; - int * pVars, * pFlops; - int i, iClause, iReg, * piLit; - // mark register variables - pVars = ABC_ALLOC( int, pCnf->nVars ); - for ( i = 0; i < pCnf->nVars; i++ ) - pVars[i] = -1; - Saig_ManForEachLi( pCnf->pMan, pObj, i ) - pVars[ pCnf->pVarNums[pObj->Id] ] = i; - Saig_ManForEachLo( pCnf->pMan, pObj, i ) - pVars[ pCnf->pVarNums[pObj->Id] ] = i; - // mark used registers - pFlops = ABC_CALLOC( int, Aig_ManRegNum(pCnf->pMan) ); - Vec_IntForEachEntry( vCore, iClause, i ) - { - // skip auxiliary clauses - if ( iClause >= pCnf->nClauses * nFrames ) - continue; - // consider the clause - iClause = iClause % pCnf->nClauses; - for ( piLit = pCnf->pClauses[iClause]; piLit < pCnf->pClauses[iClause+1]; piLit++ ) - { - iReg = pVars[ lit_var(*piLit) ]; - if ( iReg >= 0 ) - pFlops[iReg] = 1; - } - } - // collect registers - vFlops = Vec_IntAlloc( Aig_ManRegNum(pCnf->pMan) ); - for ( i = 0; i < Aig_ManRegNum(pCnf->pMan); i++ ) - if ( pFlops[i] ) - Vec_IntPush( vFlops, i ); - ABC_FREE( pFlops ); - ABC_FREE( pVars ); - return vFlops; -} - -/**Function************************************************************* - - Synopsis [Performs proof-based abstraction using BMC of the given depth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_AbsFreeCnfs( Vec_Ptr_t * vFrames ) -{ - Cnf_Dat_t * pCnf; - int i; - Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, i ) - { - Aig_ManStop( pCnf->pMan ); - Cnf_DataFree( pCnf ); - } - Vec_PtrFree( vFrames ); -} - -/**Function************************************************************* - - Synopsis [Performs proof-based abstraction using BMC of the given depth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_AbsExtendOneStep( Aig_Man_t * p, Vec_Int_t * vFlops ) -{ - Vec_Ptr_t * vFlopPtrs, * vSupp; - Aig_Obj_t * pObj; - int i, Entry; - // collect latch inputs - vFlopPtrs = Vec_PtrAlloc( 1000 ); - Vec_IntForEachEntry( vFlops, Entry, i ) - { - Vec_PtrPush( vFlopPtrs, Saig_ManLi(p, Entry) ); - pObj = Saig_ManLo(p, Entry); - pObj->fMarkA = 1; - } - // collect latch outputs - vSupp = Vec_PtrAlloc( 1000 ); - Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vFlopPtrs), Vec_PtrSize(vFlopPtrs), vSupp ); - Vec_PtrFree( vFlopPtrs ); - // mark influencing flops - Vec_PtrForEachEntry( Aig_Obj_t *, vSupp, pObj, i ) - pObj->fMarkA = 1; - Vec_PtrFree( vSupp ); - // reload flops - Vec_IntClear( vFlops ); - Aig_ManForEachPi( p, pObj, i ) - { - if ( pObj->fMarkA == 0 ) - continue; - pObj->fMarkA = 0; - if ( Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) >= 0 ) - Vec_IntPush( vFlops, Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) ); - } -} - - -/**Function************************************************************* - - Synopsis [Performs proof-based abstraction using BMC of the given depth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManProofAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ) -{ - Vec_Int_t * vFlops; - sat_solver * pSat; - Vec_Ptr_t * vFrames = NULL; - Vec_Int_t * vCore; - Cnf_Dat_t * pCnf = NULL; - int clk = clock(), clk2 = clock(); - if ( pPars->fVerbose ) - printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", pPars->nFramesMax, pPars->nConfMax ); - assert( Aig_ManRegNum(p) > 0 ); - Aig_ManSetPioNumbers( p ); - if ( pPars->fDynamic ) - { - // create CNF for the frames - vFrames = Saig_AbsCreateFrames( p, pPars->nFramesMax, pPars->fVerbose ); - // create dynamic solver - pSat = Saig_AbsCreateSolverDyn( p, vFrames ); - } - else - { - // create CNF for the AIG - pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) ); - // create SAT solver for the unrolled AIG - pSat = Saig_AbsCreateSolver( pCnf, pPars->nFramesMax ); - } - if ( pPars->fVerbose ) - { - printf( "SAT solver: Vars = %7d. Clauses = %7d. ", pSat->size, pSat->stats.clauses ); - ABC_PRT( "Time", clock() - clk2 ); - } - // compute UNSAT core - vCore = Saig_AbsSolverUnsatCore( pSat, pPars->nConfMax, pPars->fVerbose, &pPars->Status ); - sat_solver_delete( pSat ); - if ( vCore == NULL ) - { - if ( vFrames ) - Saig_AbsFreeCnfs( vFrames ); - return NULL; - } - pPars->nFramesDone = pPars->nFramesMax; - // collect registers - if ( pPars->fDynamic ) - { - vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore ); - Saig_AbsFreeCnfs( vFrames ); - } - else - { - vFlops = Saig_AbsCollectRegisters( pCnf, pPars->nFramesMax, vCore ); - Cnf_DataFree( pCnf ); - } - Vec_IntFree( vCore ); - if ( pPars->fVerbose ) - { - printf( "The number of relevant registers is %d (out of %d). ", Vec_IntSize(vFlops), Aig_ManRegNum(p) ); - ABC_PRT( "Time", clock() - clk ); - } - return vFlops; -} - -/**Function************************************************************* - - Synopsis [Performs proof-based abstraction using BMC of the given depth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ) -{ - Vec_Int_t * vFlops; - Aig_Man_t * pAbs = NULL; - vFlops = Saig_ManProofAbstractionFlops( p, pPars ); - // write the final result - if ( vFlops ) - { - pAbs = Saig_ManDeriveAbstraction( p, vFlops ); - Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 ); - printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" ); - Vec_IntFree( vFlops ); - } - return pAbs; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |