Merge pull request #12 from DVLab-NTU/develop

Develop

CMakeLists.txt

@@ -210,7 +210,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)

README.md

@@ -16,7 +16,7 @@ export PATH="$(brew --prefix)/bin:$PATH"
 ```
 - for linux (Ubuntu) :
 ```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 libgmp-dev
 ```

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.
 
-<p align="center">
-<img src="./img/build_flow.png" alt="image" width="500"/>
-</p>
-
 ## Get the Engines source
 
 We utilize ExternalProject_Add to acquire third-party engines since Yosys doesn't currently support CMake.

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 <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
+// template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
 template <class T> static inline bool operator >  (const T& x, const T& y) { return y < x;     }
 template <class T> static inline bool operator <= (const T& x, const T& y) { return !(y < x);  }
 template <class T> static inline bool operator >= (const T& x, const T& y) { return !(x < y);  }

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 {

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;
 }
 

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<GVCmdType> _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<GVCmdType> _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)                  \

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 <cstring>
+#include <iomanip>
+
+#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 <gateId> | -Output <outputIndex> > >
+//----------------------------------------------------------------------
+GVCmdExecStatus
+SATVerifyItpCmd::exec(const string& option) {
+    vector<string> 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 <gateId> | -Output <outputIndex> >" << endl;
+}
+
+void SATVerifyItpCmd::help() const {
+    cout << setw(20) << left << "SATVerify ITP:"
+         << "check the monitor by interpolation-based technique" << endl;
+}
+
+// //----------------------------------------------------------------------
+// //    SATVerify BMC < -GateId <gateId> | -Output <outputIndex> > >
+// //----------------------------------------------------------------------
+GVCmdExecStatus
+SATVerifyBmcCmd::exec(const string& option) {
+    vector<string> 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 <gateId> | -Output < outputIndex >> " << endl;
+}
+
+void SATVerifyBmcCmd::help() const {
+    cout << setw(20) << left << "SATVerify BMC:"
+         << "check the monitor by bounded model checking" << endl;
+}

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);