From 5cdded372aed1ef6d70906d3b81fa6698e2cf555 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 24 Dec 2025 19:06:29 -0800 Subject: [PATCH] Command %ufar. --- Makefile | 2 +- src/base/main/mainInit.c | 2 + src/opt/ufar/UfarCmd.cpp | 336 ++++++++ src/opt/ufar/UfarCmd.h | 23 + src/opt/ufar/UfarMgr.cpp | 1663 ++++++++++++++++++++++++++++++++++++++ src/opt/ufar/UfarMgr.h | 144 ++++ src/opt/ufar/UfarPth.cpp | 289 +++++++ src/opt/ufar/UfarPth.h | 17 + src/opt/ufar/module.make | 3 + src/opt/untk/Netlist.cpp | 63 ++ src/opt/untk/Netlist.h | 33 + src/opt/untk/NtkCmd.cpp | 12 + src/opt/untk/NtkCmd.h | 15 + src/opt/untk/NtkNtk.cpp | 1487 ++++++++++++++++++++++++++++++++++ src/opt/untk/NtkNtk.h | 150 ++++ src/opt/untk/module.make | 6 + src/opt/util/module.make | 2 + src/opt/util/util.cpp | 119 +++ src/opt/util/util.h | 85 ++ 19 files changed, 4450 insertions(+), 1 deletion(-) create mode 100755 src/opt/ufar/UfarCmd.cpp create mode 100755 src/opt/ufar/UfarCmd.h create mode 100755 src/opt/ufar/UfarMgr.cpp create mode 100755 src/opt/ufar/UfarMgr.h create mode 100755 src/opt/ufar/UfarPth.cpp create mode 100755 src/opt/ufar/UfarPth.h create mode 100755 src/opt/ufar/module.make create mode 100755 src/opt/untk/Netlist.cpp create mode 100755 src/opt/untk/Netlist.h create mode 100755 src/opt/untk/NtkCmd.cpp create mode 100755 src/opt/untk/NtkCmd.h create mode 100755 src/opt/untk/NtkNtk.cpp create mode 100755 src/opt/untk/NtkNtk.h create mode 100755 src/opt/untk/module.make create mode 100755 src/opt/util/module.make create mode 100755 src/opt/util/util.cpp create mode 100755 src/opt/util/util.h diff --git a/Makefile b/Makefile index 3e4d02719..6d4901b88 100644 --- a/Makefile +++ b/Makefile @@ -36,7 +36,7 @@ MODULES := \ src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \ src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \ src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt src/opt/rar \ - src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd src/opt/eslim \ + src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd src/opt/eslim src/opt/ufar src/opt/untk src/opt/util \ src/sat/bsat src/sat/xsat src/sat/satoko src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc src/sat/glucose src/sat/glucose2 src/sat/kissat src/sat/cadical \ src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \ src/bool/rsb src/bool/rpo \ diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c index d3ce672f5..03c6f94c0 100644 --- a/src/base/main/mainInit.c +++ b/src/base/main/mainInit.c @@ -69,6 +69,7 @@ extern void Glucose_Init( Abc_Frame_t *pAbc ); extern void Glucose_End( Abc_Frame_t * pAbc ); extern void Glucose2_Init( Abc_Frame_t *pAbc ); extern void Glucose2_End( Abc_Frame_t * pAbc ); +extern void Ufar_Init(Abc_Frame_t *pAbc); static Abc_FrameInitializer_t* s_InitializerStart = NULL; static Abc_FrameInitializer_t* s_InitializerEnd = NULL; @@ -123,6 +124,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc ) Cba_Init( pAbc ); Pla_Init( pAbc ); Test_Init( pAbc ); + Ufar_Init( pAbc ); Glucose_Init( pAbc ); Glucose2_Init( pAbc ); for( p = s_InitializerStart ; p ; p = p->next ) diff --git a/src/opt/ufar/UfarCmd.cpp b/src/opt/ufar/UfarCmd.cpp new file mode 100755 index 000000000..33b0cc3f7 --- /dev/null +++ b/src/opt/ufar/UfarCmd.cpp @@ -0,0 +1,336 @@ +/* + * UifCmd.cpp + * + * Created on: Aug 25, 2015 + * Author: Yen-Sheng Ho + */ + +#include "base/wlc/wlc.h" +#include "opt/ufar/UfarCmd.h" +#include "opt/ufar/UfarMgr.h" +#include "opt/untk/NtkNtk.h" +#include "opt/util/util.h" + +#include +#include +#include +#include + +using namespace std; + +static UFAR::UfarManager ufar_manager; + +static int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAnalyzeCex( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCreateAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCreateMiter( Abc_Frame_t * pAbc, int argc, char ** argv ); +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; } + + +void Ufar_Init(Abc_Frame_t *pAbc) +{ + //Cmd_CommandAdd( pAbc, "Word level Prove", "%%test", Abc_CommandTest, 0 ); + //Cmd_CommandAdd( pAbc, "Word level Prove", "%%cex", Abc_CommandAnalyzeCex, 0 ); + //Cmd_CommandAdd( pAbc, "Word level Prove", "%%abs", Abc_CommandCreateAbstraction, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%ufar", Abc_CommandProveUsingUif, 0 ); + //Cmd_CommandAdd( pAbc, "Word level Prove", "%%miter", Abc_CommandCreateMiter, 0 ); +} + +static int Abc_CommandCreateMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0); + Wlc_AbcUpdateNtk(pAbc, pNew); + return 0; +} + +static int Abc_CommandCreateAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNew = ufar_manager.BuildCurrentAbstraction(); + Wlc_AbcUpdateNtk(pAbc, pNew); + return 0; +} + +static int Abc_CommandAnalyzeCex( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + if ( pAbc->pCex == NULL ) + { + cout << "There is no CEX.\n"; + return 0; + } + + // ufar_manager.GetOperatorsInCex(pAbc->pCex); + ufar_manager.FindUifPairsUsingCex(pAbc->pCex); + + return 0; +} + +static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + if (Wlc_AbcGetNtk(pAbc) == NULL) { + cout << "There is no current design.\n"; + return 0; + } + + 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("--dump", "none", "str", "specify file name"); + opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name"); + opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers"); + 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("--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"); + 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["--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["--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["--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"); + } + 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"); + } + + // ufar_manager.DumpParams(); + LogT::prefix = "UIF_PROVE"; + + set 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; + } + + Wlc_Ntk_t * pNew = NULL; + timeval t1, t2; + gettimeofday(&t1, NULL); + + if (!opt_mgr["--miter"]) { + if (Wlc_NtkPoNum(Wlc_AbcGetNtk(pAbc)) != 2) { + cout << "The current design doesn't have dual outputs.\n"; + return 0; + } + pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0); + Wlc_AbcUpdateNtk(pAbc, pNew); + } + + if (ufar_manager.params.fNorm) { + pNew = UFAR::NormalizeDataTypes(Wlc_AbcGetNtk(pAbc), set_op_types, true); + Wlc_AbcUpdateNtk(pAbc, pNew); + } + + if (opt_mgr["--under"]) { + pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), stoi(opt_mgr.GetOptVal("--under"))); + Wlc_AbcUpdateNtk(pAbc, pNew); + pNew = UFAR::MakeUnderApprox2(Wlc_AbcGetNtk(pAbc), set_op_types, stoi(opt_mgr.GetOptVal("--under"))); + Wlc_AbcUpdateNtk(pAbc, pNew); + Wlc_WriteVer(Wlc_AbcGetNtk(pAbc), "UND.v", 0, 0); + } + + Gia_Man_t * pGia = UFAR::BitBlast(Wlc_AbcGetNtk(pAbc)); + Gia_ManPrintStats( pGia, NULL ); + Gia_ManStop( pGia ); + + ufar_manager.Initialize(Wlc_AbcGetNtk(pAbc), set_op_types); + + int ret = ufar_manager.PerformUIFProve(t1); + if (ret == 1) { + LOG(0) << "Proved by UIF (UNSAT)."; + } else if (ret == 0) { + LOG(0) << "Falsified by UIF (SAT)."; + } else { + LOG(0) << "Undecided by UIF."; + } + + gettimeofday(&t2, NULL); + unsigned tTotal = elapsed_time_usec(t1, t2); + if(opt_mgr["--profile"]) { + 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_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(0) << "Time = " << setprecision(5) << ((double) (tTotal) / 1000000) << " sec"; + + return 0; +} + +static int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + LogT::prefix = "TEST::"; + OptMgr opt_mgr(argv[0]); + opt_mgr.AddOpt("--ntk", "none", "str", "specify the file name (*.aig) for the input network"); + opt_mgr.AddOpt("--adder", "no", "", "toggle including adders"); + if(!opt_mgr.Parse(argc, argv)) { + opt_mgr.PrintUsage(); + return 0; + } + set set_op_types; + set_op_types.insert(WLC_OBJ_ARI_MULTI); + if(opt_mgr["--adder"]) { + set_op_types.insert(WLC_OBJ_ARI_ADD); + } + Wlc_Ntk_t * pNew = UFAR::AddConstFlops(Wlc_AbcGetNtk(pAbc), set_op_types); + Wlc_AbcUpdateNtk(pAbc, pNew); + return 0; + +#if 0 + opt_mgr.AddOpt("--ntk", "none", "str", "specify the file name (*.aig) for the input network"); + opt_mgr.AddOpt("--inv", "none", "str", "specify the file name (*.pla) for the invariant"); + if(!opt_mgr.Parse(argc, argv)) { + opt_mgr.PrintUsage(); + return 0; + } + + string nameNtk = opt_mgr.GetOptVal("--ntk"); + string nameInv = opt_mgr.GetOptVal("--inv"); + UFAR::TestInvariant(nameNtk, nameInv); +#endif +#if 0 + set set_op_types; + set_op_types.insert(WLC_OBJ_ARI_MULTI); + + OptMgr opt_mgr(argv[0]); + opt_mgr.AddOpt("--cube", "no", "", "toggle using cubes for interpolants"); + if(!opt_mgr.Parse(argc, argv)) { + opt_mgr.PrintUsage(); + return 0; + } + + UFAR::TestITP(Wlc_AbcGetNtk(pAbc), set_op_types, opt_mgr["--cube"]); +#endif +#if 0 + if ( Wlc_AbcGetNtk(pAbc) == NULL ) { + cout << "There is no current design.\n"; + return 0; + } + + if (Wlc_NtkPoNum(Wlc_AbcGetNtk(pAbc)) != 2) { + cout << "The current design doesn't have dual outputs.\n"; + return 0; + } + + set set_op_types; + set_op_types.insert(WLC_OBJ_ARI_MULTI); + if (!UFAR::HasOperator(Wlc_AbcGetNtk(pAbc), set_op_types)) { + cout << "There is no operator for UIF.\n"; + return 0; + } + + Wlc_Ntk_t * pNew = NULL; + + pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0); + Wlc_AbcUpdateNtk(pAbc, pNew); + + pNew = UFAR::NormalizeDataTypes(Wlc_AbcGetNtk(pAbc), set_op_types, true); + Wlc_AbcUpdateNtk(pAbc, pNew); + + ufar_manager.Initialize(Wlc_AbcGetNtk(pAbc), set_op_types); + ufar_manager.DumpMgrInfo(); + + pNew = ufar_manager.BuildCurrentAbstraction(); + Wlc_AbcUpdateNtk(pAbc, pNew); + + + return 0; +#endif +} + + diff --git a/src/opt/ufar/UfarCmd.h b/src/opt/ufar/UfarCmd.h new file mode 100755 index 000000000..40bdd5cf6 --- /dev/null +++ b/src/opt/ufar/UfarCmd.h @@ -0,0 +1,23 @@ +/* + * UifCmd.h + * + * Created on: Aug 25, 2015 + * Author: Yen-Sheng Ho + */ + +#ifndef SRC_EXT2_UIF_UIFCMD_H_ +#define SRC_EXT2_UIF_UIFCMD_H_ + +#include "base/main/mainInt.h" + +#ifdef __cplusplus +extern "C" { +#endif + +void Ufar_Init(Abc_Frame_t *pAbc); + +#ifdef __cplusplus +} +#endif + +#endif /* SRC_EXT2_UIF_UIFCMD_H_ */ diff --git a/src/opt/ufar/UfarMgr.cpp b/src/opt/ufar/UfarMgr.cpp new file mode 100755 index 000000000..071cfcf9e --- /dev/null +++ b/src/opt/ufar/UfarMgr.cpp @@ -0,0 +1,1663 @@ +/* + * UifMgr.cpp + * + * Created on: Aug 25, 2015 + * Author: Yen-Sheng Ho + */ + +#include +#include + +#include "UfarMgr.h" +#include "opt/untk/NtkNtk.h" +#include "opt/util/util.h" + +#include +#include +#include + +extern "C" { + Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); + void Wlc_NtkSimulatePrint( Wlc_Ntk_t * p, Vec_Int_t * vNodes, Vec_Ptr_t * vRes, int nWords, int nFrames ); +} + +#include + +#include +#include +#include +#include +#include +#include + +using namespace std; + +namespace UFAR { + +static inline unsigned log_level() { + return LogT::loglevel; +} + +static void split(const string &s, char delim, vector& elems) { + stringstream ss(s); + string item; + elems.clear(); + while (getline(ss, item, delim)) { + elems.push_back(std::move(item)); + } +} + +static void set_state_b(vector& vec_b_state, const string& str_state) { + if (vec_b_state.size() != str_state.size()) { + cerr << "Invalid initial states for B.\n" ; + return; + } + + for(size_t i = 0; i < str_state.size(); ++i) { + char state = str_state[i]; + if (state == '0') { + vec_b_state[i] = false; + } else if (state == '1') { + vec_b_state[i] = true; + } else if (state != '1') { + assert(false); + } + } +} + +static void set_state_p(set& set_p_state, const string& str_pair) { + vector tokens; + split(str_pair, ',', tokens); + assert(tokens.size() == 5); + set_p_state.insert(UIF_PAIR(OperatorID(stoi(tokens[0]), stoi(tokens[1])), OperatorID(stoi(tokens[2]), stoi(tokens[3])), tokens[4]=="1")); +} + +static void readCexFromVec(Gia_Man_t * pGia, const vector& vec_cex, Abc_Cex_t ** ppCex) { + int nBits = vec_cex.size(); + int nRegs = Gia_ManRegNum(pGia); + int nPis = Gia_ManPiNum(pGia); + + int iFrame = (nBits - nRegs) / nPis - 1; + assert(nBits == (nRegs + (iFrame + 1)*nPis)); + + *ppCex = Abc_CexAlloc(nRegs, nPis, iFrame + 1); + (*ppCex)->iFrame = iFrame; + (*ppCex)->iPo = 0; + for(size_t i = 0; i < vec_cex.size(); ++i) { + if (vec_cex[i] == 1 || vec_cex[i] == 0) { + if (vec_cex[i] == 1) + Abc_InfoSetBit((*ppCex)->pData, i); + } + } +} + +static Vec_Int_t * collect_boxes(const vector& vec_ids, const vector& vec_marks, bool fCollectBlack) { + Vec_Int_t * vec_ops = Vec_IntAlloc(10); + for(unsigned i = 0; i < vec_ids.size(); i++) { + int op_id = vec_ids[i]; + bool is_black = vec_marks[i]; + if((is_black && fCollectBlack) || (!is_black && !fCollectBlack)) + Vec_IntPush(vec_ops, op_id); + } + return vec_ops; +} + +static bool verify_cex_direct(Wlc_Ntk_t * pNtk, Abc_Cex_t * pCex) { + Gia_Man_t * pGia = BitBlast(pNtk); + int i; + + Gia_ManConst0(pGia)->Value = 0; + Gia_Obj_t * pObj, * pObjRi; + Gia_ManForEachRi( pGia, pObj, i ) + pObj->Value = 0; + for ( int f = 0; f <= pCex->iFrame; f++ ) { + for( i = 0; i < Gia_ManPiNum(pGia); i++ ) { + Gia_ManPi(pGia, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i); + } + Gia_ManForEachRiRo( pGia, pObjRi, pObj, i ) + pObj->Value = pObjRi->Value; + Gia_ManForEachAnd( pGia, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj) & Gia_ObjFanin1Copy(pObj); + Gia_ManForEachCo( pGia, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + Gia_ManForEachPo( pGia, pObj, i ) { + if (pObj->Value==1) { + LOG(3) << "CEX is valid."; + Gia_ManStop(pGia); + return true; + } + } + } + + LOG(3) << "CEX is invalid."; + Gia_ManStop(pGia); + return false; +} + +static bool verify_cex_on_original(Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex) { + Gia_Man_t * pGiaOrig = BitBlast(pOrig); + + unsigned nbits_orig_pis = compute_bit_level_pi_num(pOrig); + int nbits_ppis = pCex->nPis - Gia_ManPiNum(pGiaOrig); + LOG(3) << "VerifyCEX: #ppis = " << nbits_ppis; + + int i; + + Gia_ManConst0(pGiaOrig)->Value = 0; + Gia_Obj_t * pObj, * pObjRi; + Gia_ManForEachRi( pGiaOrig, pObj, i ) + pObj->Value = 0; + for ( int f = 0; f <= pCex->iFrame; f++ ) { + for( i = 0; i < Gia_ManPiNum(pGiaOrig); i++ ) { + if ( i < nbits_orig_pis ) { + Gia_ManPi(pGiaOrig, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i); + } else { // undc PIs + Gia_ManPi(pGiaOrig, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i + nbits_ppis); + } + } + Gia_ManForEachRiRo( pGiaOrig, pObjRi, pObj, i ) + pObj->Value = pObjRi->Value; + Gia_ManForEachAnd( pGiaOrig, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj) & Gia_ObjFanin1Copy(pObj); + Gia_ManForEachCo( pGiaOrig, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + Gia_ManForEachPo( pGiaOrig, pObj, i ) { + if (pObj->Value==1) { + LOG(3) << "CEX is real."; + return true; + } + } + } + + Gia_ManStop(pGiaOrig); + LOG(3) << "CEX is spurious."; + return false; +} + +static bool bitstr_not_equal(const string& str1, const string& str2) { + if (str1.size()!=str2.size()) return true; + + for(unsigned i = 0; i < str1.size(); i++) { + if (str1[i]=='1' && str2[i]=='0') + return true; + if (str1[i]=='0' && str2[i]=='1') + return true; + + if (str1[i]=='u' && str2[i]=='s') + return true; + if (str1[i]=='s' && str2[i]=='u') + return true; + } + + return false; +} + +static bool bitstr_all_x(const string& str) { + for(auto& x : str) { + if(x!='x') return false; + } + return true; +} + +static void print_blackboxes(const vector& vec_bb) { + ostringstream oss; + for(const auto& x : vec_bb) { + oss << (x ? "1" : "0"); + } + LOG(3) << oss.str(); +} + +static void print_pairs(const set& set_pairs) { + for(auto& x : set_pairs) { + LOG(3) << "(" << x.first << ", " << x.second << ")" << (x.fMark ? " [r]" : ""); + } +} + +/* +static int super_prove(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, bool fSimp, const string* pFileName = NULL) { + if(*ppCex) { + Abc_CexFree(*ppCex); + *ppCex = NULL; + } + + Gia_Man_t * pGia = BitBlast(pNtk); + + if (pFileName && !pFileName->empty()) + Gia_AigerWriteSimple(pGia, &((*pFileName + ".aig")[0u])); + + string tmpName = tmpnam(nullptr); + string tmpFileName = tmpName + ".aig"; + Gia_AigerWrite( pGia, &tmpFileName[0u], 0, 0 ); + + //string cmd = "super_prove -r /dev/stderr " + tmpFileName; + string cmd; + if (fSimp) + cmd = "simple " + tmpFileName; + else + cmd = "super_prove " + tmpFileName; + + vector vec_cex; + int result = call_python("run_sp", "verify", cmd.c_str(), vec_cex); + if(result == 1) + readCexFromVec(pGia, vec_cex, ppCex); + remove(tmpFileName.c_str()); + Gia_ManStop(pGia); + + if (result == 0) { + return 1; + } else if (result == 1) { + return 0; + } else { + return -1; + } +} +*/ + +static void get_operator_pair(Wlc_Ntk_t * p, const UIF_PAIR& uif_pair, array& wires1, array& wires2, const vector& vec_ids, const VecVecInt& vv_op_ffs) { + const UIF_PAIR& x = uif_pair; + assert(x.second.timediff == 0); + wires2[2] = vec_ids[x.second.idx]; + wires2[0] = x.fMark ? Wlc_ObjFaninId1(Wlc_NtkObj(p, vec_ids[x.second.idx])) : Wlc_ObjFaninId0(Wlc_NtkObj(p, vec_ids[x.second.idx])); + wires2[1] = x.fMark ? Wlc_ObjFaninId0(Wlc_NtkObj(p, vec_ids[x.second.idx])) : Wlc_ObjFaninId1(Wlc_NtkObj(p, vec_ids[x.second.idx])); + + if (x.first.timediff == 0) { + wires1[2] = vec_ids[x.first.idx]; + wires1[0] = Wlc_ObjFaninId0(Wlc_NtkObj(p, vec_ids[x.first.idx])); + wires1[1] = Wlc_ObjFaninId1(Wlc_NtkObj(p, vec_ids[x.first.idx])); + } else { + int ci_idx = vv_op_ffs[x.first.idx][0 - x.first.timediff - 1]; + wires1[2] = Wlc_ObjId(p, Wlc_NtkCi(p, ci_idx)); + wires1[1] = Wlc_ObjId(p, Wlc_NtkCi(p, ci_idx - 1)); + wires1[0] = Wlc_ObjId(p, Wlc_NtkCi(p, ci_idx - 2)); + } +} + +static Gia_Man_t * unroll_with_cex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, int nbits_old_pis, int num_sel_pis, int * p_num_ppis, bool sel_pi_first) { + Gia_Man_t * pGiaChoice = BitBlast( pChoice ); + + int nbits_new_pis = compute_bit_level_pi_num(pChoice); + int num_ppis = nbits_new_pis - nbits_old_pis - num_sel_pis; + *p_num_ppis = num_ppis; + int num_undc_pis = Gia_ManPiNum(pGiaChoice) - nbits_new_pis; + LOG(3) << "#orig_pis = " << nbits_old_pis << ", #ppis = " << num_ppis << ", #sel_pis = " << num_sel_pis << ", #undc_pis = " << num_undc_pis; + assert(Gia_ManPiNum(pGiaChoice)==nbits_old_pis+num_ppis+num_sel_pis+num_undc_pis); + assert(Gia_ManPiNum(pGiaChoice)==pCex->nPis+num_sel_pis); + + Gia_Man_t * pFrames = NULL; + + Gia_Obj_t * pObj, * pObjRi; + int f, i; + pFrames = Gia_ManStart( 10000 ); + pFrames->pName = Abc_UtilStrsav( pGiaChoice->pName ); + Gia_ManHashAlloc( pFrames ); + Gia_ManConst0(pGiaChoice)->Value = 0; + Gia_ManForEachRi( pGiaChoice, pObj, i ) + pObj->Value = 0; + + auto is_sel_pi = [=](int iPi) { + return (sel_pi_first ? iPi < nbits_old_pis + num_sel_pis : iPi >= nbits_old_pis + num_ppis); + }; + + for ( f = 0; f <= pCex->iFrame; f++ ) { + for( i = 0; i < Gia_ManPiNum(pGiaChoice); i++ ) { + if ( i >= nbits_old_pis && i < nbits_old_pis + num_ppis + num_sel_pis ) { + if(f == 0 || !is_sel_pi(i)) + Gia_ManPi(pGiaChoice, i)->Value = Gia_ManAppendCi(pFrames); + } else if (i < nbits_old_pis) { + Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i); + } else if (i >= nbits_old_pis + num_ppis + num_sel_pis) { + Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i - num_sel_pis); + } + } + Gia_ManForEachRiRo( pGiaChoice, pObjRi, pObj, i ) + pObj->Value = pObjRi->Value; + Gia_ManForEachAnd( pGiaChoice, pObj, i ) + pObj->Value = Gia_ManHashAnd(pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj)); + Gia_ManForEachCo( pGiaChoice, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + Gia_ManForEachPo( pGiaChoice, pObj, i ) + Gia_ManAppendCo(pFrames, pObj->Value); + } + Gia_ManHashStop (pFrames); + Gia_ManSetRegNum(pFrames, 0); + Gia_Man_t * pGia; + pFrames = Gia_ManCleanup(pGia = pFrames); + Gia_ManStop(pGia); + Gia_ManStop(pGiaChoice); + + return pFrames; +} + +static void compute_core_using_sat(Gia_Man_t * pFrames, vector& vec_cores, int nFrames, int num_sel_pis, int num_other_pis, bool sel_pi_first, VecVecInt* ppi_model = NULL, bool fSatMin = false, int nConfLimit = 0) { + Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames ); + Cnf_Dat_t * pCnf = Cnf_Derive(pAigFrames, Aig_ManCoNum(pAigFrames)); + sat_solver * pSat = sat_solver_new(); + sat_solver_setnvars(pSat, pCnf->nVars); + for (unsigned i = 0; i < pCnf->nClauses; i++) { + if (!sat_solver_addclause(pSat, pCnf->pClauses[i], pCnf->pClauses[i + 1])) + assert(false); + } + { + Vec_Int_t* vLits = Vec_IntAlloc(100); + Aig_Obj_t* pObj; + int i; + Aig_ManForEachCo( pAigFrames, pObj, i ) + { + assert(pCnf->pVarNums[pObj->Id] >= 0); + Vec_IntPush(vLits, toLitCond(pCnf->pVarNums[pObj->Id], 0)); + } + int ret = sat_solver_addclause(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits)); + if (!ret) { + LOG(0) << "UNSAT after adding PO clause."; + } + + Vec_IntFree(vLits); + } + { + Vec_Int_t* vLits = Vec_IntAlloc(100); + map varMap; + int first_sel_pi = sel_pi_first ? 0 : num_other_pis; + for (int i = 0; i < num_sel_pis; i++) { + //for (int i = num_sel_pis - 1; i >= 0; --i) { + int cur_pi = first_sel_pi + i; + int var = pCnf->pVarNums[Aig_ManCi(pAigFrames, cur_pi)->Id]; + assert(var >= 0); + varMap[var] = i; + Vec_IntPush(vLits, toLitCond(var, 0)); + } + if(log_level() >= 3) { + int i, Entry; + ostringstream oss; + oss << "#vLits = " << Vec_IntSize(vLits) << "; vLits = "; + Vec_IntForEachEntry(vLits, Entry, i) + oss << Entry << " "; + LOG(3) << oss.str(); + } + int status = sat_solver_solve(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)(nConfLimit), (ABC_INT64_T)(0), (ABC_INT64_T)(0), (ABC_INT64_T)(0)); + if (status == l_False) { + LOG(3) << "UNSAT."; + int nCoreLits, *pCoreLits; + nCoreLits = sat_solver_final(pSat, &pCoreLits); + + vector vec_cores_marks (Vec_IntSize(vLits),false); + for (int i = 0; i < nCoreLits; i++) { + vec_cores_marks[varMap[lit_var(pCoreLits[i])]] = true; + } + + // SAT-min + if (fSatMin && nCoreLits > 1) { + for (int i = 0; i < vec_cores_marks.size(); i++) { + if (!vec_cores_marks[i]) + Vec_IntWriteEntry(vLits, i, lit_neg(Vec_IntEntry(vLits, i))); + } + + for (int i = 0; i < vec_cores_marks.size(); i++) { + if (!vec_cores_marks[i]) + continue; + + Vec_IntWriteEntry(vLits, i, lit_neg(Vec_IntEntry(vLits, i))); + int status = sat_solver_solve(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T) (5000), (ABC_INT64_T) (0), (ABC_INT64_T) (0), (ABC_INT64_T) (0)); + + if (status == l_False) { + LOG(4) << "Loop[" << i << "] : Drop 1 literal = " << Vec_IntEntry(vLits, i); + vec_cores_marks[i] = false; + } else { + if (status == l_True) + LOG(4) << "Loop[" << i << "] : SAT"; + else + LOG(4) << "Loop[" << i << "] : Unknown"; + Vec_IntWriteEntry(vLits, i, lit_neg(Vec_IntEntry(vLits, i))); + } + } + LOG(2) << "SAT-MIN : " << nCoreLits << " ==> " << count(vec_cores_marks.begin(), vec_cores_marks.end(), true); + } + + for (int i = 0; i < vec_cores_marks.size(); i++) { + if(vec_cores_marks[i]) + vec_cores.push_back(i); + } + } else if (status == l_True) { + LOG(3) << "SAT."; + + if (ppi_model && sel_pi_first) { + ppi_model->clear(); + for (int f = 0; f < nFrames; f++) { + ppi_model->push_back(vector()); + for (int i = 0; i < num_other_pis; i++) { + int cur_pi = num_sel_pis + f * num_other_pis + i; + int var = pCnf->pVarNums[Aig_ManCi(pAigFrames, cur_pi)->Id]; + ppi_model->back().push_back(sat_solver_var_value(pSat, var)); + } + } + } + } else { + LOG(3) << "UNKNOWN."; + } + + Vec_IntFree(vLits); + } + Cnf_ManFree(); + sat_solver_delete(pSat); + Aig_ManStop(pAigFrames); +} + +std::ostream& operator<<(ostream& os, const OperatorID& obj) { + os << obj.idx << " @ " << obj.timediff; + return os; +} + +class SimUifPairFinder { + public: + SimUifPairFinder(Wlc_Ntk_t * pOrig, const vector* p_vec_ids) : + nWords(1), + nFrames(1), + nThreshold(0), + _pOrigNtk(pOrig), + _p_vec_op_ids(p_vec_ids) + {} + + void Simulate() { + _compute_max_bw(); + _simulate_and_count(); + } + void ComputeUifPairs() { + _insert_sim_pairs(); + } + void SetParams(const string& setting); + + bool HasResults() const {return !_mat_pairwise_matches.empty();} + int GetCount(const UIF_PAIR& x) const; + bool IsGood(const UIF_PAIR& x) const {return (GetCount(x) >= nThreshold);} + void AddPair(const UIF_PAIR& x); + + const set* GetSimPairsPtr() { return &_set_sim_pairs; } + + int nWords; + int nFrames; + int nThreshold; + private: + void _compute_max_bw() { ComputeMaxBW(_pOrigNtk, *_p_vec_op_ids, _max_input_bw, _max_output_bw); } + void _simulate_and_count(); + void _insert_sim_pairs(); + void _count_matches(Vec_Ptr_t * vRes, int range); + Vec_Int_t * _collect_sim_nodes(Wlc_Ntk_t * pNtk); + + Wlc_Ntk_t * _pOrigNtk; + const vector* _p_vec_op_ids; + + set _set_sim_pairs; + + int _max_input_bw {-1}; + int _max_output_bw {-1}; + + VecVecInt _mat_pairwise_matches; +}; + +void SimUifPairFinder::AddPair(const UIF_PAIR& x) { + assert(x.first.timediff == 0 && x.second.timediff == 0); + assert(x.first.idx < x.second.idx); + + if(x.fMark) + _mat_pairwise_matches[x.second.idx][x.first.idx] += nThreshold; + else + _mat_pairwise_matches[x.first.idx][x.second.idx] += nThreshold; +} +int SimUifPairFinder::GetCount(const UIF_PAIR& x) const { + assert(x.first.timediff == 0 && x.second.timediff == 0); + assert(x.first.idx < x.second.idx); + + return (x.fMark ? _mat_pairwise_matches[x.second.idx][x.first.idx] : _mat_pairwise_matches[x.first.idx][x.second.idx]); +} + +void SimUifPairFinder::SetParams(const string& setting) { + int temp = 0; + smatch sub_match; + + if(regex_search(setting, sub_match, regex(R"(w:(\d+))"))) + nWords = stoi(sub_match[1].str()); + + if(regex_search(setting, sub_match, regex(R"(f:(\d+))"))) + nFrames = stoi(sub_match[1].str()); + + if(regex_search(setting, sub_match, regex(R"(t:(\d+))"))) + temp = stoi(sub_match[1].str()); + + nThreshold = temp * nWords * nFrames * 64 / 100; +} + +Vec_Int_t * SimUifPairFinder::_collect_sim_nodes(Wlc_Ntk_t * pNtk) { + Vec_Int_t * vNodes = Vec_IntAlloc( _p_vec_op_ids->size() * 2 ); + int i; + Wlc_Obj_t * pPo; + int range = Wlc_ObjRange(Wlc_NtkPo(pNtk, 1)); + Wlc_NtkForEachPo(pNtk, pPo, i) { + if ((i%3)==0) continue; + assert(range == Wlc_ObjRange(pPo)); + Vec_IntPush(vNodes, Wlc_ObjId(pNtk, pPo)); + } + assert(Vec_IntSize(vNodes) == _p_vec_op_ids->size() * 2); + + return vNodes; +} + +static unsigned bit_count (word value) { + unsigned count = 0; + while (value > 0) { // until all bits are zero + if ((value & 1) == 1) // check lower bit + count++; + value >>= 1; // shift bits, removing lower bit + } + return count; +} + +static void bit_print (word value) { + int n_bits = 0; + while(n_bits < 64) { + if ((value & 1) == 1) + cout << "1"; + else + cout << "0"; + value >>= 1; + n_bits++; + } + cout << endl; +} + +void SimUifPairFinder::_count_matches(Vec_Ptr_t * vRes, int range) { + VecVecInt& mat = _mat_pairwise_matches; + int num_ops = _p_vec_op_ids->size(); + mat = VecVecInt(num_ops, vector(num_ops, 0)); + array op1, op2; + + for(int i = 0; i < num_ops; i++) { + for(int j = 0; j < num_ops; j++) { + if (i == j) continue; + + for(int f = 0; f < nFrames; f++) { + vector merges(nWords, ~0); + + op1[0] = (i < j) ? (i << 1) : (i << 1) + 1; + op1[1] = (i < j) ? (i << 1) + 1 : (i << 1); + op2[0] = (j << 1); + op2[1] = (j << 1) + 1; + + for (int k = 0; k < range; k++) { + for (int w = 0; w < nWords; w++) { + word w1, w2; + w1 = ((word*) Vec_VecEntryEntry((Vec_Vec_t *) vRes, op1[0], k))[f * nWords + w]; + w2 = ((word*) Vec_VecEntryEntry((Vec_Vec_t *) vRes, op2[0], k))[f * nWords + w]; + merges[w] = merges[w] & (~(w1 ^ w2)); + + w1 = ((word*) Vec_VecEntryEntry((Vec_Vec_t *) vRes, op1[1], k))[f * nWords + w]; + w2 = ((word*) Vec_VecEntryEntry((Vec_Vec_t *) vRes, op2[1], k))[f * nWords + w]; + merges[w] = merges[w] & (~(w1 ^ w2)); + } + } + + for (int w = 0; w < nWords; w++) { + mat[i][j] += bit_count(merges[w]); + } + } + } + } + + /* + for(int i = 0; i < num_ops; ++i) { + for(int j = 0; j < num_ops; ++j) { + if(i == j) continue; + if(mat[i][j] == 0) continue; + cout << "[" << i << "][" << j << "] = " << mat[i][j] << endl; + } + } + */ +} + +void SimUifPairFinder::_simulate_and_count() { + vector vec_ids = *_p_vec_op_ids; + Wlc_Ntk_t * pSimNtk = AddAuxPOsForOperators(_pOrigNtk, vec_ids, _max_input_bw, _max_output_bw); + Vec_Int_t * vNodes = _collect_sim_nodes(pSimNtk); + Vec_Ptr_t * vRes; + vRes = Wlc_NtkSimulate( pSimNtk, vNodes, nWords, nFrames ); + // Wlc_NtkSimulatePrint(pSimNtk, vNodes, vRes, nWords, nFrames); + _count_matches(vRes, Wlc_ObjRange(Wlc_NtkObj(pSimNtk, Vec_IntEntry(vNodes, 0)))); + + Wlc_NtkFree(pSimNtk); + Vec_IntFree(vNodes); + Wlc_NtkDeleteSim(vRes); +} + +void SimUifPairFinder::_insert_sim_pairs() { + VecVecInt& mat = _mat_pairwise_matches; + _set_sim_pairs.clear(); + + int num_ops = mat.size(); + + for(int i = 0; i < num_ops; ++i) { + for(int j = 0; j < num_ops; ++j) { + if(i == j) continue; + if(mat[i][j] < nThreshold) continue; + + if (i < j) + _set_sim_pairs.insert(UIF_PAIR(OperatorID(i), OperatorID(j), 0)); + else + _set_sim_pairs.insert(UIF_PAIR(OperatorID(j), OperatorID(i), 1)); + } + } +} + +class CexUifPairFinder { + public: + CexUifPairFinder(Wlc_Ntk_t * pOrigNtk, const vector* p_vec_op_ids) : + _pOrigNtk(pOrigNtk), + _p_vec_op_ids(p_vec_op_ids) + {} + + void SetStates(Abc_Cex_t * pCex, const vector* p_vec_op_marks, const set* p_set_uif_pairs, set* p_set_prev_ops, const UfarManager::Params* p_params) { + _pCex = pCex; + _p_vec_op_blackbox_marks = p_vec_op_marks; + _p_set_uif_pairs = p_set_uif_pairs; + _p_set_prev_ops = p_set_prev_ops; + _p_params = p_params; + } + void FindUifPairs(const VecVecChar& cex_po_values, unsigned nLookBack, set& set_new_pairs); + void FindUifPairsBasic(const VecVecChar& cex_po_values, unsigned nLookBack, set& set_new_pairs); + void ComputeCoreUifPairs(const set& set_candidates, set& set_core, Abc_Cex_t ** ppCex); + const VecVecStr* GetOutputs() const {return &_outputs;} + private: + void _compute_max_bw(); + string _get_bitstr(Wlc_Obj_t * pObj, const VecChar& cur_pos, unsigned& pos, bool isOutput); + + Wlc_Ntk_t * _introduce_choices(const set& set_candidates, vector& vec_choice2pair); + Wlc_Ntk_t * _apply_uif_pairs_with_choices(Wlc_Ntk_t * pNtk, const VecVecInt& vv_op_ffs, vector& vec_ids, const set& set_candidates, vector& vec_choice2pair); + + Wlc_Ntk_t * _pOrigNtk; + const vector* _p_vec_op_ids; + + Abc_Cex_t * _pCex {NULL}; + const vector* _p_vec_op_blackbox_marks {NULL}; + const set* _p_set_uif_pairs {NULL}; + set* _p_set_prev_ops {NULL}; + const UfarManager::Params* _p_params {NULL}; + + int _max_input_bw {-1}; + int _max_output_bw {-1}; + + VecVecStr _outputs; + VecVecStr _inputs; +}; + +void CexUifPairFinder::_compute_max_bw() { + // compute max bit-width + ComputeMaxBW(_pOrigNtk, *_p_vec_op_ids, _max_input_bw, _max_output_bw); + LOG(3) << "maxIn = " << _max_input_bw << "; maxOut = " << _max_output_bw; +} + +string CexUifPairFinder::_get_bitstr(Wlc_Obj_t * pObj, const VecChar& cur_pos, unsigned& pos, bool isOutput) { + int range = Wlc_ObjRange(pObj); + int max_bw = isOutput ? _max_output_bw : _max_input_bw; + string bitstr = string(cur_pos.begin() + pos, cur_pos.begin() + pos + range).append(max_bw - range, *(cur_pos.begin() + pos + range - 1)); + pos += range; + + return bitstr; +} + +Wlc_Ntk_t * CexUifPairFinder::_apply_uif_pairs_with_choices(Wlc_Ntk_t * pNtk, const VecVecInt& vv_op_ffs, vector& vec_ids, const set& set_candidates, vector& vec_choice2pair) { + array wires1; + array wires2; + + Wlc_Ntk_t * p = DupNtkAndUpdateIDs(pNtk, vec_ids); + Vec_Int_t * vUifConstrs = Vec_IntAlloc( 100 ); + Vec_Int_t * vFanins = Vec_IntAlloc( 2 ); + + for(auto& x : *_p_set_uif_pairs) { + get_operator_pair(p, x, wires1, wires2, vec_ids, vv_op_ffs); + int iObj = AddOneUifImplication(p, wires1, wires2); + Vec_IntPush(vUifConstrs, iObj); + } + + for(auto& x : set_candidates) { + vec_choice2pair.push_back(x); + get_operator_pair(p, x, wires1, wires2, vec_ids, vv_op_ffs); + int iObj = AddOneUifImplication(p, wires1, wires2); + int iSelPi = Wlc_ObjAlloc( p, WLC_OBJ_PI, 0, 0, 0); + Vec_IntFill(vFanins, 1, iSelPi); + int iSelPiNeg = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_NOT, 0, 0, 0, vFanins); + Vec_IntFillTwo(vFanins, 2, iObj, iSelPiNeg); + int iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins); + Vec_IntPush(vUifConstrs, iObjNew); + } + + if (Wlc_NtkFfNum(_pOrigNtk) == 0) + FoldCombConstraints(p, vUifConstrs); + else + FoldSeqConstraints(p, vUifConstrs); + + Wlc_Ntk_t * pNew = DupNtkAndUpdateIDs(p, vec_ids); + + Wlc_NtkFree(p); + Vec_IntFree(vUifConstrs); + Vec_IntFree(vFanins); + + return pNew; +} + +Wlc_Ntk_t * CexUifPairFinder::_introduce_choices(const set& set_candidates, vector& vec_choice2pair) { + vector vec_ids = *_p_vec_op_ids; + VecVecInt vv_op_ffs; + Wlc_Ntk_t * pNew, * pTemp; + + if(!_p_set_prev_ops->empty()) + pNew = IntroducePrevOperators(_pOrigNtk, vec_ids, *_p_set_prev_ops, vv_op_ffs); + else + pNew = DupNtkAndUpdateIDs(_pOrigNtk, vec_ids); + + if(_p_params->fGrey) { + pNew = ApplyGreyConstraints(pTemp = pNew, vec_ids, Wlc_NtkFfNum(_pOrigNtk) > 0); + Wlc_NtkFree(pTemp); + } + + pNew = _apply_uif_pairs_with_choices(pTemp = pNew, vv_op_ffs, vec_ids, set_candidates, vec_choice2pair); + Wlc_NtkFree(pTemp); + + Vec_Int_t * vec_ops = collect_boxes(vec_ids, *_p_vec_op_blackbox_marks, true /*black*/); + assert(Vec_IntSize(vec_ops) > 0); + pNew = AbstractNodes(pTemp = pNew, vec_ops); + Wlc_NtkFree(pTemp); + + return pNew; +} + + +static Abc_Cex_t * get_new_cex_with_ppi(Abc_Cex_t * pOrigCex, const VecVecInt& ppi_model, int num_orig_pis, int num_ppis, bool one_more_flop) { + Abc_Cex_t * pCex = Abc_CexAlloc( one_more_flop ? pOrigCex->nRegs + 1 : pOrigCex->nRegs, pOrigCex->nPis, pOrigCex->iFrame + 1); + pCex->iFrame = pOrigCex->iFrame; + pCex->iPo = 0; + + for(int f = 0; f < pOrigCex->iFrame + 1; f++) { + for(int i = 0; i < pOrigCex->nPis; i++) { + int iOrigBit = pOrigCex->nRegs+pOrigCex->nPis*f + i; + int iBit = one_more_flop ? iOrigBit + 1 : iOrigBit; + if ( i >= num_orig_pis && i < num_orig_pis + num_ppis ) { + if(ppi_model[f][i-num_orig_pis]) { + Abc_InfoSetBit(pCex->pData, iBit); + } + } else { // i < num_orig_pis || i >= num_orig_pis + num_ppis + if(Abc_InfoHasBit(pOrigCex->pData, iOrigBit)) { + Abc_InfoSetBit(pCex->pData, iBit); + } + } + } + } + + return pCex; +} + +void CexUifPairFinder::ComputeCoreUifPairs(const set& set_candidates, set& set_core, Abc_Cex_t ** ppCex) { + vector vec_choice2pair; + Wlc_Ntk_t * pChoice = _introduce_choices(set_candidates, vec_choice2pair); + assert(set_candidates.size() == vec_choice2pair.size()); + + int num_ppis; + int num_orig_pis = compute_bit_level_pi_num(_pOrigNtk); + Gia_Man_t * pGiaFrames = unroll_with_cex(pChoice, _pCex, num_orig_pis, vec_choice2pair.size(), &num_ppis, true); + + vector vec_cores; + VecVecInt ppi_model; + compute_core_using_sat(pGiaFrames, vec_cores, _pCex->iFrame+1, vec_choice2pair.size(), num_ppis, true, &ppi_model, false, 5000); + if(ppCex && !ppi_model.empty()) { + if(*ppCex) Abc_CexFree(*ppCex); + *ppCex = get_new_cex_with_ppi(_pCex, ppi_model, num_orig_pis, num_ppis, _p_set_uif_pairs->empty() && Wlc_NtkFfNum(_pOrigNtk)); + } + // Abc_CexPrintStats(_pCex); + // Abc_CexPrintStats(*ppCex); + + set_core.clear(); + for(auto& x : vec_cores) { + set_core.insert(vec_choice2pair[x]); + } + + Gia_ManStop(pGiaFrames); + Wlc_NtkFree(pChoice); +} + +void CexUifPairFinder::FindUifPairsBasic(const VecVecChar& cex_po_values, unsigned nLookBack, set& set_new_pairs) { + assert(Wlc_NtkPoNum(_pOrigNtk) == 1); + assert(Wlc_ObjRange(Wlc_NtkPo(_pOrigNtk, 0)) == 1); + + _inputs.clear(); + _outputs.clear(); + + for (unsigned f = 0; f < cex_po_values.size(); f++) { + _inputs.push_back(vector()); + _outputs.push_back(vector()); + + const vector& cur_po_values = cex_po_values[f]; + unsigned pos = 1; + + for (unsigned i = 0; i < _p_vec_op_ids->size(); i++) { + int op_id = _p_vec_op_ids->at(i); + Wlc_Obj_t * pObj = Wlc_NtkObj(_pOrigNtk, op_id); + + Wlc_Obj_t * pObjInput = NULL; + + pObjInput = Wlc_ObjFanin0(_pOrigNtk, pObj); + _max_input_bw = Wlc_ObjRange(pObjInput); + string bits_input0 = _get_bitstr(pObjInput, cur_po_values, pos, false); + bits_input0 += (Wlc_ObjIsSigned(pObjInput) ? 's' : 'u'); + + pObjInput = Wlc_ObjFanin1(_pOrigNtk, pObj); + _max_input_bw = Wlc_ObjRange(pObjInput); + string bits_input1 = _get_bitstr(pObjInput, cur_po_values, pos, false); + bits_input1 += (Wlc_ObjIsSigned(pObjInput) ? 's' : 'u'); + + _max_output_bw = Wlc_ObjRange(pObj); + string bits_output = _get_bitstr(pObj, cur_po_values, pos, true); + bits_output += (Wlc_ObjIsSigned(pObj) ? 's' : 'u'); + _outputs.back().push_back(bits_output); + + vector keys; + keys.push_back(bits_input0 + ':' + bits_input1); + keys.push_back(bits_input1 + ':' + bits_input0); + _inputs.back().push_back(keys[0]); + + + for (unsigned reversed = 0; reversed < keys.size(); reversed++) { + const string& key = keys[reversed]; + for (int g = f; g >= 0 && g >= (int)f - (int)nLookBack; g--) { + for (int j = 0; j < _inputs[g].size(); j++) { + if (!bitstr_not_equal(key, _inputs[g][j]) && bitstr_not_equal(_outputs[f][i], _outputs[g][j])) { + UIF_PAIR pair_int(OperatorID(j, g-f), OperatorID(i), reversed); + if (_p_set_uif_pairs->count(pair_int) == 0) + set_new_pairs.insert(pair_int); + if(g < f) + _p_set_prev_ops->insert(OperatorID(j, g-f)); + } + } + } + } + LOG(4) << "[" << f << "][" << i << "] : " << "key = " << keys[0] << " output = " << _outputs[f][i] ; + } + } +} + +void CexUifPairFinder::FindUifPairs(const VecVecChar& cex_po_values, unsigned nLookBack, set& set_new_pairs) { + assert(Wlc_NtkPoNum(_pOrigNtk) == 1); + assert(Wlc_ObjRange(Wlc_NtkPo(_pOrigNtk, 0)) == 1); + + _compute_max_bw(); + + _inputs.clear(); + _outputs.clear(); + + for (unsigned f = 0; f < cex_po_values.size(); f++) { + + _inputs.push_back(vector()); + _outputs.push_back(vector()); + + const vector& cur_po_values = cex_po_values[f]; + unsigned pos = 1; + + for (unsigned i = 0; i < _p_vec_op_ids->size(); i++) { + int op_id = _p_vec_op_ids->at(i); + Wlc_Obj_t * pObj = Wlc_NtkObj(_pOrigNtk, op_id); + + string bits_input0 = _get_bitstr(Wlc_ObjFanin0(_pOrigNtk, pObj), cur_po_values, pos, false); + string bits_input1 = _get_bitstr(Wlc_ObjFanin1(_pOrigNtk, pObj), cur_po_values, pos, false); + assert(bits_input0.size() == bits_input1.size()); + + string bits_output = _get_bitstr(pObj, cur_po_values, pos, true); + _outputs.back().push_back(bits_output); + + vector keys; + keys.push_back(bits_input0 + ':' + bits_input1); + keys.push_back(bits_input1 + ':' + bits_input0); + _inputs.back().push_back(keys[0]); + + for (unsigned reversed = 0; reversed < keys.size(); reversed++) { + const string& key = keys[reversed]; + for (int g = f; g >= 0 && g >= (int)f - (int)nLookBack; g--) { + for (int j = 0; j < _inputs[g].size(); j++) { + if (!bitstr_not_equal(key, _inputs[g][j]) && bitstr_not_equal(_outputs[f][i], _outputs[g][j])) { + UIF_PAIR pair_int(OperatorID(j, g-f), OperatorID(i), reversed); + if (_p_set_uif_pairs->count(pair_int) == 0) + set_new_pairs.insert(pair_int); + if(g < f) + _p_set_prev_ops->insert(OperatorID(j, g-f)); + } + } + } + } + LOG(4) << "[" << f << "][" << i << "] : " << "key = " << keys[0] << " output = " << _outputs[f][i] ; + } + } + +} + +UfarManager::Params::Params() : + fCexMin(true), + fPbaUif(false), + fLazySim(true), + fPbaSim(false), + fPbaCex(false), + fSatMin(false), + fCbaWb(false), + fGrey(false), + nGrey(0), + fNorm(true), + fSuper_prove(false), + fSimple(false), + fSyn(false), + fPthread(false), + iOneWb(-1), + iExp(-1), + nConstraintLimit(65536), + iVerbosity(0), + nSeqLookBack(0), + nTimeout(65536) + {} +UfarManager::UfarManager() : _pOrigNtk(NULL), _pAbsWithAuxPos(NULL) {} + +UfarManager::~UfarManager() { + if (_pOrigNtk) Wlc_NtkFree(_pOrigNtk); +} + +void UfarManager::Initialize(Wlc_Ntk_t * pNtk, const set& types) { + if (_pOrigNtk) Wlc_NtkFree(_pOrigNtk); + _vec_orig_names.clear(); + _vec_op_ids.clear(); + _vec_op_blackbox_marks.clear(); + _vec_op_greyness.clear(); + _set_uif_pairs.clear(); + _set_uif_sim_pairs.clear(); + + _vec_vec_op_ffs.clear(); + _set_prev_ops.clear(); + + profile = Profile(); + + _pOrigNtk = Wlc_NtkDupDfsSimple(pNtk); + + Wlc_Obj_t * pObj; + int i; + _vec_orig_names.resize(Wlc_NtkObjNumMax(pNtk)); + Wlc_NtkForEachObj(pNtk, pObj, i) { + _vec_orig_names[i] = (Wlc_ObjName(pNtk, i)); + + if(types.count(pObj->Type) > 0) { + _vec_op_ids.push_back(i); + if(params.nGrey) { + _vec_op_greyness.push_back(Greyness(pNtk, pObj)); + } + } + } + + _vec_op_blackbox_marks.resize(_vec_op_ids.size(), true); + + _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; + _timeout.tv_nsec = now.tv_usec * 1000; +} + +Wlc_Ntk_t * UfarManager::ApplyUifConstraints(Wlc_Ntk_t * pNtk, vector& vec_ids) { + array wires1; + array wires2; + + Wlc_Ntk_t * p = DupNtkAndUpdateIDs(pNtk, vec_ids); + Vec_Int_t * vUifConstrs = Vec_IntAlloc( 100 ); + + for(auto& x : _set_uif_pairs) { + get_operator_pair(p, x, wires1, wires2, vec_ids, _vec_vec_op_ffs); + int iObj = AddOneUifImplication(p, wires1, wires2); + Vec_IntPush(vUifConstrs, iObj); + } + + if (Wlc_NtkFfNum(_pOrigNtk) == 0) + FoldCombConstraints(p, vUifConstrs); + else + FoldSeqConstraints(p, vUifConstrs); + + Wlc_Ntk_t * pNew = DupNtkAndUpdateIDs(p, vec_ids); + + Wlc_NtkFree(p); + Vec_IntFree(vUifConstrs); + + return pNew; +} + +Wlc_Ntk_t * UfarManager::_set_up_constraints(vector& vec_ids) { + Wlc_Ntk_t * pNew, * pTemp; + + if(!_set_prev_ops.empty()) + pNew = IntroducePrevOperators(_pOrigNtk, vec_ids, _set_prev_ops, _vec_vec_op_ffs); + else + pNew = DupNtkAndUpdateIDs(_pOrigNtk, vec_ids); + + if(params.fGrey) { + pNew = ApplyGreyConstraints(pTemp = pNew, vec_ids, Wlc_NtkFfNum(_pOrigNtk) > 0); + Wlc_NtkFree(pTemp); + } + + if(!_set_uif_pairs.empty()) { + pNew = ApplyUifConstraints(pTemp = pNew, vec_ids); + Wlc_NtkFree(pTemp); + } + + if(params.nGrey) { + pNew = ApplyGreynessConstraints(pTemp = pNew, _vec_op_greyness, vec_ids); + Wlc_NtkFree(pTemp); + } + + return pNew; +} + + +Wlc_Ntk_t * UfarManager::BuildCurrentAbstraction() { + vector vec_ids = _vec_op_ids; + Wlc_Ntk_t * pNew, * pTemp; + + pNew = _set_up_constraints(vec_ids); + + pNew = AddAuxPOsForOperators(pTemp = pNew, vec_ids); + Wlc_NtkFree(pTemp); + // for(auto x : vec_ids) cout << "ID = " << x << " Type = " << Wlc_NtkObj(pNew, x)->Type << endl; + + if (count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), true) > 0) { + pNew = _abstract_operators(pTemp = pNew, vec_ids); + Wlc_NtkFree(pTemp); + } + + if(_pAbsWithAuxPos) Wlc_NtkFree(_pAbsWithAuxPos); + _pAbsWithAuxPos = Wlc_NtkDupDfsSimple(pNew); + + pNew = RemoveAuxPOs(pTemp = pNew, Wlc_NtkPoNum(_pOrigNtk)); + Wlc_NtkFree(pTemp); + + // Wlc_WriteVer(pNew, "Abs.v", 0, 0); + + return pNew; +} + +void UfarManager::_simulate() { + timeval t1, t2; + gettimeofday(&t1, NULL); + + _p_sim_mgr->SetParams(params.simSetting); + _p_sim_mgr->Simulate(); + + gettimeofday(&t2, NULL); + profile.tUifSim += elapsed_time_usec(t1, t2); +} + +void UfarManager::FindUifPairsUsingSim() { + timeval t1, t2; + gettimeofday(&t1, NULL); + + _p_sim_mgr->ComputeUifPairs(); + _set_uif_sim_pairs = *_p_sim_mgr->GetSimPairsPtr(); + + set set_new_pairs; + for(auto& x:_set_uif_sim_pairs) { + auto res = _set_uif_pairs.insert(x); + if(res.second) + set_new_pairs.insert(x); + } + if(log_level() >= 3) + print_pairs(set_new_pairs); + + gettimeofday(&t2, NULL); + profile.tUifSim += elapsed_time_usec(t1, t2); +} + +void UfarManager::FindUifPairsUsingCex(Abc_Cex_t * pCex, Abc_Cex_t ** ppCex) { + timeval t1, t2; + gettimeofday(&t1, NULL); + + VecVecChar cex_po_values; + Gia_Man_t * pGia = BitBlast(_pAbsWithAuxPos); + CollectPoValuesInCex(pGia, pCex, cex_po_values, params.fCexMin); + Gia_ManStop(pGia); + + _p_cex_mgr->SetStates(pCex, &_vec_op_blackbox_marks, &_set_uif_pairs, &_set_prev_ops, ¶ms); + set set_found_pairs, set_temp; + if (params.fNorm) { + _p_cex_mgr->FindUifPairs(cex_po_values, params.nSeqLookBack, set_found_pairs); + } else { + _p_cex_mgr->FindUifPairsBasic(cex_po_values, params.nSeqLookBack, set_found_pairs); + } + if(log_level() >= 3) print_pairs(set_found_pairs); + + if(params.fPbaUif && !set_found_pairs.empty()) { + _p_cex_mgr->ComputeCoreUifPairs(set_temp = set_found_pairs, set_found_pairs, ppCex); + if(set_found_pairs.empty()) { + LOG(2) << "Proof-based refinement failed (SAT)"; + // set_found_pairs = set_temp; + if(params.fPbaCex) { + set_found_pairs = set_temp; + } + if(params.fPbaSim && _p_sim_mgr->HasResults()) { + for(auto& x : set_temp) { + if(_p_sim_mgr->GetCount(x) > 0) + set_found_pairs.insert(x); + } + if(set_found_pairs.empty()) { + LOG(2) << "No pair found with PBA and SIM"; + } + } + } + } + + for(auto& x : set_found_pairs) _set_uif_pairs.insert(x); + + gettimeofday(&t2, NULL); + profile.tUifRefine += elapsed_time_usec(t1, t2); +} + +Wlc_Ntk_t * UfarManager::_introduce_bitwise_choices(vector& vec_choice2idx) { + vector vec_ids = _vec_op_ids; + Wlc_Ntk_t * pNew, * pTemp; + + pNew = _set_up_constraints(vec_ids); + + pNew = IntroduceBitwiseChoices(pTemp = pNew, vec_ids, _vec_op_greyness, vec_choice2idx); + Wlc_NtkFree(pTemp); + + return pNew; +} + +Wlc_Ntk_t * UfarManager::_introduce_choices(vector& vec_choice2idx, bool fBlack) { + vector vec_ids = _vec_op_ids; + Wlc_Ntk_t * pNew, * pTemp; + + pNew = _set_up_constraints(vec_ids); + + Vec_Int_t * vec_ops = collect_boxes(vec_ids, _vec_op_blackbox_marks, fBlack); + assert(Vec_IntSize(vec_ops) > 0); + map map_temp; + for(unsigned i = 0; i < vec_ids.size(); i++) + map_temp[vec_ids[i]] = i; + Vec_IntSort(vec_ops, 0); + for(int i = 0; i < Vec_IntSize(vec_ops); i++) + vec_choice2idx.push_back(map_temp[Vec_IntEntry(vec_ops, i)]); + + pNew = IntroduceChoices(pTemp = pNew, vec_ops); + Wlc_NtkFree(pTemp); + Vec_IntFree(vec_ops); + + return pNew; +} + +void UfarManager::_compute_core_choices(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, vector& vec_cores, int num_sel_pis) { + int num_ppis = -1; + Gia_Man_t * pGiaFrames = unroll_with_cex(pChoice, pCex, compute_bit_level_pi_num(_pOrigNtk), num_sel_pis, &num_ppis, false); + + compute_core_using_sat(pGiaFrames, vec_cores, pCex->iFrame+1, num_sel_pis, num_ppis, false, NULL, params.fSatMin); + + Gia_ManStop(pGiaFrames); +} + +void UfarManager::_perform_cex_based_white_boxing() { + const VecVecStr* cex_outputs = _p_cex_mgr->GetOutputs(); + + unsigned nFrames = cex_outputs->size(); + assert(nFrames); + unsigned nOperators = (*cex_outputs)[0].size(); + assert(nOperators == _vec_op_ids.size()); + + vector vec_op_refine(nOperators, false); + for(unsigned i = 0; i < nOperators; i++) { + for(unsigned f = 0; f < nFrames; f++) { + if(!bitstr_all_x((*cex_outputs)[f][i])) { + vec_op_refine[i] = true; + break; + } + } + } + + if(log_level() >= 2) { + _oss.str(""); + _oss << "#vWBs = " << count(vec_op_refine.begin(), vec_op_refine.end(), true) << "(" << nOperators << ")" << "; vWBs = "; + for(unsigned i = 0; i < nOperators; i++) { + if(vec_op_refine[i]) + _oss << i << " "; + } + LOG(2) << _oss.str(); + } + + for(unsigned i = 0; i < nOperators; i++) { + if(vec_op_refine[i]) + _vec_op_blackbox_marks[i] = false; + } +} + +void UfarManager::_shrink_final_abstraction() { + vector vec_choice2idx; + Wlc_Ntk_t * pNtkWithChoices = _introduce_choices(vec_choice2idx, false /*white*/); + + int num_sel_pis = vec_choice2idx.size(); + int num_other_pis = compute_bit_level_pi_num(pNtkWithChoices) - num_sel_pis; + + Gia_Man_t * pMiter = GetInvMiter(pNtkWithChoices, "inv.pla"); + printf("Miter stat: pi = %d, ff = %d, and = %d, po = %d\n", Gia_ManPiNum(pMiter), Gia_ManRegNum(pMiter), Gia_ManAndNum(pMiter), Gia_ManPoNum(pMiter)); + + vector vec_core_choices; + compute_core_using_sat(pMiter, vec_core_choices, 1, num_sel_pis, num_other_pis, false, NULL, params.fSatMin); + + Wlc_NtkFree(pNtkWithChoices); + Gia_ManStop(pMiter); + + LOG(2) << "Shrink from " << vec_choice2idx.size() << " to " << vec_core_choices.size(); + if(log_level() >= 3) { + _oss.str(""); + _oss << "remaining white boxes = "; + for (auto x : vec_core_choices) { + _oss << x << " "; + } + LOG(3) << _oss.str(); + } + + _vec_op_blackbox_marks = vector(_vec_op_ids.size(), true); + for (auto x : vec_core_choices) + _vec_op_blackbox_marks[vec_choice2idx[x]] = false; +} + +void UfarManager::_perform_proof_based_grey_boxing(Abc_Cex_t * pCex) { + vector vec_choice2idx; + Wlc_Ntk_t * pNtkWithChoices = _introduce_bitwise_choices(vec_choice2idx); + + vector vec_core_choices; + _compute_core_choices(pNtkWithChoices, pCex, vec_core_choices, vec_choice2idx.size()); + assert(!vec_core_choices.empty()); + Wlc_NtkFree(pNtkWithChoices); + + if(log_level() >= 4) { + for (auto x : vec_core_choices) { + LOG(4) << "WBit : operator[" << vec_choice2idx[x].first << "] at " << vec_choice2idx[x].second << "/" << _vec_op_greyness[vec_choice2idx[x].first].Size() ; + } + } + + vector vec_change_marks(_vec_op_greyness.size(), false); + for (auto x : vec_core_choices) { + _vec_op_greyness[vec_choice2idx[x].first].Set(vec_choice2idx[x].second, false); + vec_change_marks[vec_choice2idx[x].first] = true; + } + + for (size_t i = 0; i < _vec_op_greyness.size(); ++i) { + Greyness& grey = _vec_op_greyness[i]; + if(vec_change_marks[i]) + grey.UpdateCost(); + + if(grey.IsTooWhite(params.nGrey)) { + LOG(2) << "Grey: SetWhite: [" << i << "] = " << float(grey.CurrentCost())/float(grey.TotalCost()) << " (" << grey.CurrentCost() << " / " << grey.TotalCost() << ") " << grey.to_string(); + grey.SetWhite(); + _vec_op_blackbox_marks[i] = false; + } + } +} + +void UfarManager::_perform_proof_based_white_boxing(Abc_Cex_t * pCex) { + vector vec_choice2idx; + Wlc_Ntk_t * pNtkWithChoices = _introduce_choices(vec_choice2idx, true /*black*/); + + // for(unsigned i = 0; i < vec_choice2idx.size(); i++) cout << "i = " << i << " idx = " << vec_choice2idx[i] << endl; + + vector vec_core_choices; + _compute_core_choices(pNtkWithChoices, pCex, vec_core_choices, vec_choice2idx.size()); + assert(!vec_core_choices.empty()); + Wlc_NtkFree(pNtkWithChoices); + + if(log_level() >= 2) { + _oss.str(""); + _oss << "#vCores = " << vec_core_choices.size() << "; vCores = "; + for (unsigned i = 0; i < vec_core_choices.size(); i++) { + _oss << vec_choice2idx[vec_core_choices[i]] << " "; + } + LOG(2) << _oss.str(); + } + + if (params.iOneWb == -1) { + for (unsigned i = 0; i < vec_core_choices.size(); i++) + _vec_op_blackbox_marks[vec_choice2idx[vec_core_choices[i]]] = false; + } else if (params.iOneWb == 0) { + unsigned idx = 0; + for (auto x : vec_core_choices) { + if (vec_choice2idx[x] > idx) + idx = vec_choice2idx[x]; + } + _vec_op_blackbox_marks[idx] = false; + LOG(2) << "White boxing ID(" << idx << ")"; + } +} + +void UfarManager::DetermineGreyness(Abc_Cex_t *pCex) { + timeval t1, t2; + gettimeofday(&t1, NULL); + + _perform_proof_based_grey_boxing(pCex); + + gettimeofday(&t2, NULL); + profile.tGbRefine += elapsed_time_usec(t1, t2); +} + +void UfarManager::DetermineWhiteBoxes(Abc_Cex_t * pCex) { + timeval t1, t2; + gettimeofday(&t1, NULL); + + if(params.fCbaWb) { + _perform_cex_based_white_boxing(); + } else { + _perform_proof_based_white_boxing(pCex); + } + + gettimeofday(&t2, NULL); + profile.tWbRefine += elapsed_time_usec(t1, t2); +} + +int UfarManager::VerifyCurrentAbstraction(Abc_Cex_t ** ppCex) { + timeval t1, t2; + gettimeofday(&t1, NULL); + + Wlc_Ntk_t * pCurrent = BuildCurrentAbstraction(); + if(!params.fileAbs.empty()) + Wlc_WriteVer(pCurrent, &((params.fileAbs + "_abs.v")[0u]), 0, 0); + + int ret = -1; + /* + if(params.fSuper_prove || params.fSimple) { + ret = super_prove(pCurrent, ppCex, params.fSimple, ¶ms.fileName); + } else { + if ( params.fPthread ) { + ret = verify_model(pCurrent, ppCex, ¶ms.fileName, ¶ms.parSetting, params.fSyn, &_timeout); + } else { + ret = bit_level_solve(pCurrent, ppCex, ¶ms.fileName, ¶ms.parSetting, params.fSyn); + } + } + */ + ret = verify_model(pCurrent, ppCex, ¶ms.fileName, ¶ms.parSetting, params.fSyn, &_timeout); + Wlc_NtkFree(pCurrent); + + gettimeofday(&t2, NULL); + profile.tBLSolver += elapsed_time_usec(t1, t2); + + return ret; +} + +int UfarManager::PerformUIFProve(const timeval& timer) { + struct Mem { + Mem() : pCex(NULL), pCex2(NULL) {} + ~Mem() { + if (pCex) Abc_CexFree(pCex); + if (pCex2) Abc_CexFree(pCex2); + } + Abc_Cex_t * pCex; + Abc_Cex_t * pCex2; + }; + + Mem mem; + char buffer [256]; + int ret; + unsigned n_iter_wb = 0; + unsigned n_iter_uif = 0; + timeval curTime; + float elapsedTime; + + auto dump_grey_stat = [&]() { + if(!params.nGrey || log_level()<2 ) return; + float stat = 0; + for(size_t i = 0; i < _vec_op_greyness.size(); ++i) { + if (_vec_op_greyness[i].IsGrey()) { + unsigned current_cost = _vec_op_greyness[i].CurrentCost(); + unsigned total_cost = _vec_op_greyness[i].TotalCost(); + float cur_stat = float(current_cost) / float(total_cost); + stat += cur_stat; + LOG(2) << "Grey: [" << i << "] = " << setprecision(2) << cur_stat << "\t (" << current_cost << " / " + << total_cost << ") \t" << _vec_op_greyness[i].to_string(); + } + } + LOG(1) << "Grey: [Total] = " << setprecision(4) << stat << " (" << _vec_op_greyness.size() << ")"; + }; + auto print_stat = [&]() { + gettimeofday(&curTime, NULL); + elapsedTime = elapsed_time_usec(timer, curTime)/1000000.0; + sprintf(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); + LOG(1) << buffer << _get_profile_uf_wb(); + dump_grey_stat(); + if(!params.fileStatesOut.empty()) _dump_states(params.fileStatesOut); + }; + + if (!params.fileStatesIn.empty()) { + _read_states(params.fileStatesIn); + if (params.iExp != -1) _massage_state_b(); + print_stat(); + } + + if (!params.fLazySim && !params.simSetting.empty()) { + unsigned origSize = _set_uif_pairs.size(); + LOG(1) << "Try using simulation to find UIF pairs"; + _simulate(); + FindUifPairsUsingSim(); + params.simSetting.clear(); + if (origSize == _set_uif_pairs.size()) { + LOG(1) << "No new UIF pair is found using simulation"; + } else { + ++n_iter_uif; + print_stat(); + } + } + + while(true) { + while(true) { + if (params.fPbaCex && mem.pCex2) { + if(mem.pCex) Abc_CexFree(mem.pCex); + mem.pCex = mem.pCex2; + mem.pCex2 = NULL; + Wlc_Ntk_t * pCurrent = BuildCurrentAbstraction(); + Wlc_NtkFree(pCurrent); + ret = 0; + } else { + ret = VerifyCurrentAbstraction(&mem.pCex); + } + + if (ret == 0) { // SAT + // GetOperatorsInCex(mem.pCex); + if (verify_cex_on_original(_pOrigNtk, mem.pCex)) { + PrintWordCEX(_pOrigNtk, mem.pCex, &_vec_orig_names); + return 0; + } + unsigned n_before = _set_uif_pairs.size(); + + FindUifPairsUsingCex(mem.pCex, &mem.pCex2); + + if (n_before == _set_uif_pairs.size()) { + LOG(1) << "No new UIF pair is found in CEX"; + + if(!params.simSetting.empty()) { + LOG(1) << "Try using simulation to find UIF pairs"; + _simulate(); + FindUifPairsUsingSim(); + params.simSetting.clear(); + if (n_before == _set_uif_pairs.size()) { + LOG(1) << "No new UIF pair is found using simulation"; + } + } + + if (params.nGrey) { + DetermineGreyness(mem.pCex); + } + + if (n_before == _set_uif_pairs.size() && !params.nGrey) { + break; // entering white-boxing refinement + } + } + + ++n_iter_uif; + print_stat(); + + if(_set_uif_pairs.size() > params.nConstraintLimit) + return -1; + } else if (ret == 1) { // UNSAT + //_shrink_final_abstraction(); + //print_stat(); + return 1; + + } else { + return -1; + + } + } + + DetermineWhiteBoxes(mem.pCex); + + ++n_iter_wb; + print_stat(); + } + return -1; +} + +void UfarManager::_massage_state_b() { + for(const auto& x : _set_uif_pairs ) { + bool first_black = _vec_op_blackbox_marks[x.first.idx]; + bool second_black = _vec_op_blackbox_marks[x.second.idx]; + if (!first_black && !second_black) { + int to_black_idx = (params.iExp == 0 ? x.second.idx : x.first.idx); + _vec_op_blackbox_marks[to_black_idx] = true; + LOG(2) << "Blackbox (" << to_black_idx << ") for UF (" << x.first.idx << ", " << x.second.idx << ")"; + } + } +} + + +string UfarManager::_get_profile_uf_wb() { + if (log_level() <= 4) return ""; + unsigned num_full_white = 0; + unsigned num_full_black = 0; + unsigned num_grey = 0; + for(const auto& x : _set_uif_pairs ) { + bool first_black = _vec_op_blackbox_marks[x.first.idx]; + bool second_black = _vec_op_blackbox_marks[x.second.idx]; + if(first_black && second_black) { + ++num_full_black; + } else if (!first_black && !second_black) { + ++num_full_white; + LOG(3) << "ww : (" << x.first.idx << ", " << x.second.idx << ")"; + } else { + ++num_grey; + } + } + ostringstream oss; + oss << "; ww = " << num_full_white << "; bb = " << num_full_black << "; gr = " << num_grey <<";"; + return oss.str(); +} + +void UfarManager::GetOperatorsInCex(Abc_Cex_t *pCex, VecVecStr* pRes) { + VecVecChar cex_po_values; + + Gia_Man_t * pGia = BitBlast(_pAbsWithAuxPos); + CollectPoValuesInCex(pGia, pCex, cex_po_values, params.fCexMin); + Gia_ManStop(pGia); + + unsigned pos; + for(unsigned f = 0; f < cex_po_values.size(); f++) { + if (pRes) pRes->push_back(VecStr()); + vector& cur_po_vals = cex_po_values[f]; + pos = 1; + for(unsigned i = 1; i < Wlc_NtkPoNum(_pAbsWithAuxPos); i++) { + int range = Wlc_ObjRange(Wlc_NtkPo(_pAbsWithAuxPos, i)); + string bit_str = string(cur_po_vals.begin() + pos, cur_po_vals.begin() + pos + range); + if (!pRes) { + cout << "PO[" << i << "]@" << f << " = " << string(bit_str.rbegin(), bit_str.rend()) << endl; + } else { + pRes->back().push_back(bit_str); + } + pos += range; + } + } + +} + +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 << "iLogLevel" << " : " << params.iVerbosity << endl; +} + +void UfarManager::DumpMgrInfo() const { + cout << "Operators : " << endl; + for(unsigned i = 0; i < _vec_op_ids.size(); i++, printf("\n")) { + cout << "OP_ID = " << i << " : "; + cout << _vec_orig_names[_vec_op_ids[i]] << " = "; + cout << _vec_orig_names[Wlc_ObjFaninId0(Wlc_NtkObj(_pOrigNtk, _vec_op_ids[i]))] << " * "; + cout << _vec_orig_names[Wlc_ObjFaninId1(Wlc_NtkObj(_pOrigNtk, _vec_op_ids[i]))] ; + cout << (_vec_op_blackbox_marks[i] ? " (black)" : "") ; + } +} + + +void UfarManager::_dump_states(const std::string& file) { + fstream fs; + fs.open((file + "_s").c_str(), fstream::out); + + if(!fs.is_open()) { + cerr << "Cannot open the file for dumping states.\n"; + return; + } + + fs << "B\n"; + for (int i = 0; i < _vec_op_blackbox_marks.size(); ++i) { + fs << (_vec_op_blackbox_marks[i] == true ? "1" : "0"); + } + fs << "\nP\n"; + for (const auto& x : _set_uif_pairs) { + fs << x.first.idx << "," << x.first.timediff << ","; + fs << x.second.idx << "," << x.second.timediff << ","; + fs << (x.fMark == true ? "1" : "0") << "\n"; + } + + fs.close(); +} + +void UfarManager::_read_states(const std::string &file) { + fstream fs; + fs.open(file.c_str(), fstream::in); + + if(!fs.is_open()) { + cerr << "Cannot open the file for reading states.\n"; + return; + } + + string line; + getline(fs, line); + assert(line == "B"); + getline(fs, line); + set_state_b(_vec_op_blackbox_marks, line); + getline(fs, line); + assert(line == "P"); + while(getline(fs, line)) { + set_state_p(_set_uif_pairs, line); + } + + if(log_level() >= 3) print_blackboxes(_vec_op_blackbox_marks); + if(log_level() >= 3) print_pairs(_set_uif_pairs); + + fs.close(); +} + + Wlc_Ntk_t * UfarManager::_abstract_operators(Wlc_Ntk_t * pNtk, const vector& vec_ids) const { + Vec_Int_t * vec_ops = collect_boxes(vec_ids, _vec_op_blackbox_marks, true /*black*/); + assert(Vec_IntSize(vec_ops) > 0); + + Wlc_Ntk_t * pNew = NULL; + pNew = AbstractNodes(pNtk, vec_ops); + + Vec_IntFree(vec_ops); + + return pNew; +} + +} diff --git a/src/opt/ufar/UfarMgr.h b/src/opt/ufar/UfarMgr.h new file mode 100755 index 000000000..823e47a18 --- /dev/null +++ b/src/opt/ufar/UfarMgr.h @@ -0,0 +1,144 @@ +/* + * UifMgr.h + * + * Created on: Aug 25, 2015 + * Author: Yen-Sheng Ho + */ + +#ifndef SRC_EXT2_UIF_UIFMGR_H_ +#define SRC_EXT2_UIF_UIFMGR_H_ + +#include +#include +#include +#include +#include +#include +#include +#include + +typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; +typedef struct Abc_Cex_t_ Abc_Cex_t; +typedef struct Gia_Man_t_ Gia_Man_t; + +namespace UFAR { + +using VecVecInt = std::vector >; +using VecVecStr = std::vector >; +using VecChar = std::vector; +using VecStr = std::vector; +using IntPair = std::pair; + +struct OperatorID; +struct UifPair; +struct Greyness; +using UIF_PAIR = UifPair; + +class SimUifPairFinder; +class CexUifPairFinder; + +class UfarManager { + public: + struct Params { + Params(); + bool fCexMin; + bool fPbaUif; + bool fLazySim; + bool fPbaSim; + bool fPbaCex; + bool fSatMin; + bool fCbaWb; + bool fGrey; + float nGrey; + bool fNorm; + bool fSuper_prove; + bool fSimple; + bool fSyn; + bool fPthread; + int iOneWb; + int iExp; + unsigned nConstraintLimit; + unsigned iVerbosity; + unsigned nSeqLookBack; + unsigned nTimeout; + std::string simSetting; + std::string parSetting; + 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) {} + unsigned tBLSolver; + unsigned tUifRefine; + unsigned tWbRefine; + unsigned tUifSim; + unsigned tGbRefine; + }; + + UfarManager(); + ~UfarManager(); + + void Initialize(Wlc_Ntk_t * pNtk, const std::set& types); + + Wlc_Ntk_t * BuildCurrentAbstraction(); + Wlc_Ntk_t * ApplyUifConstraints(Wlc_Ntk_t * pNtk, std::vector& vec_ids); + void FindUifPairsUsingCex(Abc_Cex_t * pCex, Abc_Cex_t ** ppCex = NULL); + void FindUifPairsUsingSim(); + void DetermineWhiteBoxes(Abc_Cex_t * pCex); + void DetermineGreyness(Abc_Cex_t * pCex); + + int VerifyCurrentAbstraction(Abc_Cex_t ** ppCex); + int PerformUIFProve(const timeval& timer); + + void DumpMgrInfo() const; + void DumpParams() const; + void GetOperatorsInCex(Abc_Cex_t *pCex, VecVecStr* pRes); + + Params params; + Profile profile; + + private: + Wlc_Ntk_t * _abstract_operators(Wlc_Ntk_t * pNtk, const std::vector& vec_ids) const; + + Wlc_Ntk_t * _introduce_choices(std::vector& vec_choice2idx, bool fBlack); + Wlc_Ntk_t * _introduce_bitwise_choices(std::vector& vec_choice2idx); + Wlc_Ntk_t * _set_up_constraints(std::vector& vec_ids); + void _compute_core_choices(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, std::vector& vec_cores, int num_sel_pis); + void _simulate(); + void _perform_proof_based_white_boxing(Abc_Cex_t * pCex); + void _perform_proof_based_grey_boxing(Abc_Cex_t * pCex); + void _perform_cex_based_white_boxing(); + std::string _get_profile_uf_wb(); + void _massage_state_b(); + void _dump_states(const std::string& file); + void _read_states(const std::string& file); + + void _shrink_final_abstraction(); + + Wlc_Ntk_t * _pOrigNtk; + std::vector _vec_orig_names; + + std::vector _vec_op_ids; + std::vector _vec_op_blackbox_marks; + std::vector > _vec_vec_op_ffs; + std::vector _vec_op_greyness; + + std::set _set_uif_pairs; + std::set _set_uif_sim_pairs; + std::set _set_prev_ops; + + Wlc_Ntk_t * _pAbsWithAuxPos; + + std::unique_ptr _p_sim_mgr; + std::unique_ptr _p_cex_mgr; + + std::ostringstream _oss; + + struct timespec _timeout; +}; + +} + +#endif /* SRC_EXT2_UIF_UIFMGR_H_ */ diff --git a/src/opt/ufar/UfarPth.cpp b/src/opt/ufar/UfarPth.cpp new file mode 100755 index 000000000..45adea846 --- /dev/null +++ b/src/opt/ufar/UfarPth.cpp @@ -0,0 +1,289 @@ +#include "UfarPth.h" +#include "opt/util/util.h" +#include "opt/untk/NtkNtk.h" +#include "sat/bmc/bmc.h" +#include "proof/pdr/pdr.h" +#include "aig/gia/giaAig.h" + +#include +#include + +extern "C" { + Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pAig ); + int Abc_NtkDarBmc3( Abc_Ntk_t * pAbcNtk, Saig_ParBmc_t * pBmcPars, int fOrDecomp ); + Wla_Man_t * Wla_ManStart( Wlc_Ntk_t * pNtk, Wlc_Par_t * pPars ); + void Wla_ManStop( Wla_Man_t * pWla ); + int Wla_ManSolve( Wla_Man_t * pWla, Wlc_Par_t * pPars ); +} + +static volatile int g_nRunIds = 0; // the number of the last prover instance +int Ufar_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; } +int Ufar_GetGlobalRunId() { return g_nRunIds; } + +using namespace std; + +namespace UFAR { + +// mutext to control access to shared variables +pthread_mutex_t g_mutex; +// cv to control timer +pthread_cond_t g_cond; + +struct Pth_Data_t +{ + Pth_Data_t () : RunId(-1), pGia(NULL), pWlc(NULL), ppCex(NULL), RetValue(-1), engine(NULL) {} + void set ( const string * eng, int id, Wlc_Ntk_t * pWL, Gia_Man_t * pBL, Abc_Cex_t ** pp ) { engine = eng; RunId = id; pWlc = pWL; pGia = pBL; ppCex = pp; } + int RunId; + Gia_Man_t * pGia; + Wlc_Ntk_t * pWlc; + Abc_Cex_t ** ppCex; + int RetValue; + const string * engine; +}; + +class Solver { +public: + virtual ~Solver() {} + virtual int Solve() = 0; + virtual void SetCex( Abc_Cex_t ** ppCex ) = 0; +}; + +class PDR : public Solver { + public: + PDR( void * pArg ) { + Pth_Data_t * pData = (Pth_Data_t *)pArg; + + _pAig = Gia_ManToAigSimple( pData->pGia ); + + Pdr_Par_t * pPdrPars = &_PdrPars; + Pdr_ManSetDefaultParams(pPdrPars); + pPdrPars->nConfLimit = 0; + pPdrPars->RunId = pData->RunId; + pPdrPars->pFuncStop = Ufar_CallBackToStop; + } + ~PDR() { Aig_ManStop(_pAig); } + + virtual int Solve() { + return Pdr_ManSolve( _pAig, &_PdrPars ); + } + + virtual void SetCex( Abc_Cex_t ** ppCex ) { + assert( _pAig->pSeqModel ); + *(ppCex) = _pAig->pSeqModel; + _pAig->pSeqModel = NULL; + } + + private: + Aig_Man_t * _pAig; + Pdr_Par_t _PdrPars; +}; + +class PDRA : public Solver { + public: + PDRA( void * pArg ) { + Pth_Data_t * pData = (Pth_Data_t *)pArg; + + _pAig = Gia_ManToAigSimple( pData->pGia ); + + Pdr_Par_t * pPdrPars = &_PdrPars; + Pdr_ManSetDefaultParams(pPdrPars); + pPdrPars->nConfLimit = 0; + pPdrPars->RunId = pData->RunId; + pPdrPars->pFuncStop = Ufar_CallBackToStop; + pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction) + pPdrPars->fCtgs = 1; // use 'pdr -c' (improved generalization) + pPdrPars->fSkipDown = 0; // use 'pdr -n' (improved generalization) + pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this + } + ~PDRA() { Aig_ManStop(_pAig); } + + virtual int Solve() { + return Pdr_ManSolve( _pAig, &_PdrPars ); + } + + virtual void SetCex( Abc_Cex_t ** ppCex ) { + assert( _pAig->pSeqModel ); + *(ppCex) = _pAig->pSeqModel; + _pAig->pSeqModel = NULL; + } + + private: + Aig_Man_t * _pAig; + Pdr_Par_t _PdrPars; +}; + +class BMC3 : public Solver { + public: + BMC3 ( void * pArg ) { + Pth_Data_t * pData = (Pth_Data_t *)pArg; + Aig_Man_t * pAig = Gia_ManToAigSimple( pData->pGia ); + _pNtk = Abc_NtkFromAigPhase( pAig ); + Aig_ManStop( pAig ); + + Saig_ParBmc_t * pBmcPars = &_Pars; + Saig_ParBmcSetDefaultParams( pBmcPars ); + pBmcPars->RunId = pData->RunId; + pBmcPars->pFuncStop = Ufar_CallBackToStop; + } + ~BMC3() { Abc_NtkDelete(_pNtk); } + + virtual int Solve() { + return Abc_NtkDarBmc3( _pNtk, &_Pars, 0 ); + } + + virtual void SetCex( Abc_Cex_t ** ppCex ) { + assert( _pNtk->pSeqModel ); + *(ppCex) = _pNtk->pSeqModel; + _pNtk->pSeqModel = NULL; + } + private: + Abc_Ntk_t * _pNtk; + Saig_ParBmc_t _Pars; +}; + +class PDRWLA : public Solver { + public: + PDRWLA( void * pArg ) { + Pth_Data_t * pData = (Pth_Data_t *)pArg; + Wlc_Ntk_t * pNtk = pData->pWlc; + + Wlc_Par_t * pWlcPars = &_Pars; + Wlc_ManSetDefaultParams( pWlcPars ); + pWlcPars->nBitsAdd = 8; + pWlcPars->nBitsMul = 4; + pWlcPars->nBitsMux = 8; + pWlcPars->fXorOutput = 0; + pWlcPars->nLimit = 50; + pWlcPars->fVerbose = 1; + pWlcPars->fProofRefine = 1; + pWlcPars->fHybrid = 0; + pWlcPars->fCheckCombUnsat = 1; + pWlcPars->RunId = pData->RunId; + pWlcPars->pFuncStop = Ufar_CallBackToStop; + + _pWla = Wla_ManStart( pNtk, pWlcPars ); + } + ~PDRWLA() { Wla_ManStop(_pWla); } + + virtual int Solve() { + return Wla_ManSolve( _pWla, &_Pars ); + } + + virtual void SetCex( Abc_Cex_t ** ppCex ) { + assert( _pWla->pCex ); + *(ppCex) = _pWla->pCex; + _pWla->pCex = NULL; + } + private: + Wla_Man_t * _pWla; + Wlc_Par_t _Pars; +}; + +void KillOthers() { + pthread_cond_signal( &g_cond ); + ++g_nRunIds; +} + +void * RunSolver( void * pArg ) { + Pth_Data_t * pData = (Pth_Data_t *)pArg; + Solver * pSolver = NULL; + int status; + + if ( *(pData->engine) == "pdr" ) + pSolver = new PDR( pArg ); + else if ( *(pData->engine) == "pdra" ) + pSolver = new PDRA( pArg ); + else if ( *(pData->engine) == "bmc3" ) + pSolver = new BMC3( pArg ); + else if ( *(pData->engine) == "wla" ) + pSolver = new PDRWLA( pArg ); + else { + pthread_exit( NULL ); + assert(0); + return 0; + } + + pData->RetValue = pSolver->Solve(); + int ret = pData->RetValue; + + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + if ( ret == 0 ) { + pSolver->SetCex( pData->ppCex ); + LOG(2) << *(pData->engine) << " found CEX. RunId = " << pData->RunId; + + KillOthers(); + } else if ( ret == 1 ) { + LOG(2) << *(pData->engine) << " proved the problem. RunId = " << pData->RunId; + KillOthers(); + } else { + if ( pData->RunId < g_nRunIds ) { + LOG(2) << *(pData->engine) << " was cancelled. RunId = " << pData->RunId; + } + } + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + + delete pSolver; + + pthread_exit( NULL ); + assert(0); + return 0; +} + +void * Timer ( void * pArg ) { + struct timespec * pTimeout = ( struct timespec * )pArg; + int retcode = 0; + int status; + + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + retcode = pthread_cond_timedwait(&g_cond, &g_mutex, pTimeout); + if ( retcode == ETIMEDOUT ) { + LOG(2) << "Timer reached timeout."; + KillOthers(); + } else { + LOG(2) << "Timer was cancelled."; + } + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + + pthread_exit( NULL ); + assert(0); + return 0; +} + +int RunConcurrentSolver( Wlc_Ntk_t * pNtk, const vector& vSolvers, Abc_Cex_t ** ppCex, struct timespec * pTimeout ) { + assert( pTimeout ); + + int status; + vector vDatas ( vSolvers.size() ); + vector vThreads ( vSolvers.size() ); + pthread_t timer; + + Gia_Man_t * pGia = BitBlast( pNtk ); + + status = pthread_create( &timer, NULL, Timer, pTimeout ); + assert( status == 0 ); + + for ( size_t i = 0; i < vSolvers.size(); ++i ) { + vDatas[i].set( &vSolvers[i], g_nRunIds, pNtk, pGia, ppCex ); + status = pthread_create( &vThreads[i], NULL, RunSolver, &vDatas[i] ); + assert( status == 0 ); + } + + status = pthread_join( timer, NULL ); + assert( status == 0 ); + for ( size_t i = 0; i < vSolvers.size(); ++i ) { + status = pthread_join( vThreads[i], NULL ); + assert( status == 0 ); + } + + Gia_ManStop( pGia ); + + for( auto& x : vDatas ) { + if ( x.RetValue != -1 ) + return x.RetValue; + } + return -1; +} + + + +} diff --git a/src/opt/ufar/UfarPth.h b/src/opt/ufar/UfarPth.h new file mode 100755 index 000000000..d05da25fc --- /dev/null +++ b/src/opt/ufar/UfarPth.h @@ -0,0 +1,17 @@ +// +// Created by Yen-Sheng Ho on 04/09/17. +// + +#ifndef SRC_EXT2_UFAR_PTH_H +#define SRC_EXT2_UFAR_PTH_H + +#include "base/wlc/wlc.h" +#include +#include + +namespace UFAR +{ + int RunConcurrentSolver( Wlc_Ntk_t * pNtk, const std::vector& vSolvers, Abc_Cex_t ** ppCex, struct timespec * timeout ); +} + +#endif //SRC_EXT2_UFAR_PTH_H diff --git a/src/opt/ufar/module.make b/src/opt/ufar/module.make new file mode 100755 index 000000000..30c6c1d46 --- /dev/null +++ b/src/opt/ufar/module.make @@ -0,0 +1,3 @@ +SRC += src/opt/ufar/UfarCmd.cpp \ + src/opt/ufar/UfarPth.cpp \ + src/opt/ufar/UfarMgr.cpp diff --git a/src/opt/untk/Netlist.cpp b/src/opt/untk/Netlist.cpp new file mode 100755 index 000000000..c6643e443 --- /dev/null +++ b/src/opt/untk/Netlist.cpp @@ -0,0 +1,63 @@ +// +// Created by Yen-Sheng Ho on 8/9/16. +// + +#include "Netlist.h" + +#include + +#include + +using namespace std; + +namespace UFAR { + +WNetlist::WNetlist() { + _pNtk = Wlc_NtkAlloc("main", 100); +} + +WNetlist::WNetlist(Wlc_Ntk_t *pNtk) { + if (pNtk) + _pNtk = Wlc_NtkDupDfsSimple(pNtk); + else + _pNtk = NULL; +} + +WNetlist::WNetlist(const WNetlist& that) { + _pNtk = Wlc_NtkDupDfsSimple(that._pNtk); +} + +WNetlist::WNetlist(WNetlist && that) { + _pNtk = that._pNtk; + that._pNtk = NULL; +} + +WNetlist& WNetlist::operator=(const WNetlist& that) { + Wlc_Ntk_t * pTemp = _pNtk; + _pNtk = Wlc_NtkDupDfsSimple(that._pNtk); + if (pTemp) Wlc_NtkFree(pTemp); + return *this; +} + +WNetlist::~WNetlist() { + if (_pNtk) Wlc_NtkFree(_pNtk); +} + +void WNetlist::Clear() { + if (_pNtk) Wlc_NtkFree(_pNtk); + _pNtk = Wlc_NtkAlloc("main", 100); +} + +bool WNetlist::Empty() const { + if (_pNtk == NULL) return true; + + return Wlc_NtkObjNum(_pNtk) == 0; +} + +void WNetlist::Reset(Wlc_Ntk_t *pNtk) { + Wlc_Ntk_t * pTemp = _pNtk; + _pNtk = Wlc_NtkDupDfsSimple(pNtk); + if (pTemp) Wlc_NtkFree(pTemp); +} + +} diff --git a/src/opt/untk/Netlist.h b/src/opt/untk/Netlist.h new file mode 100755 index 000000000..07b6032c5 --- /dev/null +++ b/src/opt/untk/Netlist.h @@ -0,0 +1,33 @@ +// +// Created by ysho on 8/9/16. +// + +#ifndef ABC_WAR_NETLIST_H +#define ABC_WAR_NETLIST_H + +#include + +typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; + +namespace UFAR { + +class WNetlist { +public: + WNetlist(); + WNetlist(Wlc_Ntk_t * pNtk); + WNetlist(const WNetlist& that); + ~WNetlist(); + WNetlist(WNetlist && that); + WNetlist& operator=(const WNetlist& that); + Wlc_Ntk_t * GetNtk() const {return _pNtk;} + void Clear(); + bool Empty() const; + void Reset(Wlc_Ntk_t * pNtk); +private: + Wlc_Ntk_t * _pNtk; +}; + + +} + +#endif //ABC_WAR_NETLIST_H diff --git a/src/opt/untk/NtkCmd.cpp b/src/opt/untk/NtkCmd.cpp new file mode 100755 index 000000000..19f73f87f --- /dev/null +++ b/src/opt/untk/NtkCmd.cpp @@ -0,0 +1,12 @@ +/* + * NtkCmd.cpp + * + * Created on: Aug 25, 2015 + * Author: Yen-Sheng Ho + */ + +#include "opt/untk/NtkCmd.h" + +void Ntk_Init (Abc_Frame_t *pAbc) +{ +} diff --git a/src/opt/untk/NtkCmd.h b/src/opt/untk/NtkCmd.h new file mode 100755 index 000000000..77790a083 --- /dev/null +++ b/src/opt/untk/NtkCmd.h @@ -0,0 +1,15 @@ +/* + * NtkCmd.h + * + * Created on: Aug 25, 2015 + * Author: Yen-Sheng Ho + */ + +#ifndef SRC_EXT2_NTK_NTKCMD_H_ +#define SRC_EXT2_NTK_NTKCMD_H_ + +#include "base/main/mainInt.h" + +void Ntk_Init(Abc_Frame_t *pAbc); + +#endif /* SRC_EXT2_NTK_NTKCMD_H_ */ diff --git a/src/opt/untk/NtkNtk.cpp b/src/opt/untk/NtkNtk.cpp new file mode 100755 index 000000000..2c94bcd16 --- /dev/null +++ b/src/opt/untk/NtkNtk.cpp @@ -0,0 +1,1487 @@ +/* + * NtkNtk.cpp + * + * Created on: Aug 25, 2015 + * Author: Yen-Sheng Ho + */ + +#include "NtkNtk.h" +#include "Netlist.h" +#include "opt/util/util.h" +#include "opt/ufar/UfarPth.h" + +#include +#include +#include +#include +#include + +#include +#include +#include + +extern "C" { + Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); + int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ); + int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp ); + int Wlc_ObjDup( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * vFanins ); + void Wlc_NtkDupDfs_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * vFanins ); + void Wlc_ObjSetCo( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int fFlopInput ); + Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + Gia_Man_t * Gia_ManDupInvMiter( Gia_Man_t * p, Gia_Man_t * pInv ); + Wla_Man_t * Wla_ManStart( Wlc_Ntk_t * pNtk, Wlc_Par_t * pPars ); + void Wla_ManStop( Wla_Man_t * pWla ); + int Wla_ManSolve( Wla_Man_t * pWla, Wlc_Par_t * pPars ); + Gia_Man_t * Wlc_NtkBitBlast2( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds ); + void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars ); +} + +using namespace std; + +namespace UFAR { + +static inline int create_buffer(Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins, int max_bw) { + return Wlc_ObjCreate(p, WLC_OBJ_BUF, Wlc_ObjIsSigned(pObj), (max_bw == -1 ? Wlc_ObjRange(pObj) - 1 : max_bw - 1), 0, vFanins); +} + +Gia_Man_t * BitBlast(Wlc_Ntk_t * pNtk) { + Wlc_BstPar_t Par, * pPar = &Par; + Wlc_BstParDefault( pPar ); + return Wlc_NtkBitBlast(pNtk, pPar); + //Gia_Man_t * pGia = Wlc_NtkBitBlast2(pNtk, NULL); + //printf( "Usingn old bit-blaster: " ); + //Gia_ManPrintStats( pGia, NULL ); + //return pGia; +} + +template +void ModifyMarkedNodes(Wlc_Ntk_t * pNtk, int nOrigObjNum, Functor get_modified_node) { + Wlc_Obj_t * pObj; + int i, k, iFanin, iObj; + // iterate through the nodes in the DFS order + Wlc_NtkForEachObj( pNtk, pObj, i ) { + if (i == nOrigObjNum) { + // cout << "break at " << i << endl; + break; + } + if (pObj->Mark) { + pObj->Mark = 0; + iObj = get_modified_node(pObj); + } else { + // update fanins + Wlc_ObjForEachFanin( pObj, iFanin, k ) + Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(pNtk, iFanin); + // node to remain + iObj = i; + } + Wlc_ObjSetCopy( pNtk, i, iObj ); + } + + Wlc_NtkForEachCo( pNtk, pObj, i ) + { + iObj = Wlc_ObjId(pNtk, pObj); + if (iObj != Wlc_ObjCopy(pNtk, iObj)) { + assert(pObj->fIsFi); + Wlc_NtkObj(pNtk, Wlc_ObjCopy(pNtk, iObj))->fIsFi = 1; + Vec_IntWriteEntry(&pNtk->vCos, i, Wlc_ObjCopy(pNtk, iObj)); + } + } +} + + +Greyness::Greyness(Wlc_Ntk_t * pNtk, Wlc_Obj_t * pOpObj) { + auto compute_cone_size = [&](Wlc_Ntk_t * pOrig, const vector& ids, Vec_Int_t * vFanins) { + int i; + Wlc_Obj_t * pObj; + WNetlist N; + Wlc_Ntk_t * pNew = N.GetNtk(); + Wlc_NtkForEachCi( pOrig, pObj, i ) { + int iNewPi = Wlc_ObjAlloc(pNew, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0); + Wlc_ObjSetCopy(pOrig, Wlc_ObjId(pOrig, pObj), iNewPi); + } + + for(auto x : ids) + Wlc_NtkDupDfs_rec( pNew, pOrig, x, vFanins ); + for(auto x : ids) + Wlc_ObjSetCo( pNew, Wlc_NtkObj(pNew, Wlc_ObjCopy(pOrig, x)), 0 ); + + Gia_Man_t * pGia = BitBlast(pNew); + int cone_size = Gia_ManAndNum(pGia); + Gia_ManStop(pGia); + + return cone_size; + }; + + _current_cost = 0; + + _vec_black_bits.resize(Wlc_ObjRange(pOpObj), true); + + int iOpId = Wlc_ObjId(pNtk, pOpObj); + + _N_white = pNtk; + Wlc_Ntk_t * pOrig = _N_white.GetNtk(); + + iOpId = Wlc_ObjCopy(pNtk, iOpId); + pOpObj = Wlc_NtkObj(pOrig, iOpId); + _iOpId = iOpId; + int iFin0 = Wlc_ObjFaninId0(pOpObj); + int iFin1 = Wlc_ObjFaninId1(pOpObj); + + Vec_Int_t * vFanins = Vec_IntAlloc(100); + + Wlc_NtkCleanCopy( pOrig ); + int out_size = compute_cone_size(pOrig, vector{iOpId}, vFanins); + Wlc_NtkCleanCopy( pOrig ); + int in_size = compute_cone_size(pOrig, vector{iFin0, iFin1}, vFanins); + + assert(out_size >= in_size); + _total_cost = unsigned(out_size - in_size); + + Gia_Man_t * pGia = BitBlast(pOrig); + _orig_size = unsigned(Gia_ManAndNum(pGia)); + Gia_ManStop(pGia); + + Vec_IntFree(vFanins); +} + +void Greyness::UpdateCost() { + Wlc_Ntk_t * pOrig = _N_white.GetNtk(); + Wlc_Obj_t * pOpObj = Wlc_NtkObj(pOrig, _iOpId); + int iOpObj = _iOpId; + int offset = pOpObj->Beg; + int range = Wlc_ObjRange(pOpObj); + int is_signed = Wlc_ObjIsSigned(pOpObj); + + Wlc_NtkCleanCopy( pOrig ); + WNetlist N_Grey( pOrig ); + Wlc_Ntk_t * pGrey = N_Grey.GetNtk(); + Wlc_NtkCleanCopy( pGrey ); + int nOrigObjNum = Wlc_NtkObjNumMax( pGrey ); + iOpObj = Wlc_ObjCopy(pOrig, iOpObj); + Wlc_NtkObj(pGrey, iOpObj)->Mark = 1; + int iPPI = Wlc_ObjAlloc(pGrey, WLC_OBJ_PI, is_signed, range - 1, 0); + + auto create_grey_output = [&](Wlc_Obj_t * pObj){ + Vec_Int_t * vFanins = Vec_IntAlloc(3); + Vec_Int_t * vFanins2 = Vec_IntAlloc(3); + + for (size_t i = 0; i < _vec_black_bits.size(); ++i) { + Vec_IntClear(vFanins2); + if (_vec_black_bits[i]) + Vec_IntPush(vFanins2, iPPI); + else + Vec_IntPush(vFanins2, iOpObj); + Vec_IntPushTwo(vFanins2, i + offset, i + offset); + Vec_IntPush(vFanins, Wlc_ObjCreate(pGrey, WLC_OBJ_BIT_SELECT, 0, 0, 0, vFanins2)); + } + Vec_IntReverseOrder(vFanins); + int iObj = Wlc_ObjCreate(pGrey, WLC_OBJ_BIT_CONCAT, is_signed, range - 1, 0, vFanins); + + Vec_IntFree(vFanins); + Vec_IntFree(vFanins2); + + return iObj; + }; + + ModifyMarkedNodes(pGrey, nOrigObjNum, create_grey_output); + + WNetlist N_result(pGrey); + + Gia_Man_t * pGia = BitBlast(N_result.GetNtk()); + unsigned grey_size = unsigned(Gia_ManAndNum(pGia)); + Gia_ManStop(pGia); + + assert(_orig_size >= grey_size); + _current_cost = _total_cost - (_orig_size - grey_size); +} + +unsigned compute_bit_level_pi_num(Wlc_Ntk_t * pNtk) { + unsigned num = 0; + int i; + Wlc_Obj_t * pObj; + Wlc_NtkForEachPi(pNtk, pObj, i) { + num += Wlc_ObjRange(pObj); + } + return num; +} + +void DumpWlcNtk(Wlc_Ntk_t * pNtk) { + int i, k, iFanin; + Wlc_Obj_t * pObj; + Wlc_NtkForEachObj(pNtk, pObj, i) { + cout << i << " <-- "; + Wlc_ObjForEachFanin( pObj, iFanin, k ) { + cout << iFanin << " "; + } + cout << endl; + } +} + +Wlc_Ntk_t * DupNtkAndUpdateIDs(Wlc_Ntk_t * pNtk, std::vector& vec_ids) { + Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple(pNtk); + for(unsigned i = 0; i < vec_ids.size(); i++) { + vec_ids[i] = Wlc_ObjCopy(pNtk, vec_ids[i]); + } + return p; +} + +int AddOneFanoutFF(Wlc_Ntk_t * pNtk, int obj_id, unsigned& count_bits) { + Vec_Int_t * vFanins = Vec_IntAlloc( 1 ); + + int range = Wlc_ObjRange(Wlc_NtkObj(pNtk, obj_id)); + + // create flop + int fo = Wlc_ObjCreate( pNtk, WLC_OBJ_FO, Wlc_ObjIsSigned(Wlc_NtkObj(pNtk, obj_id)), range-1, 0, vFanins ); + + // set up FI + Wlc_NtkObj(pNtk, obj_id)->fIsFi = 1; + + // push FI + Vec_IntPush(&pNtk->vCos, obj_id); + + // push vInits + if ( pNtk->vInits == NULL ) { + pNtk->vInits = Vec_IntAlloc( 100 ); + } + Vec_IntPush( pNtk->vInits, -range ); + + count_bits += range; + + Vec_IntFree( vFanins ); + + assert(Wlc_NtkCi(pNtk, Wlc_NtkCiNum(pNtk)-1) == Wlc_NtkObj(pNtk, fo)); + return Wlc_NtkCiNum(pNtk) - 1; +} + +Wlc_Ntk_t * IntroducePrevOperators(Wlc_Ntk_t * pNtk, vector& vec_ids, const set& set_prev_ops, VecVecInt& vv_op_ffs) { + array wires; + unsigned count_bits = 0; + + vv_op_ffs = vector >(vec_ids.size(), vector()); + Wlc_Ntk_t * p = DupNtkAndUpdateIDs(pNtk, vec_ids); + + for(auto it = set_prev_ops.begin(); it != set_prev_ops.end(); it++) { + int idx = it->idx; + int prev_idx = 0 - it->timediff - 1; + assert(idx < vv_op_ffs.size()); + assert(prev_idx >= 0); + + for(int i = 0; i <= prev_idx; i++) { + if(i < vv_op_ffs[idx].size()) continue; + assert(i == vv_op_ffs[idx].size()); + + if(i == 0) { + wires[2] = vec_ids[idx]; + wires[0] = Wlc_ObjFaninId0(Wlc_NtkObj(p, vec_ids[idx])); + wires[1] = Wlc_ObjFaninId1(Wlc_NtkObj(p, vec_ids[idx])); + } else { + wires[2] = Wlc_ObjId(p, Wlc_NtkCi(p, vv_op_ffs[idx][i-1])); + wires[1] = Wlc_ObjId(p, Wlc_NtkCi(p, vv_op_ffs[idx][i-1]) - 1); + wires[0] = Wlc_ObjId(p, Wlc_NtkCi(p, vv_op_ffs[idx][i-1]) - 2); + } + + AddOneFanoutFF(p, wires[0], count_bits); + AddOneFanoutFF(p, wires[1], count_bits); + vv_op_ffs[idx].push_back(AddOneFanoutFF(p, wires[2], count_bits)); + } + } + + if (p->pInits) { + char * pStr = strcpy( + ABC_ALLOC(char, strlen(p->pInits) + count_bits + 1), + p->pInits); + for (unsigned i = 0; i < count_bits; ++i) { + pStr[strlen(p->pInits) + i] = '0'; + } + pStr[strlen(p->pInits) + count_bits] = '\0'; + ABC_FREE(p->pInits); + p->pInits = pStr; + } + + Wlc_Ntk_t * pNew = DupNtkAndUpdateIDs(p, vec_ids); + Wlc_NtkFree(p); + return pNew; +} + +int AddZeroImplication(Wlc_Ntk_t * pNtk, const array& wires) +{ + int iFaninNew; + int iObjNew, iObjNew2; + int iObjConst0; + + Vec_Int_t * vFanins = Vec_IntAlloc( 2 ); + Vec_Int_t * vCompares = Vec_IntAlloc( 2 ); + + Vec_IntFill(vFanins, 1, 0); + iObjConst0 = Wlc_ObjCreate(pNtk, WLC_OBJ_CONST, 0, 0, 0, vFanins); + + Vec_IntFillTwo( vFanins, 2, wires[0], iObjConst0); + iFaninNew = Wlc_ObjCreate( pNtk, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins ); + Vec_IntPush( vCompares, iFaninNew ); + + Vec_IntFillTwo( vFanins, 2, wires[1], iObjConst0); + iFaninNew = Wlc_ObjCreate( pNtk, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins ); + Vec_IntPush( vCompares, iFaninNew ); + + // concatenate fanin comparators + iObjNew = Wlc_ObjCreate( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares ); + // create reduction-AND node + Vec_IntFill( vFanins, 1, iObjNew ); + iObjNew = Wlc_ObjCreate( pNtk, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins ); + + // create output comparator node + Vec_IntFillTwo( vFanins, 2, wires[2], iObjConst0 ); + iObjNew2 = Wlc_ObjCreate( pNtk, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins ); + // create implication node (iObjNew is already complemented above) + Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 ); + iObjNew = Wlc_ObjCreate( pNtk, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins ); + + Vec_IntFree( vCompares ); + Vec_IntFree( vFanins ); + + return iObjNew; +} + +int AddOneUifImplication(Wlc_Ntk_t * pNtk, const array& wires1, const array& wires2) +{ + int iFaninNew; + int iObjNew, iObjNew2; + + Vec_Int_t * vFanins = Vec_IntAlloc( 2 ); + Vec_Int_t * vCompares = Vec_IntAlloc( 2 ); + + Vec_IntFillTwo( vFanins, 2, wires1[0], wires2[0]); + iFaninNew = Wlc_ObjCreate( pNtk, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins ); + Vec_IntPush( vCompares, iFaninNew ); + + Vec_IntFillTwo( vFanins, 2, wires1[1], wires2[1]); + iFaninNew = Wlc_ObjCreate( pNtk, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins ); + Vec_IntPush( vCompares, iFaninNew ); + + // concatenate fanin comparators + iObjNew = Wlc_ObjCreate( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares ); + // create reduction-OR node + Vec_IntFill( vFanins, 1, iObjNew ); + iObjNew = Wlc_ObjCreate( pNtk, WLC_OBJ_REDUCT_OR, 0, 0, 0, vFanins ); + // create output comparator node + Vec_IntFillTwo( vFanins, 2, wires1[2], wires2[2] ); + iObjNew2 = Wlc_ObjCreate( pNtk, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins ); + // create implication node (iObjNew is already complemented above) + Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 ); + iObjNew = Wlc_ObjCreate( pNtk, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins ); + + Vec_IntFree( vCompares ); + Vec_IntFree( vFanins ); + + return iObjNew; +} + +int AddOneGrey(Wlc_Ntk_t * pNtk, const array& wires, const Greyness& greyness) { + Vec_Int_t * vFanins = Vec_IntAlloc( 3 ); + Vec_Int_t * vEquals = Vec_IntAlloc( 32 ); + + Vec_IntFillTwo(vFanins, 2, wires[0], wires[1]); + Wlc_Obj_t * pOrigOut = Wlc_NtkObj(pNtk, wires[2]); + int iShadowOut = Wlc_ObjCreate(pNtk, pOrigOut->Type, Wlc_ObjIsSigned(pOrigOut), pOrigOut->End, pOrigOut->Beg, vFanins); + int offset = pOrigOut->Beg; + + for (size_t pos = 0; pos < greyness.Size(); ++pos) { + // black bit : do nothing + if (greyness.Get(pos)) continue; + + // white bit + Vec_IntClear(vFanins); + Vec_IntPush(vFanins, wires[2]); + Vec_IntPushTwo(vFanins, pos + offset, pos + offset); + int iOrigBit = Wlc_ObjCreate(pNtk, WLC_OBJ_BIT_SELECT, 0, 0, 0, vFanins); + Vec_IntClear(vFanins); + Vec_IntPush(vFanins, iShadowOut); + Vec_IntPushTwo(vFanins, pos + offset, pos + offset); + int iShadowBit = Wlc_ObjCreate(pNtk, WLC_OBJ_BIT_SELECT, 0, 0, 0, vFanins); + + Vec_IntFillTwo(vFanins, 2, iOrigBit, iShadowBit); + Vec_IntPush(vEquals, Wlc_ObjCreate(pNtk, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins)); + } + + int iConcat = Wlc_ObjCreate(pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vEquals)-1, 0, vEquals); + Vec_IntFill(vFanins, 1, iConcat); + int iRes = Wlc_ObjCreate(pNtk, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins); + + Vec_IntFree( vFanins ); + Vec_IntFree( vEquals ); + + return iRes; +} + +Wlc_Ntk_t * ApplyGreynessConstraints(Wlc_Ntk_t * pNtk, const vector& vec_grey, vector& vec_ids) { + array wires; + + Wlc_Ntk_t * p = DupNtkAndUpdateIDs(pNtk, vec_ids); + Vec_Int_t * vGreyConstrs = Vec_IntAlloc( vec_ids.size() ); + + for (size_t i = 0; i < vec_ids.size(); ++i) { + if(!vec_grey[i].IsGrey()) continue; + + int iOut = vec_ids[i]; + wires[2] = iOut; + wires[0] = Wlc_ObjFaninId0(Wlc_NtkObj(p, iOut)); + wires[1] = Wlc_ObjFaninId1(Wlc_NtkObj(p, iOut)); + Vec_IntPush(vGreyConstrs, AddOneGrey(p, wires, vec_grey[i])); + } + + if (Wlc_NtkFfNum(p) == 0) + FoldCombConstraints(p, vGreyConstrs); + else + FoldSeqConstraints(p, vGreyConstrs); + + Wlc_Ntk_t * pNew = DupNtkAndUpdateIDs(p, vec_ids); + + Wlc_NtkFree(p); + Vec_IntFree(vGreyConstrs); + + return pNew; +} + +Wlc_Ntk_t * ApplyGreyConstraints(Wlc_Ntk_t * pNtk, std::vector& vec_ids, bool fSeq) { + array wires; + + Wlc_Ntk_t * p = DupNtkAndUpdateIDs(pNtk, vec_ids); + Vec_Int_t * vGreyConstrs = Vec_IntAlloc( vec_ids.size() ); + + for(auto& x : vec_ids) { + wires[2] = x; + wires[0] = Wlc_ObjFaninId0(Wlc_NtkObj(p, x)); + wires[1] = Wlc_ObjFaninId1(Wlc_NtkObj(p, x)); + int iObj = AddZeroImplication(p, wires); + Vec_IntPush(vGreyConstrs, iObj); + } + + if (!fSeq) + FoldCombConstraints(p, vGreyConstrs); + else + FoldSeqConstraints(p, vGreyConstrs); + + Wlc_Ntk_t * pNew = DupNtkAndUpdateIDs(p, vec_ids); + + Wlc_NtkFree(p); + Vec_IntFree(vGreyConstrs); + + return pNew; +} + +void FoldSeqConstraints(Wlc_Ntk_t *pNtk, Vec_Int_t *vConstrs) +{ + if (Vec_IntSize(vConstrs) == 0) return; + + int iObjNew; + Vec_Int_t * vFanins = Vec_IntAlloc( 100 ); + + // derive the AND of the UIF constraints + assert(Vec_IntSize(vConstrs) > 0); + if (Vec_IntSize(vConstrs) == 1) + iObjNew = Vec_IntEntry(vConstrs, 0); + else { + // concatenate + iObjNew = Wlc_ObjCreate(pNtk, WLC_OBJ_BIT_CONCAT, 0, + Vec_IntSize(vConstrs) - 1, 0, vConstrs); + // create reduction-AND node + Vec_IntFill(vFanins, 1, iObjNew); + iObjNew = Wlc_ObjCreate(pNtk, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins); + } + + // create flop + int iObjFO = 0; + int iObjFI = 0; + int iObjNegAllConstraints = 0; + Vec_IntClear(vFanins); + iObjFO = Wlc_ObjCreate(pNtk, WLC_OBJ_FO, 0, 0, 0, vFanins); + Vec_IntFill(vFanins, 1, iObjNew); + iObjNegAllConstraints = Wlc_ObjCreate(pNtk, WLC_OBJ_LOGIC_NOT, 0, 0, 0, vFanins); + Vec_IntFillTwo(vFanins, 2, iObjNegAllConstraints, iObjFO); + iObjFI = Wlc_ObjCreate(pNtk, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins); + Wlc_NtkObj(pNtk, iObjFI)->fIsFi = 1; + + if (pNtk->pInits) { + char * pStr = strcpy(ABC_ALLOC(char, strlen(pNtk->pInits) + 2), pNtk->pInits); + pStr[strlen(pNtk->pInits)] = '0'; + pStr[strlen(pNtk->pInits) + 1] = '\0'; + ABC_FREE(pNtk->pInits); + pNtk->pInits = pStr; + // push vInits + Vec_IntPush( pNtk->vInits, -1 ); + } + + //Vec_IntPush(&p->vCis, iObjFO); + Vec_IntPush(&pNtk->vCos, iObjFI); + + // update PO + Vec_IntFill(vFanins, 1, iObjFI); + int iObjNegFI = Wlc_ObjCreate(pNtk, WLC_OBJ_LOGIC_NOT, 0, 0, 0, vFanins); + int iObjPO = Wlc_ObjId(pNtk, Wlc_NtkPo(pNtk, 0)); + Vec_IntFillTwo(vFanins, 2, iObjNegFI, iObjPO); + int iObjNewPO = Wlc_ObjCreate(pNtk, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins); + + Vec_IntWriteEntry(&pNtk->vPos, 0, iObjNewPO); + Vec_IntWriteEntry(&pNtk->vCos, 0, iObjNewPO); + + Wlc_NtkObj(pNtk, iObjNewPO)->fIsPo = 1; + Wlc_NtkObj(pNtk, iObjPO)->fIsPo = 0; + + Vec_IntFree( vFanins ); +} + +void FoldCombConstraints(Wlc_Ntk_t *pNtk, Vec_Int_t *vConstrs) +{ + if (Vec_IntSize(vConstrs) == 0) return; + + int iObjNew; + Vec_Int_t * vFanins = Vec_IntAlloc( 100 ); + + // derive the AND of the UIF constraints + assert(Vec_IntSize(vConstrs) > 0); + if (Vec_IntSize(vConstrs) == 1) + iObjNew = Vec_IntEntry(vConstrs, 0); + else { + // concatenate + iObjNew = Wlc_ObjCreate(pNtk, WLC_OBJ_BIT_CONCAT, 0, + Vec_IntSize(vConstrs) - 1, 0, vConstrs); + // create reduction-AND node + Vec_IntFill(vFanins, 1, iObjNew); + iObjNew = Wlc_ObjCreate(pNtk, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins); + } + + // update PO + int iObjPO = Wlc_ObjId(pNtk, Wlc_NtkPo(pNtk, 0)); + Vec_IntFillTwo(vFanins, 2, iObjNew, iObjPO); + int iObjNewPO = Wlc_ObjCreate(pNtk, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins); + + Vec_IntWriteEntry(&pNtk->vPos, 0, iObjNewPO); + Vec_IntWriteEntry(&pNtk->vCos, 0, iObjNewPO); + + Wlc_NtkObj(pNtk, iObjNewPO)->fIsPo = 1; + Wlc_NtkObj(pNtk, iObjPO)->fIsPo = 0; + + Vec_IntFree( vFanins ); +} + +static bool isPIAndDontCare(Gia_Man_t * pGia, Gia_Obj_t * pObj, Abc_Cex_t * pCare, int f) { + if(!Gia_ObjIsPi(pGia, pObj)) return false; + if(!pCare) return false; + + if(!Abc_InfoHasBit(pCare->pData, pCare->nRegs + pCare->nPis * f + pObj->Value)) + return true; + + return false; +} + +void CollectPoValuesInCex(Gia_Man_t * pGia, Abc_Cex_t * pCex, VecVecChar& po_values, bool fCexMin) +{ + assert(po_values.empty()); + + int k, iBit; + Gia_Obj_t * pObj, * pObjRi, *pObjRo; + + Abc_Cex_t * pCare = NULL; + if (fCexMin) { + pCare = Bmc_CexCareMinimizeAig(pGia, Gia_ManPiNum(pGia), pCex, 1, 0, 0); + assert(pCare != NULL); + + Gia_ManCleanValue(pGia); + Gia_ManForEachPi( pGia, pObj, k ) + pObj->Value = k; + } + + Gia_ManCleanMark0(pGia); + + iBit = pCex->nRegs; + + for ( int f = 0; f <= pCex->iFrame; f++ ) { + po_values.push_back(vector()); + Gia_ManForEachPi( pGia, pObj, k ) + pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); + Gia_ManForEachAnd( pGia, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( pGia, pObj, k ) { + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + if (Gia_ObjIsPo(pGia, pObj)) { + if(isPIAndDontCare(pGia, Gia_ObjFanin0(pObj), pCare, f)) { + po_values.back().push_back('x'); + } else { + po_values.back().push_back(pObj->fMark0 + '0'); + } + } + } + Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k ) + pObjRo->fMark0 = pObjRi->fMark0; + } + assert( iBit == pCex->nBits ); +} + +Wlc_Ntk_t * AddAuxPOsForOperators(Wlc_Ntk_t * pNtk, std::vector& vec_ids, int max_input_bw, int max_output_bw) +{ + Wlc_Ntk_t * p = DupNtkAndUpdateIDs(pNtk, vec_ids); + + Wlc_Obj_t * pObj; + int iFin0, iFin1; + int iNew, iFin0New, iFin1New; + Vec_Int_t * vFanins = Vec_IntAlloc( 1 ); + + for(unsigned i = 0; i < vec_ids.size(); i++) { + pObj = Wlc_NtkObj(p, vec_ids[i]); + iFin0 = Wlc_ObjFaninId0(pObj); + iFin1 = Wlc_ObjFaninId1(pObj); + + Vec_IntFill(vFanins, 1, iFin0); + iFin0New = create_buffer(p, Wlc_NtkObj(p, iFin0), vFanins, max_input_bw); + Vec_IntFill(vFanins, 1, iFin1); + iFin1New = create_buffer(p, Wlc_NtkObj(p, iFin1), vFanins, max_input_bw); + Vec_IntFill(vFanins, 1, vec_ids[i]); + iNew = create_buffer(p, Wlc_NtkObj(p, vec_ids[i]), vFanins, max_output_bw); + + Wlc_NtkObj(p, iFin0New)->fIsPo = 1; + Wlc_NtkObj(p, iFin1New)->fIsPo = 1; + Wlc_NtkObj(p, iNew)->fIsPo = 1; + + Vec_IntInsert(&p->vCos, Wlc_NtkPoNum(p), iFin0New); + Vec_IntPush(&p->vPos, iFin0New); + Vec_IntInsert(&p->vCos, Wlc_NtkPoNum(p), iFin1New); + Vec_IntPush(&p->vPos, iFin1New); + Vec_IntInsert(&p->vCos, Wlc_NtkPoNum(p), iNew); + Vec_IntPush(&p->vPos, iNew); + } + + Wlc_Ntk_t * pNew = DupNtkAndUpdateIDs(p, vec_ids); + + Vec_IntFree(vFanins); + Wlc_NtkFree(p); + return pNew; +} + +Wlc_Ntk_t * RemoveAuxPOs(Wlc_Ntk_t * p, int iStart) +{ + int iObj; + while (Wlc_NtkPoNum(p) > iStart) { + iObj = Vec_IntEntry(&p->vPos, iStart); + Wlc_NtkObj(p, iObj)->fIsPo = 0; + Vec_IntDrop(&p->vPos, iStart); + Vec_IntDrop(&p->vCos, iStart); + } + + Wlc_Ntk_t * pNew = Wlc_NtkDupDfsSimple(p); + return pNew; +} + +Wlc_Ntk_t * MakeUnderApprox(Wlc_Ntk_t * pNtk, int num_bits) { + int nOrigObjNum = Wlc_NtkObjNumMax(pNtk); + Wlc_NtkCleanCopy( pNtk ); + + Wlc_Obj_t * pObj; + int i; + + Wlc_NtkForEachPi(pNtk, pObj, i) { + pObj->Mark = 1; + } + + auto create_under_pi = [&pNtk, &num_bits] (Wlc_Obj_t * pObj) { + int i = Wlc_ObjId(pNtk, pObj); + int range = Wlc_ObjRange(pObj); + if (range <= num_bits) + return i; + + Vec_Int_t * vFanins = Vec_IntAlloc( 1 ); + int isSigned = Wlc_ObjIsSigned(pObj); + + Vec_IntFill(vFanins, 1, i); + int iShrink = Wlc_ObjCreate(pNtk, WLC_OBJ_BUF, isSigned, num_bits - 1, 0, vFanins); + Vec_IntFill(vFanins, 1, iShrink); + int iObj = Wlc_ObjCreate(pNtk, WLC_OBJ_BUF, isSigned, range - 1, 0, vFanins); + + Vec_IntFree(vFanins); + + return iObj; + }; + + ModifyMarkedNodes(pNtk, nOrigObjNum, create_under_pi); + + Wlc_Ntk_t * pNew = Wlc_NtkDupDfsSimple(pNtk); + + return pNew; +} + +Wlc_Ntk_t * IntroduceBitwiseChoices( Wlc_Ntk_t * pNtk, vector& vec_ids, const vector& vec_greys, vector& vec_choice2idx ) +{ + Wlc_Ntk_t * p = DupNtkAndUpdateIDs(pNtk, vec_ids); + int nOrigObjNum = Wlc_NtkObjNumMax(p); + Wlc_NtkCleanCopy( p ); + + Wlc_Obj_t * pObj; + int iObj; + + map map_node2pi; + map map_node2idx; + map map_node2grey; + + for (size_t i = 0; i < vec_greys.size(); ++i) { + const Greyness& grey = vec_greys[i]; + if(grey.IsWhite()) continue; + + iObj = vec_ids[i]; + pObj = Wlc_NtkObj(p, iObj); + pObj->Mark = 1; + map_node2pi[iObj] = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ); + map_node2grey[iObj] = &grey; + map_node2idx[iObj] = int(i); + } + + auto create_output_with_bitwise_mux = [&vec_choice2idx, &map_node2grey, &map_node2idx, &map_node2pi, &p](Wlc_Obj_t * pObj) { + Vec_Int_t * vFanins = Vec_IntAlloc( 100 ); + Vec_Int_t * vFanins2 = Vec_IntAlloc( 3 ); + + int i = Wlc_ObjId(p, pObj); + bool isSigned = bool(Wlc_ObjIsSigned(pObj)); + int range = Wlc_ObjRange(pObj); + int offset = pObj->Beg; + + Vec_IntClear(vFanins); + for (int pos = 0; pos < range; ++pos) { + Vec_IntClear(vFanins2); + Vec_IntPush(vFanins2, i); + Vec_IntPushTwo(vFanins2, pos + offset, pos + offset); + int iWhiteBit = Wlc_ObjCreate(p, WLC_OBJ_BIT_SELECT, 0, 0, 0, vFanins2); + + if(map_node2grey[i]->Get(pos)) { // add choice/sel + Vec_IntClear(vFanins2); + Vec_IntPush(vFanins2, map_node2pi[i]); + Vec_IntPushTwo(vFanins2, pos, pos); + int iBlackBit = Wlc_ObjCreate(p, WLC_OBJ_BIT_SELECT, 0, 0, 0, vFanins2); + + int iSel = Wlc_ObjAlloc( p, WLC_OBJ_PI, 0, 0, 0); + Vec_IntClear(vFanins2); + Vec_IntPush(vFanins2, iSel); + Vec_IntPush(vFanins2, iBlackBit); + Vec_IntPush(vFanins2, iWhiteBit); + Vec_IntPush(vFanins, Wlc_ObjCreate(p, WLC_OBJ_MUX, 0, 0, 0, vFanins2)); + + vec_choice2idx.push_back(IntPair(map_node2idx[i], pos)); + } else { + Vec_IntPush(vFanins, iWhiteBit); + } + } + Vec_IntReverseOrder(vFanins); + + int iObj = Wlc_ObjCreate(p, WLC_OBJ_BIT_CONCAT, isSigned, range - 1, 0, vFanins); + + Vec_IntFree(vFanins); + Vec_IntFree(vFanins2); + + return iObj; + }; + + ModifyMarkedNodes(p, nOrigObjNum, create_output_with_bitwise_mux); + + Wlc_Ntk_t * pNew = Wlc_NtkDupDfsSimple(p); + Wlc_NtkFree( p ); + + return pNew; +} + +Wlc_Ntk_t * AddConstFlops( Wlc_Ntk_t * pNtk, const set& types ) +{ + Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple(pNtk); + Wlc_NtkCleanCopy( p ); + int nOrigObjNum = Wlc_NtkObjNumMax(p); + Wlc_NtkTransferNames( p, pNtk ); + + Wlc_Obj_t * pObj; + int i, iObjConst0; + + { + Vec_Int_t * vFanins = Vec_IntAlloc( 2 ); + + Vec_IntFill(vFanins, 1, 0); + iObjConst0 = Wlc_ObjCreate(p, WLC_OBJ_CONST, 0, 0, 0, vFanins); + Wlc_NtkObj(p, iObjConst0)->fIsFi = 1; + nOrigObjNum++; + + Vec_IntFree( vFanins ); + } + + Wlc_NtkForEachObj( p, pObj, i ) { + if (types.count(pObj->Type)) { + pObj->Mark = 1; + } + } + + auto create_ff_and_mux = [p, iObjConst0](Wlc_Obj_t * pObj) { + Vec_Int_t * vFanins = Vec_IntAlloc( 3 ); + + int i = Wlc_ObjId(p, pObj); + int isSigned = Wlc_ObjIsSigned(pObj); + int range = Wlc_ObjRange(pObj); + + int iPPI = Wlc_ObjAlloc( p, WLC_OBJ_PI, isSigned, range - 1, 0 ); + int iObjFo = Wlc_ObjCreate( p, WLC_OBJ_FO, 0, 0, 0, vFanins ); + + Vec_IntPush(&p->vCos, iObjConst0); + + if (p->pInits == NULL) { + char * pStr = ABC_ALLOC(char, 2); + pStr[0] = '0'; + pStr[1] = '\0'; + p->pInits = pStr; + } else { + char * pStr = strcpy(ABC_ALLOC(char, strlen(p->pInits) + 2), p->pInits); + pStr[strlen(p->pInits)] = '0'; + pStr[strlen(p->pInits) + 1] = '\0'; + ABC_FREE(p->pInits); + p->pInits = pStr; + } + if ( p->vInits == NULL ) { + p->vInits = Vec_IntAlloc( 100 ); + } + // push vInits + Vec_IntPush( p->vInits, -1 ); + + int iSelID = iObjFo; + Vec_IntClear(vFanins); + Vec_IntPush(vFanins, iSelID); + Vec_IntPush(vFanins, i); + Vec_IntPush(vFanins, iPPI); + int iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins); + + Vec_IntFree( vFanins ); + + return iObj; + }; + + ModifyMarkedNodes(p, nOrigObjNum, create_ff_and_mux); + + Wlc_Ntk_t * pNew = Wlc_NtkDupDfsSimple( p ); + Wlc_NtkTransferNames( pNew, p ); + + Wlc_NtkFree( p ); + + return pNew; +} + +Wlc_Ntk_t * IntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) +{ + if ( vNodes == NULL ) return NULL; + + Wlc_Ntk_t * pNew; + Wlc_Obj_t * pObj; + int i, iObj; + Vec_Int_t * vFanins = Vec_IntAlloc( 3 ); + map map_node2pi; + + Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple(pNtk); + int nOrigObjNum = Wlc_NtkObjNumMax(p); + Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) { + Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj))); + } + + // Vec_IntPrint(vNodes); + Wlc_NtkCleanCopy( p ); + + // mark nodes + Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) { + iObj = Wlc_ObjId(p, pObj); + pObj->Mark = 1; + // add fresh PI with the same number of bits + map_node2pi[iObj] = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ); + } + + auto create_output_mux = [&p, &map_node2pi](Wlc_Obj_t * pObj) { + Vec_Int_t * vFanins = Vec_IntAlloc( 3 ); + + int i = Wlc_ObjId(p, pObj); + int isSigned = Wlc_ObjIsSigned(pObj); + int range = Wlc_ObjRange(pObj); + int iSelID = Wlc_ObjAlloc( p, WLC_OBJ_PI, 0, 0, 0); + Vec_IntClear(vFanins); + Vec_IntPush(vFanins, iSelID); + Vec_IntPush(vFanins, map_node2pi.at(i)); + Vec_IntPush(vFanins, i); + int iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins); + + Vec_IntFree(vFanins); + + return iObj; + }; + + ModifyMarkedNodes(p, nOrigObjNum, create_output_mux); + + // DumpWlcNtk(p); + pNew = Wlc_NtkDupDfsSimple( p ); + + Vec_IntFree(vFanins); + Wlc_NtkFree( p ); + + return pNew; +} + +Wlc_Ntk_t * AbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodesInit ) +{ + Vec_Int_t * vNodes = vNodesInit; + Wlc_Ntk_t * pNew; + Wlc_Obj_t * pObj; + int i, iObj; + map map_node2pi; + + if ( vNodes == NULL ) + return NULL; + + Wlc_Ntk_t * p = NULL; + p = Wlc_NtkDupDfsSimple(pNtk); + Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) { + Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj))); + } + + int nOrigObjNum = Wlc_NtkObjNumMax( p ); + // mark nodes + Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) { + iObj = Wlc_ObjId(p, pObj); + pObj->Mark = 1; + // add fresh PI with the same number of bits + map_node2pi[iObj] = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ); + } + + auto create_black_output = [&p, &map_node2pi](Wlc_Obj_t * pObj) { + return map_node2pi[Wlc_ObjId(p, pObj)]; + }; + + Wlc_NtkCleanCopy( p ); + ModifyMarkedNodes(p, nOrigObjNum, create_black_output); + + if ( vNodes != vNodesInit ) + Vec_IntFree( vNodes ); + // reconstruct topological order + pNew = Wlc_NtkDupDfsSimple( p ); + //Wlc_NtkTransferNames( pNew, p ); + Wlc_NtkFree( p ); + return pNew; +} + +Wlc_Ntk_t * MakeUnderApprox2(Wlc_Ntk_t * pNtk, const set& types, int num_bits) { + Wlc_Obj_t *pObj; + int i, iFanin0, iFanin1; + int iNew, iFanin0New, iFanin1New; + + Vec_Int_t *vFanins = Vec_IntAlloc(2); + Wlc_NtkForEachObj(pNtk, pObj, i) { + if (types.count(pObj->Type)) { + // Already normalized + if (pObj->Mark) continue; + + iFanin0 = Wlc_ObjFaninId0(pObj); + iFanin1 = Wlc_ObjFaninId1(pObj); + + assert(Wlc_ObjIsSigned(Wlc_NtkObj(pNtk, iFanin0))); + assert(Wlc_ObjIsSigned(Wlc_NtkObj(pNtk, iFanin1))); + assert(Wlc_ObjIsSigned(pObj)); + + int range0 = Wlc_ObjRange(Wlc_NtkObj(pNtk, iFanin0)); + int range1 = Wlc_ObjRange(Wlc_NtkObj(pNtk, iFanin1)); + + unsigned op_type = pObj->Type; + + Vec_IntFill(vFanins, 1, iFanin0); + iFanin0New = Wlc_ObjCreate(pNtk, WLC_OBJ_BUF, 1, (range0 > num_bits ? num_bits : range0) - 1, 0, vFanins); + + Vec_IntFill(vFanins, 1, iFanin1); + iFanin1New = Wlc_ObjCreate(pNtk, WLC_OBJ_BUF, 1, (range1 > num_bits ? num_bits : range1) - 1, 0, vFanins); + + int lossless_range = + Wlc_ObjRange(Wlc_NtkObj(pNtk, iFanin0New)) + Wlc_ObjRange(Wlc_NtkObj(pNtk, iFanin1New)); + + Vec_IntFillTwo(vFanins, 2, iFanin0New, iFanin1New); + iNew = Wlc_ObjCreate(pNtk, op_type, 1, lossless_range - 1, 0, vFanins); + + Wlc_NtkObj(pNtk, iNew)->Mark = 1; + + Wlc_NtkObj(pNtk, i)->Type = WLC_OBJ_BUF; + Wlc_NtkObj(pNtk, i)->nFanins = 1; + Wlc_ObjFanins(Wlc_NtkObj(pNtk, i))[0] = iNew; + } + } + + Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple(pNtk); + Vec_Int_t * vConstrs = Vec_IntAlloc(100); + + Wlc_NtkForEachObj(p, pObj, i) { + if (types.count(pObj->Type)) { + iFanin0 = Wlc_ObjFaninId0(pObj); + iFanin1 = Wlc_ObjFaninId1(pObj); + + int iFanin0Fanin0 = Wlc_ObjFaninId0(Wlc_NtkObj(p, iFanin0)); + int iFanin1Fanin0 = Wlc_ObjFaninId0(Wlc_NtkObj(p, iFanin1)); + + Vec_IntFillTwo(vFanins, 2, iFanin0, iFanin0Fanin0); + Vec_IntPush(vConstrs, Wlc_ObjCreate(p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins)); + + Vec_IntFillTwo(vFanins, 2, iFanin1, iFanin1Fanin0); + Vec_IntPush(vConstrs, Wlc_ObjCreate(p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins)); + } + } + + if (Wlc_NtkFfNum(p) == 0) + FoldCombConstraints(p, vConstrs); + else + FoldSeqConstraints(p, vConstrs); + + Wlc_Ntk_t * pNew = Wlc_NtkDupDfsSimple(p); + + Wlc_NtkFree(p); + Vec_IntFree(vFanins); + Vec_IntFree(vConstrs); + + return pNew; +} + +Wlc_Ntk_t * NormalizeDataTypes(Wlc_Ntk_t * p, const set& types, bool fUnify) +{ + Wlc_Ntk_t *pNtk, *pNew; + + pNtk = Wlc_NtkDupDfsSimple(p); + Wlc_NtkTransferNames( pNtk, p ); + + Wlc_Obj_t *pObj; + int i, iFanin0, iFanin1; + int iNew, iFanin0New, iFanin1New; + int lossless_range; + Vec_Int_t * vFanins = Vec_IntAlloc( 2 ); + vector signs; + + Wlc_NtkForEachObj( pNtk, pObj, i ) { + if ( types.count(pObj->Type) ) { + // Already normalized + if (pObj->Mark) continue; + + iFanin0 = Wlc_ObjFaninId0(pObj); + iFanin1 = Wlc_ObjFaninId1(pObj); + + signs.clear(); + signs.push_back(Wlc_ObjIsSigned(Wlc_NtkObj(pNtk, iFanin0))); + signs.push_back(Wlc_ObjIsSigned(Wlc_NtkObj(pNtk, iFanin1))); + signs.push_back(Wlc_ObjIsSigned(pObj)); + + int op_is_signed = signs[0] && signs[1]; + unsigned op_type = pObj->Type; + + Vec_IntFill(vFanins, 1, iFanin0); + if (op_is_signed) + iFanin0New = iFanin0; + else if (fUnify) + iFanin0New = Wlc_ObjCreate(pNtk, WLC_OBJ_BIT_ZEROPAD, 1, Wlc_NtkObj(pNtk, iFanin0)->End + 1, Wlc_NtkObj(pNtk, iFanin0)->Beg, vFanins); + else + iFanin0New = Wlc_ObjCreate(pNtk, WLC_OBJ_BUF, op_is_signed, Wlc_NtkObj(pNtk, iFanin0)->End, Wlc_NtkObj(pNtk, iFanin0)->Beg, vFanins); + + Vec_IntFill(vFanins, 1, iFanin1); + if (op_is_signed) + iFanin1New = iFanin1; + else if (fUnify) + iFanin1New = Wlc_ObjCreate(pNtk, WLC_OBJ_BIT_ZEROPAD, 1, Wlc_NtkObj(pNtk, iFanin1)->End + 1, Wlc_NtkObj(pNtk, iFanin1)->Beg, vFanins); + else + iFanin1New = Wlc_ObjCreate(pNtk, WLC_OBJ_BUF, op_is_signed, Wlc_NtkObj(pNtk, iFanin1)->End, Wlc_NtkObj(pNtk, iFanin1)->Beg, vFanins); + + lossless_range = Wlc_ObjRange(Wlc_NtkObj(pNtk, iFanin0New)) + Wlc_ObjRange(Wlc_NtkObj(pNtk, iFanin1New)); + + Vec_IntFillTwo(vFanins, 2, iFanin0New, iFanin1New); + if (fUnify) + iNew = Wlc_ObjCreate(pNtk, op_type, 1, lossless_range - 1, 0, vFanins); + else + iNew = Wlc_ObjCreate(pNtk, op_type, op_is_signed, lossless_range - 1, 0, vFanins); + + Wlc_NtkObj(pNtk, iNew)->Mark = 1; + + Wlc_NtkObj(pNtk, i)->Type = WLC_OBJ_BUF; + Wlc_NtkObj(pNtk, i)->nFanins = 1; + Wlc_ObjFanins(Wlc_NtkObj(pNtk, i))[0] = iNew; + } + } + Vec_IntFree(vFanins); + + pNew = Wlc_NtkDupDfsSimple(pNtk); + Wlc_NtkTransferNames( pNew, pNtk ); + Wlc_NtkFree(pNtk); + + return pNew; +} + +Wlc_Ntk_t * CreateMiter(Wlc_Ntk_t *pNtk, bool fXor) +{ + assert(Wlc_NtkPoNum(pNtk) == 2); + + Wlc_Ntk_t *pNew = Wlc_NtkDupDfsSimple(pNtk); + Wlc_NtkTransferNames( pNew, pNtk ); + + Wlc_Obj_t *pOldPo0 = Wlc_NtkPo(pNew, 0); + Wlc_Obj_t *pOldPo1 = Wlc_NtkPo(pNew, 1); + //assert(Wlc_ObjRange(pOldPo0) == Wlc_ObjRange(pOldPo1)); + + int iOldPo0 = Wlc_ObjId(pNew, pOldPo0); + int iOldPo1 = Wlc_ObjId(pNew, pOldPo1); + + Vec_Int_t *vFanins = Vec_IntAlloc( 2 ); + Vec_IntFillTwo( vFanins, 2, iOldPo0, iOldPo1 ); + int iNewPo; + if (!fXor) iNewPo = Wlc_ObjCreate( pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins ); + else iNewPo = Wlc_ObjCreate( pNew, WLC_OBJ_BIT_XOR, 0, Wlc_ObjRange(pOldPo0)-1, 0, vFanins ); + Vec_IntFree( vFanins ); + + Vec_IntWriteEntry( &pNew->vPos, 0, iNewPo ); + Vec_IntDrop( &pNew->vPos, 1 ); + Vec_IntWriteEntry( &pNew->vCos, 0, iNewPo ); + Vec_IntDrop( &pNew->vCos, 1 ); + + Wlc_NtkObj(pNew, iNewPo)->fIsPo = 1; + Wlc_NtkObj(pNew, iOldPo0)->fIsPo = 0; + Wlc_NtkObj(pNew, iOldPo1)->fIsPo = 0; + + Wlc_Ntk_t *pNewNew = Wlc_NtkDupDfsSimple(pNew); + Wlc_NtkTransferNames( pNewNew, pNew ); + Wlc_NtkFree(pNew); + return pNewNew; +} + +void PrintWordCEX(Wlc_Ntk_t * pNtk, Abc_Cex_t * pCex, const vector* names) +{ + // PIs at each frame + for (int f = 0; f <= pCex->iFrame; ++f) { + int pos = 0; + for (int i = 0; i < Wlc_NtkPiNum(pNtk); ++i) { + cout << "CEX:"; + for (int k = 0; k < Wlc_ObjRange(Wlc_NtkPi(pNtk, i)); ++k ) { + cout << Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + (Wlc_ObjRange(Wlc_NtkPi(pNtk, i))-k-1)+pos); + } + pos += Wlc_ObjRange(Wlc_NtkPi(pNtk, i)); + cout << ":" ; + if (names) + cout << (*names)[Wlc_ObjId(pNtk, Wlc_NtkPi(pNtk, i))]; + else + cout << Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, Wlc_NtkPi(pNtk, i))); + cout << "@" << f; + cout << endl; + } + } +} + +bool HasOperator(const Wlc_Ntk_t * p, const set& types) +{ + bool ret = false; + for (set::const_iterator it = types.begin(); it != types.end(); it++) { + if (p->nObjs[*it] > 0) { + ret = true; + break; + } + } + return ret; +} + +void ComputeMaxBW(Wlc_Ntk_t * p, const vector& vec_ids, int& max_input_bw, int& max_output_bw ) { + max_input_bw = max_output_bw = 0; + for (unsigned i = 0; i < vec_ids.size(); i++) { + int op_id = vec_ids[i]; + Wlc_Obj_t * pObj = Wlc_NtkObj(p, op_id); + int range = Wlc_ObjRange(pObj); + int range0 = Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)); + int range1 = Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)); + if (range0 > max_input_bw) + max_input_bw = range0; + if (range1 > max_input_bw) + max_input_bw = range1; + if (range > max_output_bw) + max_output_bw = range; + } +} + +static void get_par_solvers(const string& setting, vector& parSolvers) { + stringstream ss(setting); + string str; + while(getline(ss, str, ':')) { + parSolvers.push_back(str); + } +} + +static void writeCexToFile(int ret, FILE * file, Abc_Cex_t * pCex) { + if (file) { + fprintf(file, "%d\n", ret); + if (ret == 0) { + fprintf(file, "%d %d %d %d\n", pCex->nRegs, pCex->nPis, pCex->iFrame, pCex->iPo); + for (int i = pCex->nRegs; i < pCex->nBits; i++) { + fprintf(file, "%c", Abc_InfoHasBit(pCex->pData, i) ? '1' : '0'); + } + fprintf(file, "\n"); + } + } +} + +static void readCexFromFile(int& ret, FILE * file, Abc_Cex_t ** ppCex, int nOrigRegs = -1) { + int res = 0; + res = fscanf(file, "%d", &ret); + assert(res == 1); + if(ret == 0) { + int nRegs, nPis, iFrame, iPo; + res = fscanf(file, "%d %d %d %d", &nRegs, &nPis, &iFrame, &iPo); + assert(res == 4); + if (nOrigRegs != -1) nRegs = nOrigRegs; + *ppCex = Abc_CexAlloc(nRegs, nPis, iFrame + 1); + (*ppCex)->iFrame = iFrame; + (*ppCex)->iPo = iPo; + int c, i = nRegs; + while ((c = fgetc(file)) != EOF) { + if (c == '1' || c == '0') { + if (c == '1') + Abc_InfoSetBit((*ppCex)->pData, i); + ++i; + } + } + } +} + +int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, struct timespec * timeout) { + if ( !pParSetting || pParSetting->empty() || Wlc_NtkFfNum(pNtk) == 0 ) + return bit_level_solve( pNtk, ppCex, pFileName, pParSetting, fSyn ); + + if(*ppCex) { + Abc_CexFree(*ppCex); + *ppCex = NULL; + } + + int ret = -1; + + vector parSolvers; + parSolvers.push_back("pdr"); + get_par_solvers(*pParSetting, parSolvers); + + ret = RunConcurrentSolver( pNtk, parSolvers, ppCex, timeout ); + + return ret; +} + + +int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn) { + if(*ppCex) { + Abc_CexFree(*ppCex); + *ppCex = NULL; + } + + int ret = -1; + Gia_Man_t * pGia = BitBlast(pNtk); + + //int num_orig_regs = Gia_ManRegNum(pGia); + + if(pParSetting && fSyn) { + int num_orig_pis = Gia_ManPiNum(pGia); + pGia = Gia_ManSeqStructSweep(pGia, 1, 1, 0); + assert(num_orig_pis == Gia_ManPiNum(pGia)); + } + + Aig_Man_t * pAig = Gia_ManToAig(pGia, 0); + Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase(pAig); + + if (pFileName && !pFileName->empty()) + Gia_AigerWriteSimple(pGia, &((*pFileName + ".aig")[0u])); + + if (Gia_ManRegNum(pGia) == 0) { + Prove_Params_t Params, *pParams = &Params; + Prove_ParamsSetDefault(pParams); + pParams->fUseRewriting = 0; + pParams->fVerbose = 0; + ret = Abc_NtkIvyProve(&pAbcNtk, pParams); + if (ret == 0) { + *ppCex = Abc_CexDeriveFromCombModel(pAbcNtk->pModel, Abc_NtkPiNum(pAbcNtk), 0, 0); + } + } else { + auto runPDR = [&](FILE * file){ + Pdr_Par_t PdrPars, *pPdrPars = &PdrPars; + Pdr_ManSetDefaultParams(pPdrPars); + pPdrPars->nConfLimit = 0; + //pPdrPars->fDumpInv = 1; + Abc_FrameReadGlobalFrame()->pNtkCur = pAbcNtk; + int res = Abc_NtkDarPdr(pAbcNtk, pPdrPars); + Abc_FrameReadGlobalFrame()->pNtkCur = NULL; + + writeCexToFile(res, file, pAbcNtk->pSeqModel); + + return res; + }; + + /* + auto runBMC3 = [&](FILE * file){ + Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars; + Saig_ParBmcSetDefaultParams(pBmcPars); + int res = Abc_NtkDarBmc3(pAbcNtk, pBmcPars, 0); + + writeCexToFile(res, file, pAbcNtk->pSeqModel); + + return res; + }; + auto runWla = [&](FILE * file){ + Wlc_Par_t WlcPars, *pWlcPars = &WlcPars; + Wlc_ManSetDefaultParams( pWlcPars ); + pWlcPars->nBitsAdd = 8; + pWlcPars->nBitsMul = 4; + pWlcPars->nBitsMux = 8; + pWlcPars->fXorOutput = 0; + pWlcPars->nLimit = 50; + pWlcPars->fVerbose = 1; + pWlcPars->fProofRefine = 1; + pWlcPars->fHybrid = 0; + pWlcPars->fCheckCombUnsat = 1; + + Wla_Man_t * pWla = Wla_ManStart( pNtk, pWlcPars ); + int RetValue = Wla_ManSolve( pWla, pWlcPars ); + + writeCexToFile(RetValue, file, pWla->pCex); + + Wla_ManStop( pWla ); + return RetValue; + }; + + if(pParSetting && !pParSetting->empty()) { + vector parSolvers; + parSolvers.push_back("pdr"); + get_par_solvers(*pParSetting, parSolvers); + vector childs (parSolvers.size()); + vector files (parSolvers.size()); + + auto runChildTask = [&](const string& engine, int i) { + kill_on_parent_death(SIGQUIT); + LOG(4) << "In process (" << getpid() << ") : running " << engine << "..."; + if(engine=="bmc3") { + ret = runBMC3(files[i]); + } else if(engine=="pdr") { + ret = runPDR(files[i]); + } else if(engine=="treb" || engine=="pdra") { + ret = run_zz(pGia, files[i], engine); + } else if(engine=="wla") { + ret = runWla(files[i]); + } else { + assert(false); + } + }; + + for(int i = 0; i < childs.size(); i++) { + files[i] = tmpfile(); + if((childs[i] = fork()) < 0) { + perror("fork"); + abort(); + } else if (childs[i] == 0) { // in child process + runChildTask(parSolvers[i], i); + exit(0); + } + } + + int status; + pid_t wpid = wait(&status); + + for(unsigned i = 0; i < childs.size(); i++) { + if(wpid == childs[i]) { + LOG(2) << "BLS::" << parSolvers[i] << " returns. Kill others."; + for(unsigned j = 0; j < childs.size(); j++) { + if(i == j) continue; + kill(childs[j], SIGQUIT); + LOG(3) << "BLS::Kill " << parSolvers[j] << "."; + wpid = wait(&status); + } + + rewind(files[i]); + readCexFromFile(ret, files[i], ppCex, num_orig_regs); + + break; + } + } + + for(auto x : files) fclose(x); + + } else */ + { + ret = runPDR(NULL); + if (ret == 0) { + *ppCex = Abc_CexDup(pAbcNtk->pSeqModel, -1); + } + } + } + + Gia_ManStop(pGia); + Aig_ManStop(pAig); + Abc_NtkDelete(pAbcNtk); + + return ret; +} + + +Gia_Man_t * GetInvMiter(Wlc_Ntk_t * pNtk, char * nameInv) { + auto check_pla = [](char * name) { + string line; + ifstream ifs (name, std::ifstream::in); + if(ifs) { + while(getline(ifs, line)) { + if (line == ".p 0") { + return false; + } + } + ifs.close(); + } + return true; + }; + + Gia_Man_t * pMiter = NULL; + Gia_Man_t * pGia = BitBlast(pNtk); + printf("Gia stat: pi = %d, ff = %d, and = %d, po = %d\n", Gia_ManPiNum(pGia), Gia_ManRegNum(pGia), Gia_ManAndNum(pGia), Gia_ManPoNum(pGia)); + + if (!check_pla(nameInv)) { + LOG(2) << "Empty invariant. Changed to combinational SAT."; + pMiter = Gia_ManDupInvMiter(pGia, NULL); + } else { + Abc_Ntk_t *pAbcNtk = Io_Read(nameInv, Io_ReadFileType(nameInv), 1, 0); + Abc_Ntk_t *pStrash = Abc_NtkStrash(pAbcNtk, 0, 1, 0); + Aig_Man_t *pAig = Abc_NtkToDar(pStrash, 0, 0); + Gia_Man_t *pInv = Gia_ManFromAig(pAig); + printf("Inv stat: pi = %d, ff = %d, and = %d, po = %d\n", Gia_ManPiNum(pInv), Gia_ManRegNum(pInv), + Gia_ManAndNum(pInv), Gia_ManPoNum(pInv)); + pMiter = Gia_ManDupInvMiter(pGia, pInv); + + Abc_NtkDelete(pAbcNtk); + Abc_NtkDelete(pStrash); + Aig_ManStop(pAig); + Gia_ManStop(pInv); + } + + Gia_ManStop(pGia); + + return pMiter; +} + +void TestInvariant(string& nameNtk, string& nameInv) { + Gia_Man_t * pGia = Gia_AigerRead( &nameNtk[0u], 0, 0, 0 ); + printf("Gia stat: pi = %d, ff = %d, and = %d, po = %d\n", Gia_ManPiNum(pGia), Gia_ManRegNum(pGia), Gia_ManAndNum(pGia), Gia_ManPoNum(pGia)); + + Abc_Ntk_t * pAbcNtk = Io_Read( &nameInv[0u], Io_ReadFileType(&nameInv[0u]), 1, 0 ); + Abc_Ntk_t * pStrash = Abc_NtkStrash( pAbcNtk, 0, 1, 0 ); + Aig_Man_t * pAig = Abc_NtkToDar( pStrash, 0, 0 ); + Gia_Man_t * pInv = Gia_ManFromAig( pAig ); + printf("Inv stat: pi = %d, ff = %d, and = %d, po = %d\n", Gia_ManPiNum(pInv), Gia_ManRegNum(pInv), Gia_ManAndNum(pInv), Gia_ManPoNum(pInv)); + + Gia_Man_t * pMiter = Gia_ManDupInvMiter(pGia, pInv); + Gia_AigerWrite(pMiter, "miter.aig", 0, 0, 0); + + + // TODO : flip Node1, Abc_LitNot(Node2) + // Gia_Man_t * Gia_ManDupInvMiter( Gia_Man_t * p, Gia_Man_t * pInv ) + + // TODO : flip fUseSupp + // void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) + + Abc_NtkDelete(pAbcNtk); + Abc_NtkDelete(pStrash); + Aig_ManStop(pAig); + Gia_ManStop(pInv); + Gia_ManStop(pGia); + Gia_ManStop(pMiter); +} + + +} diff --git a/src/opt/untk/NtkNtk.h b/src/opt/untk/NtkNtk.h new file mode 100755 index 000000000..816a9c61f --- /dev/null +++ b/src/opt/untk/NtkNtk.h @@ -0,0 +1,150 @@ +/* + * NtkNtk.h + * + * Created on: Aug 25, 2015 + * Author: Yen-Sheng Ho + */ + +#ifndef SRC_EXT2_NTK_NTKNTK_H_ +#define SRC_EXT2_NTK_NTKNTK_H_ + +#include +#include +#include +#include +#include +#include +#include +#include "Netlist.h" + +typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; +typedef struct Abc_Cex_t_ Abc_Cex_t; +typedef struct Vec_Int_t_ Vec_Int_t; +typedef struct Gia_Man_t_ Gia_Man_t; + +namespace UFAR { + +using VecVecChar = std::vector >; +using VecVecInt = std::vector >; +using IntPair = std::pair; + +struct OperatorID { + OperatorID() : idx(-1), timediff(0) {} + OperatorID(int i) : idx(i), timediff(0) {} + OperatorID(int i, int t) : idx(i), timediff(t) {} + bool operator< (const OperatorID& rhs) const { + if (timediff != rhs.timediff) return (timediff < rhs.timediff); + return (idx < rhs.idx); + } + bool operator!= (const OperatorID& rhs) const { + return ((idx != rhs.idx) || (timediff != rhs.timediff)); + } + int idx; + int timediff; +}; + +std::ostream& operator<<(std::ostream& os, const OperatorID& obj); + +struct UifPair { + UifPair(const OperatorID& first_, const OperatorID& second_) : first(first_), second(second_), fMark(false) {} + UifPair(const OperatorID& first_, const OperatorID& second_, bool fMark_) : first(first_), second(second_), fMark(fMark_) {} + bool operator< (const UifPair& rhs) const { + if(first != rhs.first) return (first < rhs.first); + if(second != rhs.second) return (second < rhs.second); + return (!fMark && rhs.fMark); + } + OperatorID first; + OperatorID second; + bool fMark; +}; + +class Greyness { +public: + Greyness(Wlc_Ntk_t * pNtk, Wlc_Obj_t * pObj); + + std::string to_string() const { + std::ostringstream oss; + for (size_t i = 0; i < _vec_black_bits.size(); ++i) + oss << ( _vec_black_bits[i] ? '0' : '1' ); + return oss.str(); + } + + bool IsGrey() const { + return (!IsBlack() && !IsWhite()); + } + bool IsWhite() const { + return (std::find(_vec_black_bits.begin(), _vec_black_bits.end(), true) == _vec_black_bits.end()); + } + bool IsBlack() const { + return (std::find(_vec_black_bits.begin(), _vec_black_bits.end(), false) == _vec_black_bits.end()); + } + unsigned TotalCost() const { return _total_cost; } + unsigned CurrentCost() const { return _current_cost; } + void UpdateCost(); + + size_t Size() const { return _vec_black_bits.size(); } + bool Get(size_t pos) const { return _vec_black_bits[pos]; } + void Set(size_t pos, bool val) { _vec_black_bits[pos] = val; } + + void SetWhite() { + _vec_black_bits = std::vector(_vec_black_bits.size(), false); + _current_cost = _total_cost; + } + bool IsTooWhite(float threshold) const { + float ratio = float(_current_cost) / float(_total_cost); + if ((ratio > threshold) || (_current_cost == _total_cost)) + return true; + if (ratio > 0.5 && _total_cost < 1000) + return true; + return false; + } + +private: + std::vector _vec_black_bits; + unsigned _total_cost; + unsigned _current_cost; + unsigned _orig_size; + WNetlist _N_white; + int _iOpId; +}; + +Wlc_Ntk_t * AbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit ); +Wlc_Ntk_t * AddConstFlops( Wlc_Ntk_t * p, const std::set& types ); +Wlc_Ntk_t * IntroduceChoices( Wlc_Ntk_t * p, Vec_Int_t * vNodes ); +Wlc_Ntk_t * IntroduceBitwiseChoices( Wlc_Ntk_t * pNtk, std::vector& vec_ids, const std::vector& vec_greys, std::vector& vec_choice2idx ); +Wlc_Ntk_t * CreateMiter(Wlc_Ntk_t *pNtk, bool fXor); +Wlc_Ntk_t * NormalizeDataTypes(Wlc_Ntk_t * p, const std::set& types, bool fUnify); +Wlc_Ntk_t * AddAuxPOsForOperators(Wlc_Ntk_t * p, std::vector& vec_ids, int max_input_bw = -1, int max_output_bw = -1); +Wlc_Ntk_t * RemoveAuxPOs(Wlc_Ntk_t * p, int iStart); +Wlc_Ntk_t * DupNtkAndUpdateIDs(Wlc_Ntk_t * p, std::vector& vec_ids); +Wlc_Ntk_t * ApplyGreynessConstraints(Wlc_Ntk_t * pNtk, const std::vector& vec_grey, std::vector& vec_ids); +Wlc_Ntk_t * IntroducePrevOperators(Wlc_Ntk_t * pNtk, std::vector& vec_ids, const std::set& set_prev_ops, VecVecInt& vv_op_ffs); +Wlc_Ntk_t * ApplyGreyConstraints(Wlc_Ntk_t * pNtk, std::vector& vec_ids, bool fSeq); +int AddOneFanoutFF(Wlc_Ntk_t * pNtk, int obj_id, unsigned& count_bits); +int AddOneUifImplication(Wlc_Ntk_t * pNtk, const std::array& wires1, const std::array& wires2); +void FoldCombConstraints(Wlc_Ntk_t *pNtk, Vec_Int_t *vConstrs); +void FoldSeqConstraints(Wlc_Ntk_t *pNtk, Vec_Int_t *vConstrs); +void CollectPoValuesInCex(Gia_Man_t * pGia, Abc_Cex_t * pCex, VecVecChar& po_values, bool fCexMin); +bool HasOperator(const Wlc_Ntk_t * p, const std::set& types); + +void ComputeMaxBW(Wlc_Ntk_t * p, const std::vector& vec_ids, int& max_input_bw, int& max_output_bw ); + +void PrintWordCEX(Wlc_Ntk_t * pNtk, Abc_Cex_t * pCex, const std::vector* names = nullptr); + +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 bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const std::string* pFileName = NULL, const std::string* pParSetting = NULL, bool fSyn = false); + +Gia_Man_t * BitBlast(Wlc_Ntk_t * pNtk); + +Gia_Man_t * GetInvMiter(Wlc_Ntk_t * pNtk, char * nameInv); +void TestInvariant(std::string& nameNtk, std::string& nameInv); + +Wlc_Ntk_t * MakeUnderApprox(Wlc_Ntk_t * pNtk, int num_bits); +Wlc_Ntk_t * MakeUnderApprox2(Wlc_Ntk_t * pNtk, const std::set& types, int num_bits); + + +} + +#endif /* SRC_EXT2_NTK_NTKNTK_H_ */ diff --git a/src/opt/untk/module.make b/src/opt/untk/module.make new file mode 100755 index 000000000..35a9eac9f --- /dev/null +++ b/src/opt/untk/module.make @@ -0,0 +1,6 @@ +SRC += src/opt/untk/NtkCmd.cpp \ + src/opt/untk/NtkCmd.h \ + src/opt/untk/Netlist.cpp \ + src/opt/untk/Netlist.h \ + src/opt/untk/NtkNtk.cpp \ + src/opt/untk/NtkNtk.h diff --git a/src/opt/util/module.make b/src/opt/util/module.make new file mode 100755 index 000000000..45e46c251 --- /dev/null +++ b/src/opt/util/module.make @@ -0,0 +1,2 @@ +SRC += src/opt/util/util.cpp \ + src/opt/util/util.h diff --git a/src/opt/util/util.cpp b/src/opt/util/util.cpp new file mode 100755 index 000000000..3b5f1802c --- /dev/null +++ b/src/opt/util/util.cpp @@ -0,0 +1,119 @@ +/* + * util.cpp + * + * Created on: Aug 31, 2015 + * Author: Yen-Sheng Ho + */ + +#include +#include +#include + +#include "util.h" + +using namespace std; + +unsigned LogT::loglevel = 0; +string LogT::prefix = "LOG"; + +bool OptMgr::Parse(int argc, char * argv[]) { + if(argc <= 1) return true; + + for(int i = 1; i < argc; i++) { + if(_map.count(argv[i]) == 0) + return false; + + Option& opt = _map[argv[i]]; + opt._val = "yes"; + + if(!opt.isBool()) { + if (i + 1 == argc) + return false; + opt._val = argv[++i]; + } + } + + return true; +} + +void OptMgr::PrintUsage() { + cout << "usage: " << _cmd << endl; + cout << " Uninterpreted Function Abstraction and Refinement (UFAR)\n"; + for (auto x : _map) { + ostringstream ss; + ss << x.first << " " << (x.second.isBool() ? "" : x.second._arg_type); + cout << " " << setw(10) << left << ss.str(); + cout << " : " << x.second._help << " [default = " << x.second._default << "]" << endl; + } +} + +#ifdef __linux__ + +#include + +void kill_on_parent_death(int sig) +{ + // kill process if parent dies + prctl(PR_SET_PDEATHSIG, sig); + + // the parent might have died before calling prctl + // in that case, it would be adopted by init, whose pid is 1 + if (getppid() == 1) + { + raise(sig); + } +} + +#elif defined(__APPLE__) + +#include + +#include + +#include +#include +#include + +void kill_on_parent_death(int sig) +{ + const int ppid = getppid(); + + std::thread monitor_thread([ppid, sig](){ + + struct kevent change; + EV_SET(&change, ppid, EVFILT_PROC, EV_ADD, NOTE_EXIT, 0, nullptr); + + int kq = kqueue(); + assert( kq >= 0 ); + + struct kevent event; + struct timespec ts = {0, 0}; + + // start listening, we are guaranteed to receive a notification if ppid is dead + kevent(kq, &change, 1, &event, 1, &ts); + + // however, if ppid died before the call to kevent, ppid might not be the pid of the parent + // in that case, the process it would be adopted by init, whose pid is 1 + if( getppid() == 1 ) + { + raise(sig); + } + + // now block on kevent until the the parent process dies + retry_eintr([&](){ + return kevent(kq, &change, 1, &event, 1, nullptr); + }); + + raise(sig); + }); + + monitor_thread.detach(); +} + +#else // neither linux or OS X + +void kill_on_parent_death(int sig) +{ +} + +#endif diff --git a/src/opt/util/util.h b/src/opt/util/util.h new file mode 100755 index 000000000..747177266 --- /dev/null +++ b/src/opt/util/util.h @@ -0,0 +1,85 @@ +/* + * util.h + * + * Created on: Aug 31, 2015 + * Author: Yen-Sheng Ho + */ + +#ifndef SRC_EXT2_UTIL_UTIL_H_ +#define SRC_EXT2_UTIL_UTIL_H_ + +/* http://stackoverflow.com/questions/6168107/how-to-implement-a-good-debug-logging-feature-in-a-project */ + +#include +#include +#include +#include +#include + +#include + +class LogT { + public: + LogT(unsigned _loglevel = 0) { + // _buffer << "LOG" << _loglevel << " :" << std::string(_loglevel > 0 ? _loglevel * 4 : 1, ' '); + _buffer << prefix << " :" << std::string(_loglevel > 0 ? _loglevel * 4 : 1, ' '); + } + + template + LogT & operator<<(T const & value) { + _buffer << value; + return *this; + } + + ~LogT() { + std::cout << _buffer.str() << std::endl; + } + + static unsigned loglevel; + static std::string prefix; + private: + std::ostringstream _buffer; +}; + +#define LOG(level) \ +if (level > LogT::loglevel) ; \ +else LogT(level) + +class OptMgr { + public: + OptMgr(const std::string& cmd) : _cmd(cmd) {} + bool Parse(int argc, char * argv[]); + void AddOpt(const std::string& opt, const std::string& default_val, const std::string& arg_type, const std::string& help) { + _map[opt] = Option(default_val, arg_type, help); + } + std::string GetOptVal(const std::string& opt) {return _map[opt]._val;} + bool operator[](const std::string& opt) {return _has_opt(opt);} + + void PrintUsage(); + private: + struct Option { + Option(){} + Option(const std::string& val, const std::string& arg_type, const std::string& help) : + _default(val), _help(help), _arg_type(arg_type){} + bool isBool() {return _arg_type == "";} + std::string _default; + std::string _help; + std::string _arg_type; + std::string _val; + }; + + bool _has_opt(const std::string& opt) {return !_map[opt]._val.empty();} + + std::map _map; + std::string _cmd; +}; + +static inline unsigned elapsed_time_usec(const timeval& tBefore, const timeval& tAfter) { + return (tAfter.tv_sec - tBefore.tv_sec)*1000000 + (tAfter.tv_usec - tBefore.tv_usec); +} + +void kill_on_parent_death(int sig); + +int call_python(const char* modulename, const char* funcname, const char* aig, std::vector& cex); + +#endif /* SRC_EXT2_UTIL_UTIL_H_ */