Update Refinement Handling in Verilog Verification Target Generation

.github/workflows/cmake.yml

@@ -13,7 +13,7 @@ jobs:
     - uses: actions/checkout@v2
 
     - name: Install Dependent Packages
-      run: sudo apt install bison flex z3 libz3-dev
+      run: sudo apt install bison flex z3 libz3-dev libfl-dev
 
     - name: Create Build Environment
       run: cmake -E make_directory ${{runner.workspace}}/build

.gitmodules

@@ -7,3 +7,6 @@
 [submodule "extern/smt-switch"]
 	path = extern/smt-switch
 	url = https://github.com/makaimann/smt-switch.git
+[submodule "extern/vexpparser"]
+	path = extern/vexpparser
+	url = https://github.com/zhanghongce/vexpparser.git

.travis.yml

@@ -57,6 +57,7 @@ jobs:
             - bison
             - z3
             - libz3-dev
+            - libfl-dev
             - g++-7
       before_install:
         - echo -n | openssl s_client -connect https://scan.coverity.com:443 | sed -ne '/-BEGIN CERTIFICATE-/,/-END CERTIFICATE-/p' | sudo tee -a /etc/ssl/certs/ca-
@@ -77,6 +78,7 @@ addons:
       - bison
       - z3
       - libz3-dev
+      - libfl-dev
       - g++-7
 
 notifications:

appveyor.yml

@@ -8,7 +8,7 @@ configuration:
 
 install:
 - sudo apt update --yes
-- sudo apt install --yes z3 libz3-dev bison flex gcc g++
+- sudo apt install --yes z3 libz3-dev bison libfl-dev flex gcc g++
 
 build_script:
 - cd $APPVEYOR_BUILD_FOLDER

azure-pipelines.yml

@@ -55,27 +55,6 @@ jobs:
       ./test/unit_tests
     displayName: 'build'
 
-- job: Ubuntu_1604_LTS
-  pool:
-    vmImage: 'ubuntu-16.04'
-  steps:
-  - script: |
-      sudo apt-get update
-      sudo apt-get install bison
-      sudo apt-get install flex
-      sudo apt-get install z3
-      sudo apt-get install libz3-dev
-      sudo apt-get install g++-7   
-    displayName: 'package'
-  - script: |
-      mkdir -p build 
-      cd build
-      cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_COMPILER=g++-7
-      cmake --build .
-      sudo cmake --build . --target install 
-      cmake --build . --target test
-    displayName: 'build'
-
 - job: Ubuntu_1804_LTS
   pool:
     vmImage: 'ubuntu-18.04'
@@ -86,6 +65,7 @@ jobs:
       sudo apt-get install flex
       sudo apt-get install z3
       sudo apt-get install libz3-dev
+      sudo apt-get install libfl-dev
       sudo apt-get install g++-8   
     displayName: 'package'
   - script: |
@@ -118,7 +98,7 @@ jobs:
       cd glog
       md build
       cd build
-      cmake ..
+      cmake ..  -DFLEXLEXER_INCLUDE_PATH=c:\ProgramData\chocolatey\lib\winflexbison3\tools\
       cmake --build . --target install
     displayName: 'glog'
 
@@ -140,11 +120,20 @@ jobs:
       cmake --build . --target install
     displayName: 'vlog-parser'
 
+  - script: |
+      cd extern
+      cd vexpparser
+      md build
+      cd build
+      cmake .. -DFLEXLEXER_INCLUDE_PATH=c:\ProgramData\chocolatey\lib\winflexbison3\tools\
+      cmake --build . --target install
+    displayName: 'vexpparser'
+
   - script: |
       md build
       cd build
       # For building the test, we need CMAKE_MSVC_RUNTIME_LIBRARY (which will be supported in CMake 3.15+)
-      cmake .. -DILANG_BUILD_TEST=OFF -DBUILD_SHARED_LIBS=OFF -DILANG_BUILD_INVSYN=OFF -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe
+      cmake .. -DILANG_BUILD_TEST=OFF -DBUILD_SHARED_LIBS=OFF -DILANG_BUILD_INVSYN=OFF -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe -DFLEXLEXER_INCLUDE_PATH=c:\ProgramData\chocolatey\lib\winflexbison3\tools\
       cmake --build .
       cmake --build . --target install
     displayName: 'build'
@@ -153,7 +142,7 @@ jobs:
       cd starter
       md build
       cd build
-      cmake .. -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe
+      cmake .. -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe -DFLEXLEXER_INCLUDE_PATH=c:\ProgramData\chocolatey\lib\winflexbison3\tools\
       cmake --build . 
     displayName: 'starter'
 

cmake/config.cmake.in

@@ -6,6 +6,7 @@ find_dependency(glog REQUIRED)
 find_dependency(nlohmann_json REQUIRED)
 find_dependency(verilogparser REQUIRED)
 find_dependency(vcdparser REQUIRED)
+find_dependency(vexpparser REQUIRED)
 find_dependency(smtparser REQUIRED)
 find_dependency(fmt REQUIRED)
 find_dependency(Z3 REQUIRED)

extern/CMakeLists.txt

@@ -126,6 +126,39 @@ if(NOT VERILOGPARSER_FOUND)
 endif() # VERILOGPARSER_FOUND
 
 
+# ---------------------------------------------------------------------------- #
+# Verilog Expression Parser
+# 
+#   TARGET vexpparser::vexpparser
+#   SOURCE https://github.com/zhanghongce/vexpparser.git
+#   PATH   extern/vexpparser
+# ---------------------------------------------------------------------------- #
+# find installed package
+find_package(vexpparser 1.1.0 QUIET)
+
+# embed to build tree if not installed
+if(NOT VEXP_PARSER_FOUND)
+
+  # fetch from git
+  if(${ILANG_FETCH_DEPS})
+
+    execute_process(
+      COMMAND ${GIT_EXECUTABLE} submodule update --init vexpparser
+      WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+      RESULT_VARIABLE GIT_SUBMOD_RESULT
+    )
+
+    if(NOT GIT_SUBMOD_RESULT EQUAL "0")
+      message(FATAL_ERROR "Submodule update failed with ${GIT_SUBMOD_RESULT}")
+    endif()
+
+  endif() # ILANG_FETCH_DEPS
+
+  # embedded build
+  add_subdirectory(vexpparser)
+
+endif() # VERILOGPARSER_FOUND
+
 # ---------------------------------------------------------------------------- #
 # Template-based ILA Synthesis
 #

include/ilang/ilang++.h

@@ -16,6 +16,7 @@
 #endif // SMTSWITCH_INTERFACE
 
 #include <ilang/config.h>
+#include <ilang/rtl_verify.h>
 
 /// \namespace ilang
 /// Defines the core data structure and APIs for constructing and storing ILA.
@@ -745,6 +746,28 @@ class IlaZ3Unroller {
 
 }; // class IlaZ3Unroller
 
+
+/// \brief The wrapper of Rtl verification target generator
+class IlaVerilogRefinementChecker {
+
+public:
+  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
+  /// Default constructor
+  IlaVerilogRefinementChecker(
+      const Ila& ila,
+      const std::vector<std::string>& implementation_include_path,
+      const std::vector<std::string>& implementation_srcs,
+      const std::string& implementation_top_module,
+      const std::string& refinement_variable_mapping,
+      const std::string& refinement_conditions, 
+      const std::string& output_path,
+      ModelCheckerSelection backend,
+      const RtlVerifyConfig& vtg_config = RtlVerifyConfig() );
+  /// Default virtual destructor.
+  ~IlaVerilogRefinementChecker() {};
+
+}; // class RtlVerifier
+
 #ifdef SMTSWITCH_INTERFACE
 
 /// \brief Reset the solver and generate the SMT Term (for smt-switch).

include/ilang/rfmap-in/rfexpr_shortcut.h

@@ -0,0 +1,38 @@
+/// \file rfexpr_shortcut.h Refinement map expression
+/// construction
+/// Hongce Zhang ([email protected])
+
+#ifndef ILANG_RFEXPR_SHORTCUT_H__
+#define ILANG_RFEXPR_SHORTCUT_H__
+
+#include <ilang/rfmap-in/rfmap_typecheck.h>
+
+namespace ilang {
+
+rfmap::RfExpr rfmap_reduce_or(const rfmap::RfExpr& in);
+rfmap::RfExpr rfmap_imply(const rfmap::RfExpr& l, const rfmap::RfExpr& r);
+rfmap::RfExpr rfmap_and(const rfmap::RfExpr& l, const rfmap::RfExpr& r);
+rfmap::RfExpr rfmap_or(const rfmap::RfExpr& l, const rfmap::RfExpr& r);
+rfmap::RfExpr rfmap_and(const std::vector<rfmap::RfExpr>& v);
+rfmap::RfExpr rfmap_or(const std::vector<rfmap::RfExpr>& v);
+
+rfmap::RfExpr rfmap_ite(const rfmap::RfExpr& c, const rfmap::RfExpr& l,
+                        const rfmap::RfExpr& r);
+
+rfmap::RfExpr rfmap_eq(const rfmap::RfExpr& l, const rfmap::RfExpr& r);
+rfmap::RfExpr rfmap_le(const rfmap::RfExpr& l, const rfmap::RfExpr& r);
+
+rfmap::RfExpr rfmap_not(const rfmap::RfExpr& l);
+
+rfmap::RfExpr rfmap_true();
+rfmap::RfExpr rfmap_false();
+rfmap::RfExpr rfmap_const(unsigned b, unsigned w, unsigned v);
+/// if it is RTL. or ILA. then will use MakeVar
+/// otherwise will use MakeSpecial
+/// will not determine its type
+/// ReplExpr will determine the type
+rfmap::RfExpr rfmap_var(const std::string& v);
+
+} // namespace ilang
+
+#endif // ILANG_RFEXPR_SHORTCUT_H__

include/ilang/rfmap-in/rfexpr_to_smt.h

@@ -0,0 +1,58 @@
+/// \file rfexpr_to_smt.cc Refinement map to smt-lib2
+/// Hongce Zhang ([email protected])
+
+#ifndef ILANG_RFEXPR_TO_SMT_H__
+#define ILANG_RFEXPR_TO_SMT_H__
+
+#include <ilang/rfmap-in/rfmap_typecheck.h>
+
+namespace ilang {
+namespace rfmap {
+
+struct SmtType : public RfMapVarType {
+  bool bool_or_bv;
+
+  SmtType() : RfMapVarType(1), bool_or_bv(true) {}
+  SmtType(unsigned w) : RfMapVarType(w), bool_or_bv(false) {}
+  SmtType(unsigned a, unsigned d) : RfMapVarType(a, d), bool_or_bv(false) {}
+  SmtType(const RfMapVarType& r, bool request_bool)
+      : RfMapVarType(r), bool_or_bv(request_bool) {}
+
+  bool is_bool() const { return bool_or_bv && (RfMapVarType::is_bv()); }
+  bool is_bv() const { return (!bool_or_bv) && (RfMapVarType::is_bv()); }
+  bool operator==(const SmtType& r) const {
+    if (bool_or_bv != r.bool_or_bv)
+      return false;
+    if (type != r.type)
+      return false;
+    if (type == TYPE::BV)
+      return width == r.width;
+    if (type == TYPE::MEM)
+      return data_width == r.data_width && addr_width == r.addr_width;
+    return false; // unknown type , unknown
+  }               // operator=
+
+  std::string type_to_smt2() const;
+
+}; // SmtType
+
+struct RfExpr2Smt {
+
+public:
+  static std::string to_smt2(const RfExpr& in, SmtType expected_type);
+
+protected:
+  // helper function
+  static std::string
+  to_smt2_const(const std::shared_ptr<verilog_expr::VExprAstConstant>& in,
+                SmtType expected_type);
+  static std::string
+  to_smt2_var(const std::shared_ptr<verilog_expr::VExprAstVar>& in,
+              SmtType expected_type);
+
+}; // struct RfExpr2Smt
+
+} // namespace rfmap
+} // namespace ilang
+
+#endif // ILANG_RFEXPR_TO_SMT_H__