From c8f052bbe0526cae6ca88291a484d8945e2b00dd Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 12 Oct 2020 14:56:15 +0200 Subject: [PATCH] extend verific library API for formal apps and generators --- frontends/verific/verific.cc | 98 ++++++++++++++++++++++++++++++------ 1 file changed, 83 insertions(+), 15 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 05c4ec344..e236aaaf2 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -55,7 +55,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 < 20200901 +#if SYMBIOTIC_VERIFIC_API_VERSION < 20200902 # error "Please update your version of Symbiotic EDA flavored Verific." #endif @@ -2203,6 +2203,9 @@ struct VerificPass : public Pass { log("\n"); log("Application options:\n"); log("\n"); + log(" -module \n"); + log(" Run formal application only on specified module.\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"); @@ -2491,8 +2494,11 @@ struct VerificPass : public Pass { goto check_error; } - if (argidx+1 < GetSize(args) && args[argidx] == "-app") + 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]; @@ -2500,15 +2506,42 @@ struct VerificPass : public Pass { 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++) { - if (args[argidx] == "-blacklist" && argidx+1 < GetSize(args)) { + 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+1 < GetSize(args)) { + 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()) @@ -2525,12 +2558,32 @@ struct VerificPass : public Pass { } 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; - 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); + + 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; } @@ -2579,8 +2632,8 @@ struct VerificPass : public Pass { if (argidx < GetSize(args) && args[argidx] == "-template") { - if (!(argidx < GetSize(args))) - cmd_error(args, argidx, "No template type specified.\n"); + if (!(argidx+1 < GetSize(args))) + cmd_error(args, argidx+1, "No template type specified.\n"); VerificTemplateGenerator vfg; auto gens = vfg.GetGenerators(); @@ -2588,8 +2641,9 @@ struct VerificPass : public Pass { 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"); + 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); @@ -2604,9 +2658,19 @@ struct VerificPass : public Pass { const char *out_filename = nullptr; for (argidx++; argidx < GetSize(args); argidx++) { - if (generator->checkParams(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+2 < GetSize(args)) { + } + + 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(), @@ -2616,7 +2680,9 @@ struct VerificPass : public Pass { continue; } - if (args[argidx] == "-out" && argidx+1 < GetSize(args)) { + 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; } @@ -2630,7 +2696,9 @@ struct VerificPass : public Pass { if (err) cmd_error(args, argidx, err); - std::string val = generator->generate(veri_module, ¶meters); + std::string val; + if (!generator->generate(veri_module, val, ¶meters)) + log_error("%s", val.c_str()); FILE *of = stdout; if (out_filename) { -- 2.30.2