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

Adding command &filter_equiv to filter candidate equivalence classes using indexes of disproved POs after handling SRM as a multi-output miter.

This commit is contained in:
Alan Mishchenko 2013-04-17 22:18:43 -07:00
parent bdae7c625a
commit 06ba3d3e6c
6 changed files with 183 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

142
src/aig/gia/giaEquiv.c
View File

@ -724,7 +724,7 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide )
static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide, Vec_Int_t * vMap )
{
Gia_Obj_t * pRepr;
unsigned iLitNew;
@ -740,7 +740,11 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
if ( vTrace )
Vec_IntPush( vTrace, 1 );
if ( vGuide == NULL || Vec_IntEntry( vGuide, Vec_IntSize(vTrace)-1 ) )
{
if ( vMap )
Vec_IntPush( vMap, Gia_ObjId(p, pObj) );
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
}
}
else
{
@ -751,29 +755,6 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
pObj->Value = iLitNew;
}
/**Function*************************************************************
Synopsis [Returns 1 if AIG has dangling nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManHasNoEquivs( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i;
if ( p->pReprs == NULL )
return 1;
Gia_ManForEachObj( p, pObj, i )
if ( Gia_ObjReprObj(p, i) != NULL )
break;
return i == Gia_ManObjNum(p);
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
@ -785,15 +766,15 @@ int Gia_ManHasNoEquivs( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide )
void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide, Vec_Int_t * vMap )
{
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide );
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap );
}
/**Function*************************************************************
@ -807,7 +788,7 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace, Vec_Int_t * vMap )
{
Vec_Int_t * vXorLits;
Gia_Man_t * pNew, * pTemp;
@ -830,9 +811,9 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachRo( p, pObj, i )
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, 0, 1, vTrace, NULL );
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, 0, 1, vTrace, NULL, vMap );
Gia_ManForEachCo( p, pObj, i )
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, 0, 1, vTrace, NULL );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, 0, 1, vTrace, NULL, vMap );
Gia_ManForEachPo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Vec_IntForEachEntry( vXorLits, iLitNew, i )
@ -883,7 +864,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
if ( fSkipSome )
{
vGuide = Vec_IntAlloc( 100 );
pTemp = Gia_ManSpecReduceTrace( p, vGuide );
pTemp = Gia_ManSpecReduceTrace( p, vGuide, NULL );
Gia_ManStop( pTemp );
assert( Vec_IntSize(vGuide) == Gia_ManEquivCountLitsAll(p) );
vTrace = Vec_IntAlloc( 100 );
@ -901,9 +882,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachRo( p, pObj, i )
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide );
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide, NULL );
Gia_ManForEachCo( p, pObj, i )
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, NULL );
if ( !fSynthesis )
{
Gia_ManForEachPo( p, pObj, i )
@ -1212,7 +1193,7 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb
if ( fSkipSome )
{
Vec_Int_t * vTrace = Vec_IntAlloc( 100 );
pTemp = Gia_ManSpecReduceTrace( p, vTrace );
pTemp = Gia_ManSpecReduceTrace( p, vTrace, NULL );
Gia_ManStop( pTemp );
assert( Vec_IntSize(vTrace) == nLitsAll );
// count the number of non-zero entries
@ -1277,6 +1258,74 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb
Gia_ManStop( pMiter );
}
/**Function*************************************************************
Synopsis [Transforms equiv classes by filtering those that correspond to disproved outputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManEquivFilter( Gia_Man_t * p, Vec_Int_t * vPoIds, int fVerbose )
{
Gia_Man_t * pSrm;
Vec_Int_t * vTrace, * vMap;
int i, iObjId, Entry, Prev = -1;
// check if there are equivalences
if ( p->pReprs == NULL || p->pNexts == NULL )
{
Abc_Print( 1, "Gia_ManEquivFilter(): Equivalence classes are not defined.\n" );
return;
}
// check if PO indexes are available
if ( vPoIds == NULL )
{
Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs is not available.\n" );
return;
}
if ( Vec_IntSize(vPoIds) == 0 )
return;
// create SRM with mapping into POs
vMap = Vec_IntAlloc( 1000 );
vTrace = Vec_IntAlloc( 1000 );
pSrm = Gia_ManSpecReduceTrace( p, vTrace, vMap );
// the resulting array (vMap) maps PO indexes of the SRM into object IDs
assert( Vec_IntSize(vMap) == Gia_ManPoNum(pSrm) );
Vec_IntFree( vTrace );
Gia_ManStop( pSrm );
// check if disproved POs satisfy the range
Vec_IntSort( vPoIds, 0 );
Vec_IntForEachEntry( vPoIds, Entry, i )
{
if ( Entry < 0 || Entry >= Gia_ManPoNum(p) )
{
Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs contains PO index (%d),\n", Entry );
Abc_Print( 1, "which does not fit into the range of available PO indexes of the SRM: [%d; %d].\n", Entry, 0, Vec_IntSize(vMap)-1 );
Vec_IntFree( vMap );
return;
}
if ( Prev == Entry )
{
Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs contains at least one duplicate entry (%d),\n", Entry );
Vec_IntFree( vMap );
return;
}
Prev = Entry;
}
// perform the reduction of the equivalence classes
Vec_IntForEachEntry( vPoIds, Entry, i )
{
iObjId = Vec_IntEntry( vMap, Entry );
Gia_ObjUnsetRepr( p, iObjId );
// Gia_ObjSetNext( p, iObjId, 0 );
}
ABC_FREE( p->pNexts );
p->pNexts = Gia_ManDeriveNexts( p );
}
/**Function*************************************************************
Synopsis [Transforms equiv classes by setting a good representative.]
@ -1642,6 +1691,29 @@ ABC_NAMESPACE_IMPL_END
ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
Synopsis [Returns 1 if AIG has dangling nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManHasNoEquivs( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i;
if ( p->pReprs == NULL )
return 1;
Gia_ManForEachObj( p, pObj, i )
if ( Gia_ObjReprObj(p, i) != NULL )
break;
return i == Gia_ManObjNum(p);
}
/**Function*************************************************************
Synopsis [Implements iteration during speculation.]

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

@ -354,6 +354,7 @@ static int Abc_CommandAbc9Srm2 ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Filter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Reduce ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9EquivMark ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9EquivFilter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Verify ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Sweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -849,6 +850,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&filter", Abc_CommandAbc9Filter, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reduce", Abc_CommandAbc9Reduce, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&equiv_mark", Abc_CommandAbc9EquivMark, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&equiv_filter", Abc_CommandAbc9EquivFilter, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cec", Abc_CommandAbc9Cec, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&verify", Abc_CommandAbc9Verify, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sweep", Abc_CommandAbc9Sweep, 0 );
@ -27518,7 +27520,7 @@ int Abc_CommandAbc9EquivMark( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Reduce(): There is no AIG.\n" );
Abc_Print( -1, "Abc_CommandAbc9EquivMark(): There is no AIG.\n" );
return 1;
}
if ( argc != globalUtilOptind + 1 )
@ -27547,6 +27549,52 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9EquivFilter( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManEquivFilter( Gia_Man_t * p, Vec_Int_t * vPoIds, int fVerbose );
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9EquivFilter(): There is no AIG.\n" );
return 1;
}
Gia_ManEquivFilter( pAbc->pGia, pAbc->vAbcObjIds, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &equiv_filter [-vh]\n" );
Abc_Print( -2, "\t filters equivalence candidates after disproving some SRM outputs\n" );
Abc_Print( -2, "\t (the array of disproved outputs should be given as pAbc->vAbcObjIds)\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []

1
src/base/main/main.h
View File

@ -116,6 +116,7 @@ extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * p );
extern ABC_DLL Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p );
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p );
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p );
extern ABC_DLL Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p );
extern ABC_DLL int Abc_FrameReadCexPiNum( Abc_Frame_t * p );
extern ABC_DLL int Abc_FrameReadCexRegNum( Abc_Frame_t * p );

3
src/base/main/mainFrame.c
View File

@ -65,6 +65,7 @@ int Abc_FrameReadProbStatus( Abc_Frame_t * p ) { return s_GlobalFr
Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; }
Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ) { return s_GlobalFrame->vCexVec; }
Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ) { return s_GlobalFrame->vPoEquivs; }
Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p ) { return s_GlobalFrame->vAbcObjIds; }
int Abc_FrameReadCexPiNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nPis; }
int Abc_FrameReadCexRegNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nRegs; }
@ -142,6 +143,7 @@ Abc_Frame_t * Abc_FrameAllocate()
p->fBatchMode = 0;
// networks to be used by choice
p->vStore = Vec_PtrAlloc( 16 );
p->vAbcObjIds = Vec_IntAlloc( 0 );
// initialize decomposition manager
// define_cube_size(20);
// set_espresso_flags();
@ -172,6 +174,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
// undefine_cube_size();
Rwt_ManGlobalStop();
// Ivy_TruthManStop();
if ( p->vAbcObjIds) Vec_IntFree( p->vAbcObjIds );
if ( p->vCexVec ) Vec_PtrFreeFree( p->vCexVec );
if ( p->vPoEquivs ) Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs );
if ( p->pLibVer ) Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL );

1
src/base/main/mainInt.h
View File

@ -101,6 +101,7 @@ struct Abc_Frame_t_
Abc_Cex_t * pCex2; // copy of the above
Vec_Ptr_t * vCexVec; // a vector of counter-examples if more than one PO fails
Vec_Ptr_t * vPoEquivs; // equivalence classes of isomorphic primary outputs
Vec_Int_t * vAbcObjIds; // object IDs
int Status; // the status of verification problem (proved=1, disproved=0, undecided=-1)
int nFrames; // the number of time frames completed by BMC
Vec_Ptr_t * vPlugInComBinPairs; // pairs of command and its binary name

22
src/python/pyabc.i
View File

@ -320,6 +320,20 @@ PyObject* eq_classes()
return eq_classes;
}
void _pyabc_array_clear()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Vec_Int_t *vObjIds = Abc_FrameReadObjIds(pAbc);
Vec_IntClear( vObjIds );
}
void _pyabc_array_push(int i)
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Vec_Int_t *vObjIds = Abc_FrameReadObjIds(pAbc);
Vec_IntPush( vObjIds, i );
}
static PyObject* pyabc_internal_python_command_callback = 0;
void pyabc_internal_set_command_callback( PyObject* callback )
@ -644,6 +658,9 @@ int _cex_get_frame(Abc_Cex_t* pCex);
PyObject* eq_classes();
void _pyabc_array_clear();
void _pyabc_array_push(int i);
void pyabc_internal_set_command_callback( PyObject* callback );
void pyabc_internal_register_command( char * sGroup, char * sName, int fChanges );
@ -1168,4 +1185,9 @@ def cmd_python(cmd_args):
add_abc_command(cmd_python, "Python", "python", 0)
def create_abc_array(List):
_pyabc_array_clear()
for ObjId in List:
_pyabc_array_push(ObjId)
%}