/**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"
#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
{
Cnf_Dat_t * pCnf;
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
pAig->nRegs = 0;
pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
Aig_ManStop( pAig );
return pCnf;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPlus )
{
Gia_Obj_t * pObj;
int v;
Gia_ManForEachObj( pGia, pObj, v )
if ( p->pVarNums[Gia_ObjId(pGia, pObj)] >= 0 )
p->pVarNums[Gia_ObjId(pGia, pObj)] += nVarsPlus;
for ( v = 0; v < p->nLiterals; v++ )
p->pClauses[0][v] += 2*nVarsPlus;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pCnf, int nFramesMax, int nTimeOut, int fVerbose )
{
sat_solver * pSat;
Vec_Int_t * vLits;
Gia_Obj_t * pObj, * pObj0, * pObj1;
int i, k, iVar0, iVar1, iVarOut;
int VarShift = 0;
// 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 );
// 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) );
// load the last timeframe
Cnf_DataLiftGia( pCnf, pMiter, Gia_ManRegNum(p) + Gia_ManCoNum(p) );
VarShift += Gia_ManRegNum(p) + Gia_ManCoNum(p);
// 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_and( pSat, iVarOut, iVar0, iVar1, i );
}
// 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
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_DataLiftGia( pCnf, pMiter, pCnf->nVars );
VarShift += pCnf->nVars;
// stitch the clauses
Gia_ManForEachRi( pMiter, pObj, i )
{
iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj)];
iVar1 = Vec_IntEntry( vLits, i );
if ( iVar1 == -1 )
continue;
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 );
}
// sat_solver_compress( pSat );
Cnf_DataLiftGia( pCnf, pMiter, -VarShift );
Vec_IntFree( vLits );
return pSat;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose )
{
int fUseOldCnf = 0;
Gia_Man_t * pMiter, * pTemp;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Vec_Int_t * vLits, * vUsed;
int i, status, Lit;
int nLitsUsed, nLits, * pLits;
abctime clkStart = Abc_Clock();
assert( nFramesMax > 0 );
assert( Gia_ManRegNum(p) > 0 );
if ( fVerbose )
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) );
// create miter
pTemp = Gia_ManDup( p );
pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
Gia_ManStop( pTemp );
assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
// derive CNF
if ( fUseOldCnf )
pCnf = Cnf_DeriveGiaRemapped( pMiter );
else
{
pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
Gia_ManStop( pTemp );
pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
}
// collect positive literals
vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
for ( i = 0; i < Gia_ManRegNum(p); i++ )
Vec_IntPush( vLits, Abc_Var2Lit(i, fEmpty) );
// iteratively compute a minimal M-inductive set of next-state functions
nLitsUsed = fEmpty ? 0 : Vec_IntSize(vLits);
vUsed = Vec_IntAlloc( Vec_IntSize(vLits) );
while ( 1 )
{
int fChanges = 0;
// derive SAT solver
pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
// sat_solver_bookmark( 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 );
if ( status == l_Undef )
{
printf( "Timeout reached after %d seconds.\n", nTimeOut );
break;
}
if ( status == l_True )
{
printf( "The problem is satisfiable (the current set is not M-inductive).\n" );
break;
}
assert( status == l_False );
// call analize_final
nLits = sat_solver_final( pSat, &pLits );
// mark used literals
Vec_IntFill( vUsed, Vec_IntSize(vLits), 0 );
for ( i = 0; i < nLits; i++ )
Vec_IntWriteEntry( vUsed, Abc_Lit2Var(pLits[i]), 1 );
// check if there are any positive unused
Vec_IntForEachEntry( vLits, Lit, i )
{
assert( i == Abc_Lit2Var(Lit) );
if ( Abc_LitIsCompl(Lit) )
continue;
if ( Vec_IntEntry(vUsed, i) )
continue;
// positive literal became unused
Vec_IntWriteEntry( vLits, i, Abc_LitNot(Lit) );
nLitsUsed--;
fChanges = 1;
}
// report the results
if ( fVerbose )
printf( "M =%4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter),
Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
if ( fVerbose )
Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
// count the number of negative literals
sat_solver_delete( pSat );
if ( !fChanges || fEmpty )
break;
// break;
// sat_solver_rollback( pSat );
}
Cnf_DataFree( pCnf );
Gia_ManStop( pMiter );
Vec_IntFree( vLits );
Vec_IntFree( vUsed );
}
/**Function*************************************************************
Synopsis [Collect flops starting from the POs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bmc_PerformFindFlopOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRegs )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
if ( Gia_ObjIsCi(pObj) )
{
if ( Gia_ObjIsRo(p, pObj) )
Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
return;
}
assert( Gia_ObjIsAnd(pObj) );
Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin0(pObj), vRegs );
Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin1(pObj), vRegs );
}
void Bmc_PerformFindFlopOrder( Gia_Man_t * p, Vec_Int_t * vRegs )
{
Gia_Obj_t * pObj;
int i, iReg, k = 0;
// start with POs
Vec_IntClear( vRegs );
Gia_ManForEachPo( p, pObj, i )
Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
// add flop outputs in the B
Gia_ManIncrementTravId( p );
Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
Gia_ManForEachObjVec( vRegs, p, pObj, i )
{
assert( Gia_ObjIsPo(p, pObj) || Gia_ObjIsRo(p, pObj) );
if ( Gia_ObjIsRo(p, pObj) )
pObj = Gia_ObjRoToRi( p, pObj );
Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin0(pObj), vRegs );
}
// add dangling flops
Gia_ManForEachRo( p, pObj, i )
if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
// remove POs; keep flop outputs only; remap ObjId into CiId
assert( Vec_IntSize(vRegs) == Gia_ManCoNum(p) );
Gia_ManForEachObjVec( vRegs, p, pObj, i )
{
if ( i < Gia_ManPoNum(p) )
continue;
iReg = Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
assert( iReg >= 0 && iReg < Gia_ManRegNum(p) );
Vec_IntWriteEntry( vRegs, k++, iReg );
}
Vec_IntShrink( vRegs, k );
assert( Vec_IntSize(vRegs) == Gia_ManRegNum(p) );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fVerbose, Vec_Int_t * vLits )
{
int fUseOldCnf = 0;
Gia_Man_t * pMiter, * pTemp;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Vec_Int_t * vRegs = NULL;
// Vec_Int_t * vLits;
int i, Iter, status;
int nLitsUsed, RetValue = 0;
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, 0 );
Gia_ManStop( pTemp );
assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
// derive CNF
if ( fUseOldCnf )
pCnf = Cnf_DeriveGiaRemapped( pMiter );
else
{
//pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
//Gia_ManStop( pTemp );
//pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0, 0 );
}
/*
// collect positive literals
vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
for ( i = 0; i < Gia_ManRegNum(p); i++ )
Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
*/
// derive SAT solver
pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
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 );
if ( status == l_True )
{
printf( "I = %4d : ", nFramesMax );
printf( "Problem is satisfiable.\n" );
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Gia_ManStop( pMiter );
return 1;
}
if ( status == l_Undef )
{
printf( "ICheck: Timeout reached after %d seconds. \n", nTimeOut );
RetValue = 1;
goto cleanup;
}
assert( status == l_False );
// count the number of positive literals
nLitsUsed = 0;
for ( i = 0; i < Gia_ManRegNum(p); i++ )
if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
nLitsUsed++;
// try removing variables
vRegs = Vec_IntStartNatural( Gia_ManRegNum(p) );
if ( fBackTopo )
Bmc_PerformFindFlopOrder( p, vRegs );
if ( fReverse )
Vec_IntReverseOrder( vRegs );
// for ( Iter = 0; Iter < Gia_ManRegNum(p); Iter++ )
Vec_IntForEachEntry( vRegs, i, Iter )
{
// i = fReverse ? Gia_ManRegNum(p) - 1 - Iter : Iter;
if ( Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
continue;
Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
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 );
if ( status == l_Undef )
{
printf( "ICheck: Timeout reached after %d seconds. \n", nTimeOut );
RetValue = 1;
goto cleanup;
}
if ( status == l_True )
Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
else if ( status == l_False )
nLitsUsed--;
else assert( 0 );
// report the results
//printf( "Round %d: ", o );
if ( fVerbose )
{
printf( "I = %4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
i, (nFramesMax+1) * Gia_ManAndNum(pMiter),
Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
ABC_PRTr( "Time", Abc_Clock() - clkStart );
fflush( stdout );
}
}
// report the results
//printf( "Round %d: ", o );
if ( fVerbose )
{
printf( "M = %4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter),
Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
fflush( stdout );
}
cleanup:
// cleanup
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Gia_ManStop( pMiter );
Vec_IntFree( vRegs );
// Vec_IntFree( vLits );
return RetValue;
}
Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose )
{
Vec_Int_t * vLits, * vFlops;
int i, f;
if ( fVerbose )
printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops with %s %s flop order:\n",
Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p), fReverse ? "reverse":"direct", fBackTopo ? "backward":"natural" );
fflush( stdout );
// collect positive literals
vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
for ( i = 0; i < Gia_ManRegNum(p); i++ )
Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
for ( f = 1; f <= nFramesMax; f++ )
if ( Bmc_PerformISearchOne( p, f, nTimeOut, fReverse, fBackTopo, fVerbose, vLits ) )
{
Vec_IntFree( vLits );
return NULL;
}
// dump the numbers of the flops
if ( fDump )
{
int nLitsUsed = 0;
for ( i = 0; i < Gia_ManRegNum(p); i++ )
if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
nLitsUsed++;
printf( "The set contains %d (out of %d) next-state functions with 0-based numbers:\n", nLitsUsed, Gia_ManRegNum(p) );
for ( i = 0; i < Gia_ManRegNum(p); i++ )
if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
printf( "%d ", i );
printf( "\n" );
}
// save flop indexes
vFlops = Vec_IntAlloc( Gia_ManRegNum(p) );
for ( i = 0; i < Gia_ManRegNum(p); i++ )
if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
Vec_IntPush( vFlops, 1 );
else
Vec_IntPush( vFlops, 0 );
Vec_IntFree( vLits );
return vFlops;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END