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

Adding an option to &cec against a previous saved AIG.

This commit is contained in:
Alan Mishchenko 2025-12-19 20:32:11 -08:00
parent c327b83127
commit 64637b8395
1 changed files with 19 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -34838,10 +34838,7 @@ int Abc_CommandAbc9SaveAig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1; return 1;
} }
if ( fClear && pAbc->pGiaSaved != NULL ) if ( fClear && pAbc->pGiaSaved != NULL )
{
Gia_ManStopP( &pAbc->pGiaSaved ); Gia_ManStopP( &pAbc->pGiaSaved );
return 0;
}
if ( fArea && pAbc->pGiaSaved != NULL && Gia_ManAndNum(pAbc->pGiaSaved) <= Gia_ManAndNum(pAbc->pGia) ) if ( fArea && pAbc->pGiaSaved != NULL && Gia_ManAndNum(pAbc->pGiaSaved) <= Gia_ManAndNum(pAbc->pGia) )
return 0; return 0;
if ( !fArea && pAbc->pGiaSaved != NULL && !(Gia_ManLevelNum(pAbc->pGiaSaved) > Gia_ManLevelNum(pAbc->pGia) || (Gia_ManLevelNum(pAbc->pGiaSaved) == Gia_ManLevelNum(pAbc->pGia) && Gia_ManAndNum(pAbc->pGiaSaved) > Gia_ManAndNum(pAbc->pGia))) ) if ( !fArea && pAbc->pGiaSaved != NULL && !(Gia_ManLevelNum(pAbc->pGiaSaved) > Gia_ManLevelNum(pAbc->pGia) || (Gia_ManLevelNum(pAbc->pGiaSaved) == Gia_ManLevelNum(pAbc->pGia) && Gia_ManAndNum(pAbc->pGiaSaved) > Gia_ManAndNum(pAbc->pGia))) )
@ -42276,10 +42273,10 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pFile; FILE * pFile;
Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter; Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter;
char ** pArgvNew; char ** pArgvNew;
int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0; int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0, fSavedSpec = 0;
Cec_ManCecSetDefaultParams( pPars ); Cec_ManCecSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdasxytvwh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdbasxytvwh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -42314,6 +42311,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd': case 'd':
fDualOutput ^= 1; fDualOutput ^= 1;
break; break;
case 'b':
fSavedSpec ^= 1;
break;
case 'a': case 'a':
fDumpMiter ^= 1; fDumpMiter ^= 1;
break; break;
@ -42444,6 +42444,16 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
} }
} }
else if ( fSavedSpec )
{
if ( pAbc->pGiaSaved == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no saved specification.\n" );
return 1;
}
pGias[0] = pAbc->pGia;
pGias[1] = pAbc->pGiaSaved;
}
else else
{ {
char * FileName, * pTemp; char * FileName, * pTemp;
@ -42565,17 +42575,19 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
if ( pGias[0] != pAbc->pGia ) if ( pGias[0] != pAbc->pGia )
Gia_ManStop( pGias[0] ); Gia_ManStop( pGias[0] );
Gia_ManStop( pGias[1] ); if ( pGias[1] != pAbc->pGiaSaved )
Gia_ManStop( pGias[1] );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &cec [-CT num] [-nmdasxytvwh]\n" ); Abc_Print( -2, "usage: &cec [-CT num] [-nmdbasxytvwh]\n" );
Abc_Print( -2, "\t new combinational equivalence checker\n" ); Abc_Print( -2, "\t new combinational equivalence checker\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no"); Abc_Print( -2, "\t-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no");
Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits"); Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no"); Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no");
Abc_Print( -2, "\t-b : toggle using saved specification [default = %s]\n", fSavedSpec? "yes":"no");
Abc_Print( -2, "\t-a : toggle writing dual-output miter [default = %s]\n", fDumpMiter? "yes":"no"); Abc_Print( -2, "\t-a : toggle writing dual-output miter [default = %s]\n", fDumpMiter? "yes":"no");
Abc_Print( -2, "\t-s : toggle silent operation [default = %s]\n", pPars->fSilent ? "yes":"no"); Abc_Print( -2, "\t-s : toggle silent operation [default = %s]\n", pPars->fSilent ? "yes":"no");
Abc_Print( -2, "\t-x : toggle using new solver [default = %s]\n", fUseNewX? "yes":"no"); Abc_Print( -2, "\t-x : toggle using new solver [default = %s]\n", fUseNewX? "yes":"no");