Make Verific extensions optional

diff --git a/Makefile b/Makefile
index b267f62944c76dff2e2745505e34e193850576df..d88a7e95a46c4062029a6b3195897cfafac2e268 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -18,6 +18,7 @@ ENABLE_READLINE := 1
 ENABLE_EDITLINE := 0
 ENABLE_GHDL := 0
 ENABLE_VERIFIC := 0
+DISABLE_VERIFIC_EXTENSIONS := 0
 ENABLE_COVER := 1
 ENABLE_LIBYOSYS := 0
 ENABLE_PROTOBUF := 0
@@ -498,7 +499,11 @@ endif
 
 ifeq ($(ENABLE_VERIFIC),1)
 VERIFIC_DIR ?= /usr/local/src/verific_lib
-VERIFIC_COMPONENTS ?= verilog vhdl database util containers hier_tree extensions
+VERIFIC_COMPONENTS ?= verilog vhdl database util containers hier_tree
+ifneq ($(DISABLE_VERIFIC_EXTENSIONS),1)
+VERIFIC_COMPONENTS += extensions
+CXXFLAGS += -DYOSYSHQ_VERIFIC_EXTENSIONS
+endif
 CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABLE_VERIFIC
 ifeq ($(OS), Darwin)
 LDLIBS += $(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)) -lz

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 5a10568c7aae41eb976decdbcc7d0edb374f42ee..1b8bc1b5124d050d229e664ef9a85c27ab9019f0 100644 (file)
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -50,7 +50,9 @@ USING_YOSYS_NAMESPACE
 #include "VhdlUnits.h"
 #include "VeriLibrary.h"
 
+#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
 #include "InitialAssertions.h"
+#endif
 
 #ifndef YOSYSHQ_VERIFIC_API_VERSION
 #  error "Only YosysHQ flavored Verific is supported. Please contact office@yosyshq.com for commercial support for Yosys+Verific."
@@ -1961,7 +1963,9 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
        for (const auto &i : parameters)
                verific_params.Insert(i.first.c_str(), i.second.c_str());
 
+#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
        InitialAssertions::Rewrite("work", &verific_params);
+#endif
 
        if (top.empty()) {
                netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
@@ -2847,8 +2851,9 @@ struct VerificPass : public Pass {
 
                        std::set<std::string> top_mod_names;
 
+#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
                        InitialAssertions::Rewrite(work, &parameters);
-
+#endif
                        if (mode_all)
                        {
                                log("Running hier_tree::ElaborateAll().\n");