From 5fa2aa27417447e62cee6edfbf6c1fb07d7b17b0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 18 Feb 2018 13:52:49 +0100 Subject: [PATCH] Move Verific SVA importer to extra C++ source file Signed-off-by: Clifford Wolf --- frontends/verific/Makefile.inc | 2 + frontends/verific/verific.cc | 2232 +++++++++++++------------------ frontends/verific/verific.h | 79 ++ frontends/verific/verificsva.cc | 384 ++++++ 4 files changed, 1394 insertions(+), 1303 deletions(-) create mode 100644 frontends/verific/verific.h create mode 100644 frontends/verific/verificsva.cc diff --git a/frontends/verific/Makefile.inc b/frontends/verific/Makefile.inc index debaac0c5..972f4f9f1 100644 --- a/frontends/verific/Makefile.inc +++ b/frontends/verific/Makefile.inc @@ -3,6 +3,8 @@ OBJS += frontends/verific/verific.o ifeq ($(ENABLE_VERIFIC),1) +OBJS += frontends/verific/verificsva.o + EXTRA_TARGETS += share/verific share/verific: diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 12f572ae2..4925389ae 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -29,6 +29,8 @@ # include #endif +#include "frontends/verific/verific.h" + USING_YOSYS_NAMESPACE #ifdef YOSYS_ENABLE_VERIFIC @@ -43,7 +45,6 @@ USING_YOSYS_NAMESPACE #include "VeriModule.h" #include "VeriWrite.h" #include "VhdlUnits.h" -#include "DataBase.h" #include "Message.h" #ifdef __clang__ @@ -51,14 +52,13 @@ USING_YOSYS_NAMESPACE #endif #ifdef VERIFIC_NAMESPACE -using namespace Verific ; +using namespace Verific; #endif #endif -PRIVATE_NAMESPACE_BEGIN - #ifdef YOSYS_ENABLE_VERIFIC +YOSYS_NAMESPACE_BEGIN pool verific_sva_prims = { // Copy&paste from Verific 3.16_484_32_170630 Netlist.h @@ -118,1529 +118,1152 @@ string get_full_netlist_name(Netlist *nl) 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_map; - std::map 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 &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 &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 &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> 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 &candidates) + if (inst->Type() == PRIM_FADD) { - dict, pool> 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 &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 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 init_nets; - pool anyconst_nets; - pool 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(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(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 sva_asserts; - pool sva_assumes; - pool sva_covers; + if (inst->Type() == OPER_WIDE_XOR) { + module->addXor(inst_name, IN1, IN2, OUT, SIGNED); + return true; + } - pool 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 &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> 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 &candidates) +{ + dict, pool> 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 &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 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> 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 init_nets; + pool anyconst_nets; + pool 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(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(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 sva_asserts; + pool sva_assumes; + pool sva_covers; - seq.length++; - seq.sig_a = sig_a_q; - seq.sig_en = sig_en_q; - } + pool 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> 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; + } } // ================================================================== @@ -1728,8 +1351,11 @@ struct VerificExtNets } }; +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() diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h new file mode 100644 index 000000000..4f1cb5d0f --- /dev/null +++ b/frontends/verific/verific.h @@ -0,0 +1,79 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#ifdef YOSYS_ENABLE_VERIFIC + +#include "DataBase.h" + +YOSYS_NAMESPACE_BEGIN + +extern pool verific_sva_prims; + +struct VerificImporter; + +struct VerificClockEdge { + Verific::Net *clock_net = nullptr; + SigBit clock_sig = State::Sx; + bool posedge = false; + VerificClockEdge(VerificImporter *importer, Verific::Instance *inst); +}; + +struct VerificImporter +{ + RTLIL::Module *module; + Verific::Netlist *netlist; + + std::map net_map; + std::map sva_posedge_map; + + bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose; + + VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose); + + RTLIL::SigBit net_map_at(Verific::Net *net); + + void import_attributes(dict &attributes, Verific::DesignObj *obj); + + RTLIL::SigSpec operatorInput(Verific::Instance *inst); + RTLIL::SigSpec operatorInput1(Verific::Instance *inst); + RTLIL::SigSpec operatorInput2(Verific::Instance *inst); + RTLIL::SigSpec operatorInport(Verific::Instance *inst, const char *portname); + RTLIL::SigSpec operatorOutput(Verific::Instance *inst); + + bool import_netlist_instance_gates(Verific::Instance *inst, RTLIL::IdString inst_name); + bool import_netlist_instance_cells(Verific::Instance *inst, RTLIL::IdString inst_name); + + void merge_past_ffs_clock(pool &candidates, SigBit clock, bool clock_pol); + void merge_past_ffs(pool &candidates); + + void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set &nl_todo); +}; + + +void import_sva_assert(VerificImporter *importer, Verific::Instance *inst); +void import_sva_assume(VerificImporter *importer, Verific::Instance *inst); +void import_sva_cover(VerificImporter *importer, Verific::Instance *inst); + +void svapp_assert(Verific::Instance *inst); +void svapp_assume(Verific::Instance *inst); +void svapp_cover(Verific::Instance *inst); + +YOSYS_NAMESPACE_END + +#endif diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc new file mode 100644 index 000000000..5a56b2fe0 --- /dev/null +++ b/frontends/verific/verificsva.cc @@ -0,0 +1,384 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/yosys.h" +#include "frontends/verific/verific.h" + +USING_YOSYS_NAMESPACE + +#ifdef VERIFIC_NAMESPACE +using namespace Verific; +#endif + +YOSYS_NAMESPACE_BEGIN + +struct VerificSvaImporter +{ + VerificImporter *importer = nullptr; + Module *module = nullptr; + + Netlist *netlist = nullptr; + Instance *root = nullptr; + + SigBit clock = State::Sx; + bool clock_posedge = false; + + SigBit disable_iff = State::S0; + + bool mode_assert = false; + bool mode_assume = false; + bool mode_cover = false; + bool eventually = false; + bool did_something = false; + + Instance *net_to_ast_driver(Net *n) + { + if (n == nullptr) + return nullptr; + + if (n->IsMultipleDriven()) + return nullptr; + + Instance *inst = n->Driver(); + + if (inst == nullptr) + return nullptr; + + if (!verific_sva_prims.count(inst->Type())) + return nullptr; + + 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; + + return inst; + } + + 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()); } + + // ---------------------------------------------------------- + // SVA Preprocessor + + 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()); } + + 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); + } + 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 (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) + { + 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 (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()); + } + return default_net; + } + + return default_net; + } + + void rewrite() + { + netlist = root->Owner(); + do { + did_something = false; + rewrite(root); + } while (did_something); + } + + // ---------------------------------------------------------- + // SVA Importer + + struct sequence_t { + int length = 0; + SigBit sig_a = State::S1; + SigBit sig_en = State::S1; + }; + + void sequence_cond(sequence_t &seq, SigBit cond) + { + seq.sig_a = module->And(NEW_ID, seq.sig_a, cond); + } + + 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); + + Wire *sig_a_q = module->addWire(NEW_ID); + sig_a_q->attributes["\\init"] = Const(0, 1); + + Wire *sig_en_q = module->addWire(NEW_ID); + sig_en_q->attributes["\\init"] = Const(0, 1); + + 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); + + seq.length++; + seq.sig_a = sig_a_q; + seq.sig_en = sig_en_q; + } + + void parse_sequence(sequence_t &seq, Net *n) + { + Instance *inst = net_to_ast_driver(n); + + // Regular expression + + if (inst == nullptr) { + sequence_cond(seq, importer->net_map_at(n)); + return; + } + + // SVA Primitives + + 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_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_SVA_SEQ_CONCAT) + { + int sva_low = atoi(inst->GetAttValue("sva:low")); + int sva_high = atoi(inst->GetAttValue("sva:low")); + + if (sva_low != sva_high) + log_error("Ranges on SVA sequence concatenation operator are not supported at the moment.\n"); + + parse_sequence(seq, inst->GetInput1()); + + for (int i = 0; i < sva_low; i++) + sequence_ff(seq); + + parse_sequence(seq, inst->GetInput2()); + return; + } + + if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT) + { + int sva_low = atoi(inst->GetAttValue("sva:low")); + int sva_high = atoi(inst->GetAttValue("sva:low")); + + if (sva_low != sva_high) + log_error("Ranges on SVA consecutive repeat operator are not supported at the moment.\n"); + + parse_sequence(seq, inst->GetInput()); + + for (int i = 1; i < sva_low; i++) { + sequence_ff(seq); + parse_sequence(seq, inst->GetInput()); + } + 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()); + } + + void import() + { + module = importer->module; + netlist = root->Owner(); + + RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); + + // parse SVA property clock event + + Instance *at_node = get_ast_input(root); + + // 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); + } + + importer->import_attributes(c->attributes, root); + return; + } + + log_assert(at_node && at_node->Type() == PRIM_SVA_AT); + + VerificClockEdge clock_edge(importer, get_ast_input1(at_node)); + clock = clock_edge.clock_sig; + clock_posedge = clock_edge.posedge; + + // parse disable_iff expression + + Net *sequence_net = at_node->GetInput2(); + + while (1) + { + Instance *sequence_node = net_to_ast_driver(sequence_net); + + if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) { + eventually = true; + sequence_net = sequence_node->GetInput(); + 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(); + continue; + } + + break; + } + + // parse SVA sequence into trigger signal + + sequence_t seq; + parse_sequence(seq, sequence_net); + sequence_ff(seq); + + // generate assert/assume/cover cell + + RTLIL::Cell *c = nullptr; + + 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); + } + + importer->import_attributes(c->attributes, root); + } +}; + +void svapp_assert(Instance *inst) +{ + VerificSvaImporter worker; + worker.root = inst; + worker.mode_assert = true; + worker.rewrite(); +} + +void svapp_assume(Instance *inst) +{ + VerificSvaImporter worker; + worker.root = inst; + worker.mode_assume = true; + worker.rewrite(); +} + +void svapp_cover(Instance *inst) +{ + VerificSvaImporter worker; + worker.root = inst; + worker.mode_cover = true; + worker.rewrite(); +} + +void import_sva_assert(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_assert = true; + worker.import(); +} + +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) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_cover = true; + worker.import(); +} + +YOSYS_NAMESPACE_END -- 2.30.2