Skip to content

A
abc
Commit 0e256dc2 by Alan Mishchenko
Options

Updates for the new BMC engine.

parent 8430b6da
Showing with 644 additions and 11 deletions
abclib.dsp
......@@ -2779,6 +2779,10 @@ SOURCE=.\src\misc\vec\vecHsh.h
# End Source File
# Begin Source File
SOURCE=.\src\misc\vec\vecHsh4.h
# End Source File
# Begin Source File
SOURCE=.\src\misc\vec\vecInt.h
# End Source File
# Begin Source File
......
src/base/abci/abc.c
......@@ -31781,6 +31781,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
memset( pPars, 0, sizeof(Bmc_AndPar_t) );
pPars->nStart = 0; // starting timeframe
pPars->nFramesMax = 0; // maximum number of timeframes
pPars->nFramesAdd = 50; // the number of additional frames
pPars->nConfLimit = 0; // maximum number of conflicts at a node
pPars->fLoadCnf = 0; // dynamic CNF loading
pPars->fDumpFrames = 0; // dump unrolled timeframes
......@@ -31791,7 +31792,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nFailOuts = 0; // the number of failed outputs
pPars->nDropOuts = 0; // the number of dropped outputs
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFcdvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFAcdvwh" ) ) != EOF )
{
switch ( c )
{
......@@ -31817,6 +31818,17 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nFramesMax < 0 )
goto usage;
break;
case 'A':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesAdd = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesAdd < 0 )
goto usage;
break;
case 'c':
pPars->fLoadCnf ^= 1;
break;
......@@ -31844,10 +31856,11 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &bmc [-SF num] [-cdvwh]\n" );
Abc_Print( -2, "usage: &bmc [-SFA num] [-cdvwh]\n" );
Abc_Print( -2, "\t performs bounded model checking\n" );
Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n", pPars->nFramesAdd );
Abc_Print( -2, "\t-c : toggle dynamic CNF loading [default = %s]\n", pPars->fLoadCnf? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping unfolded timeframes [default = %s]\n", pPars->fDumpFrames? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
src/misc/vec/vecHsh4.h 0 → 100644
/**CFile****************************************************************
FileName [vecHsh4.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resizable arrays.]
Synopsis [Hashing pairs of integers into an integer.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: vecHsh4.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__misc__vec__vecHsh4_h
#define ABC__misc__vec__vecHsh4_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Hsh_Int4Obj_t_ Hsh_Int4Obj_t;
struct Hsh_Int4Obj_t_
{
int iData0;
int iData1;
int iRes;
int iNext;
};
typedef struct Hsh_Int4Man_t_ Hsh_Int4Man_t;
struct Hsh_Int4Man_t_
{
Vec_Int_t * vTable; // hash table
Vec_Int_t * vObjs; // hash objects
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline Hsh_Int4Obj_t * Hsh_Int4Obj( Hsh_Int4Man_t * p, int iObj ) { return iObj ? (Hsh_Int4Obj_t *)Vec_IntEntryP(p->vObjs, 4*iObj) : NULL; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Hashing data entries composed of nSize integers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Hsh_Int4Man_t * Hsh_Int4ManStart( int nSize )
{
Hsh_Int4Man_t * p; nSize += 100;
p = ABC_CALLOC( Hsh_Int4Man_t, 1 );
p->vTable = Vec_IntStart( Abc_PrimeCudd(nSize) );
p->vObjs = Vec_IntAlloc( 4*nSize );
Vec_IntFill( p->vObjs, 4, 0 );
return p;
}
static inline void Hsh_Int4ManStop( Hsh_Int4Man_t * p )
{
Vec_IntFree( p->vObjs );
Vec_IntFree( p->vTable );
ABC_FREE( p );
}
static inline int Hsh_Int4ManEntryNum( Hsh_Int4Man_t * p )
{
return Vec_IntSize(p->vObjs)/4 - 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Hsh_Int4ManHash( int iData0, int iData1, int nTableSize )
{
return (4177 * iData0 + 7873 * iData1) % nTableSize;
}
static inline int * Hsh_Int4ManLookup( Hsh_Int4Man_t * p, int iData0, int iData1 )
{
Hsh_Int4Obj_t * pObj;
int * pPlace = Vec_IntEntryP( p->vTable, Hsh_Int4ManHash(iData0, iData1, Vec_IntSize(p->vTable)) );
for ( ; (pObj = Hsh_Int4Obj(p, *pPlace)); pPlace = &pObj->iNext )
if ( pObj->iData0 == iData0 && pObj->iData1 == iData1 )
return pPlace;
assert( *pPlace == 0 );
return pPlace;
}
static inline int Hsh_Int4ManFind( Hsh_Int4Man_t * p, int iData0, int iData1 )
{
Hsh_Int4Obj_t * pObj;
int * pPlace = Vec_IntEntryP( p->vTable, Hsh_Int4ManHash(iData0, iData1, Vec_IntSize(p->vTable)) );
for ( ; (pObj = Hsh_Int4Obj(p, *pPlace)); pPlace = &pObj->iNext )
if ( pObj->iData0 == iData0 && pObj->iData1 == iData1 )
return pObj->iRes;
assert( *pPlace == 0 );
return -1;
}
static inline int Hsh_Int4ManInsert( Hsh_Int4Man_t * p, int iData0, int iData1, int iRes )
{
Hsh_Int4Obj_t * pObj;
int i, nObjs, * pPlace;
nObjs = Vec_IntSize(p->vObjs)/4;
if ( nObjs > Vec_IntSize(p->vTable) )
{
Vec_IntFill( p->vTable, Abc_PrimeCudd(2*Vec_IntSize(p->vTable)), 0 );
for ( i = 1; i < nObjs; i++ )
{
pObj = Hsh_Int4Obj( p, i );
pObj->iNext = 0;
pPlace = Hsh_Int4ManLookup( p, pObj->iData0, pObj->iData1 );
assert( *pPlace == 0 );
*pPlace = i;
}
}
pPlace = Hsh_Int4ManLookup( p, iData0, iData1 );
if ( *pPlace )
return 0;
assert( *pPlace == 0 );
*pPlace = nObjs;
Vec_IntPush( p->vObjs, iData0 );
Vec_IntPush( p->vObjs, iData1 );
Vec_IntPush( p->vObjs, iRes );
Vec_IntPush( p->vObjs, 0 );
return 1;
}
/**Function*************************************************************
Synopsis [Test procedure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Hsh_Int4ManHashArrayTest()
{
Hsh_Int4Man_t * p;
int RetValue;
p = Hsh_Int4ManStart( 10 );
RetValue = Hsh_Int4ManInsert( p, 10, 11, 12 );
assert( RetValue );
RetValue = Hsh_Int4ManInsert( p, 20, 21, 22 );
assert( RetValue );
RetValue = Hsh_Int4ManInsert( p, 10, 11, 12 );
assert( !RetValue );
RetValue = Hsh_Int4ManFind( p, 20, 21 );
assert( RetValue == 22 );
RetValue = Hsh_Int4ManFind( p, 20, 22 );
assert( RetValue == -1 );
Hsh_Int4ManStop( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_END
#endif
src/sat/bmc/bmc.h
......@@ -77,6 +77,7 @@ struct Bmc_AndPar_t_
{
int nStart; // starting timeframe
int nFramesMax; // maximum number of timeframes
int nFramesAdd; // the number of additional frames
int nConfLimit; // maximum number of conflicts at a node
int fLoadCnf; // dynamic CNF loading
int fDumpFrames; // dump unrolled timeframes
......
src/sat/bmc/bmcBmcAnd.c
......@@ -43,12 +43,333 @@ struct Bmc_Mna_t_
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 )
{
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 );
if ( Gia_ObjFanin1(pObj)->Value == GIA_UND )
Bmc_MnaBuild_rec( p, Gia_ObjFanin1(pObj), pNew, vMap );
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_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 )
{
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 );
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 )
{
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
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
Bmc_MnaCollect( pGia, vRoots, vCone, pStateP ); // computes vCone
Bmc_MnaBuild( pGia, vRoots, vCone, pNew, vMap ); // 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 []
......@@ -255,7 +576,7 @@ void Gia_ManBmcAddCone_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
else
Vec_IntPush( p->vInputs, iObj );
}
void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart )
void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart, int iStop )
{
Gia_Obj_t * pObj;
int i;
......@@ -263,7 +584,7 @@ void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart )
Vec_IntClear( p->vInputs );
Vec_IntClear( p->vOutputs );
Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
for ( i = iStart; i < Gia_ManPoNum(p->pFrames); i++ )
for ( i = iStart; i < iStop; i++ )
{
pObj = Gia_ManPo(p->pFrames, i);
if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
......@@ -289,10 +610,10 @@ void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart )
SeeAlso []
***********************************************************************/
int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart )
int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart, int iStop )
{
int i;
for ( i = iStart; i < Gia_ManPoNum(pFrames); i++ )
for ( i = iStart; i < iStop; i++ )
if ( Gia_ObjChild0(Gia_ManPo(pFrames, i)) != Gia_ManConst0(pFrames) )
return 0;
return 1;
......@@ -309,24 +630,25 @@ int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart )
SeeAlso []
***********************************************************************/
int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
Unr_Man_t * pUnroll;
Bmc_Mna_t * p = Bmc_MnaAlloc();
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) ) )
if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
{
// create another slice
Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia) );
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 < Gia_ManPoNum(p->pFrames); i++ )
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) )
......@@ -380,6 +702,91 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
Bmc_Mna_t * p;
int nFramesMax, f, i=0, Lit, status, RetValue = -2;
p = Bmc_MnaAlloc();
p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose );
nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
if ( pPars->fVerbose )
printf( "Performed unfolding for %d frames.\n", nFramesMax );
if ( pPars->fVerbose )
Gia_ManPrintStats( p->pFrames, NULL );
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
{
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
Gia_ManStop( p->pFrames );
Bmc_MnaFree( p );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
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