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

Merge pull request #543 from marcelwa/cec-verdict-const0 

&cec -x/-y: is the AND-free check meant to be sufficient for equivalence?
This commit is contained in:
alanminko 2026-08-16 01:49:49 +09:00 committed by GitHub
parent fe862d3647 d4e3670e21
commit 89bef47d8d
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 35 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -43722,6 +43722,29 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
return pGia; return pGia;
} }
/**Function*************************************************************
Synopsis [Returns 1 if all outputs of the swept miter are constant 0.]
Description [The equivalence check below concludes from the swept miter
having no AND nodes. An AND-free GIA can still have outputs that are
constant 1 or CI literals, which are satisfiable, so the outputs are
checked here as well.]
SideEffects []
SeeAlso []
***********************************************************************/
static int Abc_CecSweptMiterIsConst0( Gia_Man_t * p )
{
int i;
for ( i = 0; i < Gia_ManPoNum(p); i++ )
if ( !Gia_ManPoIsConst0(p, i) )
return 0;
return 1;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
@ -44150,10 +44173,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose ); extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose ); Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose );
if ( Gia_ManAndNum(pNew) == 0 ) if ( Gia_ManAndNum(pNew) != 0 )
Abc_Print( 1, "Networks are UNDECIDED. " );
else if ( Abc_CecSweptMiterIsConst0(pNew) )
Abc_Print( 1, "Networks are equivalent. " ); Abc_Print( 1, "Networks are equivalent. " );
else else
Abc_Print( 1, "Networks are UNDECIDED. " ); Abc_Print( 1, "Networks are NOT equivalent. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Gia_ManStop( pNew ); Gia_ManStop( pNew );
} }
@ -44162,10 +44187,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
extern Gia_Man_t * Cec5_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose ); extern Gia_Man_t * Cec5_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
Gia_Man_t * pNew = Cec5_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose ); Gia_Man_t * pNew = Cec5_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose );
if ( Gia_ManAndNum(pNew) == 0 ) if ( Gia_ManAndNum(pNew) != 0 )
Abc_Print( 1, "Networks are UNDECIDED. " );
else if ( Abc_CecSweptMiterIsConst0(pNew) )
Abc_Print( 1, "Networks are equivalent. " ); Abc_Print( 1, "Networks are equivalent. " );
else else
Abc_Print( 1, "Networks are UNDECIDED. " ); Abc_Print( 1, "Networks are NOT equivalent. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Gia_ManStop( pNew ); Gia_ManStop( pNew );
} }
@ -44366,10 +44393,12 @@ int Abc_CommandAbc9ICec( Abc_Frame_t * pAbc, int argc, char ** argv )
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose ); extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose ); Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose );
if ( Gia_ManAndNum(pNew) == 0 ) if ( Gia_ManAndNum(pNew) != 0 )
Abc_Print( 1, "Networks are UNDECIDED. " );
else if ( Abc_CecSweptMiterIsConst0(pNew) )
Abc_Print( 1, "Networks are equivalent. " ); Abc_Print( 1, "Networks are equivalent. " );
else else
Abc_Print( 1, "Networks are UNDECIDED. " ); Abc_Print( 1, "Networks are NOT equivalent. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Gia_ManStop( pNew ); Gia_ManStop( pNew );
} }