mirror of https://github.com/YosysHQ/yosys.git
Merge pull request #2355 from YosysHQ/verific_improvements
Add formal apps and template generators
This commit is contained in:
Miodrag Milanović
GitHub
commit
4f2b78e19a
|
|
@ -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."
|
# error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific."
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
#if SYMBIOTIC_VERIFIC_API_VERSION < 202006
|
#if SYMBIOTIC_VERIFIC_API_VERSION < 20200702
|
||||||
# error "Please update your version of Symbiotic EDA flavored Verific."
|
# error "Please update your version of Symbiotic EDA flavored Verific."
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
|
@ -2158,6 +2158,70 @@ struct VerificPass : public Pass {
|
||||||
log(" Dump the Verific netlist as a verilog file.\n");
|
log(" Dump the Verific netlist as a verilog file.\n");
|
||||||
log("\n");
|
log("\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(" -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("Use Symbiotic EDA Suite if you need Yosys+Verifc.\n");
|
||||||
log("https://www.symbioticeda.com/seda-suite\n");
|
log("https://www.symbioticeda.com/seda-suite\n");
|
||||||
log("\n");
|
log("\n");
|
||||||
|
|
@ -2202,6 +2266,9 @@ struct VerificPass : public Pass {
|
||||||
RuntimeFlags::SetVar("veri_preserve_assignments", 1);
|
RuntimeFlags::SetVar("veri_preserve_assignments", 1);
|
||||||
RuntimeFlags::SetVar("vhdl_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
|
// Workaround for VIPER #13851
|
||||||
RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
|
RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
|
||||||
|
|
||||||
|
|
@ -2399,6 +2466,161 @@ struct VerificPass : public Pass {
|
||||||
goto check_error;
|
goto check_error;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (args[argidx] == "-app" && argidx+1 < GetSize(args))
|
||||||
|
{
|
||||||
|
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());
|
||||||
|
|
||||||
|
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")
|
if (GetSize(args) > argidx && args[argidx] == "-import")
|
||||||
{
|
{
|
||||||
std::set<Netlist*> nl_todo, nl_done;
|
std::set<Netlist*> nl_todo, nl_done;
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue