Commit 75ee395f by Alan Mishchenko

Implemented additional filtering of equivalences (&srm -sf).

parent ab75993d
...@@ -393,7 +393,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) ...@@ -393,7 +393,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
// write equivalence classes // write equivalence classes
Gia_WriteAiger( pAig, "gore.aig", 0, 0 ); Gia_WriteAiger( pAig, "gore.aig", 0, 0 );
// reduce the model // reduce the model
pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0 ); pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0, 0 );
if ( pReduce ) if ( pReduce )
{ {
pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 ); pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
......
...@@ -659,7 +659,7 @@ extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose ...@@ -659,7 +659,7 @@ extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose
extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose ); extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ); extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ); extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fVerbose ); extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fSkipSome, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames, int fDualOut ); extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames, int fDualOut );
extern Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs ); extern Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs );
extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ); extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
......
...@@ -748,7 +748,7 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ) ...@@ -748,7 +748,7 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
SeeAlso [] 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 ) 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 )
{ {
Gia_Obj_t * pRepr; Gia_Obj_t * pRepr;
unsigned iLitNew; unsigned iLitNew;
...@@ -760,7 +760,14 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t ...@@ -760,7 +760,14 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
return; return;
iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
{
if ( vTrace ) Vec_IntPush( vTrace, 1 );
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) ); Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
}
else
{
if ( vTrace ) Vec_IntPush( vTrace, 0 );
}
if ( fSpeculate ) if ( fSpeculate )
pObj->Value = iLitNew; pObj->Value = iLitNew;
} }
...@@ -799,15 +806,15 @@ int Gia_ManHasNoEquivs( Gia_Man_t * p ) ...@@ -799,15 +806,15 @@ int Gia_ManHasNoEquivs( Gia_Man_t * p )
SeeAlso [] 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 ) 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 )
{ {
if ( ~pObj->Value ) if ( ~pObj->Value )
return; return;
assert( Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsAnd(pObj) );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate ); Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate ); Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate, vTrace );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate ); Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -821,36 +828,77 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V ...@@ -821,36 +828,77 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fSpeculate, int fVerbose ) Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
{ {
Vec_Int_t * vXorLits;
Gia_Man_t * pNew, * pTemp; Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
Vec_Int_t * vXorLits;
int i, iLitNew; int i, iLitNew;
if ( !p->pReprs ) if ( !p->pReprs )
{ {
printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" ); printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
return NULL; return NULL;
} }
if ( fDualOut && (Gia_ManPoNum(p) & 1) ) Vec_IntClear( vTrace );
vXorLits = Vec_IntAlloc( 1000 );
Gia_ManSetPhase( p );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachRo( p, pObj, i )
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, 0, 1, vTrace );
Gia_ManForEachCo( p, pObj, i )
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, 0, 1, vTrace );
Gia_ManForEachPo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Vec_IntForEachEntry( vXorLits, iLitNew, i )
Gia_ManAppendCo( pNew, iLitNew );
if ( Vec_IntSize(vXorLits) == 0 )
{ {
printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" ); printf( "Speculatively reduced model has no primary outputs.\n" );
return NULL; Gia_ManAppendCo( pNew, 0 );
} }
/* Gia_ManForEachRi( p, pObj, i )
if ( Gia_ManHasNoEquivs(p) ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
Vec_IntFree( vXorLits );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Reduces AIG using equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fSpeculate, int fSkipSome, int fVerbose )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
Vec_Int_t * vXorLits;
int i, iLitNew;
if ( !p->pReprs )
{ {
printf( "Gia_ManSpecReduce(): There are no equivalences to reduce.\n" ); printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
return NULL; return NULL;
} }
*/ if ( fDualOut && (Gia_ManPoNum(p) & 1) )
/*
if ( !Gia_ManCheckTopoOrder( p ) )
{ {
printf( "Gia_ManSpecReduce(): AIG is not in a correct topological order.\n" ); printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
return NULL; return NULL;
} }
*/
vXorLits = Vec_IntAlloc( 1000 ); vXorLits = Vec_IntAlloc( 1000 );
Gia_ManSetPhase( p ); Gia_ManSetPhase( p );
Gia_ManFillValue( p ); Gia_ManFillValue( p );
...@@ -863,9 +911,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int ...@@ -863,9 +911,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
Gia_ManForEachCi( p, pObj, i ) Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew); pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachRo( p, pObj, i ) Gia_ManForEachRo( p, pObj, i )
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate ); Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, NULL );
Gia_ManForEachCo( p, pObj, i ) Gia_ManForEachCo( p, pObj, i )
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate ); Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, NULL );
if ( !fSynthesis ) if ( !fSynthesis )
{ {
Gia_ManForEachPo( p, pObj, i ) Gia_ManForEachPo( p, pObj, i )
...@@ -885,6 +933,29 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int ...@@ -885,6 +933,29 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
pNew = Gia_ManCleanup( pTemp = pNew ); pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp ); Gia_ManStop( pTemp );
// update using trace
if ( fSkipSome )
{
Vec_Int_t * vTrace = Vec_IntAlloc( 100 );
int iLit, nLitNum = Gia_ManEquivCountLitsAll(p);
pTemp = Gia_ManSpecReduceTrace( p, vTrace );
Gia_ManStop( pTemp );
assert( Vec_IntSize(vTrace) == nLitNum );
assert( Gia_ManPoNum(pNew) == Gia_ManPoNum(p) + nLitNum );
iLit = Gia_ManPoNum(p);
for ( i = 0; i < nLitNum; i++ )
{
if ( Vec_IntEntry( vTrace, i ) == 0 )
continue;
pObj = Gia_ManPo( pNew, Gia_ManPoNum(p) + i );
pObj->fCompl0 = 0;
pObj->iDiff0 = Gia_ObjId( pNew, pObj );
}
Vec_IntFreeP( &vTrace );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
}
return pNew; return pNew;
} }
...@@ -1591,7 +1662,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f ...@@ -1591,7 +1662,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
printf( "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" ); printf( "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
break; break;
} }
pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0 ); pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
// bmc2 -F 100 -C 25000 // bmc2 -F 100 -C 25000
{ {
Abc_Cex_t * pCex; Abc_Cex_t * pCex;
...@@ -1628,7 +1699,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f ...@@ -1628,7 +1699,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
// write equivalence classes // write equivalence classes
Gia_WriteAiger( pGia, "gore.aig", 0, 0 ); Gia_WriteAiger( pGia, "gore.aig", 0, 0 );
// reduce the model // reduce the model
pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0 ); pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
if ( pReduce ) if ( pReduce )
{ {
pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 ); pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
......
...@@ -25941,22 +25941,26 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -25941,22 +25941,26 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
char pFileName[10], pFileName2[10]; char pFileName[10], pFileName2[10];
Gia_Man_t * pTemp, * pAux; Gia_Man_t * pTemp, * pAux;
int c, fVerbose = 0; int c, fVerbose = 0;
int fSpeculate = 1;
int fSynthesis = 0; int fSynthesis = 0;
int fSpeculate = 1;
int fSkipSome = 0;
int fDualOut = 0; int fDualOut = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "dsrvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "drsfvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 'd': case 'd':
fDualOut ^= 1; fDualOut ^= 1;
break; break;
case 'r':
fSynthesis ^= 1;
break;
case 's': case 's':
fSpeculate ^= 1; fSpeculate ^= 1;
break; break;
case 'r': case 'f':
fSynthesis ^= 1; fSkipSome ^= 1;
break; break;
case 'v': case 'v':
fVerbose ^= 1; fVerbose ^= 1;
...@@ -25974,7 +25978,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -25974,7 +25978,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
sprintf( pFileName, "gsrm%s.aig", fSpeculate? "" : "s" ); sprintf( pFileName, "gsrm%s.aig", fSpeculate? "" : "s" );
sprintf( pFileName2, "gsyn%s.aig", fSpeculate? "" : "s" ); sprintf( pFileName2, "gsyn%s.aig", fSpeculate? "" : "s" );
pTemp = Gia_ManSpecReduce( pAbc->pGia, fDualOut, fSynthesis, fSpeculate, fVerbose ); pTemp = Gia_ManSpecReduce( pAbc->pGia, fDualOut, fSynthesis, fSpeculate, fSkipSome, fVerbose );
if ( pTemp ) if ( pTemp )
{ {
if ( fSpeculate ) if ( fSpeculate )
...@@ -26004,11 +26008,12 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -26004,11 +26008,12 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &srm [-dsrvh]\n" ); Abc_Print( -2, "usage: &srm [-drsfvh]\n" );
Abc_Print( -2, "\t writes speculatively reduced model into file \"%s\"\n", pFileName ); Abc_Print( -2, "\t writes speculatively reduced model into file \"%s\"\n", pFileName );
Abc_Print( -2, "\t-d : toggle creating dual output miter [default = %s]\n", fDualOut? "yes": "no" ); Abc_Print( -2, "\t-d : toggle creating dual output miter [default = %s]\n", fDualOut? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using speculation at the internal nodes [default = %s]\n", fSpeculate? "yes": "no" );
Abc_Print( -2, "\t-r : toggle writing reduced network for synthesis [default = %s]\n", fSynthesis? "yes": "no" ); Abc_Print( -2, "\t-r : toggle writing reduced network for synthesis [default = %s]\n", fSynthesis? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using speculation at the internal nodes [default = %s]\n", fSpeculate? "yes": "no" );
Abc_Print( -2, "\t-f : toggle filtering to remove redundant equivalences [default = %s]\n", fSkipSome? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); 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"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
...@@ -26127,7 +26132,7 @@ usage: ...@@ -26127,7 +26132,7 @@ usage:
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<miter.aig> : file with the external miter to read\n"); Abc_Print( -2, "\t<miter.aig> : file with the external miter to read\n");
Abc_Print( -2, "\t \n" ); Abc_Print( -2, "\t \n" );
Abc_Print( -2, "\t The external miter should be generated by &srm -m\n" ); Abc_Print( -2, "\t The external miter should be generated by &srm -s\n" );
Abc_Print( -2, "\t and (partially) solved by any verification engine(s).\n" ); Abc_Print( -2, "\t and (partially) solved by any verification engine(s).\n" );
Abc_Print( -2, "\t The external miter should have as many POs as\n" ); Abc_Print( -2, "\t The external miter should have as many POs as\n" );
Abc_Print( -2, "\t the number of POs in the current AIG plus\n" ); Abc_Print( -2, "\t the number of POs in the current AIG plus\n" );
......
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