diff options
Diffstat (limited to 'frontends/verific/verific.cc')
-rw-r--r-- | frontends/verific/verific.cc | 431 |
1 files changed, 390 insertions, 41 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index cb0368fd5..31c77d39c 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -21,6 +21,7 @@ #include "kernel/sigtools.h" #include "kernel/celltypes.h" #include "kernel/log.h" +#include "libs/sha1/sha1.h" #include <stdlib.h> #include <stdio.h> #include <string.h> @@ -48,12 +49,13 @@ USING_YOSYS_NAMESPACE #include "VeriWrite.h" #include "VhdlUnits.h" #include "VeriLibrary.h" +#include "VeriExtensions.h" #ifndef SYMBIOTIC_VERIFIC_API_VERSION # error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific." #endif -#if SYMBIOTIC_VERIFIC_API_VERSION < 1 +#if SYMBIOTIC_VERIFIC_API_VERSION < 20201001 # error "Please update your version of Symbiotic EDA flavored Verific." #endif @@ -198,12 +200,17 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att attributes.emplace(stringf("\\enum_value_%s", p+2), RTLIL::escape_id(k)); } else if (nl->IsFromVhdl()) { - // Expect "<binary>" + // Expect "<binary>" or plain <binary> auto p = v; if (p) { - if (*p != '"') - p = nullptr; - else { + if (*p != '"') { + auto l = strlen(p); + auto q = (char*)malloc(l+1); + strncpy(q, p, l); + q[l] = '\0'; + for(char *ptr = q; *ptr; ++ptr )*ptr = tolower(*ptr); + attributes.emplace(stringf("\\enum_value_%s", q), RTLIL::escape_id(k)); + } else { auto *q = p+1; for (; *q != '"'; q++) if (*q != '0' && *q != '1') { @@ -212,16 +219,20 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att } if (p && *(q+1) != '\0') p = nullptr; + + if (p != nullptr) + { + auto l = strlen(p); + auto q = (char*)malloc(l+1-2); + strncpy(q, p+1, l-2); + q[l-2] = '\0'; + attributes.emplace(stringf("\\enum_value_%s", q), RTLIL::escape_id(k)); + free(q); + } } } if (p == nullptr) - log_error("Expected TypeRange value '%s' to be of form \"<binary>\".\n", v); - auto l = strlen(p); - auto q = (char*)malloc(l+1-2); - strncpy(q, p+1, l-2); - q[l-2] = '\0'; - attributes.emplace(stringf("\\enum_value_%s", q), RTLIL::escape_id(k)); - free(q); + log_error("Expected TypeRange value '%s' to be of form \"<binary>\" or <binary>.\n", v); } } } @@ -854,6 +865,21 @@ void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates) merge_past_ffs_clock(it.second, it.first.first, it.first.second); } +static std::string sha1_if_contain_spaces(std::string str) +{ + if(str.find_first_of(' ') != std::string::npos) { + std::size_t open = str.find_first_of('('); + std::size_t closed = str.find_last_of(')'); + if (open != std::string::npos && closed != std::string::npos) { + std::string content = str.substr(open + 1, closed - open - 1); + return str.substr(0, open + 1) + sha1(content) + str.substr(closed); + } else { + return sha1(str); + } + } + return str; +} + void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool norename) { std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name(); @@ -867,7 +893,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se module_name += nl->Name(); module_name += ")"; } - module_name = "\\" + module_name; + module_name = "\\" + sha1_if_contain_spaces(module_name); } netlist = nl; @@ -1109,7 +1135,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size()); wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex()); - import_attributes(wire->attributes, netbus, nl); + MapIter mibus; + FOREACH_NET_OF_NETBUS(netbus, mibus, net) { + if (net) + import_attributes(wire->attributes, net, nl); + break; + } RTLIL::Const initval = Const(State::Sx, GetSize(wire)); bool initval_valid = false; @@ -1262,7 +1293,10 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se if (inst->Type() == OPER_READ_PORT) { - RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name())); + RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name()), nullptr); + if (!memory) + log_error("Memory net '%s' missing, possibly no driver, use verific -flatten.\n", inst->GetInput()->Name()); + int numchunks = int(inst->OutputSize()) / memory->width; int chunksbits = ceil_log2(numchunks); @@ -1289,7 +1323,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT) { - RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name())); + RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name()), nullptr); + if (!memory) + log_error("Memory net '%s' missing, possibly no driver, use verific -flatten.\n", inst->GetInput()->Name()); int numchunks = int(inst->Input2Size()) / memory->width; int chunksbits = ceil_log2(numchunks); @@ -1435,6 +1471,16 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se continue; } + if (inst->Type() == PRIM_SEDA_INITSTATE) + { + SigBit initstate = module->Initstate(new_verific_id(inst)); + SigBit sig_o = net_map_at(inst->GetOutput()); + module->connect(sig_o, initstate); + + if (!mode_keep) + continue; + } + if (!mode_keep && verific_sva_prims.count(inst->Type())) { if (verific_verbose) log(" skipping SVA cell in non k-mode\n"); @@ -1482,7 +1528,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se inst_type += inst->View()->Name(); inst_type += ")"; } - inst_type = "\\" + inst_type; + inst_type = "\\" + sha1_if_contain_spaces(inst_type); } RTLIL::Cell *cell = module->addCell(inst_name, inst_type); @@ -1877,7 +1923,7 @@ struct VerificExtNets new_net = new Net(name.c_str()); nl->Add(new_net); - Net *n YS_ATTRIBUTE(unused) = route_up(new_net, port->IsOutput(), ca_nl, ca_net); + Net *n = route_up(new_net, port->IsOutput(), ca_nl, ca_net); log_assert(n == ca_net); } @@ -1912,6 +1958,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()); + InitialAssertionRewriter rw; + rw.RegisterCallBack(); + if (top.empty()) { netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params); } @@ -2003,7 +2052,7 @@ bool check_noverific_env() struct VerificPass : public Pass { VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -2134,6 +2183,73 @@ struct VerificPass : public Pass { log(" Dump the Verific netlist as a verilog file.\n"); log("\n"); log("\n"); + log(" verific [-work <libname>] -pp [options] <filename> [<module>]..\n"); + log("\n"); + log("Pretty print design (or just module) to the specified file from the\n"); + log("specified library. (default library when -work is not present: \"work\")\n"); + log("\n"); + log("Pretty print options:\n"); + log("\n"); + log(" -verilog\n"); + log(" Save output for Verilog/SystemVerilog design modules (default).\n"); + log("\n"); + log(" -vhdl\n"); + log(" Save output for VHDL design units.\n"); + log("\n"); + log("\n"); + log(" verific -app <application>..\n"); + log("\n"); + log("Execute SEDA formal application on loaded Verilog files.\n"); + log("\n"); + log("Application options:\n"); + log("\n"); + log(" -module <module>\n"); + log(" Run formal application only on specified module.\n"); + log("\n"); + log(" -blacklist <filename[:lineno]>\n"); + log(" Do not run application on modules from files that match the filename\n"); + log(" or filename and line number if provided in such format.\n"); + log(" Parameter can also contain comma separated list of file locations.\n"); + log("\n"); + log(" -blfile <file>\n"); + log(" Do not run application on locations specified in file, they can represent filename\n"); + log(" or filename and location in file.\n"); + log("\n"); + log("Applications:\n"); + log("\n"); +#ifdef YOSYS_ENABLE_VERIFIC + VerificFormalApplications vfa; + log("%s\n",vfa.GetHelp().c_str()); +#else + log(" WARNING: Applications only available in commercial build.\n"); + +#endif + log("\n"); + log("\n"); + log(" verific -template <name> <top_module>..\n"); + log("\n"); + log("Generate template for specified top module of loaded design.\n"); + log("\n"); + log("Template options:\n"); + log("\n"); + log(" -out\n"); + log(" Specifies output file for generated template, by default output is stdout\n"); + log("\n"); + log(" -chparam name value \n"); + log(" Generate template using this parameter value. Otherwise default parameter\n"); + log(" values will be used for templat generate functionality. This option\n"); + log(" can be specified multiple times to override multiple parameters.\n"); + log(" String values must be passed in double quotes (\").\n"); + log("\n"); + log("Templates:\n"); + log("\n"); +#ifdef YOSYS_ENABLE_VERIFIC + VerificTemplateGenerator vfg; + log("%s\n",vfg.GetHelp().c_str()); +#else + log(" WARNING: Templates only available in commercial build.\n"); + log("\n"); +#endif log("Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"); log("https://www.symbioticeda.com/seda-suite\n"); log("\n"); @@ -2142,7 +2258,7 @@ struct VerificPass : public Pass { log("\n"); } #ifdef YOSYS_ENABLE_VERIFIC - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { static bool set_verific_global_flags = true; @@ -2175,6 +2291,12 @@ struct VerificPass : public Pass { 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); + // Workaround for VIPER #13851 RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1); @@ -2327,8 +2449,10 @@ struct VerificPass : public Pass { while (argidx < GetSize(args)) file_names.Insert(args[argidx++].c_str()); - if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU)) + if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU)) { + verific_error_msg.clear(); log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n"); + } verific_import_pending = true; goto check_error; @@ -2370,6 +2494,226 @@ struct VerificPass : public Pass { goto check_error; } + if (argidx < GetSize(args) && args[argidx] == "-app") + { + if (!(argidx+1 < GetSize(args))) + cmd_error(args, argidx, "No formal application specified.\n"); + + VerificFormalApplications vfa; + auto apps = vfa.GetApps(); + std::string app = args[++argidx]; + std::vector<std::string> blacklists; + if (apps.find(app) == apps.end()) + log_cmd_error("Application '%s' does not exist.\n", app.c_str()); + + FormalApplication *application = apps[app]; + application->setLogger([](std::string msg) { log("%s",msg.c_str()); } ); + VeriModule *selected_module = nullptr; + + for (argidx++; argidx < GetSize(args); argidx++) { + std::string error; + if (application->checkParams(args, argidx, error)) { + if (!error.empty()) + cmd_error(args, argidx, error); + continue; + } + + if (args[argidx] == "-module" && argidx < GetSize(args)) { + if (!(argidx+1 < GetSize(args))) + cmd_error(args, argidx+1, "No module name specified.\n"); + std::string module = args[++argidx]; + VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1); + selected_module = veri_lib ? veri_lib->GetModule(module.c_str(), 1) : nullptr; + if (!selected_module) { + log_error("Can't find module '%s'.\n", module.c_str()); + } + continue; + } + if (args[argidx] == "-blacklist" && argidx < GetSize(args)) { + if (!(argidx+1 < GetSize(args))) + cmd_error(args, argidx+1, "No blacklist specified.\n"); + + std::string line = args[++argidx]; + std::string p; + while (!(p = next_token(line, ",\t\r\n ")).empty()) + blacklists.push_back(p); + continue; + } + if (args[argidx] == "-blfile" && argidx < GetSize(args)) { + if (!(argidx+1 < GetSize(args))) + cmd_error(args, argidx+1, "No blacklist file specified.\n"); + std::string fn = args[++argidx]; + std::ifstream f(fn); + if (f.fail()) + log_cmd_error("Can't open blacklist file '%s'!\n", fn.c_str()); + + std::string line,p; + while (std::getline(f, line)) { + while (!(p = next_token(line, ",\t\r\n ")).empty()) + blacklists.push_back(p); + } + continue; + } + break; + } + if (argidx < GetSize(args)) + cmd_error(args, argidx, "unknown option/parameter"); + + application->setBlacklists(&blacklists); + application->setSingleModuleMode(selected_module!=nullptr); + + const char *err = application->validate(); + if (err) + cmd_error(args, argidx, err); + + MapIter mi; + VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1); + log("Running formal application '%s'.\n", app.c_str()); + + if (selected_module) { + std::string out; + if (!application->execute(selected_module, out)) + log_error("%s", out.c_str()); + } + else { + VeriModule *module ; + FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, module) { + std::string out; + if (!application->execute(module, out)) { + log_error("%s", out.c_str()); + break; + } + } + } + goto check_error; + } + + if (argidx < GetSize(args) && args[argidx] == "-pp") + { + const char* filename = nullptr; + const char* module = nullptr; + bool mode_vhdl = false; + for (argidx++; argidx < GetSize(args); argidx++) { + if (args[argidx] == "-vhdl") { + mode_vhdl = true; + continue; + } + if (args[argidx] == "-verilog") { + mode_vhdl = false; + continue; + } + + if (args[argidx].compare(0, 1, "-") == 0) { + cmd_error(args, argidx, "unknown option"); + goto check_error; + } + + if (!filename) { + filename = args[argidx].c_str(); + continue; + } + if (module) + log_cmd_error("Only one module can be specified.\n"); + module = args[argidx].c_str(); + } + + if (argidx < GetSize(args)) + cmd_error(args, argidx, "unknown option/parameter"); + + if (!filename) + log_cmd_error("Filname must be specified.\n"); + + if (mode_vhdl) + vhdl_file::PrettyPrint(filename, module, work.c_str()); + else + veri_file::PrettyPrint(filename, module, work.c_str()); + goto check_error; + } + + if (argidx < GetSize(args) && args[argidx] == "-template") + { + if (!(argidx+1 < GetSize(args))) + cmd_error(args, argidx+1, "No template type specified.\n"); + + VerificTemplateGenerator vfg; + auto gens = vfg.GetGenerators(); + std::string app = args[++argidx]; + if (gens.find(app) == gens.end()) + log_cmd_error("Template generator '%s' does not exist.\n", app.c_str()); + TemplateGenerator *generator = gens[app]; + if (!(argidx+1 < GetSize(args))) + cmd_error(args, argidx+1, "No top module specified.\n"); + generator->setLogger([](std::string msg) { log("%s",msg.c_str()); } ); + + std::string module = args[++argidx]; + VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1); + VeriModule *veri_module = veri_lib ? veri_lib->GetModule(module.c_str(), 1) : nullptr; + if (!veri_module) { + log_error("Can't find module/unit '%s'.\n", module.c_str()); + } + + log("Template '%s' is running for module '%s'.\n", app.c_str(),module.c_str()); + + Map parameters(STRING_HASH); + const char *out_filename = nullptr; + + for (argidx++; argidx < GetSize(args); argidx++) { + std::string error; + if (generator->checkParams(args, argidx, error)) { + if (!error.empty()) + cmd_error(args, argidx, error); + continue; + } + + if (args[argidx] == "-chparam" && argidx < GetSize(args)) { + if (!(argidx+1 < GetSize(args))) + cmd_error(args, argidx+1, "No param name specified.\n"); + if (!(argidx+2 < GetSize(args))) + cmd_error(args, argidx+2, "No param value specified.\n"); + + const std::string &key = args[++argidx]; + const std::string &value = args[++argidx]; + unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(), + 1 /* force_overwrite */); + if (!new_insertion) + log_warning_noprefix("-chparam %s already specified: overwriting.\n", key.c_str()); + continue; + } + + if (args[argidx] == "-out" && argidx < GetSize(args)) { + if (!(argidx+1 < GetSize(args))) + cmd_error(args, argidx+1, "No output file specified.\n"); + out_filename = args[++argidx].c_str(); + continue; + } + + break; + } + if (argidx < GetSize(args)) + cmd_error(args, argidx, "unknown option/parameter"); + + const char *err = generator->validate(); + if (err) + cmd_error(args, argidx, err); + + std::string val; + if (!generator->generate(veri_module, val, ¶meters)) + log_error("%s", val.c_str()); + + FILE *of = stdout; + if (out_filename) { + of = fopen(out_filename, "w"); + if (of == nullptr) + log_error("Can't open '%s' for writing: %s\n", out_filename, strerror(errno)); + log("Writing output to '%s'\n",out_filename); + } + fprintf(of, "%s\n",val.c_str()); + fflush(of); + if (of!=stdout) + fclose(of); + goto check_error; + } + if (GetSize(args) > argidx && args[argidx] == "-import") { std::set<Netlist*> nl_todo, nl_done; @@ -2454,6 +2798,9 @@ struct VerificPass : public Pass { std::set<std::string> top_mod_names; + InitialAssertionRewriter rw; + rw.RegisterCallBack(); + if (mode_all) { log("Running hier_tree::ElaborateAll().\n"); @@ -2478,31 +2825,23 @@ struct VerificPass : public Pass { if (argidx == GetSize(args)) cmd_error(args, argidx, "No top module specified.\n"); + VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1); + VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1); + Array veri_modules, vhdl_units; for (; argidx < GetSize(args); argidx++) { const char *name = args[argidx].c_str(); top_mod_names.insert(name); - VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1); - if (veri_lib) { - VeriModule *veri_module = veri_lib->GetModule(name, 1); - if (veri_module) { - log("Adding Verilog module '%s' to elaboration queue.\n", name); - veri_modules.InsertLast(veri_module); - continue; - } - - // 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); - } + VeriModule *veri_module = veri_lib ? veri_lib->GetModule(name, 1) : nullptr; + if (veri_module) { + log("Adding Verilog module '%s' to elaboration queue.\n", name); + veri_modules.InsertLast(veri_module); + continue; } - VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1); - VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(name); + 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); @@ -2512,6 +2851,16 @@ struct VerificPass : public Pass { log_error("Can't find module/unit '%s'.\n", name); } + 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"); Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, ¶meters); Netlist *nl; @@ -2574,7 +2923,7 @@ struct VerificPass : public Pass { } #else /* YOSYS_ENABLE_VERIFIC */ - void execute(std::vector<std::string>, RTLIL::Design *) YS_OVERRIDE { + void execute(std::vector<std::string>, RTLIL::Design *) override { log_cmd_error("This version of Yosys is built without Verific support.\n" "\n" "Use Symbiotic EDA Suite if you need Yosys+Verifc.\n" @@ -2588,7 +2937,7 @@ struct VerificPass : public Pass { struct ReadPass : public Pass { ReadPass() : Pass("read", "load HDL designs") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -2629,7 +2978,7 @@ struct ReadPass : public Pass { log("Verific support. The default is to use Verific if it is available.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { #ifdef YOSYS_ENABLE_VERIFIC static bool verific_available = !check_noverific_env(); |