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.cc850
1 files changed, 598 insertions, 252 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 62a8028b8..c5eef4b55 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -19,6 +19,7 @@
#include "kernel/yosys.h"
#include "kernel/sigtools.h"
+#include "kernel/celltypes.h"
#include "kernel/log.h"
#include <stdlib.h>
#include <stdio.h>
@@ -46,7 +47,15 @@ USING_YOSYS_NAMESPACE
#include "VeriModule.h"
#include "VeriWrite.h"
#include "VhdlUnits.h"
-#include "Message.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."
+#endif
+
+#if SYMBIOTIC_VERIFIC_API_VERSION < 1
+# error "Please update your version of Symbiotic EDA flavored Verific."
+#endif
#ifdef __clang__
#pragma clang diagnostic pop
@@ -64,6 +73,9 @@ YOSYS_NAMESPACE_BEGIN
int verific_verbose;
bool verific_import_pending;
string verific_error_msg;
+int verific_sva_fsm_limit;
+
+vector<string> verific_incdirs, verific_libdirs;
void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
{
@@ -100,9 +112,10 @@ string get_full_netlist_name(Netlist *nl)
// ==================================================================
-VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover) :
+VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) :
mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
- mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover)
+ mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover),
+ mode_fullinit(mode_fullinit)
{
}
@@ -115,6 +128,27 @@ RTLIL::SigBit VerificImporter::net_map_at(Net *net)
return net_map.at(net);
}
+bool is_blackbox(Netlist *nl)
+{
+ if (nl->IsBlackBox())
+ return true;
+
+ const char *attr = nl->GetAttValue("blackbox");
+ if (attr != nullptr && strcmp(attr, "0"))
+ return true;
+
+ return false;
+}
+
+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("$%d", autoidx++);
+ return s;
+}
+
void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
{
MapIter mi;
@@ -200,7 +234,7 @@ RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst, const pool<Net*,
dummy_wire = NULL;
} else {
if (dummy_wire == NULL)
- dummy_wire = module->addWire(NEW_ID);
+ dummy_wire = module->addWire(new_verific_id(inst));
else
dummy_wire->width++;
sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
@@ -216,8 +250,8 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
}
if (inst->Type() == PRIM_NAND) {
- RTLIL::SigSpec tmp = module->addWire(NEW_ID);
- module->addAndGate(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
+ RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
+ module->addAndGate(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
return true;
}
@@ -228,8 +262,8 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
}
if (inst->Type() == PRIM_NOR) {
- RTLIL::SigSpec tmp = module->addWire(NEW_ID);
- module->addOrGate(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
+ RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
+ module->addOrGate(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
return true;
}
@@ -269,16 +303,16 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
if (inst->Type() == PRIM_FADD)
{
RTLIL::SigSpec a = net_map_at(inst->GetInput1()), b = net_map_at(inst->GetInput2()), c = net_map_at(inst->GetCin());
- RTLIL::SigSpec x = inst->GetCout() ? net_map_at(inst->GetCout()) : module->addWire(NEW_ID);
- RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(NEW_ID);
- RTLIL::SigSpec tmp1 = module->addWire(NEW_ID);
- RTLIL::SigSpec tmp2 = module->addWire(NEW_ID);
- RTLIL::SigSpec tmp3 = module->addWire(NEW_ID);
- module->addXorGate(NEW_ID, a, b, tmp1);
+ RTLIL::SigSpec x = inst->GetCout() ? net_map_at(inst->GetCout()) : module->addWire(new_verific_id(inst));
+ RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(new_verific_id(inst));
+ RTLIL::SigSpec tmp1 = module->addWire(new_verific_id(inst));
+ RTLIL::SigSpec tmp2 = module->addWire(new_verific_id(inst));
+ RTLIL::SigSpec tmp3 = module->addWire(new_verific_id(inst));
+ module->addXorGate(new_verific_id(inst), a, b, tmp1);
module->addXorGate(inst_name, tmp1, c, y);
- module->addAndGate(NEW_ID, tmp1, c, tmp2);
- module->addAndGate(NEW_ID, a, b, tmp3);
- module->addOrGate(NEW_ID, tmp2, tmp3, x);
+ module->addAndGate(new_verific_id(inst), tmp1, c, tmp2);
+ module->addAndGate(new_verific_id(inst), a, b, tmp3);
+ module->addOrGate(new_verific_id(inst), tmp2, tmp3, x);
return true;
}
@@ -305,63 +339,78 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name)
{
+ RTLIL::Cell *cell = nullptr;
+
if (inst->Type() == PRIM_AND) {
- module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ cell = module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_NAND) {
- RTLIL::SigSpec tmp = module->addWire(NEW_ID);
- module->addAnd(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
- module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
+ RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
+ cell = module->addAnd(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
+ import_attributes(cell->attributes, inst);
+ cell = module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_OR) {
- module->addOr(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ cell = module->addOr(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_NOR) {
- RTLIL::SigSpec tmp = module->addWire(NEW_ID);
- module->addOr(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
- module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
+ RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
+ cell = module->addOr(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
+ import_attributes(cell->attributes, inst);
+ cell = module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_XOR) {
- module->addXor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ cell = module->addXor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_XNOR) {
- module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ cell = module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_INV) {
- module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ cell = module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_MUX) {
- module->addMux(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
+ cell = module->addMux(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_TRI) {
- module->addMux(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
+ 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;
}
if (inst->Type() == PRIM_FADD)
{
- RTLIL::SigSpec a_plus_b = module->addWire(NEW_ID, 2);
- RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(NEW_ID);
+ RTLIL::SigSpec a_plus_b = module->addWire(new_verific_id(inst), 2);
+ RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(new_verific_id(inst));
if (inst->GetCout())
y.append(net_map_at(inst->GetCout()));
- module->addAdd(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), a_plus_b);
- module->addAdd(inst_name, a_plus_b, net_map_at(inst->GetCin()), y);
+ cell = module->addAdd(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), a_plus_b);
+ import_attributes(cell->attributes, inst);
+ cell = module->addAdd(inst_name, a_plus_b, net_map_at(inst->GetCin()), y);
+ import_attributes(cell->attributes, inst);
return true;
}
@@ -372,24 +421,26 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
log_assert(clocking.body_net == nullptr);
if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
- clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ cell = clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
else if (inst->GetSet()->IsGnd())
- clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
+ cell = clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
else if (inst->GetReset()->IsGnd())
- clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
+ cell = clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
else
- clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
+ cell = clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
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()));
+ cell = 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()),
+ cell = 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()));
+ import_attributes(cell->attributes, inst);
return true;
}
@@ -405,37 +456,45 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
if (inst->GetCout() != NULL)
out.append(net_map_at(inst->GetCout()));
if (inst->GetCin()->IsGnd()) {
- module->addAdd(inst_name, IN1, IN2, out, SIGNED);
+ cell = module->addAdd(inst_name, IN1, IN2, out, SIGNED);
+ import_attributes(cell->attributes, inst);
} else {
- RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out));
- module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED);
- module->addAdd(inst_name, tmp, net_map_at(inst->GetCin()), out, false);
+ RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst), GetSize(out));
+ cell = module->addAdd(new_verific_id(inst), IN1, IN2, tmp, SIGNED);
+ import_attributes(cell->attributes, inst);
+ cell = module->addAdd(inst_name, tmp, net_map_at(inst->GetCin()), out, false);
+ import_attributes(cell->attributes, inst);
}
return true;
}
if (inst->Type() == OPER_MULTIPLIER) {
- module->addMul(inst_name, IN1, IN2, OUT, SIGNED);
+ cell = module->addMul(inst_name, IN1, IN2, OUT, SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_DIVIDER) {
- module->addDiv(inst_name, IN1, IN2, OUT, SIGNED);
+ cell = module->addDiv(inst_name, IN1, IN2, OUT, SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_MODULO) {
- module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
+ cell = module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_REMAINDER) {
- module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
+ cell = module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_SHIFT_LEFT) {
- module->addShl(inst_name, IN1, IN2, OUT, false);
+ cell = module->addShl(inst_name, IN1, IN2, OUT, false);
+ import_attributes(cell->attributes, inst);
return true;
}
@@ -445,7 +504,8 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
for (unsigned i = 1; i < inst->OutputSize(); i++) {
vec.append(RTLIL::State::S0);
}
- module->addShl(inst_name, vec, IN, OUT, false);
+ cell = module->addShl(inst_name, vec, IN, OUT, false);
+ import_attributes(cell->attributes, inst);
return true;
}
@@ -455,7 +515,8 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
for (unsigned i = 1; i < inst->OutputSize(); i++) {
vec.append(RTLIL::State::S0);
}
- module->addShl(inst_name, vec, IN, OUT, false);
+ cell = module->addShl(inst_name, vec, IN, OUT, false);
+ import_attributes(cell->attributes, inst);
return true;
}
@@ -463,108 +524,127 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
Net *net_cin = inst->GetCin();
Net *net_a_msb = inst->GetInput1Bit(0);
if (net_cin->IsGnd())
- module->addShr(inst_name, IN1, IN2, OUT, false);
+ cell = module->addShr(inst_name, IN1, IN2, OUT, false);
else if (net_cin == net_a_msb)
- module->addSshr(inst_name, IN1, IN2, OUT, true);
+ cell = module->addSshr(inst_name, IN1, IN2, OUT, true);
else
log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst->Name());
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_REDUCE_AND) {
- module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+ cell = module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_REDUCE_OR) {
- module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+ cell = module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_REDUCE_XOR) {
- module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+ cell = module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_REDUCE_XNOR) {
- module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+ cell = module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_REDUCE_NOR) {
- SigSpec t = module->ReduceOr(NEW_ID, IN, SIGNED);
- module->addNot(inst_name, t, net_map_at(inst->GetOutput()));
+ SigSpec t = module->ReduceOr(new_verific_id(inst), IN, SIGNED);
+ cell = module->addNot(inst_name, t, net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_LESSTHAN) {
Net *net_cin = inst->GetCin();
if (net_cin->IsGnd())
- module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+ cell = module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
else if (net_cin->IsPwr())
- module->addLe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+ cell = module->addLe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
else
log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name());
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_WIDE_AND) {
- module->addAnd(inst_name, IN1, IN2, OUT, SIGNED);
+ cell = module->addAnd(inst_name, IN1, IN2, OUT, SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_WIDE_OR) {
- module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
+ cell = module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_WIDE_XOR) {
- module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
+ cell = module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_WIDE_XNOR) {
- module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
+ cell = module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_WIDE_BUF) {
- module->addPos(inst_name, IN, FILTERED_OUT, SIGNED);
+ cell = module->addPos(inst_name, IN, FILTERED_OUT, SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_WIDE_INV) {
- module->addNot(inst_name, IN, OUT, SIGNED);
+ cell = module->addNot(inst_name, IN, OUT, SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_MINUS) {
- module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
+ cell = module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_UMINUS) {
- module->addNeg(inst_name, IN, OUT, SIGNED);
+ cell = module->addNeg(inst_name, IN, OUT, SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_EQUAL) {
- module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+ cell = module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_NEQUAL) {
- module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+ cell = module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_WIDE_MUX) {
- module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
+ cell = module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_NTO1MUX) {
- module->addShr(inst_name, IN2, IN1, net_map_at(inst->GetOutput()));
+ cell = module->addShr(inst_name, IN2, IN1, net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
return true;
}
@@ -584,25 +664,29 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
padded_data.append(d);
}
- module->addShr(inst_name, padded_data, sel, out);
+ cell = module->addShr(inst_name, padded_data, sel, out);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_SELECTOR)
{
- module->addPmux(inst_name, State::S0, IN2, IN1, net_map_at(inst->GetOutput()));
+ cell = module->addPmux(inst_name, State::S0, IN2, IN1, net_map_at(inst->GetOutput()));
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_WIDE_SELECTOR)
{
SigSpec out = OUT;
- module->addPmux(inst_name, SigSpec(State::S0, GetSize(out)), IN2, IN1, out);
+ cell = module->addPmux(inst_name, SigSpec(State::S0, GetSize(out)), IN2, IN1, out);
+ import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == OPER_WIDE_TRI) {
- module->addMux(inst_name, RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT);
+ cell = module->addMux(inst_name, RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT);
+ import_attributes(cell->attributes, inst);
return true;
}
@@ -616,9 +700,10 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
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())
- clocking.addDff(inst_name, IN, OUT);
+ cell = clocking.addDff(inst_name, IN, OUT);
else
- clocking.addDffsr(inst_name, sig_set, sig_reset, IN, OUT);
+ cell = clocking.addDffsr(inst_name, sig_set, sig_reset, IN, OUT);
+ import_attributes(cell->attributes, inst);
return true;
}
@@ -701,13 +786,14 @@ void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo)
{
- std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name());
+ std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name();
+ std::string module_name = nl->IsOperator() ? "$verific$" + netlist_name : RTLIL::escape_id(netlist_name);
netlist = nl;
if (design->has(module_name)) {
- if (!nl->IsOperator())
- log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
+ if (!nl->IsOperator() && !is_blackbox(nl))
+ log_cmd_error("Re-definition of module `%s'.\n", netlist_name.c_str());
return;
}
@@ -715,7 +801,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
module->name = module_name;
design->add(module);
- if (nl->IsBlackBox()) {
+ if (is_blackbox(nl)) {
log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name));
module->set_bool_attribute("\\blackbox");
} else {
@@ -847,7 +933,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
ascii_initdata++;
}
if (initval_valid) {
- RTLIL::Cell *cell = module->addCell(NEW_ID, "$meminit");
+ RTLIL::Cell *cell = module->addCell(new_verific_id(net), "$meminit");
cell->parameters["\\WORDS"] = 1;
if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound())
cell->setPort("\\ADDR", word_idx);
@@ -910,7 +996,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (net->Bus())
continue;
- RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : NEW_ID);
+ RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : new_verific_id(net));
if (verific_verbose)
log(" importing net %s as %s.\n", net->Name(), log_id(wire_name));
@@ -934,7 +1020,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (found_new_net)
{
- RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : NEW_ID);
+ RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : new_verific_id(netbus));
if (verific_verbose)
log(" importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name));
@@ -1010,16 +1096,16 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
}
if (GetSize(anyconst_sig))
- module->connect(anyconst_sig, module->Anyconst(NEW_ID, GetSize(anyconst_sig)));
+ module->connect(anyconst_sig, module->Anyconst(new_verific_id(netbus), GetSize(anyconst_sig)));
if (GetSize(anyseq_sig))
- module->connect(anyseq_sig, module->Anyseq(NEW_ID, GetSize(anyseq_sig)));
+ module->connect(anyseq_sig, module->Anyseq(new_verific_id(netbus), GetSize(anyseq_sig)));
if (GetSize(allconst_sig))
- module->connect(allconst_sig, module->Allconst(NEW_ID, GetSize(allconst_sig)));
+ module->connect(allconst_sig, module->Allconst(new_verific_id(netbus), GetSize(allconst_sig)));
if (GetSize(allseq_sig))
- module->connect(allseq_sig, module->Allseq(NEW_ID, GetSize(allseq_sig)));
+ module->connect(allseq_sig, module->Allseq(new_verific_id(netbus), GetSize(allseq_sig)));
}
for (auto it : init_nets)
@@ -1043,10 +1129,10 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
}
for (auto net : anyconst_nets)
- module->connect(net_map_at(net), module->Anyconst(NEW_ID));
+ module->connect(net_map_at(net), module->Anyconst(new_verific_id(net)));
for (auto net : anyseq_nets)
- module->connect(net_map_at(net), module->Anyseq(NEW_ID));
+ module->connect(net_map_at(net), module->Anyseq(new_verific_id(net)));
pool<Instance*, hash_ptr_ops> sva_asserts;
pool<Instance*, hash_ptr_ops> sva_assumes;
@@ -1057,7 +1143,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
{
- RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID);
+ RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : new_verific_id(inst));
if (verific_verbose)
log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
@@ -1125,27 +1211,34 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT)
{
RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name()));
- if (memory->width != int(inst->Input2Size()))
- log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
+ int numchunks = int(inst->Input2Size()) / memory->width;
+ int chunksbits = ceil_log2(numchunks);
+
+ if ((numchunks * memory->width) != int(inst->Input2Size()) || (numchunks & (numchunks - 1)) != 0)
+ log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetOutput()->Name());
- RTLIL::SigSpec addr = operatorInput1(inst);
- RTLIL::SigSpec data = operatorInput2(inst);
-
- RTLIL::Cell *cell = module->addCell(inst_name, "$memwr");
- cell->parameters["\\MEMID"] = memory->name.str();
- cell->parameters["\\CLK_ENABLE"] = false;
- cell->parameters["\\CLK_POLARITY"] = true;
- cell->parameters["\\PRIORITY"] = 0;
- cell->parameters["\\ABITS"] = GetSize(addr);
- cell->parameters["\\WIDTH"] = GetSize(data);
- cell->setPort("\\EN", RTLIL::SigSpec(net_map_at(inst->GetControl())).repeat(GetSize(data)));
- cell->setPort("\\CLK", RTLIL::State::S0);
- cell->setPort("\\ADDR", addr);
- cell->setPort("\\DATA", data);
-
- if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
- cell->parameters["\\CLK_ENABLE"] = true;
- cell->setPort("\\CLK", net_map_at(inst->GetClock()));
+ 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);
+
+ RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
+ RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), "$memwr");
+ cell->parameters["\\MEMID"] = memory->name.str();
+ cell->parameters["\\CLK_ENABLE"] = false;
+ cell->parameters["\\CLK_POLARITY"] = true;
+ cell->parameters["\\PRIORITY"] = 0;
+ cell->parameters["\\ABITS"] = GetSize(addr);
+ cell->parameters["\\WIDTH"] = GetSize(data);
+ cell->setPort("\\EN", RTLIL::SigSpec(net_map_at(inst->GetControl())).repeat(GetSize(data)));
+ cell->setPort("\\CLK", RTLIL::State::S0);
+ cell->setPort("\\ADDR", addr);
+ cell->setPort("\\DATA", data);
+
+ if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
+ cell->parameters["\\CLK_ENABLE"] = true;
+ cell->setPort("\\CLK", net_map_at(inst->GetClock()));
+ }
}
continue;
}
@@ -1181,7 +1274,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
log_assert(inst->Input1Size() == inst->OutputSize());
SigSpec sig_d, sig_q, sig_o;
- sig_q = module->addWire(NEW_ID, inst->Input1Size());
+ sig_q = module->addWire(new_verific_id(inst), inst->Input1Size());
for (int i = int(inst->Input1Size())-1; i >= 0; i--){
sig_d.append(net_map_at(inst->GetInput1Bit(i)));
@@ -1195,8 +1288,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
}
- clocking.addDff(NEW_ID, sig_d, sig_q);
- module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
+ clocking.addDff(new_verific_id(inst), sig_d, sig_q);
+ module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
if (!mode_keep)
continue;
@@ -1210,7 +1303,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
SigSpec sig_d = net_map_at(inst->GetInput1());
SigSpec sig_o = net_map_at(inst->GetOutput());
- SigSpec sig_q = module->addWire(NEW_ID);
+ SigSpec sig_q = module->addWire(new_verific_id(inst));
if (verific_verbose) {
log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
@@ -1219,8 +1312,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
}
- clocking.addDff(NEW_ID, sig_d, sig_q);
- module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
+ clocking.addDff(new_verific_id(inst), sig_d, sig_q);
+ module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
if (!mode_keep)
continue;
@@ -1239,7 +1332,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
- past_ffs.insert(clocking.addDff(NEW_ID, sig_d, sig_q));
+ past_ffs.insert(clocking.addDff(new_verific_id(inst), sig_d, sig_q));
if (!mode_keep)
continue;
@@ -1253,14 +1346,14 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
SigBit sig_d = net_map_at(inst->GetInput1());
SigBit sig_o = net_map_at(inst->GetOutput());
- SigBit sig_q = module->addWire(NEW_ID);
+ SigBit sig_q = module->addWire(new_verific_id(inst));
if (verific_verbose)
log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
- clocking.addDff(NEW_ID, sig_d, sig_q);
- module->addEq(NEW_ID, {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
+ clocking.addDff(new_verific_id(inst), sig_d, sig_q);
+ module->addEq(new_verific_id(inst), {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
if (!mode_keep)
continue;
@@ -1283,9 +1376,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
Cell *cell = nullptr;
if (assume_attr != nullptr && !strcmp(assume_attr, "1"))
- cell = module->addAssume(NEW_ID, cond, State::S1);
+ cell = module->addAssume(new_verific_id(inst), cond, State::S1);
else
- cell = module->addAssert(NEW_ID, cond, State::S1);
+ cell = module->addAssert(new_verific_id(inst), cond, State::S1);
import_attributes(cell->attributes, inst);
continue;
@@ -1327,7 +1420,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
IdString port_name_id = RTLIL::escape_id(port_name);
auto &sigvec = cell_port_conns[port_name_id];
if (GetSize(sigvec) <= port_offset) {
- SigSpec zwires = module->addWire(NEW_ID, port_offset+1-GetSize(sigvec));
+ SigSpec zwires = module->addWire(new_verific_id(inst), port_offset+1-GetSize(sigvec));
for (auto bit : zwires)
sigvec.push_back(bit);
}
@@ -1363,6 +1456,50 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
merge_past_ffs(past_ffs);
}
+
+ if (!mode_fullinit)
+ {
+ pool<SigBit> non_ff_bits;
+ CellTypes ff_types;
+
+ ff_types.setup_internals_ff();
+ ff_types.setup_stdcells_mem();
+
+ for (auto cell : module->cells())
+ {
+ if (ff_types.cell_known(cell->type))
+ continue;
+
+ for (auto conn : cell->connections())
+ {
+ if (!cell->output(conn.first))
+ continue;
+
+ for (auto bit : conn.second)
+ if (bit.wire != nullptr)
+ non_ff_bits.insert(bit);
+ }
+ }
+
+ for (auto wire : module->wires())
+ {
+ if (!wire->attributes.count("\\init"))
+ continue;
+
+ Const &initval = wire->attributes.at("\\init");
+ for (int i = 0; i < GetSize(initval); i++)
+ {
+ if (initval[i] != State::S0 && initval[i] != State::S1)
+ continue;
+
+ if (non_ff_bits.count(SigBit(wire, i)))
+ initval[i] = State::Sx;
+ }
+
+ if (initval.is_fully_undef())
+ wire->attributes.erase("\\init");
+ }
+ }
}
// ==================================================================
@@ -1537,30 +1674,35 @@ struct VerificExtNets
int portname_cnt = 0;
// a map from Net to the same Net one level up in the design hierarchy
- std::map<Net*, Net*> net_level_up;
+ std::map<Net*, Net*> net_level_up_drive_up;
+ std::map<Net*, Net*> net_level_up_drive_down;
- Net *get_net_level_up(Net *net)
+ Net *route_up(Net *net, bool drive_up, Net *final_net = nullptr)
{
+ auto &net_level_up = drive_up ? net_level_up_drive_up : net_level_up_drive_down;
+
if (net_level_up.count(net) == 0)
{
Netlist *nl = net->Owner();
// Simply return if Netlist is not unique
- if (nl->NumOfRefs() != 1)
- return net;
+ log_assert(nl->NumOfRefs() == 1);
Instance *up_inst = (Instance*)nl->GetReferences()->GetLast();
Netlist *up_nl = up_inst->Owner();
// create new Port
string name = stringf("___extnets_%d", portname_cnt++);
- Port *new_port = new Port(name.c_str(), DIR_OUT);
+ Port *new_port = new Port(name.c_str(), drive_up ? DIR_OUT : DIR_IN);
nl->Add(new_port);
net->Connect(new_port);
// create new Net in up Netlist
- Net *new_net = new Net(name.c_str());
- up_nl->Add(new_net);
+ Net *new_net = final_net;
+ if (new_net == nullptr || new_net->Owner() != up_nl) {
+ new_net = new Net(name.c_str());
+ up_nl->Add(new_net);
+ }
up_inst->Connect(new_port, new_net);
net_level_up[net] = new_net;
@@ -1569,6 +1711,39 @@ struct VerificExtNets
return net_level_up.at(net);
}
+ Net *route_up(Net *net, bool drive_up, Netlist *dest, Net *final_net = nullptr)
+ {
+ while (net->Owner() != dest)
+ net = route_up(net, drive_up, final_net);
+ if (final_net != nullptr)
+ log_assert(net == final_net);
+ return net;
+ }
+
+ Netlist *find_common_ancestor(Netlist *A, Netlist *B)
+ {
+ std::set<Netlist*> ancestors_of_A;
+
+ Netlist *cursor = A;
+ while (1) {
+ ancestors_of_A.insert(cursor);
+ if (cursor->NumOfRefs() != 1)
+ break;
+ cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner();
+ }
+
+ cursor = B;
+ while (1) {
+ if (ancestors_of_A.count(cursor))
+ return cursor;
+ if (cursor->NumOfRefs() != 1)
+ break;
+ cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner();
+ }
+
+ log_error("No common ancestor found between %s and %s.\n", get_full_netlist_name(A).c_str(), get_full_netlist_name(B).c_str());
+ }
+
void run(Netlist *nl)
{
MapIter mi, mi2;
@@ -1592,19 +1767,37 @@ struct VerificExtNets
if (verific_verbose)
log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name());
- while (net->IsExternalTo(nl))
- {
- Net *newnet = get_net_level_up(net);
- if (newnet == net) break;
+ Netlist *ext_nl = net->Owner();
+ if (verific_verbose)
+ log(" external net owner: %s\n", get_full_netlist_name(ext_nl).c_str());
+
+ Netlist *ca_nl = find_common_ancestor(nl, ext_nl);
+
+ if (verific_verbose)
+ log(" common ancestor: %s\n", get_full_netlist_name(ca_nl).c_str());
+
+ Net *ca_net = route_up(net, !port->IsOutput(), ca_nl);
+ Net *new_net = ca_net;
+
+ if (ca_nl != nl)
+ {
if (verific_verbose)
- log(" external net: %s.%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name());
- net = newnet;
+ log(" net in common ancestor: %s\n", ca_net->Name());
+
+ string name = stringf("___extnets_%d", portname_cnt++);
+ 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);
+ log_assert(n == ca_net);
}
if (verific_verbose)
- log(" final net: %s.%s%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name(), net->IsExternalTo(nl) ? " (external)" : "");
- todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, net));
+ log(" new local net: %s\n", new_net->Name());
+
+ log_assert(!new_net->IsExternalTo(nl));
+ todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, new_net));
}
for (auto it : todo_connect) {
@@ -1614,30 +1807,64 @@ struct VerificExtNets
}
};
-void verific_import(Design *design, std::string top)
+void verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top)
{
+ verific_sva_fsm_limit = 16;
+
std::set<Netlist*> nl_todo, nl_done;
- {
- VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
- VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
+ VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
+ VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
+ Array *netlists = NULL;
+ Array veri_libs, vhdl_libs;
+ if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
+ 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());
- Array veri_libs, vhdl_libs;
- if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
- if (veri_lib) veri_libs.InsertLast(veri_lib);
+ if (top.empty()) {
+ netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
+ }
+ else {
+ Array veri_modules, vhdl_units;
+
+ if (veri_lib) {
+ VeriModule *veri_module = veri_lib->GetModule(top.c_str(), 1);
+ if (veri_module) {
+ veri_modules.InsertLast(veri_module);
+ }
- Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs);
- Netlist *nl;
- int i;
+ // 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);
+ }
+ }
- FOREACH_ARRAY_ITEM(netlists, i, nl) {
- if (top.empty() || nl->Owner()->Name() == top)
- nl_todo.insert(nl);
+ if (vhdl_lib) {
+ VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(top.c_str());
+ if (vhdl_unit)
+ vhdl_units.InsertLast(vhdl_unit);
}
- delete netlists;
+ netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &verific_params);
+ }
+
+ Netlist *nl;
+ int i;
+
+ FOREACH_ARRAY_ITEM(netlists, i, nl) {
+ if (top.empty() && nl->CellBaseName() != top)
+ continue;
+ nl->AddAtt(new Att(" \\top", NULL));
+ nl_todo.insert(nl);
}
+ delete netlists;
+
if (!verific_error_msg.empty())
log_error("%s\n", verific_error_msg.c_str());
@@ -1648,7 +1875,7 @@ void verific_import(Design *design, std::string top)
while (!nl_todo.empty()) {
Netlist *nl = *nl_todo.begin();
if (nl_done.count(nl) == 0) {
- VerificImporter importer(false, false, false, false, false, false);
+ VerificImporter importer(false, false, false, false, false, false, false);
importer.import_netlist(design, nl, nl_todo);
}
nl_todo.erase(nl);
@@ -1658,6 +1885,8 @@ void verific_import(Design *design, std::string top)
veri_file::Reset();
vhdl_file::Reset();
Libset::Reset();
+ verific_incdirs.clear();
+ verific_libdirs.clear();
verific_import_pending = false;
if (!verific_error_msg.empty())
@@ -1669,6 +1898,7 @@ YOSYS_NAMESPACE_END
PRIVATE_NAMESPACE_BEGIN
+#ifdef YOSYS_ENABLE_VERIFIC
bool check_noverific_env()
{
const char *e = getenv("YOSYS_NOVERIFIC");
@@ -1678,10 +1908,11 @@ bool check_noverific_env()
return false;
return true;
}
+#endif
struct VerificPass : public Pass {
VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -1702,11 +1933,18 @@ struct VerificPass : public Pass {
log("\n");
log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
log("\n");
+ log("\n");
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");
+ log(" verific -work <libname> {-sv|-vhdl|...} <hdl-file>\n");
+ log("\n");
+ log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n");
+ log("(default library when -work is not present: \"work\")\n");
+ log("\n");
+ log("\n");
log(" verific -vlog-incdir <directory>..\n");
log("\n");
log("Add Verilog include directories.\n");
@@ -1728,6 +1966,15 @@ struct VerificPass : public Pass {
log("Remove Verilog defines previously set with -vlog-define.\n");
log("\n");
log("\n");
+ log(" verific -set-error <msg_id>..\n");
+ log(" verific -set-warning <msg_id>..\n");
+ log(" verific -set-info <msg_id>..\n");
+ log(" verific -set-ignore <msg_id>..\n");
+ 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("\n");
+ log("\n");
log(" verific -import [options] <top-module>..\n");
log("\n");
log("Elaborate the design for the specified top modules, import to Yosys and\n");
@@ -1751,6 +1998,16 @@ struct VerificPass : public Pass {
log(" -autocover\n");
log(" Generate automatic cover statements for all asserts\n");
log("\n");
+ log(" -fullinit\n");
+ log(" Keep all register initializations, even those for non-FF registers.\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");
+ log(" cause Verific to produce a VERI-1928 or VHDL-1676 message. 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(" -v, -vv\n");
log(" Verbose log messages. (-vv is even more verbose than -v.)\n");
log("\n");
@@ -1769,6 +2026,9 @@ struct VerificPass : public Pass {
log(" -nosva\n");
log(" Ignore SVA properties, do not infer checker logic.\n");
log("\n");
+ log(" -L <int>\n");
+ log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
+ log("\n");
log(" -n\n");
log(" Keep all Verific names on instances and nets. By default only\n");
log(" user-declared names are preserved.\n");
@@ -1780,23 +2040,51 @@ struct VerificPass : public Pass {
log("\n");
}
#ifdef YOSYS_ENABLE_VERIFIC
- virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_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");
log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
- Message::SetConsoleOutput(0);
- Message::RegisterCallBackMsg(msg_func);
- RuntimeFlags::SetVar("db_preserve_user_nets", 1);
- RuntimeFlags::SetVar("db_allow_external_nets", 1);
- RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
- RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
- RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
- RuntimeFlags::SetVar("db_infer_wide_operators", 1);
+ if (set_verific_global_flags)
+ {
+ Message::SetConsoleOutput(0);
+ Message::RegisterCallBackMsg(msg_func);
+
+ RuntimeFlags::SetVar("db_preserve_user_nets", 1);
+ RuntimeFlags::SetVar("db_allow_external_nets", 1);
+ RuntimeFlags::SetVar("db_infer_wide_operators", 1);
+
+ RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
+ RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
+
+ 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);
+
+ // 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) ;
+
+#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;
const char *release_str = Message::ReleaseString();
time_t release_time = Message::ReleaseDate();
@@ -1811,16 +2099,39 @@ struct VerificPass : public Pass {
log("Built with Verific %s, released at %s.\n", release_str, release_tmstr);
int argidx = 1;
+ std::string work = "work";
+
+ if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
+ args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
+ {
+ msg_type_t new_type;
+
+ if (args[argidx] == "-set-error")
+ new_type = VERIFIC_ERROR;
+ else if (args[argidx] == "-set-warning")
+ new_type = VERIFIC_WARNING;
+ else if (args[argidx] == "-set-info")
+ new_type = VERIFIC_INFO;
+ else if (args[argidx] == "-set-ignore")
+ new_type = VERIFIC_IGNORE;
+ else
+ log_abort();
+
+ for (argidx++; argidx < GetSize(args); argidx++)
+ Message::SetMessageType(args[argidx].c_str(), new_type);
+
+ goto check_error;
+ }
if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") {
for (argidx++; argidx < GetSize(args); argidx++)
- veri_file::AddIncludeDir(args[argidx].c_str());
+ verific_incdirs.push_back(args[argidx]);
goto check_error;
}
if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") {
for (argidx++; argidx < GetSize(args); argidx++)
- veri_file::AddYDir(args[argidx].c_str());
+ verific_libdirs.push_back(args[argidx]);
goto check_error;
}
@@ -1847,6 +2158,15 @@ struct VerificPass : public Pass {
goto check_error;
}
+ for (; argidx < GetSize(args); argidx++)
+ {
+ if (args[argidx] == "-work" && argidx+1 < GetSize(args)) {
+ work = args[++argidx];
+ continue;
+ }
+ break;
+ }
+
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"))
{
@@ -1869,7 +2189,7 @@ struct VerificPass : public Pass {
veri_file::DefineMacro("VERIFIC");
veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS");
- for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].substr(0, 2) == "-D"; argidx++) {
+ for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].compare(0, 2, "-D") == 0; argidx++) {
std::string name = args[argidx].substr(2);
if (args[argidx] == "-D") {
if (++argidx >= GetSize(args))
@@ -1886,10 +2206,15 @@ struct VerificPass : public Pass {
}
}
+ for (auto &dir : verific_incdirs)
+ veri_file::AddIncludeDir(dir.c_str());
+ for (auto &dir : verific_libdirs)
+ veri_file::AddYDir(dir.c_str());
+
while (argidx < GetSize(args))
file_names.Insert(args[argidx++].c_str());
- if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, "work", veri_file::MFCU))
+ if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU))
log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
verific_import_pending = true;
@@ -1899,7 +2224,7 @@ struct VerificPass : public Pass {
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", vhdl_file::VHDL_87))
+ 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());
verific_import_pending = true;
goto check_error;
@@ -1908,7 +2233,7 @@ struct VerificPass : public Pass {
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", vhdl_file::VHDL_93))
+ 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());
verific_import_pending = true;
goto check_error;
@@ -1917,7 +2242,7 @@ struct VerificPass : public Pass {
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", vhdl_file::VHDL_2K))
+ 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());
verific_import_pending = true;
goto check_error;
@@ -1926,7 +2251,7 @@ struct VerificPass : public Pass {
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", vhdl_file::VHDL_2008))
+ 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());
verific_import_pending = true;
goto check_error;
@@ -1937,9 +2262,10 @@ struct VerificPass : public Pass {
std::set<Netlist*> nl_todo, nl_done;
bool mode_all = false, mode_gates = false, mode_keep = false;
bool mode_nosva = false, mode_names = false, mode_verific = false;
- bool mode_autocover = false;
+ bool mode_autocover = false, mode_fullinit = false;
bool flatten = false, extnets = false;
string dumpfile;
+ Map parameters(STRING_HASH);
for (argidx++; argidx < GetSize(args); argidx++) {
if (args[argidx] == "-all") {
@@ -1966,6 +2292,10 @@ struct VerificPass : public Pass {
mode_nosva = true;
continue;
}
+ if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
+ verific_sva_fsm_limit = atoi(args[++argidx].c_str());
+ continue;
+ }
if (args[argidx] == "-n") {
mode_names = true;
continue;
@@ -1974,6 +2304,19 @@ struct VerificPass : public Pass {
mode_autocover = true;
continue;
}
+ if (args[argidx] == "-fullinit") {
+ mode_fullinit = true;
+ continue;
+ }
+ if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) {
+ const std::string &key = args[++argidx];
+ const std::string &value = args[++argidx];
+ unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(),
+ 1 /* force_overwrite */);
+ if (!new_insertion)
+ log_warning_noprefix("-chparam %s already specified: overwriting.\n", key.c_str());
+ continue;
+ }
if (args[argidx] == "-V") {
mode_verific = true;
continue;
@@ -1993,98 +2336,56 @@ struct VerificPass : public Pass {
break;
}
- if (argidx > GetSize(args) && args[argidx].substr(0, 1) == "-")
+ if (argidx > GetSize(args) && args[argidx].compare(0, 1, "-") == 0)
cmd_error(args, argidx, "unknown option");
if (mode_all)
{
-#if 0
- log("Running veri_file::ElaborateAll().\n");
- if (!veri_file::ElaborateAll())
- log_cmd_error("Elaboration of Verilog modules failed.\n");
-
- log("Running vhdl_file::ElaborateAll().\n");
- if (!vhdl_file::ElaborateAll())
- log_cmd_error("Elaboration of VHDL modules failed.\n");
-
- Library *lib = Netlist::PresentDesign()->Owner()->Owner();
-
- if (argidx == GetSize(args))
- {
- MapIter iter;
- char *iter_name;
- Verific::Cell *iter_cell;
-
- FOREACH_MAP_ITEM(lib->GetCells(), iter, &iter_name, &iter_cell) {
- if (*iter_name != '$')
- nl_todo.insert(iter_cell->GetFirstNetlist());
- }
- }
- else
- {
- for (; argidx < GetSize(args); argidx++)
- {
- Verific::Cell *cell = lib->GetCell(args[argidx].c_str());
-
- if (cell == nullptr)
- log_cmd_error("Module not found: %s\n", args[argidx].c_str());
-
- nl_todo.insert(cell->GetFirstNetlist());
- cell->GetFirstNetlist()->SetPresentDesign();
- }
- }
-#else
log("Running hier_tree::ElaborateAll().\n");
- VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
- VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
+ 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;
if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
if (veri_lib) veri_libs.InsertLast(veri_lib);
- Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs);
+ Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &parameters);
Netlist *nl;
int i;
FOREACH_ARRAY_ITEM(netlists, i, nl)
nl_todo.insert(nl);
delete netlists;
-#endif
}
else
{
if (argidx == GetSize(args))
log_cmd_error("No top module specified.\n");
-#if 0
- for (; argidx < GetSize(args); argidx++) {
- if (veri_file::GetModule(args[argidx].c_str())) {
- log("Running veri_file::Elaborate(\"%s\").\n", args[argidx].c_str());
- if (!veri_file::Elaborate(args[argidx].c_str()))
- log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str());
- nl_todo.insert(Netlist::PresentDesign());
- } else {
- log("Running vhdl_file::Elaborate(\"%s\").\n", args[argidx].c_str());
- if (!vhdl_file::Elaborate(args[argidx].c_str()))
- log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str());
- nl_todo.insert(Netlist::PresentDesign());
- }
- }
-#else
Array veri_modules, vhdl_units;
for (; argidx < GetSize(args); argidx++)
{
const char *name = args[argidx].c_str();
+ 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;
+ }
- VeriModule *veri_module = veri_file::GetModule(name);
- 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);
+ }
}
- VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
+ VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(name);
if (vhdl_unit) {
log("Adding VHDL unit '%s' to elaboration queue.\n", name);
@@ -2096,14 +2397,15 @@ struct VerificPass : public Pass {
}
log("Running hier_tree::Elaborate().\n");
- Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units);
+ Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &parameters);
Netlist *nl;
int i;
- FOREACH_ARRAY_ITEM(netlists, i, nl)
+ FOREACH_ARRAY_ITEM(netlists, i, nl) {
+ nl->AddAtt(new Att(" \\top", NULL));
nl_todo.insert(nl);
+ }
delete netlists;
-#endif
}
if (!verific_error_msg.empty())
@@ -2129,7 +2431,7 @@ struct VerificPass : public Pass {
Netlist *nl = *nl_todo.begin();
if (nl_done.count(nl) == 0) {
VerificImporter importer(mode_gates, mode_keep, mode_nosva,
- mode_names, mode_verific, mode_autocover);
+ mode_names, mode_verific, mode_autocover, mode_fullinit);
importer.import_netlist(design, nl, nl_todo);
}
nl_todo.erase(nl);
@@ -2139,6 +2441,8 @@ struct VerificPass : public Pass {
veri_file::Reset();
vhdl_file::Reset();
Libset::Reset();
+ verific_incdirs.clear();
+ verific_libdirs.clear();
verific_import_pending = false;
goto check_error;
}
@@ -2151,7 +2455,7 @@ struct VerificPass : public Pass {
}
#else /* YOSYS_ENABLE_VERIFIC */
- virtual void execute(std::vector<std::string>, RTLIL::Design *) {
+ void execute(std::vector<std::string>, RTLIL::Design *) YS_OVERRIDE {
log_cmd_error("This version of Yosys is built without Verific support.\n");
}
#endif
@@ -2159,7 +2463,7 @@ struct VerificPass : public Pass {
struct ReadPass : public Pass {
ReadPass() : Pass("read", "load HDL designs") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -2186,27 +2490,54 @@ struct ReadPass : public Pass {
log("\n");
log("Unset global Verilog/SystemVerilog defines.\n");
log("\n");
+ log("\n");
+ log(" read -incdir <directory>\n");
+ log("\n");
+ log("Add directory to global Verilog/SystemVerilog include directories.\n");
+ log("\n");
+ log("\n");
+ log(" read -verific\n");
+ log(" read -noverific\n");
+ log("\n");
+ log("Subsequent calls to 'read' will either use or not use Verific. Calling 'read'\n");
+ log("with -verific will result in an error on Yosys binaries that are built without\n");
+ log("Verific support. The default is to use Verific if it is available.\n");
+ log("\n");
}
- virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
- if (args.size() < 2)
+#ifdef YOSYS_ENABLE_VERIFIC
+ static bool verific_available = !check_noverific_env();
+#else
+ static bool verific_available = false;
+#endif
+ static bool use_verific = verific_available;
+
+ if (args.size() < 2 || args[1][0] != '-')
log_cmd_error("Missing mode parameter.\n");
+ if (args[1] == "-verific" || args[1] == "-noverific") {
+ if (args.size() != 2)
+ log_cmd_error("Additional arguments to -verific/-noverific.\n");
+ if (args[1] == "-verific") {
+ if (!verific_available)
+ log_cmd_error("This version of Yosys is built without Verific support.\n");
+ use_verific = true;
+ } else {
+ use_verific = false;
+ }
+ return;
+ }
+
if (args.size() < 3)
log_cmd_error("Missing file name parameter.\n");
-#ifdef YOSYS_ENABLE_VERIFIC
- bool use_verific = !check_noverific_env();
-#else
- bool use_verific = false;
-#endif
-
if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
if (use_verific) {
args[0] = "verific";
} else {
args[0] = "read_verilog";
- args.erase(args.begin()+1, args.begin()+2);
+ args[1] = "-defer";
}
Pass::call(design, args);
return;
@@ -2220,6 +2551,7 @@ struct ReadPass : public Pass {
if (args[1] == "-formal")
args.insert(args.begin()+1, std::string());
args[1] = "-sv";
+ args.insert(args.begin()+1, "-defer");
}
Pass::call(design, args);
return;
@@ -2263,6 +2595,20 @@ struct ReadPass : public Pass {
return;
}
+ if (args[1] == "-incdir") {
+ if (use_verific) {
+ args[0] = "verific";
+ args[1] = "-vlog-incdir";
+ Pass::call(design, args);
+ }
+ args[0] = "verilog_defaults";
+ args[1] = "-add";
+ for (int i = 2; i < GetSize(args); i++)
+ args[i] = "-I" + args[i];
+ Pass::call(design, args);
+ return;
+ }
+
log_cmd_error("Missing or unsupported mode parameter.\n");
}
} ReadPass;
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-05 05:40:57 +0000