aboutsummaryrefslogtreecommitdiffstats
path: root/frontends/verific/verific.cc
diff options
context:
space:
mode:
Diffstat (limited to 'frontends/verific/verific.cc')
-rw-r--r--frontends/verific/verific.cc118
1 files changed, 101 insertions, 17 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 7bbda9d49..e236aaaf2 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>
@@ -54,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 < 20200801
+#if SYMBIOTIC_VERIFIC_API_VERSION < 20200902
# error "Please update your version of Symbiotic EDA flavored Verific."
#endif
@@ -864,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();
@@ -877,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;
@@ -1512,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);
@@ -2187,6 +2203,9 @@ struct VerificPass : public Pass {
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");
@@ -2475,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];
@@ -2484,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())
@@ -2509,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;
}
@@ -2563,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();
@@ -2572,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);
@@ -2588,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(),
@@ -2600,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;
}
@@ -2614,7 +2696,9 @@ struct VerificPass : public Pass {
if (err)
cmd_error(args, argidx, err);
- std::string val = generator->generate(veri_module, &parameters);
+ std::string val;
+ if (!generator->generate(veri_module, val, &parameters))
+ log_error("%s", val.c_str());
FILE *of = stdout;
if (out_filename) {
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-27 14:36:12 +0000