diff options
Diffstat (limited to 'src/aig/saig/saigAbs.c')
| -rw-r--r-- | src/aig/saig/saigAbs.c | 910 |
1 files changed, 155 insertions, 755 deletions
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index 2fac60f5..194add25 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -6,7 +6,7 @@ PackageName [Sequential AIG package.] - Synopsis [Proof-based abstraction.] + Synopsis [Counter-example-based abstraction.] Author [Alan Mishchenko] @@ -19,110 +19,24 @@ ***********************************************************************/ #include "saig.h" - -#include "cnf.h" -#include "satSolver.h" -#include "satStore.h" #include "ssw.h" -#include "ioa.h" #include "fra.h" +#include "bbr.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 ) -{ - Vec_Int_t * vCore; - void * pSatCnf; - Intp_Man_t * pManProof; - int RetValue, clk = clock(); - // 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" ); - 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 = Intp_ManUnsatCore( pManProof, pSatCnf, 0 ); - Intp_ManFree( pManProof ); - Sto_ManFree( 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.] + Synopsis [Collects internal nodes in the DFS order.] Description [] @@ -131,47 +45,29 @@ int Saig_AbsMarkVisited_rec( Aig_Man_t * p, Vec_Str_t * vObj2Visit, Aig_Obj_t * SeeAlso [] ***********************************************************************/ -Vec_Str_t * Saig_AbsMarkVisited( Aig_Man_t * p, int nFramesMax ) +int Saig_ManFindFirstFlop_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) { - 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++ ) + int RetValue; + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return -1; + Aig_ObjSetTravIdCurrent(p, pObj); + if ( Saig_ObjIsPi(p, pObj) ) + return -1; + if ( Saig_ObjIsLo(p, pObj) ) { - Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), Aig_ManConst1(p), f ); - Saig_ManForEachPo( p, pObj, i ) - Saig_AbsMarkVisited_rec( p, vObj2Visit, pObj, f ); + assert( Aig_ObjPioNum(pObj) >= Saig_ManPiNum(p) ); + return Aig_ObjPioNum(pObj)-Saig_ManPiNum(p); } - 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 pObj->pData; assert( Aig_ObjIsNode(pObj) ); - Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) ); - Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin1(pObj) ); - return pObj->pData = Aig_And( pFrame, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + RetValue = Saig_ManFindFirstFlop_rec( p, Aig_ObjFanin0(pObj) ); + if ( RetValue >= 0 ) + return RetValue; + return Saig_ManFindFirstFlop_rec( p, Aig_ObjFanin1(pObj) ); } /**Function************************************************************* - Synopsis [Derives a vector of AIG managers, one for each frame.] + Synopsis [Returns the index of the flop that appears in the support.] Description [] @@ -180,462 +76,12 @@ Aig_Obj_t * Saig_AbsCreateFrames_rec( Aig_Man_t * pFrame, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Saig_AbsCreateFrames( Aig_Man_t * p, int nFramesMax, int fVerbose ) +int Saig_ManFindFirstFlop( Aig_Man_t * p ) { - 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( vLoObjs, pObj, i ) - ((Aig_Obj_t *)pObj->pData)->pData = pObj; - Vec_PtrForEachEntry( 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************************************************************* + Aig_ManIncrementTravId( p ); + Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); + return Saig_ManFindFirstFlop_rec( p, Aig_ObjFanin0(Aig_ManPo(p, 0)) ); - 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( 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( vFrames, pCnf, f ) - Vec_PtrForEachEntry( 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 = Vec_PtrEntry( vFrames, 0 ); - Vec_PtrForEachEntryStart( 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 = 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( 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( 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(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(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( 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( 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( 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************************************************************* @@ -649,11 +95,15 @@ void Saig_AbsExtendOneStep( Aig_Man_t * p, Vec_Int_t * vFlops ) SeeAlso [] ***********************************************************************/ -Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCexAbs ) +Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs ) { - Ssw_Cex_t * pCex; + Abc_Cex_t * pCex; Aig_Obj_t * pObj; int i, f; + if ( !Ssw_SmlRunCounterExample( pAbs, pCexAbs ) ) + printf( "Saig_ManCexRemap(): The intial counter-example is invalid.\n" ); + else + printf( "Saig_ManCexRemap(): The intial counter-example is correct.\n" ); // start the counter-example pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 ); pCex->iFrame = pCexAbs->iFrame; @@ -672,7 +122,7 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex // verify the counter example if ( !Ssw_SmlRunCounterExample( p, pCex ) ) { - printf( "Saig_ManCexShrink(): Counter-example is invalid.\n" ); + printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" ); Ssw_SmlFreeCounterExample( pCex ); pCex = NULL; } @@ -695,7 +145,7 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex SeeAlso [] ***********************************************************************/ -int Saig_ManFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs ) +int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs ) { Aig_Obj_t * pObj; int i; @@ -710,7 +160,7 @@ int Saig_ManFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs ) /**Function************************************************************* - Synopsis [Performs proof-based abstraction using BMC of the given depth.] + Synopsis [Refines abstraction using one step.] Description [] @@ -719,15 +169,12 @@ int Saig_ManFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int * pnUseStart, int fVerbose ) +Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames ) { - extern void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite ); - extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose ); - extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent ); - - Vec_Int_t * vFlopsNew;//, * vPiToReg; -// Aig_Obj_t * pObj; - int i, Entry;//, iFlop; + extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames ); + Vec_Int_t * vFlopsNew; + int i, Entry; + *piRetValue = -1; if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 ) { Fra_Sec_t SecPar, * pSecPar = &SecPar; @@ -738,66 +185,92 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF } else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) ) { - int nBddMax = 1000000; - int nIterMax = nFrames; - int fPartition = 1; - int fReorder = 1; - int fReorderImage = 1; - Aig_ManVerifyUsingBdds( pAbs, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, 0 ); + Saig_ParBbr_t Pars, * pPars = &Pars; + Bbr_ManSetDefaultParams( pPars ); + pPars->TimeLimit = 0; + pPars->nBddMax = 1000000; + pPars->nIterMax = nFrames; + pPars->fPartition = 1; + pPars->fReorder = 1; + pPars->fReorderImage = 1; + pPars->fVerbose = fVerbose; + pPars->fSilent = 0; + Aig_ManVerifyUsingBdds( pAbs, pPars ); } else - Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 20, nConfMaxOne, 1000000, fVerbose, 0 ); + { + Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames ); + } if ( pAbs->pSeqModel == NULL ) return NULL; if ( pnUseStart ) - *pnUseStart = ((Fra_Cex_t *)pAbs->pSeqModel)->iFrame; -// vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose ); - vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose ); + *pnUseStart = pAbs->pSeqModel->iFrame; + vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose ); + if ( vFlopsNew == NULL ) + return NULL; if ( Vec_IntSize(vFlopsNew) == 0 ) { printf( "Discovered a true counter-example!\n" ); - p->pSeqModel = Saig_ManCexShrink( p, pAbs, pAbs->pSeqModel ); + p->pSeqModel = Saig_ManCexRemap( p, pAbs, pAbs->pSeqModel ); Vec_IntFree( vFlopsNew ); + *piRetValue = 0; return NULL; } + // vFlopsNew contains PI numbers that should be kept in pAbs if ( fVerbose ) printf( "Adding %d registers to the abstraction.\n", Vec_IntSize(vFlopsNew) ); - // vFlopsNew contains PI number that should be kept in pAbs -/* - // for each additional PI, collect the number of a register it stands for - Vec_IntForEachEntry( vFlops, Entry, i ) - { - pObj = Saig_ManLo( p, Entry ); - pObj->fMarkA = 1; - } - vPiToReg = Vec_IntAlloc( 1000 ); - Aig_ManForEachPi( p, pObj, i ) - { - if ( pObj->fMarkA ) - { - pObj->fMarkA = 0; - continue; - } - if ( i < Saig_ManPiNum(p) ) - Vec_IntPush( vPiToReg, -1 ); - else - Vec_IntPush( vPiToReg, Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) ); - } - // collect registers + // add to the abstraction Vec_IntForEachEntry( vFlopsNew, Entry, i ) { - iFlop = Vec_IntEntry( vPiToReg, Entry ); - assert( iFlop >= 0 ); - assert( iFlop < Aig_ManRegNum(p) ); - Vec_IntPush( vFlops, iFlop ); + Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry); + assert( Entry >= Saig_ManPiNum(p) ); + assert( Entry < Aig_ManPiNum(p) ); + Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) ); } - Vec_IntFree( vPiToReg ); Vec_IntFree( vFlopsNew ); Vec_IntSort( vFlops, 0 ); Vec_IntForEachEntryStart( vFlops, Entry, i, 1 ) assert( Vec_IntEntry(vFlops, i-1) != Entry ); -*/ + + return Saig_ManDeriveAbstraction( p, vFlops ); +} + +/**Function************************************************************* + + Synopsis [Refines abstraction using one step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fVerbose ) +{ + Aig_Man_t * pAbs; + Vec_Int_t * vFlopsNew; + int i, Entry; + pAbs = Saig_ManDeriveAbstraction( p, vFlops ); + vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose ); + if ( vFlopsNew == NULL ) + { + Aig_ManStop( pAbs ); + return 0; + } + if ( Vec_IntSize(vFlopsNew) == 0 ) + { + printf( "Refinement did not happen. Discovered a true counter-example.\n" ); + printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManPiNum(pAbs), Aig_ManPiNum(p) ); + p->pSeqModel = Saig_ManCexRemap( p, pAbs, pCex ); + Vec_IntFree( vFlopsNew ); + Aig_ManStop( pAbs ); + return 0; + } + if ( fVerbose ) + printf( "Adding %d registers to the abstraction.\n", Vec_IntSize(vFlopsNew) ); + // vFlopsNew contains PI number that should be kept in pAbs // add to the abstraction Vec_IntForEachEntry( vFlopsNew, Entry, i ) { @@ -807,17 +280,13 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) ); } Vec_IntFree( vFlopsNew ); - - Vec_IntSort( vFlops, 0 ); - Vec_IntForEachEntryStart( vFlops, Entry, i, 1 ) - assert( Vec_IntEntry(vFlops, i-1) != Entry ); - - return Saig_ManAbstraction( p, vFlops ); + Aig_ManStop( pAbs ); + return 1; } /**Function************************************************************* - Synopsis [Performs proof-based abstraction using BMC of the given depth.] + Synopsis [Computes the flops to remain after abstraction.] Description [] @@ -826,138 +295,67 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManProofAbstraction_int( Aig_Man_t * p, Gia_ParAbs_t * pPars ) +Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ) { - Aig_Man_t * pResult, * pTemp; - Cnf_Dat_t * pCnf; - Vec_Ptr_t * vFrames; - sat_solver * pSat; - Vec_Int_t * vCore; + int nUseStart = 0; + Aig_Man_t * pAbs, * pTemp; Vec_Int_t * vFlops; - int Iter, clk = clock(), clk2 = clock(); + int Iter, clk = clock(), clk2 = clock();//, iFlop; assert( Aig_ManRegNum(p) > 0 ); + if ( pPars->fVerbose ) + printf( "Performing counter-example-based refinement.\n" ); Aig_ManSetPioNumbers( p ); - - if ( pPars->fSkipProof ) - { -// assert( 0 ); - if ( pPars->fVerbose ) - printf( "Performing counter-example-based refinement.\n" ); -// vFlops = Vec_IntStartNatural( 100 ); -// Vec_IntPush( vFlops, 0 ); - vFlops = Vec_IntStartNatural( 1 ); - } - else - { - if ( pPars->fVerbose ) - printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", pPars->nFramesMax, pPars->nConfMax ); - 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 ); - sat_solver_delete( pSat ); - if ( vCore == NULL ) - { - Saig_AbsFreeCnfs( vFrames ); - return NULL; - } - // 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 ); - } - } + vFlops = Vec_IntStartNatural( 1 ); /* - // extend the abstraction - if ( fExtend ) - { - if ( fVerbose ) - printf( "Support extended from %d flops to", Vec_IntSize(vFlops) ); - Saig_AbsExtendOneStep( p, vFlops ); - if ( fVerbose ) - printf( " %d flops.\n", Vec_IntSize(vFlops) ); - } + iFlop = Saig_ManFindFirstFlop( p ); + assert( iFlop >= 0 ); + vFlops = Vec_IntAlloc( 1 ); + Vec_IntPush( vFlops, iFlop ); */ // create the resulting AIG - pResult = Saig_ManAbstraction( p, vFlops ); - - if ( pPars->fExtend ) + pAbs = Saig_ManDeriveAbstraction( p, vFlops ); + if ( !pPars->fVerbose ) { - int nUseStart = 0; - if ( !pPars->fVerbose ) + printf( "Init : " ); + Aig_ManPrintStats( pAbs ); + } + printf( "Refining abstraction...\n" ); + for ( Iter = 0; ; Iter++ ) + { + pTemp = Saig_ManCexRefine( p, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone ); + if ( pTemp == NULL ) { - printf( "Init : " ); - Aig_ManPrintStats( pResult ); + ABC_FREE( p->pSeqModel ); + p->pSeqModel = pAbs->pSeqModel; + pAbs->pSeqModel = NULL; + Aig_ManStop( pAbs ); + break; } - printf( "Refining abstraction...\n" ); - for ( Iter = 0; ; Iter++ ) - { - pTemp = Saig_ManProofRefine( p, pResult, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fUseStart?&nUseStart:NULL, pPars->fVerbose ); - if ( pTemp == NULL ) - break; - Aig_ManStop( pResult ); - pResult = pTemp; - printf( "ITER %4d : ", Iter ); - if ( !pPars->fVerbose ) - Aig_ManPrintStats( pResult ); -// else -// printf( " -----------------------------------------------------\n" ); - // output the intermediate result of abstraction - Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 ); + Aig_ManStop( pAbs ); + pAbs = pTemp; + printf( "ITER %4d : ", Iter ); + if ( !pPars->fVerbose ) + Aig_ManPrintStats( pAbs ); + // output the intermediate result of abstraction + Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 ); // printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" ); - // check if the ratio is reached - if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*pPars->nRatio ) - { - printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio ); - Aig_ManStop( pResult ); - pResult = NULL; - break; - } + // check if the ratio is reached + if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(p) < 1.0*pPars->nRatio ) + { + printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio ); + Aig_ManStop( pAbs ); + pAbs = NULL; + Vec_IntFree( vFlops ); + vFlops = NULL; + break; } } - // write the final result - if ( pResult ) - Aig_ManStop( pResult ); - else - { - Vec_IntFree( vFlops ); - vFlops = NULL; - } return vFlops; } /**Function************************************************************* - Synopsis [Performs proof-based abstraction using BMC of the given depth.] + Synopsis [Performs counter-example-based abstraction.] Description [] @@ -966,15 +364,15 @@ Vec_Int_t * Saig_ManProofAbstraction_int( Aig_Man_t * p, Gia_ParAbs_t * pPars ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ) +Aig_Man_t * Saig_ManCexAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ) { Vec_Int_t * vFlops; Aig_Man_t * pAbs = NULL; - vFlops = Saig_ManProofAbstraction_int( p, pPars ); + vFlops = Saig_ManCexAbstractionFlops( p, pPars ); // write the final result if ( vFlops ) { - pAbs = Saig_ManAbstraction( p, 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 ); @@ -987,3 +385,5 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + |