diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-11-04 20:35:36 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-11-04 20:35:36 -0800 |
commit | 8c2e51824e8925ea4e2ba6635fa24d44f10f155e (patch) | |
tree | 27275e16f1ad97f5ee5490675a4ba3edb449961a /src | |
parent | d75b8ce8744539271bfce97551450f7b4bcba452 (diff) | |
download | abc-8c2e51824e8925ea4e2ba6635fa24d44f10f155e.tar.gz abc-8c2e51824e8925ea4e2ba6635fa24d44f10f155e.tar.bz2 abc-8c2e51824e8925ea4e2ba6635fa24d44f10f155e.zip |
Experimental implementation of BMC-related procedures.
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abc.c | 86 | ||||
-rw-r--r-- | src/sat/bmc/bmcChain.c | 339 | ||||
-rw-r--r-- | src/sat/bmc/module.make | 1 |
3 files changed, 426 insertions, 0 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 37d96dcc..7bd2b617 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -428,6 +428,7 @@ static int Abc_CommandAbc9GroupProve ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SplitProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9ChainBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9BCore ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ICheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1028,6 +1029,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&splitprove", Abc_CommandAbc9SplitProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&chainbmc", Abc_CommandAbc9ChainBmc, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bcore", Abc_CommandAbc9BCore, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&icheck", Abc_CommandAbc9ICheck, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 ); @@ -35458,6 +35460,90 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9ChainBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Bmc_ChainTest( Gia_Man_t * p, int nFrameMax, int nConfMax, int fVerbose, int fVeryVerbose ); + int nFrameMax = 200; + int nConfMax = 0; + int fVerbose = 0; + int fVeryVerbose = 0; + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FCvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrameMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrameMax < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfMax < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'w': + fVeryVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9ChainBmc(): There is no AIG.\n" ); + return 0; + } + if ( !Gia_ManRegNum(pAbc->pGia) ) + { + Abc_Print( -1, "Abc_CommandAbc9ChainBmc(): The AIG is combinational.\n" ); + return 0; + } + Bmc_ChainTest( pAbc->pGia, nFrameMax, nConfMax, fVerbose, fVeryVerbose ); + //pAbc->Status = ...; + //pAbc->nFrames = pPars->iFrame; + //Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); + return 0; +usage: + Abc_Print( -2, "usage: &chainbmc [-FC <num>] [-vwh]\n" ); + Abc_Print( -2, "\t runs a specialized flavor of BMC\n" ); + Abc_Print( -2, "\t-F <num> : the max number of timeframes (0 = unused) [default = %d]\n", nFrameMax ); + Abc_Print( -2, "\t-C <num> : the max number of conflicts (0 = unused) [default = %d]\n", nConfMax ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing even more information [default = %s]\n", fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9BCore( Abc_Frame_t * pAbc, int argc, char ** argv ) { int c; diff --git a/src/sat/bmc/bmcChain.c b/src/sat/bmc/bmcChain.c new file mode 100644 index 00000000..d2a57d12 --- /dev/null +++ b/src/sat/bmc/bmcChain.c @@ -0,0 +1,339 @@ +/**CFile**************************************************************** + + FileName [bmcChain.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [Implementation of chain BMC.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bmcChain.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "aig/gia/giaAig.h" +#include "sat/cnf/cnf.h" +#include "sat/bsat/satSolver.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Find the first failure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Bmc_ChainFailOneOutput( Gia_Man_t * p, int nFrameMax, int nConfMax, int fVerbose, int fVeryVerbose ) +{ + int RetValue; + Abc_Cex_t * pCex = NULL; + Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + Saig_ParBmc_t Pars, * pPars = &Pars; + Saig_ParBmcSetDefaultParams( pPars ); + pPars->nFramesMax = nFrameMax; + pPars->nConfLimit = nConfMax; + pPars->fVerbose = fVeryVerbose; + RetValue = Saig_ManBmcScalable( pAig, pPars ); + if ( RetValue == 0 ) // SAT + { + pCex = pAig->pSeqModel, pAig->pSeqModel = NULL; + if ( fVeryVerbose ) + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n", pCex->iPo, p->pName, pCex->iFrame ); + } + else if ( fVeryVerbose ) + Abc_Print( 1, "No output asserted in %d frames. Resource limit reached.\n", pPars->iFrame+2 ); + Aig_ManStop( pAig ); + return pCex; +} + +/**Function************************************************************* + + Synopsis [Move GIA into the failing state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupWithInit( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsCi(pObj) ) + { + pObj->Value = Gia_ManAppendCi( pNew ); + pObj->Value = Abc_LitNotCond( pObj->Value, pObj->fMark0 ); + } + else if ( Gia_ObjIsCo(pObj) ) + { + pObj->Value = Gia_ObjFanin0Copy(pObj); + pObj->Value = Abc_LitNotCond( pObj->Value, pObj->fMark0 ); + pObj->Value = Gia_ManAppendCo( pNew, pObj->Value ); + } + } + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} +Gia_Man_t * Gia_ManVerifyCexAndMove( Gia_Man_t * pGia, Abc_Cex_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Gia_ManCleanMark0(pGia); + Gia_ManForEachRo( pGia, pObj, i ) + pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Gia_ManForEachPi( pGia, pObj, k ) + pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); + Gia_ManForEachAnd( pGia, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( pGia, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; + Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k ) + pObjRo->fMark0 = pObjRi->fMark0; + } + assert( iBit == p->nBits ); + RetValue = Gia_ManPo(pGia, p->iPo)->fMark0; + assert( RetValue ); + // set PI/PO values to zero and transfer RO values to RI + Gia_ManForEachPi( pGia, pObj, k ) + pObj->fMark0 = 0; + Gia_ManForEachPo( pGia, pObj, k ) + pObj->fMark0 = 0; + Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k ) + pObjRi->fMark0 = pObjRo->fMark0; + // duplicate assuming CI/CO marks are set correctly + pNew = Gia_ManDupWithInit( pGia ); + Gia_ManCleanMark0(pGia); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Find what outputs fail in this state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupPosAndPropagateInit( Gia_Man_t * p ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManHashAlloc( pNew ); + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsPi(p, pObj) ) + pObj->Value = Gia_ManAppendCi( pNew ); + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = 0; + else if ( Gia_ObjIsPo(p, pObj) ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManHashStop( pNew ); + assert( Gia_ManPiNum(p) == Gia_ManPiNum(pNew) ); + assert( Gia_ManPoNum(p) == Gia_ManPoNum(pNew) ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} +sat_solver * Gia_ManDeriveSatSolver( Gia_Man_t * p ) +{ +// return Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + sat_solver * pSat; + Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + Cnf_Dat_t * pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); + Aig_ManStop( pAig ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + Cnf_DataFree( pCnf ); + assert( p->nRegs == 0 ); + return pSat; +} +Vec_Int_t * Bmc_ChainFindFailedOutputs( Gia_Man_t * p ) +{ + Vec_Int_t * vOutputs; + Gia_Man_t * pInit; + Gia_Obj_t * pObj; + sat_solver * pSat; + int i, Lit, status = 0; + // derive output logic cones + pInit = Gia_ManDupPosAndPropagateInit( p ); + // derive SAT solver and test + pSat = Gia_ManDeriveSatSolver( pInit ); + vOutputs = Vec_IntAlloc( 100 ); + Gia_ManForEachPo( pInit, pObj, i ) + { + if ( Gia_ObjFaninLit0p(pInit, pObj) == 0 ) + continue; + Lit = Abc_Var2Lit( i+1, 0 ); + status = sat_solver_solve( pSat, &Lit, &Lit + 1, 0, 0, 0, 0 ); + if ( status == l_True ) + Vec_IntPush( vOutputs, i ); + } + Gia_ManStop( pInit ); + sat_solver_delete( pSat ); + return vOutputs; +} + +/**Function************************************************************* + + Synopsis [Cleanup AIG by removing COs replacing failed out by const0.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_ObjMakePoConst0( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + assert( Gia_ObjIsCo(pObj) ); + pObj->iDiff0 = Gia_ObjId( p, pObj ); + pObj->fCompl0 = 0; +} +int Gia_ManCountNonConst0( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, Count = 0; + Gia_ManForEachPo( p, pObj, i ) + Count += (Gia_ObjFaninLit0p(p, pObj) != 0); + return Count; +} +Gia_Man_t * Bmc_ChainCleanup( Gia_Man_t * p, Vec_Int_t * vOutputs ) +{ + int i, iOut; + Vec_IntForEachEntry( vOutputs, iOut, i ) + { + Gia_Obj_t * pObj = Gia_ManPo( p, iOut ); + assert( Gia_ObjFaninLit0p(p, pObj) != 0 ); + Gia_ObjMakePoConst0( p, pObj ); + assert( Gia_ObjFaninLit0p(p, pObj) == 0 ); + } + return Gia_ManCleanup( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_ChainTest( Gia_Man_t * p, int nFrameMax, int nConfMax, int fVerbose, int fVeryVerbose ) +{ + int Iter, IterMax = 10000; + Gia_Man_t * pTemp, * pNew = Gia_ManDup(p); + Abc_Cex_t * pCex = NULL; + Vec_Int_t * vOutputs; + abctime clk = Abc_Clock(); + int DepthTotal = 0; + for ( Iter = 0; Iter < IterMax; Iter++ ) + { + if ( Gia_ManPoNum(pNew) == 0 ) + { + if ( fVerbose ) + printf( "Finished all POs.\n" ); + break; + } + // run BMC till the first failure + pCex = Bmc_ChainFailOneOutput( pNew, nFrameMax, nConfMax, fVerbose, fVeryVerbose ); + if ( pCex == NULL ) + { + if ( fVerbose ) + printf( "BMC could not detect a failed output in %d frames with %d conflicts.\n", nFrameMax, nConfMax ); + break; + } + assert( !Iter || pCex->iFrame > 0 ); + // move the AIG to the failure state + pNew = Gia_ManVerifyCexAndMove( pTemp = pNew, pCex ); + Gia_ManStop( pTemp ); + DepthTotal += pCex->iFrame; + // find outputs that fail in this state + vOutputs = Bmc_ChainFindFailedOutputs( pNew ); + assert( Vec_IntFind(vOutputs, pCex->iPo) >= 0 ); + Abc_CexFree( pCex ); + // remove them from the AIG + pNew = Bmc_ChainCleanup( pTemp = pNew, vOutputs ); + Gia_ManStop( pTemp ); + // perform sequential cleanup +// pNew = Gia_ManSeqStructSweep( pTemp = pNew, 0, 1, 0 ); +// Gia_ManStop( pTemp ); + // printout + if ( fVerbose ) + { + int nNonConst = Gia_ManCountNonConst0(pNew); + printf( "Iter %4d : ", Iter+1 ); + printf( "Depth =%6d ", DepthTotal ); + printf( "FailPo =%6d ", Vec_IntSize(vOutputs) ); + printf( "UndefPo =%6d ", nNonConst ); + printf( "(%6.2f %%) ", 100.0 * nNonConst / Gia_ManPoNum(pNew) ); + printf( "AIG = %8d ", Gia_ManAndNum(pNew) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + Vec_IntFree( vOutputs ); + } + printf( "Completed a CEX chain with %d segments, %d frames, and %d failed POs (out of %d). ", + Iter, DepthTotal, Gia_ManPoNum(pNew) - Gia_ManCountNonConst0(pNew), Gia_ManPoNum(pNew) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + Gia_ManStop( pNew ); + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index 72af4dc1..3de71902 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -10,6 +10,7 @@ SRC += src/sat/bmc/bmcBCore.c \ src/sat/bmc/bmcCexMin1.c \ src/sat/bmc/bmcCexMin2.c \ src/sat/bmc/bmcCexTools.c \ + src/sat/bmc/bmcChain.c \ src/sat/bmc/bmcEco.c \ src/sat/bmc/bmcFault.c \ src/sat/bmc/bmcICheck.c \ |