/**CFile****************************************************************
FileName [bmcBmcAnd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis [Memory-efficient BMC engine]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bmcBmcAnd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bmc.h"
#include "aig/gia/giaAig.h"
#include "sat/bsat/satStore.h"
#include "sat/cnf/cnf.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Bmc_Mna_t_ Bmc_Mna_t;
struct Bmc_Mna_t_
{
Gia_Man_t * pFrames; // time frames
Cnf_Dat_t * pCnf; // CNF derived for the timeframes
Vec_Int_t * vPiMap; // maps unrolled GIA PIs into user GIA PIs
Vec_Int_t * vId2Var; // maps GIA IDs into SAT vars
Vec_Int_t * vInputs; // inputs of the cone
Vec_Int_t * vOutputs; // outputs of the cone
Vec_Int_t * vNodes; // internal nodes of the cone
sat_solver * pSat; // SAT solver
int nSatVars; // the counter of SAT variables
abctime clkStart; // starting time
};
static inline int Gia_ManTerSimInfoGet( unsigned * pInfo, int i )
{
return 3 & (pInfo[i >> 4] >> ((i & 15) << 1));
}
static inline void Gia_ManTerSimInfoSet( unsigned * pInfo, int i, int Value )
{
assert( Value >= GIA_ZER && Value <= GIA_UND );
Value ^= Gia_ManTerSimInfoGet( pInfo, i );
pInfo[i >> 4] ^= (Value << ((i & 15) << 1));
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs ternary simulation of the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Bmc_MnaTernary( Gia_Man_t * p, int nFrames, int nFramesAdd, int fVerbose, int * iFirst )
{
Vec_Ptr_t * vStates;
unsigned * pState;
int nStateWords = Abc_BitWordNum( 2*Gia_ManCoNum(p) );
Gia_Obj_t * pObj, * pObjRo;
int f, i, Count[4];
abctime clk = Abc_Clock();
Gia_ManConst0(p)->Value = GIA_ZER;
Gia_ManForEachPi( p, pObj, i )
pObj->Value = GIA_UND;
Gia_ManForEachRi( p, pObj, i )
pObj->Value = GIA_ZER;
*iFirst = -1;
vStates = Vec_PtrAlloc( 100 );
for ( f = 0; ; f++ )
{
// if frames are given, break at frames
if ( nFrames && f == nFrames )
break;
// if frames are not given, break after nFramesAdd from the first x-valued
if ( !nFrames && *iFirst >= 0 && f == *iFirst + nFramesAdd )
break;
// aassign CI values
Gia_ManForEachRiRo( p, pObj, pObjRo, i )
pObjRo->Value = pObj->Value;
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_XsimAndCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) );
// compute and save CO values
pState = ABC_ALLOC( unsigned, nStateWords );
Gia_ManForEachCo( p, pObj, i )
{
pObj->Value = Gia_XsimNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
Gia_ManTerSimInfoSet( pState, i, pObj->Value );
if ( *iFirst == -1 && i < Gia_ManPoNum(p) && pObj->Value == GIA_UND )
*iFirst = f;
}
Vec_PtrPush( vStates, pState );
// print statistics
if ( !fVerbose )
continue;
Count[0] = Count[1] = Count[2] = Count[3] = 0;
Gia_ManForEachRi( p, pObj, i )
Count[pObj->Value]++;
printf( "%5d : 0 =%7d 1 =%7d x =%7d all =%7d out = %s\n",
f, Count[GIA_ZER], Count[GIA_ONE], Count[GIA_UND], Gia_ManRegNum(p),
Gia_ManPo(p, 0)->Value == GIA_UND ? "x" : "0" );
}
// assert( Vec_PtrSize(vStates) == nFrames );
if ( fVerbose )
printf( "Finished %d frames. First x-valued PO is in frame %d. ", nFrames, *iFirst );
if ( fVerbose )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return vStates;
}
/**Function*************************************************************
Synopsis [Collect AIG nodes for the group of POs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bmc_MnaCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, unsigned * pState )
{
if ( pObj->fPhase )
return;
pObj->fPhase = 1;
if ( Gia_ObjIsAnd(pObj) )
{
Bmc_MnaCollect_rec( p, Gia_ObjFanin0(pObj), vNodes, pState );
Bmc_MnaCollect_rec( p, Gia_ObjFanin1(pObj), vNodes, pState );
pObj->Value = Gia_XsimAndCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) );
}
else if ( Gia_ObjIsRo(p, pObj) )
pObj->Value = pState ? Gia_ManTerSimInfoGet( pState, Gia_ObjCioId(Gia_ObjRoToRi(p, pObj)) ) : GIA_ZER;
else if ( Gia_ObjIsPi(p, pObj) )
pObj->Value = GIA_UND;
else assert( 0 );
Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
}
void Bmc_MnaCollect( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, unsigned * pState )
{
Gia_Obj_t * pObj;
int i;
Vec_IntClear( vNodes );
Gia_ManConst0(p)->fPhase = 1;
Gia_ManConst0(p)->Value = GIA_ZER;
Gia_ManForEachObjVec( vCos, p, pObj, i )
{
assert( Gia_ObjIsCo(pObj) );
Bmc_MnaCollect_rec( p, Gia_ObjFanin0(pObj), vNodes, pState );
pObj->Value = Gia_XsimNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
assert( pObj->Value == GIA_UND );
}
}
/**Function*************************************************************
Synopsis [Select related logic cones for the COs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bmc_MnaSelect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves )
{
if ( !pObj->fPhase )
return;
pObj->fPhase = 0;
assert( pObj->Value == GIA_UND );
if ( Gia_ObjIsAnd(pObj) )
{
if ( Gia_ObjFanin0(pObj)->Value == GIA_UND )
Bmc_MnaSelect_rec( p, Gia_ObjFanin0(pObj), vLeaves );
else assert( Gia_ObjFanin0(pObj)->Value + Gia_ObjFaninC0(pObj) == GIA_ONE );
if ( Gia_ObjFanin1(pObj)->Value == GIA_UND )
Bmc_MnaSelect_rec( p, Gia_ObjFanin1(pObj), vLeaves );
else assert( Gia_ObjFanin1(pObj)->Value + Gia_ObjFaninC1(pObj) == GIA_ONE );
}
else if ( Gia_ObjIsRo(p, pObj) )
Vec_IntPush( vLeaves, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
}
void Bmc_MnaSelect( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Vec_Int_t * vLeaves )
{
Gia_Obj_t * pObj;
int i;
Vec_IntClear( vLeaves );
Gia_ManForEachObjVec( vCos, p, pObj, i )
Bmc_MnaSelect_rec( p, Gia_ObjFanin0(pObj), vLeaves );
Gia_ManConst0(p)->fPhase = 0;
Gia_ManForEachObjVec( vNodes, p, pObj, i )
pObj->fPhase = 0;
}
/**Function*************************************************************
Synopsis [Build AIG for the selected cones.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bmc_MnaBuild_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew, Vec_Int_t * vMap, Vec_Int_t * vPiMap )
{
if ( !pObj->fPhase )
return;
pObj->fPhase = 0;
assert( pObj->Value == GIA_UND );
if ( Gia_ObjIsAnd(pObj) )
{
int iLit0 = 1, iLit1 = 1;
if ( Gia_ObjFanin0(pObj)->Value == GIA_UND )
Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap, vPiMap );
if ( Gia_ObjFanin1(pObj)->Value == GIA_UND )
Bmc_MnaBuild_rec( p, Gia_ObjFanin1(pObj), pNew, vMap, vPiMap );
if ( Gia_ObjFanin0(pObj)->Value == GIA_UND )
iLit0 = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) );
if ( Gia_ObjFanin1(pObj)->Value == GIA_UND )
iLit1 = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId1p(p, pObj)), Gia_ObjFaninC1(pObj) );
Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), Gia_ManHashAnd(pNew, iLit0, iLit1) );
}
else if ( Gia_ObjIsRo(p, pObj) )
assert( Vec_IntEntry(vMap, Gia_ObjId(p, pObj)) != -1 );
else if ( Gia_ObjIsPi(p, pObj) )
{
Vec_IntPush( vPiMap, Gia_ObjCioId(pObj) );
Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) );
}
else assert( 0 );
}
void Bmc_MnaBuild( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Gia_Man_t * pNew, Vec_Int_t * vMap, Vec_Int_t * vPiMap )
{
Gia_Obj_t * pObj;
int i, iLit;
Gia_ManForEachObjVec( vCos, p, pObj, i )
{
assert( Gia_ObjIsCo(pObj) );
Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap, vPiMap );
iLit = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) );
Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), iLit );
}
Gia_ManConst0(p)->fPhase = 0;
Gia_ManForEachObjVec( vNodes, p, pObj, i )
pObj->fPhase = 0;
}
/**Function*************************************************************
Synopsis [Compute the first non-trivial timeframe.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManBmcUnroll( Gia_Man_t * pGia, int nFramesMax, int nFramesAdd, int fVerbose, Vec_Int_t ** pvPiMap )
{
Gia_Obj_t * pObj;
Gia_Man_t * pNew, * pTemp;
Vec_Ptr_t * vStates, * vBegins;
Vec_Int_t * vRoots, * vCone, * vLeaves, * vMap;
unsigned * pStateF, * pStateP;
int f, i, iFirst;
Gia_ManCleanPhase( pGia );
vCone = Vec_IntAlloc( 1000 );
vLeaves = Vec_IntAlloc( 1000 );
// perform ternary simulation
vStates = Bmc_MnaTernary( pGia, nFramesMax, nFramesAdd, fVerbose, &iFirst );
// go backward
*pvPiMap = Vec_IntAlloc( 1000 );
vBegins = Vec_PtrStart( Vec_PtrSize(vStates) );
for ( f = Vec_PtrSize(vStates) - 1; f >= 0; f-- )
{
// get ternary states
pStateF = (unsigned *)Vec_PtrEntry(vStates, f);
pStateP = f ? (unsigned *)Vec_PtrEntry(vStates, f-1) : 0;
// collect roots of this frame
vRoots = Vec_IntAlloc( 100 );
Gia_ManForEachPo( pGia, pObj, i )
if ( Gia_ManTerSimInfoGet( pStateF, Gia_ObjCioId(pObj) ) == GIA_UND )
Vec_IntPush( vRoots, Gia_ObjId(pGia, pObj) );
// add leaves from the previous frame
Vec_IntAppend( vRoots, vLeaves );
Vec_PtrWriteEntry( vBegins, f, vRoots );
// find the cone
Bmc_MnaCollect( pGia, vRoots, vCone, pStateP ); // computes vCone
Bmc_MnaSelect( pGia, vRoots, vCone, vLeaves ); // computes vLeaves
if ( fVerbose )
printf( "Frame %4d : Roots = %6d Leaves = %6d Cone = %6d\n",
f, Vec_IntSize(vRoots), Vec_IntSize(vLeaves), Vec_IntSize(vCone) );
if ( Vec_IntSize(vLeaves) == 0 )
break;
// it is possible that some of the POs are still ternary...
}
assert( f >= 0 );
// go forward
vMap = Vec_IntStartFull( Gia_ManObjNum(pGia) );
pNew = Gia_ManStart( 10000 );
pNew->pName = Abc_UtilStrsav( pGia->pName );
Gia_ManHashStart( pNew );
for ( f = 0; f < Vec_PtrSize(vStates); f++ )
{
vRoots = (Vec_Int_t *)Vec_PtrEntry( vBegins, f );
if ( vRoots == NULL )
{
Gia_ManForEachPo( pGia, pObj, i )
Gia_ManAppendCo( pNew, 0 );
continue;
}
// get ternary states
pStateF = (unsigned *)Vec_PtrEntry(vStates, f);
pStateP = f ? (unsigned *)Vec_PtrEntry(vStates, f-1) : 0;
// clean POs
Gia_ManForEachPo( pGia, pObj, i )
Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pObj), 0 );
// find the cone
Vec_IntPush( *pvPiMap, -f-1 );
Bmc_MnaCollect( pGia, vRoots, vCone, pStateP ); // computes vCone
Bmc_MnaBuild( pGia, vRoots, vCone, pNew, vMap, *pvPiMap ); // computes pNew
if ( fVerbose )
printf( "Frame %4d : Roots = %6d Leaves = %6d Cone = %6d\n",
f, Vec_IntSize(vRoots), Vec_IntSize(vLeaves), Vec_IntSize(vCone) );
// create POs
Gia_ManForEachPo( pGia, pObj, i )
Gia_ManAppendCo( pNew, Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) );
// set a new map
Gia_ManForEachObjVec( vRoots, pGia, pObj, i )
if ( Gia_ObjIsRi(pGia, pObj) )
Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, Gia_ObjRiToRo(pGia, pObj)), Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) );
// else if ( Gia_ObjIsPo(pGia, pObj) )
// Gia_ManAppendCo( pNew, Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) );
// else assert( 0 );
}
Gia_ManHashStop( pNew );
Vec_VecFree( (Vec_Vec_t *)vBegins );
Vec_PtrFreeFree( vStates );
Vec_IntFree( vLeaves );
Vec_IntFree( vCone );
Vec_IntFree( vMap );
// cleanup
// Gia_ManPrintStats( pNew, NULL );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
// Gia_ManPrintStats( pNew, NULL );
return pNew;
}
/**Function*************************************************************
Synopsis [BMC manager manipulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Bmc_Mna_t * Bmc_MnaAlloc()
{
Bmc_Mna_t * p;
p = ABC_CALLOC( Bmc_Mna_t, 1 );
p->vId2Var = Vec_IntAlloc( 0 );
p->vInputs = Vec_IntAlloc( 1000 );
p->vOutputs = Vec_IntAlloc( 1000 );
p->vNodes = Vec_IntAlloc( 10000 );
p->pSat = sat_solver_new();
p->nSatVars = 1;
p->clkStart = Abc_Clock();
sat_solver_setnvars( p->pSat, 1000 );
return p;
}
void Bmc_MnaFree( Bmc_Mna_t * p )
{
Cnf_DataFree( p->pCnf );
Vec_IntFreeP( &p->vPiMap );
Vec_IntFreeP( &p->vId2Var );
Vec_IntFreeP( &p->vInputs );
Vec_IntFreeP( &p->vOutputs );
Vec_IntFreeP( &p->vNodes );
sat_solver_delete( p->pSat );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Derives GIA for the given cone.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManBmcDupCone( Gia_Man_t * p, Vec_Int_t * vIns, Vec_Int_t * vNodes, Vec_Int_t * vOuts )
{
Gia_Man_t * pNew;
Vec_Int_t * vTempIn, * vTempNode;
Gia_Obj_t * pObj;
int i;
// save values
vTempIn = Vec_IntAlloc( Vec_IntSize(vIns) );
Gia_ManForEachObjVec( vIns, p, pObj, i )
Vec_IntPush( vTempIn, pObj->Value );
// save values
vTempNode = Vec_IntAlloc( Vec_IntSize(vNodes) );
Gia_ManForEachObjVec( vNodes, p, pObj, i )
Vec_IntPush( vTempNode, pObj->Value );
// derive new GIA
pNew = Gia_ManDupFromVecs( p, vIns, vNodes, vOuts, 0 );
// reset values
Gia_ManForEachObjVec( vIns, p, pObj, i )
pObj->Value = Vec_IntEntry( vTempIn, i );
// reset values
Gia_ManForEachObjVec( vNodes, p, pObj, i )
pObj->Value = Vec_IntEntry( vTempNode, i );
// reset values
Gia_ManForEachObjVec( vOuts, p, pObj, i )
pObj->Value = 0;
Vec_IntFree( vTempIn );
Vec_IntFree( vTempNode );
return pNew;
}
/**Function*************************************************************
Synopsis [Derives GIA for the given cone.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManBmcAssignVarIds( Bmc_Mna_t * p, Vec_Int_t * vIns, Vec_Int_t * vUsed, Vec_Int_t * vOuts )
{
int i, iObj, VarC0 = p->nSatVars++;
Vec_IntForEachEntry( vIns, iObj, i )
if ( Vec_IntEntry( p->vId2Var, iObj ) == 0 )
Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
Vec_IntForEachEntryReverse( vUsed, iObj, i )
{
assert( Vec_IntEntry( p->vId2Var, iObj ) == 0 );
Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
}
Vec_IntForEachEntry( vOuts, iObj, i )
{
assert( Vec_IntEntry( p->vId2Var, iObj ) == 0 );
Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
}
// extend the SAT solver
if ( p->nSatVars > sat_solver_nvars(p->pSat) )
sat_solver_setnvars( p->pSat, p->nSatVars );
return VarC0;
}
/**Function*************************************************************
Synopsis [Derives CNF for the given cone.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManBmcAddCnf( Bmc_Mna_t * p, Gia_Man_t * pGia, Vec_Int_t * vIns, Vec_Int_t * vNodes, Vec_Int_t * vOuts )
{
Gia_Man_t * pNew = Gia_ManBmcDupCone( pGia, vIns, vNodes, vOuts );
Aig_Man_t * pAig = Gia_ManToAigSimple( pNew );
Cnf_Dat_t * pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
Vec_Int_t * vUsed, * vMap;
Gia_Obj_t * pObj;
int i, iObj, VarC0;
// collect used variables
vUsed = Vec_IntAlloc( pCnf->nVars - Vec_IntSize(vIns) - Vec_IntSize(vOuts) );
Gia_ManForEachAnd( pNew, pObj, i )
if ( pCnf->pVarNums[i] >= 0 )
Vec_IntPush( vUsed, Vec_IntEntry(vNodes, i - Vec_IntSize(vIns) - 1) );
// assign variable IDs
VarC0 = Gia_ManBmcAssignVarIds( p, vIns, vUsed, vOuts );
Vec_IntFree( vUsed );
// create variable map from CNF vars into SAT vars
vMap = Vec_IntStartFull( pCnf->nVars );
assert( pCnf->pVarNums[0] > 0 );
Vec_IntWriteEntry( vMap, pCnf->pVarNums[0], VarC0 );
Gia_ManForEachObj1( pNew, pObj, i )
{
if ( pCnf->pVarNums[i] < 0 )
continue;
assert( pCnf->pVarNums[i] >= 0 && pCnf->pVarNums[i] < pCnf->nVars );
if ( Gia_ObjIsCi(pObj) )
iObj = Vec_IntEntry( vIns, i - 1 );
else if ( Gia_ObjIsAnd(pObj) )
iObj = Vec_IntEntry( vNodes, i - Vec_IntSize(vIns) - 1 );
else if ( Gia_ObjIsCo(pObj) )
iObj = Vec_IntEntry( vOuts, i - Vec_IntSize(vIns) - Vec_IntSize(vNodes) - 1 );
else assert( 0 );
assert( Vec_IntEntry(p->vId2Var, iObj) > 0 );
Vec_IntWriteEntry( vMap, pCnf->pVarNums[i], Vec_IntEntry(p->vId2Var, iObj) );
}
//Vec_IntPrint( vMap );
// remap CNF
for ( i = 0; i < pCnf->nLiterals; i++ )
{
assert( pCnf->pClauses[0][i] > 1 && pCnf->pClauses[0][i] < 2 * pCnf->nVars );
pCnf->pClauses[0][i] = Abc_Lit2LitV( Vec_IntArray(vMap), pCnf->pClauses[0][i] );
}
Vec_IntFree( vMap );
// add clauses
for ( i = 0; i < pCnf->nClauses; i++ )
{
/*
int v;
for ( v = 0; v < pCnf->pClauses[i+1] - pCnf->pClauses[i]; v++ )
printf( "%d ", pCnf->pClauses[i][v] );
printf( "\n" );
*/
if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
break;
}
if ( i < pCnf->nClauses )
printf( "SAT solver became UNSAT after adding clauses.\n" );
Aig_ManStop( pAig );
Cnf_DataFree( pCnf );
Gia_ManStop( pNew );
}
/**Function*************************************************************
Synopsis [Collects new nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManBmcAddCone_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
{
int iObj;
if ( pObj->fMark0 )
return;
pObj->fMark0 = 1;
iObj = Gia_ObjId( p->pFrames, pObj );
if ( Gia_ObjIsAnd(pObj) && Vec_IntEntry(p->vId2Var, iObj) == 0 )
{
Gia_ManBmcAddCone_rec( p, Gia_ObjFanin0(pObj) );
Gia_ManBmcAddCone_rec( p, Gia_ObjFanin1(pObj) );
Vec_IntPush( p->vNodes, iObj );
}
else
Vec_IntPush( p->vInputs, iObj );
}
void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart, int iStop )
{
Gia_Obj_t * pObj;
int i;
Vec_IntClear( p->vNodes );
Vec_IntClear( p->vInputs );
Vec_IntClear( p->vOutputs );
Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
for ( i = iStart; i < iStop; i++ )
{
pObj = Gia_ManPo(p->pFrames, i);
if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
continue;
Gia_ManBmcAddCone_rec( p, Gia_ObjFanin0(pObj) );
Vec_IntPush( p->vOutputs, Gia_ObjId(p->pFrames, pObj) );
}
// clean attributes and create new variables
Gia_ManForEachObjVec( p->vNodes, p->pFrames, pObj, i )
pObj->fMark0 = 0;
Gia_ManForEachObjVec( p->vInputs, p->pFrames, pObj, i )
pObj->fMark0 = 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart, int iStop )
{
int i;
for ( i = iStart; i < iStop; i++ )
if ( Gia_ObjChild0(Gia_ManPo(pFrames, i)) != Gia_ManConst0(pFrames) )
return 0;
return 1;
}
int Gia_ManBmcFindFirst( Gia_Man_t * pFrames )
{
Gia_Obj_t * pObj;
int i;
Gia_ManForEachPo( pFrames, pObj, i )
if ( Gia_ObjChild0(pObj) != Gia_ManConst0(pFrames) )
return i;
return -1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
Unr_Man_t * pUnroll;
Bmc_Mna_t * p;
int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
int f, i=0, Lit, status, RetValue = -2;
p = Bmc_MnaAlloc();
pUnroll = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose );
for ( f = 0; f < nFramesMax; f++ )
{
p->pFrames = Unr_ManUnrollFrame( pUnroll, f );
if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
{
// create another slice
Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
// create CNF in the SAT solver
Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs );
// try solving the outputs
for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
{
Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i);
if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
continue;
Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 );
status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_False ) // unsat
continue;
if ( status == l_True ) // sat
RetValue = 0;
if ( status == l_Undef ) // undecided
RetValue = -1;
break;
}
}
// report statistics
if ( pPars->fVerbose )
{
printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f MB ",
f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames),
p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes),
sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
}
if ( RetValue != -2 )
{
if ( RetValue == -1 )
printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f );
else
{
printf( "Output %d of miter \"%s\" was asserted in frame %d. ",
i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
}
break;
}
}
if ( RetValue == -2 )
RetValue = -1;
// dump unfolded frames
if ( pPars->fDumpFrames )
{
p->pFrames = Gia_ManCleanup( p->pFrames );
Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
Gia_ManStop( p->pFrames );
}
// cleanup
Unr_ManFree( pUnroll );
Bmc_MnaFree( p );
return RetValue;
}
/**Function*************************************************************
Synopsis [Generate counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Gia_ManBmcCexGen( Bmc_Mna_t * pMan, Gia_Man_t * p, int iOut )
{
Abc_Cex_t * pCex;
int i, iObjId, iSatVar, iOrigPi;
int iFramePi = 0, iFrame = -1;
pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), iOut / Gia_ManPoNum(p) + 1 );
pCex->iFrame = iOut / Gia_ManPoNum(p);
pCex->iPo = iOut % Gia_ManPoNum(p);
// fill in the input values
Vec_IntForEachEntry( pMan->vPiMap, iOrigPi, i )
{
if ( iOrigPi < 0 )
{
iFrame = -iOrigPi-1;
continue;
}
// iOrigPi in iFrame of pGia has PI index iFramePi in pMan->pFrames,
iObjId = Gia_ObjId( pMan->pFrames, Gia_ManPi(pMan->pFrames, iFramePi) );
iSatVar = Vec_IntEntry( pMan->vId2Var, iObjId );
if ( sat_solver_var_value(pMan->pSat, iSatVar) )
Abc_InfoSetBit( pCex->pData, Gia_ManRegNum(p) + Gia_ManPiNum(p) * iFrame + iOrigPi );
iFramePi++;
}
assert( iFramePi == Gia_ManPiNum(pMan->pFrames) );
return pCex;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
Bmc_Mna_t * p;
int nFramesMax, f, i=0, Lit, status, RetValue = -2;
abctime clk = Abc_Clock();
p = Bmc_MnaAlloc();
p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
if ( pPars->fVerbose )
{
printf( "Unfolding for %d frames with first non-trivial PO %d. ", nFramesMax, Gia_ManBmcFindFirst(p->pFrames) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
if ( pPars->fUseSynth )
{
Gia_Man_t * pTemp = p->pFrames;
p->pFrames = Gia_ManAigSyn2( pTemp, pPars->fVerbose, 0 );
Gia_ManStop( pTemp );
}
else if ( pPars->fVerbose )
Gia_ManPrintStats( p->pFrames, NULL );
if ( pPars->fDumpFrames )
{
Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
}
for ( f = 0; f < nFramesMax; f++ )
{
if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
{
// create another slice
Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
// create CNF in the SAT solver
Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs );
// try solving the outputs
for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
{
Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i);
if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
continue;
Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 );
status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_False ) // unsat
continue;
if ( status == l_True ) // sat
RetValue = 0;
if ( status == l_Undef ) // undecided
RetValue = -1;
break;
}
// report statistics
if ( pPars->fVerbose )
{
printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f MB ",
f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames),
p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes),
sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
}
}
if ( RetValue != -2 )
{
if ( RetValue == -1 )
printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f );
else
{
ABC_FREE( pGia->pCexSeq );
pGia->pCexSeq = Gia_ManBmcCexGen( p, pGia, i );
printf( "Output %d of miter \"%s\" was asserted in frame %d. ",
i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
}
break;
}
pPars->iFrame = f;
}
if ( RetValue == -2 )
RetValue = -1;
// cleanup
Gia_ManStop( p->pFrames );
Bmc_MnaFree( p );
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManBmcAddCnfNew_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
{
int iObj = Gia_ObjId( p->pFrames, pObj );
if ( Gia_ObjIsAnd(pObj) && p->pCnf->pObj2Count[iObj] == -1 )
{
Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) );
Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) );
return;
}
if ( Vec_IntEntry(p->vId2Var, iObj) > 0 )
return;
Vec_IntWriteEntry(p->vId2Var, iObj, p->nSatVars++);
if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsPo(p->pFrames, pObj) )
{
int i, nClas, iCla;
Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) );
if ( Gia_ObjIsAnd(pObj) )
Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) );
// extend the SAT solver
if ( p->nSatVars > sat_solver_nvars(p->pSat) )
sat_solver_setnvars( p->pSat, p->nSatVars );
// add clauses
nClas = p->pCnf->pObj2Count[iObj];
iCla = p->pCnf->pObj2Clause[iObj];
for ( i = 0; i < nClas; i++ )
{
int nLits, pLits[8];
int * pClauseThis = p->pCnf->pClauses[iCla+i];
int * pClauseNext = p->pCnf->pClauses[iCla+i+1];
for ( nLits = 0; pClauseThis + nLits < pClauseNext; nLits++ )
{
if ( pClauseThis[nLits] < 2 )
printf( "\n\n\nError in CNF generation: Constant literal!\n\n\n" );
assert( pClauseThis[nLits] > 1 && pClauseThis[nLits] < 2*Gia_ManObjNum(p->pFrames) );
pLits[nLits] = Abc_Lit2LitV( Vec_IntArray(p->vId2Var), pClauseThis[nLits] );
}
assert( nLits < 8 );
if ( !sat_solver_addclause( p->pSat, pLits, pLits + nLits ) )
break;
}
if ( i < nClas )
printf( "SAT solver became UNSAT after adding clauses.\n" );
}
else assert( Gia_ObjIsCi(pObj) );
}
void Gia_ManBmcAddCnfNew( Bmc_Mna_t * p, int iStart, int iStop )
{
Gia_Obj_t * pObj;
int i;
for ( i = iStart; i < iStop; i++ )
{
pObj = Gia_ManPo(p->pFrames, i);
if ( Gia_ObjFanin0(pObj) == Gia_ManConst0(p->pFrames) )
continue;
Gia_ManBmcAddCnfNew_rec( p, pObj );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Cnf_Dat_t * Cnf_DeriveGia( Gia_Man_t * p )
{
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
Cnf_Dat_t * pCnf = Cnf_DeriveOther( pAig, 1 );
Aig_ManStop( pAig );
return pCnf;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
Bmc_Mna_t * p;
Gia_Man_t * pTemp;
int nFramesMax, f, i=0, Lit = 1, status, RetValue = -2;
abctime clk = Abc_Clock();
p = Bmc_MnaAlloc();
sat_solver_set_runtime_limit( p->pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
if ( pPars->fVerbose )
{
printf( "Unfolding for %d frames with first non-trivial PO %d. ", nFramesMax, Gia_ManBmcFindFirst(p->pFrames) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
if ( pPars->fUseSynth )
{
p->pFrames = Gia_ManAigSyn2( pTemp = p->pFrames, pPars->fVerbose, 0 ); Gia_ManStop( pTemp );
}
else if ( pPars->fVerbose )
Gia_ManPrintStats( p->pFrames, NULL );
if ( pPars->fDumpFrames )
{
Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
}
if ( pPars->fUseOldCnf )
p->pCnf = Cnf_DeriveGia( p->pFrames );
else
{
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 );
// create clauses for constant node
// sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
for ( f = 0; f < nFramesMax; f++ )
{
if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
{
// create another slice
Gia_ManBmcAddCnfNew( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
// try solving the outputs
for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
{
Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i);
if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
continue;
if ( Gia_ObjChild0(pObj) == Gia_ManConst1(p->pFrames) )
{
printf( "Output %d is trivially SAT.\n", i );
continue;
}
Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 );
status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_False ) // unsat
continue;
if ( status == l_True ) // sat
RetValue = 0;
if ( status == l_Undef ) // undecided
RetValue = -1;
break;
}
// report statistics
if ( pPars->fVerbose )
{
printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f MB ",
f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames),
p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes),
sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
}
}
if ( RetValue != -2 )
{
if ( RetValue == -1 )
printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f );
else
{
ABC_FREE( pGia->pCexSeq );
pGia->pCexSeq = Gia_ManBmcCexGen( p, pGia, i );
printf( "Output %d of miter \"%s\" was asserted in frame %d. ",
i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
}
break;
}
pPars->iFrame = f;
}
if ( RetValue == -2 )
RetValue = -1;
// cleanup
Gia_ManStop( p->pFrames );
Bmc_MnaFree( p );
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
abctime TimeToStop = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() : 0;
if ( pPars->nFramesAdd == 0 )
return Gia_ManBmcPerformInt( pGia, pPars );
// iterate over the engine until we read the global timeout
assert( pPars->nTimeOut >= 0 );
while ( 1 )
{
if ( TimeToStop && TimeToStop < Abc_Clock() )
return -1;
if ( Gia_ManBmcPerformInt( pGia, pPars ) == 0 )
return 0;
// set the new runtime limit
if ( pPars->nTimeOut )
{
pPars->nTimeOut = Abc_MinInt( pPars->nTimeOut-1, (int)((TimeToStop - Abc_Clock()) / CLOCKS_PER_SEC) );
if ( pPars->nTimeOut <= 0 )
return -1;
}
else
return -1;
// set the new frames limit
pPars->nFramesAdd *= 2;
}
return -1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END