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

&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.
This commit is contained in:
Marcel Walter 2026-08-11 19:22:06 +02:00
parent 6c51a92385
commit d4e3670e21
No known key found for this signature in database
GPG Key ID: 2979DB71A0C2C23D
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

@ -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 );
}