diff options
Diffstat (limited to 'src/sat/bmc')
| -rw-r--r-- | src/sat/bmc/bmc.h | 15 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBCore.c | 272 | ||||
| -rw-r--r-- | src/sat/bmc/module.make | 3 |
3 files changed, 288 insertions, 2 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 3eeeb7b5..558b2d62 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -94,7 +94,18 @@ struct Bmc_AndPar_t_ int nFailOuts; // the number of failed outputs int nDropOuts; // the number of dropped outputs }; - + +typedef struct Bmc_BCorePar_t_ Bmc_BCorePar_t; +struct Bmc_BCorePar_t_ +{ + int iFrame; // timeframe + int iOutput; // property output + int nTimeOut; // timeout in seconds + char * pFilePivots; // file name with AIG IDs of pivot objects + char * pFileProof; // file name to write the resulting proof + int fVerbose; // verbose output +}; + typedef struct Bmc_MulPar_t_ Bmc_MulPar_t; struct Bmc_MulPar_t_ { @@ -117,6 +128,8 @@ struct Bmc_MulPar_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== bmcBCore.c ==========================================================*/ +extern void Bmc_ManBCorePerform( Gia_Man_t * pGia, Bmc_BCorePar_t * pPars ); /*=== bmcBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); /*=== bmcBmc2.c ==========================================================*/ diff --git a/src/sat/bmc/bmcBCore.c b/src/sat/bmc/bmcBCore.c new file mode 100644 index 00000000..cde49f52 --- /dev/null +++ b/src/sat/bmc/bmcBCore.c @@ -0,0 +1,272 @@ +/**CFile**************************************************************** + + FileName [bmcBCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [Performs recording of BMC core.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bmcBCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "sat/bsat/satSolver.h" +#include "sat/bsat/satStore.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Collect pivot variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Bmc_ManBCoreReadPivots( char * pName ) +{ + int Num; + Vec_Int_t * vPivots = Vec_IntAlloc( 100 ); + FILE * pFile = fopen( pName, "r" ); + while ( fscanf( pFile, "%d", &Num ) == 1 ) + Vec_IntPush( vPivots, Num ); + fclose( pFile ); + return vPivots; +} +Vec_Int_t * Bmc_ManBCoreCollectPivots( Gia_Man_t * p, char * pName, Vec_Int_t * vVarMap ) +{ + Gia_Obj_t * pObj; + int i, iVar, iFrame; + Vec_Int_t * vPivots = Vec_IntAlloc( 100 ); + Vec_Int_t * vVars = Bmc_ManBCoreReadPivots( pName ); + Gia_ManForEachObj( p, pObj, i ) + pObj->fMark0 = 0; + Vec_IntForEachEntry( vVars, iVar, i ) + if ( iVar > 0 && iVar < Gia_ManObjNum(p) ) + Gia_ManObj( p, iVar )->fMark0 = 1; + else + printf( "Cannot find object with Id %d in the given AIG.\n", iVar ); + Vec_IntForEachEntryDouble( vVarMap, iVar, iFrame, i ) + if ( Gia_ManObj( p, iVar )->fMark0 ) + Vec_IntPush( vPivots, Abc_Lit2Var(i) ); + Gia_ManForEachObj( p, pObj, i ) + pObj->fMark0 = 0; + Vec_IntFree( vVars ); + return vPivots; +} + +/**Function************************************************************* + + Synopsis [Collect (Id; Frame) pairs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Bmc_ManBCoreAssignVar( Gia_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vNodes ) +{ + pObj->Value = Abc_Lit2Var(Vec_IntSize(vNodes)); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); + Vec_IntPush( vNodes, f ); +// printf( "Obj %3d Frame %3d ---> Var %3d ", Gia_ObjId(p, pObj), f, pObj->Value ); +// Gia_ObjPrint( p, pObj ); +} +void Bmc_ManBCoreCollect_rec( Gia_Man_t * p, int Id, int f, Vec_Int_t * vNodes, Vec_Int_t * vRootsNew ) +{ + Gia_Obj_t * pObj; + if ( Gia_ObjIsTravIdCurrentId(p, Id) ) + return; + Gia_ObjSetTravIdCurrentId(p, Id); + pObj = Gia_ManObj( p, Id ); + Bmc_ManBCoreAssignVar( p, pObj, f, vNodes ); + if ( Gia_ObjIsPi(p, pObj) ) + return; + if ( Gia_ObjIsRo(p, pObj) ) + { + Vec_IntPush( vRootsNew, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); + Bmc_ManBCoreCollect_rec( p, Gia_ObjFaninId0p(p, pObj), f, vNodes, vRootsNew ); + Bmc_ManBCoreCollect_rec( p, Gia_ObjFaninId1p(p, pObj), f, vNodes, vRootsNew ); +} +Vec_Int_t * Bmc_ManBCoreCollect( Gia_Man_t * p, int iFrame, int iOut, sat_solver * pSat ) +{ + Gia_Obj_t * pObj; + int f, i, iObj, nNodesOld; + Vec_Int_t * vNodes = Vec_IntAlloc( 100 ); + Vec_Int_t * vRoots = Vec_IntAlloc( 100 ); + Vec_Int_t * vRoots2 = Vec_IntAlloc( 100 ); + assert( iFrame >= 0 && iOut >= 0 ); + // add first variables + Vec_IntPush( vNodes, -1 ); + Vec_IntPush( vNodes, -1 ); + Bmc_ManBCoreAssignVar( p, Gia_ManPo(p, iOut), iFrame, vNodes ); + // start with root node + Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ManPo(p, iOut)) ); + // iterate through time frames + for ( f = iFrame; f >= 0; f-- ) + { + Gia_ManIncrementTravId( p ); + // add constant node + Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); + Bmc_ManBCoreAssignVar( p, Gia_ManConst0(p), f, vNodes ); + sat_solver_add_const( pSat, Gia_ManConst0(p)->Value, 1 ); + // collect nodes in this timeframe + Vec_IntClear( vRoots2 ); + nNodesOld = Vec_IntSize(vNodes); + Gia_ManForEachObjVec( vRoots, p, pObj, i ) + Bmc_ManBCoreCollect_rec( p, Gia_ObjFaninId0p(p, pObj), f, vNodes, vRoots2 ); + if ( f == iFrame ) + { + // add the final clause + pObj = Gia_ManPo(p, iOut); + assert( pObj->Value == 1 ); + assert( Gia_ObjFanin0(pObj)->Value == 3 ); +// sat_solver_add_const( pSat, Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); + sat_solver_add_constraint( pSat, Gia_ObjFanin0(pObj)->Value, pObj->Value, Gia_ObjFaninC0(pObj) ); + } + else + { + // connect current RIs to previous ROs + Gia_ManForEachObjVec( vRoots, p, pObj, i ) + sat_solver_add_buffer( pSat, pObj->Value, Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); + } + Gia_ManForEachObjVec( vRoots2, p, pObj, i ) + pObj->Value = Gia_ObjRiToRo(p, pObj)->Value; + // add nodes of this timeframe + Vec_IntForEachEntryStart( vNodes, iObj, i, nNodesOld ) + { + pObj = Gia_ManObj(p, iObj); i++; + if ( Gia_ObjIsCi(pObj) ) + continue; + assert( Gia_ObjIsAnd(pObj) ); + sat_solver_add_and( pSat, pObj->Value, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); + } + // collect constant node + ABC_SWAP( Vec_Int_t *, vRoots, vRoots2 ); + } + // add constraint variables for the init state + Gia_ManForEachObjVec( vRoots, p, pObj, i ) + { + sat_solver_add_constraint( pSat, pObj->Value, Abc_Lit2Var(Vec_IntSize(vNodes)), 1 ); + pObj = Gia_ObjRiToRo(p, pObj); + Bmc_ManBCoreAssignVar( p, pObj, -1, vNodes ); + } + Vec_IntFree( vRoots ); + Vec_IntFree( vRoots2 ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_ManBCorePerform( Gia_Man_t * p, Bmc_BCorePar_t * pPars ) +{ + clock_t clk = clock(); + Intp_Man_t * pManProof; + Vec_Int_t * vVarMap, * vCore; + sat_solver * pSat; + FILE * pFile; + void * pSatCnf; + int RetValue; + // create SAT solver + pSat = sat_solver_new(); + sat_solver_store_alloc( pSat ); + sat_solver_setnvars( pSat, 1000 ); + sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); + vVarMap = Bmc_ManBCoreCollect( p, pPars->iFrame, pPars->iOutput, pSat ); + sat_solver_store_mark_roots( pSat ); + // create pivot variables + if ( pPars->pFilePivots ) + { + Vec_Int_t * vPivots = Bmc_ManBCoreCollectPivots(p, pPars->pFilePivots, vVarMap); + sat_solver_set_pivot_variables( pSat, Vec_IntArray(vPivots), Vec_IntSize(vPivots) ); + Vec_IntReleaseArray( vPivots ); + Vec_IntFree( vPivots ); + } + // solve the problem + RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( RetValue == l_Undef ) + { + Vec_IntFree( vVarMap ); + sat_solver_delete( pSat ); + printf( "Timeout of conflict limit is reached.\n" ); + return; + } + if ( RetValue == l_True ) + { + Vec_IntFree( vVarMap ); + sat_solver_delete( pSat ); + printf( "The BMC problem is SAT.\n" ); + return; + } + if ( pPars->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 ); + Sto_ManDumpClauses( (Sto_Man_t *)pSatCnf, "cnf_store.txt" ); + // derive the UNSAT core + clk = clock(); + pManProof = Intp_ManAlloc(); + vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 1, pPars->fVerbose ); + Intp_ManFree( pManProof ); + if ( pPars->fVerbose ) + { + printf( "UNSAT core contains %8d (out of %8d) learned clauses. ", Vec_IntSize(vCore), sat_solver_nconflicts(pSat) ); + Abc_PrintTime( 1, "Time", clock() - clk ); + } + // write the problem + pFile = pPars->pFileProof ? fopen( pPars->pFileProof, "wb" ) : stdout; + Intp_ManUnsatCorePrintForBmc( pFile, (Sto_Man_t *)pSatCnf, vCore, vVarMap ); + if ( pFile != stdout ) + fclose( pFile ); + // cleanup + Sto_ManFree( (Sto_Man_t *)pSatCnf ); + Vec_IntFree( vVarMap ); + Vec_IntFree( vCore ); + sat_solver_delete( pSat ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index 6deb9eb1..2ce321c6 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -1,4 +1,5 @@ -SRC += src/sat/bmc/bmcBmc.c \ +SRC += src/sat/bmc/bmcBCore.c \ + src/sat/bmc/bmcBmc.c \ src/sat/bmc/bmcBmc2.c \ src/sat/bmc/bmcBmc3.c \ src/sat/bmc/bmcBmcAnd.c \ |