diff --git a/Makefile b/Makefile index 7760cec43..b86eb4bfa 100644 --- a/Makefile +++ b/Makefile @@ -17,10 +17,12 @@ ENABLE_READLINE := 1 ENABLE_EDITLINE := 0 ENABLE_GHDL := 0 ENABLE_VERIFIC := 0 +ENABLE_VERIFIC_SYSTEMVERILOG := 1 +ENABLE_VERIFIC_VHDL := 1 +ENABLE_VERIFIC_HIER_TREE := 1 +ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 1 ENABLE_VERIFIC_EDIF := 0 ENABLE_VERIFIC_LIBERTY := 0 -DISABLE_VERIFIC_EXTENSIONS := 0 -DISABLE_VERIFIC_VHDL := 0 ENABLE_COVER := 1 ENABLE_LIBYOSYS := 0 ENABLE_ZLIB := 1 @@ -471,8 +473,24 @@ endif LIBS_VERIFIC = ifeq ($(ENABLE_VERIFIC),1) VERIFIC_DIR ?= /usr/local/src/verific_lib -VERIFIC_COMPONENTS ?= verilog database util containers hier_tree -ifneq ($(DISABLE_VERIFIC_VHDL),1) +VERIFIC_COMPONENTS ?= database util containers +ifeq ($(ENABLE_VERIFIC_HIER_TREE),1) +VERIFIC_COMPONENTS += hier_tree +CXXFLAGS += -DVERIFIC_HIER_TREE_SUPPORT +else +ifneq ($(wildcard $(VERIFIC_DIR)/hier_tree),) +VERIFIC_COMPONENTS += hier_tree +endif +endif +ifeq ($(ENABLE_VERIFIC_SYSTEMVERILOG),1) +VERIFIC_COMPONENTS += verilog +CXXFLAGS += -DVERIFIC_SYSTEMVERILOG_SUPPORT +else +ifneq ($(wildcard $(VERIFIC_DIR)/verilog),) +VERIFIC_COMPONENTS += verilog +endif +endif +ifeq ($(ENABLE_VERIFIC_VHDL),1) VERIFIC_COMPONENTS += vhdl CXXFLAGS += -DVERIFIC_VHDL_SUPPORT else @@ -488,9 +506,13 @@ ifeq ($(ENABLE_VERIFIC_LIBERTY),1) VERIFIC_COMPONENTS += synlib CXXFLAGS += -DVERIFIC_LIBERTY_SUPPORT endif -ifneq ($(DISABLE_VERIFIC_EXTENSIONS),1) +ifeq ($(ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS),1) VERIFIC_COMPONENTS += extensions CXXFLAGS += -DYOSYSHQ_VERIFIC_EXTENSIONS +else +ifneq ($(wildcard $(VERIFIC_DIR)/extensions),) +VERIFIC_COMPONENTS += extensions +endif endif CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABLE_VERIFIC ifeq ($(OS), Darwin) diff --git a/frontends/verific/Makefile.inc b/frontends/verific/Makefile.inc index df3ac8d2d..0766240a4 100644 --- a/frontends/verific/Makefile.inc +++ b/frontends/verific/Makefile.inc @@ -10,7 +10,7 @@ EXTRA_TARGETS += share/verific share/verific: $(P) rm -rf share/verific.new $(Q) mkdir -p share/verific.new -ifneq ($(DISABLE_VERIFIC_VHDL),1) +ifeq ($(ENABLE_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 diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index f7c2cefd2..56e94489c 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -42,12 +42,19 @@ USING_YOSYS_NAMESPACE #pragma clang diagnostic ignored "-Woverloaded-virtual" #endif -#include "veri_file.h" +#include "Array.h" +#include "RuntimeFlags.h" +#ifdef VERIFIC_HIER_TREE_SUPPORT #include "hier_tree.h" +#endif + +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT +#include "veri_file.h" #include "VeriModule.h" #include "VeriWrite.h" #include "VeriLibrary.h" #include "VeriExpression.h" +#endif #ifdef VERIFIC_VHDL_SUPPORT #include "vhdl_file.h" @@ -72,12 +79,16 @@ USING_YOSYS_NAMESPACE #endif #ifndef YOSYSHQ_VERIFIC_API_VERSION -# error "Only YosysHQ flavored Verific is supported. Please contact office@yosyshq.com for commercial support for Yosys+Verific." -#endif - +#warning "Only YosysHQ flavored Verific is fully supported. Please contact office@yosyshq.com for commercial support for Yosys+Verific." +#else #if YOSYSHQ_VERIFIC_API_VERSION < 20230901 # error "Please update your version of YosysHQ flavored Verific." #endif +#endif + +#if !defined(VERIFIC_VHDL_SUPPORT) && !defined(VERIFIC_SYSTEMVERILOG_SUPPORT) +#error "At least one of HDL languages must be enabled." +#endif #ifdef __clang__ #pragma clang diagnostic pop @@ -97,7 +108,9 @@ bool verific_import_pending; string verific_error_msg; int verific_sva_fsm_limit; +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT vector verific_incdirs, verific_libdirs, verific_libexts; +#endif void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args) { @@ -115,9 +128,15 @@ void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefil if (log_verific_callback) { string full_message = stringf("%s%s\n", message_prefix.c_str(), message.c_str()); +#ifdef VERIFIC_LINEFILE_INCLUDES_COLUMNS log_verific_callback(int(msg_type), message_id, LineFile::GetFileName(linefile), linefile ? linefile->GetLeftLine() : 0, linefile ? linefile->GetLeftCol() : 0, linefile ? linefile->GetRightLine() : 0, linefile ? linefile->GetRightCol() : 0, full_message.c_str()); +#else + log_verific_callback(int(msg_type), message_id, LineFile::GetFileName(linefile), + linefile ? LineFile::GetLineNo(linefile) : 0, 0, + linefile ? LineFile::GetLineNo(linefile) : 0, 0, full_message.c_str()); +#endif } else { if (msg_type == VERIFIC_ERROR || msg_type == VERIFIC_WARNING || msg_type == VERIFIC_PROGRAM_ERROR) log_warning_noprefix("%s%s\n", message_prefix.c_str(), message.c_str()); @@ -145,6 +164,7 @@ string get_full_netlist_name(Netlist *nl) return nl->CellBaseName(); } +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT class YosysStreamCallBackHandler : public VerificStreamCallBackHandler { public: @@ -174,6 +194,7 @@ public: }; YosysStreamCallBackHandler verific_read_cb; +#endif // ================================================================== @@ -392,6 +413,7 @@ static const RTLIL::Const verific_const(const char* type_name, const char *value return extract_verilog_const(value, allow_string, output_signed); } +#ifdef YOSYSHQ_VERIFIC_API_VERSION static const std::string verific_unescape(const char *value) { std::string val = std::string(value); @@ -399,6 +421,7 @@ static const std::string verific_unescape(const char *value) return val.substr(1,val.size()-2); return value; } +#endif void VerificImporter::import_attributes(dict &attributes, DesignObj *obj, Netlist *nl) { @@ -408,8 +431,13 @@ void VerificImporter::import_attributes(dict &att MapIter mi; Att *attr; +#ifdef VERIFIC_LINEFILE_INCLUDES_COLUMNS if (obj->Linefile()) attributes[ID::src] = stringf("%s:%d.%d-%d.%d", LineFile::GetFileName(obj->Linefile()), obj->Linefile()->GetLeftLine(), obj->Linefile()->GetLeftCol(), obj->Linefile()->GetRightLine(), obj->Linefile()->GetRightCol()); +#else + if (obj->Linefile()) + attributes[ID::src] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile())); +#endif FOREACH_ATTRIBUTE(obj, mi, attr) { if (attr->Key()[0] == ' ' || attr->Value() == nullptr) @@ -1265,6 +1293,7 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr return true; } +#ifdef YOSYSHQ_VERIFIC_API_VERSION if (inst->Type() == OPER_YOSYSHQ_SET_TAG) { RTLIL::SigSpec sig_expr = operatorInport(inst, "expr"); @@ -1301,6 +1330,7 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr module->connect(operatorOutput(inst),module->FutureFF(new_verific_id(inst), operatorInput(inst))); return true; } +#endif #undef IN #undef IN1 @@ -1804,10 +1834,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma for (auto net : anyseq_nets) module->connect(net_map_at(net), module->Anyseq(new_verific_id(net))); +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT pool sva_asserts; pool sva_assumes; pool sva_covers; pool sva_triggers; +#endif pool past_ffs; @@ -1924,6 +1956,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma continue; } +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT) sva_asserts.insert(inst); @@ -2066,7 +2099,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma if (!mode_keep) continue; } +#endif +#ifdef YOSYSHQ_VERIFIC_API_VERSION if (inst->Type() == PRIM_YOSYSHQ_INITSTATE) { if (verific_verbose) @@ -2078,6 +2113,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma if (!mode_keep) continue; } +#endif if (!mode_keep && verific_sva_prims.count(inst->Type())) { if (verific_verbose) @@ -2187,6 +2223,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma } } +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT if (!mode_nosva) { for (auto inst : sva_asserts) { @@ -2206,6 +2243,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma merge_past_ffs(past_ffs); } +#endif if (!mode_fullinit) { @@ -2257,7 +2295,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma // ================================================================== -VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only) +VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only YS_MAYBE_UNUSED) { module = importer->module; @@ -2266,6 +2304,7 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a Instance *inst = net->Driver(); +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT // Detect condition expression in sva_at_only mode if (sva_at_only) do { @@ -2314,7 +2353,7 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a net = inst->GetInput(); inst = net->Driver();; } - +#endif if (inst != nullptr && inst->Type() == PRIM_INV) { net = inst->GetInput(); @@ -2360,6 +2399,7 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a inst = net->Driver();; } while (0); +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT // Detect condition expression do { if (body_net == nullptr) @@ -2384,6 +2424,7 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a cond_net = inst_mux->GetControl(); cond_pol = pwr1; } while (0); +#endif clock_net = net; clock_sig = importer->net_map_at(clock_net); @@ -2655,107 +2696,269 @@ struct VerificExtNets } }; +void import_all(const char* work, std::map *nl_todo, Map *parameters, bool show_message, std::string ppfile YS_MAYBE_UNUSED) +{ +#ifdef YOSYSHQ_VERIFIC_EXTENSIONS + VerificExtensions::ElaborateAndRewrite(work, parameters); + verific_error_msg.clear(); +#endif +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT + if (!ppfile.empty()) + veri_file::PrettyPrint(ppfile.c_str(), nullptr, work); +#endif + + Array vhdl_libs; +#ifdef VERIFIC_VHDL_SUPPORT + VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work, 1); + if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib); +#endif + Array veri_libs; +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT + VeriLibrary *veri_lib = veri_file::GetLibrary(work, 1); + if (veri_lib) veri_libs.InsertLast(veri_lib); +#endif + +#ifdef VERIFIC_HIER_TREE_SUPPORT + if (show_message) + log("Running hier_tree::ElaborateAll().\n"); + Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, parameters); + Netlist *nl; + int i; + + FOREACH_ARRAY_ITEM(netlists, i, nl) + nl_todo->emplace(nl->CellBaseName(), nl); + delete netlists; +#else + if (parameters->Size()) + log_warning("Please note that parameters are not propagated during import.\n"); +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT + if (show_message) + log("Running veri_file::ElaborateAll().\n"); + veri_file::ElaborateAll(work); +#endif +#ifdef VERIFIC_VHDL_SUPPORT + if (show_message) + log("Running vhdl_file::ElaborateAll().\n"); + vhdl_file::ElaborateAll(work); +#endif + MapIter mi ; + Verific::Cell *c ; + MapIter it ; + Library *l ; + FOREACH_LIBRARY_OF_LIBSET(Libset::Global(),it,l) { + if (l == Library::Primitives() || l == Library::Operators()) continue; + FOREACH_CELL_OF_LIBRARY(l,mi,c) { + MapIter ni ; + Netlist *nl; + FOREACH_NETLIST_OF_CELL(c, ni, nl) { + if (nl) + nl_todo->emplace(nl->CellBaseName(), nl); + } + } + } +#endif +} + +std::set import_tops(const char* work, std::map *nl_todo, Map *parameters, bool show_message, std::string ppfile YS_MAYBE_UNUSED, std::vector &tops) +{ + std::set top_mod_names; + Array *netlists = nullptr; + +#ifdef VERIFIC_VHDL_SUPPORT + VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work, 1); +#endif +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT + VeriLibrary* veri_lib = veri_file::GetLibrary(work, 1); +#endif + +#ifdef YOSYSHQ_VERIFIC_EXTENSIONS + for (int static_elaborate = 1; static_elaborate >= 0; static_elaborate--) +#endif + { + Array vhdl_units; + Array veri_modules; + for (std::string n : tops) + { + const char *name = n.c_str(); + top_mod_names.insert(name); + +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT + VeriModule *veri_module = veri_lib ? veri_lib->GetModule(name, 1) : nullptr; + if (veri_module) { + if (veri_module->IsConfiguration()) { + if (show_message) + log("Adding Verilog configuration '%s' to elaboration queue.\n", name); + veri_modules.InsertLast(veri_module); + top_mod_names.erase(name); + VeriConfiguration *cfg = (VeriConfiguration*)veri_module; + VeriName *module_name; + int i; + FOREACH_ARRAY_ITEM(cfg->GetTopModuleNames(), i, module_name) { + VeriLibrary *lib = veri_module->GetLibrary() ; + if (module_name && module_name->IsHierName()) { + VeriName *prefix = module_name->GetPrefix() ; + const char *lib_name = (prefix) ? prefix->GetName() : 0 ; + if (work != lib_name) lib = veri_file::GetLibrary(lib_name, 1) ; + } + if (lib && module_name) + top_mod_names.insert(lib->GetModule(module_name->GetName(), 1)->GetName()); + } + } else { + if (show_message) + log("Adding Verilog module '%s' to elaboration queue.\n", name); + veri_modules.InsertLast(veri_module); + } + continue; + } +#endif +#ifdef VERIFIC_VHDL_SUPPORT + VhdlDesignUnit *vhdl_unit = vhdl_lib ? vhdl_lib->GetPrimUnit(name) : nullptr; + if (vhdl_unit) { + if (show_message) + 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); + } + +#ifdef YOSYSHQ_VERIFIC_EXTENSIONS + if (static_elaborate) { + VerificExtensions::ElaborateAndRewrite(work, &veri_modules, &vhdl_units, parameters); + verific_error_msg.clear(); +#endif +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT + if (!ppfile.empty()) + veri_file::PrettyPrint(ppfile.c_str(), nullptr, work); +#endif +#ifdef YOSYSHQ_VERIFIC_EXTENSIONS + continue; + } +#endif +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT + const char *lib_name = nullptr; + SetIter si; + FOREACH_SET_ITEM(veri_file::GetAllLOptions(), si, &lib_name) { + VeriLibrary* veri_lib = veri_file::GetLibrary(lib_name, 0); + if (veri_lib) { + // Also elaborate all root modules since they may contain bind statements + MapIter mi; + VeriModule *veri_module; + FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) { + if (!veri_module->IsRootModule()) continue; + veri_modules.InsertLast(veri_module); + } + } + } +#endif +#ifdef VERIFIC_HIER_TREE_SUPPORT + if (show_message) + log("Running hier_tree::Elaborate().\n"); + netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, parameters); +#else +#if defined(VERIFIC_SYSTEMVERILOG_SUPPORT) && !defined(VERIFIC_VHDL_SUPPORT) + if (show_message) + log("Running veri_file::ElaborateMultipleTop().\n"); + // SystemVerilog support only + netlists = veri_file::ElaborateMultipleTop(&veri_modules, parameters); +#elif defined(VERIFIC_VHDL_SUPPORT) && !defined(VERIFIC_SYSTEMVERILOG_SUPPORT) + if (show_message) + log("Running vhdl_file::Elaborate().\n"); + // VHDL support only + netlists = new Array(top_mod_names.size()); + for (auto &name : top_mod_names) { + vhdl_file::Elaborate(name.c_str(), work, 0, parameters); + netlists->InsertLast(Netlist::PresentDesign()); + } +#elif defined(VERIFIC_SYSTEMVERILOG_SUPPORT) && defined(VERIFIC_VHDL_SUPPORT) + // Both SystemVerilog and VHDL support + if (veri_modules.Size()>0) { + if (show_message) + log("Running veri_file::ElaborateMultipleTop().\n"); + netlists = veri_file::ElaborateMultipleTop(&veri_modules, parameters); + } else + netlists = new Array(1); + if (vhdl_units.Size()>0) { + if (show_message) + log("Running vhdl_file::Elaborate().\n"); + for (auto &name : top_mod_names) { + vhdl_file::Elaborate(name.c_str(), work, 0, parameters); + netlists->InsertLast(Netlist::PresentDesign()); + } + } +#else +#endif +#endif + } + Netlist *nl; + int i; + + FOREACH_ARRAY_ITEM(netlists, i, nl) { + if (!nl) continue; + if (!top_mod_names.count(nl->CellBaseName())) + continue; + nl->AddAtt(new Att(" \\top", NULL)); + nl_todo->emplace(nl->CellBaseName(), nl); + } + delete netlists; + return top_mod_names; +} + +void verific_cleanup() +{ +#ifdef YOSYSHQ_VERIFIC_EXTENSIONS + VerificExtensions::Reset(); +#endif +#ifdef VERIFIC_HIER_TREE_SUPPORT + hier_tree::DeleteHierarchicalTree(); +#endif +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT + veri_file::Reset(); +#endif +#ifdef VERIFIC_VHDL_SUPPORT + vhdl_file::Reset(); +#endif +#ifdef VERIFIC_EDIF_SUPPORT + edif_file::Reset(); +#endif +#ifdef VERIFIC_LIBERTY_SUPPORT + synlib_file::Reset(); +#endif + Libset::Reset(); + Message::Reset(); + RuntimeFlags::DeleteAllFlags(); + LineFile::DeleteAllLineFiles(); +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT + verific_incdirs.clear(); + verific_libdirs.clear(); + verific_libexts.clear(); +#endif + verific_import_pending = false; +} + std::string verific_import(Design *design, const std::map ¶meters, std::string top) { verific_sva_fsm_limit = 16; std::map nl_todo, nl_done; - 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); for (const auto &i : parameters) verific_params.Insert(i.first.c_str(), i.second.c_str()); + std::set top_mod_names; if (top.empty()) { - -#ifdef YOSYSHQ_VERIFIC_EXTENSIONS - VerificExtensions::ElaborateAndRewrite("work", &verific_params); - verific_error_msg.clear(); + import_all("work", &nl_todo, &verific_params, false, ""); + } else { + std::vector tops; + tops.push_back(top); +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT + veri_file::RemoveAllLOptions(); + veri_file::AddLOption("work"); #endif - netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params); + top_mod_names = import_tops("work", &nl_todo, &verific_params, false, "", tops) ; } - else { - -#ifdef YOSYSHQ_VERIFIC_EXTENSIONS - for (int static_elaborate = 1; static_elaborate >= 0; static_elaborate--) -#endif - { - Array veri_modules, vhdl_units; - - if (veri_lib) { - VeriModule *veri_module = veri_lib->GetModule(top.c_str(), 1); - if (veri_module) { - veri_modules.InsertLast(veri_module); - if (veri_module->IsConfiguration()) { - VeriConfiguration *cfg = (VeriConfiguration*)veri_module; - VeriName *module_name = (VeriName*)cfg->GetTopModuleNames()->GetLast(); - VeriLibrary *lib = veri_module->GetLibrary() ; - if (module_name && module_name->IsHierName()) { - VeriName *prefix = module_name->GetPrefix() ; - const char *lib_name = (prefix) ? prefix->GetName() : 0 ; - if (!Strings::compare("work", lib_name)) lib = veri_file::GetLibrary(lib_name, 1) ; - } - if (lib && module_name) - top = lib->GetModule(module_name->GetName(), 1)->GetName(); - } - } - -#ifdef YOSYSHQ_VERIFIC_EXTENSIONS - if (!static_elaborate) -#endif - { - // Also elaborate all root modules since they may contain bind statements - MapIter mi; - FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) { - if (!veri_module->IsRootModule()) continue; - veri_modules.InsertLast(veri_module); - } - } - } - -#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 - -#ifdef YOSYSHQ_VERIFIC_EXTENSIONS - if (static_elaborate) { - VerificExtensions::ElaborateAndRewrite("work", &veri_modules, &vhdl_units, &verific_params); - verific_error_msg.clear(); - continue; - } -#endif - - netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &verific_params); - } - } - - Netlist *nl; - int i; - std::string cell_name = top; - - FOREACH_ARRAY_ITEM(netlists, i, nl) { - if (!nl) continue; - if (!top.empty() && nl->CellBaseName() != top) - continue; - nl->AddAtt(new Att(" \\top", NULL)); - nl_todo.emplace(nl->CellBaseName(), nl); - cell_name = nl->CellBaseName(); - } - if (top.empty()) cell_name = top; - - delete netlists; if (!verific_error_msg.empty()) log_error("%s\n", verific_error_msg.c_str()); @@ -2773,34 +2976,12 @@ std::string verific_import(Design *design, const std::mapfirst) == 0) { VerificImporter importer(false, false, false, false, false, false, false); nl_done[it->first] = it->second; - importer.import_netlist(design, nl, nl_todo, nl->CellBaseName() == cell_name); + importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->CellBaseName())); } nl_todo.erase(it); } -#ifdef YOSYSHQ_VERIFIC_EXTENSIONS - VerificExtensions::Reset(); -#endif - hier_tree::DeleteHierarchicalTree(); - veri_file::Reset(); -#ifdef VERIFIC_VHDL_SUPPORT - vhdl_file::Reset(); -#endif -#ifdef VERIFIC_EDIF_SUPPORT - edif_file::Reset(); -#endif -#ifdef VERIFIC_LIBERTY_SUPPORT - synlib_file::Reset(); -#endif - Libset::Reset(); - Message::Reset(); - RuntimeFlags::DeleteAllFlags(); - LineFile::DeleteAllLineFiles(); - verific_incdirs.clear(); - verific_libdirs.clear(); - verific_libexts.clear(); - verific_import_pending = false; - + verific_cleanup(); if (!verific_error_msg.empty()) log_error("%s\n", verific_error_msg.c_str()); return top; @@ -2829,6 +3010,7 @@ struct VerificPass : public Pass { { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT log(" verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} ..\n"); log("\n"); log("Load the specified Verilog/SystemVerilog files into Verific.\n"); @@ -2847,6 +3029,7 @@ struct VerificPass : public Pass { log("Like -sv, but define FORMAL instead of SYNTHESIS.\n"); log("\n"); log("\n"); +#endif #ifdef VERIFIC_VHDL_SUPPORT log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl2019|-vhdl} ..\n"); log("\n"); @@ -2873,6 +3056,7 @@ struct VerificPass : public Pass { log("\n"); log("\n"); #endif +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT log(" verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|\n"); log(" -sv2012|-sv|-formal] \n"); log("\n"); @@ -2906,6 +3090,7 @@ struct VerificPass : public Pass { log(" -sverilog\n"); log("\n"); log("\n"); +#endif log(" verific [-work ] {-sv|-vhdl|...} \n"); log("\n"); log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n"); @@ -2918,6 +3103,7 @@ struct VerificPass : public Pass { log("(-L may be used more than once)\n"); log("\n"); log("\n"); +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT log(" verific -vlog-incdir ..\n"); log("\n"); log("Add Verilog include directories.\n"); @@ -2944,6 +3130,7 @@ struct VerificPass : public Pass { log("Remove Verilog defines previously set with -vlog-define.\n"); log("\n"); log("\n"); +#endif log(" verific -set-error ..\n"); log(" verific -set-warning ..\n"); log(" verific -set-info ..\n"); @@ -2978,9 +3165,11 @@ struct VerificPass : public Pass { log(" -no-split-complex-ports\n"); log(" Complex ports (structs or arrays) are not split and remain packed as a single port.\n"); log("\n"); +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT log(" -autocover\n"); log(" Generate automatic cover statements for all asserts\n"); log("\n"); +#endif log(" -fullinit\n"); log(" Keep all register initializations, even those for non-FF registers.\n"); log("\n"); @@ -3013,12 +3202,14 @@ struct VerificPass : public Pass { log(" -V\n"); log(" Import Verific netlist as-is without translating to Yosys cell types. \n"); log("\n"); +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT log(" -nosva\n"); log(" Ignore SVA properties, do not infer checker logic.\n"); log("\n"); log(" -L \n"); log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n"); log("\n"); +#endif log(" -n\n"); log(" Keep all Verific names on instances and nets. By default only\n"); log(" user-declared names are preserved.\n"); @@ -3142,7 +3333,7 @@ struct VerificPass : public Pass { #endif msg_type_t prev_1063; - +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT void add_modules_to_map(Map &map, std::string work, bool flag_lib) { MapIter mi ; @@ -3176,6 +3367,7 @@ struct VerificPass : public Pass { if (Message::GetMessageType("VERI-1063")!=prev_1063) Message::SetMessageType("VERI-1063", prev_1063); } +#endif void execute(std::vector args, RTLIL::Design *design) override { @@ -3208,10 +3400,11 @@ struct VerificPass : public Pass { // Properly respect order of read and write for rams RuntimeFlags::SetVar("db_change_inplace_ram_blocking_write_before_read", 1); +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT RuntimeFlags::SetVar("veri_extract_dualport_rams", 0); RuntimeFlags::SetVar("veri_extract_multiport_rams", 1); RuntimeFlags::SetVar("veri_allow_any_ram_in_loop", 1); - +#endif #ifdef VERIFIC_VHDL_SUPPORT RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0); RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1); @@ -3224,6 +3417,7 @@ struct VerificPass : public Pass { //RuntimeFlags::SetVar("vhdl_preserve_comments", 1); RuntimeFlags::SetVar("vhdl_preserve_drivers", 1); #endif +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT RuntimeFlags::SetVar("veri_preserve_assignments", 1); RuntimeFlags::SetVar("veri_preserve_comments", 1); RuntimeFlags::SetVar("veri_preserve_drivers", 1); @@ -3236,7 +3430,7 @@ struct VerificPass : public Pass { // https://github.com/YosysHQ/yosys/issues/1055 RuntimeFlags::SetVar("veri_elaborate_top_level_modules_having_interface_ports", 1) ; - +#endif RuntimeFlags::SetVar("verific_produce_verbose_syntax_error_message", 1); #ifndef DB_PRESERVE_INITIAL_VALUE @@ -3266,8 +3460,9 @@ struct VerificPass : public Pass { std::string work = "work"; bool is_work_set = false; (void)is_work_set; +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT veri_file::RegisterCallBackVerificStream(&verific_read_cb); - +#endif if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" || args[argidx] == "-set-info" || args[argidx] == "-set-ignore")) { @@ -3301,6 +3496,7 @@ struct VerificPass : public Pass { goto check_error; } +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") { for (argidx++; argidx < GetSize(args); argidx++) verific_incdirs.push_back(args[argidx]); @@ -3343,6 +3539,7 @@ struct VerificPass : public Pass { } veri_file::RemoveAllLOptions(); +#endif for (int i = argidx; i < GetSize(args); i++) { if (args[i] == "-work" && i+1 < GetSize(args)) { @@ -3350,24 +3547,30 @@ struct VerificPass : public Pass { is_work_set = true; continue; } +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT if (args[i] == "-L" && i+1 < GetSize(args)) { ++i; continue; } +#endif break; } +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT veri_file::AddLOption(work.c_str()); +#endif for (int i = argidx; i < GetSize(args); i++) { if (args[i] == "-work" && i+1 < GetSize(args)) { ++i; continue; } +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT if (args[i] == "-L" && i+1 < GetSize(args)) { if (args[++i] == work) veri_file::RemoveAllLOptions(); continue; } +#endif break; } for (; argidx < GetSize(args); argidx++) @@ -3377,13 +3580,16 @@ struct VerificPass : public Pass { is_work_set = true; continue; } +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT if (args[argidx] == "-L" && argidx+1 < GetSize(args)) { veri_file::AddLOption(args[++argidx].c_str()); continue; } +#endif break; } +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT if (GetSize(args) > argidx && (args[argidx] == "-f" || args[argidx] == "-F")) { unsigned verilog_mode = veri_file::UNDEFINED; @@ -3520,14 +3726,17 @@ struct VerificPass : public Pass { verific_import_pending = true; goto check_error; } +#endif #ifdef VERIFIC_VHDL_SUPPORT if (GetSize(args) > argidx && args[argidx] == "-vhdl87") { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str()); bool flag_lib = false; - for (argidx++; argidx < GetSize(args); argidx++) { + argidx++; + while (argidx < GetSize(args)) { if (args[argidx] == "-lib") { flag_lib = true; + argidx++; continue; } if (args[argidx].compare(0, 1, "-") == 0) { @@ -3548,9 +3757,11 @@ struct VerificPass : public Pass { if (GetSize(args) > argidx && args[argidx] == "-vhdl93") { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str()); bool flag_lib = false; - for (argidx++; argidx < GetSize(args); argidx++) { + argidx++; + while (argidx < GetSize(args)) { if (args[argidx] == "-lib") { flag_lib = true; + argidx++; continue; } if (args[argidx].compare(0, 1, "-") == 0) { @@ -3571,9 +3782,11 @@ struct VerificPass : public Pass { if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str()); bool flag_lib = false; - for (argidx++; argidx < GetSize(args); argidx++) { + argidx++; + while (argidx < GetSize(args)) { if (args[argidx] == "-lib") { flag_lib = true; + argidx++; continue; } if (args[argidx].compare(0, 1, "-") == 0) { @@ -3594,9 +3807,11 @@ struct VerificPass : public Pass { if (GetSize(args) > argidx && (args[argidx] == "-vhdl2019")) { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2019").c_str()); bool flag_lib = false; - for (argidx++; argidx < GetSize(args); argidx++) { + argidx++; + while (argidx < GetSize(args)) { if (args[argidx] == "-lib") { flag_lib = true; + argidx++; continue; } if (args[argidx].compare(0, 1, "-") == 0) { @@ -3617,9 +3832,11 @@ struct VerificPass : public Pass { if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str()); bool flag_lib = false; - for (argidx++; argidx < GetSize(args); argidx++) { + argidx++; + while (argidx < GetSize(args)) { if (args[argidx] == "-lib") { flag_lib = true; + argidx++; continue; } if (args[argidx].compare(0, 1, "-") == 0) { @@ -3728,8 +3945,10 @@ struct VerificPass : public Pass { #else goto check_error; #endif +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT else veri_file::PrettyPrint(filename, module, work.c_str()); +#endif goto check_error; } @@ -3770,6 +3989,7 @@ struct VerificPass : public Pass { mode_keep = true; continue; } +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT if (args[argidx] == "-nosva") { mode_nosva = true; continue; @@ -3778,14 +3998,15 @@ struct VerificPass : public Pass { verific_sva_fsm_limit = atoi(args[++argidx].c_str()); continue; } - if (args[argidx] == "-n") { - mode_names = true; - continue; - } if (args[argidx] == "-autocover") { mode_autocover = true; continue; } +#endif + if (args[argidx] == "-n") { + mode_names = true; + continue; + } if (args[argidx] == "-fullinit") { mode_fullinit = true; continue; @@ -3833,136 +4054,17 @@ struct VerificPass : public Pass { if (mode_all) { - -#ifdef YOSYSHQ_VERIFIC_EXTENSIONS - VerificExtensions::ElaborateAndRewrite(work, ¶meters); - verific_error_msg.clear(); -#endif - if (!ppfile.empty()) - veri_file::PrettyPrint(ppfile.c_str(), nullptr, work.c_str()); - - log("Running hier_tree::ElaborateAll().\n"); - - 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, ¶meters); - Netlist *nl; - int i; - - FOREACH_ARRAY_ITEM(netlists, i, nl) - nl_todo.emplace(nl->CellBaseName(), nl); - delete netlists; + import_all(work.c_str(), &nl_todo, ¶meters, true, ppfile); } else { if (argidx == GetSize(args)) cmd_error(args, argidx, "No top module specified.\n"); - Array *netlists = nullptr; - -#ifdef YOSYSHQ_VERIFIC_EXTENSIONS - for (int static_elaborate = 1; static_elaborate >= 0; static_elaborate--) -#endif - { - - 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 (int i = argidx; i < GetSize(args); i++) - { - const char *name = args[i].c_str(); - top_mod_names.insert(name); - - VeriModule *veri_module = veri_lib ? veri_lib->GetModule(name, 1) : nullptr; - if (veri_module) { - if (veri_module->IsConfiguration()) { - log("Adding Verilog configuration '%s' to elaboration queue.\n", name); - veri_modules.InsertLast(veri_module); - - top_mod_names.erase(name); - - VeriConfiguration *cfg = (VeriConfiguration*)veri_module; - VeriName *module_name; - int i; - FOREACH_ARRAY_ITEM(cfg->GetTopModuleNames(), i, module_name) { - VeriLibrary *lib = veri_module->GetLibrary() ; - if (module_name && module_name->IsHierName()) { - VeriName *prefix = module_name->GetPrefix() ; - const char *lib_name = (prefix) ? prefix->GetName() : 0 ; - if (work != lib_name) lib = veri_file::GetLibrary(lib_name, 1) ; - } - if (lib && module_name) - top_mod_names.insert(lib->GetModule(module_name->GetName(), 1)->GetName()); - } - } else { - log("Adding Verilog module '%s' to elaboration queue.\n", name); - 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); - } - -#ifdef YOSYSHQ_VERIFIC_EXTENSIONS - if (static_elaborate) { - VerificExtensions::ElaborateAndRewrite(work, &veri_modules, &vhdl_units, ¶meters); - verific_error_msg.clear(); -#endif - if (!ppfile.empty()) - veri_file::PrettyPrint(ppfile.c_str(), nullptr, work.c_str()); - -#ifdef YOSYSHQ_VERIFIC_EXTENSIONS - continue; - } -#endif - const char *lib_name = nullptr; - SetIter si; - FOREACH_SET_ITEM(veri_file::GetAllLOptions(), si, &lib_name) { - VeriLibrary* veri_lib = veri_file::GetLibrary(lib_name, 0); - if (veri_lib) { - // Also elaborate all root modules since they may contain bind statements - MapIter mi; - VeriModule *veri_module; - FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) { - if (!veri_module->IsRootModule()) continue; - veri_modules.InsertLast(veri_module); - } - } - } - - log("Running hier_tree::Elaborate().\n"); - netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, ¶meters); - } - - Netlist *nl; - int i; - - FOREACH_ARRAY_ITEM(netlists, i, nl) { - if (!nl) continue; - if (!top_mod_names.count(nl->CellBaseName())) - continue; - nl->AddAtt(new Att(" \\top", NULL)); - nl_todo.emplace(nl->CellBaseName(), nl); - } - delete netlists; + std::vector tops; + for (int i = argidx; i < GetSize(args); i++) + tops.push_back(args[i].c_str()); + top_mod_names = import_tops(work.c_str(), &nl_todo, ¶meters, true, ppfile, tops) ; } if (mode_cells) { log("Importing all cells.\n"); @@ -4006,11 +4108,12 @@ struct VerificPass : public Pass { nl.second->ChangePortBusStructures(1 /* hierarchical */); } +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT if (!dumpfile.empty()) { VeriWrite veri_writer; veri_writer.WriteFile(dumpfile.c_str(), Netlist::PresentDesign()); } - +#endif while (!nl_todo.empty()) { auto it = nl_todo.begin(); Netlist *nl = it->second; @@ -4023,28 +4126,7 @@ struct VerificPass : public Pass { nl_todo.erase(it); } -#ifdef YOSYSHQ_VERIFIC_EXTENSIONS - VerificExtensions::Reset(); -#endif - hier_tree::DeleteHierarchicalTree(); - veri_file::Reset(); -#ifdef VERIFIC_VHDL_SUPPORT - vhdl_file::Reset(); -#endif -#ifdef VERIFIC_EDIF_SUPPORT - edif_file::Reset(); -#endif -#ifdef VERIFIC_LIBERTY_SUPPORT - synlib_file::Reset(); -#endif - Libset::Reset(); - Message::Reset(); - RuntimeFlags::DeleteAllFlags(); - LineFile::DeleteAllLineFiles(); - verific_incdirs.clear(); - verific_libdirs.clear(); - verific_libexts.clear(); - verific_import_pending = false; + verific_cleanup(); goto check_error; } diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 222c7d2e9..b219c0165 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -80,6 +80,7 @@ USING_YOSYS_NAMESPACE using namespace Verific; #endif +#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT PRIVATE_NAMESPACE_BEGIN // Non-deterministic FSM @@ -1878,5 +1879,8 @@ bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net) worker.importer = importer; return worker.net_to_ast_driver(net) != nullptr; } - +#else +YOSYS_NAMESPACE_BEGIN +pool verific_sva_prims = {}; +#endif YOSYS_NAMESPACE_END