From 7a7e1be2f37916ecf7c02231a4d480c766f43579 Mon Sep 17 00:00:00 2001 From: hchchiu Date: Tue, 24 Sep 2024 21:18:55 +0800 Subject: [PATCH 01/10] update the installation method --- README.md | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 21e8471b..c94c3c4f 100755 --- a/README.md +++ b/README.md @@ -3,16 +3,18 @@ - **GV** serves as the bridge between multiple engines, meaning that developers who require several engines can implement their algorithms using only **"GV"** # GV Installation -```json= -git clone git@github.com:ric2k1/gv0.git -cd gv0/ -./SETUP.sh -./INSTALL.sh +```bash= +git clone git@github.com:DVLab-NTU/gv.git +cd gv/ +make +``` +- ** Run unit tests +```bash= +make test ``` - **For using GV tool interface, type after installation:** -```json= -cd GV/ +```bash= ./gv ``` From afa098d66554b2e4f5dacf6c76e1b08357f91679 Mon Sep 17 00:00:00 2001 From: hchchiu Date: Tue, 24 Sep 2024 21:19:50 +0800 Subject: [PATCH 02/10] fix typo --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index c94c3c4f..9d917573 100755 --- a/README.md +++ b/README.md @@ -8,7 +8,7 @@ git clone git@github.com:DVLab-NTU/gv.git cd gv/ make ``` -- ** Run unit tests +- ** Run unit tests:** ```bash= make test ``` From af106796998e9fabf99276dfe3b66dcf52f67757 Mon Sep 17 00:00:00 2001 From: hchchiu Date: Tue, 24 Sep 2024 21:21:39 +0800 Subject: [PATCH 03/10] fix typo --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 9d917573..0cca5a99 100755 --- a/README.md +++ b/README.md @@ -8,7 +8,7 @@ git clone git@github.com:DVLab-NTU/gv.git cd gv/ make ``` -- ** Run unit tests:** +- **Run unit tests:** ```bash= make test ``` From 43a2330222c78b328956bda778be316b942f8cb7 Mon Sep 17 00:00:00 2001 From: hchchiu Date: Wed, 25 Sep 2024 20:34:11 +0800 Subject: [PATCH 04/10] remove support for reading BLIF file --- src/cir/cirCmd.cpp | 7 +------ src/cir/cirMgr.cpp | 3 --- 2 files changed, 1 insertion(+), 9 deletions(-) diff --git a/src/cir/cirCmd.cpp b/src/cir/cirCmd.cpp index be8f0c96..d161679b 100644 --- a/src/cir/cirCmd.cpp +++ b/src/cir/cirCmd.cpp @@ -79,8 +79,6 @@ GVCmdExecStatus CirReadCmd::exec(const string& option) { fileType = VERILOG; } else if (myStrNCmp("-Aiger", options[i], 2) == 0) { fileType = AIGER; - } else if (myStrNCmp("-Blif", options[i], 2) == 0) { - fileType = BLIF; } else { if (fileName.size()) return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[i]); @@ -99,9 +97,6 @@ GVCmdExecStatus CirReadCmd::exec(const string& option) { } else if (fileType == AIGER) { fileExt = fileName.substr(fileName.size() - 4); fileError = (fileExt != ".aig"); - } else if (fileType == BLIF) { - fileExt = fileName.substr(fileName.size() - 5); - fileError = (fileExt != ".blif"); } } else fileError = true; @@ -131,7 +126,7 @@ GVCmdExecStatus CirReadCmd::exec(const string& option) { } void CirReadCmd::usage(const bool& verbose) const { - cout << "Usage: CIRRead <-Verilog | -Aiger | -Blif> <(string fileName)> [-Replace]" << endl; + cout << "Usage: CIRRead <-Verilog | -Aiger> <(string fileName)> [-Replace]" << endl; } void CirReadCmd::help() const { diff --git a/src/cir/cirMgr.cpp b/src/cir/cirMgr.cpp index 0ba070ee..2db77398 100644 --- a/src/cir/cirMgr.cpp +++ b/src/cir/cirMgr.cpp @@ -63,9 +63,6 @@ bool CirMgr::readCircuitNew() { _abcMgr->giaToCir(_fileType, id2Name); genDfsList(); } - /* else if (_fileType == BLIF) {*/ - /* _ysyMgr->readBlif(_fileName);*/ - /*}*/ return true; } From bdb8e7fb3272ea97c37eda6d788a1d307c4bc233 Mon Sep 17 00:00:00 2001 From: hchchiu Date: Wed, 25 Sep 2024 20:45:35 +0800 Subject: [PATCH 05/10] remove building flow figure --- docs/BUILD_TUTORIAL.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/docs/BUILD_TUTORIAL.md b/docs/BUILD_TUTORIAL.md index 8de97361..db5e3a5a 100644 --- a/docs/BUILD_TUTORIAL.md +++ b/docs/BUILD_TUTORIAL.md @@ -6,10 +6,6 @@ This document serves as a guide to understand the building process of GV, focusi This document outlines the steps involved in building GV using CMakeLists. -

-image -

- ## Get the Engines source We utilize ExternalProject_Add to acquire third-party engines since Yosys doesn't currently support CMake. From 98c07fcfd1cafb655e8f26166037211a7f60b91a Mon Sep 17 00:00:00 2001 From: b09901189 Date: Fri, 4 Oct 2024 20:37:55 +0800 Subject: [PATCH 06/10] update CMAKElist and readme for wsl install --- CMakeLists.txt | 3 ++- README.md | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d0905a69..46f052bd 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -208,7 +208,8 @@ target_include_directories(${CMAKE_PROJECT_NAME} PRIVATE ${glucose_SOURCE_DIR}) target_include_directories(${CMAKE_PROJECT_NAME} PRIVATE ${CMAKE_SOURCE_DIR}/satsolvers) # target_link_libraries(${CMAKE_PROJECT_NAME} libabc libyosys readline gmp) -target_link_libraries(${CMAKE_PROJECT_NAME} libabc readline gmp) +find_package(Threads REQUIRED) +target_link_libraries(${CMAKE_PROJECT_NAME} libabc readline gmp dl Threads::Threads) target_link_libraries(${CMAKE_PROJECT_NAME} ${LIBYOSYS_PATH}) # * Link the filesystem library # target_link_libraries(${CMAKE_PROJECT_NAME} stdc++fs) diff --git a/README.md b/README.md index 8a9373c0..89aaa3b6 100755 --- a/README.md +++ b/README.md @@ -16,7 +16,7 @@ export PATH="$(brew --prefix)/bin:$PATH" ``` - for linux : ```bash= -sudo apt-get -y install gperf build-essential bison flex libreadline-dev gawk tcl-dev libffi-dev git cmake parallel +sudo apt-get -y install libgmp-dev gperf build-essential bison flex libreadline-dev gawk tcl-dev libffi-dev git cmake parallel sudo apt-get -y install graphviz xdot pkg-config python3 libboost-system-dev libboost-python-dev libboost-filesystem-dev zlib1g-dev ``` From c2ead507b8d72476f0d958db77da925b11d3e2e0 Mon Sep 17 00:00:00 2001 From: jerry34567 Date: Sun, 6 Oct 2024 15:51:05 +0800 Subject: [PATCH 07/10] add SATSolve DIMACS command --- scripts/RUN_TEST | 6 ++++- src/cmd/gvCmdMgr.h | 7 +++-- src/main/main.cpp | 3 ++- src/sat/minisatMgr.cpp | 59 ++++++++++++++++++++++++++++++++++++++++++ src/sat/minisatMgr.h | 4 +++ src/sat/satCmd.cpp | 59 ++++++++++++++++++++++++++++++++++++++++++ src/sat/satCmd.h | 7 +++++ src/sat/satMgr.cpp | 2 ++ src/sat/satMgr.h | 2 ++ 9 files changed, 145 insertions(+), 4 deletions(-) create mode 100644 src/sat/satCmd.cpp create mode 100644 src/sat/satCmd.h diff --git a/scripts/RUN_TEST b/scripts/RUN_TEST index ee5950a0..ea4d4d28 100755 --- a/scripts/RUN_TEST +++ b/scripts/RUN_TEST @@ -161,7 +161,11 @@ done # run dofile with gv and diff the output with the expected output ref-path() { local TEST=$1 - echo $(realpath --relative-to $(pwd) "$(dirname ${TEST})/../ref_${SYSTEM}/$(basename ${TEST%.*}).log") + local DIR=$(dirname "${TEST}") + local BASE=$(basename "${TEST%.*}") + local REF_DIR="${DIR}/../ref_${SYSTEM}" + local REF_PATH="${REF_DIR}/${BASE}.log" + echo $(perl -MFile::Spec -e 'print File::Spec->abs2rel($ARGV[0], $ARGV[1])' "${REF_PATH}" "$(pwd)") } export -f ref-path diff --git a/src/cmd/gvCmdMgr.h b/src/cmd/gvCmdMgr.h index 68e3affb..74e06a5c 100644 --- a/src/cmd/gvCmdMgr.h +++ b/src/cmd/gvCmdMgr.h @@ -17,7 +17,7 @@ extern GVCmdMgr* gvCmdMgr; // Command Categories to String const string GVCmdTypeString[] = {"Revealed", "Common", "Verify", "Simulate", "Network", - "Abc", "Yosys", "Mode", "Bdd", "Prove", "Itp", "APP", "EXP"}; + "Abc", "Yosys", "Mode", "Bdd", "Prove", "Itp", "APP", "SATSolving", "EXP"}; // Command Categories Enum enum GVCmdType { @@ -34,7 +34,8 @@ enum GVCmdType { GV_CMD_TYPE_PROVE = 9, GV_CMD_TYPE_ITP = 10, GV_CMD_TYPE_APP = 11, - GV_CMD_TYPE_EXPERIMENT = 12, + GV_CMD_TYPE_SATSOLVE = 12, + GV_CMD_TYPE_EXPERIMENT = 13, }; enum GVCmdExecStatus { @@ -60,6 +61,7 @@ const unordered_set _setupMode{ GV_CMD_TYPE_MOD, GV_CMD_TYPE_BDD, GV_CMD_TYPE_YOSYS, + GV_CMD_TYPE_SATSOLVE, GV_CMD_TYPE_EXPERIMENT, GV_CMD_TYPE_SIMULATE}; @@ -70,6 +72,7 @@ const unordered_set _vrfMode{ GV_CMD_TYPE_MOD, GV_CMD_TYPE_PROVE, GV_CMD_TYPE_ITP, + GV_CMD_TYPE_SATSOLVE, GV_CMD_TYPE_EXPERIMENT}; #define GV_COMMAND(cmd, type) \ diff --git a/src/main/main.cpp b/src/main/main.cpp index b9b75f17..98c6376e 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -38,6 +38,7 @@ extern bool initItpCmd(); extern bool initCirCmd(); extern bool initYosysCmd(); extern bool initAppCmd(); +extern bool initSatCmd(); extern bool initExpCmd(); static void usage() { @@ -73,7 +74,7 @@ int main(int argc, char** argv) { // cout << "[EXPERIMENTAL VERSION FOR CMAKE v0.1]\n"; // clang-format off if (!(initCommonCmd() && initSimCmd() && initVrfCmd() && initAbcCmd() && initModCmd() && initBddCmd() - && initProveCmd() && initItpCmd() && initCirCmd() && initYosysCmd() && initAppCmd() && initExpCmd())) + && initProveCmd() && initItpCmd() && initCirCmd() && initYosysCmd() && initAppCmd() && initSatCmd() && initExpCmd())) return 1; // clang-format on diff --git a/src/sat/minisatMgr.cpp b/src/sat/minisatMgr.cpp index 50515af2..936370f1 100644 --- a/src/sat/minisatMgr.cpp +++ b/src/sat/minisatMgr.cpp @@ -9,6 +9,7 @@ #include "minisatMgr.h" #include +#include #include "cirGate.h" #include "cirMgr.h" @@ -17,6 +18,8 @@ using namespace gv::cir; using gv::sat::MinisatMgr; +MinisatMgr::MinisatMgr() {} + MinisatMgr::MinisatMgr(CirMgr* cirMgr) : SatSolverMgr(cirMgr), _cirMgr(cirMgr) { _solver = new SolverV(); _solver->proof = new Proof(); @@ -259,3 +262,59 @@ void MinisatMgr::addBoundedVerifyDataRecursively(const CirGate* gate, const uint const bool MinisatMgr::existVerifyData(const CirGate* gate, const uint32_t& depth) { return getVerifyData(gate, depth); } + +void MinisatMgr::solve_dimacs_cnf(const string& filename) { + _solver_dimacs = new SolverV(); + + fstream file; + file.open(filename); + + string p; + string cnf; + int nVars, nClauses; + string line; + getline(file,line); + while (line[0] == 'c') { + getline(file, line); + } + if (file.eof()) { + cerr << "Error: Unexpected end of file" << endl; + return; + } + stringstream ss(line); + ss >> p >> cnf >> nVars >> nClauses; + + for (int i = 0; i < nVars; ++i) { + _solver_dimacs->newVar(); + } + + for (int i = 0; i < nClauses; ++i) { + getline(file, line); + if (line[0] == 'c') { + --i; + continue; + } + vec lits; + lits.clear(); + stringstream ss(line); + int lit; + while (ss >> lit) { + if (lit == 0) break; + lits.push(mkLit(abs(lit) - 1, lit < 0)); + } + _solver_dimacs->addClause(lits); + } + _solver_dimacs->verbosity = 1; + bool result = _solver_dimacs->solve(); + if (result) { + cout << "SAT" << endl; + for (int i = 0; i < nVars; ++i) { + if (_solver_dimacs->model[i] == gv_l_True) + cout << i + 1 << " "; + else + cout << -(i + 1) << " "; + } + } else { + cout << "UNSAT"; + } +} \ No newline at end of file diff --git a/src/sat/minisatMgr.h b/src/sat/minisatMgr.h index 3ff19dad..3fd30746 100644 --- a/src/sat/minisatMgr.h +++ b/src/sat/minisatMgr.h @@ -33,6 +33,7 @@ class MinisatMgr : public SatSolverMgr { friend class gv::itp::ItpMgr; public: + MinisatMgr(); MinisatMgr(gv::cir::CirMgr*); ~MinisatMgr(); @@ -71,6 +72,8 @@ class MinisatMgr : public SatSolverMgr { int nVars() { return _solver->nVars(); }; const Var getVerifyData(const gv::cir::CirGate*, const uint32_t&) const; + void solve_dimacs_cnf(const string& filename); + private: const Var newVar(); /*const Var getVerifyData(const gv::cir::CirGate*, const uint32_t&) const;*/ @@ -81,6 +84,7 @@ class MinisatMgr : public SatSolverMgr { inline const size_t getNegVar(const Var& v) const { return ((getPosVar(v)) | 1ul); } SolverV* _solver; // Pointer to a Minisat solver + SolverV* _solver_dimacs; // Pointer to a Minisat solver for DIMACS CNF Var _curVar; // Variable currently vec _assump; // Assumption List for assumption solve vector* _ntkData; // Mapping between GVNetId and Solver Data diff --git a/src/sat/satCmd.cpp b/src/sat/satCmd.cpp new file mode 100644 index 00000000..96415422 --- /dev/null +++ b/src/sat/satCmd.cpp @@ -0,0 +1,59 @@ +#ifndef GV_SIM_CMD_C +#define GV_SIM_CMD_C + +#include "satCmd.h" + +#include +#include + +#include "gvMsg.h" + +#include "minisatMgr.h" +#include "satMgr.h" +#include "util.h" + +#include "iostream" + +bool initSatCmd() { + return (gvCmdMgr->regCmd("SATSolve DIMACS", 4, 6, new SatSolveDimacCmd)); +} + +using namespace gv::sat; + +//---------------------------------------------------------------------- +// EXPeriment +//---------------------------------------------------------------------- +GVCmdExecStatus SatSolveDimacCmd::exec(const string& option) { + //! Place your experimental functions and commands here + vector options; + GVCmdExec::lexOptions(option, options); + + if (options.size() < 2) return GVCmdExec::errorOption(GV_CMD_OPT_MISSING, ""); + if (options.size() > 2) return GVCmdExec::errorOption(GV_CMD_OPT_EXTRA, options[2]); + + if (myStrNCmp("-File", options[0], 2) != 0) + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[0]); + + string filename = options[1]; + ifstream file(filename); + if (!file.is_open()) { + gvMsg(GV_MSG_ERR) << "File " << filename << " does NOT Exist !!" << endl; + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[1]); + } + + SatSolverMgr *gvSatSolver = new gv::sat::MinisatMgr(); + gvSatSolver->solve_dimacs_cnf(filename); + + return GV_CMD_EXEC_DONE; +} + +void SatSolveDimacCmd::usage(const bool& verbose) const { + gvMsg(GV_MSG_IFO) << "Usage: SATSolve DIMACS <-File >" << endl; +} + +void SatSolveDimacCmd::help() const { + gvMsg(GV_MSG_IFO) << setw(20) << std::left << "SATSolve DIMACS: " + << "Command for satsolving DIMACS format file." << endl; +} + +#endif diff --git a/src/sat/satCmd.h b/src/sat/satCmd.h new file mode 100644 index 00000000..244b6b1c --- /dev/null +++ b/src/sat/satCmd.h @@ -0,0 +1,7 @@ +#pragma once + + +#include "gvCmdMgr.h" + +GV_COMMAND(SatSolveDimacCmd, GV_CMD_TYPE_SATSOLVE); + diff --git a/src/sat/satMgr.cpp b/src/sat/satMgr.cpp index 854eae13..7beadf18 100644 --- a/src/sat/satMgr.cpp +++ b/src/sat/satMgr.cpp @@ -5,6 +5,8 @@ namespace sat { /*SatSolverMgr::SatSolverMgr(CirMgr* c) : _cirMgr(c), _solver(Solver::MINISAT) {*/ /*}*/ +SatSolverMgr::SatSolverMgr() {} + SatSolverMgr::SatSolverMgr(gv::cir::CirMgr* c) : _cirMgr(c) {} SatSolverMgr::~SatSolverMgr() {} diff --git a/src/sat/satMgr.h b/src/sat/satMgr.h index b6cfed2c..9d612486 100644 --- a/src/sat/satMgr.h +++ b/src/sat/satMgr.h @@ -25,6 +25,7 @@ enum class SATSolverType { // Top-level SAT solver manager class SatSolverMgr { public: + SatSolverMgr(); SatSolverMgr(gv::cir::CirMgr*); virtual ~SatSolverMgr(); @@ -53,6 +54,7 @@ class SatSolverMgr { virtual int nVars() { return 0; }; virtual const GVBitVecX getDataValue(const gv::cir::CirGate* gate, const uint32_t& depth) const { return GVBitVecX(); }; virtual const Var getVerifyData(const gv::cir::CirGate*, const uint32_t&) const {}; + virtual void solve_dimacs_cnf(const string& filename) {}; private: gv::cir::CirMgr* _cirMgr; From 06717c23bba7b944ff153cbca38ad41d41c70dd4 Mon Sep 17 00:00:00 2001 From: jerry34567 Date: Sun, 6 Oct 2024 20:39:05 +0800 Subject: [PATCH 08/10] update satsolve dimacs test dofile and comment out minisat/Global.h operator overload != --- satsolvers/minisat/Global.h | 2 +- testbench/dimacs_sat.txt | 151 +++++++++++++ testbench/dimacs_unsat.txt | 202 ++++++++++++++++++ tests/common/ref_linux/help.log | 3 + tests/sat/dofile/satsolve_dimacs_sat.dofile | 2 + tests/sat/dofile/satsolve_dimacs_unsat.dofile | 2 + tests/sat/ref_linux/satsolve_dimacs_sat.log | 11 + tests/sat/ref_linux/satsolve_dimacs_unsat.log | 10 + 8 files changed, 382 insertions(+), 1 deletion(-) create mode 100644 testbench/dimacs_sat.txt create mode 100644 testbench/dimacs_unsat.txt create mode 100644 tests/sat/dofile/satsolve_dimacs_sat.dofile create mode 100644 tests/sat/dofile/satsolve_dimacs_unsat.dofile create mode 100644 tests/sat/ref_linux/satsolve_dimacs_sat.log create mode 100644 tests/sat/ref_linux/satsolve_dimacs_unsat.log diff --git a/satsolvers/minisat/Global.h b/satsolvers/minisat/Global.h index 44a082a0..02842b6f 100644 --- a/satsolvers/minisat/Global.h +++ b/satsolvers/minisat/Global.h @@ -275,7 +275,7 @@ const gvlbool gv_l_Undef = toLbool( 0); #ifndef __SGI_STL_INTERNAL_RELOPS // (be aware of SGI's STL implementation...) #define __SGI_STL_INTERNAL_RELOPS -template static inline bool operator != (const T& x, const T& y) { return !(x == y); } +// template static inline bool operator != (const T& x, const T& y) { return !(x == y); } template static inline bool operator > (const T& x, const T& y) { return y < x; } template static inline bool operator <= (const T& x, const T& y) { return !(y < x); } template static inline bool operator >= (const T& x, const T& y) { return !(x < y); } diff --git a/testbench/dimacs_sat.txt b/testbench/dimacs_sat.txt new file mode 100644 index 00000000..0522edaa --- /dev/null +++ b/testbench/dimacs_sat.txt @@ -0,0 +1,151 @@ +p cnf 60 150 +16 -53 32 -9 0 +-17 -52 0 +-53 32 -45 2 0 +43 8 -20 0 +51 -17 26 -57 0 +17 -43 0 +54 30 -4 10 0 +-42 5 20 -17 0 +34 -30 -36 0 +-60 30 -13 0 +18 -17 -58 -1 0 +14 -29 -36 0 +-57 19 6 0 +47 33 0 +-28 -11 51 0 +-60 -59 0 +-2 -1 -45 37 0 +-50 4 -10 0 +30 26 0 +-8 -17 19 0 +44 -8 0 +14 -2 8 0 +5 45 -51 0 +-16 -39 -49 0 +56 -2 0 +-47 47 0 +-38 -60 34 32 0 +-30 5 0 +-25 17 -11 -49 0 +47 -23 11 -59 0 +-58 20 23 0 +51 31 40 -3 0 +-25 13 0 +46 -16 -26 0 +40 -32 -7 0 +19 -41 -35 0 +-35 24 30 -33 0 +-47 40 0 +38 -43 -41 -17 0 +-50 -18 60 0 +-43 57 39 0 +-53 -21 -52 -58 0 +-49 -31 0 +-38 -41 0 +-38 -31 0 +-1 37 12 34 0 +-14 -59 -9 45 0 +-23 -42 -25 -43 0 +55 44 -52 -20 0 +-2 -59 0 +-22 44 26 47 0 +21 5 0 +29 45 -39 -38 0 +-43 -25 -32 0 +-19 23 10 0 +-33 20 15 0 +18 32 23 0 +-33 -26 0 +13 -20 -53 6 0 +51 -48 0 +-56 41 -34 0 +-48 58 55 0 +25 50 0 +46 -6 43 58 0 +57 -30 -13 0 +-43 -14 -40 0 +-27 -60 -9 31 0 +2 44 50 0 +-48 6 0 +-8 33 42 0 +-57 -18 -40 6 0 +-8 -26 -6 -54 0 +46 -32 0 +32 -11 0 +27 53 -32 -32 0 +58 -55 51 0 +-31 30 -21 0 +-37 9 -30 0 +42 -6 -59 23 0 +16 -49 24 20 0 +3 -15 -15 -4 0 +-22 58 0 +-35 -39 -29 26 0 +28 11 0 +39 24 -60 0 +-14 -54 -53 -54 0 +55 27 0 +49 -35 0 +12 -48 -10 0 +-21 4 52 -50 0 +14 54 2 -42 0 +42 -5 26 0 +-18 24 30 0 +-3 1 0 +33 30 -51 0 +40 -9 -45 -32 0 +-34 23 0 +27 59 -4 0 +-39 6 0 +42 23 -32 0 +29 -55 -15 -59 0 +13 -30 0 +45 58 -33 4 0 +-34 34 0 +-53 -23 -23 54 0 +-14 11 17 0 +7 -5 0 +51 -12 32 0 +3 16 0 +-24 -15 0 +-7 39 0 +41 39 -22 0 +-40 -31 0 +-40 12 -7 -24 0 +-3 3 0 +60 -51 0 +-52 -23 47 0 +38 -36 5 0 +50 21 0 +39 43 -34 0 +-6 -20 -42 -14 0 +-55 -8 32 0 +-41 21 -18 0 +38 12 0 +-38 52 3 -27 0 +20 29 24 36 0 +-42 -39 5 -42 0 +21 -36 30 -25 0 +-23 -42 0 +4 -37 0 +21 -59 -15 55 0 +-39 -13 -41 13 0 +7 -38 37 52 0 +-2 23 20 5 0 +-37 -25 0 +38 46 15 0 +-59 55 0 +-29 -25 -40 -37 0 +-15 -7 37 -46 0 +51 44 -33 0 +46 17 0 +3 54 6 19 0 +-56 17 -9 -57 0 +-47 31 38 -17 0 +60 -59 -59 0 +-56 -21 0 +35 -26 52 -2 0 +-24 -52 8 0 +29 -14 4 -57 0 +41 -41 0 diff --git a/testbench/dimacs_unsat.txt b/testbench/dimacs_unsat.txt new file mode 100644 index 00000000..1957a7a7 --- /dev/null +++ b/testbench/dimacs_unsat.txt @@ -0,0 +1,202 @@ +p cnf 60 200 +-22 -26 -55 0 +-42 -39 48 -4 0 +-59 -33 -49 -54 0 +-30 7 -51 -55 0 +20 23 0 +58 -59 0 +16 -4 -47 -16 0 +38 36 26 0 +37 45 17 -3 0 +12 -19 -15 0 +-31 23 0 +-8 60 0 +-30 -26 -2 0 +38 -33 0 +-40 52 0 +58 11 60 -24 0 +30 17 0 +38 -38 0 +11 18 -42 20 0 +8 -49 0 +55 53 -42 7 0 +-13 41 0 +49 38 51 2 0 +-38 -24 -35 0 +-22 -29 0 +32 11 -41 25 0 +52 -38 0 +-33 58 -7 0 +57 32 -17 28 0 +51 27 -26 31 0 +32 -2 -3 0 +10 -34 0 +15 57 40 15 0 +-50 56 -10 -22 0 +-30 30 15 3 0 +45 15 0 +53 55 -28 35 0 +-47 17 47 0 +60 -40 0 +36 -54 43 4 0 +23 -49 -58 14 0 +-26 59 -1 -35 0 +-39 -36 0 +32 -51 40 51 0 +42 -15 6 4 0 +31 22 3 0 +-28 -32 0 +-47 30 5 6 0 +16 52 48 -10 0 +5 21 -42 -37 0 +35 -45 34 50 0 +-50 -47 0 +30 22 0 +-28 18 14 0 +-44 50 0 +24 -12 -5 0 +-31 -39 -4 0 +33 19 -47 -40 0 +56 30 0 +22 -56 0 +-48 53 0 +-44 -32 -10 0 +-44 29 0 +24 38 0 +-12 54 -37 0 +55 38 38 0 +8 14 -59 0 +-35 12 0 +48 48 0 +-36 -33 -13 -1 0 +45 -59 0 +-25 20 29 0 +27 -1 7 49 0 +-55 -40 -29 0 +-25 -17 20 -6 0 +18 32 22 0 +-49 18 -38 -16 0 +-22 -50 0 +-30 10 0 +50 25 0 +21 -7 16 51 0 +-11 -33 -26 0 +-11 -3 -52 0 +-37 -34 15 0 +41 -57 31 8 0 +-36 1 -2 -56 0 +-27 27 0 +-47 -1 -6 55 0 +43 -50 44 -34 0 +34 18 46 0 +27 -38 -56 1 0 +55 20 0 +42 -2 0 +56 33 4 -7 0 +-47 -11 0 +53 46 0 +19 32 -41 0 +34 35 -9 0 +-46 -44 31 0 +-10 -50 0 +-16 -30 32 0 +37 -15 56 -30 0 +28 29 -50 24 0 +-33 -28 0 +28 44 -23 32 0 +7 34 -31 0 +51 -3 -29 0 +-24 37 25 -38 0 +5 -46 -37 0 +-44 2 -26 0 +26 8 29 21 0 +-17 -48 32 0 +35 59 51 0 +17 25 6 -29 0 +-11 -2 27 0 +-4 -46 0 +12 -59 0 +60 37 -3 54 0 +-40 18 0 +-29 22 -8 0 +53 -57 -46 0 +-59 8 0 +-32 -16 -46 0 +-54 -31 40 0 +-24 -3 18 -20 0 +31 -57 -15 -17 0 +-22 16 49 0 +22 20 26 -44 0 +-15 -23 9 0 +26 -22 0 +-32 11 -31 0 +17 3 10 0 +-43 -44 38 19 0 +-12 40 5 0 +-22 -43 0 +50 -27 3 0 +35 6 0 +-14 53 -25 0 +-10 -28 19 0 +18 7 5 0 +30 29 -4 45 0 +-16 -43 0 +-43 16 0 +-41 9 39 0 +49 26 55 0 +-29 44 -24 0 +-60 9 0 +40 -16 1 26 0 +57 -12 0 +39 -45 46 0 +-29 59 -35 0 +39 1 -48 -42 0 +-26 44 55 0 +-11 56 0 +26 -26 -11 -42 0 +52 23 -32 -43 0 +-25 -28 0 +-57 41 0 +-51 -7 -46 0 +-39 -6 0 +-3 -37 -33 40 0 +28 41 -15 0 +15 -40 18 2 0 +30 -24 2 0 +-29 36 -50 -34 0 +-10 -42 -12 58 0 +-41 -2 51 0 +-25 57 -29 0 +45 -45 0 +39 -45 17 0 +-46 44 -37 -12 0 +-19 -59 0 +15 -46 47 -14 0 +50 58 16 2 0 +-24 28 0 +5 41 0 +49 -54 -25 -13 0 +-48 13 47 -15 0 +-22 -54 -48 0 +31 -12 0 +-30 -54 0 +48 -5 0 +58 -37 5 0 +25 -36 -56 0 +-55 55 60 0 +-50 18 -4 -3 0 +-21 -58 4 0 +30 -40 37 -36 0 +-7 -42 49 0 +-55 -53 -53 0 +60 -5 0 +-41 -3 -59 0 +2 5 0 +-1 37 0 +54 30 0 +11 -51 0 +16 6 0 +24 -23 28 53 0 +-29 -18 -18 -17 0 +-47 -13 4 60 0 + diff --git a/tests/common/ref_linux/help.log b/tests/common/ref_linux/help.log index 6c169bc0..7ca0a1d3 100644 --- a/tests/common/ref_linux/help.log +++ b/tests/common/ref_linux/help.log @@ -45,6 +45,9 @@ BSIMulate: BDD simulation BXNOR: BDD Xnor BXOR: BDD Xor +========== SATSolving Commands : ========== +SATSolve DIMACS: Command for satsolving DIMACS format file. + ========== EXP Commands : ========== EXPeriment: Command for the testing of the experimental functions. diff --git a/tests/sat/dofile/satsolve_dimacs_sat.dofile b/tests/sat/dofile/satsolve_dimacs_sat.dofile new file mode 100644 index 00000000..f6a207e8 --- /dev/null +++ b/tests/sat/dofile/satsolve_dimacs_sat.dofile @@ -0,0 +1,2 @@ +satsolve dimacs -file ./testbench/dimacs_sat.txt +q -f \ No newline at end of file diff --git a/tests/sat/dofile/satsolve_dimacs_unsat.dofile b/tests/sat/dofile/satsolve_dimacs_unsat.dofile new file mode 100644 index 00000000..72e05ddd --- /dev/null +++ b/tests/sat/dofile/satsolve_dimacs_unsat.dofile @@ -0,0 +1,2 @@ +satsolve dimacs -file ./testbench/dimacs_unsat.txt +q -f \ No newline at end of file diff --git a/tests/sat/ref_linux/satsolve_dimacs_sat.log b/tests/sat/ref_linux/satsolve_dimacs_sat.log new file mode 100644 index 00000000..f94ae02e --- /dev/null +++ b/tests/sat/ref_linux/satsolve_dimacs_sat.log @@ -0,0 +1,11 @@ +setup> satsolve dimacs -file ./testbench/dimacs_sat.txt +==================================[MINISAT]=================================== +| Conflicts | ORIGINAL | LEARNT | Progress | +| | Clauses Literals | Limit Clauses Literals Lit/Cl | | +============================================================================== +| 0 | 145 439 | 48 0 0 -nan | 0.000 % | +============================================================================== +SAT +-1 -2 -3 -4 -5 6 -7 -8 -9 -10 11 12 13 -14 -15 16 -17 -18 -19 -20 21 -22 23 24 25 26 27 -28 -29 -30 -31 32 -33 -34 -35 -36 -37 -38 -39 40 -41 -42 -43 44 -45 46 47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 +setup> q -f + diff --git a/tests/sat/ref_linux/satsolve_dimacs_unsat.log b/tests/sat/ref_linux/satsolve_dimacs_unsat.log new file mode 100644 index 00000000..bf47eaaf --- /dev/null +++ b/tests/sat/ref_linux/satsolve_dimacs_unsat.log @@ -0,0 +1,10 @@ +setup> satsolve dimacs -file ./testbench/dimacs_unsat.txt +==================================[MINISAT]=================================== +| Conflicts | ORIGINAL | LEARNT | Progress | +| | Clauses Literals | Limit Clauses Literals Lit/Cl | | +============================================================================== +| 0 | 166 485 | 55 0 0 -nan | 0.000 % | +============================================================================== +UNSAT +setup> q -f + From b29934b04e0458604705baea8bff30ec941d2dc2 Mon Sep 17 00:00:00 2001 From: jerry34567 Date: Sun, 6 Oct 2024 20:48:49 +0800 Subject: [PATCH 09/10] update macos test file --- tests/common/ref_macos/help.log | 3 +++ tests/sat/ref_macos/satsolve_dimacs_sat.log | 11 +++++++++++ tests/sat/ref_macos/satsolve_dimacs_unsat.log | 10 ++++++++++ 3 files changed, 24 insertions(+) create mode 100644 tests/sat/ref_macos/satsolve_dimacs_sat.log create mode 100644 tests/sat/ref_macos/satsolve_dimacs_unsat.log diff --git a/tests/common/ref_macos/help.log b/tests/common/ref_macos/help.log index 6c169bc0..7ca0a1d3 100644 --- a/tests/common/ref_macos/help.log +++ b/tests/common/ref_macos/help.log @@ -45,6 +45,9 @@ BSIMulate: BDD simulation BXNOR: BDD Xnor BXOR: BDD Xor +========== SATSolving Commands : ========== +SATSolve DIMACS: Command for satsolving DIMACS format file. + ========== EXP Commands : ========== EXPeriment: Command for the testing of the experimental functions. diff --git a/tests/sat/ref_macos/satsolve_dimacs_sat.log b/tests/sat/ref_macos/satsolve_dimacs_sat.log new file mode 100644 index 00000000..c262825a --- /dev/null +++ b/tests/sat/ref_macos/satsolve_dimacs_sat.log @@ -0,0 +1,11 @@ +setup> satsolve dimacs -file ./testbench/dimacs_sat.txt +==================================[MINISAT]=================================== +| Conflicts | ORIGINAL | LEARNT | Progress | +| | Clauses Literals | Limit Clauses Literals Lit/Cl | | +============================================================================== +| 0 | 145 439 | 48 0 0 nan | 0.000 % | +============================================================================== +SAT +-1 -2 -3 -4 -5 6 -7 -8 -9 -10 11 12 13 -14 -15 16 -17 -18 -19 -20 21 -22 23 24 25 26 27 -28 -29 -30 -31 32 -33 -34 -35 -36 -37 -38 -39 40 -41 -42 -43 44 -45 46 47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 +setup> q -f + diff --git a/tests/sat/ref_macos/satsolve_dimacs_unsat.log b/tests/sat/ref_macos/satsolve_dimacs_unsat.log new file mode 100644 index 00000000..6ac12482 --- /dev/null +++ b/tests/sat/ref_macos/satsolve_dimacs_unsat.log @@ -0,0 +1,10 @@ +setup> satsolve dimacs -file ./testbench/dimacs_unsat.txt +==================================[MINISAT]=================================== +| Conflicts | ORIGINAL | LEARNT | Progress | +| | Clauses Literals | Limit Clauses Literals Lit/Cl | | +============================================================================== +| 0 | 166 485 | 55 0 0 nan | 0.000 % | +============================================================================== +UNSAT +setup> q -f + From 142c9e03b5cf3387b8aa3b851ea806afc260149e Mon Sep 17 00:00:00 2001 From: jerry34567 Date: Sun, 6 Oct 2024 22:31:01 +0800 Subject: [PATCH 10/10] add itp and prove but exculding socv_hw part --- src/itp/itpCmd.cpp | 139 ++++++++++ src/itp/itpCmd.h | 17 ++ src/itp/itpMgr.cpp | 566 +++++++++++++++++++++++++++++++++++++++++ src/itp/itpMgr.h | 126 +++++++++ src/prove/proveBdd.cpp | 69 +++++ src/prove/proveCmd.cpp | 230 +++++++++++++++++ src/prove/proveCmd.h | 19 ++ 7 files changed, 1166 insertions(+) create mode 100644 src/itp/itpCmd.cpp create mode 100644 src/itp/itpCmd.h create mode 100644 src/itp/itpMgr.cpp create mode 100644 src/itp/itpMgr.h create mode 100644 src/prove/proveBdd.cpp create mode 100644 src/prove/proveCmd.cpp create mode 100644 src/prove/proveCmd.h diff --git a/src/itp/itpCmd.cpp b/src/itp/itpCmd.cpp new file mode 100644 index 00000000..64a03a7b --- /dev/null +++ b/src/itp/itpCmd.cpp @@ -0,0 +1,139 @@ +/**************************************************************************** + FileName [ satCmd.cpp ] + PackageName [ sat ] + Synopsis [ Define basic sat prove package commands ] + Author [ ] + Copyright [ Copyright(c) 2023-present DVLab, GIEE, NTU, Taiwan ] + ****************************************************************************/ + +#include "itpCmd.h" + +#include +#include + +#include "cirGate.h" +#include "cirMgr.h" +#include "gvMsg.h" +#include "itpMgr.h" +#include "minisatMgr.h" +#include "util.h" +using namespace std; + +using namespace gv::cir; + +static gv::itp::ItpMgr* itpMgr = new gv::itp::ItpMgr(); + +bool initItpCmd() { + return (gvCmdMgr->regCmd("SATVerify ITP", 4, 3, new SATVerifyItpCmd) && + gvCmdMgr->regCmd("SATVerify BMC", 4, 3, new SATVerifyBmcCmd)); +} + +//---------------------------------------------------------------------- +// SATVerify ITP < -GateId | -Output > > +//---------------------------------------------------------------------- +GVCmdExecStatus +SATVerifyItpCmd::exec(const string& option) { + vector options; + GVCmdExec::lexOptions(option, options); + + if (options.size() < 2) return GVCmdExec::errorOption(GV_CMD_OPT_MISSING, ""); + if (options.size() > 2) return GVCmdExec::errorOption(GV_CMD_OPT_EXTRA, options[2]); + + bool isNet = false; + + if (myStrNCmp("-GateId", options[0], 2) == 0) + isNet = true; + else if (myStrNCmp("-Output", options[0], 2) == 0) + isNet = false; + else + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[0]); + + int num = 0; + CirGate* gate; + string monitorName = ""; + if (!myStr2Int(options[1], num) || (num < 0)) return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[1]); + if (isNet) { + if ((unsigned)num >= cirMgr->getNumTots()) { + gvMsg(GV_MSG_ERR) << "Net with Id " << num << " does NOT Exist in Current Ntk !!" << endl; + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[1]); + } + gate = cirMgr->getGate(num); + } else { + if ((unsigned)num >= cirMgr->getNumPOs()) { + gvMsg(GV_MSG_ERR) << "Output with Index " << num << " does NOT Exist in Current Ntk !!" << endl; + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[1]); + } + gate = cirMgr->getPo(num); + monitorName = gate->getName(); + } + // get PO's input, since the PO is actually a redundant node and should be removed + CirGate* monitor = new CirAigGate(cirMgr->getNumTots(), 0); + cirMgr->addTotGate(monitor); + monitor->setIn0(gate->getIn0Gate(), gate->getIn0().isInv()); + monitor->setIn1(cirMgr->_const1, false); + itpMgr->verifyPropertyItp(monitorName, monitor); + + return GV_CMD_EXEC_DONE; +} + +void SATVerifyItpCmd::usage(const bool& verbose) const { + cout << "Usage: SATVerify ITP < -GateId | -Output >" << endl; +} + +void SATVerifyItpCmd::help() const { + cout << setw(20) << left << "SATVerify ITP:" + << "check the monitor by interpolation-based technique" << endl; +} + +// //---------------------------------------------------------------------- +// // SATVerify BMC < -GateId | -Output > > +// //---------------------------------------------------------------------- +GVCmdExecStatus +SATVerifyBmcCmd::exec(const string& option) { + vector options; + GVCmdExec::lexOptions(option, options); + + if (options.size() < 2) return GVCmdExec::errorOption(GV_CMD_OPT_MISSING, ""); + if (options.size() > 2) return GVCmdExec::errorOption(GV_CMD_OPT_EXTRA, options[2]); + + bool isNet = false; + + if (myStrNCmp("-GateId", options[0], 2) == 0) + isNet = true; + else if (myStrNCmp("-Output", options[0], 2) == 0) + isNet = false; + else + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[0]); + + int num = 0; + CirGate* gate; + string monitorName = ""; + if (!myStr2Int(options[1], num) || (num < 0)) return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[1]); + if (isNet) { + if ((unsigned)num >= cirMgr->getNumTots()) { + gvMsg(GV_MSG_ERR) << "Gate with Id " << num << " does NOT Exist in Current Cir !!" << endl; + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[1]); + } + gate = cirMgr->getGate(num); + } else { + if ((unsigned)num >= cirMgr->getNumPOs()) { + gvMsg(GV_MSG_ERR) << "Output with Index " << num << " does NOT Exist in Current Cir !!" << endl; + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[1]); + } + monitorName = cirMgr->getPo(num)->getName(); + gate = cirMgr->getPo(num)->getIn0Gate(); + } + // get PO's input, since the PO is actually a redundant node and should be removed + itpMgr->verifyPropertyBmc(monitorName, gate); + + return GV_CMD_EXEC_DONE; +} + +void SATVerifyBmcCmd::usage(const bool& verbose) const { + cout << "Usage: SATVerify BMC < -GateId | -Output < outputIndex >> " << endl; +} + +void SATVerifyBmcCmd::help() const { + cout << setw(20) << left << "SATVerify BMC:" + << "check the monitor by bounded model checking" << endl; +} diff --git a/src/itp/itpCmd.h b/src/itp/itpCmd.h new file mode 100644 index 00000000..a82ac165 --- /dev/null +++ b/src/itp/itpCmd.h @@ -0,0 +1,17 @@ +/**************************************************************************** + FileName [ satCmd.h ] + PackageName [ sat ] + Synopsis [ Define basic sat prove package commands ] + Author [ ] + Copyright [ Copyright(c) 2023-present DVLab, GIEE, NTU, Taiwan ] +****************************************************************************/ + +#pragma once + +#include "gvCmdMgr.h" + +// ============================================================================ +// Classes for Prove package commands +// ============================================================================ +GV_COMMAND(SATVerifyItpCmd, GV_CMD_TYPE_ITP); +GV_COMMAND(SATVerifyBmcCmd, GV_CMD_TYPE_ITP); diff --git a/src/itp/itpMgr.cpp b/src/itp/itpMgr.cpp new file mode 100644 index 00000000..4f56a718 --- /dev/null +++ b/src/itp/itpMgr.cpp @@ -0,0 +1,566 @@ +/**************************************************************************** + FileName [ satMgr.cpp ] + PackageName [ sat ] + Synopsis [ Define sat prove package interface ] + Author [ ] + Copyright [ Copyright(c) 2023-present DVLab, GIEE, NTU, Taiwan ] + ****************************************************************************/ + +#include "itpMgr.h" + +#include +#include +#include +#include + +#include "cirGate.h" +#include "cirMgr.h" +#include "gvMsg.h" +#include "minisat/reader.h" +#include "minisatMgr.h" +#include "satMgr.h" + +using gv::cir::CirMgr; +using gv::sat::MinisatMgr; +using gv::sat::SatSolverMgr; +using namespace gv::cir; + +namespace gv { +namespace itp { + +void ItpMgr::verifyPropertyItp(const string &name, const CirGate *monitor) { + // Initialize + // duplicate the network, so you can modified + // the ntk for the proving property without + // destroying the original network + _cirMgr = new CirMgr(); + *_cirMgr = *cirMgr; + SatProofRes pRes; + /*MinisatMgr *gvSatSolver = new gv::sat::MinisatMgr(_cirMgr);*/ + gv::sat::SatSolverMgr *gvSatSolver = new MinisatMgr(_cirMgr); + + // Prove the monitor here!! + pRes.setMaxDepth(1000); + pRes.setSatSolver(gvSatSolver); + itpUbmc(monitor, pRes); + + pRes.reportResult(name); + if (pRes.isFired()) pRes.reportCex(monitor, _cirMgr); + + // delete gvSatSolver; + // delete _cirMgr; + reset(); +} + +void ItpMgr::verifyPropertyBmc(const string &name, const CirGate *monitor) { + // Initialize + // duplicate the network, so you can modified + // the ntk for the proving property without + // destroying the original network + _cirMgr = new CirMgr(); + *_cirMgr = *cirMgr; + SatProofRes pRes; + /*GVSatSolver *gvSatSolver = new GVSatSolver(_cirMgr);*/ + SatSolverMgr *gvSatSolver = new gv::sat::MinisatMgr(_cirMgr); + + // Prove the monitor here!! + pRes.setMaxDepth(1000); + pRes.setSatSolver(gvSatSolver); + indBmc(monitor, pRes); + + pRes.reportResult(name); + if (pRes.isFired()) pRes.reportCex(monitor, _cirMgr); + + // delete gvSatSolver; + // delete _cirMgr; + reset(); +} + +void ItpMgr::indBmc(const CirGate *monitor, SatProofRes &pRes) { + SatSolverMgr *gvSatSolver = pRes.getSatSolver(); + bind(gvSatSolver); + + uint32_t i = 0; + // GVNetId I = buildInitState(); + CirGate *I = buildInitState(); + + gvSatSolver->addBoundedVerifyData(I, i); + gvSatSolver->assertProperty(I, false, i); + // Start Bounded Model Checking + for (uint32_t j = pRes.getMaxDepth(); i < j; ++i) { + // Add time frame expanded circuit to SAT Solver + gvSatSolver->addBoundedVerifyData(monitor, i); + gvSatSolver->assumeRelease(); + gvSatSolver->assumeProperty(monitor, false, i); + gvSatSolver->simplify(); + // Assumption Solver: If SAT, diproved! + if (gvSatSolver->assump_solve()) { + pRes.setFired(i); + break; + } + gvSatSolver->assertProperty(monitor, true, i); + } +} + +void ItpMgr::itpUbmc(const CirGate *const monitor, SatProofRes &pRes) { + SatSolverMgr *gvSatSolver = pRes.getSatSolver(); + bind(gvSatSolver); + + size_t num_clauses = getNumClauses(); + bool proved = false; + gvSatSolver->assumeRelease(); + // GVNetId S, R, R_prime, tmp1, tmp2, tmp3, tmp4; + CirGate *S; + CirGate *R; + CirGate *R_prime; + CirGate *tmp1; + CirGate *tmp2; + CirGate *tmp3; + CirGate *tmp4; + CirGate *tmp5; + + // TODO : finish your own Interpolation-based property checking + + // PART I: + // Build Initial State + + // PART II: + // Take care the first timeframe (i.e. Timeframe 0 ) + // Check if monitor is violated at timeframe 0 + // Build the whole timeframe 0 and map the var to latch net + // Mark the added clauses ( up to now ) to onset + + // PART III: + // Start the ITP verification loop + // Perform BMC + // SAT -> cex found + // UNSAT-> start inner loop to compute the approx. images + // Each time the clauses are added to the solver, + // mark them to onset/offset carefully + // ( ex. addedBoundedVerifyData(), assertProperty() are called ) +} + +void ItpMgr::bind(SatSolverMgr *ptrMinisat) { + _ptrMinisat = ptrMinisat; + /*if (_ptrMinisat->getProof() == NULL) {*/ + if (_ptrMinisat->getProof() == NULL) { + gvMsg(GV_MSG_ERR) << "The Solver has no Proof!! Try Declaring the Solver " + "with proofLog be set!!" + << endl; + exit(0); + } +} + +void ItpMgr::reset() { + _ptrMinisat = NULL; + _varGroup.clear(); + _var2Net.clear(); + _isClauseOn.clear(); + _isClaOnDup.clear(); +} + +void ItpMgr::markOnsetClause(const ClauseId &cid) { + unsigned cSize = getNumClauses(); + assert(cid < (int)cSize); + if (_isClauseOn.size() < cSize) { + _isClauseOn.resize(cSize, false); + } + _isClauseOn[cid] = true; +} + +void ItpMgr::markOffsetClause(const ClauseId &cid) { + unsigned cSize = getNumClauses(); + assert(cid < (int)cSize); + if (_isClauseOn.size() < cSize) { + _isClauseOn.resize(cSize, false); + } + _isClauseOn[cid] = false; +} + +void ItpMgr::mapVar2Net(const Var &var, CirGate *net) { _var2Net[var] = net; } + +CirGate *ItpMgr::getItp() const { + assert(_ptrMinisat); + // assert(_ptrMinisat->getProof()); + + string proofName = "socv_proof.itp"; + // remove proof log if exist + ifstream logFile(proofName.c_str()); + if (logFile.good()) { + string rmCmd = "rm " + proofName + " -f"; + system(rmCmd.c_str()); + } + + // save proof log + /*_ptrMinisat->getProof()->save(proofName.c_str());*/ + _ptrMinisat->getProof()->save(proofName.c_str()); + + // bulding ITP + // GVNetId netId = buildItp(proofName); + CirGate *gateId = buildItp(proofName); + + // delete proof log + unlink(proofName.c_str()); + + return gateId; +} + +vector ItpMgr::getUNSATCore() const { + assert(_ptrMinisat); + // assert(_ptrMinisat->getProof()); + + vector unsatCore; + unsatCore.clear(); + + // save proof log + string proofName = "socv_proof.itp"; + _ptrMinisat->getProof()->save(proofName.c_str()); + + // generate unsat core + Reader rdr; + rdr.open(proofName.c_str()); + retrieveProof(rdr, unsatCore); + + // delete proof log + unlink(proofName.c_str()); + + return unsatCore; +} + +void ItpMgr::retrieveProof(Reader &rdr, vector &unsatCore) const { + unsigned int tmp, cid, idx, tmp_cid; + + // Clear all + vector clausePos; + clausePos.clear(); + unsatCore.clear(); + + // Generate clausePos + assert(!rdr.null()); + rdr.seek(0); + for (unsigned int pos = 0; (tmp = rdr.get64()) != RDR_EOF; pos = rdr.Current_Pos()) { + cid = clausePos.size(); + clausePos.push_back(pos); + if ((tmp & 1) == 0) { // root clause + while ((tmp = rdr.get64()) != 0) { + } + } else { // learnt clause + idx = 0; + while ((tmp = rdr.get64()) != 0) { + idx = 1; + } + if (idx == 0) clausePos.pop_back(); // Clause Deleted + } + } + + // Generate unsatCore + priority_queue clause_queue; + vector in_queue; + in_queue.resize(clausePos.size()); + for (unsigned int i = 0; i < in_queue.size(); ++i) in_queue[i] = false; + in_queue[in_queue.size() - 1] = true; + clause_queue.push(clausePos.size() - 1); // Push leaf (empty) clause + while (clause_queue.size() != 0) { + cid = clause_queue.top(); + clause_queue.pop(); + + rdr.seek(clausePos[cid]); + + tmp = rdr.get64(); + if ((tmp & 1) == 0) { + // root clause + vec lits; + idx = tmp >> 1; + lits.push(gvToLit(idx)); + while (_varGroup[idx >> 1] != COMMON) { + tmp = rdr.get64(); + if (tmp == 0) break; + idx += tmp; + lits.push(gvToLit(idx)); + } + unsatCore.push_back(Clause(false, lits)); + } else { + // derived clause + tmp_cid = cid - (tmp >> 1); + if (!in_queue[tmp_cid]) { + in_queue[tmp_cid] = true; + clause_queue.push(tmp_cid); + } + while (1) { + tmp = rdr.get64(); + if (tmp == 0) break; + tmp_cid = cid - rdr.get64(); + if (!in_queue[tmp_cid]) { + in_queue[tmp_cid] = true; + clause_queue.push(tmp_cid); + } + } + } + } +} + +void ItpMgr::retrieveProof(Reader &rdr, vector &clausePos, vector &usedClause) const { + unsigned int tmp, cid, idx, tmp_cid, root_cid; + + // Clear all + clausePos.clear(); + usedClause.clear(); + _varGroup.clear(); + /*_varGroup.resize(_ptrMinisat->_solver->nVars(), NONE);*/ + _varGroup.resize(_ptrMinisat->nVars(), NONE); + _isClaOnDup.clear(); + assert((int)_isClauseOn.size() == getNumClauses()); + + // Generate clausePos && varGroup + assert(!rdr.null()); + rdr.seek(0); + root_cid = 0; + for (unsigned int pos = 0; (tmp = rdr.get64()) != RDR_EOF; pos = rdr.Current_Pos()) { + cid = clausePos.size(); + clausePos.push_back(pos); + if ((tmp & 1) == 0) { + // Root Clause + _isClaOnDup.push_back(_isClauseOn[root_cid]); + idx = tmp >> 1; + if (_isClauseOn[root_cid]) { + if (_varGroup[idx >> 1] == NONE) + _varGroup[idx >> 1] = LOCAL_ON; + else if (_varGroup[idx >> 1] == LOCAL_OFF) + _varGroup[idx >> 1] = COMMON; + } else { + if (_varGroup[idx >> 1] == NONE) + _varGroup[idx >> 1] = LOCAL_OFF; + else if (_varGroup[idx >> 1] == LOCAL_ON) + _varGroup[idx >> 1] = COMMON; + } + while (1) { + tmp = rdr.get64(); + if (tmp == 0) break; + idx += tmp; + if (_isClauseOn[root_cid]) { + if (_varGroup[idx >> 1] == NONE) + _varGroup[idx >> 1] = LOCAL_ON; + else if (_varGroup[idx >> 1] == LOCAL_OFF) + _varGroup[idx >> 1] = COMMON; + } else { + if (_varGroup[idx >> 1] == NONE) + _varGroup[idx >> 1] = LOCAL_OFF; + else if (_varGroup[idx >> 1] == LOCAL_ON) + _varGroup[idx >> 1] = COMMON; + } + } + ++root_cid; + } else { + _isClaOnDup.push_back(false); + idx = 0; + while (1) { + tmp = rdr.get64(); + if (tmp == 0) break; + idx = 1; + tmp = rdr.get64(); + } + if (idx == 0) { + clausePos.pop_back(); // Clause Deleted + _isClaOnDup.pop_back(); // Clause Deleted + } + } + } + + // Generate usedClause + priority_queue clause_queue; + vector in_queue; + in_queue.resize(clausePos.size()); + for (unsigned int i = 0; i < in_queue.size(); ++i) in_queue[i] = false; + in_queue[in_queue.size() - 1] = true; + clause_queue.push(clausePos.size() - 1); // Push root empty clause + while (clause_queue.size() != 0) { + cid = clause_queue.top(); + clause_queue.pop(); + + rdr.seek(clausePos[cid]); + + tmp = rdr.get64(); + if ((tmp & 1) == 0) continue; // root clause + + // else, derived clause + tmp_cid = cid - (tmp >> 1); + if (!in_queue[tmp_cid]) { + in_queue[tmp_cid] = true; + clause_queue.push(tmp_cid); + } + while (1) { + tmp = rdr.get64(); + if (tmp == 0) break; + tmp_cid = cid - rdr.get64(); + if (!in_queue[tmp_cid]) { + in_queue[tmp_cid] = true; + clause_queue.push(tmp_cid); + } + } + } + for (unsigned int i = 0; i < in_queue.size(); ++i) { + if (in_queue[i]) { + usedClause.push_back(i); + } + } +} + +CirGate *ItpMgr::buildInitState() const { + // TODO: build initial state + CirAigGate *I; + return I; +} + +// build the McMillan Interpolant +CirGate *ItpMgr::buildItp(const string &proofName) const { + Reader rdr; + // records + map claItpLookup; + vector clausePos; + vector usedClause; + // ntk + uint32_t netSize = _cirMgr->getNumTots(); + // temperate variables + CirGate *nId; + CirGate *nId1; + CirGate *nId2; + int i, cid, tmp, idx, tmp_cid; + // const 1 & const 0 + CirGate *CONST0 = _cirMgr->_const0; + CirGate *CONST1 = _cirMgr->_const1; + + rdr.open(proofName.c_str()); + retrieveProof(rdr, clausePos, usedClause); + + for (i = 0; i < (int)usedClause.size(); i++) { + cid = usedClause[i]; + rdr.seek(clausePos[cid]); + tmp = rdr.get64(); + if ((tmp & 1) == 0) { + // Root Clause + if (_isClaOnDup[cid]) { + idx = tmp >> 1; + while (_varGroup[idx >> 1] != COMMON) { + tmp = rdr.get64(); + if (tmp == 0) break; + idx += tmp; + } + if (_varGroup[idx >> 1] == COMMON) { + assert(_var2Net.find(idx >> 1) != _var2Net.end()); + nId = (_var2Net.find(idx >> 1))->second; + nId1 = (_var2Net.find(idx >> 1))->second; + if ((idx & 1) == 1) nId1 = _cirMgr->createNotGate(nId1); + if ((idx & 1) == 1) nId = _cirMgr->createNotGate(nId); + while (1) { + tmp = rdr.get64(); + if (tmp == 0) break; + idx += tmp; + if (_varGroup[idx >> 1] == COMMON) { + assert(_var2Net.find(idx >> 1) != _var2Net.end()); + nId2 = (_var2Net.find(idx >> 1))->second; + if ((idx & 1) == 1) nId2 = _cirMgr->createNotGate(nId2); + nId = _cirMgr->createOrGate(nId1, nId2); + nId1 = nId; + } + } + } else { + nId = CONST0; + } + claItpLookup[cid] = nId; + } else { + claItpLookup[cid] = CONST1; + } + } else { + // Derived Clause + tmp_cid = cid - (tmp >> 1); + assert(claItpLookup.find(tmp_cid) != claItpLookup.end()); + nId = (claItpLookup.find(tmp_cid))->second; + nId1 = (claItpLookup.find(tmp_cid))->second; + while (1) { + idx = rdr.get64(); + if (idx == 0) break; + idx--; + // Var is idx + tmp_cid = cid - rdr.get64(); + assert(claItpLookup.find(tmp_cid) != claItpLookup.end()); + nId2 = (claItpLookup.find(tmp_cid))->second; + if (nId1 != nId2) { + if (_varGroup[idx] == LOCAL_ON) { // Local to A. Build OR Gate. + if (nId1 == CONST1 || nId2 == CONST1) { + nId = CONST1; + nId1 = nId; + } else if (nId1 == CONST0) { + nId = nId2; + nId1 = nId; + } else if (nId2 == CONST0) { + nId = nId1; + nId1 = nId; + } else { + // or + nId = _cirMgr->createOrGate(nId1, nId2); + nId1 = nId; + } + } else { // Build AND Gate. + if (nId1 == CONST0 || nId2 == CONST0) { + nId = CONST0; + nId1 = nId; + } else if (nId1 == CONST1) { + nId = nId2; + nId1 = nId; + } else if (nId2 == CONST1) { + nId = nId1; + nId1 = nId; + } else { + // and + nId = _cirMgr->createAndGate(nId1, nId2); + nId1 = nId; + } + } + } + } + claItpLookup[cid] = nId; + } + } + + cid = usedClause[usedClause.size() - 1]; + nId = claItpLookup[cid]; + + /*_ptrMinisat->resizeNtkData(_cirMgr->getNumTots() - netSize); // resize Solver data to ntk size*/ + + return nId; +} + +void SatProofRes::reportResult(const string &name) const { + // Report Verification Result + cout << endl; + if (isProved()) { + cout << "Monitor \"" << name << "\" is safe." << endl; + } else if (isFired()) { + cout << "Monitor \"" << name << "\" is violated." << endl; + } else { + cout << "UNDECIDED at depth = " << _maxDepth << endl; + } +} + +void SatProofRes::reportCex(const CirGate *monitor, const CirMgr *const _cirMgr) const { + assert(_satSolver != 0); + + // Output Pattern Value (PI + PIO) + GVBitVecX dataValue; + for (uint32_t i = 0; i <= _fired; ++i) { + cout << i << ": "; + for (int j = _cirMgr->getNumPIs() - 1; j >= 0; --j) { + if (_satSolver->existVerifyData(_cirMgr->getPi(j), i)) { + dataValue = _satSolver->getDataValue(_cirMgr->getPi(j), i); + cout << dataValue[0]; + } else { + cout << 'x'; + } + } + cout << endl; + assert(_satSolver->existVerifyData(monitor, i)); + } +} + +} // namespace itp +} // namespace gv diff --git a/src/itp/itpMgr.h b/src/itp/itpMgr.h new file mode 100644 index 00000000..32e2bab3 --- /dev/null +++ b/src/itp/itpMgr.h @@ -0,0 +1,126 @@ +/**************************************************************************** + FileName [ itpMgr.h ] + PackageName [ itp ] + Synopsis [ Define sat prove package interface ] + Author [ ] + Copyright [ Copyright(c) 2023-present DVLab, GIEE, NTU, Taiwan ] + ****************************************************************************/ +#pragma once + +#include + +#include +#include +#include +#include + +#include "cirGate.h" +#include "cirMgr.h" +#include "minisat/reader.h" +#include "minisatMgr.h" +#include "satMgr.h" + +class GVNetId; +typedef int ClauseId; + +enum VAR_GROUP { + LOCAL_ON, + LOCAL_OFF, + COMMON, + NONE +}; + +namespace gv { +namespace itp { + +class SatProofRes { +public: + SatProofRes(gv::sat::SatSolverMgr* s = 0) : _proved(UINT_MAX), _fired(UINT_MAX), _maxDepth(UINT_MAX), _satSolver(s) {} + + void setProved(size_t i) { _proved = i; } + void setFired(size_t i) { _fired = i; } + + bool isProved() const { return (_proved != UINT_MAX); } + bool isFired() const { return (_fired != UINT_MAX); } + + void setMaxDepth(size_t d) { _maxDepth = d; } + size_t getMaxDepth() const { return _maxDepth; } + + /*void setSatSolver(gv::sat::MinisatMgr* s) { _satSolver = s; }*/ + void setSatSolver(gv::sat::SatSolverMgr* s) { _satSolver = s; } + /*gv::sat::MinisatMgr* getSatSolver() const { return _satSolver; }*/ + gv::sat::SatSolverMgr* getSatSolver() const { return _satSolver; } + + void reportResult(const string&) const; + void reportCex(const gv::cir::CirGate*, const gv::cir::CirMgr* const) const; + +private: + size_t _proved; + size_t _fired; + size_t _maxDepth; // maximum proof depth + /*gv::sat::MinisatMgr* _satSolver;*/ + gv::sat::SatSolverMgr* _satSolver; +}; +} // namespace itp +} // namespace gv + +namespace gv { +namespace itp { + +class ItpMgr { +public: + ItpMgr() : _ptrMinisat(NULL), _cirMgr(NULL) { reset(); } + ~ItpMgr() { reset(); } + + // entry point for SoCV SAT property checking + void verifyPropertyItp(const string& name, const gv::cir::CirGate* monitor); + void verifyPropertyBmc(const string& name, const gv::cir::CirGate* monitor); + // Various proof engines + void indBmc(const gv::cir::CirGate*, SatProofRes&); + void itpUbmc(const gv::cir::CirGate*, SatProofRes&); + + // bind with a solver to get proof info. + void bind(gv::sat::SatSolverMgr* ptrMinisat); + // clear data members + void reset(); + // mark onset/offset clause + void markOnsetClause(const ClauseId& cid); + void markOffsetClause(const ClauseId& cid); + // map var to V3Net (PPI) + void mapVar2Net(const Var& var, gv::cir::CirGate* net); + // please be sure that you call these function right after a UNSAT solving + // GVNetId getItp() const; + gv::cir::CirGate* getItp() const; + vector getUNSATCore() const; + // get number of clauses (the latest clause id + 1) + int getNumClauses() const { return _ptrMinisat->getNumClauses(); } + + // self define helper function + void markSet(bool onORoff, ClauseId& currClause); + bool startSatSolver(gv::sat::SatSolverMgr* GVSatSolver); + void buildMiter(gv::sat::SatSolverMgr* GVSatSolver, GVNetId& R_, GVNetId& R, int& orgNtkSize); + +private: + // helper functions to get proof info. + // GVNetId buildInitState() const; + gv::cir::CirGate* buildInitState() const; + // GVNetId buildItp(const string& proofName) const; + gv::cir::CirGate* buildItp(const string& proofName) const; + void retrieveProof(Reader& rdr, vector& clausePos, vector& usedClause) const; + void retrieveProof(Reader& rdr, vector& unsatCore) const; + + // GV minisat interface for model checking + gv::sat::SatSolverMgr* _ptrMinisat; + // The duplicated Cir + gv::cir::CirMgr* _cirMgr; + + // to handle interpolation + map _var2Net; // mapping common variables to net + vector _isClauseOn; // record onset clauses + // will be determined in retrieveProof, you don't need to take care about this! + mutable vector _isClaOnDup; // duplication & extension of _isClauseOn + mutable vector _varGroup; // mapping var to different groups +}; + +} // namespace itp +} // namespace gv diff --git a/src/prove/proveBdd.cpp b/src/prove/proveBdd.cpp new file mode 100644 index 00000000..f5bb59ec --- /dev/null +++ b/src/prove/proveBdd.cpp @@ -0,0 +1,69 @@ +/**************************************************************************** + FileName [ proveBdd.cpp ] + PackageName [ prove ] + Synopsis [ For BDD-based verification ] + Author [ ] + Copyright [ Copyright(c) 2023-present DVLab, GIEE, NTU, Taiwan ] +****************************************************************************/ + +#include "bddMgrV.h" +#include "gvMsg.h" +// #include "gvNtk.h" +#include +#include +#include + +#include "cirGate.h" +#include "cirMgr.h" +#include "util.h" + +void BddMgrV::buildPInitialState() { + // TODO : remember to set _initState + // set initial state to all zero +} + +void BddMgrV::buildPTransRelation() { + // TODO : remember to set _tr, _tri +} + +BddNodeV BddMgrV::restrict(const BddNodeV& f, const BddNodeV& g) { + if (g == BddNodeV::_zero) { + cout << "Error in restrict!!" << endl; + } + if (g == BddNodeV::_one) { + return f; + } + if (f == BddNodeV::_zero || f == BddNodeV::_one) { + return f; + } + unsigned a = g.getLevel(); + if (g.getLeftCofactor(a) == BddNodeV::_zero) { + return restrict(f.getRightCofactor(a), g.getRightCofactor(a)); + } + if (g.getRightCofactor(a) == BddNodeV::_zero) { + return restrict(f.getLeftCofactor(a), g.getLeftCofactor(a)); + } + if (f.getLeftCofactor(a) == f.getRightCofactor(a)) { + return restrict(f, g.getLeftCofactor(a) | g.getRightCofactor(a)); + } + BddNodeV newNode = + (~getSupport(a)& restrict(f.getRightCofactor(a), + g.getRightCofactor(a))) | + (getSupport(a)& restrict(f.getLeftCofactor(a), g.getLeftCofactor(a))); + return newNode; +} + +void BddMgrV::buildPImage(int level) { + // TODO : remember to add _reachStates and set _isFixed + // note:: _reachStates record the set of reachable states +} + +void BddMgrV::runPCheckProperty(const string& name, BddNodeV monitor) { + // TODO : prove the correctness of AG(~monitor) +} + +BddNodeV +BddMgrV::find_ns(BddNodeV cs) {} + +BddNodeV +BddMgrV::ns_to_cs(BddNodeV ns) {} diff --git a/src/prove/proveCmd.cpp b/src/prove/proveCmd.cpp new file mode 100644 index 00000000..8f7595bc --- /dev/null +++ b/src/prove/proveCmd.cpp @@ -0,0 +1,230 @@ +/**************************************************************************** + FileName [ proveCmd.cpp ] + PackageName [ prove ] + Synopsis [ Define basic prove package commands ] + Author [ ] + Copyright [ Copyright(c) 2023-present DVLab, GIEE, NTU, Taiwan ] + ****************************************************************************/ + +#include "proveCmd.h" + +#include +#include + +#include "bddMgrV.h" +#include "cirGate.h" +#include "cirMgr.h" +#include "gvMsg.h" +#include "util.h" + +using namespace std; + +bool initProveCmd() { + return (gvCmdMgr->regCmd("PINITialstate", 5, new PInitialStateCmd) && + gvCmdMgr->regCmd("PTRansrelation", 3, new PTransRelationCmd) && + gvCmdMgr->regCmd("PIMAGe", 5, new PImageCmd) && + gvCmdMgr->regCmd("PCHECKProperty", 7, new PCheckPropertyCmd)); +} + +extern BddNodeV getBddNodeV(const string& bddName); + +//---------------------------------------------------------------------- +// PINITialstate [(string varName)] +//---------------------------------------------------------------------- +GVCmdExecStatus +PInitialStateCmd::exec(const string& option) { + vector options; + GVCmdExec::lexOptions(option, options); + if (options.size() > 1) { + return GVCmdExec::errorOption(GV_CMD_OPT_EXTRA, options[1]); + } + string token = ""; + if (options.size()) { + if (!isValidVarName(options[0])) + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[0]); + else token = options[0]; + } + + bddMgrV->buildPInitialState(); + if (!token.empty() && + !bddMgrV->addBddNodeV(token, bddMgrV->getPInitState()())) { + gvMsg(GV_MSG_ERR) + << "\"" << token + << "\" has Already been Associated With Another BddNode!!" << endl; + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, token); + } + return GV_CMD_EXEC_DONE; +} + +void PInitialStateCmd::usage(const bool& verbose) const { + cout << "Usage: PINITialstate [(string varName)]" << endl; +} + +void PInitialStateCmd::help() const { + cout << setw(20) << left << "PINITialstate: " + << "Set initial state BDD" << endl; +} + +//---------------------------------------------------------------------- +// PTRansrelation [(string triName)] [(string trName)] +//---------------------------------------------------------------------- +GVCmdExecStatus +PTransRelationCmd::exec(const string& option) { + size_t op = 0; + vector options; + GVCmdExec::lexOptions(option, options); + if (options.size() > 2) + return GVCmdExec::errorOption(GV_CMD_OPT_EXTRA, options[2]); + + string triName, trName; + if (op < options.size()) { + triName = options[op++]; + if (!isValidVarName(triName)) + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, triName); + } + if (op < options.size()) { + trName = options[op++]; + if (!isValidVarName(trName)) + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, trName); + } + bddMgrV->buildPTransRelation(); + if (!triName.empty() && + !bddMgrV->addBddNodeV(triName, bddMgrV->getPTri()())) { + gvMsg(GV_MSG_ERR) + << "\"" << triName + << "\" has Already been Associated With Another BddNode!!" << endl; + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, triName); + } + if (!trName.empty() && !bddMgrV->addBddNodeV(trName, bddMgrV->getPTr()())) { + gvMsg(GV_MSG_ERR) + << "\"" << trName + << "\" has Already been Associated With Another BddNode!!" << endl; + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, trName); + } + return GV_CMD_EXEC_DONE; +} + +void PTransRelationCmd::usage(const bool& verbose) const { + cout + << "Usage: PTRansrelation [(string triName)] [(stirng trName)]" << endl; +} + +void PTransRelationCmd::help() const { + cout << setw(20) << left << "PTRansrelation: " + << "build the transition relationship in BDDs" << endl; +} + +//---------------------------------------------------------------------- +// PIMAGe [-Next <(int numTimeframes)>] [(string varName)] +//---------------------------------------------------------------------- +GVCmdExecStatus +PImageCmd::exec(const string& option) { + if (bddMgrV->getPInitState()() == 0) { + gvMsg(GV_MSG_ERR) << "BDD of Initial State is Not Yet Constructed !!!" + << endl; + return GV_CMD_EXEC_ERROR; + } else if (bddMgrV->getPTr()() == 0) { + gvMsg(GV_MSG_ERR) + << "BDD of Transition Relation is Not Yet Constructed !!!" << endl; + return GV_CMD_EXEC_ERROR; + } + + int level = 1; + string name; + vector options; + GVCmdExec::lexOptions(option, options); + + for (size_t i = 0, n = options.size(); i < n; ++i) + if (!myStrNCmp("-Next", options[i], 2)) + if (++i < n) { + if (!myStr2Int(options[i], level) || level <= 0) + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, + options[i]); + } else + return GVCmdExec::errorOption(GV_CMD_OPT_MISSING, + options[i - 1]); + else if (name.empty()) { + name = options[i]; + if (!isValidVarName(name)) + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, name); + } else return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[i]); + bddMgrV->buildPImage(level); + if (!name.empty()) + bddMgrV->forceAddBddNodeV(name, bddMgrV->getPReachState()()); + return GV_CMD_EXEC_DONE; +} + +void PImageCmd::usage(const bool& verbose) const { + cout + << "Usage: PIMAGe [-Next <(int numTimeframes)>] [(string varName)]" + << endl; +} + +void PImageCmd::help() const { + cout << setw(20) << left << "PIMAGe: " + << "build the next state images in BDDs" << endl; +} + +//---------------------------------------------------------------------- +// PCHECKProperty < -Netid | -Output > > +//---------------------------------------------------------------------- +GVCmdExecStatus +PCheckPropertyCmd::exec(const string& option) { + if (bddMgrV->getPReachState()() == 0) { + gvMsg(GV_MSG_ERR) << "BDD of Reached State is Not Yet Constructed !!!" + << endl; + return GV_CMD_EXEC_ERROR; + } + + vector options; + GVCmdExec::lexOptions(option, options); + + if (options.size() < 2) + return GVCmdExec::errorOption(GV_CMD_OPT_MISSING, ""); + if (options.size() > 2) + return GVCmdExec::errorOption(GV_CMD_OPT_EXTRA, options[2]); + + bool isNet = false; + + if (!myStrNCmp("-Netid", options[0], 2)) isNet = true; + else if (!myStrNCmp("-Output", options[0], 2)) isNet = false; + else return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[0]); + + int num = 0; + if (!myStr2Int(options[1], num) || (num < 0)) + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[1]); + if (isNet) { + if ((unsigned)num >= cirMgr->getNumTots()) { + gvMsg(GV_MSG_ERR) << "Net with Id " << num + << " does NOT Exist in Current Ntk !!" << endl; + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[1]); + } + // netId = GVNetId::makeNetId(num); + } else { + if ((unsigned)num >= cirMgr->getNumPOs()) { + gvMsg(GV_MSG_ERR) << "Output with Index " << num + << " does NOT Exist in Current Ntk !!" << endl; + return GVCmdExec::errorOption(GV_CMD_OPT_ILLEGAL, options[1]); + } + // netId = gvNtkMgr->getOutput(num); + } + + // BddNodeV monitor = bddMgrV->getBddNodeV(netId.id); + BddNodeV monitor = bddMgrV->getBddNodeV(cirMgr->getPo(num)->getGid()); + assert(monitor()); + // bddMgrV->runPCheckProperty(gvNtkMgr->getNetNameFromId(netId.id), monitor); + string mStr = "monitor"; + bddMgrV->runPCheckProperty(cirMgr->getPo(num)->getName(), monitor); + + return GV_CMD_EXEC_DONE; +} + +void PCheckPropertyCmd::usage(const bool& verbose) const { + cout << "Usage: PCHECKProperty < -Netid | -Output >" + << endl; +} + +void PCheckPropertyCmd::help() const { + cout << setw(20) << left << "PCHECKProperty:" + << "check the monitor by BDDs" << endl; +} diff --git a/src/prove/proveCmd.h b/src/prove/proveCmd.h new file mode 100644 index 00000000..bc92fb76 --- /dev/null +++ b/src/prove/proveCmd.h @@ -0,0 +1,19 @@ +/**************************************************************************** + FileName [ proveCmd.h ] + PackageName [ prove ] + Synopsis [ Define basic prove package commands ] + Author [ ] + Copyright [ Copyright(c) 2023-present DVLab, GIEE, NTU, Taiwan ] +****************************************************************************/ + +#pragma once + +#include "gvCmdMgr.h" + +// ============================================================================ +// Classes for Prove package commands +// ============================================================================ +GV_COMMAND(PInitialStateCmd, GV_CMD_TYPE_PROVE); +GV_COMMAND(PTransRelationCmd, GV_CMD_TYPE_PROVE); +GV_COMMAND(PImageCmd, GV_CMD_TYPE_PROVE); +GV_COMMAND(PCheckPropertyCmd, GV_CMD_TYPE_PROVE);