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.cc929
1 files changed, 840 insertions, 89 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 9785b8eff..17dbed067 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
@@ -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>
@@ -42,19 +43,26 @@ USING_YOSYS_NAMESPACE
#endif
#include "veri_file.h"
-#include "vhdl_file.h"
#include "hier_tree.h"
#include "VeriModule.h"
#include "VeriWrite.h"
-#include "VhdlUnits.h"
#include "VeriLibrary.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."
+#ifdef VERIFIC_VHDL_SUPPORT
+#include "vhdl_file.h"
+#include "VhdlUnits.h"
+#endif
+
+#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
+#include "InitialAssertions.h"
#endif
-#if SYMBIOTIC_VERIFIC_API_VERSION < 202006
-# error "Please update your version of Symbiotic EDA flavored Verific."
+#ifndef YOSYSHQ_VERIFIC_API_VERSION
+# error "Only YosysHQ flavored Verific is supported. Please contact office@yosyshq.com for commercial support for Yosys+Verific."
+#endif
+
+#if YOSYSHQ_VERIFIC_API_VERSION < 20210801
+# error "Please update your version of YosysHQ flavored Verific."
#endif
#ifdef __clang__
@@ -170,8 +178,10 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att
return;
if (!type_range->IsTypeEnum())
return;
+#ifdef VERIFIC_VHDL_SUPPORT
if (nl->IsFromVhdl() && strcmp(type_range->GetTypeName(), "STD_LOGIC") == 0)
return;
+#endif
auto type_name = type_range->GetTypeName();
if (!type_name)
return;
@@ -188,7 +198,7 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att
p = nullptr;
else
for (auto q = p+2; *q != '\0'; q++)
- if (*q != '0' && *q != '1') {
+ if (*q != '0' && *q != '1' && *q != 'x' && *q != 'z') {
p = nullptr;
break;
}
@@ -197,13 +207,19 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att
log_error("Expected TypeRange value '%s' to be of form <decimal>'b<binary>.\n", v);
attributes.emplace(stringf("\\enum_value_%s", p+2), RTLIL::escape_id(k));
}
+#ifdef VERIFIC_VHDL_SUPPORT
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') {
@@ -212,17 +228,22 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att
}
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);
}
+#endif
}
}
}
@@ -357,7 +378,7 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
return true;
}
- if (inst->Type() == PRIM_TRI) {
+ if ((inst->Type() == PRIM_TRI) || (inst->Type() == PRIM_BUFIF1)) {
module->addMuxGate(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
return true;
}
@@ -396,6 +417,42 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
return true;
}
+ if (inst->Type() == PRIM_DLATCHRS)
+ {
+ if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
+ module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ else
+ module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
+ net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ return true;
+ }
+
+ if (inst->Type() == PRIM_DFF)
+ {
+ VerificClocking clocking(this, inst->GetClock());
+ log_assert(clocking.disable_sig == State::S0);
+ log_assert(clocking.body_net == nullptr);
+
+ if (inst->GetAsyncCond()->IsGnd())
+ clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ else
+ clocking.addAldff(inst_name, net_map_at(inst->GetAsyncCond()), net_map_at(inst->GetAsyncVal()),
+ net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ return true;
+ }
+
+ if (inst->Type() == PRIM_DLATCH)
+ {
+ if (inst->GetAsyncCond()->IsGnd()) {
+ module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ } else {
+ RTLIL::SigSpec sig_set = module->And(NEW_ID, net_map_at(inst->GetAsyncCond()), net_map_at(inst->GetAsyncVal()));
+ RTLIL::SigSpec sig_clr = module->And(NEW_ID, net_map_at(inst->GetAsyncCond()), module->Not(NEW_ID, net_map_at(inst->GetAsyncVal())));
+ module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), sig_set, sig_clr, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ }
+ return true;
+ }
+
return false;
}
@@ -457,7 +514,7 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
return true;
}
- if (inst->Type() == PRIM_TRI) {
+ if ((inst->Type() == PRIM_TRI) || (inst->Type() == PRIM_BUFIF1)) {
cell = module->addMux(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
@@ -506,6 +563,34 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
return true;
}
+ if (inst->Type() == PRIM_DFF)
+ {
+ VerificClocking clocking(this, inst->GetClock());
+ log_assert(clocking.disable_sig == State::S0);
+ log_assert(clocking.body_net == nullptr);
+
+ if (inst->GetAsyncCond()->IsGnd())
+ cell = clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ else
+ cell = clocking.addAldff(inst_name, net_map_at(inst->GetAsyncCond()), net_map_at(inst->GetAsyncVal()),
+ net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
+ return true;
+ }
+
+ if (inst->Type() == PRIM_DLATCH)
+ {
+ if (inst->GetAsyncCond()->IsGnd()) {
+ cell = module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ } else {
+ RTLIL::SigSpec sig_set = module->And(NEW_ID, net_map_at(inst->GetAsyncCond()), net_map_at(inst->GetAsyncVal()));
+ RTLIL::SigSpec sig_clr = module->And(NEW_ID, net_map_at(inst->GetAsyncCond()), module->Not(NEW_ID, net_map_at(inst->GetAsyncVal())));
+ cell = module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), sig_set, sig_clr, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ }
+ import_attributes(cell->attributes, inst);
+ return true;
+ }
+
#define IN operatorInput(inst)
#define IN1 operatorInput1(inst)
#define IN2 operatorInput2(inst)
@@ -713,28 +798,14 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
}
if (inst->Type() == OPER_NTO1MUX) {
- cell = module->addShr(inst_name, IN2, IN1, net_map_at(inst->GetOutput()));
+ cell = module->addBmux(inst_name, IN2, IN1, net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_WIDE_NTO1MUX)
{
- SigSpec data = IN2, out = OUT;
-
- int wordsize_bits = ceil_log2(GetSize(out));
- int wordsize = 1 << wordsize_bits;
-
- SigSpec sel = {IN1, SigSpec(State::S0, wordsize_bits)};
-
- SigSpec padded_data;
- for (int i = 0; i < GetSize(data); i += GetSize(out)) {
- SigSpec d = data.extract(i, GetSize(out));
- d.extend_u0(wordsize);
- padded_data.append(d);
- }
-
- cell = module->addShr(inst_name, padded_data, sel, out);
+ cell = module->addBmux(inst_name, IN2, IN1, OUT);
import_attributes(cell->attributes, inst);
return true;
}
@@ -778,6 +849,74 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
return true;
}
+ if (inst->Type() == OPER_WIDE_DLATCHRS)
+ {
+ RTLIL::SigSpec sig_set = operatorInport(inst, "set");
+ RTLIL::SigSpec sig_reset = operatorInport(inst, "reset");
+
+ if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool())
+ cell = module->addDlatch(inst_name, net_map_at(inst->GetControl()), IN, OUT);
+ else
+ cell = module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), sig_set, sig_reset, IN, OUT);
+ import_attributes(cell->attributes, inst);
+
+ return true;
+ }
+
+ if (inst->Type() == OPER_WIDE_DFF)
+ {
+ VerificClocking clocking(this, inst->GetClock());
+ log_assert(clocking.disable_sig == State::S0);
+ log_assert(clocking.body_net == nullptr);
+
+ RTLIL::SigSpec sig_d = IN;
+ RTLIL::SigSpec sig_q = OUT;
+ RTLIL::SigSpec sig_adata = IN1;
+ RTLIL::SigSpec sig_acond = IN2;
+
+ if (sig_acond.is_fully_const() && !sig_acond.as_bool()) {
+ cell = clocking.addDff(inst_name, sig_d, sig_q);
+ import_attributes(cell->attributes, inst);
+ } else {
+ int offset = 0, width = 0;
+ for (offset = 0; offset < GetSize(sig_acond); offset += width) {
+ for (width = 1; offset+width < GetSize(sig_acond); width++)
+ if (sig_acond[offset] != sig_acond[offset+width]) break;
+ cell = clocking.addAldff(module->uniquify(inst_name), sig_acond[offset], sig_adata.extract(offset, width),
+ sig_d.extract(offset, width), sig_q.extract(offset, width));
+ import_attributes(cell->attributes, inst);
+ }
+ }
+
+ return true;
+ }
+
+ if (inst->Type() == OPER_WIDE_DLATCH)
+ {
+ RTLIL::SigSpec sig_d = IN;
+ RTLIL::SigSpec sig_q = OUT;
+ RTLIL::SigSpec sig_adata = IN1;
+ RTLIL::SigSpec sig_acond = IN2;
+
+ if (sig_acond.is_fully_const() && !sig_acond.as_bool()) {
+ cell = module->addDlatch(inst_name, net_map_at(inst->GetControl()), sig_d, sig_q);
+ import_attributes(cell->attributes, inst);
+ } else {
+ int offset = 0, width = 0;
+ for (offset = 0; offset < GetSize(sig_acond); offset += width) {
+ for (width = 1; offset+width < GetSize(sig_acond); width++)
+ if (sig_acond[offset] != sig_acond[offset+width]) break;
+ RTLIL::SigSpec sig_set = module->Mux(NEW_ID, RTLIL::SigSpec(0, width), sig_adata.extract(offset, width), sig_acond[offset]);
+ RTLIL::SigSpec sig_clr = module->Mux(NEW_ID, RTLIL::SigSpec(0, width), module->Not(NEW_ID, sig_adata.extract(offset, width)), sig_acond[offset]);
+ cell = module->addDlatchsr(module->uniquify(inst_name), net_map_at(inst->GetControl()), sig_set, sig_clr,
+ sig_d.extract(offset, width), sig_q.extract(offset, width));
+ import_attributes(cell->attributes, inst);
+ }
+ }
+
+ return true;
+ }
+
#undef IN
#undef IN1
#undef IN2
@@ -854,6 +993,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();
@@ -867,7 +1021,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;
@@ -888,6 +1042,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
} else {
log("Importing module %s.\n", RTLIL::id2cstr(module->name));
}
+ import_attributes(module->attributes, nl, nl);
SetIter si;
MapIter mi, mi2;
@@ -936,18 +1091,28 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
import_attributes(wire->attributes, portbus, nl);
- if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN)
+ bool portbus_input = portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN;
+ if (portbus_input)
wire->port_input = true;
if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_OUT)
wire->port_output = true;
for (int i = portbus->LeftIndex();; i += portbus->IsUp() ? +1 : -1) {
if (portbus->ElementAtIndex(i) && portbus->ElementAtIndex(i)->GetNet()) {
+ bool bit_input = portbus_input;
+ if (portbus->GetDir() == DIR_NONE) {
+ Port *p = portbus->ElementAtIndex(i);
+ bit_input = p->GetDir() == DIR_INOUT || p->GetDir() == DIR_IN;
+ if (bit_input)
+ wire->port_input = true;
+ if (p->GetDir() == DIR_INOUT || p->GetDir() == DIR_OUT)
+ wire->port_output = true;
+ }
net = portbus->ElementAtIndex(i)->GetNet();
RTLIL::SigBit bit(wire, i - wire->start_offset);
if (net_map.count(net) == 0)
net_map[net] = bit;
- else if (wire->port_input)
+ else if (bit_input)
module->connect(net_map_at(net), bit);
else
module->connect(bit, net_map_at(net));
@@ -974,7 +1139,6 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
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) {
@@ -1445,6 +1609,18 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
continue;
}
+ if (inst->Type() == PRIM_YOSYSHQ_INITSTATE)
+ {
+ if (verific_verbose)
+ log(" adding YosysHQ init state\n");
+ 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");
@@ -1492,7 +1668,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);
@@ -1716,30 +1892,62 @@ Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const
{
log_assert(GetSize(sig_d) == GetSize(sig_q));
- if (GetSize(init_value) != 0) {
- log_assert(GetSize(sig_q) == GetSize(init_value));
- if (sig_q.is_wire()) {
- sig_q.as_wire()->attributes[ID::init] = init_value;
+ auto set_init_attribute = [&](SigSpec &s) {
+ if (GetSize(init_value) == 0)
+ return;
+ log_assert(GetSize(s) == GetSize(init_value));
+ if (s.is_wire()) {
+ s.as_wire()->attributes[ID::init] = init_value;
} else {
- Wire *w = module->addWire(NEW_ID, GetSize(sig_q));
+ Wire *w = module->addWire(NEW_ID, GetSize(s));
w->attributes[ID::init] = init_value;
- module->connect(sig_q, w);
- sig_q = w;
+ module->connect(s, w);
+ s = w;
}
- }
+ };
if (enable_sig != State::S1)
sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
if (disable_sig != State::S0) {
- log_assert(gclk == false);
log_assert(GetSize(sig_q) == GetSize(init_value));
+
+ if (gclk) {
+ Wire *pre_d = module->addWire(NEW_ID, GetSize(sig_d));
+ Wire *post_q_w = module->addWire(NEW_ID, GetSize(sig_q));
+
+ Const initval(State::Sx, GetSize(sig_q));
+ int offset = 0;
+ for (auto c : sig_q.chunks()) {
+ if (c.wire && c.wire->attributes.count(ID::init)) {
+ Const val = c.wire->attributes.at(ID::init);
+ for (int i = 0; i < GetSize(c); i++)
+ initval[offset+i] = val[c.offset+i];
+ }
+ offset += GetSize(c);
+ }
+
+ if (!initval.is_fully_undef())
+ post_q_w->attributes[ID::init] = initval;
+
+ module->addMux(NEW_ID, sig_d, init_value, disable_sig, pre_d);
+ module->addMux(NEW_ID, post_q_w, init_value, disable_sig, sig_q);
+
+ SigSpec post_q(post_q_w);
+ set_init_attribute(post_q);
+ return module->addFf(name, pre_d, post_q);
+ }
+
+ set_init_attribute(sig_q);
return module->addAdff(name, clock_sig, disable_sig, sig_d, sig_q, init_value, posedge);
}
- if (gclk)
+ if (gclk) {
+ set_init_attribute(sig_q);
return module->addFf(name, sig_d, sig_q);
+ }
+ set_init_attribute(sig_q);
return module->addDff(name, clock_sig, sig_d, sig_q, posedge);
}
@@ -1748,6 +1956,7 @@ Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec s
log_assert(gclk == false);
log_assert(disable_sig == State::S0);
+ // FIXME: Adffe
if (enable_sig != State::S1)
sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
@@ -1759,12 +1968,48 @@ Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::Si
log_assert(gclk == false);
log_assert(disable_sig == State::S0);
+ // FIXME: Dffsre
if (enable_sig != State::S1)
sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
return module->addDffsr(name, clock_sig, sig_set, sig_clr, sig_d, sig_q, posedge);
}
+Cell *VerificClocking::addAldff(IdString name, RTLIL::SigSpec sig_aload, RTLIL::SigSpec sig_adata, SigSpec sig_d, SigSpec sig_q)
+{
+ log_assert(disable_sig == State::S0);
+
+ // FIXME: Aldffe
+ if (enable_sig != State::S1)
+ sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
+
+ if (gclk) {
+ Wire *pre_d = module->addWire(NEW_ID, GetSize(sig_d));
+ Wire *post_q = module->addWire(NEW_ID, GetSize(sig_q));
+
+ Const initval(State::Sx, GetSize(sig_q));
+ int offset = 0;
+ for (auto c : sig_q.chunks()) {
+ if (c.wire && c.wire->attributes.count(ID::init)) {
+ Const val = c.wire->attributes.at(ID::init);
+ for (int i = 0; i < GetSize(c); i++)
+ initval[offset+i] = val[c.offset+i];
+ }
+ offset += GetSize(c);
+ }
+
+ if (!initval.is_fully_undef())
+ post_q->attributes[ID::init] = initval;
+
+ module->addMux(NEW_ID, sig_d, sig_adata, sig_aload, pre_d);
+ module->addMux(NEW_ID, post_q, sig_adata, sig_aload, sig_q);
+
+ return module->addFf(name, pre_d, post_q);
+ }
+
+ return module->addAldff(name, clock_sig, sig_aload, sig_d, sig_q, sig_adata, posedge);
+}
+
// ==================================================================
struct VerificExtNets
@@ -1911,17 +2156,23 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
std::set<Netlist*> nl_todo, nl_done;
- VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
Array *netlists = NULL;
Array veri_libs, vhdl_libs;
+#ifdef VERIFIC_VHDL_SUPPORT
+ VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
+#endif
if (veri_lib) veri_libs.InsertLast(veri_lib);
Map verific_params(STRING_HASH);
for (const auto &i : parameters)
verific_params.Insert(i.first.c_str(), i.second.c_str());
+#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
+ InitialAssertions::Rewrite("work", &verific_params);
+#endif
+
if (top.empty()) {
netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
}
@@ -1942,12 +2193,13 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
}
}
+#ifdef VERIFIC_VHDL_SUPPORT
if (vhdl_lib) {
VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(top.c_str());
if (vhdl_unit)
vhdl_units.InsertLast(vhdl_unit);
}
-
+#endif
netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &verific_params);
}
@@ -1984,7 +2236,9 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
}
veri_file::Reset();
+#ifdef VERIFIC_VHDL_SUPPORT
vhdl_file::Reset();
+#endif
Libset::Reset();
verific_incdirs.clear();
verific_libdirs.clear();
@@ -2027,7 +2281,7 @@ struct VerificPass : public Pass {
log("\n");
log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
log("the language version (and before file names) to set additional verilog defines.\n");
- log("The macros SYNTHESIS and VERIFIC are defined implicitly.\n");
+ log("The macros YOSYS, SYNTHESIS, and VERIFIC are defined implicitly.\n");
log("\n");
log("\n");
log(" verific -formal <verilog-file>..\n");
@@ -2035,11 +2289,41 @@ struct VerificPass : public Pass {
log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
log("\n");
log("\n");
+#ifdef VERIFIC_VHDL_SUPPORT
log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
log("\n");
log("Load the specified VHDL files into Verific.\n");
log("\n");
log("\n");
+#endif
+ log(" verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal] <command-file>\n");
+ log("\n");
+ log("Load and execute the specified command file.\n");
+ log("Override verilog parsing mode can be set.\n");
+ log("The macros YOSYS, SYNTHESIS/FORMAL, and VERIFIC are defined implicitly.\n");
+ log("\n");
+ log("Command file parser supports following commands:\n");
+ log(" +define - defines macro\n");
+ log(" -u - upper case all identifier (makes Verilog parser case insensitive)\n");
+ log(" -v - register library name (file)\n");
+ log(" -y - register library name (directory)\n");
+ log(" +incdir - specify include dir\n");
+ log(" +libext - specify library extension\n");
+ log(" +liborder - add library in ordered list\n");
+ log(" +librescan - unresolved modules will be always searched starting with the first\n");
+ log(" library specified by -y/-v options.\n");
+ log(" -f/-file - nested -f option\n");
+ log(" -F - nested -F option\n");
+ log("\n");
+ log(" parse mode:\n");
+ log(" -ams\n");
+ log(" +systemverilogext\n");
+ log(" +v2k\n");
+ log(" +verilog1995ext\n");
+ log(" +verilog2001ext\n");
+ log(" -sverilog\n");
+ log("\n");
+ log("\n");
log(" verific [-work <libname>] {-sv|-vhdl|...} <hdl-file>\n");
log("\n");
log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n");
@@ -2144,11 +2428,85 @@ struct VerificPass : public Pass {
log(" Dump the Verific netlist as a verilog file.\n");
log("\n");
log("\n");
- log("Use Symbiotic EDA Suite if you need Yosys+Verifc.\n");
- log("https://www.symbioticeda.com/seda-suite\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 YosysHQ 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");
+#if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_FORMALAPPS)
+ 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("Contact office@symbioticeda.com for free evaluation\n");
- log("binaries of Symbiotic EDA Suite.\n");
+ log("Templates:\n");
+ log("\n");
+#if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_TEMPLATES)
+ VerificTemplateGenerator vfg;
+ log("%s\n",vfg.GetHelp().c_str());
+#else
+ log(" WARNING: Templates only available in commercial build.\n");
+ log("\n");
+#endif
+ log("\n");
+ log("\n");
+ log(" verific -cfg [<name> [<value>]]\n");
+ log("\n");
+ log("Get/set Verific runtime flags.\n");
+ log("\n");
+ log("\n");
+ log("Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.\n");
+ log("https://www.yosyshq.com/\n");
+ log("\n");
+ log("Contact office@yosyshq.com for free evaluation\n");
+ log("binaries of YosysHQ Tabby CAD Suite.\n");
log("\n");
}
#ifdef YOSYS_ENABLE_VERIFIC
@@ -2159,11 +2517,11 @@ struct VerificPass : public Pass {
if (check_noverific_env())
log_cmd_error("This version of Yosys is built without Verific support.\n"
"\n"
- "Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"
- "https://www.symbioticeda.com/seda-suite\n"
+ "Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.\n"
+ "https://www.yosyshq.com/\n"
"\n"
- "Contact office@symbioticeda.com for free evaluation\n"
- "binaries of Symbiotic EDA Suite.\n");
+ "Contact office@yosyshq.com for free evaluation\n"
+ "binaries of YosysHQ Tabby CAD Suite.\n");
log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
@@ -2172,21 +2530,31 @@ struct VerificPass : public Pass {
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);
+#ifdef VERIFIC_VHDL_SUPPORT
RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
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("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);
@@ -2197,6 +2565,8 @@ struct VerificPass : public Pass {
// 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
@@ -2293,6 +2663,65 @@ struct VerificPass : public Pass {
break;
}
+ if (GetSize(args) > argidx && (args[argidx] == "-f" || args[argidx] == "-F"))
+ {
+ unsigned verilog_mode = veri_file::VERILOG_95; // default recommended by Verific
+ bool is_formal = false;
+ const char* filename = nullptr;
+
+ Verific::veri_file::f_file_flags flags = (args[argidx] == "-f") ? veri_file::F_FILE_NONE : veri_file::F_FILE_CAPITAL;
+
+ for (argidx++; argidx < GetSize(args); argidx++) {
+ if (args[argidx] == "-vlog95") {
+ verilog_mode = veri_file::VERILOG_95;
+ continue;
+ } else if (args[argidx] == "-vlog2k") {
+ verilog_mode = veri_file::VERILOG_2K;
+ continue;
+ } else if (args[argidx] == "-sv2005") {
+ verilog_mode = veri_file::SYSTEM_VERILOG_2005;
+ continue;
+ } else if (args[argidx] == "-sv2009") {
+ verilog_mode = veri_file::SYSTEM_VERILOG_2009;
+ continue;
+ } else if (args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal") {
+ verilog_mode = veri_file::SYSTEM_VERILOG;
+ if (args[argidx] == "-formal") is_formal = true;
+ continue;
+ } else if (args[argidx].compare(0, 1, "-") == 0) {
+ cmd_error(args, argidx, "unknown option");
+ goto check_error;
+ }
+
+ if (!filename) {
+ filename = args[argidx].c_str();
+ continue;
+ } else {
+ log_cmd_error("Only one filename can be specified.\n");
+ }
+ }
+ if (!filename)
+ log_cmd_error("Filname must be specified.\n");
+
+ unsigned analysis_mode = verilog_mode; // keep default as provided by user if not defined in file
+ Array *file_names = veri_file::ProcessFFile(filename, flags, analysis_mode);
+ if (analysis_mode != verilog_mode)
+ log_warning("Provided verilog mode differs from one specified in file.\n");
+
+ veri_file::DefineMacro("YOSYS");
+ veri_file::DefineMacro("VERIFIC");
+ veri_file::DefineMacro(is_formal ? "FORMAL" : "SYNTHESIS");
+
+ 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");
+ }
+
+ delete file_names;
+ verific_import_pending = true;
+ goto check_error;
+ }
+
if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" ||
args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal"))
{
@@ -2312,6 +2741,7 @@ struct VerificPass : public Pass {
else
log_abort();
+ veri_file::DefineMacro("YOSYS");
veri_file::DefineMacro("VERIFIC");
veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS");
@@ -2340,13 +2770,16 @@ struct VerificPass : public Pass {
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;
}
+#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++)
@@ -2382,7 +2815,236 @@ struct VerificPass : public Pass {
verific_import_pending = true;
goto check_error;
}
+#endif
+
+#ifdef YOSYSHQ_VERIFIC_FORMALAPPS
+ 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;
+ }
+#endif
+ 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++) {
+#ifdef VERIFIC_VHDL_SUPPORT
+ if (args[argidx] == "-vhdl") {
+ mode_vhdl = true;
+ continue;
+ }
+#endif
+ 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)
+#ifdef VERIFIC_VHDL_SUPPORT
+ vhdl_file::PrettyPrint(filename, module, work.c_str());
+#else
+ goto check_error;
+#endif
+ else
+ veri_file::PrettyPrint(filename, module, work.c_str());
+ goto check_error;
+ }
+
+#ifdef YOSYSHQ_VERIFIC_TEMPLATES
+ 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, &parameters))
+ 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;
+ }
+#endif
if (GetSize(args) > argidx && args[argidx] == "-import")
{
std::set<Netlist*> nl_todo, nl_done;
@@ -2467,15 +3129,20 @@ struct VerificPass : public Pass {
std::set<std::string> top_mod_names;
+#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
+ InitialAssertions::Rewrite(work, &parameters);
+#endif
if (mode_all)
{
log("Running hier_tree::ElaborateAll().\n");
- VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
Array veri_libs, vhdl_libs;
+#ifdef VERIFIC_VHDL_SUPPORT
+ VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
+#endif
if (veri_lib) veri_libs.InsertLast(veri_lib);
Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &parameters);
@@ -2491,40 +3158,44 @@ struct VerificPass : public Pass {
if (argidx == GetSize(args))
cmd_error(args, argidx, "No top module specified.\n");
+ VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
+#ifdef VERIFIC_VHDL_SUPPORT
+ VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
+#endif
+
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);
+#ifdef VERIFIC_VHDL_SUPPORT
+ 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);
continue;
}
-
+#endif
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, &parameters);
Netlist *nl;
@@ -2571,7 +3242,9 @@ struct VerificPass : public Pass {
}
veri_file::Reset();
+#ifdef VERIFIC_VHDL_SUPPORT
vhdl_file::Reset();
+#endif
Libset::Reset();
verific_incdirs.clear();
verific_libdirs.clear();
@@ -2579,6 +3252,65 @@ struct VerificPass : public Pass {
goto check_error;
}
+ if (argidx < GetSize(args) && args[argidx] == "-cfg")
+ {
+ if (argidx+1 == GetSize(args)) {
+ MapIter mi;
+ const char *k, *s;
+ unsigned long v;
+ pool<std::string> lines;
+ FOREACH_MAP_ITEM(RuntimeFlags::GetVarMap(), mi, &k, &v) {
+ lines.insert(stringf("%s %lu", k, v));
+ }
+ FOREACH_MAP_ITEM(RuntimeFlags::GetStringVarMap(), mi, &k, &s) {
+ if (s == nullptr)
+ lines.insert(stringf("%s NULL", k));
+ else
+ lines.insert(stringf("%s \"%s\"", k, s));
+ }
+ lines.sort();
+ for (auto &line : lines)
+ log("verific -cfg %s\n", line.c_str());
+ goto check_error;
+ }
+
+ if (argidx+2 == GetSize(args)) {
+ const char *k = args[argidx+1].c_str();
+ if (RuntimeFlags::HasUnsignedVar(k)) {
+ log("verific -cfg %s %lu\n", k, RuntimeFlags::GetVar(k));
+ goto check_error;
+ }
+ if (RuntimeFlags::HasStringVar(k)) {
+ const char *s = RuntimeFlags::GetStringVar(k);
+ if (s == nullptr)
+ log("verific -cfg %s NULL\n", k);
+ else
+ log("verific -cfg %s \"%s\"\n", k, s);
+ goto check_error;
+ }
+ log_cmd_error("Can't find Verific Runtime flag '%s'.\n", k);
+ }
+
+ if (argidx+3 == GetSize(args)) {
+ const auto &k = args[argidx+1], &v = args[argidx+2];
+ if (v == "NULL") {
+ RuntimeFlags::SetStringVar(k.c_str(), nullptr);
+ goto check_error;
+ }
+ if (v[0] == '"') {
+ std::string s = v.substr(1, GetSize(v)-2);
+ RuntimeFlags::SetStringVar(k.c_str(), v.c_str());
+ goto check_error;
+ }
+ char *endptr;
+ unsigned long n = strtol(v.c_str(), &endptr, 0);
+ if (*endptr == 0) {
+ RuntimeFlags::SetVar(k.c_str(), n);
+ goto check_error;
+ }
+ }
+ }
+
cmd_error(args, argidx, "Missing or unsupported mode parameter.\n");
check_error:
@@ -2590,11 +3322,11 @@ struct VerificPass : public Pass {
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"
- "https://www.symbioticeda.com/seda-suite\n"
+ "Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.\n"
+ "https://www.yosyshq.com/\n"
"\n"
- "Contact office@symbioticeda.com for free evaluation\n"
- "binaries of Symbiotic EDA Suite.\n");
+ "Contact office@yosyshq.com for free evaluation\n"
+ "binaries of YosysHQ Tabby CAD Suite.\n");
}
#endif
} VerificPass;
@@ -2614,11 +3346,19 @@ struct ReadPass : public Pass {
log("the language version (and before file names) to set additional verilog defines.\n");
log("\n");
log("\n");
+#ifdef VERIFIC_VHDL_SUPPORT
log(" read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
log("\n");
log("Load the specified VHDL files. (Requires Verific.)\n");
log("\n");
log("\n");
+#endif
+ log(" read {-f|-F} <command-file>\n");
+ log("\n");
+ log("Load and execute the specified command file. (Requires Verific.)\n");
+ log("Check verific command for more information about supported commands in file.\n");
+ log("\n");
+ log("\n");
log(" read -define <macro>[=<value>]..\n");
log("\n");
log("Set global Verilog/SystemVerilog defines.\n");
@@ -2695,6 +3435,7 @@ struct ReadPass : public Pass {
return;
}
+#ifdef VERIFIC_VHDL_SUPPORT
if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl") {
if (use_verific) {
args[0] = "verific";
@@ -2704,6 +3445,16 @@ struct ReadPass : public Pass {
}
return;
}
+#endif
+ if (args[1] == "-f" || args[1] == "-F") {
+ 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;
+ }
if (args[1] == "-define") {
if (use_verific) {
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 21:26:23 +0000