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

Added equivalence class computation for flop outputs only in &equiv2.

This commit is contained in:
Alan Mishchenko 2011-07-13 10:13:24 +07:00
parent c4e8593075
commit 73702835c6
2 changed files with 13 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/aig/ssw/sswFilter.c
View File

@ -378,7 +378,7 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
SeeAlso []
***********************************************************************/
void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fVerbose )
void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
{
Ssw_Pars_t Pars, * pPars = &Pars;
Ssw_Man_t * p;
@ -401,7 +401,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
pPars->nFramesK = nFramesMax;
// create trivial equivalence classes with all nodes being candidates for constant 1
if ( pAig->pReprs == NULL )
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, 0, 0 );
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, fLatchOnly, 0 );
else
p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
@ -468,7 +468,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
SeeAlso []
***********************************************************************/
void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fVerbose )
void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
{
Aig_Man_t * pAig;
pAig = Gia_ManToAigSimple( p );
@ -478,7 +478,7 @@ void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRoun
ABC_FREE( p->pReprs );
ABC_FREE( p->pNexts );
}
Ssw_SignalFilter( pAig, nFramesMax, nConfMax, nRounds, TimeLimit, TimeLimit2, pCex, fVerbose );
Ssw_SignalFilter( pAig, nFramesMax, nConfMax, nRounds, TimeLimit, TimeLimit2, pCex, fLatchOnly, fVerbose );
Gia_ManReprFromAigRepr( pAig, p );
Aig_ManStop( pAig );
}

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

@ -24998,17 +24998,18 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Equiv2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fVerbose );
extern void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
int nFramesMax = 20;
int nConfMax = 500;
int nRounds = 10;
int TimeLimit = 0;
int TimeLimit2 = 0;
int fUseCex = 0;
int fLatchOnly = 0;
int fVerbose = 0;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCRTSxvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCRTSxlvh" ) ) != EOF )
{
switch ( c )
{
@ -25070,6 +25071,9 @@ int Abc_CommandAbc9Equiv2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'x':
fUseCex ^= 1;
break;
case 'l':
fLatchOnly ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -25098,14 +25102,14 @@ int Abc_CommandAbc9Equiv2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
}
Ssw_SignalFilterGia( pAbc->pGia, nFramesMax, nConfMax, nRounds, TimeLimit, TimeLimit2, fUseCex? pAbc->pCex: NULL, fVerbose );
Ssw_SignalFilterGia( pAbc->pGia, nFramesMax, nConfMax, nRounds, TimeLimit, TimeLimit2, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
pAbc->Status = -1;
// pAbc->nFrames = pAbc->pCex->iFrame;
// Abc_FrameReplaceCex( pAbc, &pAbc->pCex );
return 0;
usage:
Abc_Print( -2, "usage: &equiv2 [-FCRTS num] [-xvh]\n" );
Abc_Print( -2, "usage: &equiv2 [-FCRTS num] [-xlvh]\n" );
Abc_Print( -2, "\t computes candidate equivalence classes\n" );
Abc_Print( -2, "\t-F num : the max number of frames for BMC [default = %d]\n", nFramesMax );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax );
@ -25113,6 +25117,7 @@ usage:
Abc_Print( -2, "\t-T num : runtime limit in seconds for all rounds [default = %d]\n", TimeLimit );
Abc_Print( -2, "\t-S num : runtime limit in seconds for one round [default = %d]\n", TimeLimit2 );
Abc_Print( -2, "\t-x : toggle using the current cex to perform refinement [default = %s]\n", fUseCex? "yes": "no" );
Abc_Print( -2, "\t-l : toggle considering only latch output equivalences [default = %s]\n", fLatchOnly? "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");
return 1;