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

Bug fix in handling ufar calls.

This commit is contained in:
Alan Mishchenko 2026-05-11 19:27:06 -07:00
parent 9d410e8163
commit c61f1a04e9
2 changed files with 130 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -51574,7 +51574,7 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pGiaUse = pAbc->pGia, * pGiaTemp = NULL;
Wlc_Ntk_t * pWlc = (Wlc_Ntk_t *)pAbc->pAbcWlc;
char * pReplayFile = NULL, * pUfarArgs = NULL;
char * pReplayFile = NULL, * pUfarArgs = NULL, * pUfarArgsAlloc = NULL;
int c, nProcs = 6, nProcsNew = 0, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PTUCWRusvwh" ) ) != EOF )
@ -51621,8 +51621,22 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-C\" should be followed by a string.\n" );
goto usage;
}
pUfarArgs = argv[globalUtilOptind];
globalUtilOptind++;
{
int iArg, nChars = 0;
ABC_FREE( pUfarArgsAlloc );
for ( iArg = globalUtilOptind; iArg < argc; iArg++ )
nChars += (int)strlen(argv[iArg]) + 1;
pUfarArgsAlloc = ABC_ALLOC( char, nChars + 1 );
pUfarArgsAlloc[0] = 0;
for ( iArg = globalUtilOptind; iArg < argc; iArg++ )
{
if ( iArg > globalUtilOptind )
strcat( pUfarArgsAlloc, " " );
strcat( pUfarArgsAlloc, argv[iArg] );
}
pUfarArgs = pUfarArgsAlloc;
globalUtilOptind = argc;
}
break;
case 'W':
if ( globalUtilOptind >= argc )
@ -51668,18 +51682,21 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pWlc == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no word-level design for option \"-u\".\n" );
ABC_FREE( pUfarArgsAlloc );
return 1;
}
pGiaTemp = Wlc_NtkBitBlast( pWlc, NULL );
if ( pGiaTemp == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9SProve(): Word-level bit-blasting has failed.\n" );
ABC_FREE( pUfarArgsAlloc );
return 1;
}
if ( (Gia_ManPoNum(pGiaTemp) & 1) == 1 )
{
Abc_Print( -1, "Abc_CommandAbc9SProve(): Internal \"&miter -x\" requires even number of bit-level outputs.\n" );
Gia_ManStop( pGiaTemp );
ABC_FREE( pUfarArgsAlloc );
return 1;
}
pGiaUse = Gia_ManTransformMiter2( pGiaTemp );
@ -51689,11 +51706,13 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
else if ( pUfarArgs != NULL )
{
Abc_Print( -1, "Abc_CommandAbc9SProve(): Option \"-C\" requires \"-u\".\n" );
ABC_FREE( pUfarArgsAlloc );
return 1;
}
if ( pGiaUse == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no AIG.\n" );
ABC_FREE( pUfarArgsAlloc );
return 1;
}
if ( Gia_ManRegNum(pGiaUse) == 0 )
@ -51701,12 +51720,14 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9SProve(): The problem is combinational.\n" );
if ( fUseUif )
Gia_ManStop( pGiaUse );
ABC_FREE( pUfarArgsAlloc );
return 1;
}
pAbc->Status = Cec_GiaProveTest( pGiaUse, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile, pUfarArgs );
Abc_FrameReplaceCex( pAbc, &pGiaUse->pCexSeq );
if ( fUseUif )
Gia_ManStop( pGiaUse );
ABC_FREE( pUfarArgsAlloc );
return 0;
usage:
@ -51723,6 +51744,7 @@ usage:
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
ABC_FREE( pUfarArgsAlloc );
return 1;
}

106
src/opt/ufar/UfarCmd.cpp
View File

@ -311,6 +311,104 @@ static bool Ufar_TokenizeArgs( const char * pArgs, vector<string> & Tokens )
return true;
}
static inline void Ufar_TrimString( string & s )
{
while ( !s.empty() && isspace((unsigned char)s.front()) )
s.erase( s.begin() );
while ( !s.empty() && isspace((unsigned char)s.back()) )
s.pop_back();
}
static bool Ufar_ExtractSolverArg( const char * pArgs, string & ArgsWithoutSolver, string & SolverArg )
{
string Args = pArgs ? pArgs : "";
size_t i = 0, n = Args.size();
ArgsWithoutSolver = Args;
SolverArg.clear();
while ( i < n )
{
while ( i < n && isspace((unsigned char)Args[i]) )
i++;
if ( i == n )
break;
size_t TokenStart = i;
char Quote = 0;
string Token;
while ( i < n )
{
unsigned char c = (unsigned char)Args[i];
if ( Quote )
{
if ( c == (unsigned char)Quote )
Quote = 0;
else if ( c == '\\' && i + 1 < n )
Token += Args[++i];
else
Token += (char)c;
i++;
continue;
}
if ( c == '"' || c == '\'' )
{
Quote = (char)c;
i++;
continue;
}
if ( isspace(c) )
break;
if ( c == '\\' && i + 1 < n )
{
Token += Args[++i];
i++;
continue;
}
Token += (char)c;
i++;
}
if ( Token == "--solver" )
{
size_t ValueStart = i;
while ( ValueStart < n && isspace((unsigned char)Args[ValueStart]) )
ValueStart++;
if ( ValueStart == n )
return false;
string Prefix = Args.substr( 0, TokenStart );
string Suffix;
if ( Args[ValueStart] == '"' || Args[ValueStart] == '\'' )
{
char ValueQuote = Args[ValueStart++];
size_t k = ValueStart;
while ( k < n )
{
unsigned char c = (unsigned char)Args[k];
if ( c == (unsigned char)ValueQuote )
{
k++;
break;
}
if ( c == '\\' && k + 1 < n )
SolverArg += Args[++k];
else
SolverArg += (char)c;
k++;
}
Suffix = Args.substr( k );
}
else
{
SolverArg = Args.substr( ValueStart );
}
Ufar_TrimString( SolverArg );
ArgsWithoutSolver = Prefix + Suffix;
Ufar_TrimString( ArgsWithoutSolver );
return !SolverArg.empty();
}
while ( i < n && isspace((unsigned char)Args[i]) )
i++;
}
return false;
}
void Ufar_Init(Abc_Frame_t *pAbc)
{
@ -328,6 +426,7 @@ int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*p
vector<string> Tokens;
vector<char *> Argv;
set<unsigned> set_op_types;
string ArgsWithoutSolver, SolverArg;
string firstAigDumpFile, dumpLogFile;
string statusName;
int fNeedMiter = 1, fCrossStats = 0, UnderSize = -1;
@ -338,9 +437,12 @@ int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*p
Ufar_SetDefaultParams( manager.params, nTimeOut, fVerbose, pFuncStop, RunId );
if ( pArgs && pArgs[0] )
{
const char * pParseArgs = pArgs;
if ( Ufar_ExtractSolverArg(pArgs, ArgsWithoutSolver, SolverArg) )
pParseArgs = ArgsWithoutSolver.c_str();
OptMgr opt_mgr("%ufar");
Ufar_AddOptions( opt_mgr, manager.params );
if ( !Ufar_TokenizeArgs(pArgs, Tokens) )
if ( !Ufar_TokenizeArgs(pParseArgs, Tokens) )
{
cout << "Cannot parse internal %ufar option string." << endl;
return -1;
@ -355,6 +457,8 @@ int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*p
return -1;
}
Ufar_ApplyOptions( opt_mgr, manager.params, set_op_types, firstAigDumpFile, dumpLogFile, fNeedMiter, fCrossStats, UnderSize );
if ( !SolverArg.empty() )
manager.params.solverSetting = SolverArg;
}
else
set_op_types.insert( WLC_OBJ_ARI_MULTI );