Updating interface of scorr.

This commit is contained in:
Alan Mishchenko 2023-01-28 09:31:13 -10:00
parent 66a5fe7aec
commit 70a07869c6
2 changed files with 41 additions and 4 deletions

View File

@ -36828,14 +36828,15 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Cec_ManScorrCorrespondence( Gia_Man_t * p, Cec_ParCor_t * pPars );
extern Gia_Man_t * Gia_ManScorrDivideTest( Gia_Man_t * p, Cec_ParCor_t * pPars );
Cec_ParCor_t Pars, * pPars = &Pars;
Gia_Man_t * pTemp;
int fPartition = 0;
int c;
int fUseOld = 0, c;
Cec_ManCorSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPXpkrecqwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPXpkrecqowvh" ) ) != EOF )
{
switch ( c )
{
@ -36901,6 +36902,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'q':
pPars->fStopWhenGone ^= 1;
break;
case 'o':
fUseOld ^= 1;
break;
case 'w':
pPars->fVerboseFlops ^= 1;
break;
@ -36932,7 +36936,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 0, "The network is combinational.\n" );
return 0;
}
if ( fPartition )
if ( fUseOld )
pTemp = Cec_ManScorrCorrespondence( pAbc->pGia, pPars );
else if ( fPartition )
pTemp = Gia_ManScorrDivideTest( pAbc->pGia, pPars );
else
pTemp = Cec_ManLSCorrespondence( pAbc->pGia, pPars );
@ -36940,7 +36946,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &scorr [-FCPX num] [-pkrecqwvh]\n" );
Abc_Print( -2, "usage: &scorr [-FCPX num] [-pkrecqowvh]\n" );
Abc_Print( -2, "\t performs signal correpondence computation\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
@ -36952,6 +36958,7 @@ usage:
Abc_Print( -2, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
Abc_Print( -2, "\t-q : toggle quitting when PO is not a constant candidate [default = %s]\n", pPars->fStopWhenGone? "yes": "no" );
Abc_Print( -2, "\t-o : toggle calling old engine [default = %s]\n", fUseOld? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing verbose info about equivalent flops [default = %s]\n", pPars->fVerboseFlops? "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");

View File

@ -444,6 +444,36 @@ Abc_Ntk_t * Abc_NtkTestScorr( char * pFileNameIn, char * pFileNameOut, int nStep
return pResult;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManScorrCorrespondence( Gia_Man_t * p, Cec_ParCor_t * pCorPars )
{
Gia_Man_t * pRes = NULL;
Aig_Man_t * pOld, * pNew;
Ssw_Pars_t SswPars, * pSswPars = &SswPars;
Ssw_ManSetDefaultParams( pSswPars );
pSswPars->nBTLimit = pCorPars->nBTLimit;
pSswPars->nFramesK = pCorPars->nFrames;
pSswPars->fLatchCorr = pCorPars->fLatchCorr;
pSswPars->fVerbose = pCorPars->fVerbose;
pOld = Gia_ManToAigSimple( p );
pNew = Ssw_SignalCorrespondence( pOld, pSswPars );
pRes = Gia_ManFromAigSimple( pNew );
Gia_ManReprFromAigRepr( pOld, p );
Aig_ManStop( pOld );
Aig_ManStop( pNew );
return pRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///