diff --git a/Makefile b/Makefile index b267f6294..d88a7e95a 100644 --- 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 5a10568c7..1b8bc1b51 100644 --- 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 &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 top_mod_names; +#ifdef YOSYSHQ_VERIFIC_EXTENSIONS InitialAssertions::Rewrite(work, ¶meters); - +#endif if (mode_all) { log("Running hier_tree::ElaborateAll().\n");