Skip to content

A
abc
Commit f620a857 by Alan Mishchenko
Options

Specialized induction check.

parent a457bfe1
Showing with 289 additions and 5 deletions
abclib.dsp
......@@ -1443,6 +1443,10 @@ SOURCE=.\src\sat\bmc\bmcCexTools.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcICheck.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcLoad.c
# End Source File
# Begin Source File
......
src/aig/gia/gia.h
......@@ -253,6 +253,7 @@ struct Jf_Par_t_
int fCutMin;
int fFuncDsd;
int fGenCnf;
int fCnfObjIds;
int fPureAig;
int fVerbose;
int fVeryVerbose;
......@@ -1097,7 +1098,7 @@ extern Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars,
/*=== giaJf.c ===========================================================*/
extern void Jf_ManSetDefaultPars( Jf_Par_t * pPars );
extern Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );
extern Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p );
extern Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p, int fCnfObjIds );
/*=== giaIso.c ===========================================================*/
extern Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose );
......
src/aig/gia/giaJf.c
......@@ -1540,7 +1540,10 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p )
// derive CNF
if ( p->pPars->fGenCnf )
{
pNew->pData = Jf_ManCreateCnf( pNew, vLits, vClas );
if ( p->pPars->fCnfObjIds )
pNew->pData = Jf_ManCreateCnf( pNew, vLits, vClas );
else
pNew->pData = Jf_ManCreateCnfRemap( pNew, vLits, vClas );
}
Vec_IntFreeP( &vLits );
Vec_IntFreeP( &vClas );
......@@ -1749,11 +1752,12 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
Jf_ManFree( p );
return pNew;
}
Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p )
Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p, int fCnfObjIds )
{
Jf_Par_t Pars, * pPars = &Pars;
Jf_ManSetDefaultPars( pPars );
pPars->fGenCnf = 1;
pPars->fCnfObjIds = fCnfObjIds;
return Jf_ManPerformMapping( p, pPars );
}
void Jf_ManTestCnf( Gia_Man_t * p )
......@@ -1762,7 +1766,7 @@ void Jf_ManTestCnf( Gia_Man_t * p )
Cnf_Dat_t * pCnf;
int i;
// Cnf_Dat_t * pCnf = Cnf_DeriveGia( p );
pNew = Jf_ManDeriveCnf( p );
pNew = Jf_ManDeriveCnf( p, 1 );
pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
Cnf_DataWriteIntoFile( pCnf, "test.cnf", 0, NULL, NULL );
for ( i = 0; i < pCnf->nVars; i++ )
......
src/base/abci/abc.c
......@@ -401,6 +401,7 @@ static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9GroupProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Bmc ( 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 );
//static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -965,6 +966,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&gprove", Abc_CommandAbc9GroupProve, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&icheck", Abc_CommandAbc9ICheck, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
......@@ -32572,6 +32574,79 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int c, nFramesMax = 1, nTimeOut = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MTvh" ) ) != EOF )
{
switch ( c )
{
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFramesMax < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
nTimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nTimeOut < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9ICheck(): There is no AIG.\n" );
return 0;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "Abc_CommandAbc9ICheck(): The AIG is combinational.\n" );
return 0;
}
Bmc_PerformICheck( pAbc->pGia, nFramesMax, nTimeOut, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &icheck [-MT num] [-cvh]\n" );
Abc_Print( -2, "\t performs specialized inductiveness check\n" );
Abc_Print( -2, "\t-M num : the number of timeframes used for inductiion [default = %d]\n", nFramesMax );
Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9SatTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Bmc_LoadTest( Gia_Man_t * pGia, int fLoadCnf, int fVerbose );
src/sat/bmc/bmc.h
......@@ -128,6 +128,8 @@ extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, i
extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
/*=== bmcCexMin.c ==========================================================*/
extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
/*=== bmcICheck.c ==========================================================*/
extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbose );
/*=== bmcUnroll.c ==========================================================*/
extern Unr_Man_t * Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose );
extern Gia_Man_t * Unr_ManUnrollFrame( Unr_Man_t * p, int f );
......
src/sat/bmc/bmcBmcAnd.c
......@@ -983,7 +983,7 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
p->pCnf = Cnf_DeriveGia( p->pFrames );
else
{
p->pFrames = Jf_ManDeriveCnf( pTemp = p->pFrames ); Gia_ManStop( pTemp );
p->pFrames = Jf_ManDeriveCnf( pTemp = p->pFrames, 1 ); Gia_ManStop( pTemp );
p->pCnf = (Cnf_Dat_t *)p->pFrames->pData; p->pFrames->pData = NULL;
}
Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
......
src/sat/bmc/bmcICheck.c 0 → 100644
/**CFile****************************************************************
FileName [bmcICheck.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis [Performs specialized check.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bmcICheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbose )
{
Gia_Man_t * pMiter, * pTemp;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Vec_Int_t * vLits;
Gia_Obj_t * pObj, * pObj0, * pObj1;
int i, k, status, iVar0, iVar1, iVarOut;
int nLits, * pLits;
abctime clkStart = Abc_Clock();
assert( nFramesMax > 0 );
assert( Gia_ManRegNum(p) > 0 );
// create miter
pTemp = Gia_ManDup( p );
pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0 );
Gia_ManStop( pTemp );
assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
// derive CNF
pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
Gia_ManStop( pTemp );
pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
// start the SAT solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, Gia_ManRegNum(p) + Gia_ManCoNum(p) + pCnf->nVars * (nFramesMax + 1) );
sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
// load the last timeframe
Cnf_DataLift( pCnf, Gia_ManRegNum(p) + Gia_ManCoNum(p) );
// add one large OR clause
vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
Gia_ManForEachCo( p, pObj, i )
Vec_IntPush( vLits, Abc_Var2Lit(Gia_ManRegNum(p) + i, 0) );
sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
// add XOR clauses
Gia_ManForEachPo( p, pObj, i )
{
pObj0 = Gia_ManPo( pMiter, 2*i+0 );
pObj1 = Gia_ManPo( pMiter, 2*i+1 );
iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
iVarOut = Gia_ManRegNum(p) + i;
sat_solver_add_xor( pSat, iVar0, iVar1, iVarOut, 0 );
}
Gia_ManForEachRi( p, pObj, i )
{
pObj0 = Gia_ManRi( pMiter, i );
pObj1 = Gia_ManRi( pMiter, i + Gia_ManRegNum(p) );
iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
iVarOut = Gia_ManRegNum(p) + Gia_ManPoNum(p) + i;
sat_solver_add_xor( pSat, iVar0, iVar1, iVarOut, 0 );
}
// add timeframe clauses
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
assert( 0 );
// add other timeframes
printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
for ( k = 0; k < nFramesMax; k++ )
{
// collect variables of the RO nodes
Vec_IntClear( vLits );
Gia_ManForEachRo( pMiter, pObj, i )
Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pMiter, pObj)] );
// lift CNF again
Cnf_DataLift( pCnf, pCnf->nVars );
// stitch the clauses
Gia_ManForEachRi( pMiter, pObj, i )
{
iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj)];
iVar1 = Vec_IntEntry( vLits, i );
sat_solver_add_buffer( pSat, iVar0, iVar1, 0 );
}
// add equality clauses for the COs
Gia_ManForEachPo( p, pObj, i )
{
pObj0 = Gia_ManPo( pMiter, 2*i+0 );
pObj1 = Gia_ManPo( pMiter, 2*i+1 );
iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
sat_solver_add_buffer( pSat, iVar0, iVar1, 0 );
}
Gia_ManForEachRi( p, pObj, i )
{
pObj0 = Gia_ManRi( pMiter, i );
pObj1 = Gia_ManRi( pMiter, i + Gia_ManRegNum(p) );
iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
sat_solver_add_buffer_enable( pSat, iVar0, iVar1, i, 0 );
}
// add timeframe clauses
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
assert( 0 );
// collect literals
Vec_IntClear( vLits );
for ( i = 0; i < Gia_ManRegNum(p); i++ )
Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
// call the SAT solver
// sat_solver_compress( pSat );
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
assert( status == l_False );
// call analize_final
nLits = sat_solver_final( pSat, &pLits );
printf( "M = %d. AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
k+1, (k+1) * Gia_ManAndNum(pMiter),
sat_solver_nvars(pSat), sat_solver_nconflicts(pSat),
nLits, 100.0 * nLits / Gia_ManRegNum(p) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
}
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Gia_ManStop( pMiter );
Vec_IntFree( vLits );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/sat/bmc/module.make
......@@ -7,6 +7,7 @@ SRC += src/sat/bmc/bmcBmc.c \
src/sat/bmc/bmcCexMin1.c \
src/sat/bmc/bmcCexMin2.c \
src/sat/bmc/bmcCexTools.c \
src/sat/bmc/bmcICheck.c \
src/sat/bmc/bmcLoad.c \
src/sat/bmc/bmcMulti.c \
src/sat/bmc/bmcUnroll.c
src/sat/bsat/satSolver.h
......@@ -296,6 +296,25 @@ static inline int sat_solver_add_buffer( sat_solver * pSat, int iVarA, int iVarB
assert( Cid );
return 2;
}
static inline int sat_solver_add_buffer_enable( sat_solver * pSat, int iVarA, int iVarB, int iVarEn, int fCompl )
{
lit Lits[3];
int Cid;
assert( iVarA >= 0 && iVarB >= 0 && iVarEn >= 0 );
Lits[0] = toLitCond( iVarA, 0 );
Lits[1] = toLitCond( iVarB, !fCompl );
Lits[2] = toLitCond( iVarEn, 1 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
assert( Cid );
Lits[0] = toLitCond( iVarA, 1 );
Lits[1] = toLitCond( iVarB, fCompl );
Lits[2] = toLitCond( iVarEn, 1 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
assert( Cid );
return 2;
}
static inline int sat_solver_add_and( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
{
lit Lits[3];
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment