# include <dirent.h>
#endif
+#include "frontends/verific/verific.h"
+
USING_YOSYS_NAMESPACE
#ifdef YOSYS_ENABLE_VERIFIC
#include "VeriModule.h"
#include "VeriWrite.h"
#include "VhdlUnits.h"
-#include "DataBase.h"
#include "Message.h"
#ifdef __clang__
#endif
#ifdef VERIFIC_NAMESPACE
-using namespace Verific ;
+using namespace Verific;
#endif
#endif
-PRIVATE_NAMESPACE_BEGIN
-
#ifdef YOSYS_ENABLE_VERIFIC
+YOSYS_NAMESPACE_BEGIN
pool<int> verific_sva_prims = {
// Copy&paste from Verific 3.16_484_32_170630 Netlist.h
return nl->CellBaseName();
}
-struct VerificImporter;
-void import_sva_assert(VerificImporter *importer, Instance *inst);
-void import_sva_assume(VerificImporter *importer, Instance *inst);
-void import_sva_cover(VerificImporter *importer, Instance *inst);
-void svapp_assert(Instance *inst);
-void svapp_assume(Instance *inst);
-void svapp_cover(Instance *inst);
-
-struct VerificClockEdge {
- Net *clock_net = nullptr;
- SigBit clock_sig = State::Sx;
- bool posedge = false;
- VerificClockEdge(VerificImporter *importer, Instance *inst);
-};
+// ==================================================================
-struct VerificImporter
+VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) :
+ mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
+ mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose)
{
- RTLIL::Module *module;
- Netlist *netlist;
+}
- std::map<Net*, RTLIL::SigBit> net_map;
- std::map<Net*, Net*> sva_posedge_map;
+RTLIL::SigBit VerificImporter::net_map_at(Net *net)
+{
+ if (net->IsExternalTo(netlist))
+ log_error("Found external reference to '%s.%s' in netlist '%s', please use -flatten or -extnets.\n",
+ get_full_netlist_name(net->Owner()).c_str(), net->Name(), get_full_netlist_name(netlist).c_str());
- bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose;
+ return net_map.at(net);
+}
- VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) :
- mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
- mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose)
- {
- }
+void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
+{
+ MapIter mi;
+ Att *attr;
- RTLIL::SigBit net_map_at(Net *net)
- {
- if (net->IsExternalTo(netlist))
- log_error("Found external reference to '%s.%s' in netlist '%s', please use -flatten or -extnets.\n",
- get_full_netlist_name(net->Owner()).c_str(), net->Name(), get_full_netlist_name(netlist).c_str());
+ if (obj->Linefile())
+ attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
- return net_map.at(net);
- }
+ // FIXME: Parse numeric attributes
+ FOREACH_ATTRIBUTE(obj, mi, attr)
+ attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
+}
- void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
- {
- MapIter mi;
- Att *attr;
+RTLIL::SigSpec VerificImporter::operatorInput(Instance *inst)
+{
+ RTLIL::SigSpec sig;
+ for (int i = int(inst->InputSize())-1; i >= 0; i--)
+ if (inst->GetInputBit(i))
+ sig.append(net_map_at(inst->GetInputBit(i)));
+ else
+ sig.append(RTLIL::State::Sz);
+ return sig;
+}
- if (obj->Linefile())
- attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
+RTLIL::SigSpec VerificImporter::operatorInput1(Instance *inst)
+{
+ RTLIL::SigSpec sig;
+ for (int i = int(inst->Input1Size())-1; i >= 0; i--)
+ if (inst->GetInput1Bit(i))
+ sig.append(net_map_at(inst->GetInput1Bit(i)));
+ else
+ sig.append(RTLIL::State::Sz);
+ return sig;
+}
- // FIXME: Parse numeric attributes
- FOREACH_ATTRIBUTE(obj, mi, attr)
- attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
- }
+RTLIL::SigSpec VerificImporter::operatorInput2(Instance *inst)
+{
+ RTLIL::SigSpec sig;
+ for (int i = int(inst->Input2Size())-1; i >= 0; i--)
+ if (inst->GetInput2Bit(i))
+ sig.append(net_map_at(inst->GetInput2Bit(i)));
+ else
+ sig.append(RTLIL::State::Sz);
+ return sig;
+}
- RTLIL::SigSpec operatorInput(Instance *inst)
- {
+RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portname)
+{
+ PortBus *portbus = inst->View()->GetPortBus(portname);
+ if (portbus) {
RTLIL::SigSpec sig;
- for (int i = int(inst->InputSize())-1; i >= 0; i--)
- if (inst->GetInputBit(i))
- sig.append(net_map_at(inst->GetInputBit(i)));
- else
+ for (unsigned i = 0; i < portbus->Size(); i++) {
+ Net *net = inst->GetNet(portbus->ElementAtIndex(i));
+ if (net) {
+ if (net->IsGnd())
+ sig.append(RTLIL::State::S0);
+ else if (net->IsPwr())
+ sig.append(RTLIL::State::S1);
+ else
+ sig.append(net_map_at(net));
+ } else
sig.append(RTLIL::State::Sz);
+ }
return sig;
+ } else {
+ Port *port = inst->View()->GetPort(portname);
+ log_assert(port != NULL);
+ Net *net = inst->GetNet(port);
+ return net_map_at(net);
}
+}
- RTLIL::SigSpec operatorInput1(Instance *inst)
- {
- RTLIL::SigSpec sig;
- for (int i = int(inst->Input1Size())-1; i >= 0; i--)
- if (inst->GetInput1Bit(i))
- sig.append(net_map_at(inst->GetInput1Bit(i)));
+RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst)
+{
+ RTLIL::SigSpec sig;
+ RTLIL::Wire *dummy_wire = NULL;
+ for (int i = int(inst->OutputSize())-1; i >= 0; i--)
+ if (inst->GetOutputBit(i)) {
+ sig.append(net_map_at(inst->GetOutputBit(i)));
+ dummy_wire = NULL;
+ } else {
+ if (dummy_wire == NULL)
+ dummy_wire = module->addWire(NEW_ID);
else
- sig.append(RTLIL::State::Sz);
- return sig;
- }
+ dummy_wire->width++;
+ sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
+ }
+ return sig;
+}
- RTLIL::SigSpec operatorInput2(Instance *inst)
- {
- RTLIL::SigSpec sig;
- for (int i = int(inst->Input2Size())-1; i >= 0; i--)
- if (inst->GetInput2Bit(i))
- sig.append(net_map_at(inst->GetInput2Bit(i)));
- else
- sig.append(RTLIL::State::Sz);
- return sig;
+bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdString inst_name)
+{
+ if (inst->Type() == PRIM_AND) {
+ module->addAndGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ return true;
}
- RTLIL::SigSpec operatorInport(Instance *inst, const char *portname)
- {
- PortBus *portbus = inst->View()->GetPortBus(portname);
- if (portbus) {
- RTLIL::SigSpec sig;
- for (unsigned i = 0; i < portbus->Size(); i++) {
- Net *net = inst->GetNet(portbus->ElementAtIndex(i));
- if (net) {
- if (net->IsGnd())
- sig.append(RTLIL::State::S0);
- else if (net->IsPwr())
- sig.append(RTLIL::State::S1);
- else
- sig.append(net_map_at(net));
- } else
- sig.append(RTLIL::State::Sz);
- }
- return sig;
- } else {
- Port *port = inst->View()->GetPort(portname);
- log_assert(port != NULL);
- Net *net = inst->GetNet(port);
- return net_map_at(net);
- }
+ 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);
+ module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
+ return true;
}
- RTLIL::SigSpec operatorOutput(Instance *inst)
- {
- RTLIL::SigSpec sig;
- RTLIL::Wire *dummy_wire = NULL;
- for (int i = int(inst->OutputSize())-1; i >= 0; i--)
- if (inst->GetOutputBit(i)) {
- sig.append(net_map_at(inst->GetOutputBit(i)));
- dummy_wire = NULL;
- } else {
- if (dummy_wire == NULL)
- dummy_wire = module->addWire(NEW_ID);
- else
- dummy_wire->width++;
- sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
- }
- return sig;
+ if (inst->Type() == PRIM_OR) {
+ module->addOrGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ return true;
}
- bool import_netlist_instance_gates(Instance *inst, RTLIL::IdString inst_name)
- {
- if (inst->Type() == PRIM_AND) {
- module->addAndGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
- return true;
- }
-
- 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);
- module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
- return true;
- }
-
- if (inst->Type() == PRIM_OR) {
- module->addOrGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
- return true;
- }
-
- 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);
- module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
- return true;
- }
-
- if (inst->Type() == PRIM_XOR) {
- module->addXorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
- return true;
- }
-
- if (inst->Type() == PRIM_XNOR) {
- module->addXnorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
- return true;
- }
-
- if (inst->Type() == PRIM_BUF) {
- module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
- return true;
- }
+ 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);
+ module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
+ return true;
+ }
- if (inst->Type() == PRIM_INV) {
- module->addNotGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
- return true;
- }
+ if (inst->Type() == PRIM_XOR) {
+ module->addXorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ return true;
+ }
- if (inst->Type() == PRIM_MUX) {
- module->addMuxGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
- return true;
- }
+ if (inst->Type() == PRIM_XNOR) {
+ module->addXnorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ return true;
+ }
- if (inst->Type() == PRIM_TRI) {
- module->addMuxGate(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
- return true;
- }
+ if (inst->Type() == PRIM_BUF) {
+ module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ return true;
+ }
- 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);
- 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);
- return true;
- }
+ if (inst->Type() == PRIM_INV) {
+ module->addNotGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ return true;
+ }
- if (inst->Type() == PRIM_DFFRS)
- {
- if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
- module->addDffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
- else if (inst->GetSet()->IsGnd())
- module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()),
- net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), false);
- else if (inst->GetReset()->IsGnd())
- module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()),
- net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), true);
- else
- module->addDffsrGate(inst_name, net_map_at(inst->GetClock()), 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_MUX) {
+ module->addMuxGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
+ return true;
+ }
- return false;
+ if (inst->Type() == PRIM_TRI) {
+ module->addMuxGate(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
+ return true;
}
- bool import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name)
+ if (inst->Type() == PRIM_FADD)
{
- if (inst->Type() == PRIM_AND) {
- module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
- 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()));
- 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()));
- 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()));
- 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()));
- 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()));
- return true;
- }
-
- if (inst->Type() == PRIM_INV) {
- module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
- 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()));
- 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()));
- 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);
- 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);
- return true;
- }
-
- if (inst->Type() == PRIM_DFFRS)
- {
- if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
- module->addDff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
- else if (inst->GetSet()->IsGnd())
- module->addAdff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()),
- net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
- else if (inst->GetReset()->IsGnd())
- module->addAdff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()),
- net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
- else
- module->addDffsr(inst_name, net_map_at(inst->GetClock()), 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_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;
- }
-
- #define IN operatorInput(inst)
- #define IN1 operatorInput1(inst)
- #define IN2 operatorInput2(inst)
- #define OUT operatorOutput(inst)
- #define SIGNED inst->View()->IsSigned()
-
- if (inst->Type() == OPER_ADDER) {
- RTLIL::SigSpec out = OUT;
- if (inst->GetCout() != NULL)
- out.append(net_map_at(inst->GetCout()));
- if (inst->GetCin()->IsGnd()) {
- module->addAdd(inst_name, IN1, IN2, out, SIGNED);
- } 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);
- }
- return true;
- }
-
- if (inst->Type() == OPER_MULTIPLIER) {
- module->addMul(inst_name, IN1, IN2, OUT, SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_DIVIDER) {
- module->addDiv(inst_name, IN1, IN2, OUT, SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_MODULO) {
- module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_REMAINDER) {
- module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_SHIFT_LEFT) {
- module->addShl(inst_name, IN1, IN2, OUT, false);
- return true;
- }
-
- if (inst->Type() == OPER_ENABLED_DECODER) {
- RTLIL::SigSpec vec;
- vec.append(net_map_at(inst->GetControl()));
- for (unsigned i = 1; i < inst->OutputSize(); i++) {
- vec.append(RTLIL::State::S0);
- }
- module->addShl(inst_name, vec, IN, OUT, false);
- return true;
- }
-
- if (inst->Type() == OPER_DECODER) {
- RTLIL::SigSpec vec;
- vec.append(RTLIL::State::S1);
- for (unsigned i = 1; i < inst->OutputSize(); i++) {
- vec.append(RTLIL::State::S0);
- }
- module->addShl(inst_name, vec, IN, OUT, false);
- return true;
- }
-
- if (inst->Type() == OPER_SHIFT_RIGHT) {
- Net *net_cin = inst->GetCin();
- Net *net_a_msb = inst->GetInput1Bit(0);
- if (net_cin->IsGnd())
- module->addShr(inst_name, IN1, IN2, OUT, false);
- else if (net_cin == net_a_msb)
- 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());
- return true;
- }
-
- if (inst->Type() == OPER_REDUCE_AND) {
- module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_REDUCE_OR) {
- module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_REDUCE_XOR) {
- module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_REDUCE_XNOR) {
- module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
- 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);
- else if (net_cin->IsPwr())
- 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());
- return true;
- }
-
- if (inst->Type() == OPER_WIDE_AND) {
- module->addAnd(inst_name, IN1, IN2, OUT, SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_WIDE_OR) {
- module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_WIDE_XOR) {
- module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_WIDE_XNOR) {
- module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_WIDE_BUF) {
- module->addPos(inst_name, IN, OUT, SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_WIDE_INV) {
- module->addNot(inst_name, IN, OUT, SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_MINUS) {
- module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_UMINUS) {
- module->addNeg(inst_name, IN, OUT, SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_EQUAL) {
- module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_NEQUAL) {
- module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
- return true;
- }
-
- if (inst->Type() == OPER_WIDE_MUX) {
- module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
- 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);
- return true;
- }
-
- if (inst->Type() == OPER_WIDE_DFFRS) {
- 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())
- module->addDff(inst_name, net_map_at(inst->GetClock()), IN, OUT);
- else
- module->addDffsr(inst_name, net_map_at(inst->GetClock()), sig_set, sig_reset, IN, OUT);
- return true;
- }
-
- #undef IN
- #undef IN1
- #undef IN2
- #undef OUT
- #undef SIGNED
-
- return false;
+ 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);
+ 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);
+ return true;
}
- void merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol)
+ if (inst->Type() == PRIM_DFFRS)
{
- bool keep_running = true;
- SigMap sigmap;
-
- while (keep_running)
- {
- keep_running = false;
+ if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
+ module->addDffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ else if (inst->GetSet()->IsGnd())
+ module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()),
+ net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), false);
+ else if (inst->GetReset()->IsGnd())
+ module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()),
+ net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), true);
+ else
+ module->addDffsrGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
+ net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ return true;
+ }
- dict<SigBit, pool<RTLIL::Cell*>> dbits_db;
- SigSpec dbits;
+ return false;
+}
- for (auto cell : candidates) {
- SigBit bit = sigmap(cell->getPort("\\D"));
- dbits_db[bit].insert(cell);
- dbits.append(bit);
- }
+bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name)
+{
+ if (inst->Type() == PRIM_AND) {
+ module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ return true;
+ }
- dbits.sort_and_unify();
+ 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()));
+ return true;
+ }
- for (auto chunk : dbits.chunks())
- {
- SigSpec sig_d = chunk;
+ if (inst->Type() == PRIM_OR) {
+ module->addOr(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ return true;
+ }
- if (chunk.wire == nullptr || GetSize(sig_d) == 1)
- continue;
+ 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()));
+ return true;
+ }
- SigSpec sig_q = module->addWire(NEW_ID, GetSize(sig_d));
- RTLIL::Cell *new_ff = module->addDff(NEW_ID, clock, sig_d, sig_q, clock_pol);
+ if (inst->Type() == PRIM_XOR) {
+ module->addXor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ return true;
+ }
- if (verbose)
- log(" merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff));
+ if (inst->Type() == PRIM_XNOR) {
+ module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+ return true;
+ }
- for (int i = 0; i < GetSize(sig_d); i++)
- for (auto old_ff : dbits_db[sig_d[i]])
- {
- if (verbose)
- log(" replacing old ff %s on bit %d.\n", log_id(old_ff), i);
+ if (inst->Type() == PRIM_INV) {
+ module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ return true;
+ }
- SigBit old_q = old_ff->getPort("\\Q");
- SigBit new_q = sig_q[i];
+ 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()));
+ return true;
+ }
- sigmap.add(old_q, new_q);
- module->connect(old_q, new_q);
- candidates.erase(old_ff);
- module->remove(old_ff);
- keep_running = 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()));
+ return true;
}
- void merge_past_ffs(pool<RTLIL::Cell*> &candidates)
+ if (inst->Type() == PRIM_FADD)
{
- dict<pair<SigBit, int>, pool<RTLIL::Cell*>> database;
-
- for (auto cell : candidates)
- {
- SigBit clock = cell->getPort("\\CLK");
- bool clock_pol = cell->getParam("\\CLK_POLARITY").as_bool();
- database[make_pair(clock, int(clock_pol))].insert(cell);
- }
-
- for (auto it : database)
- merge_past_ffs_clock(it.second, it.first.first, it.first.second);
+ RTLIL::SigSpec a_plus_b = module->addWire(NEW_ID, 2);
+ RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(NEW_ID);
+ 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);
+ return true;
}
- void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo)
+ if (inst->Type() == PRIM_DFFRS)
{
- std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name());
-
- netlist = nl;
-
- if (design->has(module_name)) {
- if (!nl->IsOperator())
- log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
- return;
- }
+ if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
+ module->addDff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ else if (inst->GetSet()->IsGnd())
+ module->addAdff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()),
+ net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
+ else if (inst->GetReset()->IsGnd())
+ module->addAdff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()),
+ net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
+ else
+ module->addDffsr(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
+ net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ return true;
+ }
- module = new RTLIL::Module;
- module->name = module_name;
- design->add(module);
+ 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 (nl->IsBlackBox()) {
- log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name));
- module->set_bool_attribute("\\blackbox");
+ #define IN operatorInput(inst)
+ #define IN1 operatorInput1(inst)
+ #define IN2 operatorInput2(inst)
+ #define OUT operatorOutput(inst)
+ #define SIGNED inst->View()->IsSigned()
+
+ if (inst->Type() == OPER_ADDER) {
+ RTLIL::SigSpec out = OUT;
+ if (inst->GetCout() != NULL)
+ out.append(net_map_at(inst->GetCout()));
+ if (inst->GetCin()->IsGnd()) {
+ module->addAdd(inst_name, IN1, IN2, out, SIGNED);
} else {
- log("Importing module %s.\n", RTLIL::id2cstr(module->name));
- }
-
- SetIter si;
- MapIter mi, mi2;
- Port *port;
- PortBus *portbus;
- Net *net;
- NetBus *netbus;
- Instance *inst;
- PortRef *pr;
-
- if (!mode_nosvapp)
- {
- vector<Instance*> asserts, assumes, covers;
-
- FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
- {
- if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
- asserts.push_back(inst);
-
- if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
- assumes.push_back(inst);
-
- if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
- covers.push_back(inst);
- }
-
- for (auto inst : asserts)
- svapp_assert(inst);
-
- for (auto inst : assumes)
- svapp_assume(inst);
-
- for (auto inst : covers)
- svapp_cover(inst);
+ 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);
}
+ return true;
+ }
- FOREACH_PORT_OF_NETLIST(nl, mi, port)
- {
- if (port->Bus())
- continue;
+ if (inst->Type() == OPER_MULTIPLIER) {
+ module->addMul(inst_name, IN1, IN2, OUT, SIGNED);
+ return true;
+ }
- if (verbose)
- log(" importing port %s.\n", port->Name());
+ if (inst->Type() == OPER_DIVIDER) {
+ module->addDiv(inst_name, IN1, IN2, OUT, SIGNED);
+ return true;
+ }
- RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
- import_attributes(wire->attributes, port);
+ if (inst->Type() == OPER_MODULO) {
+ module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
+ return true;
+ }
- wire->port_id = nl->IndexOf(port) + 1;
+ if (inst->Type() == OPER_REMAINDER) {
+ module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
+ return true;
+ }
- if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_IN)
- wire->port_input = true;
- if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_OUT)
- wire->port_output = true;
+ if (inst->Type() == OPER_SHIFT_LEFT) {
+ module->addShl(inst_name, IN1, IN2, OUT, false);
+ return true;
+ }
- if (port->GetNet()) {
- net = port->GetNet();
- if (net_map.count(net) == 0)
- net_map[net] = wire;
- else if (wire->port_input)
- module->connect(net_map_at(net), wire);
- else
- module->connect(wire, net_map_at(net));
- }
+ if (inst->Type() == OPER_ENABLED_DECODER) {
+ RTLIL::SigSpec vec;
+ vec.append(net_map_at(inst->GetControl()));
+ for (unsigned i = 1; i < inst->OutputSize(); i++) {
+ vec.append(RTLIL::State::S0);
}
+ module->addShl(inst_name, vec, IN, OUT, false);
+ return true;
+ }
- FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
- {
- if (verbose)
- log(" importing portbus %s.\n", portbus->Name());
-
- RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size());
- wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
- import_attributes(wire->attributes, portbus);
-
- if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN)
- 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()) {
- 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)
- module->connect(net_map_at(net), bit);
- else
- module->connect(bit, net_map_at(net));
- }
- if (i == portbus->RightIndex())
- break;
- }
- }
-
- module->fixup_ports();
-
- dict<Net*, char, hash_ptr_ops> init_nets;
- pool<Net*, hash_ptr_ops> anyconst_nets;
- pool<Net*, hash_ptr_ops> anyseq_nets;
-
- FOREACH_NET_OF_NETLIST(nl, mi, net)
- {
- if (net->IsRamNet())
- {
- RTLIL::Memory *memory = new RTLIL::Memory;
- memory->name = RTLIL::escape_id(net->Name());
- log_assert(module->count_id(memory->name) == 0);
- module->memories[memory->name] = memory;
-
- int number_of_bits = net->Size();
- int bits_in_word = number_of_bits;
- FOREACH_PORTREF_OF_NET(net, si, pr) {
- if (pr->GetInst()->Type() == OPER_READ_PORT) {
- bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize());
- continue;
- }
- if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) {
- bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size());
- continue;
- }
- log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
- net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name());
- }
-
- memory->width = bits_in_word;
- memory->size = number_of_bits / bits_in_word;
-
- const char *ascii_initdata = net->GetWideInitialValue();
- if (ascii_initdata) {
- while (*ascii_initdata != 0 && *ascii_initdata != '\'')
- ascii_initdata++;
- if (*ascii_initdata == '\'')
- ascii_initdata++;
- if (*ascii_initdata != 0) {
- log_assert(*ascii_initdata == 'b');
- ascii_initdata++;
- }
- for (int word_idx = 0; word_idx < memory->size; word_idx++) {
- Const initval = Const(State::Sx, memory->width);
- bool initval_valid = false;
- for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) {
- if (*ascii_initdata == 0)
- break;
- if (*ascii_initdata == '0' || *ascii_initdata == '1') {
- initval[bit_idx] = (*ascii_initdata == '0') ? State::S0 : State::S1;
- initval_valid = true;
- }
- ascii_initdata++;
- }
- if (initval_valid) {
- RTLIL::Cell *cell = module->addCell(NEW_ID, "$meminit");
- cell->parameters["\\WORDS"] = 1;
- if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound())
- cell->setPort("\\ADDR", word_idx);
- else
- cell->setPort("\\ADDR", memory->size - word_idx - 1);
- cell->setPort("\\DATA", initval);
- cell->parameters["\\MEMID"] = RTLIL::Const(memory->name.str());
- cell->parameters["\\ABITS"] = 32;
- cell->parameters["\\WIDTH"] = memory->width;
- cell->parameters["\\PRIORITY"] = RTLIL::Const(autoidx-1);
- }
- }
- }
- continue;
- }
-
- if (net->GetInitialValue())
- init_nets[net] = net->GetInitialValue();
-
- const char *rand_const_attr = net->GetAttValue(" rand_const");
- const char *rand_attr = net->GetAttValue(" rand");
-
- if (rand_const_attr != nullptr && !strcmp(rand_const_attr, "1"))
- anyconst_nets.insert(net);
-
- else if (rand_attr != nullptr && !strcmp(rand_attr, "1"))
- anyseq_nets.insert(net);
-
- if (net_map.count(net)) {
- if (verbose)
- log(" skipping net %s.\n", net->Name());
- continue;
- }
-
- if (net->Bus())
- continue;
-
- RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : NEW_ID);
-
- if (verbose)
- log(" importing net %s as %s.\n", net->Name(), log_id(wire_name));
-
- RTLIL::Wire *wire = module->addWire(wire_name);
- import_attributes(wire->attributes, net);
-
- net_map[net] = wire;
+ if (inst->Type() == OPER_DECODER) {
+ RTLIL::SigSpec vec;
+ vec.append(RTLIL::State::S1);
+ for (unsigned i = 1; i < inst->OutputSize(); i++) {
+ vec.append(RTLIL::State::S0);
}
+ module->addShl(inst_name, vec, IN, OUT, false);
+ return true;
+ }
- FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus)
- {
- bool found_new_net = false;
- for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
- net = netbus->ElementAtIndex(i);
- if (net_map.count(net) == 0)
- found_new_net = true;
- if (i == netbus->RightIndex())
- break;
- }
-
- if (found_new_net)
- {
- RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : NEW_ID);
-
- if (verbose)
- log(" importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name));
-
- RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
- wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
- import_attributes(wire->attributes, netbus);
-
- RTLIL::Const initval = Const(State::Sx, GetSize(wire));
- bool initval_valid = false;
-
- for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1)
- {
- if (netbus->ElementAtIndex(i))
- {
- int bitidx = i - wire->start_offset;
- net = netbus->ElementAtIndex(i);
- RTLIL::SigBit bit(wire, bitidx);
-
- if (init_nets.count(net)) {
- if (init_nets.at(net) == '0')
- initval.bits.at(bitidx) = State::S0;
- if (init_nets.at(net) == '1')
- initval.bits.at(bitidx) = State::S1;
- initval_valid = true;
- init_nets.erase(net);
- }
-
- if (net_map.count(net) == 0)
- net_map[net] = bit;
- else
- module->connect(bit, net_map_at(net));
- }
-
- if (i == netbus->RightIndex())
- break;
- }
-
- if (initval_valid)
- wire->attributes["\\init"] = initval;
- }
- else
- {
- if (verbose)
- log(" skipping netbus %s.\n", netbus->Name());
- }
-
- SigSpec anyconst_sig;
- SigSpec anyseq_sig;
-
- for (int i = netbus->RightIndex();; i += netbus->IsUp() ? -1 : +1) {
- net = netbus->ElementAtIndex(i);
- if (net != nullptr && anyconst_nets.count(net)) {
- anyconst_sig.append(net_map_at(net));
- anyconst_nets.erase(net);
- }
- if (net != nullptr && anyseq_nets.count(net)) {
- anyseq_sig.append(net_map_at(net));
- anyseq_nets.erase(net);
- }
- if (i == netbus->LeftIndex())
- break;
- }
-
- if (GetSize(anyconst_sig))
- module->connect(anyconst_sig, module->Anyconst(NEW_ID, GetSize(anyconst_sig)));
-
- if (GetSize(anyseq_sig))
- module->connect(anyseq_sig, module->Anyseq(NEW_ID, GetSize(anyseq_sig)));
- }
+ if (inst->Type() == OPER_SHIFT_RIGHT) {
+ Net *net_cin = inst->GetCin();
+ Net *net_a_msb = inst->GetInput1Bit(0);
+ if (net_cin->IsGnd())
+ module->addShr(inst_name, IN1, IN2, OUT, false);
+ else if (net_cin == net_a_msb)
+ 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());
+ return true;
+ }
- for (auto it : init_nets)
- {
- Const initval;
- SigBit bit = net_map_at(it.first);
- log_assert(bit.wire);
+ if (inst->Type() == OPER_REDUCE_AND) {
+ module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+ return true;
+ }
- if (bit.wire->attributes.count("\\init"))
- initval = bit.wire->attributes.at("\\init");
+ if (inst->Type() == OPER_REDUCE_OR) {
+ module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+ return true;
+ }
- while (GetSize(initval) < GetSize(bit.wire))
- initval.bits.push_back(State::Sx);
+ if (inst->Type() == OPER_REDUCE_XOR) {
+ module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+ return true;
+ }
- if (it.second == '0')
- initval.bits.at(bit.offset) = State::S0;
- if (it.second == '1')
- initval.bits.at(bit.offset) = State::S1;
+ if (inst->Type() == OPER_REDUCE_XNOR) {
+ module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+ return true;
+ }
- bit.wire->attributes["\\init"] = initval;
- }
+ 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);
+ else if (net_cin->IsPwr())
+ 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());
+ return true;
+ }
- for (auto net : anyconst_nets)
- module->connect(net_map_at(net), module->Anyconst(NEW_ID));
+ if (inst->Type() == OPER_WIDE_AND) {
+ module->addAnd(inst_name, IN1, IN2, OUT, SIGNED);
+ return true;
+ }
- for (auto net : anyseq_nets)
- module->connect(net_map_at(net), module->Anyseq(NEW_ID));
+ if (inst->Type() == OPER_WIDE_OR) {
+ module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
+ return true;
+ }
- pool<Instance*, hash_ptr_ops> sva_asserts;
- pool<Instance*, hash_ptr_ops> sva_assumes;
- pool<Instance*, hash_ptr_ops> sva_covers;
+ if (inst->Type() == OPER_WIDE_XOR) {
+ module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
+ return true;
+ }
- pool<RTLIL::Cell*> past_ffs;
+ if (inst->Type() == OPER_WIDE_XNOR) {
+ module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
+ return true;
+ }
- FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
- {
- RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID);
+ if (inst->Type() == OPER_WIDE_BUF) {
+ module->addPos(inst_name, IN, OUT, SIGNED);
+ return true;
+ }
- if (verbose)
- log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
+ if (inst->Type() == OPER_WIDE_INV) {
+ module->addNot(inst_name, IN, OUT, SIGNED);
+ return true;
+ }
- if (inst->Type() == PRIM_PWR) {
- module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1);
- continue;
- }
+ if (inst->Type() == OPER_MINUS) {
+ module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
+ return true;
+ }
- if (inst->Type() == PRIM_GND) {
- module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S0);
- continue;
- }
+ if (inst->Type() == OPER_UMINUS) {
+ module->addNeg(inst_name, IN, OUT, SIGNED);
+ return true;
+ }
- if (inst->Type() == PRIM_BUF) {
- module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
- continue;
- }
+ if (inst->Type() == OPER_EQUAL) {
+ module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+ return true;
+ }
- if (inst->Type() == PRIM_X) {
- module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sx);
- continue;
- }
+ if (inst->Type() == OPER_NEQUAL) {
+ module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+ return true;
+ }
- if (inst->Type() == PRIM_Z) {
- module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sz);
- continue;
- }
+ if (inst->Type() == OPER_WIDE_MUX) {
+ module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
+ return true;
+ }
- if (inst->Type() == OPER_READ_PORT)
- {
- RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name()));
- if (memory->width != int(inst->OutputSize()))
- log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
-
- RTLIL::SigSpec addr = operatorInput1(inst);
- RTLIL::SigSpec data = operatorOutput(inst);
-
- RTLIL::Cell *cell = module->addCell(inst_name, "$memrd");
- cell->parameters["\\MEMID"] = memory->name.str();
- cell->parameters["\\CLK_ENABLE"] = false;
- cell->parameters["\\CLK_POLARITY"] = true;
- cell->parameters["\\TRANSPARENT"] = false;
- cell->parameters["\\ABITS"] = GetSize(addr);
- cell->parameters["\\WIDTH"] = GetSize(data);
- cell->setPort("\\CLK", RTLIL::State::Sx);
- cell->setPort("\\EN", RTLIL::State::Sx);
- cell->setPort("\\ADDR", addr);
- cell->setPort("\\DATA", data);
- continue;
- }
+ if (inst->Type() == OPER_WIDE_TRI) {
+ module->addMux(inst_name, RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT);
+ return true;
+ }
- 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 asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->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()));
- }
- continue;
- }
+ if (inst->Type() == OPER_WIDE_DFFRS) {
+ 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())
+ module->addDff(inst_name, net_map_at(inst->GetClock()), IN, OUT);
+ else
+ module->addDffsr(inst_name, net_map_at(inst->GetClock()), sig_set, sig_reset, IN, OUT);
+ return true;
+ }
- if (!mode_gates) {
- if (import_netlist_instance_cells(inst, inst_name))
- continue;
- if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()))
- log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
- } else {
- if (import_netlist_instance_gates(inst, inst_name))
- continue;
- }
+ #undef IN
+ #undef IN1
+ #undef IN2
+ #undef OUT
+ #undef SIGNED
- if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
- sva_asserts.insert(inst);
+ return false;
+}
- if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
- sva_assumes.insert(inst);
+void VerificImporter::merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol)
+{
+ bool keep_running = true;
+ SigMap sigmap;
- if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
- sva_covers.insert(inst);
+ while (keep_running)
+ {
+ keep_running = false;
- if (inst->Type() == OPER_SVA_STABLE && !mode_nosva)
- {
- VerificClockEdge clock_edge(this, inst->GetInput2Bit(0)->Driver());
+ dict<SigBit, pool<RTLIL::Cell*>> dbits_db;
+ SigSpec dbits;
- log_assert(inst->Input1Size() == inst->OutputSize());
+ for (auto cell : candidates) {
+ SigBit bit = sigmap(cell->getPort("\\D"));
+ dbits_db[bit].insert(cell);
+ dbits.append(bit);
+ }
- SigSpec sig_d, sig_q, sig_o;
- sig_q = module->addWire(NEW_ID, inst->Input1Size());
+ dbits.sort_and_unify();
- for (int i = int(inst->Input1Size())-1; i >= 0; i--){
- sig_d.append(net_map_at(inst->GetInput1Bit(i)));
- sig_o.append(net_map_at(inst->GetOutputBit(i)));
- }
+ for (auto chunk : dbits.chunks())
+ {
+ SigSpec sig_d = chunk;
- if (verbose) {
- log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
- log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
- log(" XNOR with A=%s, B=%s, Y=%s.\n",
- log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
- }
+ if (chunk.wire == nullptr || GetSize(sig_d) == 1)
+ continue;
- module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
- module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
+ SigSpec sig_q = module->addWire(NEW_ID, GetSize(sig_d));
+ RTLIL::Cell *new_ff = module->addDff(NEW_ID, clock, sig_d, sig_q, clock_pol);
- if (!mode_keep)
- continue;
- }
+ if (verbose)
+ log(" merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff));
- if (inst->Type() == PRIM_SVA_STABLE && !mode_nosva)
- {
- VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
+ for (int i = 0; i < GetSize(sig_d); i++)
+ for (auto old_ff : dbits_db[sig_d[i]])
+ {
+ if (verbose)
+ log(" replacing old ff %s on bit %d.\n", log_id(old_ff), i);
- SigSpec sig_d = net_map_at(inst->GetInput1());
- SigSpec sig_o = net_map_at(inst->GetOutput());
- SigSpec sig_q = module->addWire(NEW_ID);
+ SigBit old_q = old_ff->getPort("\\Q");
+ SigBit new_q = sig_q[i];
- if (verbose) {
- log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
- log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
- log(" XNOR with A=%s, B=%s, Y=%s.\n",
- log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
+ sigmap.add(old_q, new_q);
+ module->connect(old_q, new_q);
+ candidates.erase(old_ff);
+ module->remove(old_ff);
+ keep_running = true;
}
+ }
+ }
+}
- module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
- module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
+void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
+{
+ dict<pair<SigBit, int>, pool<RTLIL::Cell*>> database;
- if (!mode_keep)
- continue;
- }
+ for (auto cell : candidates)
+ {
+ SigBit clock = cell->getPort("\\CLK");
+ bool clock_pol = cell->getParam("\\CLK_POLARITY").as_bool();
+ database[make_pair(clock, int(clock_pol))].insert(cell);
+ }
- if (inst->Type() == PRIM_SVA_PAST && !mode_nosva)
- {
- VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
+ for (auto it : database)
+ merge_past_ffs_clock(it.second, it.first.first, it.first.second);
+}
- SigBit sig_d = net_map_at(inst->GetInput1());
- SigBit sig_q = net_map_at(inst->GetOutput());
+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());
- if (verbose)
- log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
- log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
+ netlist = nl;
- past_ffs.insert(module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge));
+ if (design->has(module_name)) {
+ if (!nl->IsOperator())
+ log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
+ return;
+ }
- if (!mode_keep)
- continue;
- }
+ module = new RTLIL::Module;
+ module->name = module_name;
+ design->add(module);
- if (!mode_keep && verific_sva_prims.count(inst->Type())) {
- if (verbose)
- log(" skipping SVA cell in non k-mode\n");
- continue;
- }
+ if (nl->IsBlackBox()) {
+ log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name));
+ module->set_bool_attribute("\\blackbox");
+ } else {
+ log("Importing module %s.\n", RTLIL::id2cstr(module->name));
+ }
- if (inst->IsPrimitive())
- {
- if (inst->Type() == PRIM_HDL_ASSERTION)
- continue;
+ SetIter si;
+ MapIter mi, mi2;
+ Port *port;
+ PortBus *portbus;
+ Net *net;
+ NetBus *netbus;
+ Instance *inst;
+ PortRef *pr;
- if (!mode_keep)
- log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
+ if (!mode_nosvapp)
+ {
+ vector<Instance*> asserts, assumes, covers;
- if (!verific_sva_prims.count(inst->Type()))
- log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
- }
+ FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
+ {
+ if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
+ asserts.push_back(inst);
- nl_todo.insert(inst->View());
+ if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
+ assumes.push_back(inst);
- RTLIL::Cell *cell = module->addCell(inst_name, inst->IsOperator() ?
- std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name()));
+ if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
+ covers.push_back(inst);
+ }
- if (inst->IsPrimitive() && mode_keep)
- cell->attributes["\\keep"] = 1;
+ for (auto inst : asserts)
+ svapp_assert(inst);
- dict<IdString, vector<SigBit>> cell_port_conns;
+ for (auto inst : assumes)
+ svapp_assume(inst);
- if (verbose)
- log(" ports in verific db:\n");
+ for (auto inst : covers)
+ svapp_cover(inst);
+ }
- FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
- if (verbose)
- log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
- const char *port_name = pr->GetPort()->Name();
- int port_offset = 0;
- if (pr->GetPort()->Bus()) {
- port_name = pr->GetPort()->Bus()->Name();
- port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
- min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
- }
- 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));
- for (auto bit : zwires)
- sigvec.push_back(bit);
- }
- sigvec[port_offset] = net_map_at(pr->GetNet());
- }
+ FOREACH_PORT_OF_NETLIST(nl, mi, port)
+ {
+ if (port->Bus())
+ continue;
- if (verbose)
- log(" ports in yosys db:\n");
+ if (verbose)
+ log(" importing port %s.\n", port->Name());
- for (auto &it : cell_port_conns) {
- if (verbose)
- log(" .%s(%s)\n", log_id(it.first), log_signal(it.second));
- cell->setPort(it.first, it.second);
- }
- }
+ RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
+ import_attributes(wire->attributes, port);
- if (!mode_nosva)
- {
- for (auto inst : sva_asserts)
- import_sva_assert(this, inst);
+ wire->port_id = nl->IndexOf(port) + 1;
- for (auto inst : sva_assumes)
- import_sva_assume(this, inst);
+ if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_IN)
+ wire->port_input = true;
+ if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_OUT)
+ wire->port_output = true;
- for (auto inst : sva_covers)
- import_sva_cover(this, inst);
+ if (port->GetNet()) {
+ net = port->GetNet();
+ if (net_map.count(net) == 0)
+ net_map[net] = wire;
+ else if (wire->port_input)
+ module->connect(net_map_at(net), wire);
+ else
+ module->connect(wire, net_map_at(net));
+ }
+ }
- merge_past_ffs(past_ffs);
+ FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
+ {
+ if (verbose)
+ log(" importing portbus %s.\n", portbus->Name());
+
+ RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size());
+ wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
+ import_attributes(wire->attributes, portbus);
+
+ if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN)
+ 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()) {
+ 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)
+ module->connect(net_map_at(net), bit);
+ else
+ module->connect(bit, net_map_at(net));
+ }
+ if (i == portbus->RightIndex())
+ break;
}
}
-};
-VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
-{
- log_assert(importer != nullptr);
- log_assert(inst != nullptr);
+ module->fixup_ports();
- // SVA posedge/negedge
- if (inst->Type() == PRIM_SVA_POSEDGE)
+ dict<Net*, char, hash_ptr_ops> init_nets;
+ pool<Net*, hash_ptr_ops> anyconst_nets;
+ pool<Net*, hash_ptr_ops> anyseq_nets;
+
+ FOREACH_NET_OF_NETLIST(nl, mi, net)
{
- clock_net = inst->GetInput();
- posedge = true;
+ if (net->IsRamNet())
+ {
+ RTLIL::Memory *memory = new RTLIL::Memory;
+ memory->name = RTLIL::escape_id(net->Name());
+ log_assert(module->count_id(memory->name) == 0);
+ module->memories[memory->name] = memory;
+
+ int number_of_bits = net->Size();
+ int bits_in_word = number_of_bits;
+ FOREACH_PORTREF_OF_NET(net, si, pr) {
+ if (pr->GetInst()->Type() == OPER_READ_PORT) {
+ bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize());
+ continue;
+ }
+ if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) {
+ bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size());
+ continue;
+ }
+ log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
+ net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name());
+ }
- Instance *driver = clock_net->Driver();
- if (!clock_net->IsMultipleDriven() && driver && driver->Type() == PRIM_INV) {
- clock_net = driver->GetInput();
- posedge = false;
+ memory->width = bits_in_word;
+ memory->size = number_of_bits / bits_in_word;
+
+ const char *ascii_initdata = net->GetWideInitialValue();
+ if (ascii_initdata) {
+ while (*ascii_initdata != 0 && *ascii_initdata != '\'')
+ ascii_initdata++;
+ if (*ascii_initdata == '\'')
+ ascii_initdata++;
+ if (*ascii_initdata != 0) {
+ log_assert(*ascii_initdata == 'b');
+ ascii_initdata++;
+ }
+ for (int word_idx = 0; word_idx < memory->size; word_idx++) {
+ Const initval = Const(State::Sx, memory->width);
+ bool initval_valid = false;
+ for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) {
+ if (*ascii_initdata == 0)
+ break;
+ if (*ascii_initdata == '0' || *ascii_initdata == '1') {
+ initval[bit_idx] = (*ascii_initdata == '0') ? State::S0 : State::S1;
+ initval_valid = true;
+ }
+ ascii_initdata++;
+ }
+ if (initval_valid) {
+ RTLIL::Cell *cell = module->addCell(NEW_ID, "$meminit");
+ cell->parameters["\\WORDS"] = 1;
+ if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound())
+ cell->setPort("\\ADDR", word_idx);
+ else
+ cell->setPort("\\ADDR", memory->size - word_idx - 1);
+ cell->setPort("\\DATA", initval);
+ cell->parameters["\\MEMID"] = RTLIL::Const(memory->name.str());
+ cell->parameters["\\ABITS"] = 32;
+ cell->parameters["\\WIDTH"] = memory->width;
+ cell->parameters["\\PRIORITY"] = RTLIL::Const(autoidx-1);
+ }
+ }
+ }
+ continue;
}
- clock_sig = importer->net_map_at(clock_net);
- return;
- }
-}
+ if (net->GetInitialValue())
+ init_nets[net] = net->GetInitialValue();
-// ==================================================================
+ const char *rand_const_attr = net->GetAttValue(" rand_const");
+ const char *rand_attr = net->GetAttValue(" rand");
-struct VerificSvaImporter
-{
- VerificImporter *importer;
- Module *module;
+ if (rand_const_attr != nullptr && !strcmp(rand_const_attr, "1"))
+ anyconst_nets.insert(net);
- Netlist *netlist;
- Instance *root;
+ else if (rand_attr != nullptr && !strcmp(rand_attr, "1"))
+ anyseq_nets.insert(net);
- SigBit clock = State::Sx;
- bool clock_posedge = false;
+ if (net_map.count(net)) {
+ if (verbose)
+ log(" skipping net %s.\n", net->Name());
+ continue;
+ }
- SigBit disable_iff = State::S0;
+ if (net->Bus())
+ continue;
- bool mode_assert = false;
- bool mode_assume = false;
- bool mode_cover = false;
- bool eventually = false;
- bool did_something = false;
+ RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : NEW_ID);
- Instance *net_to_ast_driver(Net *n)
- {
- if (n == nullptr)
- return nullptr;
+ if (verbose)
+ log(" importing net %s as %s.\n", net->Name(), log_id(wire_name));
- if (n->IsMultipleDriven())
- return nullptr;
+ RTLIL::Wire *wire = module->addWire(wire_name);
+ import_attributes(wire->attributes, net);
- Instance *inst = n->Driver();
+ net_map[net] = wire;
+ }
- if (inst == nullptr)
- return nullptr;
+ FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus)
+ {
+ bool found_new_net = false;
+ for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
+ net = netbus->ElementAtIndex(i);
+ if (net_map.count(net) == 0)
+ found_new_net = true;
+ if (i == netbus->RightIndex())
+ break;
+ }
- if (!verific_sva_prims.count(inst->Type()))
- return nullptr;
+ if (found_new_net)
+ {
+ RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : NEW_ID);
- if (inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL ||
- inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE || inst->Type() == PRIM_SVA_PAST)
- return nullptr;
+ if (verbose)
+ log(" importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name));
- return inst;
- }
+ RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
+ wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
+ import_attributes(wire->attributes, netbus);
- Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); }
- Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); }
- Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); }
- Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
- Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
+ RTLIL::Const initval = Const(State::Sx, GetSize(wire));
+ bool initval_valid = false;
- // ----------------------------------------------------------
- // SVA Preprocessor
+ for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1)
+ {
+ if (netbus->ElementAtIndex(i))
+ {
+ int bitidx = i - wire->start_offset;
+ net = netbus->ElementAtIndex(i);
+ RTLIL::SigBit bit(wire, bitidx);
+
+ if (init_nets.count(net)) {
+ if (init_nets.at(net) == '0')
+ initval.bits.at(bitidx) = State::S0;
+ if (init_nets.at(net) == '1')
+ initval.bits.at(bitidx) = State::S1;
+ initval_valid = true;
+ init_nets.erase(net);
+ }
- Net *rewrite_input(Instance *inst) { return rewrite(get_ast_input(inst), inst->GetInput()); }
- Net *rewrite_input1(Instance *inst) { return rewrite(get_ast_input1(inst), inst->GetInput1()); }
- Net *rewrite_input2(Instance *inst) { return rewrite(get_ast_input2(inst), inst->GetInput2()); }
- Net *rewrite_input3(Instance *inst) { return rewrite(get_ast_input3(inst), inst->GetInput3()); }
- Net *rewrite_control(Instance *inst) { return rewrite(get_ast_control(inst), inst->GetControl()); }
+ if (net_map.count(net) == 0)
+ net_map[net] = bit;
+ else
+ module->connect(bit, net_map_at(net));
+ }
- Net *rewrite(Instance *inst, Net *default_net = nullptr)
- {
- if (inst == nullptr)
- return default_net;
-
- if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME ||
- inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) {
- Net *new_net = rewrite(get_ast_input(inst));
- if (new_net) {
- inst->Disconnect(inst->View()->GetInput());
- inst->Connect(inst->View()->GetInput(), new_net);
+ if (i == netbus->RightIndex())
+ break;
}
- return default_net;
- }
- if (inst->Type() == PRIM_SVA_AT || inst->Type() == PRIM_SVA_DISABLE_IFF) {
- Net *new_net = rewrite(get_ast_input2(inst));
- if (new_net) {
- inst->Disconnect(inst->View()->GetInput2());
- inst->Connect(inst->View()->GetInput2(), new_net);
- }
- return default_net;
+ if (initval_valid)
+ wire->attributes["\\init"] = initval;
}
-
- if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+ else
{
- if (mode_cover) {
- did_something = true;
- Net *new_in1 = rewrite_input1(inst);
- Net *new_in2 = rewrite_input2(inst);
- return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile());
- }
- return default_net;
+ if (verbose)
+ log(" skipping netbus %s.\n", netbus->Name());
}
- if (inst->Type() == PRIM_SVA_NOT)
- {
- if (mode_assert || mode_assume) {
- did_something = true;
- Net *new_in = rewrite_input(inst);
- Net *net_zero = netlist->Gnd(inst->Linefile());
- return netlist->SvaBinary(PRIM_SVA_OVERLAPPED_IMPLICATION, new_in, net_zero, inst->Linefile());
+ SigSpec anyconst_sig;
+ SigSpec anyseq_sig;
+
+ for (int i = netbus->RightIndex();; i += netbus->IsUp() ? -1 : +1) {
+ net = netbus->ElementAtIndex(i);
+ if (net != nullptr && anyconst_nets.count(net)) {
+ anyconst_sig.append(net_map_at(net));
+ anyconst_nets.erase(net);
+ }
+ if (net != nullptr && anyseq_nets.count(net)) {
+ anyseq_sig.append(net_map_at(net));
+ anyseq_nets.erase(net);
}
- return default_net;
+ if (i == netbus->LeftIndex())
+ break;
}
- return default_net;
+ if (GetSize(anyconst_sig))
+ module->connect(anyconst_sig, module->Anyconst(NEW_ID, GetSize(anyconst_sig)));
+
+ if (GetSize(anyseq_sig))
+ module->connect(anyseq_sig, module->Anyseq(NEW_ID, GetSize(anyseq_sig)));
}
- void rewrite()
+ for (auto it : init_nets)
{
- netlist = root->Owner();
- do {
- did_something = false;
- rewrite(root);
- } while (did_something);
- }
+ Const initval;
+ SigBit bit = net_map_at(it.first);
+ log_assert(bit.wire);
- // ----------------------------------------------------------
- // SVA Inporter
+ if (bit.wire->attributes.count("\\init"))
+ initval = bit.wire->attributes.at("\\init");
- struct sequence_t {
- int length = 0;
- SigBit sig_a = State::S1;
- SigBit sig_en = State::S1;
- };
+ while (GetSize(initval) < GetSize(bit.wire))
+ initval.bits.push_back(State::Sx);
- void sequence_cond(sequence_t &seq, SigBit cond)
- {
- seq.sig_a = module->And(NEW_ID, seq.sig_a, cond);
- }
+ if (it.second == '0')
+ initval.bits.at(bit.offset) = State::S0;
+ if (it.second == '1')
+ initval.bits.at(bit.offset) = State::S1;
- void sequence_ff(sequence_t &seq)
- {
- if (disable_iff != State::S0)
- seq.sig_en = module->Mux(NEW_ID, seq.sig_en, State::S0, disable_iff);
+ bit.wire->attributes["\\init"] = initval;
+ }
- Wire *sig_a_q = module->addWire(NEW_ID);
- sig_a_q->attributes["\\init"] = Const(0, 1);
+ for (auto net : anyconst_nets)
+ module->connect(net_map_at(net), module->Anyconst(NEW_ID));
- Wire *sig_en_q = module->addWire(NEW_ID);
- sig_en_q->attributes["\\init"] = Const(0, 1);
+ for (auto net : anyseq_nets)
+ module->connect(net_map_at(net), module->Anyseq(NEW_ID));
- module->addDff(NEW_ID, clock, seq.sig_a, sig_a_q, clock_posedge);
- module->addDff(NEW_ID, clock, seq.sig_en, sig_en_q, clock_posedge);
+ pool<Instance*, hash_ptr_ops> sva_asserts;
+ pool<Instance*, hash_ptr_ops> sva_assumes;
+ pool<Instance*, hash_ptr_ops> sva_covers;
- seq.length++;
- seq.sig_a = sig_a_q;
- seq.sig_en = sig_en_q;
- }
+ pool<RTLIL::Cell*> past_ffs;
- void parse_sequence(sequence_t &seq, Net *n)
+ FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
{
- Instance *inst = net_to_ast_driver(n);
+ RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID);
- // Regular expression
+ if (verbose)
+ log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
- if (inst == nullptr) {
- sequence_cond(seq, importer->net_map_at(n));
- return;
+ if (inst->Type() == PRIM_PWR) {
+ module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1);
+ continue;
}
- // SVA Primitives
+ if (inst->Type() == PRIM_GND) {
+ module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S0);
+ continue;
+ }
- if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION)
- {
- parse_sequence(seq, inst->GetInput1());
- seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
- parse_sequence(seq, inst->GetInput2());
- return;
+ if (inst->Type() == PRIM_BUF) {
+ module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ continue;
}
- if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
- {
- parse_sequence(seq, inst->GetInput1());
- seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
- sequence_ff(seq);
- parse_sequence(seq, inst->GetInput2());
- return;
+ if (inst->Type() == PRIM_X) {
+ module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sx);
+ continue;
+ }
+
+ if (inst->Type() == PRIM_Z) {
+ module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sz);
+ continue;
}
- if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
+ if (inst->Type() == OPER_READ_PORT)
+ {
+ RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name()));
+ if (memory->width != int(inst->OutputSize()))
+ log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
+
+ RTLIL::SigSpec addr = operatorInput1(inst);
+ RTLIL::SigSpec data = operatorOutput(inst);
+
+ RTLIL::Cell *cell = module->addCell(inst_name, "$memrd");
+ cell->parameters["\\MEMID"] = memory->name.str();
+ cell->parameters["\\CLK_ENABLE"] = false;
+ cell->parameters["\\CLK_POLARITY"] = true;
+ cell->parameters["\\TRANSPARENT"] = false;
+ cell->parameters["\\ABITS"] = GetSize(addr);
+ cell->parameters["\\WIDTH"] = GetSize(data);
+ cell->setPort("\\CLK", RTLIL::State::Sx);
+ cell->setPort("\\EN", RTLIL::State::Sx);
+ cell->setPort("\\ADDR", addr);
+ cell->setPort("\\DATA", data);
+ continue;
+ }
+
+ if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT)
{
- int sva_low = atoi(inst->GetAttValue("sva:low"));
- int sva_high = atoi(inst->GetAttValue("sva:low"));
+ RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name()));
+ if (memory->width != int(inst->Input2Size()))
+ log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->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()));
+ }
+ continue;
+ }
- if (sva_low != sva_high)
- log_error("Ranges on SVA sequence concatenation operator are not supported at the moment.\n");
+ if (!mode_gates) {
+ if (import_netlist_instance_cells(inst, inst_name))
+ continue;
+ if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()))
+ log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
+ } else {
+ if (import_netlist_instance_gates(inst, inst_name))
+ continue;
+ }
- parse_sequence(seq, inst->GetInput1());
+ if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
+ sva_asserts.insert(inst);
- for (int i = 0; i < sva_low; i++)
- sequence_ff(seq);
+ if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
+ sva_assumes.insert(inst);
- parse_sequence(seq, inst->GetInput2());
- return;
- }
+ if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
+ sva_covers.insert(inst);
- if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
+ if (inst->Type() == OPER_SVA_STABLE && !mode_nosva)
{
- int sva_low = atoi(inst->GetAttValue("sva:low"));
- int sva_high = atoi(inst->GetAttValue("sva:low"));
+ VerificClockEdge clock_edge(this, inst->GetInput2Bit(0)->Driver());
- if (sva_low != sva_high)
- log_error("Ranges on SVA consecutive repeat operator are not supported at the moment.\n");
+ log_assert(inst->Input1Size() == inst->OutputSize());
- parse_sequence(seq, inst->GetInput());
+ SigSpec sig_d, sig_q, sig_o;
+ sig_q = module->addWire(NEW_ID, inst->Input1Size());
- for (int i = 1; i < sva_low; i++) {
- sequence_ff(seq);
- parse_sequence(seq, inst->GetInput());
+ for (int i = int(inst->Input1Size())-1; i >= 0; i--){
+ sig_d.append(net_map_at(inst->GetInput1Bit(i)));
+ sig_o.append(net_map_at(inst->GetOutputBit(i)));
}
- return;
- }
- // Handle unsupported primitives
-
- if (!importer->mode_keep)
- log_error("Unsupported Verific SVA primitive %s of type %s.\n", inst->Name(), inst->View()->Owner()->Name());
- log_warning("Unsupported Verific SVA primitive %s of type %s.\n", inst->Name(), inst->View()->Owner()->Name());
- }
+ if (verbose) {
+ log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
+ log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
+ log(" XNOR with A=%s, B=%s, Y=%s.\n",
+ log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
+ }
- void import()
- {
- module = importer->module;
- netlist = root->Owner();
+ module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
+ module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
- RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
+ if (!mode_keep)
+ continue;
+ }
- // parse SVA property clock event
+ if (inst->Type() == PRIM_SVA_STABLE && !mode_nosva)
+ {
+ VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
- Instance *at_node = get_ast_input(root);
+ SigSpec sig_d = net_map_at(inst->GetInput1());
+ SigSpec sig_o = net_map_at(inst->GetOutput());
+ SigSpec sig_q = module->addWire(NEW_ID);
- // asynchronous immediate assertion/assumption/cover
- if (at_node == nullptr && (root->Type() == PRIM_SVA_IMMEDIATE_ASSERT ||
- root->Type() == PRIM_SVA_IMMEDIATE_COVER || root->Type() == PRIM_SVA_IMMEDIATE_ASSUME))
- {
- SigSpec sig_a = importer->net_map_at(root->GetInput());
- RTLIL::Cell *c = nullptr;
-
- if (eventually) {
- if (mode_assert) c = module->addLive(root_name, sig_a, State::S1);
- if (mode_assume) c = module->addFair(root_name, sig_a, State::S1);
- } else {
- if (mode_assert) c = module->addAssert(root_name, sig_a, State::S1);
- if (mode_assume) c = module->addAssume(root_name, sig_a, State::S1);
- if (mode_cover) c = module->addCover(root_name, sig_a, State::S1);
+ if (verbose) {
+ log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
+ log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
+ log(" XNOR with A=%s, B=%s, Y=%s.\n",
+ log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
}
- importer->import_attributes(c->attributes, root);
- return;
- }
+ module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
+ module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
- log_assert(at_node && at_node->Type() == PRIM_SVA_AT);
+ if (!mode_keep)
+ continue;
+ }
- VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
- clock = clock_edge.clock_sig;
- clock_posedge = clock_edge.posedge;
+ if (inst->Type() == PRIM_SVA_PAST && !mode_nosva)
+ {
+ VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
- // parse disable_iff expression
+ SigBit sig_d = net_map_at(inst->GetInput1());
+ SigBit sig_q = net_map_at(inst->GetOutput());
- Net *sequence_net = at_node->GetInput2();
+ if (verbose)
+ log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
+ log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
- while (1)
- {
- Instance *sequence_node = net_to_ast_driver(sequence_net);
+ past_ffs.insert(module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge));
- if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) {
- eventually = true;
- sequence_net = sequence_node->GetInput();
+ if (!mode_keep)
continue;
- }
+ }
- if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) {
- disable_iff = importer->net_map_at(sequence_node->GetInput1());
- sequence_net = sequence_node->GetInput2();
+ if (!mode_keep && verific_sva_prims.count(inst->Type())) {
+ if (verbose)
+ log(" skipping SVA cell in non k-mode\n");
+ continue;
+ }
+
+ if (inst->IsPrimitive())
+ {
+ if (inst->Type() == PRIM_HDL_ASSERTION)
continue;
- }
- break;
+ if (!mode_keep)
+ log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
+
+ if (!verific_sva_prims.count(inst->Type()))
+ log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
}
- // parse SVA sequence into trigger signal
+ nl_todo.insert(inst->View());
- sequence_t seq;
- parse_sequence(seq, sequence_net);
- sequence_ff(seq);
+ RTLIL::Cell *cell = module->addCell(inst_name, inst->IsOperator() ?
+ std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name()));
- // generate assert/assume/cover cell
+ if (inst->IsPrimitive() && mode_keep)
+ cell->attributes["\\keep"] = 1;
- RTLIL::Cell *c = nullptr;
+ dict<IdString, vector<SigBit>> cell_port_conns;
- if (eventually) {
- if (mode_assert) c = module->addLive(root_name, seq.sig_a, seq.sig_en);
- if (mode_assume) c = module->addFair(root_name, seq.sig_a, seq.sig_en);
- } else {
- if (mode_assert) c = module->addAssert(root_name, seq.sig_a, seq.sig_en);
- if (mode_assume) c = module->addAssume(root_name, seq.sig_a, seq.sig_en);
- if (mode_cover) c = module->addCover(root_name, seq.sig_a, seq.sig_en);
+ if (verbose)
+ log(" ports in verific db:\n");
+
+ FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
+ if (verbose)
+ log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
+ const char *port_name = pr->GetPort()->Name();
+ int port_offset = 0;
+ if (pr->GetPort()->Bus()) {
+ port_name = pr->GetPort()->Bus()->Name();
+ port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
+ min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
+ }
+ 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));
+ for (auto bit : zwires)
+ sigvec.push_back(bit);
+ }
+ sigvec[port_offset] = net_map_at(pr->GetNet());
}
- importer->import_attributes(c->attributes, root);
+ if (verbose)
+ log(" ports in yosys db:\n");
+
+ for (auto &it : cell_port_conns) {
+ if (verbose)
+ log(" .%s(%s)\n", log_id(it.first), log_signal(it.second));
+ cell->setPort(it.first, it.second);
+ }
}
-};
-void svapp_assert(Instance *inst)
-{
- VerificSvaImporter worker;
- worker.root = inst;
- worker.mode_assert = true;
- worker.rewrite();
-}
+ if (!mode_nosva)
+ {
+ for (auto inst : sva_asserts)
+ import_sva_assert(this, inst);
-void svapp_assume(Instance *inst)
-{
- VerificSvaImporter worker;
- worker.root = inst;
- worker.mode_assume = true;
- worker.rewrite();
-}
+ for (auto inst : sva_assumes)
+ import_sva_assume(this, inst);
-void svapp_cover(Instance *inst)
-{
- VerificSvaImporter worker;
- worker.root = inst;
- worker.mode_cover = true;
- worker.rewrite();
-}
+ for (auto inst : sva_covers)
+ import_sva_cover(this, inst);
-void import_sva_assert(VerificImporter *importer, Instance *inst)
-{
- VerificSvaImporter worker;
- worker.importer = importer;
- worker.root = inst;
- worker.mode_assert = true;
- worker.import();
+ merge_past_ffs(past_ffs);
+ }
}
-void import_sva_assume(VerificImporter *importer, Instance *inst)
-{
- VerificSvaImporter worker;
- worker.importer = importer;
- worker.root = inst;
- worker.mode_assume = true;
- worker.import();
-}
+// ==================================================================
-void import_sva_cover(VerificImporter *importer, Instance *inst)
+VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
{
- VerificSvaImporter worker;
- worker.importer = importer;
- worker.root = inst;
- worker.mode_cover = true;
- worker.import();
+ log_assert(importer != nullptr);
+ log_assert(inst != nullptr);
+
+ // SVA posedge/negedge
+ if (inst->Type() == PRIM_SVA_POSEDGE)
+ {
+ clock_net = inst->GetInput();
+ posedge = true;
+
+ Instance *driver = clock_net->Driver();
+ if (!clock_net->IsMultipleDriven() && driver && driver->Type() == PRIM_INV) {
+ clock_net = driver->GetInput();
+ posedge = false;
+ }
+
+ clock_sig = importer->net_map_at(clock_net);
+ return;
+ }
}
// ==================================================================
}
};
+YOSYS_NAMESPACE_END
#endif /* YOSYS_ENABLE_VERIFIC */
+PRIVATE_NAMESPACE_BEGIN
+
struct VerificPass : public Pass {
VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
virtual void help()
projects / yosys.git / commitdiff