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

Added counter-example printout to "&cec -t".

This commit is contained in:
Alan Mishchenko 2025-12-24 15:57:57 -08:00
parent c0ea0cf4d0
commit 58023c97b7
2 changed files with 23 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -42284,6 +42284,7 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Cec_ManPrintCexSummary( Gia_Man_t * p, Abc_Cex_t * pCex, Cec_ParCec_t * pPars );
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
FILE * pFile;
Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter;
@ -42553,12 +42554,32 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
extern int Gia_ManCheckSimEquiv( Gia_Man_t * p, int fVerbose );
int Status = Gia_ManCheckSimEquiv( pMiter, pPars->fVerbose );
if ( Status == 1 )
{
Abc_Print( 1, "Networks are equivalent. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
else if ( Status == 0 )
{
Abc_Print( 1, "Networks are NOT equivalent. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
{
Cec_ParCec_t ParsTemp = *pPars;
ParsTemp.fSilent = 1;
Cec_ManVerify( pMiter, &ParsTemp );
if ( pMiter->pCexComb )
{
Cec_ManPrintCexSummary( pMiter, pMiter->pCexComb, pPars );
pGias[0]->pCexComb = pMiter->pCexComb;
pMiter->pCexComb = NULL;
Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
}
}
}
else
{
Abc_Print( 1, "Networks are UNDECIDED. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
}
else if ( fUseNewX )
{

2
src/proof/cec/cecCec.c
View File

@ -75,7 +75,7 @@ static const char * Cec_ManGetName( const char * pName, const char * pPrefix, in
}
}
static void Cec_ManPrintCexSummary( Gia_Man_t * p, Abc_Cex_t * pCex, Cec_ParCec_t * pPars )
void Cec_ManPrintCexSummary( Gia_Man_t * p, Abc_Cex_t * pCex, Cec_ParCec_t * pPars )
{
Vec_Ptr_t * vToFree = NULL;
const char ** ppInNames = NULL;