Option to disable verific VHDL support

2 files changed, 45 insertions, 11 deletions

diff --git a/frontends/verific/Makefile.inc b/frontends/verific/Makefile.inc
index 972f4f9f1..c82428613 100644
--- a/frontends/verific/Makefile.inc
+++ b/frontends/verific/Makefile.inc
@@ -10,9 +10,11 @@ EXTRA_TARGETS += share/verific
 share/verific:
 	$(P) rm -rf share/verific.new
 	$(Q) mkdir -p share/verific.new
+ifneq ($(DISABLE_VERIFIC_VHDL),1)
 	$(Q) cp -r $(VERIFIC_DIR)/vhdl_packages/vdbs_1987/. share/verific.new/vhdl_vdbs_1987
 	$(Q) cp -r $(VERIFIC_DIR)/vhdl_packages/vdbs_1993/. share/verific.new/vhdl_vdbs_1993
 	$(Q) cp -r $(VERIFIC_DIR)/vhdl_packages/vdbs_2008/. share/verific.new/vhdl_vdbs_2008
+endif
 	$(Q) chmod -R a+rX share/verific.new
 	$(Q) mv share/verific.new share/verific
 
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index fcacbd086..a265dc8b4 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -43,13 +43,16 @@ USING_YOSYS_NAMESPACE
 #endif
 
 #include "veri_file.h"
-#include "vhdl_file.h"
 #include "hier_tree.h"
 #include "VeriModule.h"
 #include "VeriWrite.h"
-#include "VhdlUnits.h"
 #include "VeriLibrary.h"
 
+#ifdef VERIFIC_VHDL_SUPPORT
+#include "vhdl_file.h"
+#include "VhdlUnits.h"
+#endif
+
 #ifdef YOSYSHQ_VERIFIC_EXTENSIONS
 #include "InitialAssertions.h"
 #endif
@@ -175,8 +178,10 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att
 			return;
 		if (!type_range->IsTypeEnum())
 			return;
+#ifdef VERIFIC_VHDL_SUPPORT
 		if (nl->IsFromVhdl() && strcmp(type_range->GetTypeName(), "STD_LOGIC") == 0)
 			return;
+#endif
 		auto type_name = type_range->GetTypeName();
 		if (!type_name)
 			return;
@@ -202,6 +207,7 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att
 					log_error("Expected TypeRange value '%s' to be of form <decimal>'b<binary>.\n", v);
 				attributes.emplace(stringf("\\enum_value_%s", p+2), RTLIL::escape_id(k));
 			}
+#ifdef VERIFIC_VHDL_SUPPORT
 			else if (nl->IsFromVhdl()) {
 				// Expect "<binary>" or plain <binary>
 				auto p = v;
@@ -237,6 +243,7 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att
 				if (p == nullptr)
 					log_error("Expected TypeRange value '%s' to be of form \"<binary>\" or <binary>.\n", v);
 			}
+#endif
 		}
 	}
 }
@@ -2042,11 +2049,13 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
 
 	std::set<Netlist*> nl_todo, nl_done;
 
-	VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
 	VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
 	Array *netlists = NULL;
 	Array veri_libs, vhdl_libs;
+#ifdef VERIFIC_VHDL_SUPPORT
+	VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
 	if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
+#endif
 	if (veri_lib) veri_libs.InsertLast(veri_lib);
 
 	Map verific_params(STRING_HASH);
@@ -2077,12 +2086,13 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
 			}
 		}
 
+#ifdef VERIFIC_VHDL_SUPPORT
 		if (vhdl_lib) {
 			VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(top.c_str());
 			if (vhdl_unit)
 				vhdl_units.InsertLast(vhdl_unit);
 		}
-
+#endif
 		netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &verific_params);
 	}
 
@@ -2119,7 +2129,9 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
 	}
 
 	veri_file::Reset();
+#ifdef VERIFIC_VHDL_SUPPORT
 	vhdl_file::Reset();
+#endif
 	Libset::Reset();
 	verific_incdirs.clear();
 	verific_libdirs.clear();
@@ -2170,11 +2182,13 @@ struct VerificPass : public Pass {
 		log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
 		log("\n");
 		log("\n");
+#ifdef VERIFIC_VHDL_SUPPORT
 		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
 		log("\n");
 		log("Load the specified VHDL files into Verific.\n");
 		log("\n");
 		log("\n");
+#endif
 		log("    verific {-f|-F} <command-file>\n");
 		log("\n");
 		log("Load and execute the specified command file.\n");
@@ -2408,17 +2422,18 @@ struct VerificPass : public Pass {
 			RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
 			RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
 
+#ifdef VERIFIC_VHDL_SUPPORT
 			RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
 			RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
 
 			RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
 			RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
 
-			RuntimeFlags::SetVar("veri_preserve_assignments", 1);
 			RuntimeFlags::SetVar("vhdl_preserve_assignments", 1);
-
-			RuntimeFlags::SetVar("veri_preserve_comments",1);
 			//RuntimeFlags::SetVar("vhdl_preserve_comments",1);
+#endif
+			RuntimeFlags::SetVar("veri_preserve_assignments", 1);
+			RuntimeFlags::SetVar("veri_preserve_comments",1);
 
 			// Workaround for VIPER #13851
 			RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
@@ -2600,6 +2615,7 @@ struct VerificPass : public Pass {
 			goto check_error;
 		}
 
+#ifdef VERIFIC_VHDL_SUPPORT
 		if (GetSize(args) > argidx && args[argidx] == "-vhdl87") {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
 			for (argidx++; argidx < GetSize(args); argidx++)
@@ -2635,6 +2651,7 @@ struct VerificPass : public Pass {
 			verific_import_pending = true;
 			goto check_error;
 		}
+#endif
 
 #ifdef YOSYSHQ_VERIFIC_FORMALAPPS
 		if (argidx < GetSize(args) && args[argidx] == "-app")
@@ -2737,10 +2754,12 @@ struct VerificPass : public Pass {
 			const char* module = nullptr;
 			bool mode_vhdl = false;
 			for (argidx++; argidx < GetSize(args); argidx++) {
+#ifdef VERIFIC_VHDL_SUPPORT
 				if (args[argidx] == "-vhdl") {
 					mode_vhdl = true;
 					continue;
 				}
+#endif
 				if (args[argidx] == "-verilog") {
 					mode_vhdl = false;
 					continue;
@@ -2767,7 +2786,11 @@ struct VerificPass : public Pass {
 				log_cmd_error("Filname must be specified.\n");
 
 			if (mode_vhdl)
+#ifdef VERIFIC_VHDL_SUPPORT
 				vhdl_file::PrettyPrint(filename, module, work.c_str());
+#else
+				goto check_error;
+#endif
 			else
 				veri_file::PrettyPrint(filename, module, work.c_str());
 			goto check_error;
@@ -2949,11 +2972,13 @@ struct VerificPass : public Pass {
 			{
 				log("Running hier_tree::ElaborateAll().\n");
 
-				VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
 				VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
 
 				Array veri_libs, vhdl_libs;
+#ifdef VERIFIC_VHDL_SUPPORT
+				VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
 				if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
+#endif
 				if (veri_lib) veri_libs.InsertLast(veri_lib);
 
 				Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &parameters);
@@ -2970,7 +2995,9 @@ struct VerificPass : public Pass {
 					cmd_error(args, argidx, "No top module specified.\n");
 
 				VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
+#ifdef VERIFIC_VHDL_SUPPORT
 				VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
+#endif
 
 				Array veri_modules, vhdl_units;
 				for (; argidx < GetSize(args); argidx++)
@@ -2984,14 +3011,14 @@ struct VerificPass : public Pass {
 						veri_modules.InsertLast(veri_module);
 						continue;
 					}
-
+#ifdef VERIFIC_VHDL_SUPPORT
 					VhdlDesignUnit *vhdl_unit = vhdl_lib ? vhdl_lib->GetPrimUnit(name) : nullptr;
 					if (vhdl_unit) {
 						log("Adding VHDL unit '%s' to elaboration queue.\n", name);
 						vhdl_units.InsertLast(vhdl_unit);
 						continue;
 					}
-
+#endif
 					log_error("Can't find module/unit '%s'.\n", name);
 				}
 
@@ -3051,7 +3078,9 @@ struct VerificPass : public Pass {
 			}
 
 			veri_file::Reset();
+#ifdef VERIFIC_VHDL_SUPPORT
 			vhdl_file::Reset();
+#endif
 			Libset::Reset();
 			verific_incdirs.clear();
 			verific_libdirs.clear();
@@ -3094,11 +3123,13 @@ struct ReadPass : public Pass {
 		log("the language version (and before file names) to set additional verilog defines.\n");
 		log("\n");
 		log("\n");
+#ifdef VERIFIC_VHDL_SUPPORT
 		log("    read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
 		log("\n");
 		log("Load the specified VHDL files. (Requires Verific.)\n");
 		log("\n");
 		log("\n");
+#endif
 		log("    read {-f|-F} <command-file>\n");
 		log("\n");
 		log("Load and execute the specified command file. (Requires Verific.)\n");
@@ -3181,6 +3212,7 @@ struct ReadPass : public Pass {
 			return;
 		}
 
+#ifdef VERIFIC_VHDL_SUPPORT
 		if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl") {
 			if (use_verific) {
 				args[0] = "verific";
@@ -3190,7 +3222,7 @@ struct ReadPass : public Pass {
 			}
 			return;
 		}
-
+#endif
 		if (args[1] == "-f" || args[1] == "-F") {
 			if (use_verific) {
 				args[0] = "verific";