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.cc623
1 files changed, 514 insertions, 109 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 5e610c0f3..c1e9fc7d0 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -47,20 +47,27 @@ USING_YOSYS_NAMESPACE
#include "VeriModule.h"
#include "VeriWrite.h"
#include "VeriLibrary.h"
+#include "VeriExpression.h"
#ifdef VERIFIC_VHDL_SUPPORT
#include "vhdl_file.h"
#include "VhdlUnits.h"
#endif
+#ifdef VERIFIC_EDIF_SUPPORT
+#include "edif_file.h"
+#endif
+
+#ifdef VERIFIC_LIBERTY_SUPPORT
+#include "synlib_file.h"
+#include "SynlibGroup.h"
+#endif
+
#include "VerificStream.h"
#include "FileSystem.h"
#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
-#include "InitialAssertions.h"
-#include "VerificBasePass.h"
-#include "TemplateGenerator.h"
-#include "FormalApplication.h"
+#include "VerificExtensions.h"
#endif
#ifndef YOSYSHQ_VERIFIC_API_VERSION
@@ -152,7 +159,7 @@ public:
}
};
-static YosysStreamCallBackHandler stream_cb;
+YosysStreamCallBackHandler verific_read_cb;
// ==================================================================
@@ -188,11 +195,41 @@ RTLIL::IdString VerificImporter::new_verific_id(Verific::DesignObj *obj)
{
std::string s = stringf("$verific$%s", obj->Name());
if (obj->Linefile())
- s += stringf("$%s:%d", Verific::LineFile::GetFileName(obj->Linefile()), Verific::LineFile::GetLineNo(obj->Linefile()));
+ s += stringf("$%s:%d", RTLIL::encode_filename(Verific::LineFile::GetFileName(obj->Linefile())).c_str(), Verific::LineFile::GetLineNo(obj->Linefile()));
s += stringf("$%d", autoidx++);
return s;
}
+static bool isNumber(const string& str)
+{
+ for (auto &c : str) {
+ if (std::isdigit(c) == 0) return false;
+ }
+ return true;
+}
+
+// When used as attributes or parameter values Verific constants come already processed.
+// - Real string values are already under quotes
+// - Numeric values with specified width are always converted to binary
+// - Rest of user defined values are handled as 32bit integers
+// - There could be some internal values that are strings without quotes
+// so we check if value is all digits or not
+//
+static const RTLIL::Const verific_const(const char *value)
+{
+ std::string val = std::string(value);
+ if (val.size()>1 && val[0]=='\"' && val.back()=='\"')
+ return RTLIL::Const(val.substr(1,val.size()-2));
+ else
+ if (val.find("'b") != std::string::npos)
+ return RTLIL::Const::from_string(val.substr(val.find("'b") + 2));
+ else
+ if (isNumber(val))
+ return RTLIL::Const(std::stoi(val),32);
+ else
+ return RTLIL::Const(val);
+}
+
void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj, Netlist *nl)
{
MapIter mi;
@@ -201,14 +238,10 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att
if (obj->Linefile())
attributes[ID::src] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
- // FIXME: Parse numeric attributes
FOREACH_ATTRIBUTE(obj, mi, attr) {
if (attr->Key()[0] == ' ' || attr->Value() == nullptr)
continue;
- std::string val = std::string(attr->Value());
- if (val.size()>1 && val[0]=='\"' && val.back()=='\"')
- val = val.substr(1,val.size()-2);
- attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(val);
+ attributes[RTLIL::escape_id(attr->Key())] = verific_const(attr->Value());
}
if (nl) {
@@ -328,10 +361,16 @@ RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portn
for (unsigned i = 0; i < portbus->Size(); i++) {
Net *net = inst->GetNet(portbus->ElementAtIndex(i));
if (net) {
- if (net->IsGnd())
- sig.append(RTLIL::State::S0);
- else if (net->IsPwr())
- sig.append(RTLIL::State::S1);
+ if (net->IsConstant()) {
+ if (net->IsGnd())
+ sig.append(RTLIL::State::S0);
+ else if (net->IsPwr())
+ sig.append(RTLIL::State::S1);
+ else if (net->IsX())
+ sig.append(RTLIL::State::Sx);
+ else
+ sig.append(RTLIL::State::Sz);
+ }
else
sig.append(net_map_at(net));
} else
@@ -346,6 +385,36 @@ RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portn
}
}
+RTLIL::SigSpec VerificImporter::operatorInportCase(Instance *inst, const char *portname)
+{
+ PortBus *portbus = inst->View()->GetPortBus(portname);
+ if (portbus) {
+ RTLIL::SigSpec sig;
+ for (unsigned i = 0; i < portbus->Size(); i++) {
+ Net *net = inst->GetNet(portbus->ElementAtIndex(i));
+ if (net) {
+ if (net->IsConstant()) {
+ if (net->IsGnd())
+ sig.append(RTLIL::State::S0);
+ else if (net->IsPwr())
+ sig.append(RTLIL::State::S1);
+ else
+ sig.append(RTLIL::State::Sa);
+ }
+ else
+ sig.append(net_map_at(net));
+ } else
+ sig.append(RTLIL::State::Sa);
+ }
+ return sig;
+ } else {
+ Port *port = inst->View()->GetPort(portname);
+ log_assert(port != NULL);
+ Net *net = inst->GetNet(port);
+ return net_map_at(net);
+ }
+}
+
RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst, const pool<Net*, hash_ptr_ops> *any_all_nets)
{
RTLIL::SigSpec sig;
@@ -956,6 +1025,47 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
return true;
}
+ if (inst->Type() == OPER_WIDE_CASE_SELECT_BOX)
+ {
+ RTLIL::SigSpec sig_out_val = operatorInport(inst, "out_value");
+ RTLIL::SigSpec sig_select = operatorInport(inst, "select");
+ RTLIL::SigSpec sig_select_values = operatorInportCase(inst, "select_values");
+ RTLIL::SigSpec sig_data_values = operatorInport(inst, "data_values");
+ RTLIL::SigSpec sig_data_default = operatorInport(inst, "default_value");
+
+ RTLIL::Process *proc = module->addProcess(new_verific_id(inst));
+ import_attributes(proc->attributes, inst);
+
+ RTLIL::CaseRule *current_case = &proc->root_case;
+ current_case = &proc->root_case;
+
+ RTLIL::SwitchRule *sw = new RTLIL::SwitchRule;
+ sw->signal = sig_select;
+ current_case->switches.push_back(sw);
+
+ int select_width = inst->InputSize();
+ int data_width = inst->OutputSize();
+ int select_num = inst->Input1Size() / inst->InputSize();
+
+ int offset_select = 0;
+ int offset_data = 0;
+
+ for (int i = 0; i < select_num; i++) {
+ RTLIL::CaseRule *cs = new RTLIL::CaseRule;
+ cs->compare.push_back(sig_select_values.extract(offset_select, select_width));
+ cs->actions.push_back(SigSig(sig_out_val, sig_data_values.extract(offset_data, data_width)));
+ sw->cases.push_back(cs);
+
+ offset_select += select_width;
+ offset_data += data_width;
+ }
+ RTLIL::CaseRule *cs_default = new RTLIL::CaseRule;
+ cs_default->actions.push_back(SigSig(sig_out_val, sig_data_default));
+ sw->cases.push_back(cs_default);
+
+ return true;
+ }
+
#undef IN
#undef IN1
#undef IN2
@@ -1092,6 +1202,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
NetBus *netbus;
Instance *inst;
PortRef *pr;
+ Att *attr;
+
+ FOREACH_ATTRIBUTE(nl, mi, attr) {
+ if (!strcmp(attr->Key(), "noblackbox"))
+ module->set_bool_attribute(ID::blackbox, false);
+ }
FOREACH_PORT_OF_NETLIST(nl, mi, port)
{
@@ -1129,6 +1245,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size());
wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
+ wire->upto = portbus->IsUp();
import_attributes(wire->attributes, portbus, nl);
bool portbus_input = portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN;
@@ -1149,7 +1266,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
wire->port_output = true;
}
net = portbus->ElementAtIndex(i)->GetNet();
- RTLIL::SigBit bit(wire, i - wire->start_offset);
+ int bitidx = wire->upto ? (wire->width - 1 - (i - wire->start_offset)) : (i - wire->start_offset);
+ RTLIL::SigBit bit(wire, bitidx);
if (net_map.count(net) == 0)
net_map[net] = bit;
else if (bit_input)
@@ -1177,6 +1295,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
memory->name = RTLIL::escape_id(net->Name());
log_assert(module->count_id(memory->name) == 0);
module->memories[memory->name] = memory;
+ import_attributes(memory->attributes, net, nl);
int number_of_bits = net->Size();
int bits_in_word = number_of_bits;
@@ -1313,6 +1432,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
+ wire->upto = netbus->IsUp();
MapIter mibus;
FOREACH_NET_OF_NETBUS(netbus, mibus, net) {
if (net)
@@ -1327,7 +1447,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
{
if (netbus->ElementAtIndex(i))
{
- int bitidx = i - wire->start_offset;
+ int bitidx = wire->upto ? (wire->width - 1 - (i - wire->start_offset)) : (i - wire->start_offset);
net = netbus->ElementAtIndex(i);
RTLIL::SigBit bit(wire, bitidx);
@@ -2231,7 +2351,7 @@ struct VerificExtNets
}
};
-void verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top)
+std::string verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top)
{
verific_sva_fsm_limit = 16;
@@ -2251,7 +2371,8 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
verific_params.Insert(i.first.c_str(), i.second.c_str());
#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
- InitialAssertions::Rewrite("work", &verific_params);
+ VerificExtensions::ElaborateAndRewrite("work", &verific_params);
+ verific_error_msg.clear();
#endif
if (top.empty()) {
@@ -2264,6 +2385,18 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
VeriModule *veri_module = veri_lib->GetModule(top.c_str(), 1);
if (veri_module) {
veri_modules.InsertLast(veri_module);
+ if (veri_module->IsConfiguration()) {
+ VeriConfiguration *cfg = (VeriConfiguration*)veri_module;
+ VeriName *module_name = (VeriName*)cfg->GetTopModuleNames()->GetLast();
+ VeriLibrary *lib = veri_module->GetLibrary() ;
+ if (module_name && module_name->IsHierName()) {
+ VeriName *prefix = module_name->GetPrefix() ;
+ const char *lib_name = (prefix) ? prefix->GetName() : 0 ;
+ if (!Strings::compare("work", lib_name)) lib = veri_file::GetLibrary(lib_name, 1) ;
+ }
+ if (lib && module_name)
+ top = lib->GetModule(module_name->GetName(), 1)->GetName();
+ }
}
// Also elaborate all root modules since they may contain bind statements
@@ -2288,6 +2421,7 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
int i;
FOREACH_ARRAY_ITEM(netlists, i, nl) {
+ if (!nl) continue;
if (!top.empty() && nl->CellBaseName() != top)
continue;
nl->AddAtt(new Att(" \\top", NULL));
@@ -2317,11 +2451,20 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
nl_todo.erase(it);
}
+#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
+ VerificExtensions::Reset();
+#endif
hier_tree::DeleteHierarchicalTree();
veri_file::Reset();
#ifdef VERIFIC_VHDL_SUPPORT
vhdl_file::Reset();
#endif
+#ifdef VERIFIC_EDIF_SUPPORT
+ edif_file::Reset();
+#endif
+#ifdef VERIFIC_LIBERTY_SUPPORT
+ synlib_file::Reset();
+#endif
Libset::Reset();
Message::Reset();
RuntimeFlags::DeleteAllFlags();
@@ -2333,6 +2476,7 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
if (!verific_error_msg.empty())
log_error("%s\n", verific_error_msg.c_str());
+ return top;
}
YOSYS_NAMESPACE_END
@@ -2350,64 +2494,6 @@ bool check_noverific_env()
return false;
return true;
}
-
-void set_verific_global_flags()
-{
- static bool g_set_verific_global_flags = true;
-
- if (g_set_verific_global_flags)
- {
- Message::SetConsoleOutput(0);
- Message::RegisterCallBackMsg(msg_func);
-
- RuntimeFlags::SetVar("db_preserve_user_instances", 1);
- RuntimeFlags::SetVar("db_preserve_user_nets", 1);
- RuntimeFlags::SetVar("db_preserve_x", 1);
-
- RuntimeFlags::SetVar("db_allow_external_nets", 1);
- RuntimeFlags::SetVar("db_infer_wide_operators", 1);
- RuntimeFlags::SetVar("db_infer_set_reset_registers", 0);
-
- RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
- RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
- RuntimeFlags::SetVar("veri_allow_any_ram_in_loop", 1);
-
-#ifdef VERIFIC_VHDL_SUPPORT
- RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
- RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
- RuntimeFlags::SetVar("vhdl_allow_any_ram_in_loop", 1);
-
- RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
- RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
-
- RuntimeFlags::SetVar("vhdl_preserve_assignments", 1);
- //RuntimeFlags::SetVar("vhdl_preserve_comments", 1);
- RuntimeFlags::SetVar("vhdl_preserve_drivers", 1);
-#endif
- RuntimeFlags::SetVar("veri_preserve_assignments", 1);
- RuntimeFlags::SetVar("veri_preserve_comments", 1);
- RuntimeFlags::SetVar("veri_preserve_drivers", 1);
-
- // Workaround for VIPER #13851
- RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
-
- // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
- Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
-
- // https://github.com/YosysHQ/yosys/issues/1055
- RuntimeFlags::SetVar("veri_elaborate_top_level_modules_having_interface_ports", 1) ;
-
- RuntimeFlags::SetVar("verific_produce_verbose_syntax_error_message", 1);
-
-#ifndef DB_PRESERVE_INITIAL_VALUE
-# warning Verific was built without DB_PRESERVE_INITIAL_VALUE.
-#endif
-
- veri_file::RegisterCallBackVerificStream(&stream_cb);
-
- g_set_verific_global_flags = false;
- }
-}
#endif
struct VerificPass : public Pass {
@@ -2441,6 +2527,25 @@ struct VerificPass : public Pass {
log("\n");
log("\n");
#endif
+#ifdef VERIFIC_EDIF_SUPPORT
+ log(" verific {-edif} <edif-file>..\n");
+ log("\n");
+ log("Load the specified EDIF files into Verific.\n");
+ log("\n");
+ log("\n");
+#endif
+#ifdef VERIFIC_LIBERTY_SUPPORT
+ log(" verific {-liberty} <liberty-file>..\n");
+ log("\n");
+ log("Load the specified Liberty files into Verific.\n");
+ log("Default library when -work is not present is one specified in liberty file.\n");
+ log("To use from SystemVerilog or VHDL use -L to specify liberty library.");
+ log("\n");
+ log(" -lib\n");
+ log(" only create empty blackbox modules\n");
+ log("\n");
+ log("\n");
+#endif
log(" verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|\n");
log(" -sv2012|-sv|-formal] <command-file>\n");
log("\n");
@@ -2519,12 +2624,14 @@ struct VerificPass : public Pass {
log("\n");
log("Set message severity. <msg_id> is the string in square brackets when a message\n");
log("is printed, such as VERI-1209.\n");
+ log("Also errors, warnings, infos and comments could be used to set new severity for\n");
+ log("all messages of certain type.\n");
log("\n");
log("\n");
- log(" verific -import [options] <top-module>..\n");
+ log(" verific -import [options] <top>..\n");
log("\n");
- log("Elaborate the design for the specified top modules, import to Yosys and\n");
- log("reset the internal state of Verific.\n");
+ log("Elaborate the design for the specified top modules or configurations, import to\n");
+ log("Yosys and reset the internal state of Verific.\n");
log("\n");
log("Import options:\n");
log("\n");
@@ -2547,6 +2654,10 @@ struct VerificPass : public Pass {
log(" -fullinit\n");
log(" Keep all register initializations, even those for non-FF registers.\n");
log("\n");
+ log(" -cells\n");
+ log(" Import all cell definitions from Verific loaded libraries even if they are\n");
+ log(" unused in design. Useful with \"-edif\" and \"-liberty\" option.\n");
+ log("\n");
log(" -chparam name value \n");
log(" Elaborate the specified top modules (all modules when -all given) using\n");
log(" this parameter value. Modules on which this parameter does not exist will\n");
@@ -2557,6 +2668,9 @@ struct VerificPass : public Pass {
log(" -v, -vv\n");
log(" Verbose log messages. (-vv is even more verbose than -v.)\n");
log("\n");
+ log(" -pp <filename>\n");
+ log(" Pretty print design after elaboration to specified file.\n");
+ log("\n");
log("The following additional import options are useful for debugging the Verific\n");
log("bindings (for Yosys and/or Verific developers):\n");
log("\n");
@@ -2602,6 +2716,9 @@ struct VerificPass : public Pass {
log("Get/set Verific runtime flags.\n");
log("\n");
log("\n");
+#if defined(YOSYS_ENABLE_VERIFIC) and defined(YOSYSHQ_VERIFIC_EXTENSIONS)
+ VerificExtensions::Help();
+#endif
log("Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.\n");
log("https://www.yosyshq.com/\n");
log("\n");
@@ -2610,8 +2727,49 @@ struct VerificPass : public Pass {
log("\n");
}
#ifdef YOSYS_ENABLE_VERIFIC
+ std::string frontent_rewrite(std::vector<std::string> &args, int &argidx, std::vector<std::string> &tmp_files)
+ {
+ std::string filename = args[argidx++];
+ //Accommodate heredocs with EOT marker spaced out from "<<", e.g. "<< EOT" vs. "<<EOT"
+ if (filename == "<<" && (argidx < GetSize(args))) {
+ filename += args[argidx++];
+ }
+ if (filename.compare(0, 2, "<<") == 0) {
+ if (filename.size() <= 2)
+ log_error("Missing EOT marker in here document!\n");
+ std::string eot_marker = filename.substr(2);
+ if (Frontend::current_script_file == nullptr)
+ filename = "<stdin>";
+ std::string last_here_document;
+ while (1) {
+ std::string buffer;
+ char block[4096];
+ while (1) {
+ if (fgets(block, 4096, Frontend::current_script_file == nullptr? stdin : Frontend::current_script_file) == nullptr)
+ log_error("Unexpected end of file in here document '%s'!\n", filename.c_str());
+ buffer += block;
+ if (buffer.size() > 0 && (buffer[buffer.size() - 1] == '\n' || buffer[buffer.size() - 1] == '\r'))
+ break;
+ }
+ size_t indent = buffer.find_first_not_of(" \t\r\n");
+ if (indent != std::string::npos && buffer.compare(indent, eot_marker.size(), eot_marker) == 0)
+ break;
+ last_here_document += buffer;
+ }
+ filename = make_temp_file();
+ tmp_files.push_back(filename);
+ std::ofstream file(filename);
+ file << last_here_document;
+ } else {
+ rewrite_filename(filename);
+ }
+ return filename;
+ }
+
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
+ static bool set_verific_global_flags = true;
+
if (check_noverific_env())
log_cmd_error("This version of Yosys is built without Verific support.\n"
"\n"
@@ -2623,7 +2781,56 @@ struct VerificPass : public Pass {
log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
- set_verific_global_flags();
+ if (set_verific_global_flags)
+ {
+ Message::SetConsoleOutput(0);
+ Message::RegisterCallBackMsg(msg_func);
+
+ RuntimeFlags::SetVar("db_preserve_user_instances", 1);
+ RuntimeFlags::SetVar("db_preserve_user_nets", 1);
+ RuntimeFlags::SetVar("db_preserve_x", 1);
+
+ RuntimeFlags::SetVar("db_allow_external_nets", 1);
+ RuntimeFlags::SetVar("db_infer_wide_operators", 1);
+ RuntimeFlags::SetVar("db_infer_set_reset_registers", 0);
+
+ RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
+ RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
+ RuntimeFlags::SetVar("veri_allow_any_ram_in_loop", 1);
+
+#ifdef VERIFIC_VHDL_SUPPORT
+ RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
+ RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
+ RuntimeFlags::SetVar("vhdl_allow_any_ram_in_loop", 1);
+
+ RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
+ RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
+
+ RuntimeFlags::SetVar("vhdl_preserve_assignments", 1);
+ //RuntimeFlags::SetVar("vhdl_preserve_comments", 1);
+ RuntimeFlags::SetVar("vhdl_preserve_drivers", 1);
+#endif
+ RuntimeFlags::SetVar("veri_preserve_assignments", 1);
+ RuntimeFlags::SetVar("veri_preserve_comments", 1);
+ RuntimeFlags::SetVar("veri_preserve_drivers", 1);
+
+ // Workaround for VIPER #13851
+ RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
+
+ // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
+ Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
+
+ // https://github.com/YosysHQ/yosys/issues/1055
+ RuntimeFlags::SetVar("veri_elaborate_top_level_modules_having_interface_ports", 1) ;
+
+ RuntimeFlags::SetVar("verific_produce_verbose_syntax_error_message", 1);
+
+#ifndef DB_PRESERVE_INITIAL_VALUE
+# warning Verific was built without DB_PRESERVE_INITIAL_VALUE.
+#endif
+
+ set_verific_global_flags = false;
+ }
verific_verbose = 0;
verific_sva_fsm_limit = 16;
@@ -2631,6 +2838,7 @@ struct VerificPass : public Pass {
const char *release_str = Message::ReleaseString();
time_t release_time = Message::ReleaseDate();
char *release_tmstr = ctime(&release_time);
+ std::vector<std::string> tmp_files;
if (release_str == nullptr)
release_str = "(no release string)";
@@ -2642,6 +2850,8 @@ struct VerificPass : public Pass {
int argidx = 1;
std::string work = "work";
+ bool is_work_set = false;
+ veri_file::RegisterCallBackVerificStream(&verific_read_cb);
if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
@@ -2659,9 +2869,20 @@ struct VerificPass : public Pass {
else
log_abort();
- for (argidx++; argidx < GetSize(args); argidx++)
- Message::SetMessageType(args[argidx].c_str(), new_type);
-
+ for (argidx++; argidx < GetSize(args); argidx++) {
+ if (Strings::compare(args[argidx].c_str(), "errors")) {
+ Message::SetMessageType("VERI-1063", new_type);
+ Message::SetAllMessageType(VERIFIC_ERROR, new_type);
+ } else if (Strings::compare(args[argidx].c_str(), "warnings")) {
+ Message::SetAllMessageType(VERIFIC_WARNING, new_type);
+ } else if (Strings::compare(args[argidx].c_str(), "infos")) {
+ Message::SetAllMessageType(VERIFIC_INFO, new_type);
+ } else if (Strings::compare(args[argidx].c_str(), "comments")) {
+ Message::SetAllMessageType(VERIFIC_COMMENT, new_type);
+ } else {
+ Message::SetMessageType(args[argidx].c_str(), new_type);
+ }
+ }
goto check_error;
}
@@ -2707,10 +2928,25 @@ struct VerificPass : public Pass {
}
veri_file::RemoveAllLOptions();
+ veri_file::AddLOption("work");
+ for (int i = argidx; i < GetSize(args); i++)
+ {
+ if (args[i] == "-work" && i+1 < GetSize(args)) {
+ ++i;
+ continue;
+ }
+ if (args[i] == "-L" && i+1 < GetSize(args)) {
+ if (args[++i] == "work")
+ veri_file::RemoveAllLOptions();
+ continue;
+ }
+ break;
+ }
for (; argidx < GetSize(args); argidx++)
{
if (args[argidx] == "-work" && argidx+1 < GetSize(args)) {
work = args[++argidx];
+ is_work_set = true;
continue;
}
if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
@@ -2826,9 +3062,10 @@ struct VerificPass : public Pass {
for (auto &ext : verific_libexts)
veri_file::AddLibExt(ext.c_str());
- while (argidx < GetSize(args))
- file_names.Insert(args[argidx++].c_str());
-
+ while (argidx < GetSize(args)) {
+ std::string filename = frontent_rewrite(args, argidx, tmp_files);
+ file_names.Insert(strdup(filename.c_str()));
+ }
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");
@@ -2841,41 +3078,100 @@ struct VerificPass : public Pass {
#ifdef VERIFIC_VHDL_SUPPORT
if (GetSize(args) > argidx && args[argidx] == "-vhdl87") {
vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
- for (argidx++; argidx < GetSize(args); argidx++)
- if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_87))
- log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str());
+ argidx++;
+ while (argidx < GetSize(args)) {
+ std::string filename = frontent_rewrite(args, argidx, tmp_files);
+ if (!vhdl_file::Analyze(filename.c_str(), work.c_str(), vhdl_file::VHDL_87))
+ log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", filename.c_str());
+ }
verific_import_pending = true;
goto check_error;
}
if (GetSize(args) > argidx && args[argidx] == "-vhdl93") {
vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
- for (argidx++; argidx < GetSize(args); argidx++)
- if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_93))
- log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str());
+ argidx++;
+ while (argidx < GetSize(args)) {
+ std::string filename = frontent_rewrite(args, argidx, tmp_files);
+ if (!vhdl_file::Analyze(filename.c_str(), work.c_str(), vhdl_file::VHDL_93))
+ log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", filename.c_str());
+ }
verific_import_pending = true;
goto check_error;
}
if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") {
vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
- for (argidx++; argidx < GetSize(args); argidx++)
- if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2K))
- log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str());
+ argidx++;
+ while (argidx < GetSize(args)) {
+ std::string filename = frontent_rewrite(args, argidx, tmp_files);
+ if (!vhdl_file::Analyze(filename.c_str(), work.c_str(), vhdl_file::VHDL_2K))
+ log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", filename.c_str());
+ }
verific_import_pending = true;
goto check_error;
}
if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) {
vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
- for (argidx++; argidx < GetSize(args); argidx++)
- if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2008))
- log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str());
+ argidx++;
+ while (argidx < GetSize(args)) {
+ std::string filename = frontent_rewrite(args, argidx, tmp_files);
+ if (!vhdl_file::Analyze(filename.c_str(), work.c_str(), vhdl_file::VHDL_2008))
+ log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", filename.c_str());
+ }
verific_import_pending = true;
goto check_error;
}
#endif
+#ifdef VERIFIC_EDIF_SUPPORT
+ if (GetSize(args) > argidx && args[argidx] == "-edif") {
+ edif_file edif;
+ argidx++;
+ while (argidx < GetSize(args)) {
+ std::string filename = frontent_rewrite(args, argidx, tmp_files);
+ if (!edif.Read(filename.c_str()))
+ log_cmd_error("Reading `%s' in EDIF mode failed.\n", filename.c_str());
+ }
+ goto check_error;
+ }
+#endif
+#ifdef VERIFIC_LIBERTY_SUPPORT
+ if (GetSize(args) > argidx && args[argidx] == "-liberty") {
+ bool flag_lib = false;
+ for (argidx++; argidx < GetSize(args); argidx++) {
+ if (args[argidx] == "-lib") {
+ flag_lib = true;
+ continue;
+ }
+ if (args[argidx].compare(0, 1, "-") == 0) {
+ cmd_error(args, argidx, "unknown option");
+ goto check_error;
+ }
+ break;
+ }
+ while (argidx < GetSize(args)) {
+ std::string filename = frontent_rewrite(args, argidx, tmp_files);
+ if (!synlib_file::Read(filename.c_str(), is_work_set ? work.c_str() : nullptr))
+ log_cmd_error("Reading `%s' in LIBERTY mode failed.\n", filename.c_str());
+ SynlibLibrary *lib = synlib_file::GetLastLibraryAnalyzed();
+ if (lib && flag_lib) {
+ MapIter mi ;
+ Verific::Cell *c ;
+ FOREACH_CELL_OF_LIBRARY(lib->GetLibrary(),mi,c) {
+ MapIter ni ;
+ Netlist *nl;
+ FOREACH_NETLIST_OF_CELL(c, ni, nl) {
+ if (nl)
+ nl->MakeBlackBox();
+ }
+ }
+ }
+ }
+ goto check_error;
+ }
+#endif
if (argidx < GetSize(args) && args[argidx] == "-pp")
{
const char* filename = nullptr;
@@ -2930,8 +3226,9 @@ struct VerificPass : public Pass {
bool mode_all = false, mode_gates = false, mode_keep = false;
bool mode_nosva = false, mode_names = false, mode_verific = false;
bool mode_autocover = false, mode_fullinit = false;
- bool flatten = false, extnets = false;
+ bool flatten = false, extnets = false, mode_cells = false;
string dumpfile;
+ string ppfile;
Map parameters(STRING_HASH);
for (argidx++; argidx < GetSize(args); argidx++) {
@@ -2975,6 +3272,10 @@ struct VerificPass : public Pass {
mode_fullinit = true;
continue;
}
+ if (args[argidx] == "-cells") {
+ mode_cells = true;
+ continue;
+ }
if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) {
const std::string &key = args[++argidx];
const std::string &value = args[++argidx];
@@ -3000,6 +3301,10 @@ struct VerificPass : public Pass {
dumpfile = args[++argidx];
continue;
}
+ if (args[argidx] == "-pp" && argidx+1 < GetSize(args)) {
+ ppfile = args[++argidx];
+ continue;
+ }
break;
}
@@ -3009,8 +3314,12 @@ struct VerificPass : public Pass {
std::set<std::string> top_mod_names;
#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
- InitialAssertions::Rewrite(work, &parameters);
+ VerificExtensions::ElaborateAndRewrite(work, &parameters);
+ verific_error_msg.clear();
#endif
+ if (!ppfile.empty())
+ veri_file::PrettyPrint(ppfile.c_str(), nullptr, work.c_str());
+
if (mode_all)
{
log("Running hier_tree::ElaborateAll().\n");
@@ -3050,8 +3359,29 @@ struct VerificPass : public Pass {
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);
+ if (veri_module->IsConfiguration()) {
+ log("Adding Verilog configuration '%s' to elaboration queue.\n", name);
+ veri_modules.InsertLast(veri_module);
+
+ top_mod_names.erase(name);
+
+ VeriConfiguration *cfg = (VeriConfiguration*)veri_module;
+ VeriName *module_name;
+ int i;
+ FOREACH_ARRAY_ITEM(cfg->GetTopModuleNames(), i, module_name) {
+ VeriLibrary *lib = veri_module->GetLibrary() ;
+ if (module_name && module_name->IsHierName()) {
+ VeriName *prefix = module_name->GetPrefix() ;
+ const char *lib_name = (prefix) ? prefix->GetName() : 0 ;
+ if (!Strings::compare("work", lib_name)) lib = veri_file::GetLibrary(lib_name, 1) ;
+ }
+ if (lib && module_name)
+ top_mod_names.insert(lib->GetModule(module_name->GetName(), 1)->GetName());
+ }
+ } else {
+ log("Adding Verilog module '%s' to elaboration queue.\n", name);
+ veri_modules.InsertLast(veri_module);
+ }
continue;
}
#ifdef VERIFIC_VHDL_SUPPORT
@@ -3081,6 +3411,7 @@ struct VerificPass : public Pass {
int i;
FOREACH_ARRAY_ITEM(netlists, i, nl) {
+ if (!nl) continue;
if (!top_mod_names.count(nl->CellBaseName()))
continue;
nl->AddAtt(new Att(" \\top", NULL));
@@ -3088,6 +3419,28 @@ struct VerificPass : public Pass {
}
delete netlists;
}
+ if (mode_cells) {
+ log("Importing all cells.\n");
+ Libset *gls = Libset::Global() ;
+ MapIter it ;
+ Library *l ;
+ FOREACH_LIBRARY_OF_LIBSET(gls,it,l) {
+ MapIter mi ;
+ Verific::Cell *c ;
+ FOREACH_CELL_OF_LIBRARY(l,mi,c) {
+ if (!mode_verific && (l == Library::Primitives() || l == Library::Operators())) continue;
+ MapIter ni ;
+ if (c->NumOfNetlists() == 1) {
+ c->GetFirstNetlist()->SetName("");
+ }
+ Netlist *nl;
+ FOREACH_NETLIST_OF_CELL(c, ni, nl) {
+ if (nl)
+ nl_todo.emplace(nl->CellBaseName(), nl);
+ }
+ }
+ }
+ }
if (!verific_error_msg.empty())
goto check_error;
@@ -3123,11 +3476,20 @@ struct VerificPass : public Pass {
nl_todo.erase(it);
}
+#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
+ VerificExtensions::Reset();
+#endif
hier_tree::DeleteHierarchicalTree();
veri_file::Reset();
#ifdef VERIFIC_VHDL_SUPPORT
vhdl_file::Reset();
#endif
+#ifdef VERIFIC_EDIF_SUPPORT
+ edif_file::Reset();
+#endif
+#ifdef VERIFIC_LIBERTY_SUPPORT
+ synlib_file::Reset();
+#endif
Libset::Reset();
Message::Reset();
RuntimeFlags::DeleteAllFlags();
@@ -3197,10 +3559,24 @@ struct VerificPass : public Pass {
}
}
}
+#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
+ if (VerificExtensions::Execute(args, argidx, work,
+ [this](const std::vector<std::string> &args, size_t argidx, std::string msg)
+ { cmd_error(args, argidx, msg); } )) {
+ goto check_error;
+ }
+#endif
cmd_error(args, argidx, "Missing or unsupported mode parameter.\n");
check_error:
+ if (tmp_files.size()) {
+ log("Removing temp files.\n");
+ for(auto &fn : tmp_files) {
+ remove(fn.c_str());
+ }
+ }
+
if (!verific_error_msg.empty())
log_error("%s\n", verific_error_msg.c_str());
@@ -3218,12 +3594,6 @@ struct VerificPass : public Pass {
#endif
} VerificPass;
-
-#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
-VERIFIC_PASS(VerificTemplateGenerator, "template", "generate template")
-VERIFIC_PASS(VerificFormalApplication, "formal_app", "running formal application")
-#endif
-
struct ReadPass : public Pass {
ReadPass() : Pass("read", "load HDL designs") { }
void help() override
@@ -3246,6 +3616,21 @@ struct ReadPass : public Pass {
log("\n");
log("\n");
#endif
+#ifdef VERIFIC_EDIF_SUPPORT
+ log(" read {-edif} <edif-file>..\n");
+ log("\n");
+ log("Load the specified EDIF files. (Requires Verific.)\n");
+ log("\n");
+ log("\n");
+#endif
+ log(" read {-liberty} <liberty-file>..\n");
+ log("\n");
+ log("Load the specified Liberty files.\n");
+ log("\n");
+ log(" -lib\n");
+ log(" only create empty blackbox modules\n");
+ log("\n");
+ log("\n");
log(" read {-f|-F} <command-file>\n");
log("\n");
log("Load and execute the specified command file. (Requires Verific.)\n");
@@ -3339,6 +3724,26 @@ struct ReadPass : public Pass {
return;
}
#endif
+#ifdef VERIFIC_EDIF_SUPPORT
+ if (args[1] == "-edif") {
+ if (use_verific) {
+ args[0] = "verific";
+ Pass::call(design, args);
+ } else {
+ cmd_error(args, 1, "This version of Yosys is built without Verific support.\n");
+ }
+ return;
+ }
+#endif
+ if (args[1] == "-liberty") {
+ if (use_verific) {
+ args[0] = "verific";
+ } else {
+ args[0] = "read_liberty";
+ }
+ Pass::call(design, args);
+ return;
+ }
if (args[1] == "-f" || args[1] == "-F") {
if (use_verific) {
args[0] = "verific";
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 12:14:15 +0000