mirror of https://github.com/YosysHQ/abc.git
Experimental implementation of BMC-related procedures.
This commit is contained in:
Alan Mishchenko
parent
d75b8ce874
commit
8c2e51824e
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
@ -35447,6 +35449,90 @@ usage:
|
|||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
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 []
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
@ -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 \
|
||||
|
|
|
|||
Loading…
Reference in New Issue