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

Bug fix in &gencex.

This commit is contained in:
Alan Mishchenko 2025-01-02 00:33:22 +07:00
parent 350dcd3ea4
commit d5e1a5d445
2 changed files with 7 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/aig/gia/giaPat2.c
View File

@ -965,6 +965,12 @@ Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTrie
if ( Vec_IntEntry(vStats[2], i) >= nMinCexes || Vec_IntEntry(vStats[1], i) > 10*Vec_IntEntry(vStats[2], i) )
continue;
{
assert( Gia_ObjIsCo(pObj) );
if ( Gia_ObjFaninId0p(p, pObj) == 0 ) {
if ( fVerbose )
printf( "Output %d is driven by constant %d.\n", Gia_ObjCioId(pObj), Gia_ObjFaninC0(pObj) );
continue;
}
abctime clk = Abc_Clock();
int iObj = Min_ManCo(pNew, i);
int Index = Gia_ObjCioId(pObj);

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

@ -54262,7 +54262,7 @@ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: &gencex [-CM num] [-F file] [-stcbvh]\n" );
Abc_Print( -2, "\t generates satisfying assignments for each output of the miter\n" );
Abc_Print( -2, "\t-C num : the number of timeframes [default = %d]\n", nMinCexes );
Abc_Print( -2, "\t-C num : the number of satisfying assignments [default = %d]\n", nMinCexes );
Abc_Print( -2, "\t-M num : the max simulation runs before using SAT [default = %d]\n", nMaxTries );
Abc_Print( -2, "\t-F file : the output file name [default = %s]\n", pFileName );
Abc_Print( -2, "\t-s : toggles using reverse simulation [default = %s]\n", fUseSim ? "yes": "no" );