diff options
Diffstat (limited to 'src/aig/saig/saigBmc.c')
| -rw-r--r-- | src/aig/saig/saigBmc.c | 215 |
1 files changed, 179 insertions, 36 deletions
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 0bbf63f9..2248fb37 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -21,6 +21,7 @@ #include "saig.h" #include "cnf.h" #include "satStore.h" +#include "ssw.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -33,9 +34,9 @@ struct Saig_Bmc_t_ { // parameters int nFramesMax; // the max number of timeframes to consider + int nNodesMax; // the max number of nodes to add int nConfMaxOne; // the max number of conflicts at a target int nConfMaxAll; // the max number of conflicts for all targets - int nNodesMax; // the max number of nodes to add int fVerbose; // enables verbose output // AIG managers Aig_Man_t * pAig; // the user's AIG manager @@ -46,11 +47,14 @@ struct Saig_Bmc_t_ Vec_Ptr_t * vAig2Frm; // mapping of AIG nodees into Frames nodes // SAT solver sat_solver * pSat; // SAT solver - Vec_Int_t * vObj2Var; // mapping of frames objects in CNF variables int nSatVars; // the number of used SAT variables + Vec_Int_t * vObj2Var; // mapping of frames objects in CNF variables + // subproblems Vec_Ptr_t * vTargets; // targets to be solved in this interval - int iFramelast; // last frame + int iFrameLast; // last frame int iOutputLast; // last output + int iFrameFail; // failed frame + int iOutputFail; // failed output }; static inline int Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vObj2Var, pObj->Id ); } @@ -77,7 +81,7 @@ static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, i SeeAlso [] ***********************************************************************/ -Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose ) +Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ) { Saig_Bmc_t * p; Aig_Obj_t * pObj; @@ -86,10 +90,10 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAl p = (Saig_Bmc_t *)malloc( sizeof(Saig_Bmc_t) ); memset( p, 0, sizeof(Saig_Bmc_t) ); // set parameters - p->nFramesMax = 1000000; + p->nFramesMax = nFramesMax; + p->nNodesMax = nNodesMax; p->nConfMaxOne = nConfMaxOne; p->nConfMaxAll = nConfMaxAll; - p->nNodesMax = nNodesMax; p->fVerbose = fVerbose; p->pAig = pAig; p->nObjs = Aig_ManObjNumMax(pAig); @@ -103,15 +107,17 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAl Saig_ManForEachLo( pAig, pObj, i ) Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); // create SAT solver + p->nSatVars = 1; p->pSat = sat_solver_new(); sat_solver_setnvars( p->pSat, 2000 ); - p->nSatVars = 1; Lit = toLit( p->nSatVars ); sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ ); // other data structures p->vTargets = Vec_PtrAlloc( 0 ); p->vVisited = Vec_PtrAlloc( 0 ); + p->iOutputFail = -1; + p->iFrameFail = -1; return p; } @@ -174,15 +180,15 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i p1 = Saig_BmcObjChild1( p, pObj, i ); if ( p0 == Aig_Not(p1) ) - pRes = Aig_Not(pConst1); + pRes = Aig_ManConst0(p->pFrm); else if ( Aig_Regular(p0) == pConst1 ) - pRes = (p0 == pConst1) ? p1 : Aig_Not(pConst1); + pRes = (p0 == pConst1) ? p1 : Aig_ManConst0(p->pFrm); else if ( Aig_Regular(p1) == pConst1 ) - pRes = (p1 == pConst1) ? p0 : Aig_Not(pConst1); + pRes = (p1 == pConst1) ? p0 : Aig_ManConst0(p->pFrm); else pRes = AIG_VISITED; - if ( pRes != pConst1 && pRes != Aig_Not(pConst1) ) + if ( pRes != AIG_VISITED && !Aig_ObjIsConst1(Aig_Regular(pRes)) ) pRes = AIG_VISITED; } Saig_BmcObjSetFrame( p, pObj, i, pRes ); @@ -222,6 +228,7 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i ); pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) ); } + assert( pRes != AIG_VISITED ); Saig_BmcObjSetFrame( p, pObj, i, pRes ); return pRes; } @@ -239,23 +246,30 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int ***********************************************************************/ void Saig_BmcInterval( Saig_Bmc_t * p ) { - Aig_Obj_t * pTarget, * pObj; - int i, nNodes = Aig_ManNodeNum( p->pFrm ); + Aig_Obj_t * pTarget; +// Aig_Obj_t * pObj; +// int i; + int nNodes = Aig_ManObjNum( p->pFrm ); Vec_PtrClear( p->vTargets ); - for ( ; p->iFramelast < p->nFramesMax; p->iFramelast++, p->iOutputLast = 0 ) + for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 ) { if ( p->iOutputLast == 0 ) { - Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFramelast, Aig_ManConst1(p->pFrm) ); - Saig_ManForEachPi( p->pAig, pObj, i ) - Saig_BmcObjSetFrame( p, pObj, p->iFramelast, Aig_ObjCreatePi(p->pFrm) ); + Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) ); +// Saig_ManForEachPi( p->pAig, pObj, i ) +// Saig_BmcObjSetFrame( p, pObj, p->iFrameLast, Aig_ObjCreatePi(p->pFrm) ); } for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ ) { - if ( Aig_ManNodeNum(p->pFrm) >= nNodes + p->nNodesMax ) + if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax ) return; - Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax ); - pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax ); + Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast ); + pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast ); + + ///////// +// if ( Aig_ObjIsConst1(Aig_Regular(pTarget)) ) +// continue; + Vec_PtrPush( p->vTargets, pTarget ); } } @@ -281,6 +295,7 @@ Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj return pObj->pData = Aig_ObjCreatePi(pNew); Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) ); Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) ); + assert( pObj->pData == NULL ); return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); } @@ -300,13 +315,18 @@ Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p ) Aig_Man_t * pNew; Aig_Obj_t * pObj, * pObjNew; int i; + Aig_ManForEachObj( p->pFrm, pObj, i ) + assert( pObj->pData == NULL ); + pNew = Aig_ManStart( p->nNodesMax ); Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew); Vec_PtrClear( p->vVisited ); Vec_PtrPush( p->vVisited, Aig_ManConst1(p->pFrm) ); Vec_PtrForEachEntry( p->vTargets, pObj, i ) { +// assert( !Aig_ObjIsConst1(Aig_Regular(pObj)) ); pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) ); + assert( !Aig_IsComplement(pObjNew) ); Aig_ObjCreatePo( pNew, pObjNew ); } return pNew; @@ -329,12 +349,14 @@ void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf ) int i, Lits[2], VarNumOld, VarNumNew; Vec_PtrForEachEntry( p->vVisited, pObj, i ) { - pObjNew = pObj->pData; + // get the new variable of this node + pObjNew = pObj->pData; pObj->pData = NULL; - VarNumNew = pCnf->pVarNums[ pObjNew->Id ]; + VarNumNew = pCnf->pVarNums[ pObjNew->Id ]; if ( VarNumNew == -1 ) continue; - VarNumOld = Saig_BmcSatNum( p, pObj ); + // get the old variable of this node + VarNumOld = Saig_BmcSatNum( p, pObj ); if ( VarNumOld == 0 ) { Saig_BmcSetSatNum( p, pObj, VarNumNew ); @@ -369,11 +391,88 @@ void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf ) SeeAlso [] ***********************************************************************/ +void Saig_BmcDeriveFailed( Saig_Bmc_t * p, int iTargetFail ) +{ + int k; + p->iOutputFail = p->iOutputLast; + p->iFrameFail = p->iFrameLast; + for ( k = Vec_PtrSize(p->vTargets); k > iTargetFail; k-- ) + { + if ( p->iOutputFail == 0 ) + { + p->iOutputFail = Saig_ManPoNum(p->pAig); + p->iFrameFail--; + } + p->iOutputFail--; + } +} + +/**Function************************************************************* + + Synopsis [Solves targets with the given resource limit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p ) +{ + Ssw_Cex_t * pCex; + Aig_Obj_t * pObj, * pObjFrm; + int i, f, iVarNum; + // start the counter-example + pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 ); + pCex->iFrame = p->iFrameFail; + pCex->iPo = p->iOutputFail; + // copy the bit data + for ( f = 0; f <= p->iFrameFail; f++ ) + { + Saig_ManForEachPi( p->pAig, pObj, i ) + { + pObjFrm = Saig_BmcObjFrame( p, pObj, f ); + if ( pObjFrm == NULL ) + continue; + iVarNum = Saig_BmcSatNum( p, pObjFrm ); + if ( iVarNum == 0 ) + continue; + if ( sat_solver_var_value( p->pSat, iVarNum ) ) + Aig_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i ); + } + } + // verify the counter example + if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) ) + { + printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" ); + Ssw_SmlFreeCounterExample( pCex ); + pCex = NULL; + } + return pCex; +} + +/**Function************************************************************* + + Synopsis [Solves targets with the given resource limit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Saig_BmcSolveTargets( Saig_Bmc_t * p ) { Aig_Obj_t * pObj; int i, VarNum, Lit, RetValue; assert( Vec_PtrSize(p->vTargets) > 0 ); + if ( p->pSat->qtail != p->pSat->qhead ) + { + RetValue = sat_solver_simplify(p->pSat); + assert( RetValue != 0 ); + } Vec_PtrForEachEntry( p->vTargets, pObj, i ) { if ( p->pSat->stats.conflicts > p->nConfMaxAll ) @@ -386,6 +485,8 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p ) if ( RetValue == l_Undef ) // undecided return l_Undef; // generate counter-example + Saig_BmcDeriveFailed( p, i ); + p->pAig->pSeqModel = Saig_BmcGenerateCounterExample( p ); return l_True; } return l_False; @@ -393,6 +494,28 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Vec_PtrForEachEntry( p->vTargets, pObj, i ) + Aig_ObjCreatePo( p->pFrm, pObj ); + Aig_ManPrintStats( p->pFrm ); + Aig_ManCleanup( p->pFrm ); + Aig_ManPrintStats( p->pFrm ); +} + +/**Function************************************************************* + Synopsis [Performs BMC with the given parameters.] Description [] @@ -402,17 +525,27 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p ) SeeAlso [] ***********************************************************************/ -void Saig_BmcPerform( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose ) +void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ) { Saig_Bmc_t * p; Aig_Man_t * pNew; Cnf_Dat_t * pCnf; - int RetValue, clk = clock(); - p = Saig_BmcManStart( pAig, nConfMaxOne, nConfMaxAll, nNodesMax, fVerbose ); - while ( 1 ) + int Iter, RetValue, clk = clock(), clk2; + p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose ); + if ( fVerbose ) + { + printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", + Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), + Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); + printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", + nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll ); + } + for ( Iter = 0; ; Iter++ ) { - // add new logic slice to frames + clk2 = clock(); + // add new logic interval to frames Saig_BmcInterval( p ); +// Saig_BmcAddTargetsAsPos( p ); if ( Vec_PtrSize(p->vTargets) == 0 ) break; // convert logic slice into new AIG @@ -427,20 +560,30 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nN Aig_ManStop( pNew ); // solve the targets RetValue = Saig_BmcSolveTargets( p ); + if ( fVerbose ) + { + printf( "%3d : F = %3d. O = %3d. And = %7d. Var = %7d. Conf = %7d. ", + Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts ); + PRT( "Time", clock() - clk2 ); + } if ( RetValue != l_False ) break; } if ( RetValue == l_True ) - printf( "BMC failed for output %d in frame %d. ", p->iOutputLast, p->iFramelast ); + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", + p->iOutputFail, p->iFrameFail ); else // if ( RetValue == l_False || RetValue == l_Undef ) - printf( "BMC completed for %d timeframes. ", p->iFramelast ); + printf( "No output was asserted in %d frames. ", p->iFrameLast ); PRT( "Time", clock() - clk ); - if ( p->iFramelast >= p->nFramesMax ) - printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); - else if ( p->pSat->stats.conflicts > p->nConfMaxAll ) - printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); - else - printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne ); + if ( RetValue != l_True ) + { + if ( p->iFrameLast >= p->nFramesMax ) + printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); + else if ( p->pSat->stats.conflicts > p->nConfMaxAll ) + printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); + else + printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne ); + } Saig_BmcManStop( p ); } |