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

Extending &sprove interface

This commit is contained in:
Alan Mishchenko 2026-04-25 17:45:55 -07:00
parent 8e6b287674
commit c20832627f
5 changed files with 474 additions and 170 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -686,7 +686,7 @@ extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wr
typedef struct Wlc_Ntk_t_ Wlc_Ntk_t;
typedef struct Wlc_BstPar_t_ Wlc_BstPar_t;
extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars );
extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile );
extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile, char * pUfarArgs );
extern int Cec_GiaReplayReadParams( char * pFileName, int * pnProcs, int * pnTimeOut, int * pnTimeOut2, int * pnTimeOut3, int * pfUseUif );
extern int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, int fVerbose, int fVeryVerbose, int fSilent );
@ -51559,10 +51559,10 @@ 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;
char * pReplayFile = NULL, * pUfarArgs = 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, "PTUWRusvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PTUCWRusvwh" ) ) != EOF )
{
switch ( c )
{
@ -51599,7 +51599,16 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
globalUtilOptind++;
if ( nTimeOut2 <= 0 )
goto usage;
break;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by a string.\n" );
goto usage;
}
pUfarArgs = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'W':
if ( globalUtilOptind >= argc )
{
@ -51662,6 +51671,11 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ManStop( pGiaTemp );
pGiaTemp = NULL;
}
else if ( pUfarArgs != NULL )
{
Abc_Print( -1, "Abc_CommandAbc9SProve(): Option \"-C\" requires \"-u\".\n" );
return 1;
}
if ( pGiaUse == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no AIG.\n" );
@ -51674,18 +51688,19 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ManStop( pGiaUse );
return 1;
}
pAbc->Status = Cec_GiaProveTest( pGiaUse, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile );
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 );
return 0;
usage:
Abc_Print( -2, "usage: &sprove [-PTUW num] [-R file] [-usvwh]\n" );
Abc_Print( -2, "usage: &sprove [-PTUW num] [-C str] [-R file] [-usvwh]\n" );
Abc_Print( -2, "\t proves CEC problem by case-splitting\n" );
Abc_Print( -2, "\t-P num : the number of concurrent processes (1 <= num <= 6) [default = %d]\n", nProcs );
Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-U num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut2 );
Abc_Print( -2, "\t-U num : second-stage timeout in seconds [default = %d]\n", nTimeOut2 );
Abc_Print( -2, "\t-C str : with -u, pass this option string to internal %%ufar\n" );
Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut3 );
Abc_Print( -2, "\t-R str : dump replay/trace file for later execution by &sprove2\n" );
Abc_Print( -2, "\t-u : enable concurrent UFAR on word-level design (uses internal %%blast + &miter -x)\n" );

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

@ -17,6 +17,7 @@
#include <regex>
#include <cstdlib>
#include <cstdio>
#include <cctype>
#include "base/wlc/wlc.h"
#include "aig/gia/giaAig.h"
@ -30,6 +31,14 @@ ABC_NAMESPACE_IMPL_START
using namespace std;
static UFAR::UfarManager ufar_manager;
typedef struct Ufar_StopCtx_t_
{
int (*pFuncStop)(int);
int nTimeOut;
int fActive;
timeval TimeStart;
} Ufar_StopCtx_t;
static __thread Ufar_StopCtx_t g_UfarStopCtx = { NULL, 0, 0, {0, 0} };
static int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAnalyzeCex( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -40,6 +49,38 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Wlc_Ntk_t *)pAbc->pAbcWlc; }
static inline void Wlc_AbcFreeNtk( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc)); }
static inline void Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ) { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk; }
static inline long long Ufar_ElapsedUsec( const timeval & Start, const timeval & Stop ) { return 1000000ll * (long long)(Stop.tv_sec - Start.tv_sec) + (long long)(Stop.tv_usec - Start.tv_usec); }
static int Ufar_StopWithTimeout( int RunId )
{
if ( g_UfarStopCtx.pFuncStop && g_UfarStopCtx.pFuncStop(RunId) )
return 1;
if ( g_UfarStopCtx.fActive && g_UfarStopCtx.nTimeOut > 0 )
{
timeval Now;
gettimeofday( &Now, NULL );
if ( Ufar_ElapsedUsec(g_UfarStopCtx.TimeStart, Now) >= 1000000ll * (long long)g_UfarStopCtx.nTimeOut )
return 1;
}
return 0;
}
struct Ufar_StopScope_t
{
Ufar_StopCtx_t Saved;
Ufar_StopScope_t( int (*pFuncStop)(int), int nTimeOut )
{
Saved = g_UfarStopCtx;
g_UfarStopCtx.pFuncStop = pFuncStop;
g_UfarStopCtx.nTimeOut = nTimeOut;
g_UfarStopCtx.fActive = 1;
gettimeofday( &g_UfarStopCtx.TimeStart, NULL );
}
~Ufar_StopScope_t()
{
g_UfarStopCtx = Saved;
}
};
static string Ufar_GetStatusName( Wlc_Ntk_t * pNtk )
{
@ -74,6 +115,194 @@ static void Ufar_DumpStatusLog( const string & FileName, int RetValue, const str
fclose( pFile );
}
static void Ufar_SetDefaultParams( UFAR::UfarManager::Params & Params, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId )
{
Params = UFAR::UfarManager::Params();
Params.RunId = RunId;
Params.pFuncStop = pFuncStop;
if ( nTimeOut > 0 )
Params.nTimeout = nTimeOut;
Params.iVerbosity = fVerbose ? 1 : 0;
}
static void Ufar_AddOptions( OptMgr & opt_mgr, const UFAR::UfarManager::Params & Params )
{
opt_mgr.AddOpt("--norm", Params.fNorm ? "yes" : "no", "", "toggle using data type normalization");
opt_mgr.AddOpt("--adder", "no", "", "toggle including adders");
opt_mgr.AddOpt("--cexmin", Params.fCexMin ? "yes" : "no", "", "toggle using CEX minimization");
opt_mgr.AddOpt("--sim", "none", "str", "use simulation and specify its setting");
opt_mgr.AddOpt("-v", to_string(Params.iVerbosity), "num", "specify verbosity level");
opt_mgr.AddOpt("--seq", to_string(Params.nSeqLookBack), "num", "specify the number of look-back frames (0 = no sequential UIF)");
opt_mgr.AddOpt("--profile", "no", "", "dump time distribution");
opt_mgr.AddOpt("--pba_uif", Params.fPbaUif ? "yes" : "no", "", "toggle using proof-based refinement for UIF pairs");
opt_mgr.AddOpt("--lazysim", Params.fLazySim ? "yes" : "no", "", "toggle applying UIF pairs based on simulation");
opt_mgr.AddOpt("--pbasim", Params.fPbaSim ? "yes" : "no", "", "toggle combining pba and sim");
opt_mgr.AddOpt("--pbacex", Params.fPbaCex ? "yes" : "no", "", "toggle combining pba and cex");
opt_mgr.AddOpt("--satmin", Params.fSatMin ? "yes" : "no", "", "toggle using sat-min in pba");
opt_mgr.AddOpt("--cbawb", Params.fCbaWb ? "yes" : "no", "", "toggle using cex-based refinement for white boxing");
opt_mgr.AddOpt("--grey", Params.fGrey ? "yes" : "no", "", "toggle using grey-box constraints");
opt_mgr.AddOpt("--grey2", to_string(Params.nGrey), "float", "specify the greyness threshold");
opt_mgr.AddOpt("--allwb", Params.fAllWb ? "yes" : "no", "", "start with all operators white-boxed (no initial abstraction)");
opt_mgr.AddOpt("--crossonly", Params.fCrossOnly ? "yes" : "no", "", "allow UIF pairs only across LHS/RHS cones of the miter");
opt_mgr.AddOpt("--crossstats", "no", "", "print multiplier counts in LHS/RHS/shared cones and exit");
opt_mgr.AddOpt("--dump", "none", "str", "specify file name");
opt_mgr.AddOpt("--dump-log", "none", "str", "write status log");
opt_mgr.AddOpt("--dump-first-aig", "none", "str", "dump first internal bit-blasted AIG and exit");
opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name");
opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers");
opt_mgr.AddOpt("--solver", "none", "str", "external solver command line");
opt_mgr.AddOpt("--dump_states", "none", "str", "specify the name for the states file");
opt_mgr.AddOpt("--read_states", "none", "str", "specify the name for the states file");
opt_mgr.AddOpt("--sp", Params.fSuper_prove ? "yes" : "no", "", "toggle using super_prove");
opt_mgr.AddOpt("--simp", Params.fSimple ? "yes" : "no", "", "toggle using simple (prove)");
opt_mgr.AddOpt("--syn", Params.fSyn ? "yes" : "no", "", "toggle using simple synthesis");
opt_mgr.AddOpt("--pth", Params.fPthread ? "yes" : "no", "", "toggle using pthreads");
opt_mgr.AddOpt("--onewb", to_string(Params.iOneWb), "int", "specify the mode for one-white-boxing");
opt_mgr.AddOpt("--initallpairs", to_string(Params.nInitAllPairsLimit), "num", "pre-seed all compatible UIF pairs when #ops <= this limit (0=off)");
opt_mgr.AddOpt("--initnear", to_string(Params.nInitNearMults), "num", "pre-seed UIF pairs among up to this many multipliers closest to output");
opt_mgr.AddOpt("--timeout", to_string(Params.nTimeout), "num", "specify the timeout (sec)");
opt_mgr.AddOpt("--exp", to_string(Params.iExp), "int", "specify the exp mode");
opt_mgr.AddOpt("--miter", "yes", "", "toggle mitering the problem");
opt_mgr.AddOpt("--under", "-1", "num", "try under-approximation with the given size");
}
static void Ufar_ApplyOptions( OptMgr & opt_mgr, UFAR::UfarManager::Params & Params, set<unsigned> & set_op_types, string & firstAigDumpFile, string & dumpLogFile, int & fNeedMiter, int & fCrossStats, int & UnderSize )
{
firstAigDumpFile = "";
dumpLogFile = opt_mgr["--dump-log"] ? opt_mgr.GetOptVal("--dump-log") : "";
fNeedMiter = !opt_mgr["--miter"];
fCrossStats = opt_mgr["--crossstats"] ? 1 : 0;
UnderSize = opt_mgr["--under"] ? stoi(opt_mgr.GetOptVal("--under")) : -1;
if(opt_mgr["--norm"])
Params.fNorm ^= 1;
if(opt_mgr["--cexmin"])
Params.fCexMin ^= 1;
if(opt_mgr["--pba_uif"])
Params.fPbaUif ^= 1;
if(opt_mgr["--pbasim"])
Params.fPbaSim ^= 1;
if(opt_mgr["--pbacex"])
Params.fPbaCex ^= 1;
if(opt_mgr["--satmin"])
Params.fSatMin ^= 1;
if(opt_mgr["--cbawb"])
Params.fCbaWb ^= 1;
if(opt_mgr["--grey"])
Params.fGrey ^= 1;
if(opt_mgr["--allwb"])
Params.fAllWb ^= 1;
if(opt_mgr["--crossonly"])
Params.fCrossOnly ^= 1;
if(opt_mgr["--grey2"])
Params.nGrey = stof(opt_mgr.GetOptVal("--grey2"));
if(opt_mgr["--sp"])
Params.fSuper_prove ^= 1;
if(opt_mgr["--simp"])
Params.fSimple ^= 1;
if(opt_mgr["--syn"])
Params.fSyn ^= 1;
if(opt_mgr["--pth"])
Params.fPthread ^= 1;
if(opt_mgr["--onewb"])
Params.iOneWb = stoi(opt_mgr.GetOptVal("--onewb"));
if(opt_mgr["--initallpairs"])
Params.nInitAllPairsLimit = stoi(opt_mgr.GetOptVal("--initallpairs"));
if(opt_mgr["--initnear"])
Params.nInitNearMults = stoi(opt_mgr.GetOptVal("--initnear"));
if(opt_mgr["--exp"])
Params.iExp = stoi(opt_mgr.GetOptVal("--exp"));
if(opt_mgr["--par"])
Params.parSetting = opt_mgr.GetOptVal("--par");
if(opt_mgr["--solver"])
Params.solverSetting = opt_mgr.GetOptVal("--solver");
if(opt_mgr["--sim"])
Params.simSetting = opt_mgr.GetOptVal("--sim");
if(opt_mgr["--dump_states"]) {
smatch sub_match;
string option = opt_mgr.GetOptVal("--dump_states");
if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
Params.fileStatesOut = sub_match[1].str();
else
Params.fileStatesOut = opt_mgr.GetOptVal("--dump_states");
}
if(opt_mgr["--read_states"])
Params.fileStatesIn = opt_mgr.GetOptVal("--read_states");
if(opt_mgr["--lazysim"])
Params.fLazySim ^= 1;
if(opt_mgr["-v"])
Params.iVerbosity = stoi(opt_mgr.GetOptVal("-v"));
if(opt_mgr["--timeout"])
Params.nTimeout = stoi(opt_mgr.GetOptVal("--timeout"));
if(opt_mgr["--seq"])
Params.nSeqLookBack = stoi(opt_mgr.GetOptVal("--seq"));
if(opt_mgr["--dump-abs"]) {
smatch sub_match;
string option = opt_mgr.GetOptVal("--dump-abs");
if(regex_search(option, sub_match, regex(R"(/?(\w+)\.v$)")))
Params.fileAbs = sub_match[1].str();
else
Params.fileAbs = opt_mgr.GetOptVal("--dump-abs");
}
if(opt_mgr["--dump"]) {
smatch sub_match;
string option = opt_mgr.GetOptVal("--dump");
if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
Params.fileName = sub_match[1].str();
else
Params.fileName = opt_mgr.GetOptVal("--dump");
}
if ( opt_mgr["--dump-first-aig"] )
firstAigDumpFile = opt_mgr.GetOptVal("--dump-first-aig");
set_op_types.insert(WLC_OBJ_ARI_MULTI);
if (opt_mgr["--adder"])
set_op_types.insert(WLC_OBJ_ARI_ADD);
}
static bool Ufar_TokenizeArgs( const char * pArgs, vector<string> & Tokens )
{
string Cur;
char Quote = 0;
if ( pArgs == NULL )
return true;
for ( ; *pArgs; ++pArgs )
{
unsigned char c = (unsigned char)*pArgs;
if ( Quote )
{
if ( c == (unsigned char)Quote )
Quote = 0;
else if ( c == '\\' && pArgs[1] )
Cur += *++pArgs;
else
Cur += (char)c;
continue;
}
if ( c == '"' || c == '\'' )
{
Quote = (char)c;
continue;
}
if ( isspace(c) )
{
if ( !Cur.empty() )
{
Tokens.push_back( Cur );
Cur.clear();
}
continue;
}
if ( c == '\\' && pArgs[1] )
{
Cur += *++pArgs;
continue;
}
Cur += (char)c;
}
if ( Quote )
return false;
if ( !Cur.empty() )
Tokens.push_back( Cur );
return true;
}
void Ufar_Init(Abc_Frame_t *pAbc)
{
@ -84,39 +313,163 @@ void Ufar_Init(Abc_Frame_t *pAbc)
//Cmd_CommandAdd( pAbc, "Word level Prove", "%%miter", Abc_CommandCreateMiter, 0 );
}
int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId )
int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs )
{
UFAR::UfarManager manager;
timeval t1;
vector<string> Tokens;
vector<char *> Argv;
set<unsigned> set_op_types;
Wlc_Ntk_t * pUse = pNtk;
string firstAigDumpFile, dumpLogFile;
string statusName;
int fNeedMiter = 1, fCrossStats = 0, UnderSize = -1;
Wlc_Ntk_t * pUse = pNtk, * pNew = NULL;
int RetValue = -1;
if ( pNtk == NULL )
return -1;
if ( Wlc_NtkPoNum(pUse) == 2 )
Ufar_SetDefaultParams( manager.params, nTimeOut, fVerbose, pFuncStop, RunId );
if ( pArgs && pArgs[0] )
{
pUse = UFAR::CreateMiter( pUse, 0 );
if ( pUse == NULL )
OptMgr opt_mgr("%ufar");
Ufar_AddOptions( opt_mgr, manager.params );
if ( !Ufar_TokenizeArgs(pArgs, Tokens) )
{
cout << "Cannot parse internal %ufar option string." << endl;
return -1;
}
Argv.reserve( Tokens.size() + 1 );
Argv.push_back( (char *)"%ufar" );
for ( size_t i = 0; i < Tokens.size(); i++ )
Argv.push_back( (char *)Tokens[i].c_str() );
if ( !opt_mgr.Parse((int)Argv.size(), Argv.data()) )
{
opt_mgr.PrintUsage();
return -1;
}
Ufar_ApplyOptions( opt_mgr, manager.params, set_op_types, firstAigDumpFile, dumpLogFile, fNeedMiter, fCrossStats, UnderSize );
}
else
set_op_types.insert( WLC_OBJ_ARI_MULTI );
Ufar_StopScope_t StopScope( manager.params.pFuncStop, (int)manager.params.nTimeout );
manager.params.pFuncStop = Ufar_StopWithTimeout;
if ( fNeedMiter )
{
if ( Wlc_NtkPoNum(pUse) == 2 )
{
pNew = UFAR::CreateMiter( pUse, 0 );
if ( pUse != pNtk )
Wlc_NtkFree( pUse );
pUse = pNew;
if ( pUse == NULL )
return -1;
}
else if ( Wlc_NtkPoNum(pUse) != 1 )
{
return -1;
}
}
else if ( Wlc_NtkPoNum(pUse) != 1 )
return -1;
set_op_types.insert( WLC_OBJ_ARI_MULTI );
statusName = Ufar_GetStatusName( pUse );
if ( manager.params.fNorm )
{
pNew = UFAR::NormalizeDataTypes( pUse, set_op_types, true );
if ( pUse != pNtk )
Wlc_NtkFree( pUse );
pUse = pNew;
}
if ( fCrossStats )
{
Wlc_Ntk_t * pCur = pUse;
if ( Wlc_NtkPoNum(pCur) != 2 )
{
cout << "CrossStats requires dual outputs before mitering.\n";
if ( pUse != pNtk )
Wlc_NtkFree( pUse );
return -1;
}
int nObjs = Wlc_NtkObjNumMax(pCur);
vector<char> vConeL(nObjs, 0), vConeR(nObjs, 0);
auto mark_cone = [&]( int iStart, vector<char>& vMark )
{
if ( iStart < 0 || iStart >= nObjs )
return;
vector<int> stack(1, iStart);
while ( !stack.empty() )
{
int iObj = stack.back();
stack.pop_back();
if ( iObj < 0 || iObj >= nObjs || vMark[iObj] )
continue;
vMark[iObj] = 1;
Wlc_Obj_t * pObjT = Wlc_NtkObj(pCur, iObj);
if ( pObjT->Type == WLC_OBJ_FO )
{
Wlc_Obj_t * pFi = Wlc_ObjFo2Fi(pCur, pObjT);
stack.push_back( Wlc_ObjId(pCur, pFi) );
}
int iFanin, k;
Wlc_ObjForEachFanin( pObjT, iFanin, k )
stack.push_back(iFanin);
}
};
int iRootL = Wlc_ObjFaninId0( Wlc_NtkPo(pCur, 0) );
int iRootR = Wlc_ObjFaninId0( Wlc_NtkPo(pCur, 1) );
mark_cone(iRootL, vConeL);
mark_cone(iRootR, vConeR);
int nL = 0, nR = 0, nB = 0, nN = 0;
Wlc_Obj_t * pObjT; int iObj;
Wlc_NtkForEachObj( pCur, pObjT, iObj )
{
if ( pObjT->Type != WLC_OBJ_ARI_MULTI )
continue;
bool fL = vConeL[iObj] != 0;
bool fR = vConeR[iObj] != 0;
if ( fL && fR ) nB++;
else if ( fL ) nL++;
else if ( fR ) nR++;
else nN++;
}
cout << "UIF_PROVE : CrossStats: L=" << nL
<< " R=" << nR
<< " BOTH=" << nB
<< " NONE=" << nN
<< " TOTAL=" << (nL + nR + nB + nN) << endl;
if ( pUse != pNtk )
Wlc_NtkFree( pUse );
return -1;
}
if ( !UFAR::HasOperator( pUse, set_op_types ) )
{
if ( pUse != pNtk )
Wlc_NtkFree( pUse );
return -1;
}
manager.params = UFAR::UfarManager::Params();
manager.params.RunId = RunId;
manager.params.pFuncStop = pFuncStop;
if ( nTimeOut > 0 )
manager.params.nTimeout = nTimeOut;
manager.params.iVerbosity = fVerbose ? 1 : 0;
if ( UnderSize >= 0 )
{
pNew = UFAR::MakeUnderApprox( pUse, UnderSize );
if ( pUse != pNtk )
Wlc_NtkFree( pUse );
pUse = pNew;
pNew = UFAR::MakeUnderApprox2( pUse, set_op_types, UnderSize );
if ( pUse != pNtk )
Wlc_NtkFree( pUse );
pUse = pNew;
}
if ( !firstAigDumpFile.empty() && firstAigDumpFile != "none" )
{
Gia_Man_t * pGia = UFAR::BitBlast( pUse );
Gia_AigerWriteSimple( pGia, (char *)firstAigDumpFile.c_str() );
Gia_ManStop( pGia );
if ( pUse != pNtk )
Wlc_NtkFree( pUse );
return -1;
}
gettimeofday( &t1, NULL );
manager.Initialize( pUse, set_op_types );
RetValue = manager.PerformUIFProve( t1 );
Ufar_DumpStatusLog( dumpLogFile, RetValue, statusName );
if ( pUse != pNtk )
Wlc_NtkFree( pUse );
return RetValue;
@ -160,141 +513,22 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
ufar_manager.params = UFAR::UfarManager::Params();
OptMgr opt_mgr(argv[0]);
opt_mgr.AddOpt("--norm", ufar_manager.params.fNorm ? "yes" : "no", "", "toggle using data type normalization");
opt_mgr.AddOpt("--adder", "no", "", "toggle including adders");
opt_mgr.AddOpt("--cexmin", ufar_manager.params.fCexMin ? "yes" : "no", "", "toggle using CEX minimization");
opt_mgr.AddOpt("--sim", "none", "str", "use simulation and specify its setting");
opt_mgr.AddOpt("-v", to_string(ufar_manager.params.iVerbosity), "num", "specify verbosity level");
opt_mgr.AddOpt("--seq", to_string(ufar_manager.params.nSeqLookBack), "num", "specify the number of look-back frames (0 = no sequential UIF)");
opt_mgr.AddOpt("--profile", "no", "", "dump time distribution");
opt_mgr.AddOpt("--pba_uif", ufar_manager.params.fPbaUif ? "yes" : "no", "", "toggle using proof-based refinement for UIF pairs");
opt_mgr.AddOpt("--lazysim", ufar_manager.params.fLazySim ? "yes" : "no", "", "toggle applying UIF pairs based on simulation");
opt_mgr.AddOpt("--pbasim", ufar_manager.params.fPbaSim ? "yes" : "no", "", "toggle combining pba and sim");
opt_mgr.AddOpt("--pbacex", ufar_manager.params.fPbaCex ? "yes" : "no", "", "toggle combining pba and cex");
opt_mgr.AddOpt("--satmin", ufar_manager.params.fSatMin ? "yes" : "no", "", "toggle using sat-min in pba");
opt_mgr.AddOpt("--cbawb", ufar_manager.params.fCbaWb ? "yes" : "no", "", "toggle using cex-based refinement for white boxing");
opt_mgr.AddOpt("--grey", ufar_manager.params.fGrey ? "yes" : "no", "", "toggle using grey-box constraints");
opt_mgr.AddOpt("--grey2", to_string(ufar_manager.params.nGrey), "float", "specify the greyness threshold");
opt_mgr.AddOpt("--allwb", ufar_manager.params.fAllWb ? "yes" : "no", "", "start with all operators white-boxed (no initial abstraction)");
opt_mgr.AddOpt("--crossonly", ufar_manager.params.fCrossOnly ? "yes" : "no", "", "allow UIF pairs only across LHS/RHS cones of the miter");
opt_mgr.AddOpt("--crossstats", "no", "", "print multiplier counts in LHS/RHS/shared cones and exit");
opt_mgr.AddOpt("--dump", "none", "str", "specify file name");
opt_mgr.AddOpt("--dump-log", "none", "str", "write status log");
opt_mgr.AddOpt("--dump-first-aig", "none", "str", "dump first internal bit-blasted AIG and exit");
opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name");
opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers");
opt_mgr.AddOpt("--solver", "none", "str", "external solver command line");
opt_mgr.AddOpt("--dump_states", "none", "str", "specify the name for the states file");
opt_mgr.AddOpt("--read_states", "none", "str", "specify the name for the states file");
opt_mgr.AddOpt("--sp", ufar_manager.params.fSuper_prove ? "yes" : "no", "", "toggle using super_prove");
opt_mgr.AddOpt("--simp", ufar_manager.params.fSimple ? "yes" : "no", "", "toggle using simple (prove)");
opt_mgr.AddOpt("--syn", ufar_manager.params.fSyn ? "yes" : "no", "", "toggle using simple synthesis");
opt_mgr.AddOpt("--pth", ufar_manager.params.fPthread ? "yes" : "no", "", "toggle using pthreads");
opt_mgr.AddOpt("--onewb", to_string(ufar_manager.params.iOneWb), "int", "specify the mode for one-white-boxing");
opt_mgr.AddOpt("--initallpairs", to_string(ufar_manager.params.nInitAllPairsLimit), "num", "pre-seed all compatible UIF pairs when #ops <= this limit (0=off)");
opt_mgr.AddOpt("--initnear", to_string(ufar_manager.params.nInitNearMults), "num", "pre-seed UIF pairs among up to this many multipliers closest to output");
opt_mgr.AddOpt("--timeout", to_string(ufar_manager.params.nTimeout), "num", "specify the timeout (sec)");
opt_mgr.AddOpt("--exp", to_string(ufar_manager.params.iExp), "int", "specify the exp mode");
opt_mgr.AddOpt("--miter", "yes", "", "toggle mitering the problem");
opt_mgr.AddOpt("--under", "-1", "num", "try under-approximation with the given size");
set<unsigned> set_op_types;
string firstAigDumpFile = "";
string dumpLogFile = "";
int fNeedMiter = 1, fCrossStats = 0, UnderSize = -1;
Ufar_AddOptions( opt_mgr, ufar_manager.params );
if(!opt_mgr.Parse(argc, argv)) {
opt_mgr.PrintUsage();
cout << "\n This command was developed by Yen-Sheng Ho at UC Berkeley in 2015.\n";
cout << " https://people.eecs.berkeley.edu/~alanmi/publications/2016/fmcad16_uif.pdf \n";
return 0;
}
if(opt_mgr["--norm"])
ufar_manager.params.fNorm ^= 1;
if(opt_mgr["--cexmin"])
ufar_manager.params.fCexMin ^= 1;
if(opt_mgr["--pba_uif"])
ufar_manager.params.fPbaUif ^= 1;
if(opt_mgr["--pbasim"])
ufar_manager.params.fPbaSim ^= 1;
if(opt_mgr["--pbacex"])
ufar_manager.params.fPbaCex ^= 1;
if(opt_mgr["--satmin"])
ufar_manager.params.fSatMin ^= 1;
if(opt_mgr["--cbawb"])
ufar_manager.params.fCbaWb ^= 1;
if(opt_mgr["--grey"])
ufar_manager.params.fGrey ^= 1;
if(opt_mgr["--allwb"])
ufar_manager.params.fAllWb ^= 1;
if(opt_mgr["--crossonly"])
ufar_manager.params.fCrossOnly ^= 1;
if(opt_mgr["--grey2"])
ufar_manager.params.nGrey = stof(opt_mgr.GetOptVal("--grey2"));
if(opt_mgr["--sp"])
ufar_manager.params.fSuper_prove ^= 1;
if(opt_mgr["--simp"])
ufar_manager.params.fSimple ^= 1;
if(opt_mgr["--syn"])
ufar_manager.params.fSyn ^= 1;
if(opt_mgr["--pth"])
ufar_manager.params.fPthread ^= 1;
if(opt_mgr["--onewb"])
ufar_manager.params.iOneWb = stoi(opt_mgr.GetOptVal("--onewb"));
if(opt_mgr["--initallpairs"])
ufar_manager.params.nInitAllPairsLimit = stoi(opt_mgr.GetOptVal("--initallpairs"));
if(opt_mgr["--initnear"])
ufar_manager.params.nInitNearMults = stoi(opt_mgr.GetOptVal("--initnear"));
if(opt_mgr["--exp"])
ufar_manager.params.iExp = stoi(opt_mgr.GetOptVal("--exp"));
if(opt_mgr["--par"])
ufar_manager.params.parSetting = opt_mgr.GetOptVal("--par");
if(opt_mgr["--solver"])
ufar_manager.params.solverSetting = opt_mgr.GetOptVal("--solver");
if(opt_mgr["--sim"])
ufar_manager.params.simSetting = opt_mgr.GetOptVal("--sim");
if(opt_mgr["--dump_states"]) {
smatch sub_match;
string option = opt_mgr.GetOptVal("--dump_states");
if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
ufar_manager.params.fileStatesOut = sub_match[1].str();
else
ufar_manager.params.fileStatesOut = opt_mgr.GetOptVal("--dump_states");
}
if(opt_mgr["--read_states"])
ufar_manager.params.fileStatesIn = opt_mgr.GetOptVal("--read_states");
if(opt_mgr["--lazysim"])
ufar_manager.params.fLazySim ^= 1;
if(opt_mgr["-v"])
ufar_manager.params.iVerbosity = stoi(opt_mgr.GetOptVal("-v"));
if(opt_mgr["--timeout"])
ufar_manager.params.nTimeout = stoi(opt_mgr.GetOptVal("--timeout"));
if(opt_mgr["--seq"])
ufar_manager.params.nSeqLookBack = stoi(opt_mgr.GetOptVal("--seq"));
if(opt_mgr["--dump-abs"]) {
smatch sub_match;
string option = opt_mgr.GetOptVal("--dump-abs");
if(regex_search(option, sub_match, regex(R"(/?(\w+)\.v$)")))
ufar_manager.params.fileAbs = sub_match[1].str();
else
ufar_manager.params.fileAbs = opt_mgr.GetOptVal("--dump-abs");
}
if(opt_mgr["--dump"]) {
smatch sub_match;
string option = opt_mgr.GetOptVal("--dump");
if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
ufar_manager.params.fileName = sub_match[1].str();
else
ufar_manager.params.fileName = opt_mgr.GetOptVal("--dump");
}
string firstAigDumpFile = "";
if ( opt_mgr["--dump-first-aig"] )
firstAigDumpFile = opt_mgr.GetOptVal("--dump-first-aig");
Ufar_ApplyOptions( opt_mgr, ufar_manager.params, set_op_types, firstAigDumpFile, dumpLogFile, fNeedMiter, fCrossStats, UnderSize );
// ufar_manager.DumpParams();
LogT::prefix = "UIF_PROVE";
string dumpLogFile = opt_mgr["--dump-log"] ? opt_mgr.GetOptVal("--dump-log") : "";
string statusName = Ufar_GetStatusName( Wlc_AbcGetNtk(pAbc) );
set<unsigned> set_op_types;
set_op_types.insert(WLC_OBJ_ARI_MULTI);
if (opt_mgr["--adder"])
set_op_types.insert(WLC_OBJ_ARI_ADD);
if (!UFAR::HasOperator(Wlc_AbcGetNtk(pAbc), set_op_types)) {
cout << "There is no operator for UIF.\n";
return 0;
@ -304,7 +538,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
timeval t1, t2;
gettimeofday(&t1, NULL);
if (!opt_mgr["--miter"]) {
if (fNeedMiter) {
if (Wlc_NtkPoNum(Wlc_AbcGetNtk(pAbc)) != 2) {
cout << "The current design doesn't have dual outputs.\n";
return 0;
@ -318,7 +552,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
Wlc_AbcUpdateNtk(pAbc, pNew);
}
if ( opt_mgr["--crossstats"] )
if ( fCrossStats )
{
Wlc_Ntk_t * pCur = Wlc_AbcGetNtk(pAbc);
if ( Wlc_NtkPoNum(pCur) != 2 )
@ -380,10 +614,10 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
return 0;
}
if (opt_mgr["--under"]) {
pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), stoi(opt_mgr.GetOptVal("--under")));
if ( UnderSize >= 0 ) {
pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), UnderSize);
Wlc_AbcUpdateNtk(pAbc, pNew);
pNew = UFAR::MakeUnderApprox2(Wlc_AbcGetNtk(pAbc), set_op_types, stoi(opt_mgr.GetOptVal("--under")));
pNew = UFAR::MakeUnderApprox2(Wlc_AbcGetNtk(pAbc), set_op_types, UnderSize);
Wlc_AbcUpdateNtk(pAbc, pNew);
Wlc_WriteVer(Wlc_AbcGetNtk(pAbc), "UND.v", 0, 0);
}

2
src/opt/ufar/UfarCmd.h
View File

@ -15,7 +15,7 @@ ABC_NAMESPACE_HEADER_START
void Ufar_Init(Abc_Frame_t *pAbc);
typedef struct Wlc_Ntk_t_ Wlc_Ntk_t;
extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId );
extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs );
ABC_NAMESPACE_HEADER_END

24
src/opt/untk/NtkNtk.cpp
View File

@ -805,7 +805,8 @@ Wlc_Ntk_t * AddConstFlops( Wlc_Ntk_t * pNtk, const set<unsigned>& types )
Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple(pNtk);
Wlc_NtkCleanCopy( p );
int nOrigObjNum = Wlc_NtkObjNumMax(p);
Wlc_NtkTransferNames( p, pNtk );
if ( !Wlc_NtkHasNameId(p) && Wlc_NtkHasNameId(pNtk) )
Wlc_NtkTransferNames( p, pNtk );
Wlc_Obj_t * pObj;
int i, iObjConst0;
@ -872,7 +873,8 @@ Wlc_Ntk_t * AddConstFlops( Wlc_Ntk_t * pNtk, const set<unsigned>& types )
ModifyMarkedNodes(p, nOrigObjNum, create_ff_and_mux);
Wlc_Ntk_t * pNew = Wlc_NtkDupDfsSimple( p );
Wlc_NtkTransferNames( pNew, p );
if ( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(p) )
Wlc_NtkTransferNames( pNew, p );
Wlc_NtkFree( p );
@ -1058,7 +1060,8 @@ Wlc_Ntk_t * NormalizeDataTypes(Wlc_Ntk_t * p, const set<unsigned>& types, bool f
Wlc_Ntk_t *pNtk, *pNew;
pNtk = Wlc_NtkDupDfsSimple(p);
Wlc_NtkTransferNames( pNtk, p );
if ( !Wlc_NtkHasNameId(pNtk) && Wlc_NtkHasNameId(p) )
Wlc_NtkTransferNames( pNtk, p );
Wlc_Obj_t *pObj;
int i, iFanin0, iFanin1;
@ -1117,7 +1120,8 @@ Wlc_Ntk_t * NormalizeDataTypes(Wlc_Ntk_t * p, const set<unsigned>& types, bool f
Vec_IntFree(vFanins);
pNew = Wlc_NtkDupDfsSimple(pNtk);
Wlc_NtkTransferNames( pNew, pNtk );
if ( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(pNtk) )
Wlc_NtkTransferNames( pNew, pNtk );
Wlc_NtkFree(pNtk);
return pNew;
@ -1266,11 +1270,15 @@ static inline int run_external_solver_on_aig( Abc_Ntk_t * pAbcNtk, const string&
Io_Write( pAbcNtk, (char *)pAigFile, IO_FILE_AIGER );
std::remove( "status.txt" );
std::remove( "log.txt" );
string command = solverCmd;
if ( command.find(pAigFile) == string::npos )
command += string(" ") + pAigFile;
string solverCall = solverCmd;
string command;
if ( solverCall.find(pAigFile) == string::npos )
solverCall += string(" ") + pAigFile;
if ( nRuntimeLimitSec > 0 )
command += " " + to_string(nRuntimeLimitSec);
solverCall += " " + to_string(nRuntimeLimitSec);
command = solverCall;
if ( nRuntimeLimitSec > 0 )
command = "timeout " + to_string(nRuntimeLimitSec) + " " + command;
command += " > log.txt 2>&1";
LOG(1) << "UFAR external solver: launching command instead of PDR: " << command;
int res = system( command.c_str() );

71
src/proof/cec/cecProve.c
View File

@ -61,15 +61,15 @@ struct Cec_SproveTrace_t_;
static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result );
static Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
static Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, struct Cec_SproveTrace_t_ * pTrace );
static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, const char * pUfarArgs, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, struct Cec_SproveTrace_t_ * pTrace );
static void Cec_GiaStopThreads( Par_ThData_t * ThData, pthread_t * WorkerThread, int nWorkers );
static int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine );
extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId );
extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs );
#ifndef ABC_USE_PTHREADS
int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile ) { return -1; }
int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile, char * pUfarArgs ) { return -1; }
int Cec_GiaReplayReadParams( char * pFileName, int * pnProcs, int * pnTimeOut, int * pnTimeOut2, int * pnTimeOut3, int * pfUseUif ) { return 0; }
int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; }
@ -104,6 +104,7 @@ typedef struct Par_ThData_t_
int fVerbose;
int nTimeOutU;
Wlc_Ntk_t * pWlc;
const char * pUfarArgs;
int WorkerId;
int StageId;
int NetId;
@ -152,6 +153,7 @@ struct Cec_SprovePlan_t_
int nTimeOut2;
int nTimeOut3;
int fUseUif;
char * pUfarArgs;
int nStages;
Cec_SproveStage_t Stages[SPROVE_STAGE_MAX];
};
@ -309,6 +311,13 @@ static void Cec_SproveDeriveEngineList( int nProcs, int fUseUif, int * pEngines,
{
int i, nEngines = nProcs + (fUseUif ? 1 : 0);
assert( nEngines >= 1 && nEngines <= PAR_THR_MAX );
if ( fUseUif && nProcs == 6 )
{
int UifEngines[7] = { 0, 1, 2, 3, 4, PAR_ENGINE_GLA, PAR_ENGINE_UFAR };
memcpy( pEngines, UifEngines, sizeof(UifEngines) );
*pnEngines = 7;
return;
}
for ( i = 0; i < nEngines; i++ )
{
if ( fUseUif && i == nEngines - 1 )
@ -320,7 +329,25 @@ static void Cec_SproveDeriveEngineList( int nProcs, int fUseUif, int * pEngines,
}
*pnEngines = nEngines;
}
static void Cec_SprovePlanDefault( Cec_SprovePlan_t * pPlan, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif )
static void Cec_SproveTrimLineEnd( char * pLine )
{
int nSize = strlen( pLine );
while ( nSize > 0 && (pLine[nSize - 1] == '\n' || pLine[nSize - 1] == '\r') )
pLine[--nSize] = 0;
}
static void Cec_SprovePlanSetUfarArgs( Cec_SprovePlan_t * pPlan, const char * pUfarArgs )
{
ABC_FREE( pPlan->pUfarArgs );
pPlan->pUfarArgs = NULL;
if ( pUfarArgs && pUfarArgs[0] )
pPlan->pUfarArgs = Abc_UtilStrsav( (char *)pUfarArgs );
}
static void Cec_SprovePlanFree( Cec_SprovePlan_t * pPlan )
{
ABC_FREE( pPlan->pUfarArgs );
pPlan->pUfarArgs = NULL;
}
static void Cec_SprovePlanDefault( Cec_SprovePlan_t * pPlan, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, const char * pUfarArgs )
{
int nEngines;
memset( pPlan, 0, sizeof(Cec_SprovePlan_t) );
@ -334,6 +361,7 @@ static void Cec_SprovePlanDefault( Cec_SprovePlan_t * pPlan, int nProcs, int nTi
pPlan->nTimeOut2 = nTimeOut2;
pPlan->nTimeOut3 = nTimeOut3;
pPlan->fUseUif = fUseUif;
Cec_SprovePlanSetUfarArgs( pPlan, pUfarArgs );
pPlan->nStages = 4;
Cec_SproveDeriveEngineList( nProcs, fUseUif, pPlan->Stages[0].RoundEngines, &nEngines );
@ -408,6 +436,8 @@ static void Cec_SproveTraceOpen( Cec_SproveTrace_t * pTrace, Gia_Man_t * p, Cec_
Cec_SproveTraceWrite( pTrace, "SPROVE_REPLAY 1" );
Cec_SproveTraceWrite( pTrace, "CASE %s", pProbName ? pProbName : "(none)" );
Cec_SproveTraceWrite( pTrace, "PARAMS P=%d T=%d U=%d W=%d UIF=%d", pPlan->nProcs, pPlan->nTimeOut, pPlan->nTimeOut2, pPlan->nTimeOut3, pPlan->fUseUif );
if ( pPlan->pUfarArgs && pPlan->pUfarArgs[0] )
Cec_SproveTraceWrite( pTrace, "UFAR_ARGS %s", pPlan->pUfarArgs );
Cec_SproveTraceWrite( pTrace, "" );
Cec_SproveTraceWrite( pTrace, "PLAN_BEGIN" );
for ( i = 0; i < pPlan->nStages; i++ )
@ -479,12 +509,20 @@ static int Cec_SproveReplayReadParamsInt( char * pFileName, Cec_SprovePlan_t * p
pPlan->nTimeOut3 = atoi(Value);
if ( !Cec_SproveFindValue(Buffer, "UIF=", Value, sizeof(Value)) ) break;
pPlan->fUseUif = atoi(Value);
}
else if ( strncmp(Buffer, "UFAR_ARGS ", 10) == 0 )
{
Cec_SproveTrimLineEnd( Buffer );
Cec_SprovePlanSetUfarArgs( pPlan, Buffer + 10 );
}
else if ( pPlan->nProcs > 0 && (strncmp(Buffer, "PLAN_BEGIN", 10) == 0 || strncmp(Buffer, "OBSERVED_BEGIN", 14) == 0) )
{
fclose( pFile );
return 1;
}
}
fclose( pFile );
return 0;
return pPlan->nProcs > 0;
}
static int Cec_SproveReplayReadPlan( char * pFileName, Cec_SprovePlan_t * pPlan )
{
@ -717,7 +755,7 @@ static int Cec_SproveExecutePlan( Gia_Man_t * p, Cec_SprovePlan_t * pPlan, Wlc_N
}
Cec_SproveTraceWrite( &Trace, "START kind=round stage=%d net=%s timeout=%d t=%llu",
pStage->Id, Cec_SproveNetName(pStage->RoundNet), pStage->RoundTimeout, Cec_SproveClockToMs( Cec_SproveTraceTime(&Trace) ) );
Cec_GiaInitThreads( ThData, pStage->nRoundEngines, pRoundNet, pStage->RoundTimeout, pPlan->nTimeOut3, pWlc, fVerbose,
Cec_GiaInitThreads( ThData, pStage->nRoundEngines, pRoundNet, pStage->RoundTimeout, pStage->RoundTimeout, pWlc, pPlan->pUfarArgs, fVerbose,
fThreadsStarted ? NULL : WorkerThread, &Share, pStage->RoundEngines, pStage->Id, pStage->RoundNet, &Trace );
fThreadsStarted = 1;
}
@ -918,7 +956,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
if ( pThData && pThData->pWlc )
{
g_pUfarShare = pThData->pShare;
RetValue = Ufar_ProveWithTimeout( pThData->pWlc, pThData->nTimeOutU, fVerbose, Cec_SProveStopUfar, 0 );
RetValue = Ufar_ProveWithTimeout( pThData->pWlc, pThData->nTimeOutU, fVerbose, Cec_SProveStopUfar, 0, pThData->pUfarArgs );
g_pUfarShare = NULL;
}
}
@ -1070,7 +1108,7 @@ static void Cec_GiaStartThreads( Par_ThData_t * ThData, int nWorkers )
assert( status == 0 );
}
}
static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, Cec_SproveTrace_t * pTrace )
static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, const char * pUfarArgs, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, Cec_SproveTrace_t * pTrace )
{
int i, status;
assert( nWorkers <= PAR_THR_MAX );
@ -1088,6 +1126,7 @@ static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t *
ThData[i].fVerbose = fVerbose;
ThData[i].nTimeOutU= nTimeOutU;
ThData[i].pWlc = pWlc;
ThData[i].pUfarArgs= pUfarArgs;
ThData[i].WorkerId = i;
ThData[i].StageId = StageId;
ThData[i].NetId = NetId;
@ -1115,6 +1154,7 @@ static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t *
ThData[i].fVerbose = fVerbose;
ThData[i].nTimeOutU= nTimeOutU;
ThData[i].pWlc = pWlc;
ThData[i].pUfarArgs= pUfarArgs;
ThData[i].WorkerId = i;
ThData[i].StageId = StageId;
ThData[i].NetId = NetId;
@ -1188,22 +1228,29 @@ int Cec_GiaReplayReadParams( char * pFileName, int * pnProcs, int * pnTimeOut, i
*pnTimeOut3 = Plan.nTimeOut3;
if ( pfUseUif )
*pfUseUif = Plan.fUseUif;
Cec_SprovePlanFree( &Plan );
return 1;
}
int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile )
int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile, char * pUfarArgs )
{
Cec_SprovePlan_t Plan;
Cec_SprovePlanDefault( &Plan, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif );
int RetValue;
Cec_SprovePlanDefault( &Plan, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pUfarArgs );
assert( nProcs >= 1 && nProcs <= 6 );
assert( nProcs + (fUseUif ? 1 : 0) <= PAR_THR_MAX );
return Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile );
RetValue = Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile );
Cec_SprovePlanFree( &Plan );
return RetValue;
}
int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, int fVerbose, int fVeryVerbose, int fSilent )
{
Cec_SprovePlan_t Plan;
int RetValue;
if ( !Cec_SproveReplayReadPlan( pFileName, &Plan ) )
return -1;
return Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, NULL );
RetValue = Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, NULL );
Cec_SprovePlanFree( &Plan );
return RetValue;
}
#endif // pthreads are used