From 472a1d525b8c825598226a281d48a040c87dc651 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 21 May 2024 16:45:29 +0200 Subject: [PATCH] Add initial support for Verific without additional YosysHQ patch --- Makefile | 11 +++++- frontends/verific/verific.cc | 76 ++++++++++++++++++++++++++++++++++-- 2 files changed, 83 insertions(+), 4 deletions(-) diff --git a/Makefile b/Makefile index 9e3fd1a20ff..92f2f9a9f2f 100644 --- a/Makefile +++ b/Makefile @@ -21,6 +21,7 @@ ENABLE_VERIFIC_EDIF := 0 ENABLE_VERIFIC_LIBERTY := 0 DISABLE_VERIFIC_EXTENSIONS := 0 DISABLE_VERIFIC_VHDL := 0 +DISABLE_VERIFIC_HIER_TREE := 0 ENABLE_COVER := 1 ENABLE_LIBYOSYS := 0 ENABLE_ZLIB := 1 @@ -471,7 +472,15 @@ endif LIBS_VERIFIC = ifeq ($(ENABLE_VERIFIC),1) VERIFIC_DIR ?= /usr/local/src/verific_lib -VERIFIC_COMPONENTS ?= verilog database util containers hier_tree +VERIFIC_COMPONENTS ?= verilog database util containers +ifneq ($(DISABLE_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 ifneq ($(DISABLE_VERIFIC_VHDL),1) VERIFIC_COMPONENTS += vhdl CXXFLAGS += -DVERIFIC_VHDL_SUPPORT diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index b4b0664d341..5485a9fb5bc 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -43,7 +43,9 @@ USING_YOSYS_NAMESPACE #endif #include "veri_file.h" +#ifdef DVERIFIC_HIER_TREE_SUPPORT #include "hier_tree.h" +#endif #include "VeriModule.h" #include "VeriWrite.h" #include "VeriLibrary.h" @@ -72,12 +74,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 + +#ifndef DB_PRESERVE_INITIAL_VALUE +#error "Verific must have DB_PRESERVE_INITIAL_VALUE compile flag set on" +#endif #ifdef __clang__ #pragma clang diagnostic pop @@ -115,9 +121,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()); @@ -392,6 +404,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 +412,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 +422,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 +1284,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 +1321,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 @@ -2067,6 +2088,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma continue; } +#ifdef YOSYSHQ_VERIFIC_API_VERSION if (inst->Type() == PRIM_YOSYSHQ_INITSTATE) { if (verific_verbose) @@ -2078,6 +2100,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) @@ -2680,7 +2703,24 @@ std::string verific_import(Design *design, const std::mapGetLibrary("work"); + 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 } else { @@ -2737,7 +2777,11 @@ std::string verific_import(Design *design, const std::mapCellBaseName(), nl); delete netlists; +#else + if (parameters.Size()) + log_warning("Please note that parameters are not propagated during import.\n"); + veri_file::ElaborateAll(work.c_str()); + + MapIter mi ; + Verific::Cell *c ; + Library *l = Libset::Global()->GetLibrary(work.c_str()); + 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 } else { @@ -3943,7 +4007,11 @@ struct VerificPass : public Pass { } log("Running hier_tree::Elaborate().\n"); +#ifdef VERIFIC_HIER_TREE_SUPPORT netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, ¶meters); +#else + netlists = veri_file::ElaborateMultipleTop(&veri_modules, ¶meters); +#endif } Netlist *nl; @@ -4020,7 +4088,9 @@ struct VerificPass : public Pass { #ifdef YOSYSHQ_VERIFIC_EXTENSIONS VerificExtensions::Reset(); #endif +#ifdef VERIFIC_HIER_TREE_SUPPORT hier_tree::DeleteHierarchicalTree(); +#endif veri_file::Reset(); #ifdef VERIFIC_VHDL_SUPPORT vhdl_file::Reset();