From fe8226a22d6f4030a525a6792a6188817571718b Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 26 Aug 2020 10:39:57 +0200 Subject: [PATCH] Add formal apps and template generators --- frontends/verific/verific.cc | 224 ++++++++++++++++++++++++++++++++++- 1 file changed, 223 insertions(+), 1 deletion(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 632dc51fd..52047ae2b 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -54,7 +54,7 @@ USING_YOSYS_NAMESPACE # 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 < 202006 +#if SYMBIOTIC_VERIFIC_API_VERSION < 20200702 # error "Please update your version of Symbiotic EDA flavored Verific." #endif @@ -2158,6 +2158,70 @@ struct VerificPass : public Pass { log(" Dump the Verific netlist as a verilog file.\n"); log("\n"); log("\n"); + log(" verific [-work ] -pp [options] []..\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 ..\n"); + log("\n"); + log("Execute SEDA formal application on loaded Verilog files.\n"); + log("\n"); + log("Application options:\n"); + log("\n"); + log(" -blacklist \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 \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 ..\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"); @@ -2202,6 +2266,9 @@ struct VerificPass : public Pass { 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); @@ -2399,6 +2466,161 @@ struct VerificPass : public Pass { goto check_error; } + if (args[argidx] == "-app" && argidx+1 < GetSize(args)) + { + VerificFormalApplications vfa; + auto apps = vfa.GetApps(); + std::string app = args[++argidx]; + std::vector blacklists; + if (apps.find(app) == apps.end()) + log_cmd_error("Application '%s' does not exist.\n", app.c_str()); + + for (argidx++; argidx < GetSize(args); argidx++) { + if (args[argidx] == "-blacklist" && argidx+1 < GetSize(args)) { + 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+1 < GetSize(args)) { + 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"); + MapIter mi; + VeriModule *module ; + VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1); + log("Running formal application '%s'.\n", app.c_str()); + FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, module) { + vfa.Run(module,apps[app],blacklists); + } + goto check_error; + } + + if (args[argidx] == "-pp" && argidx < GetSize(args)) + { + 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 (args[argidx] == "-template" && argidx < GetSize(args)) + { + if (!(argidx < GetSize(args))) + cmd_error(args, argidx, "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 < GetSize(args))) + cmd_error(args, argidx, "No top module specified.\n"); + + 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++) { + if (generator->checkParams(args, argidx)) + continue; + if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) { + 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+1 < GetSize(args)) { + 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 = generator->generate(veri_module, ¶meters); + + 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 nl_todo, nl_done; -- 2.30.2