#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>
#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 < 20200902
# error "Please update your version of Symbiotic EDA flavored Verific."
#endif
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') {
}
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);
}
}
}
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();
module_name += nl->Name();
module_name += ")";
}
- module_name = "\\" + module_name;
+ module_name = "\\" + sha1_if_contain_spaces(module_name);
}
netlist = nl;
module->memories[memory->name] = memory;
int number_of_bits = net->Size();
+ number_of_bits = 1 << ceil_log2(number_of_bits);
int bits_in_word = number_of_bits;
FOREACH_PORTREF_OF_NET(net, si, pr) {
if (pr->GetInst()->Type() == OPER_READ_PORT) {
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;
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);
- if ((numchunks * memory->width) != int(inst->OutputSize()))
- log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
-
for (int i = 0; i < numchunks; i++)
{
RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)};
RTLIL::SigSpec data = operatorOutput(inst).extract(i * memory->width, memory->width);
- if ((numchunks & (numchunks - 1)) != 0) {
- addr = module->Mul(NEW_ID, operatorInput1(inst), RTLIL::Const(numchunks));
- addr = module->Add(NEW_ID, addr, RTLIL::Const(i));
- }
-
RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), ID($memrd));
cell->parameters[ID::MEMID] = memory->name.str();
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);
- if ((numchunks * memory->width) != int(inst->Input2Size()))
- log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetOutput()->Name());
-
for (int i = 0; i < numchunks; i++)
{
RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)};
RTLIL::SigSpec data = operatorInput2(inst).extract(i * memory->width, memory->width);
- if ((numchunks & (numchunks - 1)) != 0) {
- addr = module->Mul(NEW_ID, operatorInput1(inst), RTLIL::Const(numchunks));
- addr = module->Add(NEW_ID, addr, RTLIL::Const(i));
- }
-
RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), ID($memwr));
cell->parameters[ID::MEMID] = memory->name.str();
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");
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);
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);
}
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);
}
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");
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");
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;
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);
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;
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;
std::set<std::string> top_mod_names;
+ InitialAssertionRewriter rw;
+ rw.RegisterCallBack();
+
if (mode_all)
{
log("Running hier_tree::ElaborateAll().\n");
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);
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;
}
#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"
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");
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();
projects / yosys.git / blobdiff