summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abclib.dsp4
-rw-r--r--src/base/abci/abc.c86
-rw-r--r--src/sat/bmc/bmcChain.c339
-rw-r--r--src/sat/bmc/module.make1
4 files changed, 430 insertions, 0 deletions
diff --git a/abclib.dsp b/abclib.dsp
index ba457573..5559b243 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1479,6 +1479,10 @@ SOURCE=.\src\sat\bmc\bmcCexTools.c
# End Source File
# Begin Source File
+SOURCE=.\src\sat\bmc\bmcChain.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\sat\bmc\bmcEco.c
# End Source File
# Begin Source File
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 \
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-27 19:32:08 +0000