luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Reducing memory usage in bmc2 and bmc3.

This commit is contained in:
Alan Mishchenko 2012-07-01 02:19:19 -07:00
parent a4908534f1
commit d3c018cd23
5 changed files with 229 additions and 179 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/aig/gia/gia.h
View File

@ -739,6 +739,7 @@ extern void Gia_ManUnrollStop( void * pMan );
extern int Gia_ManUnrollLastLit( void * pMan );
extern void Gia_ManFraSetDefaultParams( Gia_ParFra_t * p );
extern Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars );
extern Gia_Man_t * Gia_ManFramesInitSpecial( Gia_Man_t * pAig, int nFrames, int fVerbose );
/*=== giaFront.c ==========================================================*/
extern Gia_Man_t * Gia_ManFront( Gia_Man_t * p );
extern void Gia_ManFrontTest( Gia_Man_t * p );

60
src/aig/gia/giaFrames.c
View File

@ -915,6 +915,66 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
return pFrames;
}
/**Function*************************************************************
Synopsis [Perform init unrolling as long as PO(s) are constant 0.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManFramesInitSpecial( Gia_Man_t * pAig, int nFrames, int fVerbose )
{
Gia_Man_t * pFrames, * pTemp;
Gia_Obj_t * pObj;
int i, f;
assert( Gia_ManRegNum(pAig) > 0 );
if ( nFrames > 0 )
printf( "Computing specialized unrolling with %d frames...\n", nFrames );
pFrames = Gia_ManStart( Gia_ManObjNum(pAig) );
pFrames->pName = Abc_UtilStrsav( pAig->pName );
Gia_ManHashAlloc( pFrames );
Gia_ManConst0(pAig)->Value = 0;
for ( f = 0; nFrames == 0 || f < nFrames; f++ )
{
if ( fVerbose && (f % 100 == 0) )
{
printf( "%6d : ", f );
Gia_ManPrintStats( pFrames, 0, 0 );
}
Gia_ManForEachRo( pAig, pObj, i )
pObj->Value = f ? Gia_ObjRoToRi( pAig, pObj )->Value : 0;
Gia_ManForEachPi( pAig, pObj, i )
pObj->Value = Gia_ManAppendCi( pFrames );
Gia_ManForEachAnd( pAig, pObj, i )
pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachPo( pAig, pObj, i )
if ( Gia_ObjFanin0Copy(pObj) != 0 )
break;
if ( i < Gia_ManPoNum(pAig) )
break;
Gia_ManForEachRi( pAig, pObj, i )
pObj->Value = Gia_ObjFanin0Copy(pObj);
}
if ( fVerbose )
printf( "Computed prefix of %d frames.\n", f );
Gia_ManForEachRi( pAig, pObj, i )
Gia_ManAppendCo( pFrames, pObj->Value );
Gia_ManHashStop( pFrames );
pFrames = Gia_ManCleanup( pTemp = pFrames );
if ( fVerbose )
printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n",
Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) );
Gia_ManStop( pTemp );
return pFrames;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

122
src/aig/saig/saigBmc2.c
View File

@ -25,12 +25,11 @@
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define AIG_VISITED ((Aig_Obj_t *)(ABC_PTRUINT_T)1)
//#define AIG_VISITED ((Aig_Obj_t *)(ABC_PTRUINT_T)1)
typedef struct Saig_Bmc_t_ Saig_Bmc_t;
struct Saig_Bmc_t_
@ -44,11 +43,10 @@ struct Saig_Bmc_t_
// AIG managers
Aig_Man_t * pAig; // the user's AIG manager
Aig_Man_t * pFrm; // Frames manager
Vec_Ptr_t * vVisited; // nodes visited in Frames
Vec_Int_t * vVisited; // nodes visited in Frames
// node mapping
int nObjs; // the largest number of an AIG object
Vec_Ptr_t * vAig2Frm; // mapping of AIG nodees into Frames nodes
// Vec_Str_t * vAig2Frm2; // mapping of AIG nodees into Frames nodes
// SAT solver
sat_solver * pSat; // SAT solver
int nSatVars; // the number of used SAT variables
@ -63,15 +61,43 @@ struct Saig_Bmc_t_
int iOutputFail; // failed output
};
static inline int Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vObj2Var, pObj->Id ); }
static inline void Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num); }
static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id ); }
static inline void Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode ); }
static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
{
// return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id );
Aig_Obj_t * pRes;
Vec_Int_t * vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i );
int iObjLit = Vec_IntEntry( vFrame, Aig_ObjId(pObj) );
if ( iObjLit == -1 )
return NULL;
pRes = Aig_ManObj( p->pFrm, Abc_Lit2Var(iObjLit) );
if ( pRes == NULL )
Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), -1 );
else
pRes = Aig_NotCond( pRes, Abc_LitIsCompl(iObjLit) );
return pRes;
}
static inline void Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode )
{
// Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode );
Vec_Int_t * vFrame;
int iObjLit;
if ( i == Vec_PtrSize(p->vAig2Frm) )
Vec_PtrPush( p->vAig2Frm, Vec_IntStartFull(p->nObjs) );
assert( i < Vec_PtrSize(p->vAig2Frm) );
vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i );
if ( pNode == NULL )
iObjLit = -1;
else
iObjLit = Abc_Var2Lit( Aig_ObjId(Aig_Regular(pNode)), Aig_IsComplement(pNode) );
Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), iObjLit );
}
static inline Aig_Obj_t * Saig_BmcObjChild0( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)); }
static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)); }
static inline int Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vObj2Var, pObj->Id ); }
static inline void Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -268,12 +294,11 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax,
p->pAig = pAig;
p->nObjs = Aig_ManObjNumMax(pAig);
// create node and variable mappings
p->vAig2Frm = Vec_PtrAlloc( 0 );
Vec_PtrFill( p->vAig2Frm, 5 * p->nObjs, NULL );
p->vAig2Frm = Vec_PtrAlloc( 100 );
p->vObj2Var = Vec_IntAlloc( 0 );
Vec_IntFill( p->vObj2Var, 5 * p->nObjs, 0 );
Vec_IntFill( p->vObj2Var, p->nObjs, 0 );
// start the AIG manager and map primary inputs
p->pFrm = Aig_ManStart( 5 * p->nObjs );
p->pFrm = Aig_ManStart( p->nObjs );
Saig_ManForEachLo( pAig, pObj, i )
Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) );
// create SAT solver
@ -284,8 +309,8 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax,
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ );
// other data structures
p->vTargets = Vec_PtrAlloc( 0 );
p->vVisited = Vec_PtrAlloc( 0 );
p->vTargets = Vec_PtrAlloc( 1000 );
p->vVisited = Vec_IntAlloc( 1000 );
p->iOutputFail = -1;
p->iFrameFail = -1;
return p;
@ -304,36 +329,12 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax,
***********************************************************************/
void Saig_BmcManStop( Saig_Bmc_t * p )
{
// Aig_Obj_t * pObj;
// int i, f, Counter = 0;
// int i, Counter = 0;
// for ( i = 0; i < p->vAig2Frm2->nSize; i++ )
// Counter += (p->vAig2Frm2->pArray[i] != 0);
// for ( i = 0; i < p->vAig2Frm->nSize; i++ )
// Counter += (p->vAig2Frm->pArray[i] != NULL);
// printf( "Objs = %d. Nodes = %d. Frames = %d. Used = %d. Non-empty = %d.\n",
// p->nObjs, Aig_ManNodeNum(p->pAig), p->iFrameLast, p->vAig2Frm->nSize, Counter );
/*
Aig_ManForEachObj( p->pAig, pObj, i )
{
int Last = -1;
for ( f = 0; f <= p->iFrameLast; f++ )
if ( Saig_BmcObjFrame( p, pObj, f ) )
Last = f;
if ( i % 50 == 0 )
printf( "%d ", Last );
}
printf( "\n" );
*/
Aig_ManStop( p->pFrm );
Vec_PtrFree( p->vAig2Frm );
// Vec_StrFree( p->vAig2Frm2 );
Vec_VecFree( (Vec_Vec_t *)p->vAig2Frm );
Vec_IntFree( p->vObj2Var );
sat_solver_delete( p->pSat );
Vec_PtrFree( p->vTargets );
Vec_PtrFree( p->vVisited );
Vec_IntFree( p->vVisited );
ABC_FREE( p );
}
@ -348,6 +349,7 @@ void Saig_BmcManStop( Saig_Bmc_t * p )
SeeAlso []
***********************************************************************/
/*
Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
{
Aig_Obj_t * pRes, * p0, * p1, * pConst1 = Aig_ManConst1(p->pAig);
@ -388,6 +390,7 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i
Saig_BmcObjSetFrame( p, pObj, i, pRes );
return pRes;
}
*/
/**Function*************************************************************
@ -400,7 +403,7 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i
SeeAlso []
***********************************************************************/
Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Vec_Ptr_t * vVisited )
Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Vec_Int_t * vVisited )
{
Aig_Obj_t * pRes;
pRes = Saig_BmcObjFrame( p, pObj, i );
@ -428,8 +431,8 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int
}
assert( pRes != NULL );
Saig_BmcObjSetFrame( p, pObj, i, pRes );
Vec_PtrPush( vVisited, pObj );
Vec_PtrPush( vVisited, (void *)(ABC_PTRINT_T)i );
Vec_IntPush( vVisited, Aig_ObjId(pObj) );
Vec_IntPush( vVisited, i );
return pRes;
}
@ -447,13 +450,12 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int
void Saig_BmcInterval( Saig_Bmc_t * p )
{
Aig_Obj_t * pTarget;
Aig_Obj_t * pObj, * pRes;
int i, iFrame, Counter;
int i, iObj, iFrame;
int nNodes = Aig_ManObjNum( p->pFrm );
Vec_PtrClear( p->vTargets );
p->iFramePrev = p->iFrameLast;
for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 )
{
{
if ( p->iOutputLast == 0 )
{
Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) );
@ -463,24 +465,14 @@ void Saig_BmcInterval( Saig_Bmc_t * p )
if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax )
return;
// Saig_BmcIntervalExplore_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast );
Vec_PtrClear( p->vVisited );
Vec_IntClear( p->vVisited );
pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited );
Vec_PtrPush( p->vTargets, pTarget );
Aig_ObjCreateCo( p->pFrm, pTarget );
Aig_ManCleanup( p->pFrm );
// check if the node is gone
Counter = 0;
Vec_PtrForEachEntry( Aig_Obj_t *, p->vVisited, pObj, i )
{
iFrame = (int)(ABC_PTRINT_T)Vec_PtrEntry( p->vVisited, 1+i++ );
pRes = Saig_BmcObjFrame( p, pObj, iFrame );
if ( Aig_ObjIsNone( Aig_Regular(pRes) ) )
{
Saig_BmcObjSetFrame( p, pObj, iFrame, NULL );
Counter++;
}
}
// printf( "%d ", Counter );
Vec_IntForEachEntryDouble( p->vVisited, iObj, iFrame, i )
Saig_BmcObjFrame( p, Aig_ManObj(p->pAig, iObj), iFrame );
}
}
}
@ -500,7 +492,7 @@ Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj
{
if ( pObj->pData )
return (Aig_Obj_t *)pObj->pData;
Vec_PtrPush( p->vVisited, pObj );
Vec_IntPush( p->vVisited, Aig_ObjId(pObj) );
if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsCi(pObj) )
{
p->nStitchVars += !Aig_ObjIsCi(pObj);
@ -533,15 +525,15 @@ Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p )
pNew = Aig_ManStart( p->nNodesMax );
Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew);
Vec_PtrClear( p->vVisited );
Vec_PtrPush( p->vVisited, Aig_ManConst1(p->pFrm) );
Vec_IntClear( p->vVisited );
Vec_IntPush( p->vVisited, Aig_ObjId(Aig_ManConst1(p->pFrm)) );
Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
{
// assert( !Aig_ObjIsConst1(Aig_Regular(pObj)) );
pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
assert( !Aig_IsComplement(pObjNew) );
Aig_ObjCreateCo( pNew, pObjNew );
}
}
return pNew;
}
@ -560,7 +552,7 @@ void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
{
Aig_Obj_t * pObj, * pObjNew;
int i, Lits[2], VarNumOld, VarNumNew;
Vec_PtrForEachEntry( Aig_Obj_t *, p->vVisited, pObj, i )
Aig_ManForEachObjVec( p->vVisited, p->pFrm, pObj, i )
{
// get the new variable of this node
pObjNew = (Aig_Obj_t *)pObj->pData;

199
src/aig/saig/saigBmc3.c
View File

@ -40,14 +40,13 @@ struct Gia_ManBmc_t_
Vec_Int_t * vMapping; // mapping
Vec_Vec_t * vSects; // sections
Vec_Int_t * vId2Num; // number of each node
Vec_Int_t * vVisited; // visited nodes
// SAT variables
Vec_Int_t * vPiVars; // SAT vars for the PIs
Vec_Ptr_t * vTerInfo; // ternary information
Vec_Ptr_t * vId2Var; // SAT vars for each object
// SAT solver
sat_solver * pSat; // SAT solver
int nSatVars; // SAT variables
int nObjNums; // SAT objects
int nWordNum; // unsigned words for ternary simulation
int nBufNum; // the number of simple nodes
int nDupNum; // the number of simple nodes
char * pSopSizes, ** pSops; // CNF representation
@ -684,14 +683,15 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
Vec_IntWriteEntry( p->vId2Num, Aig_ObjId(pObj), p->nObjNums++ );
Aig_ManForEachCo( pAig, pObj, i )
Vec_IntWriteEntry( p->vId2Num, Aig_ObjId(pObj), p->nObjNums++ );
p->vPiVars = Vec_IntAlloc( 1000 );
p->vId2Var = Vec_PtrAlloc( 100 );
p->vVisited = Vec_IntAlloc( 1000 );
p->vTerInfo = Vec_PtrAlloc( 100 );
// create solver
p->nSatVars = 1;
p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 1000 );
Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
// terminary simulation
p->nWordNum = Abc_BitWordNum( 2 * Aig_ManObjNumMax(pAig) );
return p;
}
@ -708,7 +708,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
***********************************************************************/
void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
{
Aig_ManCleanMarkA( p->pAig );
// Aig_ManCleanMarkA( p->pAig );
if ( p->vCexes )
{
assert( p->pAig->vSeqModelVec == NULL );
@ -719,9 +719,8 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
Vec_IntFree( p->vMapping );
Vec_VecFree( p->vSects );
Vec_IntFree( p->vId2Num );
Vec_IntFree( p->vPiVars );
Vec_IntFree( p->vVisited );
Vec_VecFree( (Vec_Vec_t *)p->vId2Var );
Vec_PtrFreeFree( p->vTerInfo );
sat_solver_delete( p->pSat );
free( p->pSopSizes );
free( p->pSops[1] );
@ -790,13 +789,6 @@ static inline int Saig_ManBmcSetLiteral( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int
ObjNum = Vec_IntEntry( p->vId2Num, Aig_ObjId(pObj) );
vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vId2Var, iFrame );
Vec_IntWriteEntry( vFrame, ObjNum, iLit );
if ( iLit == ABC_INFINITY || iLit == ABC_INFINITY+1 )
{
Vec_IntPush( p->vVisited, Aig_ObjId(pObj) );
Vec_IntPush( p->vVisited, iFrame );
}
else if ( iLit != ~0 && Saig_ObjIsPi(p->pAig, pObj) ) // save PI SAT var num
Vec_IntWriteEntry( p->vPiVars, iFrame*Saig_ManPiNum(p->pAig)+Aig_ObjCioId(pObj), lit_var(iLit) );
return iLit;
}
@ -1058,9 +1050,57 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in
{
iLit = ABC_INFINITY;
}
assert( iLit != ABC_INFINITY );
return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
}
/**Function*************************************************************
Synopsis [Recursively performs terminary simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManBmcRunTerSim_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
{
unsigned * pInfo = (unsigned *)Vec_PtrEntry( p->vTerInfo, iFrame );
int Val0, Val1, Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
if ( Value != SAIG_TER_NON )
return Value;
if ( Aig_ObjIsCo(pObj) )
{
Value = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame );
if ( Aig_ObjFaninC0(pObj) )
Value = Saig_ManBmcSimInfoNot( Value );
}
else if ( Saig_ObjIsLo(p->pAig, pObj) )
{
assert( iFrame > 0 );
Value = Saig_ManBmcRunTerSim_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame - 1 );
}
else if ( Aig_ObjIsNode(pObj) )
{
Val0 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame );
Val1 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin1(pObj), iFrame );
if ( Aig_ObjFaninC0(pObj) )
Val0 = Saig_ManBmcSimInfoNot( Val0 );
if ( Aig_ObjFaninC1(pObj) )
Val1 = Saig_ManBmcSimInfoNot( Val1 );
Value = Saig_ManBmcSimInfoAnd( Val0, Val1 );
}
else assert( 0 );
Saig_ManBmcSimInfoSet( pInfo, pObj, Value );
// transfer to the unrolling
if ( Saig_ManBmcMapping(p, pObj) && Value != SAIG_TER_UND )
Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) );
return Value;
}
/**Function*************************************************************
Synopsis [Derives CNF for one node.]
@ -1074,23 +1114,11 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in
***********************************************************************/
int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
{
int i, iLit, Entry, iFrameOld, Value;
Vec_IntClear( p->vVisited );
iLit = Saig_ManBmcCreateCnf_rec( p, pObj, iFrame, 0 );
Vec_IntForEachEntry( p->vVisited, Entry, i )
{
iFrameOld = Vec_IntEntry( p->vVisited, ++i );
Value = Saig_ManBmcLiteral( p, Aig_ManObj(p->pAig, Entry), iFrameOld );
// assert( Value == 0 || Value == 1 || Value == ABC_INFINITY || Value == ABC_INFINITY+1 );
assert( Value == ABC_INFINITY || Value == ABC_INFINITY+1 );
if ( !(Value == ABC_INFINITY || Value == ABC_INFINITY+1) )
printf( "Internal error!\n" );
// if ( Value == 0 || Value == 1 )
// continue;
Saig_ManBmcSetLiteral( p, Aig_ManObj(p->pAig, Entry), iFrameOld, ~0 );
}
if ( iLit < 2 )
return iLit;
// perform terminary simulation
int Value = Saig_ManBmcRunTerSim_rec( p, pObj, iFrame );
if ( Value != SAIG_TER_UND )
return (int)(Value == SAIG_TER_ONE);
// construct CNF if value is ternary
return Saig_ManBmcCreateCnf_rec( p, pObj, iFrame, 1 );
}
@ -1122,44 +1150,6 @@ int Aig_NodeCompareRefsIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
return 0;
}
/**Function*************************************************************
Synopsis [Mark PIs to be skipped based on nPisAbstract.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManBmcMarkPis( Aig_Man_t * pAig, int nPisAbstract )
{
Vec_Ptr_t * vPis;
Aig_Obj_t * pObj;
int i;
if ( nPisAbstract < 1 )
return;
// sort PIs by the number of their fanouts
vPis = Vec_PtrAlloc( 100 );
Saig_ManForEachPi( pAig, pObj, i )
Vec_PtrPush( vPis, pObj );
Vec_PtrSort( vPis, (int (*)(void))Aig_NodeCompareRefsIncrease );
Vec_PtrForEachEntry( Aig_Obj_t *, vPis, pObj, i )
{
if ( i < nPisAbstract )
{
pObj->fMarkA = 1;
// printf( "%d=%d ", Aig_ObjCioId(pObj), Aig_ObjRefs(pObj) );
}
}
// printf( "\n" );
// print primary inputs
// Saig_ManForEachPi( pAig, pObj, i )
// printf( "%d=%d ", i, Aig_ObjRefs(pObj) );
// printf( "\n" );
}
/**Function*************************************************************
Synopsis [This procedure sets default parameters.]
@ -1203,19 +1193,18 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
{
Gia_ManBmc_t * p;
Aig_Obj_t * pObj;
unsigned * pInfo;
int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock();
int nTimeToStop = time(NULL) + pPars->nTimeOut;
if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 )
printf( "Performing BMC with constraints...\n" );
p = Saig_Bmc3ManStart( pAig );
p->pPars = pPars;
if ( pPars->fVerbose )
{
printf( "Running \"bmc3\". AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d. Map = %6d. Sect =%3d.\n",
printf( "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d. Sect =%3d.\n",
Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), (Vec_IntSize(p->vMapping)-Aig_ManObjNumMax(pAig))/5, Vec_VecSize(p->vSects) );
Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), p->nObjNums, Vec_VecSize(p->vSects) );
printf( "Params: Start = %d. FramesMax = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n",
pPars->nStart, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
}
@ -1225,7 +1214,6 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
// perform frames
Aig_ManRandom( 1 );
Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract );
for ( f = 0; f < pPars->nFramesMax; f++ )
{
// stop BMC after exploring all reachable states
@ -1235,7 +1223,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
return pPars->nFailOuts ? 0 : 1;
}
// stop BMC if all targets are solved
if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) )
if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) )
{
Saig_Bmc3ManStop( p );
return 0;
@ -1243,11 +1231,12 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
// consider the next timeframe
if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame )
pPars->iFrame = f-1;
// resize the array
Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 );
// map nodes of this section
Vec_PtrPush( p->vId2Var, Vec_IntStartFull(p->nObjNums) );
Vec_PtrPush( p->vTerInfo, (pInfo = ABC_CALLOC(unsigned, p->nWordNum)) );
/*
// cannot remove mapping of frame values for any timeframes
// because with constant propagation they may be needed arbitrarily far
if ( f > 2*Vec_VecSize(p->vSects) )
{
int iFrameOld = f - 2*Vec_VecSize( p->vSects );
@ -1257,28 +1246,15 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
*/
// prepare some nodes
Saig_ManBmcSetLiteral( p, Aig_ManConst1(pAig), f, 1 );
Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(pAig), SAIG_TER_ONE );
Saig_ManForEachPi( pAig, pObj, i )
Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND );
if ( f == 0 )
Saig_ManForEachLo( p->pAig, pObj, i )
Saig_ManBmcSetLiteral( p, pObj, 0, 0 );
// set PIs to zero if they are marked
Saig_ManForEachPi( p->pAig, pObj, i )
if ( pObj->fMarkA )
Saig_ManBmcSetLiteral( p, pObj, f, Aig_ManRandom(0) & 1 );
// add the constraints for this frame
Saig_ManForEachPo( pAig, pObj, i )
{
if ( i < Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) )
continue;
clk2 = clock();
Lit = Saig_ManBmcCreateCnf( p, pObj, f );
Lit = lit_neg( Lit );
clkOther += clock() - clk2;
status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
if ( status == 0 )
Saig_ManForEachLo( p->pAig, pObj, i )
{
printf( "SAT problem became UNSAT after adding constraints in frame %d.\n", f );
Saig_Bmc3ManStop( p );
return 1;
Saig_ManBmcSetLiteral( p, pObj, 0, 0 );
Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_ZER );
}
}
if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
@ -1287,7 +1263,7 @@ clkOther += clock() - clk2;
clk = clock();
Saig_ManForEachPo( pAig, pObj, i )
{
if ( i >= Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) )
if ( i >= Saig_ManPoNum(pAig) )
break;
// skip solved outputs
if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
@ -1311,7 +1287,7 @@ clkOther += clock() - clk2;
}
pPars->nFailOuts++;
printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex );
@ -1332,13 +1308,19 @@ clkOther += clock() - clk2;
}
else if ( status == l_True )
{
int * pModel = Sat_SolverGetModel( p->pSat, Vec_IntArray(p->vPiVars), Vec_IntSize(p->vPiVars) );
Abc_Cex_t * pCex = Abc_CexCreate( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), pModel, f, i, 1 );
ABC_FREE( pModel );
Aig_Obj_t * pObjPi;
Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
int j, k, iBit = Saig_ManRegNum(pAig);
for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(pAig) )
Saig_ManForEachPi( p->pAig, pObjPi, k )
{
int iLit = Saig_ManBmcLiteral( p, pObjPi, j );
if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
Abc_InfoSetBit( pCex->pData, iBit + k );
}
fFirst = 0;
if ( !pPars->fSolveAll )
{
//ABC_PRT( "CNF generation runtime", clkOther );
if ( pPars->fVerbose )
{
printf( "%3d %s : ", f, fUnfinished ? "-" : "+" );
@ -1347,8 +1329,9 @@ clkOther += clock() - clk2;
printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts );
printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
// ABC_PRT( "Time", clock() - clk );
printf( "%4.0f Mb", 4.0*(f+1)*p->nObjNums /(1<<20) );
printf( "%4.0f Mb", 1.0*sat_solver_memory(p->pSat)/(1<<20) );
printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
printf( "%5.0f Mb", 1.0+sat_solver_memory(p->pSat)/(1<<20) );
printf( "\n" );
// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
// ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
@ -1364,7 +1347,7 @@ clkOther += clock() - clk2;
}
pPars->nFailOuts++;
printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex );
@ -1409,8 +1392,10 @@ clkOther += clock() - clk2;
printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
// ABC_PRT( "Time", clock() - clk );
// printf( "%4.0f Mb", 4.0*Vec_IntSize(p->vVisited) /(1<<20) );
printf( "%4.0f Mb", 4.0*(f+1)*p->nObjNums /(1<<20) );
printf( "%4.0f Mb", 1.0*sat_solver_memory(p->pSat)/(1<<20) );
printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
printf( "%5.0f Mb", 1.0+sat_solver_memory(p->pSat)/(1<<20) );
printf( "\n" );
// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
// ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );

26
src/base/abci/abc.c
View File

@ -19927,6 +19927,11 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Does not work for combinational networks.\n" );
return 0;
}
if ( Abc_NtkConstrNum(pNtk) > 0 )
{
Abc_Print( -1, "Constraints have to be folded (use \"fold\").\n" );
return 0;
}
pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
@ -24162,10 +24167,11 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ParFra_t Pars, * pPars = &Pars;
int c;
int nCofFanLit = 0;
int nNewAlgo = 1;
int fNewAlgo = 1;
int fInitSpecial = 0;
Gia_ManFraSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FLiavh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FLiasvh" ) ) != EOF )
{
switch ( c )
{
@ -24195,7 +24201,10 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fInit ^= 1;
break;
case 'a':
nNewAlgo ^= 1;
fNewAlgo ^= 1;
break;
case 's':
fInitSpecial ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
@ -24216,9 +24225,11 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
if ( nCofFanLit )
if ( fInitSpecial )
pTemp = Gia_ManFramesInitSpecial( pAbc->pGia, pPars->nFrames, pPars->fVerbose );
else if ( nCofFanLit )
pTemp = Gia_ManUnrollAndCofactor( pAbc->pGia, pPars->nFrames, nCofFanLit, pPars->fVerbose );
else if ( nNewAlgo )
else if ( fNewAlgo )
pTemp = Gia_ManFrames2( pAbc->pGia, pPars );
else
pTemp = Gia_ManFrames( pAbc->pGia, pPars );
@ -24226,12 +24237,13 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &frames [-FL <num>] [-aivh]\n" );
Abc_Print( -2, "usage: &frames [-FL <num>] [-iasvh]\n" );
Abc_Print( -2, "\t unrolls the design for several timeframes\n" );
Abc_Print( -2, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames );
Abc_Print( -2, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit );
Abc_Print( -2, "\t-i : toggle initializing registers [default = %s]\n", pPars->fInit? "yes": "no" );
Abc_Print( -2, "\t-a : toggle using new algorithm [default = %s]\n", nNewAlgo? "yes": "no" );
Abc_Print( -2, "\t-a : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes": "no" );
Abc_Print( -2, "\t-s : toggle computing special AIG for BMC [default = %s]\n", fInitSpecial? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;