From d4e3670e213ec884170ba6511a8f4f60cdd1f906 Mon Sep 17 00:00:00 2001 From: Marcel Walter Date: Tue, 11 Aug 2026 19:22:06 +0200 Subject: [PATCH] &cec -x/-y, &icec: also require the swept miter outputs to be constant 0 The equivalence verdict in these three branches is taken from Gia_ManAndNum(pNew) == 0 after Cec4_/Cec5_ManSimulateTest3. An AND-free GIA can still have outputs that are constant 1 or CI literals, which are satisfiable, so this reports "Networks are equivalent" for some non-equivalent pairs -- for example `a & b` against `~(a & b)`, where the miter sweeps to constant 1. Check the outputs as well: AND nodes remaining -> UNDECIDED as before; AND-free with all outputs constant 0 -> equivalent as before; AND-free otherwise -> NOT equivalent, which is decidable by inspection since such a miter is satisfiable. --- src/base/abci/abc.c | 41 +++++++++++++++++++++++++++++++++++------ 1 file changed, 35 insertions(+), 6 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 86a9fd2ca..708d19013 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -43874,6 +43874,29 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam 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************************************************************* Synopsis [] @@ -44302,10 +44325,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) abctime clk = Abc_Clock(); 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 ); - 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. " ); else - Abc_Print( 1, "Networks are UNDECIDED. " ); + Abc_Print( 1, "Networks are NOT equivalent. " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Gia_ManStop( pNew ); } @@ -44314,10 +44339,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) abctime clk = Abc_Clock(); 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 ); - 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. " ); else - Abc_Print( 1, "Networks are UNDECIDED. " ); + Abc_Print( 1, "Networks are NOT equivalent. " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Gia_ManStop( pNew ); } @@ -44518,10 +44545,12 @@ int Abc_CommandAbc9ICec( Abc_Frame_t * pAbc, int argc, char ** argv ) abctime clk = Abc_Clock(); 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 ); - 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. " ); else - Abc_Print( 1, "Networks are UNDECIDED. " ); + Abc_Print( 1, "Networks are NOT equivalent. " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Gia_ManStop( pNew ); }