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

Merge remote-tracking branch 'upstream/master' into yosys-experimental

This commit is contained in:
Miodrag Milanovic 2026-03-09 11:32:02 +01:00
parent 8e401543d3 7ae0f4966a
commit 55f552b454
15 changed files with 754 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/giaAiger.c
View File

@ -1297,7 +1297,7 @@ Vec_Str_t * Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p )
Gia_AigerWriteUnsigned( vBuffer, uLit - uLit1 );
Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 );
}
Vec_StrPrintStr( vBuffer, "c" );
Vec_StrPrintStr( vBuffer, "c\n" );
return vBuffer;
}

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

@ -1838,6 +1838,12 @@ static inline int Lf_ManDerivePart( Lf_Man_t * p, Gia_Man_t * pNew, Vec_Int_t *
}
pTruth = Lf_CutTruth( p, pCut );
iLit = Kit_TruthToGia( pNew, (unsigned *)pTruth, Vec_IntSize(vLeaves), vCover, vLeaves, 0 );
// do not create LUT in the simple case
if ( Abc_Lit2Var(iLit) == 0 )
return iLit;
Vec_IntForEachEntry( vLeaves, iTemp, k )
if ( Abc_Lit2Var(iLit) == Abc_Lit2Var(iTemp) )
return iLit;
// create mapping
Vec_IntSetEntry( vMapping, Abc_Lit2Var(iLit), Vec_IntSize(vMapping2) );
Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) );

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

@ -51412,7 +51412,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;
int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
int c, nProcs = 6, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWusvwh" ) ) != EOF )
{

75
src/base/cmd/cmd.c
View File

@ -67,6 +67,7 @@ static int CmdCommandCapo ( Abc_Frame_t * pAbc, int argc, char ** argv
static int CmdCommandStarter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int CmdCommandAutoTuner ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int CmdCommandSolver ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int CmdCommandSolver2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
extern int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -123,6 +124,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "starter", CmdCommandStarter, 0 );
Cmd_CommandAdd( pAbc, "Various", "autotuner", CmdCommandAutoTuner, 0 );
Cmd_CommandAdd( pAbc, "Various", "&solver", CmdCommandSolver, 0 );
Cmd_CommandAdd( pAbc, "Various", "&solver2", CmdCommandSolver2, 0 );
Cmd_CommandAdd( pAbc, "Various", "load_plugin", Cmd_CommandAbcLoadPlugIn, 0 );
}
@ -2971,6 +2973,79 @@ usage:
return 1;
}
/**Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
******************************************************************************/
int CmdCommandSolver2( Abc_Frame_t * pAbc, int argc, char **argv )
{
FILE * pFile;
char Command[2000];
int i;
if ( argc > 1 )
{
if ( strcmp( argv[1], "-h" ) == 0 )
goto usage;
if ( strcmp( argv[1], "-?" ) == 0 )
goto usage;
}
#if defined(__wasm)
fprintf( pAbc->Err, "Unsupported command.\n" );
return 1;
#else
// Check if solver binary exists in current directory or PATH
if ( (pFile = fopen( "./solver", "r" )) != NULL )
{
sprintf( Command, "%s", "./solver" );
fclose( pFile );
}
else
{
char CheckCommand[100];
sprintf( CheckCommand, "which solver > /dev/null 2>&1" );
if ( system( CheckCommand ) != 0 )
{
fprintf( pAbc->Err, "Cannot find \"solver\" binary in the current directory or in PATH.\n" );
goto usage;
}
sprintf( Command, "%s", "solver" );
}
// Append user-provided arguments as-is: solver <args>
for ( i = 1; i < argc; i++ )
{
strcat( Command, " " );
strcat( Command, argv[i] );
}
fprintf( pAbc->Out, "Executing command: %s\n", Command );
if ( system( Command ) == -1 )
{
fprintf( pAbc->Err, "The following command has failed:\n" );
fprintf( pAbc->Err, "\"%s\"\n", Command );
return 1;
}
#endif
return 0;
usage:
fprintf( pAbc->Err, "\tusage: &solver2 <args>\n");
fprintf( pAbc->Err, "\t run the external solver as \"solver <args>\"\n" );
fprintf( pAbc->Err, "\t-h : print the command usage\n" );
fprintf( pAbc->Err, "\t<args> : all arguments passed directly to solver\n" );
return 1;
}
/**Function********************************************************************
Synopsis [Print the version string.]

9
src/map/scl/sclLiberty.c
View File

@ -559,14 +559,17 @@ static char * Io_LibLoadFileGz( char * pFileName, long * pnFileSize )
const int READ_BLOCK_SIZE = 100000;
gzFile pFile;
char * pContents;
long amtRead, readBlock, nFileSize = READ_BLOCK_SIZE;
long amtRead, readBlock, nFileSize = READ_BLOCK_SIZE, nCapacity = READ_BLOCK_SIZE;
pFile = gzopen( pFileName, "rb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen
pContents = ABC_ALLOC( char, nFileSize );
pContents = ABC_ALLOC( char, nCapacity );
readBlock = 0;
while ((amtRead = gzread(pFile, pContents + readBlock * READ_BLOCK_SIZE, READ_BLOCK_SIZE)) == READ_BLOCK_SIZE) {
//Abc_Print( 1,"%d: read %d bytes\n", readBlock, amtRead);
nFileSize += READ_BLOCK_SIZE;
pContents = ABC_REALLOC(char, pContents, nFileSize);
if ( nFileSize > nCapacity ) {
nCapacity *= 2;
pContents = ABC_REALLOC(char, pContents, nCapacity);
}
++readBlock;
}
//Abc_Print( 1,"%d: read %d bytes\n", readBlock, amtRead);

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

@ -15,8 +15,11 @@
#include <iomanip>
#include <climits>
#include <regex>
#include <cstdlib>
#include <cstdio>
#include "base/wlc/wlc.h"
#include "aig/gia/giaAig.h"
#include "opt/ufar/UfarCmd.h"
#include "opt/ufar/UfarMgr.h"
#include "opt/untk/NtkNtk.h"
@ -120,6 +123,8 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
cout << "There is no current design.\n";
return 0;
}
// Make each %ufar invocation stateless: always start from factory defaults.
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");
@ -137,9 +142,14 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
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-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");
@ -147,6 +157,8 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
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");
@ -174,6 +186,10 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
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"])
@ -186,10 +202,16 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
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"]) {
@ -216,7 +238,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
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");
ufar_manager.params.fileAbs = opt_mgr.GetOptVal("--dump-abs");
}
if(opt_mgr["--dump"]) {
smatch sub_match;
@ -226,6 +248,9 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
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_manager.DumpParams();
LogT::prefix = "UIF_PROVE";
@ -257,6 +282,68 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
Wlc_AbcUpdateNtk(pAbc, pNew);
}
if ( opt_mgr["--crossstats"] )
{
Wlc_Ntk_t * pCur = Wlc_AbcGetNtk(pAbc);
if ( Wlc_NtkPoNum(pCur) != 2 )
{
cout << "CrossStats requires dual outputs before mitering.\n";
return 0;
}
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);
// Sequential traversal: from flop output (FO) continue to corresponding flop input (FI).
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;
//fflush(stdout);
//exit(1);
return 0;
}
if (opt_mgr["--under"]) {
pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), stoi(opt_mgr.GetOptVal("--under")));
Wlc_AbcUpdateNtk(pAbc, pNew);
@ -267,6 +354,12 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
Gia_Man_t * pGia = UFAR::BitBlast(Wlc_AbcGetNtk(pAbc));
Gia_ManPrintStats( pGia, NULL );
if ( !firstAigDumpFile.empty() && firstAigDumpFile != "none" )
{
Gia_AigerWriteSimple( pGia, (char *)firstAigDumpFile.c_str() );
Gia_ManStop( pGia );
return 0;
}
Gia_ManStop( pGia );
ufar_manager.Initialize(Wlc_AbcGetNtk(pAbc), set_op_types);
@ -283,14 +376,61 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
gettimeofday(&t2, NULL);
unsigned tTotal = elapsed_time_usec(t1, t2);
if(opt_mgr["--profile"]) {
unsigned nCexChecks = 0, nBitBlasts = 0;
unsigned long long tBitBlastUsec = 0, tCexCheckUsec = 0;
UFAR::Ufar_GetOrigCexStats(&nCexChecks, &nBitBlasts, &tBitBlastUsec, &tCexCheckUsec);
LOG(0) << "OrigCexStats: checks = " << nCexChecks
<< ", bitblasts = " << nBitBlasts
<< ", blast_time = " << fixed << setprecision(4) << ((double)tBitBlastUsec / 1000000.0)
<< " sec [" << (tTotal ? (100.0 * (double)tBitBlastUsec / (double)tTotal) : 0.0) << "%]"
<< ", cex_check_time = " << ((double)tCexCheckUsec / 1000000.0)
<< " sec [" << (tTotal ? (100.0 * (double)tCexCheckUsec / (double)tTotal) : 0.0) << "%]";
auto log_profile = [&](const string& str, abctime t) {
LOG(1) << str << " time = " << fixed << setprecision(4) << setw(8) << (double)t/1000000 << " sec [" << setw(7) << (double)t/tTotal*100 << "%]";
LOG(0) << str << " time = " << fixed << setprecision(4) << setw(8) << (double)t/1000000 << " sec [" << setw(7) << (double)t/tTotal*100 << "%]";
};
auto pct = [&](unsigned n, unsigned d) {
return d ? 100.0 * (double)n / (double)d : 0.0;
};
log_profile("BLSolver ", ufar_manager.profile.tBLSolver);
log_profile("UifRefine ", ufar_manager.profile.tUifRefine);
log_profile("WbRefine ", ufar_manager.profile.tWbRefine);
log_profile("UifSim ", ufar_manager.profile.tUifSim);
log_profile("GbRefine ", ufar_manager.profile.tGbRefine);
log_profile("CexCheck ", ufar_manager.profile.tCexCheckOrig);
{
unsigned long long tKnown = (unsigned long long)ufar_manager.profile.tBLSolver
+ (unsigned long long)ufar_manager.profile.tUifRefine
+ (unsigned long long)ufar_manager.profile.tWbRefine
+ (unsigned long long)ufar_manager.profile.tUifSim
+ (unsigned long long)ufar_manager.profile.tGbRefine
+ (unsigned long long)ufar_manager.profile.tCexCheckOrig;
unsigned long long tUnaccounted = (tTotal > tKnown) ? (tTotal - tKnown) : 0;
LOG(0) << "Unaccounted time = " << fixed << setprecision(4) << setw(8)
<< ((double)tUnaccounted / 1000000.0) << " sec [" << setw(7)
<< (tTotal ? (double)tUnaccounted * 100.0 / (double)tTotal : 0.0) << "%]";
}
LOG(0) << "UFAR calls: verify = " << ufar_manager.profile.nVerifyCalls
<< " (sat = " << ufar_manager.profile.nSatCalls
<< ", unsat = " << ufar_manager.profile.nUnsatCalls
<< ", undec = " << ufar_manager.profile.nUnknownCalls << ")";
LOG(0) << "UFAR cex : real = " << ufar_manager.profile.nRealCex
<< ", spurious = " << ufar_manager.profile.nSpuriousCex
<< " [" << fixed << setprecision(1)
<< pct(ufar_manager.profile.nSpuriousCex, ufar_manager.profile.nSatCalls)
<< "% spurious among SAT-abstraction]";
LOG(0) << "UFAR ref : iters_uif = " << ufar_manager.profile.nIterUif
<< ", iters_wb = " << ufar_manager.profile.nIterWb
<< ", pairs_added = " << ufar_manager.profile.nUifPairsAdded
<< ", mul_mul_pairs_added = " << ufar_manager.profile.nUifMulMulPairsAdded
<< ", wb_added = " << ufar_manager.profile.nWbAdded;
LOG(0) << "UFAR size : max_pairs = " << ufar_manager.profile.nMaxUifPairs
<< ", max_white_boxes = " << ufar_manager.profile.nMaxWhiteBoxes;
if ( ufar_manager.profile.nVerifyCalls ) {
LOG(0) << "UFAR avg : blsolve_call = "
<< fixed << setprecision(4)
<< (double)ufar_manager.profile.tBLSolver / 1000000.0 / (double)ufar_manager.profile.nVerifyCalls
<< " sec/call";
}
}
LOG(0) << "Time = " << setprecision(5) << ((double) (tTotal) / 1000000) << " sec";

329
src/opt/ufar/UfarMgr.cpp
View File

@ -13,6 +13,7 @@
#include <algorithm>
#include <array>
#include <regex>
#include <queue>
#ifdef _WIN32
#include <windows.h>
@ -35,6 +36,27 @@ static inline unsigned log_level() {
return LogT::loglevel;
}
static unsigned s_nOrigCexChecks = 0;
static unsigned s_nOrigBitBlasts = 0;
static unsigned long long s_tOrigBitBlastUsec = 0;
static unsigned long long s_tOrigCexCheckUsec = 0;
void Ufar_ResetOrigCexStats()
{
s_nOrigCexChecks = 0;
s_nOrigBitBlasts = 0;
s_tOrigBitBlastUsec = 0;
s_tOrigCexCheckUsec = 0;
}
void Ufar_GetOrigCexStats( unsigned * pChecks, unsigned * pBitBlasts, unsigned long long * pBitBlastUsec, unsigned long long * pCexCheckUsec )
{
if ( pChecks ) *pChecks = s_nOrigCexChecks;
if ( pBitBlasts ) *pBitBlasts = s_nOrigBitBlasts;
if ( pBitBlastUsec ) *pBitBlastUsec = s_tOrigBitBlastUsec;
if ( pCexCheckUsec ) *pCexCheckUsec = s_tOrigCexCheckUsec;
}
static void split(const string &s, char delim, vector<string>& elems) {
stringstream ss(s);
string item;
@ -132,7 +154,14 @@ static bool verify_cex_direct(Wlc_Ntk_t * pNtk, Abc_Cex_t * pCex) {
}
static bool verify_cex_on_original(Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex) {
timeval t1, t2, tCheck1, tCheck2;
gettimeofday(&tCheck1, NULL);
gettimeofday(&t1, NULL);
Gia_Man_t * pGiaOrig = BitBlast(pOrig);
gettimeofday(&t2, NULL);
s_nOrigCexChecks++;
s_nOrigBitBlasts++;
s_tOrigBitBlastUsec += elapsed_time_usec(t1, t2);
unsigned nbits_orig_pis = compute_bit_level_pi_num(pOrig);
int nbits_ppis = pCex->nPis - Gia_ManPiNum(pGiaOrig);
@ -161,6 +190,9 @@ static bool verify_cex_on_original(Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex) {
Gia_ManForEachPo( pGiaOrig, pObj, i ) {
if (pObj->Value==1) {
LOG(3) << "CEX is real.";
Gia_ManStop(pGiaOrig);
gettimeofday(&tCheck2, NULL);
s_tOrigCexCheckUsec += elapsed_time_usec(tCheck1, tCheck2);
return true;
}
}
@ -168,6 +200,8 @@ static bool verify_cex_on_original(Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex) {
Gia_ManStop(pGiaOrig);
LOG(3) << "CEX is spurious.";
gettimeofday(&tCheck2, NULL);
s_tOrigCexCheckUsec += elapsed_time_usec(tCheck1, tCheck2);
return false;
}
@ -949,6 +983,8 @@ UfarManager::Params::Params() :
fGrey(false),
nGrey(0),
fNorm(true),
fAllWb(false),
fCrossOnly(false),
fSuper_prove(false),
fSimple(false),
fSyn(false),
@ -956,21 +992,26 @@ UfarManager::Params::Params() :
iOneWb(-1),
iExp(-1),
nConstraintLimit(65536),
nInitAllPairsLimit(0),
nInitNearMults(0),
iVerbosity(0),
nSeqLookBack(0),
nTimeout(65536)
{}
UfarManager::UfarManager() : _pOrigNtk(NULL), _pAbsWithAuxPos(NULL) {}
UfarManager::UfarManager() : _pOrigNtk(NULL), _pAbsWithAuxPos(NULL), _fCrossReady(false) {}
UfarManager::~UfarManager() {
if (_pOrigNtk) Wlc_NtkFree(_pOrigNtk);
}
void UfarManager::Initialize(Wlc_Ntk_t * pNtk, const set<unsigned>& types) {
Ufar_ResetOrigCexStats();
LogT::loglevel = params.iVerbosity;
if (_pOrigNtk) Wlc_NtkFree(_pOrigNtk);
_vec_orig_names.clear();
_vec_op_ids.clear();
_vec_op_blackbox_marks.clear();
_vec_op_side.clear();
_vec_op_greyness.clear();
_set_uif_pairs.clear();
_set_uif_sim_pairs.clear();
@ -1001,12 +1042,211 @@ void UfarManager::Initialize(Wlc_Ntk_t * pNtk, const set<unsigned>& types) {
}
_vec_op_blackbox_marks.resize(_vec_op_ids.size(), true);
_vec_op_side.resize(_vec_op_ids.size(), 0);
_fCrossReady = false;
if ( params.fAllWb )
std::fill( _vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false );
if ( params.fCrossOnly )
{
int nObjs = Wlc_NtkObjNumMax(_pOrigNtk);
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(_pOrigNtk, iObj);
// Sequential traversal: from flop output (FO) continue to corresponding flop input (FI).
if ( pObjT->Type == WLC_OBJ_FO )
{
Wlc_Obj_t * pFi = Wlc_ObjFo2Fi(_pOrigNtk, pObjT);
stack.push_back( Wlc_ObjId(_pOrigNtk, pFi) );
}
int iFanin, k;
Wlc_ObjForEachFanin( pObjT, iFanin, k )
stack.push_back(iFanin);
}
};
if ( Wlc_NtkPoNum(_pOrigNtk) == 1 )
{
Wlc_Obj_t * pPo = Wlc_NtkPo(_pOrigNtk, 0);
int iMiter = Wlc_ObjFaninId0(pPo);
if ( iMiter >= 0 && iMiter < nObjs )
{
Wlc_Obj_t * pMit = Wlc_NtkObj(_pOrigNtk, iMiter);
if ( Wlc_ObjFaninNum(pMit) >= 2 )
{
int iL = Wlc_ObjFaninId0(pMit);
int iR = Wlc_ObjFaninId1(pMit);
mark_cone(iL, vConeL);
mark_cone(iR, vConeR);
_fCrossReady = true;
}
}
}
if ( _fCrossReady )
{
int nL = 0, nR = 0, nB = 0, nN = 0;
for ( size_t iOp = 0; iOp < _vec_op_ids.size(); ++iOp )
{
int iObj = _vec_op_ids[iOp];
bool fL = vConeL[iObj] != 0;
bool fR = vConeR[iObj] != 0;
char Side = fL ? (fR ? 3 : 1) : (fR ? 2 : 0);
_vec_op_side[iOp] = Side;
if ( Side == 1 ) nL++;
else if ( Side == 2 ) nR++;
else if ( Side == 3 ) nB++;
else nN++;
}
LOG(1) << "CrossOnly: classified operators L=" << nL << " R=" << nR << " BOTH=" << nB << " NONE=" << nN;
}
else
LOG(1) << "CrossOnly: unable to derive LHS/RHS cones from miter; disabling cross filter.";
}
auto seed_pairs_for_indices = [&]( const vector<int>& vOpIdxs )
{
auto sig = [&]( int iObj, int iFanin )
{
int iFin = (iFanin == 0) ? Wlc_ObjFaninId0(Wlc_NtkObj(_pOrigNtk, iObj)) : Wlc_ObjFaninId1(Wlc_NtkObj(_pOrigNtk, iObj));
Wlc_Obj_t * pFin = Wlc_NtkObj(_pOrigNtk, iFin);
return std::make_pair( Wlc_ObjRange(pFin), Wlc_ObjIsSigned(pFin) );
};
auto sigOut = [&]( int iObj )
{
Wlc_Obj_t * pObj = Wlc_NtkObj(_pOrigNtk, iObj);
return std::make_pair( Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) );
};
for ( size_t i = 0; i < vOpIdxs.size(); ++i )
for ( size_t j = i + 1; j < vOpIdxs.size(); ++j )
{
int idx1 = vOpIdxs[i];
int idx2 = vOpIdxs[j];
int iObj1 = _vec_op_ids[idx1];
int iObj2 = _vec_op_ids[idx2];
Wlc_Obj_t * pObj1 = Wlc_NtkObj(_pOrigNtk, iObj1);
Wlc_Obj_t * pObj2 = Wlc_NtkObj(_pOrigNtk, iObj2);
if ( pObj1->Type != pObj2->Type )
continue;
if ( sigOut(iObj1) != sigOut(iObj2) )
continue;
bool fDirect = (sig(iObj1, 0) == sig(iObj2, 0)) && (sig(iObj1, 1) == sig(iObj2, 1));
bool fSwap = (sig(iObj1, 0) == sig(iObj2, 1)) && (sig(iObj1, 1) == sig(iObj2, 0));
if ( fDirect ) {
UIF_PAIR Pair(OperatorID(idx1), OperatorID(idx2), 0);
if ( _allow_uif_pair(Pair) )
_set_uif_pairs.insert( Pair );
}
if ( fSwap ) {
UIF_PAIR Pair(OperatorID(idx1), OperatorID(idx2), 1);
if ( _allow_uif_pair(Pair) )
_set_uif_pairs.insert( Pair );
}
}
};
if ( params.nInitNearMults > 0 )
{
vector<pair<int, int> > vScoreIdx; // (seq distance from outputs, op-index in _vec_op_ids)
int nObjs = Wlc_NtkObjNumMax(_pOrigNtk);
vector<int> vDist(nObjs, -1);
queue<int> q;
Wlc_Obj_t * pPoT; int iPo;
Wlc_NtkForEachPo( _pOrigNtk, pPoT, iPo )
{
int iRoot = Wlc_ObjFaninId0(pPoT);
if ( iRoot > 0 && iRoot < nObjs && vDist[iRoot] == -1 )
{
vDist[iRoot] = 0;
q.push(iRoot);
}
}
while ( !q.empty() )
{
int iObj = q.front();
q.pop();
Wlc_Obj_t * pObjT = Wlc_NtkObj(_pOrigNtk, iObj);
int dNext = vDist[iObj] + 1;
if ( pObjT->Type == WLC_OBJ_FO )
{
Wlc_Obj_t * pFi = Wlc_ObjFo2Fi(_pOrigNtk, pObjT);
int iFi = Wlc_ObjId(_pOrigNtk, pFi);
if ( iFi > 0 && iFi < nObjs && (vDist[iFi] == -1 || dNext < vDist[iFi]) )
{
vDist[iFi] = dNext;
q.push(iFi);
}
}
int iFanin, k;
Wlc_ObjForEachFanin( pObjT, iFanin, k )
{
if ( iFanin <= 0 || iFanin >= nObjs )
continue;
if ( vDist[iFanin] == -1 || dNext < vDist[iFanin] )
{
vDist[iFanin] = dNext;
q.push(iFanin);
}
}
}
for ( size_t i = 0; i < _vec_op_ids.size(); ++i )
{
int iObj = _vec_op_ids[i];
if ( Wlc_NtkObj(_pOrigNtk, iObj)->Type != WLC_OBJ_ARI_MULTI )
continue;
if ( iObj <= 0 || iObj >= nObjs )
continue;
if ( vDist[iObj] < 0 )
continue;
vScoreIdx.push_back( { vDist[iObj], (int)i } );
}
sort( vScoreIdx.begin(), vScoreIdx.end(),
[]( const pair<int,int>& a, const pair<int,int>& b )
{ return a.first != b.first ? a.first < b.first : a.second < b.second; } );
vector<int> vSeedOps;
size_t nTake = Abc_MinInt( (int)vScoreIdx.size(), (int)params.nInitNearMults );
vSeedOps.reserve( nTake );
for ( size_t i = 0; i < nTake; ++i )
vSeedOps.push_back( vScoreIdx[i].second );
sort( vSeedOps.begin(), vSeedOps.end() );
size_t nBefore = _set_uif_pairs.size();
seed_pairs_for_indices( vSeedOps );
if ( _set_uif_pairs.size() > nBefore ) {
LOG(1) << "InitNear: pre-seeded " << (_set_uif_pairs.size() - nBefore)
<< " UIF pairs among " << vSeedOps.size() << " closest multipliers (limit = " << params.nInitNearMults << ")";
}
}
if ( params.nInitAllPairsLimit > 0 && _vec_op_ids.size() <= params.nInitAllPairsLimit )
{
vector<int> vAllOps;
vAllOps.reserve( _vec_op_ids.size() );
for ( size_t i = 0; i < _vec_op_ids.size(); ++i )
vAllOps.push_back( (int)i );
size_t nBefore = _set_uif_pairs.size();
seed_pairs_for_indices( vAllOps );
if ( _set_uif_pairs.size() > nBefore ) {
LOG(1) << "InitAllPairs: pre-seeded " << (_set_uif_pairs.size() - nBefore)
<< " UIF pairs (ops = " << _vec_op_ids.size() << ", limit = " << params.nInitAllPairsLimit << ")";
}
}
_p_sim_mgr.reset(new SimUifPairFinder(_pOrigNtk, &_vec_op_ids));
_p_cex_mgr.reset(new CexUifPairFinder(_pOrigNtk, &_vec_op_ids));
LogT::loglevel = params.iVerbosity;
struct timeval now;
gettimeofday(&now, NULL);
_timeout.tv_sec = now.tv_sec + params.nTimeout;
@ -1122,6 +1362,8 @@ void UfarManager::FindUifPairsUsingSim() {
set<UIF_PAIR> set_new_pairs;
for(auto& x:_set_uif_sim_pairs) {
if ( !_allow_uif_pair(x) )
continue;
auto res = _set_uif_pairs.insert(x);
if(res.second)
set_new_pairs.insert(x);
@ -1149,6 +1391,14 @@ void UfarManager::FindUifPairsUsingCex(Abc_Cex_t * pCex, Abc_Cex_t ** ppCex) {
} else {
_p_cex_mgr->FindUifPairsBasic(cex_po_values, params.nSeqLookBack, set_found_pairs);
}
if ( params.fCrossOnly && _fCrossReady )
{
for ( auto it = set_found_pairs.begin(); it != set_found_pairs.end(); )
if ( !_allow_uif_pair(*it) )
it = set_found_pairs.erase(it);
else
++it;
}
if(log_level() >= 3) print_pairs(set_found_pairs);
if(params.fPbaUif && !set_found_pairs.empty()) {
@ -1171,6 +1421,14 @@ void UfarManager::FindUifPairsUsingCex(Abc_Cex_t * pCex, Abc_Cex_t ** ppCex) {
}
}
if ( params.fCrossOnly && _fCrossReady )
{
for ( auto it = set_found_pairs.begin(); it != set_found_pairs.end(); )
if ( !_allow_uif_pair(*it) )
it = set_found_pairs.erase(it);
else
++it;
}
for(auto& x : set_found_pairs) _set_uif_pairs.insert(x);
gettimeofday(&t2, NULL);
@ -1403,7 +1661,7 @@ int UfarManager::VerifyCurrentAbstraction(Abc_Cex_t ** ppCex) {
}
}
*/
ret = verify_model(pCurrent, ppCex, &params.fileName, &params.parSetting, params.fSyn, &_timeout, params.pFuncStop, params.RunId);
ret = verify_model(pCurrent, ppCex, &params.fileName, &params.parSetting, params.fSyn, &_timeout, params.pFuncStop, params.RunId, &params.solverSetting, (int)params.nTimeout);
Wlc_NtkFree(pCurrent);
gettimeofday(&t2, NULL);
@ -1447,9 +1705,14 @@ int UfarManager::PerformUIFProve(const timeval& timer) {
LOG(1) << "Grey: [Total] = " << setprecision(4) << stat << " (" << _vec_op_greyness.size() << ")";
};
auto print_stat = [&]() {
unsigned nWhiteBoxes = count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false);
if (profile.nMaxUifPairs < _set_uif_pairs.size())
profile.nMaxUifPairs = _set_uif_pairs.size();
if (profile.nMaxWhiteBoxes < nWhiteBoxes)
profile.nMaxWhiteBoxes = nWhiteBoxes;
gettimeofday(&curTime, NULL);
elapsedTime = elapsed_time_usec(timer, curTime)/1000000.0;
snprintf(buffer, sizeof(buffer), "Iteration[%2u][%3u]: %4lu White boxes\t%4lu UIF constraints (time = %.4f)", n_iter_wb, n_iter_uif, count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false), _set_uif_pairs.size(), elapsedTime);
snprintf(buffer, sizeof(buffer), "Iteration[%2u][%3u]: %4u White boxes\t%4lu UIF constraints (time = %.4f)", n_iter_wb, n_iter_uif, nWhiteBoxes, _set_uif_pairs.size(), elapsedTime);
LOG(1) << buffer << _get_profile_uf_wb();
dump_grey_stat();
if(!params.fileStatesOut.empty()) _dump_states(params.fileStatesOut);
@ -1491,18 +1754,28 @@ int UfarManager::PerformUIFProve(const timeval& timer) {
Wlc_NtkFree(pCurrent);
ret = 0;
} else {
profile.nVerifyCalls++;
ret = VerifyCurrentAbstraction(&mem.pCex);
}
if (ret == 0) { // SAT
profile.nSatCalls++;
if ( Ufar_ShouldStop(params) )
return -1;
// GetOperatorsInCex(mem.pCex);
if (verify_cex_on_original(_pOrigNtk, mem.pCex)) {
timeval tCheck1, tCheck2;
gettimeofday(&tCheck1, NULL);
bool fRealCex = verify_cex_on_original(_pOrigNtk, mem.pCex);
gettimeofday(&tCheck2, NULL);
profile.tCexCheckOrig += elapsed_time_usec(tCheck1, tCheck2);
if (fRealCex) {
profile.nRealCex++;
PrintWordCEX(_pOrigNtk, mem.pCex, &_vec_orig_names);
return 0;
}
profile.nSpuriousCex++;
unsigned n_before = _set_uif_pairs.size();
set<UIF_PAIR> set_before = _set_uif_pairs;
FindUifPairsUsingCex(mem.pCex, &mem.pCex2);
if ( Ufar_ShouldStop(params) )
@ -1534,17 +1807,28 @@ int UfarManager::PerformUIFProve(const timeval& timer) {
}
}
if (_set_uif_pairs.size() > n_before)
profile.nUifPairsAdded += (_set_uif_pairs.size() - n_before);
if (_set_uif_pairs.size() > n_before) {
for (const auto& x : _set_uif_pairs) {
if (set_before.find(x) == set_before.end() && _is_mul_mul_pair(x))
profile.nUifMulMulPairsAdded++;
}
}
++n_iter_uif;
profile.nIterUif++;
print_stat();
if(_set_uif_pairs.size() > params.nConstraintLimit)
return -1;
} else if (ret == 1) { // UNSAT
profile.nUnsatCalls++;
//_shrink_final_abstraction();
//print_stat();
return 1;
} else {
profile.nUnknownCalls++;
return -1;
}
@ -1552,9 +1836,14 @@ int UfarManager::PerformUIFProve(const timeval& timer) {
if ( Ufar_ShouldStop(params) )
return -1;
unsigned nWhiteBoxesBefore = count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false);
DetermineWhiteBoxes(mem.pCex);
unsigned nWhiteBoxesAfter = count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false);
if (nWhiteBoxesAfter > nWhiteBoxesBefore)
profile.nWbAdded += (nWhiteBoxesAfter - nWhiteBoxesBefore);
++n_iter_wb;
profile.nIterWb++;
print_stat();
}
return -1;
@ -1573,6 +1862,31 @@ void UfarManager::_massage_state_b() {
}
bool UfarManager::_is_mul_mul_pair(const UIF_PAIR& x) const {
if (!_pOrigNtk)
return false;
if (x.first.idx >= _vec_op_ids.size() || x.second.idx >= _vec_op_ids.size())
return false;
int obj1 = _vec_op_ids[x.first.idx];
int obj2 = _vec_op_ids[x.second.idx];
Wlc_Obj_t * pObj1 = Wlc_NtkObj(_pOrigNtk, obj1);
Wlc_Obj_t * pObj2 = Wlc_NtkObj(_pOrigNtk, obj2);
return pObj1 && pObj2 && pObj1->Type == WLC_OBJ_ARI_MULTI && pObj2->Type == WLC_OBJ_ARI_MULTI;
}
bool UfarManager::_allow_uif_pair(const UIF_PAIR& x) const {
if ( !params.fCrossOnly || !_fCrossReady )
return true;
if ( x.first.idx < 0 || x.second.idx < 0 )
return false;
if ( x.first.idx >= (int)_vec_op_side.size() || x.second.idx >= (int)_vec_op_side.size() )
return false;
char s1 = _vec_op_side[x.first.idx];
char s2 = _vec_op_side[x.second.idx];
return (s1 == 1 && s2 == 2) || (s1 == 2 && s2 == 1);
}
string UfarManager::_get_profile_uf_wb() {
if (log_level() <= 4) return "";
unsigned num_full_white = 0;
@ -1625,6 +1939,9 @@ void UfarManager::DumpParams() const {
unsigned n_setw = 15;
cout << "Parameters : " << endl;
cout << " " << setw(n_setw) << left << "cexmin" << " : " << (params.fCexMin ? "yes" : "no") << endl;
cout << " " << setw(n_setw) << left << "allwb" << " : " << (params.fAllWb ? "yes" : "no") << endl;
cout << " " << setw(n_setw) << left << "crossonly" << " : " << (params.fCrossOnly ? "yes" : "no") << endl;
cout << " " << setw(n_setw) << left << "initnear" << " : " << params.nInitNearMults << endl;
cout << " " << setw(n_setw) << left << "iLogLevel" << " : " << params.iVerbosity << endl;
}

31
src/opt/ufar/UfarMgr.h
View File

@ -42,6 +42,9 @@ typedef struct Gia_Man_t_ Gia_Man_t;
namespace UFAR {
void Ufar_ResetOrigCexStats();
void Ufar_GetOrigCexStats(unsigned * pChecks, unsigned * pBitBlasts, unsigned long long * pBitBlastUsec, unsigned long long * pCexCheckUsec);
using VecVecInt = std::vector<std::vector<int> >;
using VecVecStr = std::vector<std::vector<std::string> >;
using VecChar = std::vector<char>;
@ -72,6 +75,8 @@ class UfarManager {
bool fGrey;
float nGrey;
bool fNorm;
bool fAllWb;
bool fCrossOnly;
bool fSuper_prove;
bool fSimple;
bool fSyn;
@ -79,23 +84,43 @@ class UfarManager {
int iOneWb;
int iExp;
unsigned nConstraintLimit;
unsigned nInitAllPairsLimit;
unsigned nInitNearMults;
unsigned iVerbosity;
unsigned nSeqLookBack;
unsigned nTimeout;
std::string simSetting;
std::string parSetting;
std::string solverSetting;
std::string fileName;
std::string fileAbs;
std::string fileStatesOut;
std::string fileStatesIn;
};
struct Profile {
Profile() : tBLSolver(0), tUifRefine(0), tWbRefine(0), tUifSim(0), tGbRefine(0) {}
Profile() : tBLSolver(0), tUifRefine(0), tWbRefine(0), tUifSim(0), tGbRefine(0), tCexCheckOrig(0),
nVerifyCalls(0), nSatCalls(0), nUnsatCalls(0), nUnknownCalls(0),
nRealCex(0), nSpuriousCex(0), nIterUif(0), nIterWb(0),
nUifPairsAdded(0), nUifMulMulPairsAdded(0), nWbAdded(0), nMaxUifPairs(0), nMaxWhiteBoxes(0) {}
unsigned tBLSolver;
unsigned tUifRefine;
unsigned tWbRefine;
unsigned tUifSim;
unsigned tGbRefine;
unsigned tCexCheckOrig;
unsigned nVerifyCalls;
unsigned nSatCalls;
unsigned nUnsatCalls;
unsigned nUnknownCalls;
unsigned nRealCex;
unsigned nSpuriousCex;
unsigned nIterUif;
unsigned nIterWb;
unsigned nUifPairsAdded;
unsigned nUifMulMulPairsAdded;
unsigned nWbAdded;
unsigned nMaxUifPairs;
unsigned nMaxWhiteBoxes;
};
UfarManager();
@ -132,6 +157,8 @@ class UfarManager {
void _perform_proof_based_grey_boxing(Abc_Cex_t * pCex);
void _perform_cex_based_white_boxing();
std::string _get_profile_uf_wb();
bool _is_mul_mul_pair(const UIF_PAIR& x) const;
bool _allow_uif_pair(const UIF_PAIR& x) const;
void _massage_state_b();
void _dump_states(const std::string& file);
void _read_states(const std::string& file);
@ -143,6 +170,7 @@ class UfarManager {
std::vector<int> _vec_op_ids;
std::vector<bool> _vec_op_blackbox_marks;
std::vector<char> _vec_op_side; // 0=unknown, 1=L-only, 2=R-only, 3=both
std::vector<std::vector<int> > _vec_vec_op_ffs;
std::vector<Greyness> _vec_op_greyness;
@ -156,6 +184,7 @@ class UfarManager {
std::unique_ptr<CexUifPairFinder> _p_cex_mgr;
std::ostringstream _oss;
bool _fCrossReady;
struct timespec _timeout;
};

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

@ -11,12 +11,18 @@
#include <unistd.h>
#endif
#include <fstream>
#include <cstdio>
#include <cstdlib>
#include <ctime>
#include <algorithm>
#include <cctype>
#include <base/wlc/wlc.h>
#include <sat/bmc/bmc.h>
#include <proof/pdr/pdr.h>
#include <proof/fraig/fraig.h>
#include <aig/gia/giaAig.h>
#include <base/io/ioAbc.h>
#include "opt/util/util.h"
#include "opt/ufar/UfarPth.h"
@ -1250,11 +1256,77 @@ static void readCexFromFile(int& ret, FILE * file, Abc_Cex_t ** ppCex, int nOrig
}
}
int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, struct timespec * timeout, int (*pFuncStop)(int), int RunId) {
static inline bool is_solver_cmd_defined(const string* pSolverSetting) {
return pSolverSetting && !pSolverSetting->empty() && *pSolverSetting != "none";
}
static inline int run_external_solver_on_aig( Abc_Ntk_t * pAbcNtk, const string& solverCmd, int nRuntimeLimitSec )
{
const char * pAigFile = "file.aig";
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;
if ( nRuntimeLimitSec > 0 )
command += " " + to_string(nRuntimeLimitSec);
command += " > log.txt 2>&1";
LOG(1) << "UFAR external solver: launching command instead of PDR: " << command;
int res = system( command.c_str() );
std::remove( pAigFile );
return res;
}
static inline int read_external_status_unsat_first_line()
{
ifstream ifs("status.txt", std::ifstream::in);
if ( !ifs )
return -1;
int firstLine = -1;
ifs >> firstLine;
if ( ifs && firstLine == 0 )
return 1;
return -1;
}
static inline int read_external_result_from_log_last_line()
{
ifstream ifs("log.txt", std::ifstream::in);
if ( !ifs )
return -1;
string line, last;
auto trim = []( 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();
};
while ( getline(ifs, line) )
{
trim(line);
if ( !line.empty() )
last = line;
}
if ( last.empty() )
return -1;
transform( last.begin(), last.end(), last.begin(),
[]( unsigned char c ){ return (char)toupper(c); } );
if ( last.find("UNSAT") != string::npos )
return 1;
if ( last.find("SAT") != string::npos )
return 0;
if ( last.find("UNKNOWN") != string::npos || last.find("UNDECIDED") != string::npos )
return -1;
return -1;
}
int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, struct timespec * timeout, int (*pFuncStop)(int), int RunId, const string* pSolverSetting, int nUfarTimeoutSec) {
if ( pFuncStop && pFuncStop(RunId) )
return -1;
if ( !pParSetting || pParSetting->empty() || Wlc_NtkFfNum(pNtk) == 0 )
return bit_level_solve( pNtk, ppCex, pFileName, pParSetting, fSyn, pFuncStop, RunId );
return bit_level_solve( pNtk, ppCex, pFileName, pParSetting, fSyn, pFuncStop, RunId, pSolverSetting, nUfarTimeoutSec );
if(*ppCex) {
Abc_CexFree(*ppCex);
@ -1275,7 +1347,7 @@ int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName,
}
int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, int (*pFuncStop)(int), int RunId) {
int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, int (*pFuncStop)(int), int RunId, const string* pSolverSetting, int nRuntimeLimitSec) {
if ( pFuncStop && pFuncStop(RunId) )
return -1;
if(*ppCex) {
@ -1319,6 +1391,27 @@ int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileNam
}
} else {
auto runPDR = [&](FILE * file){
if ( is_solver_cmd_defined(pSolverSetting) )
{
run_external_solver_on_aig( pAbcNtk, *pSolverSetting, nRuntimeLimitSec );
int extStatus = read_external_result_from_log_last_line();
if ( extStatus == -1 )
extStatus = read_external_status_unsat_first_line();
if ( extStatus == 1 )
LOG(1) << "UFAR external solver result (UNSAT) available. Skipping PDR.";
else
LOG(1) << "UFAR external solver result not usable (log/status not UNSAT). Calling PDR.";
if ( extStatus == 1 )
{
writeCexToFile(1, file, NULL);
return 1;
}
if ( pFuncStop && pFuncStop(RunId) )
{
writeCexToFile(-1, file, NULL);
return -1;
}
}
Pdr_Par_t PdrPars, *pPdrPars = &PdrPars;
Pdr_ManSetDefaultParams(pPdrPars);
pPdrPars->nConfLimit = 0;

4
src/opt/untk/NtkNtk.h
View File

@ -136,8 +136,8 @@ void PrintWordCEX(Wlc_Ntk_t * pNtk, Abc_Cex_t * pCex, const std::vector<s
unsigned compute_bit_level_pi_num(Wlc_Ntk_t * pNtk);
int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const std::string* pFileName = NULL, const std::string* pParSetting = NULL, bool fSyn = false, struct timespec * timeout = NULL, int (*pFuncStop)(int) = NULL, int RunId = -1);
int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const std::string* pFileName = NULL, const std::string* pParSetting = NULL, bool fSyn = false, int (*pFuncStop)(int) = NULL, int RunId = -1);
int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const std::string* pFileName = NULL, const std::string* pParSetting = NULL, bool fSyn = false, struct timespec * timeout = NULL, int (*pFuncStop)(int) = NULL, int RunId = -1, const std::string* pSolverSetting = NULL, int nUfarTimeoutSec = -1);
int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const std::string* pFileName = NULL, const std::string* pParSetting = NULL, bool fSyn = false, int (*pFuncStop)(int) = NULL, int RunId = -1, const std::string* pSolverSetting = NULL, int nRuntimeLimitSec = -1);
Gia_Man_t * BitBlast(Wlc_Ntk_t * pNtk);

27
src/opt/util/util.cpp
View File

@ -48,7 +48,32 @@ bool OptMgr::Parse(int argc, char * argv[]) {
if(!opt.isBool()) {
if (i + 1 == argc)
return false;
opt._val = argv[++i];
string val = argv[++i];
if ( !val.empty() && (val[0] == '"' || val[0] == '\'') )
{
char q = val[0];
bool fClosed = val.size() >= 2 && val.back() == q;
if ( fClosed )
val = val.substr(1, val.size() - 2);
else
{
val.erase(0, 1);
while ( i + 1 < argc )
{
string next = argv[++i];
if ( !next.empty() && next.back() == q )
{
val += " " + next.substr(0, next.size() - 1);
fClosed = true;
break;
}
val += " " + next;
}
if ( !fClosed )
return false;
}
}
opt._val = val;
}
}

3
src/proof/abs/abs.h
View File

@ -74,6 +74,8 @@ struct Abs_Par_t_
char * pFileVabs; // dumps the abstracted model into this file
int fVerbose; // verbose flag
int fVeryVerbose; // print additional information
int RunId; // id in this run
int (*pFuncStop)(int); // callback to terminate
int iFrame; // the number of frames covered
int iFrameProved; // the number of frames proved
int nFramesNoChange; // the number of last frames without changes
@ -174,4 +176,3 @@ ABC_NAMESPACE_HEADER_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

10
src/proof/abs/absGla.c
View File

@ -1576,6 +1576,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
{
int nAbsOld;
if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) )
goto finish;
// remember the timeframe
p->pPars->iFrame = -1;
// create new SAT solver
@ -1585,6 +1587,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
// unroll the circuit
for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
{
if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) )
goto finish;
// remember current limits
int nConflsBeg = sat_solver2_nconflicts(p->pSat);
int nAbs = Vec_IntSize(p->vAbs);
@ -1618,6 +1622,11 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
nVarsOld = p->nSatVars;
for ( c = 0; ; c++ )
{
if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) )
{
Status = l_Undef;
goto finish;
}
// consider the special case when the target literal is implied false
// by implications which happened as a result of previous refinements
// note that incremental UNSAT core cannot be computed because there is no learned clauses
@ -1898,4 +1907,3 @@ finish:
ABC_NAMESPACE_IMPL_END

3
src/proof/abs/absUtil.c
View File

@ -59,6 +59,8 @@ void Abs_ParSetDefaults( Abs_Par_t * p )
p->fUseRollback = 0; // use rollback to the starting number of frames
p->fPropFanout = 1; // propagate fanouts during refinement
p->fVerbose = 0; // verbose flag
p->RunId = -1; // id in this run
p->pFuncStop = NULL; // callback to terminate
p->iFrame = -1; // the number of frames covered
p->iFrameProved = -1; // the number of frames proved
p->nFramesNoChangeLim = 2; // the number of frames without change to dump abstraction
@ -254,4 +256,3 @@ int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla )
ABC_NAMESPACE_IMPL_END

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

@ -26,6 +26,7 @@
#include "proof/pdr/pdr.h"
#include "proof/cec/cec.h"
#include "proof/ssw/ssw.h"
#include "proof/abs/abs.h"
#ifdef ABC_USE_PTHREADS
@ -66,6 +67,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
#define PAR_ENGINE_UFAR 6
#define PAR_ENGINE_SCORR1 7
#define PAR_ENGINE_SCORR2 8
#define PAR_ENGINE_GLA 9
struct Par_Share_t_
{
volatile int fSolved;
@ -90,6 +92,7 @@ typedef struct Cec_ScorrStop_t_
abctime TimeToStop;
} Cec_ScorrStop_t;
static volatile Par_Share_t * g_pUfarShare = NULL;
static volatile Par_Share_t * g_pGlaShare = NULL;
static inline const char * Cec_SolveEngineName( int iEngine )
{
if ( iEngine == 0 ) return "rar";
@ -101,6 +104,7 @@ static inline const char * Cec_SolveEngineName( int iEngine )
if ( iEngine == PAR_ENGINE_UFAR ) return "ufar";
if ( iEngine == PAR_ENGINE_SCORR1 ) return "scorr-new";
if ( iEngine == PAR_ENGINE_SCORR2 ) return "scorr-old";
if ( iEngine == PAR_ENGINE_GLA ) return "gla-q";
return "unknown";
}
static inline void Cec_CopyGiaName( Gia_Man_t * pSrc, Gia_Man_t * pDst )
@ -128,6 +132,11 @@ static int Cec_SProveStopUfar( int RunId )
(void)RunId;
return g_pUfarShare && g_pUfarShare->fSolved != 0;
}
static int Cec_SProveStopGla( int RunId )
{
(void)RunId;
return g_pGlaShare && g_pGlaShare->fSolved != 0;
}
static int Cec_ScorrStop( void * pUser )
{
Cec_ScorrStop_t * p = (Cec_ScorrStop_t *)pUser;
@ -177,7 +186,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
{
abctime clk = Abc_Clock();
int RetValue = -1;
if ( iEngine != PAR_ENGINE_UFAR && Gia_ManRegNum(p) == 0 )
if ( iEngine != PAR_ENGINE_UFAR && iEngine != PAR_ENGINE_GLA && Gia_ManRegNum(p) == 0 )
{
if ( fVerbose )
printf( "Engine %d skipped because the current miter is combinational.\n", iEngine );
@ -294,6 +303,22 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
g_pUfarShare = NULL;
}
}
else if ( iEngine == PAR_ENGINE_GLA )
{
if ( Gia_ManPoNum(p) != 1 )
return -1;
Abs_Par_t Pars, * pPars = &Pars;
Abs_ParSetDefaults( pPars );
pPars->nTimeOut = nTimeOut;
pPars->fCallProver = 1; // emulate "&gla -q"
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
pPars->RunId = 0;
pPars->pFuncStop = Cec_SProveStopGla;
g_pGlaShare = pThData ? pThData->pShare : NULL;
RetValue = Gia_ManPerformGla( p, pPars );
g_pGlaShare = NULL;
}
else assert( 0 );
//while ( Abc_Clock() < clkStop );
if ( pThData && pThData->pShare && RetValue != -1 )
@ -379,7 +404,12 @@ void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int
{
ThData[i].p = Gia_ManDup(p);
Cec_CopyGiaName( p, ThData[i].p );
ThData[i].iEngine = (fUseUif && i == nWorkers - 1) ? PAR_ENGINE_UFAR : i;
if ( fUseUif && i == nWorkers - 1 )
ThData[i].iEngine = PAR_ENGINE_UFAR;
else if ( !fUseUif && nWorkers == 6 && i == 5 )
ThData[i].iEngine = PAR_ENGINE_GLA;
else
ThData[i].iEngine = i;
ThData[i].nTimeOut = nTimeOut;
ThData[i].fWorking = 0;
ThData[i].Result = -1;
@ -427,7 +457,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
printf( "Processes = %d TimeOut = %d sec Verbose = %d.\n", nProcs, nTimeOut, fVerbose );
fflush( stdout );
assert( nProcs == 3 || nProcs == 5 );
assert( nProcs == 3 || nProcs == 5 || nProcs == 6 );
assert( nWorkers <= PAR_THR_MAX );
Cec_GiaInitThreads( ThData, nWorkers, p, nTimeOut, nTimeOut3, pWlc, fUseUif, fVerbose, WorkerThread, &Share );