diff options
Diffstat (limited to 'frontends/verific')
| -rw-r--r-- | frontends/verific/Makefile.inc | 3 | ||||
| -rw-r--r-- | frontends/verific/README | 35 | ||||
| -rw-r--r-- | frontends/verific/verific.cc | 3356 | ||||
| -rw-r--r-- | frontends/verific/verific.h | 109 | ||||
| -rw-r--r-- | frontends/verific/verificsva.cc | 1860 |
5 files changed, 3886 insertions, 1477 deletions
diff --git a/frontends/verific/Makefile.inc b/frontends/verific/Makefile.inc index 68ef9aed1..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: @@ -11,6 +13,7 @@ share/verific: $(Q) cp -r $(VERIFIC_DIR)/vhdl_packages/vdbs_1987/. share/verific.new/vhdl_vdbs_1987 $(Q) cp -r $(VERIFIC_DIR)/vhdl_packages/vdbs_1993/. share/verific.new/vhdl_vdbs_1993 $(Q) cp -r $(VERIFIC_DIR)/vhdl_packages/vdbs_2008/. share/verific.new/vhdl_vdbs_2008 + $(Q) chmod -R a+rX share/verific.new $(Q) mv share/verific.new share/verific endif diff --git a/frontends/verific/README b/frontends/verific/README index b4c436a3a..c37d76343 100644 --- a/frontends/verific/README +++ b/frontends/verific/README @@ -1,36 +1,11 @@ - This directory contains Verific bindings for Yosys. -See http://www.verific.com/ for details. - - -Building Yosys with the 32 bit Verific eval library on amd64: -============================================================= - -1.) Use a Makefile.conf like the following one: - ---snip-- -CONFIG := gcc -ENABLE_TCL := 0 -ENABLE_PLUGINS := 0 -ENABLE_VERIFIC := 1 -CXXFLAGS += -m32 -LDFLAGS += -m32 -VERIFIC_DIR = /usr/local/src/verific_lib_eval ---snap-- - - -2.) Install the necessary multilib packages - -Hint: On debian/ubuntu the multilib packages have names such as -libreadline-dev:i386 or lib32readline6-dev, depending on the -exact version of debian/ubuntu you are working with. - -3.) Build and test +Use Symbiotic EDA Suite if you need Yosys+Verifc. +https://www.symbioticeda.com/seda-suite -make -j8 -./yosys -p 'verific -sv frontends/verific/example.sv; verific -import top' +Contact office@symbioticeda.com for free evaluation +binaries of Symbiotic EDA Suite. Verific Features that should be enabled in your Verific library @@ -50,7 +25,7 @@ Then run in the following command in this directory: sby -f example.sby -This will generate approximately one page of text outpout. The last lines +This will generate approximately one page of text output. The last lines should be something like this: SBY [example] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 77594b8cf..9274cf5ca 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -19,6 +19,7 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" +#include "kernel/celltypes.h" #include "kernel/log.h" #include <stdlib.h> #include <stdio.h> @@ -29,6 +30,8 @@ # include <dirent.h> #endif +#include "frontends/verific/verific.h" + USING_YOSYS_NAMESPACE #ifdef YOSYS_ENABLE_VERIFIC @@ -40,27 +43,39 @@ USING_YOSYS_NAMESPACE #include "veri_file.h" #include "vhdl_file.h" +#include "hier_tree.h" #include "VeriModule.h" #include "VeriWrite.h" #include "VhdlUnits.h" -#include "DataBase.h" -#include "Message.h" +#include "VeriLibrary.h" + +#ifndef SYMBIOTIC_VERIFIC_API_VERSION +# error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific." +#endif + +#if SYMBIOTIC_VERIFIC_API_VERSION < 1 +# error "Please update your version of Symbiotic EDA flavored Verific." +#endif #ifdef __clang__ #pragma clang diagnostic pop #endif #ifdef VERIFIC_NAMESPACE -using namespace Verific ; +using namespace Verific; #endif #endif -PRIVATE_NAMESPACE_BEGIN - #ifdef YOSYS_ENABLE_VERIFIC +YOSYS_NAMESPACE_BEGIN +int verific_verbose; +bool verific_import_pending; string verific_error_msg; +int verific_sva_fsm_limit; + +vector<string> verific_incdirs, verific_libdirs; void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args) { @@ -95,993 +110,1101 @@ 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(VerificImporter *importer, Instance *inst); -void svapp_assume(VerificImporter *importer, Instance *inst); -void svapp_cover(VerificImporter *importer, Instance *inst); - -struct VerificClockEdge { - Net *clock_net; - SigBit clock_sig; - bool posedge; - VerificClockEdge(VerificImporter *importer, Instance *inst); -}; +// ================================================================== + +VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) : + mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), + mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover), + mode_fullinit(mode_fullinit) +{ +} -struct VerificImporter +RTLIL::SigBit VerificImporter::net_map_at(Net *net) { - RTLIL::Module *module; - Netlist *netlist; + 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()); - std::map<Net*, RTLIL::SigBit> net_map; - std::map<Net*, Net*> sva_posedge_map; + return net_map.at(net); +} - bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose; +bool is_blackbox(Netlist *nl) +{ + if (nl->IsBlackBox() || nl->IsEmptyBox()) + return true; - pool<int> verific_sva_prims; - pool<int> verific_psl_prims; + const char *attr = nl->GetAttValue("blackbox"); + if (attr != nullptr && strcmp(attr, "0")) + return true; - 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) - { - // Copy&paste from Verific 3.16_484_32_170630 Netlist.h - vector<int> sva_prims { - PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME, - PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH, - PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT, - PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT, - PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND, - PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION, - PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY, - PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT, - PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED, - PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST, - PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF, - PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK, - PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS, - PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL, - PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF, - PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON, - PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF, - PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME, - PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE - }; - - for (int p : sva_prims) - verific_sva_prims.insert(p); - - // Copy&paste from Verific 3.16_484_32_170630 Netlist.h - vector<int> psl_prims { - OPER_PSLPREV, OPER_PSLNEXTFUNC, PRIM_PSL_ASSERT, PRIM_PSL_ASSUME, - PRIM_PSL_ASSUME_GUARANTEE, PRIM_PSL_RESTRICT, PRIM_PSL_RESTRICT_GUARANTEE, - PRIM_PSL_COVER, PRIM_ENDPOINT, PRIM_ROSE, PRIM_FELL, PRIM_AT, PRIM_ATSTRONG, - PRIM_ABORT, PRIM_PSL_NOT, PRIM_PSL_AND, PRIM_PSL_OR, PRIM_IMPL, PRIM_EQUIV, - PRIM_PSL_X, PRIM_PSL_XSTRONG, PRIM_PSL_G, PRIM_PSL_F, PRIM_PSL_U, PRIM_PSL_W, - PRIM_NEXT, PRIM_NEXTSTRONG, PRIM_ALWAYS, PRIM_NEVER, PRIM_EVENTUALLY, - PRIM_UNTIL, PRIM_UNTIL_, PRIM_UNTILSTRONG, PRIM_UNTILSTRONG_, PRIM_BEFORE, - PRIM_BEFORE_, PRIM_BEFORESTRONG, PRIM_BEFORESTRONG_, PRIM_NEXT_A, - PRIM_NEXT_ASTRONG, PRIM_NEXT_E, PRIM_NEXT_ESTRONG, PRIM_NEXT_EVENT, - PRIM_NEXT_EVENTSTRONG, PRIM_NEXT_EVENT_A, PRIM_NEXT_EVENT_ASTRONG, - PRIM_NEXT_EVENT_E, PRIM_NEXT_EVENT_ESTRONG, PRIM_SEQ_IMPL, PRIM_OSUFFIX_IMPL, - PRIM_SUFFIX_IMPL, PRIM_OSUFFIX_IMPLSTRONG, PRIM_SUFFIX_IMPLSTRONG, PRIM_WITHIN, - PRIM_WITHIN_, PRIM_WITHINSTRONG, PRIM_WITHINSTRONG_, PRIM_WHILENOT, - PRIM_WHILENOT_, PRIM_WHILENOTSTRONG, PRIM_WHILENOTSTRONG_, PRIM_CONCAT, - PRIM_FUSION, PRIM_SEQ_AND_LEN, PRIM_SEQ_AND, PRIM_SEQ_OR, PRIM_CONS_REP, - PRIM_NONCONS_REP, PRIM_GOTO_REP - }; - - for (int p : psl_prims) - verific_psl_prims.insert(p); - } - - 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()); + return false; +} - return net_map.at(net); - } +RTLIL::IdString VerificImporter::new_verific_id(Verific::DesignObj *obj) +{ + std::string s = stringf("$verific$%s", obj->Name()); + if (obj->Linefile()) + s += stringf("$%s:%d", Verific::LineFile::GetFileName(obj->Linefile()), Verific::LineFile::GetLineNo(obj->Linefile())); + s += stringf("$%d", autoidx++); + return s; +} - void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj) - { - MapIter mi; - Att *attr; +void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj) +{ + MapIter mi; + Att *attr; - if (obj->Linefile()) - attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile())); + if (obj->Linefile()) + attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile())); - // FIXME: Parse numeric attributes - FOREACH_ATTRIBUTE(obj, mi, attr) - attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value())); + // FIXME: Parse numeric attributes + FOREACH_ATTRIBUTE(obj, mi, attr) { + if (attr->Key()[0] == ' ' || attr->Value() == nullptr) + continue; + attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value())); } +} - RTLIL::SigSpec operatorInput(Instance *inst) - { +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; +} + +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; +} + +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 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, const pool<Net*, hash_ptr_ops> *any_all_nets) +{ + RTLIL::SigSpec sig; + RTLIL::Wire *dummy_wire = NULL; + for (int i = int(inst->OutputSize())-1; i >= 0; i--) + if (inst->GetOutputBit(i) && (!any_all_nets || !any_all_nets->count(inst->GetOutputBit(i)))) { + sig.append(net_map_at(inst->GetOutputBit(i))); + dummy_wire = NULL; + } else { + if (dummy_wire == NULL) + dummy_wire = module->addWire(new_verific_id(inst)); else - sig.append(RTLIL::State::Sz); - return sig; + dummy_wire->width++; + sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1)); + } + 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 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; + if (inst->Type() == PRIM_NAND) { + RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst)); + module->addAndGate(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp); + module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput())); + return true; } - 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_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_verific_id(inst)); + module->addOrGate(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp); + module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput())); + return true; } - RTLIL::SigSpec operatorOutput(Instance *inst) + 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) { + auto outnet = inst->GetOutput(); + if (!any_all_nets.count(outnet)) + module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet)); + 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_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_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_FADD) { - 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; + 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_verific_id(inst)); + RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(new_verific_id(inst)); + RTLIL::SigSpec tmp1 = module->addWire(new_verific_id(inst)); + RTLIL::SigSpec tmp2 = module->addWire(new_verific_id(inst)); + RTLIL::SigSpec tmp3 = module->addWire(new_verific_id(inst)); + module->addXorGate(new_verific_id(inst), a, b, tmp1); + module->addXorGate(inst_name, tmp1, c, y); + module->addAndGate(new_verific_id(inst), tmp1, c, tmp2); + module->addAndGate(new_verific_id(inst), a, b, tmp3); + module->addOrGate(new_verific_id(inst), tmp2, tmp3, x); + return true; } - bool import_netlist_instance_gates(Instance *inst, RTLIL::IdString inst_name) + if (inst->Type() == PRIM_DFFRS) { - 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; - } + VerificClocking clocking(this, inst->GetClock()); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); + + if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) + clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + else if (inst->GetSet()->IsGnd()) + clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S0); + else if (inst->GetReset()->IsGnd()) + clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S1); + else + clocking.addDffsr(inst_name, 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_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; - } + return false; +} - 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 VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name) +{ + RTLIL::Cell *cell = nullptr; - 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_AND) { + cell = module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_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_NAND) { + RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst)); + cell = module->addAnd(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp); + import_attributes(cell->attributes, inst); + cell = module->addNot(inst_name, tmp, net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_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_OR) { + cell = module->addOr(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_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_verific_id(inst)); + cell = module->addOr(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp); + import_attributes(cell->attributes, inst); + cell = module->addNot(inst_name, tmp, net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_INV) { - module->addNotGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); - return true; - } + if (inst->Type() == PRIM_XOR) { + cell = module->addXor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_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) { + cell = module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_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_INV) { + cell = module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_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_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) { + cell = module->addMux(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - return false; + if (inst->Type() == PRIM_TRI) { + cell = module->addMux(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; } - 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; - } + RTLIL::SigSpec a_plus_b = module->addWire(new_verific_id(inst), 2); + RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(new_verific_id(inst)); + if (inst->GetCout()) + y.append(net_map_at(inst->GetCout())); + cell = module->addAdd(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), a_plus_b); + import_attributes(cell->attributes, inst); + cell = module->addAdd(inst_name, a_plus_b, net_map_at(inst->GetCin()), y); + import_attributes(cell->attributes, inst); + return true; + } - 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_DFFRS) + { + VerificClocking clocking(this, inst->GetClock()); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); + + if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) + cell = clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + else if (inst->GetSet()->IsGnd()) + cell = clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0); + else if (inst->GetReset()->IsGnd()) + cell = clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1); + else + cell = clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), + net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_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_DLATCHRS) + { + if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) + cell = module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + else + cell = module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), + net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - 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; + #define IN operatorInput(inst) + #define IN1 operatorInput1(inst) + #define IN2 operatorInput2(inst) + #define OUT operatorOutput(inst) + #define FILTERED_OUT operatorOutput(inst, &any_all_nets) + #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()) { + cell = module->addAdd(inst_name, IN1, IN2, out, SIGNED); + import_attributes(cell->attributes, inst); + } else { + RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst), GetSize(out)); + cell = module->addAdd(new_verific_id(inst), IN1, IN2, tmp, SIGNED); + import_attributes(cell->attributes, inst); + cell = module->addAdd(inst_name, tmp, net_map_at(inst->GetCin()), out, false); + import_attributes(cell->attributes, inst); } + return true; + } - if (inst->Type() == 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() == OPER_MULTIPLIER) { + cell = module->addMul(inst_name, IN1, IN2, OUT, SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_XNOR) { - module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); - return true; - } + if (inst->Type() == OPER_DIVIDER) { + cell = module->addDiv(inst_name, IN1, IN2, OUT, SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_INV) { - module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); - return true; - } + if (inst->Type() == OPER_MODULO) { + cell = module->addMod(inst_name, IN1, IN2, OUT, SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_MUX) { - module->addMux(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput())); - return true; - } + if (inst->Type() == OPER_REMAINDER) { + cell = module->addMod(inst_name, IN1, IN2, OUT, SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_TRI) { - module->addMux(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput())); - return true; - } + if (inst->Type() == OPER_SHIFT_LEFT) { + cell = module->addShl(inst_name, IN1, IN2, OUT, false); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_FADD) - { - RTLIL::SigSpec a_plus_b = module->addWire(NEW_ID, 2); - RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(NEW_ID); - 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() == 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); } + cell = module->addShl(inst_name, vec, IN, OUT, false); + import_attributes(cell->attributes, inst); + 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() == OPER_DECODER) { + RTLIL::SigSpec vec; + vec.append(RTLIL::State::S1); + for (unsigned i = 1; i < inst->OutputSize(); i++) { + vec.append(RTLIL::State::S0); } + cell = module->addShl(inst_name, vec, IN, OUT, false); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == PRIM_DLATCHRS) - { - if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) - module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); - 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_SHIFT_RIGHT) { + Net *net_cin = inst->GetCin(); + Net *net_a_msb = inst->GetInput1Bit(0); + if (net_cin->IsGnd()) + cell = module->addShr(inst_name, IN1, IN2, OUT, false); + else if (net_cin == net_a_msb) + cell = module->addSshr(inst_name, IN1, IN2, OUT, true); + else + log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst->Name()); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_MULTIPLIER) { - module->addMul(inst_name, IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_REDUCE_AND) { + cell = module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_DIVIDER) { - module->addDiv(inst_name, IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_REDUCE_OR) { + cell = module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_MODULO) { - module->addMod(inst_name, IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_REDUCE_XOR) { + cell = module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_REMAINDER) { - module->addMod(inst_name, IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_REDUCE_XNOR) { + cell = module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_SHIFT_LEFT) { - module->addShl(inst_name, IN1, IN2, OUT, false); - return true; - } + if (inst->Type() == OPER_REDUCE_NOR) { + SigSpec t = module->ReduceOr(new_verific_id(inst), IN, SIGNED); + cell = module->addNot(inst_name, t, net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_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_LESSTHAN) { + Net *net_cin = inst->GetCin(); + if (net_cin->IsGnd()) + cell = module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); + else if (net_cin->IsPwr()) + cell = module->addLe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); + else + log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name()); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_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_WIDE_AND) { + cell = module->addAnd(inst_name, IN1, IN2, OUT, SIGNED); + import_attributes(cell->attributes, inst); + 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_WIDE_OR) { + cell = module->addOr(inst_name, IN1, IN2, OUT, SIGNED); + import_attributes(cell->attributes, inst); + 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_WIDE_XOR) { + cell = module->addXor(inst_name, IN1, IN2, OUT, SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_REDUCE_OR) { - module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED); - return true; - } + if (inst->Type() == OPER_WIDE_XNOR) { + cell = module->addXnor(inst_name, IN1, IN2, OUT, SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_REDUCE_XOR) { - module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED); - return true; - } + if (inst->Type() == OPER_WIDE_BUF) { + cell = module->addPos(inst_name, IN, FILTERED_OUT, SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_REDUCE_XNOR) { - module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED); - return true; - } + if (inst->Type() == OPER_WIDE_INV) { + cell = module->addNot(inst_name, IN, OUT, SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_LESSTHAN) { - Net *net_cin = inst->GetCin(); - if (net_cin->IsGnd()) - module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); - 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_MINUS) { + cell = module->addSub(inst_name, IN1, IN2, OUT, SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_WIDE_AND) { - module->addAnd(inst_name, IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_UMINUS) { + cell = module->addNeg(inst_name, IN, OUT, SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_WIDE_OR) { - module->addOr(inst_name, IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_EQUAL) { + cell = module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_WIDE_XOR) { - module->addXor(inst_name, IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_NEQUAL) { + cell = module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_WIDE_XNOR) { - module->addXnor(inst_name, IN1, IN2, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_WIDE_MUX) { + cell = module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_WIDE_BUF) { - module->addPos(inst_name, IN, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_NTO1MUX) { + cell = module->addShr(inst_name, IN2, IN1, net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_WIDE_INV) { - module->addNot(inst_name, IN, OUT, SIGNED); - return true; - } + if (inst->Type() == OPER_WIDE_NTO1MUX) + { + SigSpec data = IN2, out = OUT; - if (inst->Type() == OPER_MINUS) { - module->addSub(inst_name, IN1, IN2, OUT, SIGNED); - return true; - } + int wordsize_bits = ceil_log2(GetSize(out)); + int wordsize = 1 << wordsize_bits; - if (inst->Type() == OPER_UMINUS) { - module->addNeg(inst_name, IN, OUT, SIGNED); - return true; - } + SigSpec sel = {IN1, SigSpec(State::S0, wordsize_bits)}; - if (inst->Type() == OPER_EQUAL) { - module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); - return true; + SigSpec padded_data; + for (int i = 0; i < GetSize(data); i += GetSize(out)) { + SigSpec d = data.extract(i, GetSize(out)); + d.extend_u0(wordsize); + padded_data.append(d); } - if (inst->Type() == OPER_NEQUAL) { - module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); - return true; - } + cell = module->addShr(inst_name, padded_data, sel, out); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_WIDE_MUX) { - module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT); - return true; - } + if (inst->Type() == OPER_SELECTOR) + { + cell = module->addPmux(inst_name, State::S0, IN2, IN1, net_map_at(inst->GetOutput())); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_WIDE_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_SELECTOR) + { + SigSpec out = OUT; + cell = module->addPmux(inst_name, SigSpec(State::S0, GetSize(out)), IN2, IN1, out); + import_attributes(cell->attributes, inst); + return true; + } - if (inst->Type() == OPER_WIDE_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 (inst->Type() == OPER_WIDE_TRI) { + cell = module->addMux(inst_name, RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT); + import_attributes(cell->attributes, inst); + return true; + } + + if (inst->Type() == OPER_WIDE_DFFRS) + { + VerificClocking clocking(this, inst->GetClock()); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); - #undef IN - #undef IN1 - #undef IN2 - #undef OUT - #undef SIGNED + RTLIL::SigSpec sig_set = operatorInport(inst, "set"); + RTLIL::SigSpec sig_reset = operatorInport(inst, "reset"); - return false; + if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool()) + cell = clocking.addDff(inst_name, IN, OUT); + else + cell = clocking.addDffsr(inst_name, sig_set, sig_reset, IN, OUT); + import_attributes(cell->attributes, inst); + + return true; } - void merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol) - { - bool keep_running = true; - SigMap sigmap; + #undef IN + #undef IN1 + #undef IN2 + #undef OUT + #undef SIGNED - while (keep_running) - { - keep_running = false; + return false; +} - dict<SigBit, pool<RTLIL::Cell*>> dbits_db; - SigSpec dbits; +void VerificImporter::merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol) +{ + bool keep_running = true; + SigMap sigmap; - for (auto cell : candidates) { - SigBit bit = sigmap(cell->getPort("\\D")); - dbits_db[bit].insert(cell); - dbits.append(bit); - } + while (keep_running) + { + keep_running = false; - dbits.sort_and_unify(); + dict<SigBit, pool<RTLIL::Cell*>> dbits_db; + SigSpec dbits; - for (auto chunk : dbits.chunks()) - { - SigSpec sig_d = chunk; + for (auto cell : candidates) { + SigBit bit = sigmap(cell->getPort("\\D")); + dbits_db[bit].insert(cell); + dbits.append(bit); + } - if (chunk.wire == nullptr || GetSize(sig_d) == 1) - continue; + dbits.sort_and_unify(); - 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); + for (auto chunk : dbits.chunks()) + { + SigSpec sig_d = chunk; - if (verbose) - log(" merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff)); + if (chunk.wire == nullptr || GetSize(sig_d) == 1) + continue; - 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_q = module->addWire(NEW_ID, GetSize(sig_d)); + RTLIL::Cell *new_ff = module->addDff(NEW_ID, clock, sig_d, sig_q, clock_pol); - SigBit old_q = old_ff->getPort("\\Q"); - SigBit new_q = sig_q[i]; + if (verific_verbose) + log(" merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff)); - sigmap.add(old_q, new_q); - module->connect(old_q, new_q); - candidates.erase(old_ff); - module->remove(old_ff); - keep_running = true; - } - } + for (int i = 0; i < GetSize(sig_d); i++) + for (auto old_ff : dbits_db[sig_d[i]]) + { + if (verific_verbose) + log(" replacing old ff %s on bit %d.\n", log_id(old_ff), i); + + SigBit old_q = old_ff->getPort("\\Q"); + SigBit new_q = sig_q[i]; + + sigmap.add(old_q, new_q); + module->connect(old_q, new_q); + candidates.erase(old_ff); + module->remove(old_ff); + keep_running = true; + } } } +} - void merge_past_ffs(pool<RTLIL::Cell*> &candidates) +void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates) +{ + dict<pair<SigBit, int>, pool<RTLIL::Cell*>> database; + + for (auto cell : candidates) { - dict<pair<SigBit, int>, pool<RTLIL::Cell*>> database; + 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 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); +} - for (auto it : database) - merge_past_ffs_clock(it.second, it.first.first, it.first.second); +void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool norename) +{ + std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name(); + std::string module_name = netlist_name; + + if (nl->IsOperator() || nl->IsPrimitive()) { + module_name = "$verific$" + module_name; + } else { + if (!norename && *nl->Name()) { + module_name += "("; + module_name += nl->Name(); + module_name += ")"; + } + module_name = "\\" + module_name; } - void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo) - { - std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name()); + netlist = nl; - netlist = nl; + if (design->has(module_name)) { + if (!nl->IsOperator() && !is_blackbox(nl)) + log_cmd_error("Re-definition of module `%s'.\n", netlist_name.c_str()); + return; + } - if (design->has(module_name)) { - if (!nl->IsOperator()) - log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name()); - return; - } + module = new RTLIL::Module; + module->name = module_name; + design->add(module); - module = new RTLIL::Module; - module->name = module_name; - design->add(module); + if (is_blackbox(nl)) { + 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 (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)); - } + SetIter si; + MapIter mi, mi2; + Port *port; + PortBus *portbus; + Net *net; + NetBus *netbus; + Instance *inst; + PortRef *pr; - SetIter si; - MapIter mi, mi2; - Port *port; - PortBus *portbus; - Net *net; - NetBus *netbus; - Instance *inst; - PortRef *pr; + FOREACH_PORT_OF_NETLIST(nl, mi, port) + { + if (port->Bus()) + continue; - FOREACH_PORT_OF_NETLIST(nl, mi, port) - { - if (port->Bus()) - continue; + if (verific_verbose) + log(" importing port %s.\n", port->Name()); - if (verbose) - log(" importing port %s.\n", port->Name()); + RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name())); + import_attributes(wire->attributes, port); - RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name())); - import_attributes(wire->attributes, port); + wire->port_id = nl->IndexOf(port) + 1; - wire->port_id = nl->IndexOf(port) + 1; + 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 (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 (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 (port->GetNet()) { - net = port->GetNet(); + FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus) + { + if (verific_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] = wire; + net_map[net] = bit; else if (wire->port_input) - module->connect(net_map_at(net), wire); + module->connect(net_map_at(net), bit); else - module->connect(wire, net_map_at(net)); - } - } - - 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->connect(bit, net_map_at(net)); } + if (i == portbus->RightIndex()) + break; } + } - module->fixup_ports(); + module->fixup_ports(); - dict<Net*, char, hash_ptr_ops> init_nets; - pool<Net*, hash_ptr_ops> anyconst_nets; - pool<Net*, hash_ptr_ops> anyseq_nets; + dict<Net*, char, hash_ptr_ops> init_nets; + pool<Net*, hash_ptr_ops> anyconst_nets, anyseq_nets; + pool<Net*, hash_ptr_ops> allconst_nets, allseq_nets; + any_all_nets.clear(); - FOREACH_NET_OF_NETLIST(nl, mi, net) + FOREACH_NET_OF_NETLIST(nl, mi, net) + { + if (net->IsRamNet()) { - if (net->IsRamNet()) - { - RTLIL::Memory *memory = new RTLIL::Memory; - memory->name = RTLIL::escape_id(net->Name()); - log_assert(module->count_id(memory->name) == 0); - module->memories[memory->name] = memory; - - int number_of_bits = net->Size(); - int bits_in_word = number_of_bits; - FOREACH_PORTREF_OF_NET(net, si, pr) { - if (pr->GetInst()->Type() == OPER_READ_PORT) { - bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize()); - continue; - } - if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) { - bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size()); - continue; - } - log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n", - net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name()); + RTLIL::Memory *memory = new RTLIL::Memory; + memory->name = RTLIL::escape_id(net->Name()); + log_assert(module->count_id(memory->name) == 0); + module->memories[memory->name] = memory; + + int number_of_bits = net->Size(); + int bits_in_word = number_of_bits; + FOREACH_PORTREF_OF_NET(net, si, pr) { + if (pr->GetInst()->Type() == OPER_READ_PORT) { + bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize()); + continue; } + if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) { + bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size()); + continue; + } + log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n", + net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name()); + } - memory->width = bits_in_word; - memory->size = number_of_bits / bits_in_word; - - const char *ascii_initdata = net->GetWideInitialValue(); - if (ascii_initdata) { - while (*ascii_initdata != 0 && *ascii_initdata != '\'') - ascii_initdata++; - if (*ascii_initdata == '\'') - ascii_initdata++; - if (*ascii_initdata != 0) { - log_assert(*ascii_initdata == 'b'); + 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++; } - 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); - } + if (initval_valid) { + RTLIL::Cell *cell = module->addCell(new_verific_id(net), "$meminit"); + cell->parameters["\\WORDS"] = 1; + if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound()) + cell->setPort("\\ADDR", word_idx); + 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; } + continue; + } - if (net->GetInitialValue()) - init_nets[net] = net->GetInitialValue(); + if (net->GetInitialValue()) + init_nets[net] = net->GetInitialValue(); - const char *rand_const_attr = net->GetAttValue(" rand_const"); - const char *rand_attr = net->GetAttValue(" rand"); + 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); + const char *anyconst_attr = net->GetAttValue("anyconst"); + const char *anyseq_attr = net->GetAttValue("anyseq"); - else if (rand_attr != nullptr && !strcmp(rand_attr, "1")) - anyseq_nets.insert(net); + const char *allconst_attr = net->GetAttValue("allconst"); + const char *allseq_attr = net->GetAttValue("allseq"); - if (net_map.count(net)) { - if (verbose) - log(" skipping net %s.\n", net->Name()); - continue; - } + if (rand_const_attr != nullptr && (!strcmp(rand_const_attr, "1") || !strcmp(rand_const_attr, "'1'"))) { + anyconst_nets.insert(net); + any_all_nets.insert(net); + } + else if (rand_attr != nullptr && (!strcmp(rand_attr, "1") || !strcmp(rand_attr, "'1'"))) { + anyseq_nets.insert(net); + any_all_nets.insert(net); + } + else if (anyconst_attr != nullptr && (!strcmp(anyconst_attr, "1") || !strcmp(anyconst_attr, "'1'"))) { + anyconst_nets.insert(net); + any_all_nets.insert(net); + } + else if (anyseq_attr != nullptr && (!strcmp(anyseq_attr, "1") || !strcmp(anyseq_attr, "'1'"))) { + anyseq_nets.insert(net); + any_all_nets.insert(net); + } + else if (allconst_attr != nullptr && (!strcmp(allconst_attr, "1") || !strcmp(allconst_attr, "'1'"))) { + allconst_nets.insert(net); + any_all_nets.insert(net); + } + else if (allseq_attr != nullptr && (!strcmp(allseq_attr, "1") || !strcmp(allseq_attr, "'1'"))) { + allseq_nets.insert(net); + any_all_nets.insert(net); + } - if (net->Bus()) - continue; + if (net_map.count(net)) { + if (verific_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); + RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : new_verific_id(net)); - if (verbose) - log(" importing net %s as %s.\n", net->Name(), log_id(wire_name)); + if (verific_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); + RTLIL::Wire *wire = module->addWire(wire_name); + import_attributes(wire->attributes, net); - net_map[net] = wire; + net_map[net] = wire; + } + + 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; } - FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus) + if (found_new_net) { - 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); + RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : new_verific_id(netbus)); - if (verbose) - log(" importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name)); + if (verific_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::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; + RTLIL::Const initval = Const(State::Sx, GetSize(wire)); + bool initval_valid = false; - for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) + for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) + { + if (netbus->ElementAtIndex(i)) { - 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)); + 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 (i == netbus->RightIndex()) - break; + if (net_map.count(net) == 0) + net_map[net] = bit; + else + module->connect(bit, net_map_at(net)); } - if (initval_valid) - wire->attributes["\\init"] = initval; - } - else - { - if (verbose) - log(" skipping netbus %s.\n", netbus->Name()); + if (i == netbus->RightIndex()) + break; } - SigSpec anyconst_sig; - SigSpec anyseq_sig; + if (initval_valid) + wire->attributes["\\init"] = initval; + } + else + { + if (verific_verbose) + log(" skipping netbus %s.\n", netbus->Name()); + } - 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; + SigSpec anyconst_sig; + SigSpec anyseq_sig; + SigSpec allconst_sig; + SigSpec allseq_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 (net != nullptr && allconst_nets.count(net)) { + allconst_sig.append(net_map_at(net)); + allconst_nets.erase(net); + } + if (net != nullptr && allseq_nets.count(net)) { + allseq_sig.append(net_map_at(net)); + allseq_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(anyconst_sig)) + module->connect(anyconst_sig, module->Anyconst(new_verific_id(netbus), GetSize(anyconst_sig))); - if (GetSize(anyseq_sig)) - module->connect(anyseq_sig, module->Anyseq(NEW_ID, GetSize(anyseq_sig))); - } + if (GetSize(anyseq_sig)) + module->connect(anyseq_sig, module->Anyseq(new_verific_id(netbus), GetSize(anyseq_sig))); - for (auto it : init_nets) - { - Const initval; - SigBit bit = net_map_at(it.first); - log_assert(bit.wire); + if (GetSize(allconst_sig)) + module->connect(allconst_sig, module->Allconst(new_verific_id(netbus), GetSize(allconst_sig))); - if (bit.wire->attributes.count("\\init")) - initval = bit.wire->attributes.at("\\init"); + if (GetSize(allseq_sig)) + module->connect(allseq_sig, module->Allseq(new_verific_id(netbus), GetSize(allseq_sig))); + } - while (GetSize(initval) < GetSize(bit.wire)) - initval.bits.push_back(State::Sx); + for (auto it : init_nets) + { + Const initval; + SigBit bit = net_map_at(it.first); + log_assert(bit.wire); - if (it.second == '0') - initval.bits.at(bit.offset) = State::S0; - if (it.second == '1') - initval.bits.at(bit.offset) = State::S1; + if (bit.wire->attributes.count("\\init")) + initval = bit.wire->attributes.at("\\init"); - bit.wire->attributes["\\init"] = initval; - } + while (GetSize(initval) < GetSize(bit.wire)) + initval.bits.push_back(State::Sx); - for (auto net : anyconst_nets) - module->connect(net_map_at(net), module->Anyconst(NEW_ID)); + if (it.second == '0') + initval.bits.at(bit.offset) = State::S0; + if (it.second == '1') + initval.bits.at(bit.offset) = State::S1; - for (auto net : anyseq_nets) - module->connect(net_map_at(net), module->Anyseq(NEW_ID)); + bit.wire->attributes["\\init"] = initval; + } - pool<Instance*, hash_ptr_ops> sva_asserts; - pool<Instance*, hash_ptr_ops> sva_assumes; - pool<Instance*, hash_ptr_ops> sva_covers; + for (auto net : anyconst_nets) + module->connect(net_map_at(net), module->Anyconst(new_verific_id(net))); - pool<RTLIL::Cell*> past_ffs; + for (auto net : anyseq_nets) + module->connect(net_map_at(net), module->Anyseq(new_verific_id(net))); - FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) - { - RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID); + pool<Instance*, hash_ptr_ops> sva_asserts; + pool<Instance*, hash_ptr_ops> sva_assumes; + pool<Instance*, hash_ptr_ops> sva_covers; + pool<Instance*, hash_ptr_ops> sva_triggers; - if (verbose) - log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name)); + pool<RTLIL::Cell*> past_ffs; - if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT) { - Net *in = inst->GetInput(); - module->addAssert(NEW_ID, net_map_at(in), State::S1); - continue; - } + FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) + { + RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : new_verific_id(inst)); - if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) { - Net *in = inst->GetInput(); - module->addAssume(NEW_ID, net_map_at(in), State::S1); - continue; - } + if (verific_verbose) + log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name)); - if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER) { - Net *in = inst->GetInput(); - module->addCover(NEW_ID, net_map_at(in), State::S1); - continue; - } + if (mode_verific) + goto import_verific_cells; - if (inst->Type() == PRIM_PWR) { - module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1); - continue; - } + if (inst->Type() == PRIM_PWR) { + module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1); + continue; + } - if (inst->Type() == PRIM_GND) { - module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S0); - continue; - } + if (inst->Type() == PRIM_GND) { + module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S0); + continue; + } - if (inst->Type() == PRIM_BUF) { - module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); - continue; - } + if (inst->Type() == PRIM_BUF) { + auto outnet = inst->GetOutput(); + if (!any_all_nets.count(outnet)) + module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet)); + continue; + } - if (inst->Type() == PRIM_X) { - module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sx); - continue; - } + 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_Z) { + module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sz); + continue; + } - 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()); + if (inst->Type() == OPER_READ_PORT) + { + RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name())); + int numchunks = int(inst->OutputSize()) / memory->width; + int chunksbits = ceil_log2(numchunks); + + if ((numchunks * memory->width) != int(inst->OutputSize()) || (numchunks & (numchunks - 1)) != 0) + log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name()); - RTLIL::SigSpec addr = operatorInput1(inst); - RTLIL::SigSpec data = operatorOutput(inst); + for (int i = 0; i < numchunks; i++) + { + RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)}; + RTLIL::SigSpec data = operatorOutput(inst).extract(i * memory->width, memory->width); - RTLIL::Cell *cell = module->addCell(inst_name, "$memrd"); + RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name : + RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), "$memrd"); cell->parameters["\\MEMID"] = memory->name.str(); cell->parameters["\\CLK_ENABLE"] = false; cell->parameters["\\CLK_POLARITY"] = true; @@ -1092,19 +1215,26 @@ struct VerificImporter cell->setPort("\\EN", RTLIL::State::Sx); cell->setPort("\\ADDR", addr); cell->setPort("\\DATA", data); - continue; } + continue; + } - 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()); + if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT) + { + RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name())); + int numchunks = int(inst->Input2Size()) / memory->width; + int chunksbits = ceil_log2(numchunks); - RTLIL::SigSpec addr = operatorInput1(inst); - RTLIL::SigSpec data = operatorInput2(inst); + if ((numchunks * memory->width) != int(inst->Input2Size()) || (numchunks & (numchunks - 1)) != 0) + log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetOutput()->Name()); - RTLIL::Cell *cell = module->addCell(inst_name, "$memwr"); + for (int i = 0; i < numchunks; i++) + { + RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)}; + RTLIL::SigSpec data = operatorInput2(inst).extract(i * memory->width, memory->width); + + RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name : + RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), "$memwr"); cell->parameters["\\MEMID"] = memory->name.str(); cell->parameters["\\CLK_ENABLE"] = false; cell->parameters["\\CLK_POLARITY"] = true; @@ -1120,632 +1250,444 @@ struct VerificImporter cell->parameters["\\CLK_ENABLE"] = true; cell->setPort("\\CLK", net_map_at(inst->GetClock())); } - continue; } + continue; + } - if (!mode_gates) { - if (import_netlist_instance_cells(inst, inst_name)) - continue; - if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()) && !verific_psl_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; - } + 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; + } - if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_PSL_ASSERT) - sva_asserts.insert(inst); + if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT) + sva_asserts.insert(inst); - if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_PSL_ASSUME) - sva_assumes.insert(inst); + if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME || inst->Type() == PRIM_SVA_RESTRICT) + sva_assumes.insert(inst); - if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_PSL_COVER) - sva_covers.insert(inst); + if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER) + sva_covers.insert(inst); - if (inst->Type() == PRIM_SVA_PAST && !mode_nosva) - { - VerificClockEdge clock_edge(this, inst->GetInput2()->Driver()); + if (inst->Type() == PRIM_SVA_TRIGGERED) + sva_triggers.insert(inst); - SigBit sig_d = net_map_at(inst->GetInput1()); - SigBit sig_q = net_map_at(inst->GetOutput()); + if (inst->Type() == OPER_SVA_STABLE) + { + VerificClocking clocking(this, inst->GetInput2Bit(0)); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); - 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_assert(inst->Input1Size() == inst->OutputSize()); - past_ffs.insert(module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge)); + SigSpec sig_d, sig_q, sig_o; + sig_q = module->addWire(new_verific_id(inst), inst->Input1Size()); - if (!mode_keep) - continue; + 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))); } - if (inst->Type() == OPER_PSLPREV && !mode_nosva) - { - Net *clock = inst->GetClock(); - - if (!clock->IsConstant()) - { - VerificClockEdge clock_edge(this, clock->Driver()); - - SigSpec sig_d, sig_q; - - for (int i = 0; i < int(inst->InputSize()); i++) { - sig_d.append(net_map_at(inst->GetInputBit(i))); - sig_q.append(net_map_at(inst->GetOutputBit(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)); + if (verific_verbose) { + log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", + log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); + log(" XNOR with A=%s, B=%s, Y=%s.\n", + log_signal(sig_d), log_signal(sig_q), log_signal(sig_o)); + } - RTLIL::Cell *ff = module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge); + clocking.addDff(new_verific_id(inst), sig_d, sig_q); + module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o); - if (inst->InputSize() == 1) - past_ffs.insert(ff); + if (!mode_keep) + continue; + } - if (!mode_keep) - continue; - } + if (inst->Type() == PRIM_SVA_STABLE) + { + VerificClocking clocking(this, inst->GetInput2()); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); + + SigSpec sig_d = net_map_at(inst->GetInput1()); + SigSpec sig_o = net_map_at(inst->GetOutput()); + SigSpec sig_q = module->addWire(new_verific_id(inst)); + + if (verific_verbose) { + log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", + log_signal(sig_d), log_signal(sig_q), log_signal(clocking.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 (!mode_keep && (verific_sva_prims.count(inst->Type()) || verific_psl_prims.count(inst->Type()))) { - if (verbose) - log(" skipping SVA/PSL cell in non k-mode\n"); + clocking.addDff(new_verific_id(inst), sig_d, sig_q); + module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o); + + if (!mode_keep) continue; - } + } - if (inst->IsPrimitive()) - { - if (inst->Type() == PRIM_HDL_ASSERTION) - continue; + if (inst->Type() == PRIM_SVA_PAST) + { + VerificClocking clocking(this, inst->GetInput2()); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); - if (!mode_keep) - log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); + SigBit sig_d = net_map_at(inst->GetInput1()); + SigBit sig_q = net_map_at(inst->GetOutput()); - if (!verific_sva_prims.count(inst->Type()) && !verific_psl_prims.count(inst->Type())) - log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); - } + if (verific_verbose) + log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", + log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); - nl_todo.insert(inst->View()); + past_ffs.insert(clocking.addDff(new_verific_id(inst), sig_d, sig_q)); - RTLIL::Cell *cell = module->addCell(inst_name, inst->IsOperator() ? - std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name())); + if (!mode_keep) + continue; + } - if (inst->IsPrimitive() && mode_keep) - cell->attributes["\\keep"] = 1; + if ((inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL)) + { + VerificClocking clocking(this, inst->GetInput2()); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); - dict<IdString, vector<SigBit>> cell_port_conns; + SigBit sig_d = net_map_at(inst->GetInput1()); + SigBit sig_o = net_map_at(inst->GetOutput()); + SigBit sig_q = module->addWire(new_verific_id(inst)); - if (verbose) - log(" ports in verific db:\n"); + if (verific_verbose) + log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", + log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); - 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()); - } + clocking.addDff(new_verific_id(inst), sig_d, sig_q); + module->addEq(new_verific_id(inst), {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o); - if (verbose) - log(" ports in yosys db:\n"); + if (!mode_keep) + continue; + } - 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); - } + if (!mode_keep && verific_sva_prims.count(inst->Type())) { + if (verific_verbose) + log(" skipping SVA cell in non k-mode\n"); + continue; } - if (!mode_nosvapp) + if (inst->Type() == PRIM_HDL_ASSERTION) { - for (auto inst : sva_asserts) - svapp_assert(this, inst); + SigBit cond = net_map_at(inst->GetInput()); - for (auto inst : sva_assumes) - svapp_assume(this, inst); + if (verific_verbose) + log(" assert condition %s.\n", log_signal(cond)); - for (auto inst : sva_covers) - svapp_cover(this, inst); - } + const char *assume_attr = nullptr; // inst->GetAttValue("assume"); - if (!mode_nosva) - { - for (auto inst : sva_asserts) - import_sva_assert(this, inst); + Cell *cell = nullptr; + if (assume_attr != nullptr && !strcmp(assume_attr, "1")) + cell = module->addAssume(new_verific_id(inst), cond, State::S1); + else + cell = module->addAssert(new_verific_id(inst), cond, State::S1); - for (auto inst : sva_assumes) - import_sva_assume(this, inst); + import_attributes(cell->attributes, inst); + continue; + } - for (auto inst : sva_covers) - import_sva_cover(this, inst); + if (inst->IsPrimitive()) + { + if (!mode_keep) + log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); - merge_past_ffs(past_ffs); + if (!verific_sva_prims.count(inst->Type())) + log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); } - } -}; -Net *verific_follow_inv(Net *w) -{ - if (w == nullptr || w->IsMultipleDriven()) - return nullptr; + import_verific_cells: + nl_todo.insert(inst->View()); - Instance *i = w->Driver(); - if (i == nullptr || i->Type() != PRIM_INV) - return nullptr; + std::string inst_type = inst->View()->Owner()->Name(); - return i->GetInput(); -} + if (inst->View()->IsOperator() || inst->View()->IsPrimitive()) { + inst_type = "$verific$" + inst_type; + } else { + if (*inst->View()->Name()) { + inst_type += "("; + inst_type += inst->View()->Name(); + inst_type += ")"; + } + inst_type = "\\" + inst_type; + } -Net *verific_follow_pslprev(Net *w) -{ - if (w == nullptr || w->IsMultipleDriven()) - return nullptr; + RTLIL::Cell *cell = module->addCell(inst_name, inst_type); - Instance *i = w->Driver(); - if (i == nullptr || i->Type() != OPER_PSLPREV || i->InputSize() != 1) - return nullptr; + if (inst->IsPrimitive() && mode_keep) + cell->attributes["\\keep"] = 1; - return i->GetInputBit(0); -} + dict<IdString, vector<SigBit>> cell_port_conns; -Net *verific_follow_inv_pslprev(Net *w) -{ - w = verific_follow_inv(w); - return verific_follow_pslprev(w); -} + if (verific_verbose) + log(" ports in verific db:\n"); -VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst) -{ - log_assert(importer != nullptr); - log_assert(inst != nullptr); + FOREACH_PORTREF_OF_INST(inst, mi2, pr) { + if (verific_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_verific_id(inst), port_offset+1-GetSize(sigvec)); + for (auto bit : zwires) + sigvec.push_back(bit); + } + sigvec[port_offset] = net_map_at(pr->GetNet()); + } - // SVA posedge/negedge - if (inst->Type() == PRIM_SVA_POSEDGE) - { - clock_net = inst->GetInput(); - posedge = true; + if (verific_verbose) + log(" ports in yosys db:\n"); - Instance *driver = clock_net->Driver(); - if (!clock_net->IsMultipleDriven() && driver && driver->Type() == PRIM_INV) { - clock_net = driver->GetInput(); - posedge = false; + for (auto &it : cell_port_conns) { + if (verific_verbose) + log(" .%s(%s)\n", log_id(it.first), log_signal(it.second)); + cell->setPort(it.first, it.second); } - - clock_sig = importer->net_map_at(clock_net); - return; } - // VHDL-flavored PSL clock - if (inst->Type() == PRIM_AND) + if (!mode_nosva) { - Net *w1 = inst->GetInput1(); - Net *w2 = inst->GetInput2(); - - clock_net = verific_follow_inv_pslprev(w1); - if (clock_net == w2) { - clock_sig = importer->net_map_at(clock_net); - posedge = true; - return; + for (auto inst : sva_asserts) { + if (mode_autocover) + verific_import_sva_cover(this, inst); + verific_import_sva_assert(this, inst); } - clock_net = verific_follow_inv_pslprev(w2); - if (clock_net == w1) { - clock_sig = importer->net_map_at(clock_net); - posedge = true; - return; - } + for (auto inst : sva_assumes) + verific_import_sva_assume(this, inst); - clock_net = verific_follow_pslprev(w1); - if (clock_net == verific_follow_inv(w2)) { - clock_sig = importer->net_map_at(clock_net); - posedge = false; - return; - } + for (auto inst : sva_covers) + verific_import_sva_cover(this, inst); - clock_net = verific_follow_pslprev(w2); - if (clock_net == verific_follow_inv(w1)) { - clock_sig = importer->net_map_at(clock_net); - posedge = false; - return; - } + for (auto inst : sva_triggers) + verific_import_sva_trigger(this, inst); - log_abort(); + merge_past_ffs(past_ffs); } -} - -// ================================================================== - -struct VerificSvaPP -{ - VerificImporter *importer; - Module *module; - Netlist *netlist; - Instance *root; - - bool mode_assert = false; - bool mode_assume = false; - bool mode_cover = false; - - Instance *net_to_ast_driver(Net *n) + if (!mode_fullinit) { - if (n == nullptr) - return nullptr; - - if (n->IsMultipleDriven()) - return nullptr; - - Instance *inst = n->Driver(); - - if (inst == nullptr) - return nullptr; - - if (!importer->verific_sva_prims.count(inst->Type()) && - !importer->verific_psl_prims.count(inst->Type())) - return nullptr; + pool<SigBit> non_ff_bits; + CellTypes ff_types; - if (inst->Type() == PRIM_SVA_PAST) - return nullptr; - - return inst; - } + ff_types.setup_internals_ff(); + ff_types.setup_stdcells_mem(); - 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()); } + for (auto cell : module->cells()) + { + if (ff_types.cell_known(cell->type)) + continue; - Net *impl_to_seq(Instance *inst) - { - if (inst == nullptr) - return nullptr; - - if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME) { - Net *new_net = impl_to_seq(get_ast_input(inst)); - if (new_net) { - inst->Disconnect(inst->View()->GetInput()); - inst->Connect(inst->View()->GetInput(), new_net); - } - return nullptr; - } + for (auto conn : cell->connections()) + { + if (!cell->output(conn.first)) + continue; - if (inst->Type() == PRIM_SVA_AT) { - Net *new_net = impl_to_seq(get_ast_input2(inst)); - if (new_net) { - inst->Disconnect(inst->View()->GetInput2()); - inst->Connect(inst->View()->GetInput2(), new_net); + for (auto bit : conn.second) + if (bit.wire != nullptr) + non_ff_bits.insert(bit); } - return nullptr; } - if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) + for (auto wire : module->wires()) { - if (mode_cover) { - Net *new_in1 = impl_to_seq(get_ast_input1(inst)); - Net *new_in2 = impl_to_seq(get_ast_input2(inst)); - if (!new_in1) new_in1 = inst->GetInput1(); - if (!new_in2) new_in2 = inst->GetInput2(); - return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile()); - } - } + if (!wire->attributes.count("\\init")) + continue; - return nullptr; - } + Const &initval = wire->attributes.at("\\init"); + for (int i = 0; i < GetSize(initval); i++) + { + if (initval[i] != State::S0 && initval[i] != State::S1) + continue; - void run() - { - module = importer->module; - netlist = root->Owner(); + if (non_ff_bits.count(SigBit(wire, i))) + initval[i] = State::Sx; + } - // impl_to_seq(root); + if (initval.is_fully_undef()) + wire->attributes.erase("\\init"); + } } -}; - -void svapp_assert(VerificImporter *importer, Instance *inst) -{ - VerificSvaPP worker; - worker.importer = importer; - worker.root = inst; - worker.mode_assert = true; - worker.run(); -} - -void svapp_assume(VerificImporter *importer, Instance *inst) -{ - VerificSvaPP worker; - worker.importer = importer; - worker.root = inst; - worker.mode_assume = true; - worker.run(); -} - -void svapp_cover(VerificImporter *importer, Instance *inst) -{ - VerificSvaPP worker; - worker.importer = importer; - worker.root = inst; - worker.mode_cover = true; - worker.run(); } // ================================================================== -struct VerificSvaImporter +VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only) { - VerificImporter *importer; - Module *module; + module = importer->module; - Netlist *netlist; - Instance *root; - - SigBit clock = State::Sx; - bool clock_posedge = false; - - SigBit disable_iff = State::S0; + log_assert(importer != nullptr); + log_assert(net != nullptr); - bool mode_assert = false; - bool mode_assume = false; - bool mode_cover = false; - bool eventually = false; + Instance *inst = net->Driver(); - Instance *net_to_ast_driver(Net *n) + if (inst != nullptr && inst->Type() == PRIM_SVA_AT) { - if (n == nullptr) - return nullptr; + net = inst->GetInput1(); + body_net = inst->GetInput2(); - if (n->IsMultipleDriven()) - return nullptr; + inst = net->Driver(); - Instance *inst = n->Driver(); - - if (inst == nullptr) - return nullptr; - - if (!importer->verific_sva_prims.count(inst->Type()) && - !importer->verific_psl_prims.count(inst->Type())) - return nullptr; - - if (inst->Type() == PRIM_SVA_PAST) - return nullptr; - - return inst; + Instance *body_inst = body_net->Driver(); + if (body_inst != nullptr && body_inst->Type() == PRIM_SVA_DISABLE_IFF) { + disable_net = body_inst->GetInput1(); + disable_sig = importer->net_map_at(disable_net); + body_net = body_inst->GetInput2(); + } } - - 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()); } - - struct sequence_t { - int length = 0; - SigBit sig_a = State::S1; - SigBit sig_en = State::S1; - }; - - void sequence_cond(sequence_t &seq, SigBit cond) + else { - seq.sig_a = module->And(NEW_ID, seq.sig_a, cond); + if (sva_at_only) + return; } - void sequence_ff(sequence_t &seq) + // Use while() instead of if() to work around VIPER #13453 + while (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE) { - 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; + net = inst->GetInput(); + inst = net->Driver();; } - void parse_sequence(sequence_t &seq, Net *n) + if (inst != nullptr && inst->Type() == PRIM_INV) { - 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; - } + net = inst->GetInput(); + inst = net->Driver();; + posedge = false; + } - // PSL Primitives + // Detect clock-enable circuit + do { + if (inst == nullptr || inst->Type() != PRIM_AND) + break; - if (inst->Type() == PRIM_ALWAYS) - { - parse_sequence(seq, inst->GetInput()); - return; - } + Net *net_dlatch = inst->GetInput1(); + Instance *inst_dlatch = net_dlatch->Driver(); - if (inst->Type() == PRIM_IMPL) - { - 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_dlatch == nullptr || inst_dlatch->Type() != PRIM_DLATCHRS) + break; - if (inst->Type() == PRIM_SUFFIX_IMPL) - { - 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_dlatch->GetSet()->IsGnd() || !inst_dlatch->GetReset()->IsGnd()) + break; - // Handle unsupported primitives + Net *net_enable = inst_dlatch->GetInput(); + Net *net_not_clock = inst_dlatch->GetControl(); - 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 (net_enable == nullptr || net_not_clock == nullptr) + break; - void run() - { - module = importer->module; - netlist = root->Owner(); + Instance *inst_not_clock = net_not_clock->Driver(); - // parse SVA property clock event + if (inst_not_clock == nullptr || inst_not_clock->Type() != PRIM_INV) + break; - Instance *at_node = get_ast_input(root); - log_assert(at_node && (at_node->Type() == PRIM_SVA_AT || at_node->Type() == PRIM_AT)); + Net *net_clock1 = inst_not_clock->GetInput(); + Net *net_clock2 = inst->GetInput2(); - VerificClockEdge clock_edge(importer, at_node->Type() == PRIM_SVA_AT ? get_ast_input1(at_node) : at_node->GetInput2()->Driver()); - clock = clock_edge.clock_sig; - clock_posedge = clock_edge.posedge; + if (net_clock1 == nullptr || net_clock1 != net_clock2) + break; - // parse disable_iff expression + enable_net = net_enable; + enable_sig = importer->net_map_at(enable_net); - Net *sequence_net = at_node->Type() == PRIM_SVA_AT ? at_node->GetInput2() : at_node->GetInput1(); + net = net_clock1; + inst = net->Driver();; + } while (0); - while (1) - { - Instance *sequence_node = net_to_ast_driver(sequence_net); + // Detect condition expression + do { + if (body_net == nullptr) + break; - if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) { - eventually = true; - sequence_net = sequence_node->GetInput(); - continue; - } + Instance *inst_mux = body_net->Driver(); - 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; - } + if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX) + break; - if (sequence_node && sequence_node->Type() == PRIM_ABORT) { - disable_iff = importer->net_map_at(sequence_node->GetInput2()); - sequence_net = sequence_node->GetInput1(); - continue; - } + if (!inst_mux->GetInput1()->IsPwr()) + break; + Net *sva_net = inst_mux->GetInput2(); + if (!verific_is_sva_net(importer, sva_net)) break; - } - // parse SVA sequence into trigger signal + body_net = sva_net; + cond_net = inst_mux->GetControl(); + } while (0); - sequence_t seq; - parse_sequence(seq, sequence_net); - sequence_ff(seq); + clock_net = net; + clock_sig = importer->net_map_at(clock_net); - // generate assert/assume/cover cell + const char *gclk_attr = clock_net->GetAttValue("gclk"); + if (gclk_attr != nullptr && (!strcmp(gclk_attr, "1") || !strcmp(gclk_attr, "'1'"))) + gclk = true; +} - RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); +Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value) +{ + log_assert(GetSize(sig_d) == GetSize(sig_q)); - if (eventually) { - if (mode_assert) module->addLive(root_name, seq.sig_a, seq.sig_en); - if (mode_assume) module->addFair(root_name, seq.sig_a, seq.sig_en); + if (GetSize(init_value) != 0) { + log_assert(GetSize(sig_q) == GetSize(init_value)); + if (sig_q.is_wire()) { + sig_q.as_wire()->attributes["\\init"] = init_value; } else { - if (mode_assert) module->addAssert(root_name, seq.sig_a, seq.sig_en); - if (mode_assume) module->addAssume(root_name, seq.sig_a, seq.sig_en); - if (mode_cover) module->addCover(root_name, seq.sig_a, seq.sig_en); + Wire *w = module->addWire(NEW_ID, GetSize(sig_q)); + w->attributes["\\init"] = init_value; + module->connect(sig_q, w); + sig_q = w; } } -}; -void import_sva_assert(VerificImporter *importer, Instance *inst) -{ - VerificSvaImporter worker; - worker.importer = importer; - worker.root = inst; - worker.mode_assert = true; - worker.run(); + if (enable_sig != State::S1) + sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig); + + if (disable_sig != State::S0) { + log_assert(gclk == false); + log_assert(GetSize(sig_q) == GetSize(init_value)); + return module->addAdff(name, clock_sig, disable_sig, sig_d, sig_q, init_value, posedge); + } + + if (gclk) + return module->addFf(name, sig_d, sig_q); + + return module->addDff(name, clock_sig, sig_d, sig_q, posedge); } -void import_sva_assume(VerificImporter *importer, Instance *inst) +Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value) { - VerificSvaImporter worker; - worker.importer = importer; - worker.root = inst; - worker.mode_assume = true; - worker.run(); + log_assert(gclk == false); + log_assert(disable_sig == State::S0); + + if (enable_sig != State::S1) + sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig); + + return module->addAdff(name, clock_sig, sig_arst, sig_d, sig_q, arst_value, posedge); } -void import_sva_cover(VerificImporter *importer, Instance *inst) +Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q) { - VerificSvaImporter worker; - worker.importer = importer; - worker.root = inst; - worker.mode_cover = true; - worker.run(); + log_assert(gclk == false); + log_assert(disable_sig == State::S0); + + if (enable_sig != State::S1) + sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig); + + return module->addDffsr(name, clock_sig, sig_set, sig_clr, sig_d, sig_q, posedge); } // ================================================================== @@ -1753,33 +1695,37 @@ void import_sva_cover(VerificImporter *importer, Instance *inst) struct VerificExtNets { int portname_cnt = 0; - bool verbose = false; // a map from Net to the same Net one level up in the design hierarchy - std::map<Net*, Net*> net_level_up; + std::map<Net*, Net*> net_level_up_drive_up; + std::map<Net*, Net*> net_level_up_drive_down; - Net *get_net_level_up(Net *net) + Net *route_up(Net *net, bool drive_up, Net *final_net = nullptr) { + auto &net_level_up = drive_up ? net_level_up_drive_up : net_level_up_drive_down; + if (net_level_up.count(net) == 0) { Netlist *nl = net->Owner(); // Simply return if Netlist is not unique - if (nl->NumOfRefs() != 1) - return net; + log_assert(nl->NumOfRefs() == 1); Instance *up_inst = (Instance*)nl->GetReferences()->GetLast(); Netlist *up_nl = up_inst->Owner(); // create new Port string name = stringf("___extnets_%d", portname_cnt++); - Port *new_port = new Port(name.c_str(), DIR_OUT); + Port *new_port = new Port(name.c_str(), drive_up ? DIR_OUT : DIR_IN); nl->Add(new_port); net->Connect(new_port); // create new Net in up Netlist - Net *new_net = new Net(name.c_str()); - up_nl->Add(new_net); + Net *new_net = final_net; + if (new_net == nullptr || new_net->Owner() != up_nl) { + new_net = new Net(name.c_str()); + up_nl->Add(new_net); + } up_inst->Connect(new_port, new_net); net_level_up[net] = new_net; @@ -1788,6 +1734,39 @@ struct VerificExtNets return net_level_up.at(net); } + Net *route_up(Net *net, bool drive_up, Netlist *dest, Net *final_net = nullptr) + { + while (net->Owner() != dest) + net = route_up(net, drive_up, final_net); + if (final_net != nullptr) + log_assert(net == final_net); + return net; + } + + Netlist *find_common_ancestor(Netlist *A, Netlist *B) + { + std::set<Netlist*> ancestors_of_A; + + Netlist *cursor = A; + while (1) { + ancestors_of_A.insert(cursor); + if (cursor->NumOfRefs() != 1) + break; + cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner(); + } + + cursor = B; + while (1) { + if (ancestors_of_A.count(cursor)) + return cursor; + if (cursor->NumOfRefs() != 1) + break; + cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner(); + } + + log_error("No common ancestor found between %s and %s.\n", get_full_netlist_name(A).c_str(), get_full_netlist_name(B).c_str()); + } + void run(Netlist *nl) { MapIter mi, mi2; @@ -1808,22 +1787,40 @@ struct VerificExtNets if (!net->IsExternalTo(nl)) continue; - if (verbose) + if (verific_verbose) log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name()); - while (net->IsExternalTo(nl)) + Netlist *ext_nl = net->Owner(); + + if (verific_verbose) + log(" external net owner: %s\n", get_full_netlist_name(ext_nl).c_str()); + + Netlist *ca_nl = find_common_ancestor(nl, ext_nl); + + if (verific_verbose) + log(" common ancestor: %s\n", get_full_netlist_name(ca_nl).c_str()); + + Net *ca_net = route_up(net, !port->IsOutput(), ca_nl); + Net *new_net = ca_net; + + if (ca_nl != nl) { - Net *newnet = get_net_level_up(net); - if (newnet == net) break; + if (verific_verbose) + log(" net in common ancestor: %s\n", ca_net->Name()); + + string name = stringf("___extnets_%d", portname_cnt++); + new_net = new Net(name.c_str()); + nl->Add(new_net); - if (verbose) - log(" external net: %s.%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name()); - net = newnet; + Net *n YS_ATTRIBUTE(unused) = route_up(new_net, port->IsOutput(), ca_nl, ca_net); + log_assert(n == ca_net); } - if (verbose) - log(" final net: %s.%s%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name(), net->IsExternalTo(nl) ? " (external)" : ""); - todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, net)); + if (verific_verbose) + log(" new local net: %s\n", new_net->Name()); + + log_assert(!new_net->IsExternalTo(nl)); + todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, new_net)); } for (auto it : todo_connect) { @@ -1833,11 +1830,112 @@ struct VerificExtNets } }; +void verific_import(Design *design, const std::map<std::string,std::string> ¶meters, std::string top) +{ + verific_sva_fsm_limit = 16; + + std::set<Netlist*> nl_todo, nl_done; + + VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1); + VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1); + Array *netlists = NULL; + Array veri_libs, vhdl_libs; + if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib); + if (veri_lib) veri_libs.InsertLast(veri_lib); + + Map verific_params(STRING_HASH); + for (const auto &i : parameters) + verific_params.Insert(i.first.c_str(), i.second.c_str()); + + if (top.empty()) { + netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params); + } + else { + Array veri_modules, vhdl_units; + + if (veri_lib) { + VeriModule *veri_module = veri_lib->GetModule(top.c_str(), 1); + if (veri_module) { + veri_modules.InsertLast(veri_module); + } + + // Also elaborate all root modules since they may contain bind statements + MapIter mi; + FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) { + if (!veri_module->IsRootModule()) continue; + veri_modules.InsertLast(veri_module); + } + } + + if (vhdl_lib) { + VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(top.c_str()); + if (vhdl_unit) + vhdl_units.InsertLast(vhdl_unit); + } + + netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &verific_params); + } + + Netlist *nl; + int i; + + FOREACH_ARRAY_ITEM(netlists, i, nl) { + if (top.empty() && nl->CellBaseName() != top) + continue; + nl->AddAtt(new Att(" \\top", NULL)); + nl_todo.insert(nl); + } + + delete netlists; + + if (!verific_error_msg.empty()) + log_error("%s\n", verific_error_msg.c_str()); + + VerificExtNets worker; + for (auto nl : nl_todo) + worker.run(nl); + + while (!nl_todo.empty()) { + Netlist *nl = *nl_todo.begin(); + if (nl_done.count(nl) == 0) { + VerificImporter importer(false, false, false, false, false, false, false); + importer.import_netlist(design, nl, nl_todo, nl->Owner()->Name() == top); + } + nl_todo.erase(nl); + nl_done.insert(nl); + } + + veri_file::Reset(); + vhdl_file::Reset(); + Libset::Reset(); + verific_incdirs.clear(); + verific_libdirs.clear(); + verific_import_pending = false; + + if (!verific_error_msg.empty()) + log_error("%s\n", verific_error_msg.c_str()); +} + +YOSYS_NAMESPACE_END #endif /* YOSYS_ENABLE_VERIFIC */ +PRIVATE_NAMESPACE_BEGIN + +#ifdef YOSYS_ENABLE_VERIFIC +bool check_noverific_env() +{ + const char *e = getenv("YOSYS_NOVERIFIC"); + if (e == nullptr) + return false; + if (atoi(e) == 0) + return false; + return true; +} +#endif + struct VerificPass : public Pass { VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { } - virtual void help() + void help() YS_OVERRIDE { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -1845,12 +1943,37 @@ struct VerificPass : public Pass { log("\n"); log("Load the specified Verilog/SystemVerilog files into Verific.\n"); log("\n"); + log("All files specified in one call to this command are one compilation unit.\n"); + log("Files passed to different calls to this command are treated as belonging to\n"); + log("different compilation units.\n"); log("\n"); - log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl|-vhdpsl} <vhdl-file>..\n"); + log("Additional -D<macro>[=<value>] options may be added after the option indicating\n"); + log("the language version (and before file names) to set additional verilog defines.\n"); + log("The macros SYNTHESIS and VERIFIC are defined implicitly.\n"); + log("\n"); + log("\n"); + log(" verific -formal <verilog-file>..\n"); + log("\n"); + log("Like -sv, but define FORMAL instead of SYNTHESIS.\n"); + log("\n"); + log("\n"); + log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n"); log("\n"); log("Load the specified VHDL files into Verific.\n"); log("\n"); log("\n"); + log(" verific [-work <libname>] {-sv|-vhdl|...} <hdl-file>\n"); + log("\n"); + log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n"); + log("(default library when -work is not present: \"work\")\n"); + log("\n"); + log("\n"); + log(" verific [-L <libname>] {-sv|-vhdl|...} <hdl-file>\n"); + log("\n"); + log("Look up external definitions in the specified library.\n"); + log("(-L may be used more than once)\n"); + log("\n"); + log("\n"); log(" verific -vlog-incdir <directory>..\n"); log("\n"); log("Add Verilog include directories.\n"); @@ -1864,7 +1987,21 @@ struct VerificPass : public Pass { log("\n"); log(" verific -vlog-define <macro>[=<value>]..\n"); log("\n"); - log("Add Verilog defines. (The macros SYNTHESIS and VERIFIC are defined implicitly.)\n"); + log("Add Verilog defines.\n"); + log("\n"); + log("\n"); + log(" verific -vlog-undef <macro>..\n"); + log("\n"); + log("Remove Verilog defines previously set with -vlog-define.\n"); + log("\n"); + log("\n"); + log(" verific -set-error <msg_id>..\n"); + log(" verific -set-warning <msg_id>..\n"); + log(" verific -set-info <msg_id>..\n"); + log(" verific -set-ignore <msg_id>..\n"); + log("\n"); + log("Set message severity. <msg_id> is the string in square brackets when a message\n"); + log("is printed, such as VERI-1209.\n"); log("\n"); log("\n"); log(" verific -import [options] <top-module>..\n"); @@ -1887,8 +2024,21 @@ struct VerificPass : public Pass { log(" -extnets\n"); log(" Resolve references to external nets by adding module ports as needed.\n"); log("\n"); - log(" -v\n"); - log(" Verbose log messages.\n"); + log(" -autocover\n"); + log(" Generate automatic cover statements for all asserts\n"); + log("\n"); + log(" -fullinit\n"); + log(" Keep all register initializations, even those for non-FF registers.\n"); + log("\n"); + log(" -chparam name value \n"); + log(" Elaborate the specified top modules (all modules when -all given) using\n"); + log(" this parameter value. Modules on which this parameter does not exist will\n"); + log(" cause Verific to produce a VERI-1928 or VHDL-1676 message. This option\n"); + log(" can be specified multiple times to override multiple parameters.\n"); + log(" String values must be passed in double quotes (\").\n"); + log("\n"); + log(" -v, -vv\n"); + log(" Verbose log messages. (-vv is even more verbose than -v.)\n"); log("\n"); log("The following additional import options are useful for debugging the Verific\n"); log("bindings (for Yosys and/or Verific developers):\n"); @@ -1899,12 +2049,14 @@ struct VerificPass : public Pass { log(" This will also add all SVA related cells to the design parallel to\n"); log(" the checker logic inferred by it.\n"); log("\n"); + log(" -V\n"); + log(" Import Verific netlist as-is without translating to Yosys cell types. \n"); + log("\n"); log(" -nosva\n"); - log(" Ignore SVA properties, do not infer checker logic. (This also disables\n"); - log(" PSL properties in -vhdpsl mode.)\n"); + log(" Ignore SVA properties, do not infer checker logic.\n"); log("\n"); - log(" -nosvapp\n"); - log(" Disable SVA properties pre-processing pass. This implies -nosva.\n"); + log(" -L <int>\n"); + log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n"); log("\n"); log(" -n\n"); log(" Keep all Verific names on instances and nets. By default only\n"); @@ -1913,20 +2065,66 @@ struct VerificPass : public Pass { log(" -d <dump_file>\n"); log(" Dump the Verific netlist as a verilog file.\n"); log("\n"); - log("Visit http://verific.com/ for more information on Verific.\n"); + log("\n"); + log("Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"); + log("https://www.symbioticeda.com/seda-suite\n"); + log("\n"); + log("Contact office@symbioticeda.com for free evaluation\n"); + log("binaries of Symbiotic EDA Suite.\n"); log("\n"); } #ifdef YOSYS_ENABLE_VERIFIC - virtual void execute(std::vector<std::string> args, RTLIL::Design *design) + void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE { + static bool set_verific_global_flags = true; + + if (check_noverific_env()) + log_cmd_error("This version of Yosys is built without Verific support.\n" + "\n" + "Use Symbiotic EDA Suite if you need Yosys+Verifc.\n" + "https://www.symbioticeda.com/seda-suite\n" + "\n" + "Contact office@symbioticeda.com for free evaluation\n" + "binaries of Symbiotic EDA Suite.\n"); + log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n"); - Message::SetConsoleOutput(0); - Message::RegisterCallBackMsg(msg_func); - RuntimeFlags::SetVar("db_allow_external_nets", 1); - RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0); - veri_file::DefineCmdLineMacro("VERIFIC"); - veri_file::DefineCmdLineMacro("SYNTHESIS"); + if (set_verific_global_flags) + { + Message::SetConsoleOutput(0); + Message::RegisterCallBackMsg(msg_func); + + RuntimeFlags::SetVar("db_preserve_user_nets", 1); + RuntimeFlags::SetVar("db_allow_external_nets", 1); + RuntimeFlags::SetVar("db_infer_wide_operators", 1); + + RuntimeFlags::SetVar("veri_extract_dualport_rams", 0); + RuntimeFlags::SetVar("veri_extract_multiport_rams", 1); + + RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0); + RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1); + + RuntimeFlags::SetVar("vhdl_support_variable_slice", 1); + RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0); + + // Workaround for VIPER #13851 + RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1); + + // WARNING: instantiating unknown module 'XYZ' (VERI-1063) + Message::SetMessageType("VERI-1063", VERIFIC_ERROR); + + // https://github.com/YosysHQ/yosys/issues/1055 + RuntimeFlags::SetVar("veri_elaborate_top_level_modules_having_interface_ports", 1) ; + +#ifndef DB_PRESERVE_INITIAL_VALUE +# warning Verific was built without DB_PRESERVE_INITIAL_VALUE. +#endif + + set_verific_global_flags = false; + } + + verific_verbose = 0; + verific_sva_fsm_limit = 16; const char *release_str = Message::ReleaseString(); time_t release_time = Message::ReleaseDate(); @@ -1941,16 +2139,39 @@ struct VerificPass : public Pass { log("Built with Verific %s, released at %s.\n", release_str, release_tmstr); int argidx = 1; + std::string work = "work"; + + if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" || + args[argidx] == "-set-info" || args[argidx] == "-set-ignore")) + { + msg_type_t new_type; + + if (args[argidx] == "-set-error") + new_type = VERIFIC_ERROR; + else if (args[argidx] == "-set-warning") + new_type = VERIFIC_WARNING; + else if (args[argidx] == "-set-info") + new_type = VERIFIC_INFO; + else if (args[argidx] == "-set-ignore") + new_type = VERIFIC_IGNORE; + else + log_abort(); + + for (argidx++; argidx < GetSize(args); argidx++) + Message::SetMessageType(args[argidx].c_str(), new_type); + + goto check_error; + } if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") { for (argidx++; argidx < GetSize(args); argidx++) - veri_file::AddIncludeDir(args[argidx].c_str()); + verific_incdirs.push_back(args[argidx]); goto check_error; } if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") { for (argidx++; argidx < GetSize(args); argidx++) - veri_file::AddYDir(args[argidx].c_str()); + verific_libdirs.push_back(args[argidx]); goto check_error; } @@ -1969,78 +2190,115 @@ struct VerificPass : public Pass { goto check_error; } - if (GetSize(args) > argidx && args[argidx] == "-vlog95") { - for (argidx++; argidx < GetSize(args); argidx++) - if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_95)) - log_cmd_error("Reading `%s' in VERILOG_95 mode failed.\n", args[argidx].c_str()); + if (GetSize(args) > argidx && args[argidx] == "-vlog-undef") { + for (argidx++; argidx < GetSize(args); argidx++) { + string name = args[argidx]; + veri_file::UndefineMacro(name.c_str()); + } goto check_error; } - if (GetSize(args) > argidx && args[argidx] == "-vlog2k") { - for (argidx++; argidx < GetSize(args); argidx++) - if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_2K)) - log_cmd_error("Reading `%s' in VERILOG_2K mode failed.\n", args[argidx].c_str()); - goto check_error; + veri_file::RemoveAllLOptions(); + for (; argidx < GetSize(args); argidx++) + { + if (args[argidx] == "-work" && argidx+1 < GetSize(args)) { + work = args[++argidx]; + continue; + } + if (args[argidx] == "-L" && argidx+1 < GetSize(args)) { + veri_file::AddLOption(args[++argidx].c_str()); + continue; + } + break; } - if (GetSize(args) > argidx && args[argidx] == "-sv2005") { - for (argidx++; argidx < GetSize(args); argidx++) - if (!veri_file::Analyze(args[argidx].c_str(), veri_file::SYSTEM_VERILOG_2005)) - log_cmd_error("Reading `%s' in SYSTEM_VERILOG_2005 mode failed.\n", args[argidx].c_str()); - goto check_error; - } + if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" || + args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal")) + { + Array file_names; + unsigned verilog_mode; + + if (args[argidx] == "-vlog95") + verilog_mode = veri_file::VERILOG_95; + else if (args[argidx] == "-vlog2k") + verilog_mode = veri_file::VERILOG_2K; + else if (args[argidx] == "-sv2005") + verilog_mode = veri_file::SYSTEM_VERILOG_2005; + else if (args[argidx] == "-sv2009") + verilog_mode = veri_file::SYSTEM_VERILOG_2009; + else if (args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal") + verilog_mode = veri_file::SYSTEM_VERILOG; + else + log_abort(); - if (GetSize(args) > argidx && args[argidx] == "-sv2009") { - for (argidx++; argidx < GetSize(args); argidx++) - if (!veri_file::Analyze(args[argidx].c_str(), veri_file::SYSTEM_VERILOG_2009)) - log_cmd_error("Reading `%s' in SYSTEM_VERILOG_2009 mode failed.\n", args[argidx].c_str()); - goto check_error; - } + veri_file::DefineMacro("VERIFIC"); + veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS"); - if (GetSize(args) > argidx && (args[argidx] == "-sv2012" || args[argidx] == "-sv")) { - for (argidx++; argidx < GetSize(args); argidx++) - if (!veri_file::Analyze(args[argidx].c_str(), veri_file::SYSTEM_VERILOG)) - log_cmd_error("Reading `%s' in SYSTEM_VERILOG mode failed.\n", args[argidx].c_str()); + for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].compare(0, 2, "-D") == 0; argidx++) { + std::string name = args[argidx].substr(2); + if (args[argidx] == "-D") { + if (++argidx >= GetSize(args)) + break; + name = args[argidx]; + } + size_t equal = name.find('='); + if (equal != std::string::npos) { + string value = name.substr(equal+1); + name = name.substr(0, equal); + veri_file::DefineMacro(name.c_str(), value.c_str()); + } else { + veri_file::DefineMacro(name.c_str()); + } + } + + for (auto &dir : verific_incdirs) + veri_file::AddIncludeDir(dir.c_str()); + for (auto &dir : verific_libdirs) + veri_file::AddYDir(dir.c_str()); + + while (argidx < GetSize(args)) + file_names.Insert(args[argidx++].c_str()); + + if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU)) + log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n"); + + verific_import_pending = true; goto check_error; } if (GetSize(args) > argidx && args[argidx] == "-vhdl87") { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str()); for (argidx++; argidx < GetSize(args); argidx++) - if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_87)) + if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_87)) log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str()); + verific_import_pending = true; goto check_error; } if (GetSize(args) > argidx && args[argidx] == "-vhdl93") { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str()); for (argidx++; argidx < GetSize(args); argidx++) - if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_93)) + if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_93)) log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str()); + verific_import_pending = true; goto check_error; } if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str()); for (argidx++; argidx < GetSize(args); argidx++) - if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2K)) + if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2K)) log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str()); + verific_import_pending = true; goto check_error; } if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str()); for (argidx++; argidx < GetSize(args); argidx++) - if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2008)) + if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2008)) log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str()); - goto check_error; - } - - if (GetSize(args) > argidx && args[argidx] == "-vhdpsl") { - vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str()); - for (argidx++; argidx < GetSize(args); argidx++) - if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_PSL)) - log_cmd_error("Reading `%s' in VHDL_PSL mode failed.\n", args[argidx].c_str()); + verific_import_pending = true; goto check_error; } @@ -2048,9 +2306,11 @@ struct VerificPass : public Pass { { std::set<Netlist*> nl_todo, nl_done; bool mode_all = false, mode_gates = false, mode_keep = false; - bool mode_nosva = false, mode_nosvapp = false, mode_names = false; - bool verbose = false, flatten = false, extnets = false; + bool mode_nosva = false, mode_names = false, mode_verific = false; + bool mode_autocover = false, mode_fullinit = false; + bool flatten = false, extnets = false; string dumpfile; + Map parameters(STRING_HASH); for (argidx++; argidx < GetSize(args); argidx++) { if (args[argidx] == "-all") { @@ -2077,17 +2337,41 @@ struct VerificPass : public Pass { mode_nosva = true; continue; } - if (args[argidx] == "-nosvapp") { - mode_nosva = true; - mode_nosvapp = true; + if (args[argidx] == "-L" && argidx+1 < GetSize(args)) { + verific_sva_fsm_limit = atoi(args[++argidx].c_str()); continue; } if (args[argidx] == "-n") { mode_names = true; continue; } + if (args[argidx] == "-autocover") { + mode_autocover = true; + continue; + } + if (args[argidx] == "-fullinit") { + mode_fullinit = true; + continue; + } + if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) { + const std::string &key = args[++argidx]; + const std::string &value = args[++argidx]; + unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(), + 1 /* force_overwrite */); + if (!new_insertion) + log_warning_noprefix("-chparam %s already specified: overwriting.\n", key.c_str()); + continue; + } + if (args[argidx] == "-V") { + mode_verific = true; + continue; + } if (args[argidx] == "-v") { - verbose = true; + verific_verbose = 1; + continue; + } + if (args[argidx] == "-vv") { + verific_verbose = 2; continue; } if (args[argidx] == "-d" && argidx+1 < GetSize(args)) { @@ -2097,66 +2381,84 @@ struct VerificPass : public Pass { break; } - if (argidx > GetSize(args) && args[argidx].substr(0, 1) == "-") + if (argidx > GetSize(args) && args[argidx].compare(0, 1, "-") == 0) cmd_error(args, argidx, "unknown option"); + std::set<std::string> top_mod_names; + if (mode_all) { - log("Running veri_file::ElaborateAll().\n"); - if (!veri_file::ElaborateAll()) - log_cmd_error("Elaboration of Verilog modules failed.\n"); + log("Running hier_tree::ElaborateAll().\n"); - log("Running vhdl_file::ElaborateAll().\n"); - if (!vhdl_file::ElaborateAll()) - log_cmd_error("Elaboration of VHDL modules failed.\n"); - - Library *lib = Netlist::PresentDesign()->Owner()->Owner(); - - if (argidx == GetSize(args)) - { - MapIter iter; - char *iter_name; - Verific::Cell *iter_cell; + VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1); + VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1); - FOREACH_MAP_ITEM(lib->GetCells(), iter, &iter_name, &iter_cell) { - if (*iter_name != '$') - nl_todo.insert(iter_cell->GetFirstNetlist()); - } - } - else - { - for (; argidx < GetSize(args); argidx++) - { - Verific::Cell *cell = lib->GetCell(args[argidx].c_str()); + Array veri_libs, vhdl_libs; + if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib); + if (veri_lib) veri_libs.InsertLast(veri_lib); - if (cell == nullptr) - log_cmd_error("Module not found: %s\n", args[argidx].c_str()); + Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, ¶meters); + Netlist *nl; + int i; - nl_todo.insert(cell->GetFirstNetlist()); - cell->GetFirstNetlist()->SetPresentDesign(); - } - } + FOREACH_ARRAY_ITEM(netlists, i, nl) + nl_todo.insert(nl); + delete netlists; } else { if (argidx == GetSize(args)) log_cmd_error("No top module specified.\n"); - for (; argidx < GetSize(args); argidx++) { - if (veri_file::GetModule(args[argidx].c_str())) { - log("Running veri_file::Elaborate(\"%s\").\n", args[argidx].c_str()); - if (!veri_file::Elaborate(args[argidx].c_str())) - log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str()); - nl_todo.insert(Netlist::PresentDesign()); - } else { - log("Running vhdl_file::Elaborate(\"%s\").\n", args[argidx].c_str()); - if (!vhdl_file::Elaborate(args[argidx].c_str())) - log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str()); - nl_todo.insert(Netlist::PresentDesign()); + Array veri_modules, vhdl_units; + for (; argidx < GetSize(args); argidx++) + { + const char *name = args[argidx].c_str(); + top_mod_names.insert(name); + VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1); + + if (veri_lib) { + VeriModule *veri_module = veri_lib->GetModule(name, 1); + if (veri_module) { + log("Adding Verilog module '%s' to elaboration queue.\n", name); + veri_modules.InsertLast(veri_module); + continue; + } + + // Also elaborate all root modules since they may contain bind statements + MapIter mi; + FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) { + if (!veri_module->IsRootModule()) continue; + veri_modules.InsertLast(veri_module); + } } + + VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1); + VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(name); + if (vhdl_unit) { + log("Adding VHDL unit '%s' to elaboration queue.\n", name); + vhdl_units.InsertLast(vhdl_unit); + continue; + } + + log_error("Can't find module/unit '%s'.\n", name); + } + + log("Running hier_tree::Elaborate().\n"); + Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, ¶meters); + Netlist *nl; + int i; + + FOREACH_ARRAY_ITEM(netlists, i, nl) { + nl->AddAtt(new Att(" \\top", NULL)); + nl_todo.insert(nl); } + delete netlists; } + if (!verific_error_msg.empty()) + goto check_error; + if (flatten) { for (auto nl : nl_todo) nl->Flatten(); @@ -2164,7 +2466,6 @@ struct VerificPass : public Pass { if (extnets) { VerificExtNets worker; - worker.verbose = verbose; for (auto nl : nl_todo) worker.run(nl); } @@ -2177,8 +2478,9 @@ struct VerificPass : public Pass { while (!nl_todo.empty()) { Netlist *nl = *nl_todo.begin(); if (nl_done.count(nl) == 0) { - VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose); - importer.import_netlist(design, nl, nl_todo); + VerificImporter importer(mode_gates, mode_keep, mode_nosva, + mode_names, mode_verific, mode_autocover, mode_fullinit); + importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->Owner()->Name())); } nl_todo.erase(nl); nl_done.insert(nl); @@ -2187,6 +2489,9 @@ struct VerificPass : public Pass { veri_file::Reset(); vhdl_file::Reset(); Libset::Reset(); + verific_incdirs.clear(); + verific_libdirs.clear(); + verific_import_pending = false; goto check_error; } @@ -2198,11 +2503,168 @@ struct VerificPass : public Pass { } #else /* YOSYS_ENABLE_VERIFIC */ - virtual void execute(std::vector<std::string>, RTLIL::Design *) { - log_cmd_error("This version of Yosys is built without Verific support.\n"); + void execute(std::vector<std::string>, RTLIL::Design *) YS_OVERRIDE { + log_cmd_error("This version of Yosys is built without Verific support.\n" + "\n" + "Use Symbiotic EDA Suite if you need Yosys+Verifc.\n" + "https://www.symbioticeda.com/seda-suite\n" + "\n" + "Contact office@symbioticeda.com for free evaluation\n" + "binaries of Symbiotic EDA Suite.\n"); } #endif } VerificPass; -PRIVATE_NAMESPACE_END +struct ReadPass : public Pass { + ReadPass() : Pass("read", "load HDL designs") { } + void help() YS_OVERRIDE + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..\n"); + log("\n"); + log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n"); + log("is only available via Verific.)\n"); + log("\n"); + log("Additional -D<macro>[=<value>] options may be added after the option indicating\n"); + log("the language version (and before file names) to set additional verilog defines.\n"); + log("\n"); + log("\n"); + log(" read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n"); + log("\n"); + log("Load the specified VHDL files. (Requires Verific.)\n"); + log("\n"); + log("\n"); + log(" read -define <macro>[=<value>]..\n"); + log("\n"); + log("Set global Verilog/SystemVerilog defines.\n"); + log("\n"); + log("\n"); + log(" read -undef <macro>..\n"); + log("\n"); + log("Unset global Verilog/SystemVerilog defines.\n"); + log("\n"); + log("\n"); + log(" read -incdir <directory>\n"); + log("\n"); + log("Add directory to global Verilog/SystemVerilog include directories.\n"); + log("\n"); + log("\n"); + log(" read -verific\n"); + log(" read -noverific\n"); + log("\n"); + log("Subsequent calls to 'read' will either use or not use Verific. Calling 'read'\n"); + log("with -verific will result in an error on Yosys binaries that are built without\n"); + log("Verific support. The default is to use Verific if it is available.\n"); + log("\n"); + } + void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + { +#ifdef YOSYS_ENABLE_VERIFIC + static bool verific_available = !check_noverific_env(); +#else + static bool verific_available = false; +#endif + static bool use_verific = verific_available; + + if (args.size() < 2 || args[1][0] != '-') + log_cmd_error("Missing mode parameter.\n"); + + if (args[1] == "-verific" || args[1] == "-noverific") { + if (args.size() != 2) + log_cmd_error("Additional arguments to -verific/-noverific.\n"); + if (args[1] == "-verific") { + if (!verific_available) + log_cmd_error("This version of Yosys is built without Verific support.\n"); + use_verific = true; + } else { + use_verific = false; + } + return; + } + + if (args.size() < 3) + log_cmd_error("Missing file name parameter.\n"); + + if (args[1] == "-vlog95" || args[1] == "-vlog2k") { + if (use_verific) { + args[0] = "verific"; + } else { + args[0] = "read_verilog"; + args[1] = "-defer"; + } + Pass::call(design, args); + return; + } + + if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv" || args[1] == "-formal") { + if (use_verific) { + args[0] = "verific"; + } else { + args[0] = "read_verilog"; + if (args[1] == "-formal") + args.insert(args.begin()+1, std::string()); + args[1] = "-sv"; + args.insert(args.begin()+1, "-defer"); + } + Pass::call(design, args); + return; + } + + if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl") { + if (use_verific) { + args[0] = "verific"; + Pass::call(design, args); + } else { + log_cmd_error("This version of Yosys is built without Verific support.\n"); + } + return; + } + + if (args[1] == "-define") { + if (use_verific) { + args[0] = "verific"; + args[1] = "-vlog-define"; + Pass::call(design, args); + } + args[0] = "verilog_defines"; + args.erase(args.begin()+1, args.begin()+2); + for (int i = 1; i < GetSize(args); i++) + args[i] = "-D" + args[i]; + Pass::call(design, args); + return; + } + if (args[1] == "-undef") { + if (use_verific) { + args[0] = "verific"; + args[1] = "-vlog-undef"; + Pass::call(design, args); + } + args[0] = "verilog_defines"; + args.erase(args.begin()+1, args.begin()+2); + for (int i = 1; i < GetSize(args); i++) + args[i] = "-U" + args[i]; + Pass::call(design, args); + return; + } + + if (args[1] == "-incdir") { + if (use_verific) { + args[0] = "verific"; + args[1] = "-vlog-incdir"; + Pass::call(design, args); + } + args[0] = "verilog_defaults"; + args[1] = "-add"; + for (int i = 2; i < GetSize(args); i++) + args[i] = "-I" + args[i]; + Pass::call(design, args); + return; + } + + log_cmd_error("Missing or unsupported mode parameter.\n"); + } +} ReadPass; + +PRIVATE_NAMESPACE_END diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h new file mode 100644 index 000000000..2ccfcd42c --- /dev/null +++ b/frontends/verific/verific.h @@ -0,0 +1,109 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> + * + * 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 int verific_verbose; + +extern bool verific_import_pending; +extern void verific_import(Design *design, const std::map<std::string,std::string> ¶meters, std::string top = std::string()); + +extern pool<int> verific_sva_prims; + +struct VerificImporter; + +struct VerificClocking { + RTLIL::Module *module = nullptr; + Verific::Net *clock_net = nullptr; + Verific::Net *enable_net = nullptr; + Verific::Net *disable_net = nullptr; + Verific::Net *body_net = nullptr; + Verific::Net *cond_net = nullptr; + SigBit clock_sig = State::Sx; + SigBit enable_sig = State::S1; + SigBit disable_sig = State::S0; + bool posedge = true; + bool gclk = false; + + VerificClocking() { } + VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false); + RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const()); + RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value); + RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q); + + bool property_matches_sequence(const VerificClocking &seq) const { + if (clock_net != seq.clock_net) + return false; + if (enable_net != seq.enable_net) + return false; + if (posedge != seq.posedge) + return false; + return true; + } +}; + +struct VerificImporter +{ + RTLIL::Module *module; + Verific::Netlist *netlist; + + std::map<Verific::Net*, RTLIL::SigBit> net_map; + std::map<Verific::Net*, Verific::Net*> sva_posedge_map; + pool<Verific::Net*, hash_ptr_ops> any_all_nets; + + bool mode_gates, mode_keep, mode_nosva, mode_names, mode_verific; + bool mode_autocover, mode_fullinit; + + VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit); + + RTLIL::SigBit net_map_at(Verific::Net *net); + + RTLIL::IdString new_verific_id(Verific::DesignObj *obj); + void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &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, const pool<Verific::Net*, hash_ptr_ops> *any_all_nets = nullptr); + + 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<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol); + void merge_past_ffs(pool<RTLIL::Cell*> &candidates); + + void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set<Verific::Netlist*> &nl_todo, bool norename = false); +}; + +void verific_import_sva_assert(VerificImporter *importer, Verific::Instance *inst); +void verific_import_sva_assume(VerificImporter *importer, Verific::Instance *inst); +void verific_import_sva_cover(VerificImporter *importer, Verific::Instance *inst); +void verific_import_sva_trigger(VerificImporter *importer, Verific::Instance *inst); +bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net); + +extern int verific_sva_fsm_limit; + +YOSYS_NAMESPACE_END + +#endif diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc new file mode 100644 index 000000000..49c0c40ac --- /dev/null +++ b/frontends/verific/verificsva.cc @@ -0,0 +1,1860 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> + * + * 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. + * + */ + + +// Currently supported SVA sequence and property syntax: +// http://symbiyosys.readthedocs.io/en/latest/verific.html +// +// Next gen property syntax: +// basic_property +// [antecedent_condition] property +// [antecedent_condition] always.. property +// [antecedent_condition] eventually.. basic_property +// [antecedent_condition] property until.. expression +// [antecedent_condition] basic_property until.. basic_property (assert/assume only) +// +// antecedent_condition: +// sequence |-> +// sequence |=> +// +// basic_property: +// sequence +// not basic_property +// nexttime basic_property +// nexttime[N] basic_property +// sequence #-# basic_property +// sequence #=# basic_property +// basic_property or basic_property (cover only) +// basic_property and basic_property (assert/assume only) +// basic_property implies basic_property +// basic_property iff basic_property +// +// sequence: +// expression +// sequence ##N sequence +// sequence ##[*] sequence +// sequence ##[+] sequence +// sequence ##[N:M] sequence +// sequence ##[N:$] sequence +// expression [*] +// expression [+] +// expression [*N] +// expression [*N:M] +// expression [*N:$] +// sequence or sequence +// sequence and sequence +// expression throughout sequence +// sequence intersect sequence +// sequence within sequence +// first_match( sequence ) +// expression [=N] +// expression [=N:M] +// expression [=N:$] +// expression [->N] +// expression [->N:M] +// expression [->N:$] + + +#include "kernel/yosys.h" +#include "frontends/verific/verific.h" + +USING_YOSYS_NAMESPACE + +#ifdef VERIFIC_NAMESPACE +using namespace Verific; +#endif + +PRIVATE_NAMESPACE_BEGIN + +// Non-deterministic FSM +struct SvaNFsmNode +{ + // Edge: Activate the target node if ctrl signal is true, consumes clock cycle + // Link: Activate the target node if ctrl signal is true, doesn't consume clock cycle + vector<pair<int, SigBit>> edges, links; + bool is_cond_node; +}; + +// Non-deterministic FSM after resolving links +struct SvaUFsmNode +{ + // Edge: Activate the target node if all bits in ctrl signal are true, consumes clock cycle + // Accept: This node functions as an accept node if all bits in ctrl signal are true + vector<pair<int, SigSpec>> edges; + vector<SigSpec> accept, cond; + bool reachable; +}; + +// Deterministic FSM +struct SvaDFsmNode +{ + // A DFSM state corresponds to a set of NFSM states. We represent DFSM states as sorted vectors + // of NFSM state node ids. Edge/accept controls are constants matched against the ctrl sigspec. + SigSpec ctrl; + vector<pair<vector<int>, Const>> edges; + vector<Const> accept, reject; + + // additional temp data for getReject() + Wire *ffoutwire; + SigBit statesig; + SigSpec nextstate; + + // additional temp data for getDFsm() + int outnode; +}; + +struct SvaFsm +{ + Module *module; + VerificClocking clocking; + + SigBit trigger_sig = State::S1, disable_sig; + SigBit throughout_sig = State::S1; + bool in_cond_mode = false; + + vector<SigBit> disable_stack; + vector<SigBit> throughout_stack; + + int startNode, acceptNode, condNode; + vector<SvaNFsmNode> nodes; + + vector<SvaUFsmNode> unodes; + dict<vector<int>, SvaDFsmNode> dnodes; + dict<pair<SigSpec, SigSpec>, SigBit> cond_eq_cache; + bool materialized = false; + + SigBit final_accept_sig = State::Sx; + SigBit final_reject_sig = State::Sx; + + SvaFsm(const VerificClocking &clking, SigBit trig = State::S1) + { + module = clking.module; + clocking = clking; + trigger_sig = trig; + + startNode = createNode(); + acceptNode = createNode(); + + in_cond_mode = true; + condNode = createNode(); + in_cond_mode = false; + } + + void pushDisable(SigBit sig) + { + log_assert(!materialized); + + disable_stack.push_back(disable_sig); + + if (disable_sig == State::S0) + disable_sig = sig; + else + disable_sig = module->Or(NEW_ID, disable_sig, sig); + } + + void popDisable() + { + log_assert(!materialized); + log_assert(!disable_stack.empty()); + + disable_sig = disable_stack.back(); + disable_stack.pop_back(); + } + + void pushThroughout(SigBit sig) + { + log_assert(!materialized); + + throughout_stack.push_back(throughout_sig); + + if (throughout_sig == State::S1) + throughout_sig = sig; + else + throughout_sig = module->And(NEW_ID, throughout_sig, sig); + } + + void popThroughout() + { + log_assert(!materialized); + log_assert(!throughout_stack.empty()); + + throughout_sig = throughout_stack.back(); + throughout_stack.pop_back(); + } + + int createNode(int link_node = -1) + { + log_assert(!materialized); + + int idx = GetSize(nodes); + nodes.push_back(SvaNFsmNode()); + nodes.back().is_cond_node = in_cond_mode; + if (link_node >= 0) + createLink(link_node, idx); + return idx; + } + + int createStartNode() + { + return createNode(startNode); + } + + void createEdge(int from_node, int to_node, SigBit ctrl = State::S1) + { + log_assert(!materialized); + log_assert(0 <= from_node && from_node < GetSize(nodes)); + log_assert(0 <= to_node && to_node < GetSize(nodes)); + log_assert(from_node != acceptNode); + log_assert(to_node != acceptNode); + log_assert(from_node != condNode); + log_assert(to_node != condNode); + log_assert(to_node != startNode); + + if (from_node != startNode) + log_assert(nodes.at(from_node).is_cond_node == nodes.at(to_node).is_cond_node); + + if (throughout_sig != State::S1) { + if (ctrl != State::S1) + ctrl = module->And(NEW_ID, throughout_sig, ctrl); + else + ctrl = throughout_sig; + } + + nodes[from_node].edges.push_back(make_pair(to_node, ctrl)); + } + + void createLink(int from_node, int to_node, SigBit ctrl = State::S1) + { + log_assert(!materialized); + log_assert(0 <= from_node && from_node < GetSize(nodes)); + log_assert(0 <= to_node && to_node < GetSize(nodes)); + log_assert(from_node != acceptNode); + log_assert(from_node != condNode); + log_assert(to_node != startNode); + + if (from_node != startNode) + log_assert(nodes.at(from_node).is_cond_node == nodes.at(to_node).is_cond_node); + + if (throughout_sig != State::S1) { + if (ctrl != State::S1) + ctrl = module->And(NEW_ID, throughout_sig, ctrl); + else + ctrl = throughout_sig; + } + + nodes[from_node].links.push_back(make_pair(to_node, ctrl)); + } + + void make_link_order(vector<int> &order, int node, int min) + { + order[node] = std::max(order[node], min); + for (auto &it : nodes[node].links) + make_link_order(order, it.first, order[node]+1); + } + + // ---------------------------------------------------- + // Generating NFSM circuit to acquire accept signal + + SigBit getAccept() + { + log_assert(!materialized); + materialized = true; + + vector<Wire*> state_wire(GetSize(nodes)); + vector<SigBit> state_sig(GetSize(nodes)); + vector<SigBit> next_state_sig(GetSize(nodes)); + + // Create state signals + + { + SigBit not_disable = State::S1; + + if (disable_sig != State::S0) + not_disable = module->Not(NEW_ID, disable_sig); + + for (int i = 0; i < GetSize(nodes); i++) + { + Wire *w = module->addWire(NEW_ID); + state_wire[i] = w; + state_sig[i] = w; + + if (i == startNode) + state_sig[i] = module->Or(NEW_ID, state_sig[i], trigger_sig); + + if (disable_sig != State::S0) + state_sig[i] = module->And(NEW_ID, state_sig[i], not_disable); + } + } + + // Follow Links + + { + vector<int> node_order(GetSize(nodes)); + vector<vector<int>> order_to_nodes; + + for (int i = 0; i < GetSize(nodes); i++) + make_link_order(node_order, i, 0); + + for (int i = 0; i < GetSize(nodes); i++) { + if (node_order[i] >= GetSize(order_to_nodes)) + order_to_nodes.resize(node_order[i]+1); + order_to_nodes[node_order[i]].push_back(i); + } + + for (int order = 0; order < GetSize(order_to_nodes); order++) + for (int node : order_to_nodes[order]) + { + for (auto &it : nodes[node].links) + { + int target = it.first; + SigBit ctrl = state_sig[node]; + + if (it.second != State::S1) + ctrl = module->And(NEW_ID, ctrl, it.second); + + state_sig[target] = module->Or(NEW_ID, state_sig[target], ctrl); + } + } + } + + // Construct activations + + { + vector<SigSpec> activate_sig(GetSize(nodes)); + vector<SigBit> activate_bit(GetSize(nodes)); + + for (int i = 0; i < GetSize(nodes); i++) { + for (auto &it : nodes[i].edges) + activate_sig[it.first].append(module->And(NEW_ID, state_sig[i], it.second)); + } + + for (int i = 0; i < GetSize(nodes); i++) { + if (GetSize(activate_sig[i]) == 0) + next_state_sig[i] = State::S0; + else if (GetSize(activate_sig[i]) == 1) + next_state_sig[i] = activate_sig[i]; + else + next_state_sig[i] = module->ReduceOr(NEW_ID, activate_sig[i]); + } + } + + // Create state FFs + + for (int i = 0; i < GetSize(nodes); i++) + { + if (next_state_sig[i] != State::S0) { + clocking.addDff(NEW_ID, next_state_sig[i], state_wire[i], State::S0); + } else { + module->connect(state_wire[i], State::S0); + } + } + + final_accept_sig = state_sig[acceptNode]; + return final_accept_sig; + } + + // ---------------------------------------------------- + // Generating quantifier-based NFSM circuit to acquire reject signal + + SigBit getAnyAllRejectWorker(bool /* allMode */) + { + // FIXME + log_abort(); + } + + SigBit getAnyReject() + { + return getAnyAllRejectWorker(false); + } + + SigBit getAllReject() + { + return getAnyAllRejectWorker(true); + } + + // ---------------------------------------------------- + // Generating DFSM circuit to acquire reject signal + + void node_to_unode(int node, int unode, SigSpec ctrl) + { + if (node == acceptNode) + unodes[unode].accept.push_back(ctrl); + + if (node == condNode) + unodes[unode].cond.push_back(ctrl); + + for (auto &it : nodes[node].edges) { + if (it.second != State::S1) { + SigSpec s = {ctrl, it.second}; + s.sort_and_unify(); + unodes[unode].edges.push_back(make_pair(it.first, s)); + } else { + unodes[unode].edges.push_back(make_pair(it.first, ctrl)); + } + } + + for (auto &it : nodes[node].links) { + if (it.second != State::S1) { + SigSpec s = {ctrl, it.second}; + s.sort_and_unify(); + node_to_unode(it.first, unode, s); + } else { + node_to_unode(it.first, unode, ctrl); + } + } + } + + void mark_reachable_unode(int unode) + { + if (unodes[unode].reachable) + return; + + unodes[unode].reachable = true; + for (auto &it : unodes[unode].edges) + mark_reachable_unode(it.first); + } + + void usortint(vector<int> &vec) + { + vector<int> newvec; + std::sort(vec.begin(), vec.end()); + for (int i = 0; i < GetSize(vec); i++) + if (i == GetSize(vec)-1 || vec[i] != vec[i+1]) + newvec.push_back(vec[i]); + vec.swap(newvec); + } + + bool cmp_ctrl(const pool<SigBit> &ctrl_bits, const SigSpec &ctrl) + { + for (int i = 0; i < GetSize(ctrl); i++) + if (ctrl_bits.count(ctrl[i]) == 0) + return false; + return true; + } + + void create_dnode(const vector<int> &state, bool firstmatch, bool condaccept) + { + if (dnodes.count(state) != 0) + return; + + SvaDFsmNode dnode; + dnodes[state] = SvaDFsmNode(); + + for (int unode : state) { + log_assert(unodes[unode].reachable); + for (auto &it : unodes[unode].edges) + dnode.ctrl.append(it.second); + for (auto &it : unodes[unode].accept) + dnode.ctrl.append(it); + for (auto &it : unodes[unode].cond) + dnode.ctrl.append(it); + } + + dnode.ctrl.sort_and_unify(); + + if (GetSize(dnode.ctrl) > verific_sva_fsm_limit) { + if (verific_verbose >= 2) { + log(" detected state explosion in DFSM generation:\n"); + dump(); + log(" ctrl signal: %s\n", log_signal(dnode.ctrl)); + } + log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n", + GetSize(dnode.ctrl), verific_sva_fsm_limit); + } + + for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++) + { + Const ctrl_val(i, GetSize(dnode.ctrl)); + pool<SigBit> ctrl_bits; + + for (int i = 0; i < GetSize(dnode.ctrl); i++) + if (ctrl_val[i] == State::S1) + ctrl_bits.insert(dnode.ctrl[i]); + + vector<int> new_state; + bool accept = false, cond = false; + + for (int unode : state) { + for (auto &it : unodes[unode].accept) + if (cmp_ctrl(ctrl_bits, it)) + accept = true; + for (auto &it : unodes[unode].cond) + if (cmp_ctrl(ctrl_bits, it)) + cond = true; + } + + bool new_state_cond = false; + bool new_state_noncond = false; + + if (accept && condaccept) + accept = cond; + + if (!accept || !firstmatch) { + for (int unode : state) + for (auto &it : unodes[unode].edges) + if (cmp_ctrl(ctrl_bits, it.second)) { + if (nodes.at(it.first).is_cond_node) + new_state_cond = true; + else + new_state_noncond = true; + new_state.push_back(it.first); + } + } + + if (accept) + dnode.accept.push_back(ctrl_val); + + if (condaccept && (!new_state_cond || !new_state_noncond)) + new_state.clear(); + + if (new_state.empty()) { + if (!accept) + dnode.reject.push_back(ctrl_val); + } else { + usortint(new_state); + dnode.edges.push_back(make_pair(new_state, ctrl_val)); + create_dnode(new_state, firstmatch, condaccept); + } + } + + dnodes[state] = dnode; + } + + void optimize_cond(vector<Const> &values) + { + bool did_something = true; + + while (did_something) + { + did_something = false; + + for (int i = 0; i < GetSize(values); i++) + for (int j = 0; j < GetSize(values); j++) + { + if (i == j) + continue; + + log_assert(GetSize(values[i]) == GetSize(values[j])); + + int delta_pos = -1; + bool i_within_j = true; + bool j_within_i = true; + + for (int k = 0; k < GetSize(values[i]); k++) { + if (values[i][k] == State::Sa && values[j][k] != State::Sa) { + i_within_j = false; + continue; + } + if (values[i][k] != State::Sa && values[j][k] == State::Sa) { + j_within_i = false; + continue; + } + if (values[i][k] == values[j][k]) + continue; + if (delta_pos >= 0) + goto next_pair; + delta_pos = k; + } + + if (delta_pos >= 0 && i_within_j && j_within_i) { + did_something = true; + values[i][delta_pos] = State::Sa; + values[j] = values.back(); + values.pop_back(); + goto next_pair; + } + + if (delta_pos < 0 && i_within_j) { + did_something = true; + values[i] = values.back(); + values.pop_back(); + goto next_pair; + } + + if (delta_pos < 0 && j_within_i) { + did_something = true; + values[j] = values.back(); + values.pop_back(); + goto next_pair; + } + next_pair:; + } + } + } + + SigBit make_cond_eq(const SigSpec &ctrl, const Const &value, SigBit enable = State::S1) + { + SigSpec sig_a, sig_b; + + log_assert(GetSize(ctrl) == GetSize(value)); + + for (int i = 0; i < GetSize(ctrl); i++) + if (value[i] != State::Sa) { + sig_a.append(ctrl[i]); + sig_b.append(value[i]); + } + + if (GetSize(sig_a) == 0) + return enable; + + if (enable != State::S1) { + sig_a.append(enable); + sig_b.append(State::S1); + } + + auto key = make_pair(sig_a, sig_b); + + if (cond_eq_cache.count(key) == 0) + { + if (sig_b == State::S1) + cond_eq_cache[key] = sig_a; + else if (sig_b == State::S0) + cond_eq_cache[key] = module->Not(NEW_ID, sig_a); + else + cond_eq_cache[key] = module->Eq(NEW_ID, sig_a, sig_b); + + if (verific_verbose >= 2) { + log(" Cond: %s := %s == %s\n", log_signal(cond_eq_cache[key]), + log_signal(sig_a), log_signal(sig_b)); + } + } + + return cond_eq_cache.at(key); + } + + void getFirstAcceptReject(SigBit *accept_p, SigBit *reject_p) + { + log_assert(!materialized); + materialized = true; + + // Create unlinked NFSM + + unodes.resize(GetSize(nodes)); + + for (int node = 0; node < GetSize(nodes); node++) + node_to_unode(node, node, SigSpec()); + + mark_reachable_unode(startNode); + + // Create DFSM + + create_dnode(vector<int>{startNode}, true, false); + dnodes.sort(); + + // Create DFSM Circuit + + SigSpec accept_sig, reject_sig; + + for (auto &it : dnodes) + { + SvaDFsmNode &dnode = it.second; + dnode.ffoutwire = module->addWire(NEW_ID); + dnode.statesig = dnode.ffoutwire; + + if (it.first == vector<int>{startNode}) + dnode.statesig = module->Or(NEW_ID, dnode.statesig, trigger_sig); + } + + for (auto &it : dnodes) + { + SvaDFsmNode &dnode = it.second; + dict<vector<int>, vector<Const>> edge_cond; + + for (auto &edge : dnode.edges) + edge_cond[edge.first].push_back(edge.second); + + for (auto &it : edge_cond) { + optimize_cond(it.second); + for (auto &value : it.second) + dnodes.at(it.first).nextstate.append(make_cond_eq(dnode.ctrl, value, dnode.statesig)); + } + + if (accept_p) { + vector<Const> accept_cond = dnode.accept; + optimize_cond(accept_cond); + for (auto &value : accept_cond) + accept_sig.append(make_cond_eq(dnode.ctrl, value, dnode.statesig)); + } + + if (reject_p) { + vector<Const> reject_cond = dnode.reject; + optimize_cond(reject_cond); + for (auto &value : reject_cond) + reject_sig.append(make_cond_eq(dnode.ctrl, value, dnode.statesig)); + } + } + + for (auto &it : dnodes) + { + SvaDFsmNode &dnode = it.second; + if (GetSize(dnode.nextstate) == 0) { + module->connect(dnode.ffoutwire, State::S0); + } else + if (GetSize(dnode.nextstate) == 1) { + clocking.addDff(NEW_ID, dnode.nextstate, dnode.ffoutwire, State::S0); + } else { + SigSpec nextstate = module->ReduceOr(NEW_ID, dnode.nextstate); + clocking.addDff(NEW_ID, nextstate, dnode.ffoutwire, State::S0); + } + } + + if (accept_p) + { + if (GetSize(accept_sig) == 0) + final_accept_sig = State::S0; + else if (GetSize(accept_sig) == 1) + final_accept_sig = accept_sig; + else + final_accept_sig = module->ReduceOr(NEW_ID, accept_sig); + *accept_p = final_accept_sig; + } + + if (reject_p) + { + if (GetSize(reject_sig) == 0) + final_reject_sig = State::S0; + else if (GetSize(reject_sig) == 1) + final_reject_sig = reject_sig; + else + final_reject_sig = module->ReduceOr(NEW_ID, reject_sig); + *reject_p = final_reject_sig; + } + } + + SigBit getFirstAccept() + { + SigBit accept; + getFirstAcceptReject(&accept, nullptr); + return accept; + } + + SigBit getReject() + { + SigBit reject; + getFirstAcceptReject(nullptr, &reject); + return reject; + } + + void getDFsm(SvaFsm &output_fsm, int output_start_node, int output_accept_node, int output_reject_node = -1, bool firstmatch = true, bool condaccept = false) + { + log_assert(!materialized); + materialized = true; + + // Create unlinked NFSM + + unodes.resize(GetSize(nodes)); + + for (int node = 0; node < GetSize(nodes); node++) + node_to_unode(node, node, SigSpec()); + + mark_reachable_unode(startNode); + + // Create DFSM + + create_dnode(vector<int>{startNode}, firstmatch, condaccept); + dnodes.sort(); + + // Create DFSM Graph + + for (auto &it : dnodes) + { + SvaDFsmNode &dnode = it.second; + dnode.outnode = output_fsm.createNode(); + + if (it.first == vector<int>{startNode}) + output_fsm.createLink(output_start_node, dnode.outnode); + + if (output_accept_node >= 0) { + vector<Const> accept_cond = dnode.accept; + optimize_cond(accept_cond); + for (auto &value : accept_cond) + output_fsm.createLink(it.second.outnode, output_accept_node, make_cond_eq(dnode.ctrl, value)); + } + + if (output_reject_node >= 0) { + vector<Const> reject_cond = dnode.reject; + optimize_cond(reject_cond); + for (auto &value : reject_cond) + output_fsm.createLink(it.second.outnode, output_reject_node, make_cond_eq(dnode.ctrl, value)); + } + } + + for (auto &it : dnodes) + { + SvaDFsmNode &dnode = it.second; + dict<vector<int>, vector<Const>> edge_cond; + + for (auto &edge : dnode.edges) + edge_cond[edge.first].push_back(edge.second); + + for (auto &it : edge_cond) { + optimize_cond(it.second); + for (auto &value : it.second) + output_fsm.createEdge(dnode.outnode, dnodes.at(it.first).outnode, make_cond_eq(dnode.ctrl, value)); + } + } + } + + // ---------------------------------------------------- + // State dump for verbose log messages + + void dump_nodes() + { + if (nodes.empty()) + return; + + log(" non-deterministic encoding:\n"); + for (int i = 0; i < GetSize(nodes); i++) + { + log(" node %d:%s\n", i, + i == startNode ? " [start]" : + i == acceptNode ? " [accept]" : + i == condNode ? " [cond]" : ""); + + for (auto &it : nodes[i].edges) { + if (it.second != State::S1) + log(" edge %s -> %d\n", log_signal(it.second), it.first); + else + log(" edge -> %d\n", it.first); + } + + for (auto &it : nodes[i].links) { + if (it.second != State::S1) + log(" link %s -> %d\n", log_signal(it.second), it.first); + else + log(" link -> %d\n", it.first); + } + } + } + + void dump_unodes() + { + if (unodes.empty()) + return; + + log(" unlinked non-deterministic encoding:\n"); + for (int i = 0; i < GetSize(unodes); i++) + { + if (!unodes[i].reachable) + continue; + + log(" unode %d:%s\n", i, i == startNode ? " [start]" : ""); + + for (auto &it : unodes[i].edges) { + if (!it.second.empty()) + log(" edge %s -> %d\n", log_signal(it.second), it.first); + else + log(" edge -> %d\n", it.first); + } + + for (auto &ctrl : unodes[i].accept) { + if (!ctrl.empty()) + log(" accept %s\n", log_signal(ctrl)); + else + log(" accept\n"); + } + + for (auto &ctrl : unodes[i].cond) { + if (!ctrl.empty()) + log(" cond %s\n", log_signal(ctrl)); + else + log(" cond\n"); + } + } + } + + void dump_dnodes() + { + if (dnodes.empty()) + return; + + log(" deterministic encoding:\n"); + for (auto &it : dnodes) + { + log(" dnode {"); + for (int i = 0; i < GetSize(it.first); i++) + log("%s%d", i ? "," : "", it.first[i]); + log("}:%s\n", GetSize(it.first) == 1 && it.first[0] == startNode ? " [start]" : ""); + + log(" ctrl %s\n", log_signal(it.second.ctrl)); + + for (auto &edge : it.second.edges) { + log(" edge %s -> {", log_signal(edge.second)); + for (int i = 0; i < GetSize(edge.first); i++) + log("%s%d", i ? "," : "", edge.first[i]); + log("}\n"); + } + + for (auto &value : it.second.accept) + log(" accept %s\n", log_signal(value)); + + for (auto &value : it.second.reject) + log(" reject %s\n", log_signal(value)); + } + } + + void dump() + { + if (!nodes.empty()) + log(" number of NFSM states: %d\n", GetSize(nodes)); + + if (!unodes.empty()) { + int count = 0; + for (auto &unode : unodes) + if (unode.reachable) + count++; + log(" number of reachable UFSM states: %d\n", count); + } + + if (!dnodes.empty()) + log(" number of DFSM states: %d\n", GetSize(dnodes)); + + if (verific_verbose >= 2) { + dump_nodes(); + dump_unodes(); + dump_dnodes(); + } + + if (trigger_sig != State::S1) + log(" trigger signal: %s\n", log_signal(trigger_sig)); + + if (final_accept_sig != State::Sx) + log(" accept signal: %s\n", log_signal(final_accept_sig)); + + if (final_reject_sig != State::Sx) + log(" reject signal: %s\n", log_signal(final_reject_sig)); + } +}; + +PRIVATE_NAMESPACE_END + +YOSYS_NAMESPACE_BEGIN + +pool<int> verific_sva_prims = { + // Copy&paste from Verific 3.16_484_32_170630 Netlist.h + PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME, + PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH, + PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT, + PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT, + PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND, + PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION, + PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY, + PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT, + PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED, + PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST, + PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF, + PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK, + PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS, + PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL, + PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF, + PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON, + PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF, + PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME, + PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE +}; + +struct VerificSvaImporter +{ + VerificImporter *importer = nullptr; + Module *module = nullptr; + + Netlist *netlist = nullptr; + Instance *root = nullptr; + + VerificClocking clocking; + + bool mode_assert = false; + bool mode_assume = false; + bool mode_cover = false; + bool mode_trigger = 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 || inst->Type() == PRIM_SVA_TRIGGERED) + 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 Importer + + struct ParserErrorException { + }; + + [[noreturn]] void parser_error(std::string errmsg) + { + if (!importer->mode_keep) + log_error("%s", errmsg.c_str()); + log_warning("%s", errmsg.c_str()); + throw ParserErrorException(); + } + + [[noreturn]] void parser_error(std::string errmsg, linefile_type loc) + { + parser_error(stringf("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc))); + } + + [[noreturn]] void parser_error(std::string errmsg, Instance *inst) + { + parser_error(stringf("%s at %s (%s)", errmsg.c_str(), inst->View()->Owner()->Name(), inst->Name()), inst->Linefile()); + } + + [[noreturn]] void parser_error(Instance *inst) + { + parser_error(stringf("Verific SVA primitive %s (%s) is currently unsupported in this context", + inst->View()->Owner()->Name(), inst->Name()), inst->Linefile()); + } + + dict<Net*, bool, hash_ptr_ops> check_expression_cache; + + bool check_expression(Net *net, bool raise_error = false) + { + while (!check_expression_cache.count(net)) + { + Instance *inst = net_to_ast_driver(net); + + if (inst == nullptr) { + check_expression_cache[net] = true; + break; + } + + if (inst->Type() == PRIM_SVA_AT) + { + VerificClocking new_clocking(importer, net); + log_assert(new_clocking.cond_net == nullptr); + if (!clocking.property_matches_sequence(new_clocking)) + parser_error("Mixed clocking is currently not supported", inst); + check_expression_cache[net] = check_expression(new_clocking.body_net, raise_error); + break; + } + + if (inst->Type() == PRIM_SVA_FIRST_MATCH || inst->Type() == PRIM_SVA_NOT) + { + check_expression_cache[net] = check_expression(inst->GetInput(), raise_error); + break; + } + + if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_INTERSECT || + inst->Type() == PRIM_SVA_WITHIN || inst->Type() == PRIM_SVA_THROUGHOUT || + inst->Type() == PRIM_SVA_OR || inst->Type() == PRIM_SVA_AND) + { + check_expression_cache[net] = check_expression(inst->GetInput1(), raise_error) && check_expression(inst->GetInput2(), raise_error); + break; + } + + if (inst->Type() == PRIM_SVA_SEQ_CONCAT) + { + const char *sva_low_s = inst->GetAttValue("sva:low"); + const char *sva_high_s = inst->GetAttValue("sva:high"); + + int sva_low = atoi(sva_low_s); + int sva_high = atoi(sva_high_s); + bool sva_inf = !strcmp(sva_high_s, "$"); + + if (sva_low == 0 && sva_high == 0 && !sva_inf) + check_expression_cache[net] = check_expression(inst->GetInput1(), raise_error) && check_expression(inst->GetInput2(), raise_error); + else + check_expression_cache[net] = false; + break; + } + + check_expression_cache[net] = false; + } + + if (raise_error && !check_expression_cache.at(net)) + parser_error(net_to_ast_driver(net)); + return check_expression_cache.at(net); + } + + SigBit parse_expression(Net *net) + { + check_expression(net, true); + + Instance *inst = net_to_ast_driver(net); + + if (inst == nullptr) { + return importer->net_map_at(net); + } + + if (inst->Type() == PRIM_SVA_AT) + { + VerificClocking new_clocking(importer, net); + log_assert(new_clocking.cond_net == nullptr); + if (!clocking.property_matches_sequence(new_clocking)) + parser_error("Mixed clocking is currently not supported", inst); + return parse_expression(new_clocking.body_net); + } + + if (inst->Type() == PRIM_SVA_FIRST_MATCH) + return parse_expression(inst->GetInput()); + + if (inst->Type() == PRIM_SVA_NOT) + return module->Not(NEW_ID, parse_expression(inst->GetInput())); + + if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_OR) + return module->Or(NEW_ID, parse_expression(inst->GetInput1()), parse_expression(inst->GetInput2())); + + if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND || inst->Type() == PRIM_SVA_INTERSECT || + inst->Type() == PRIM_SVA_WITHIN || inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_SEQ_CONCAT) + return module->And(NEW_ID, parse_expression(inst->GetInput1()), parse_expression(inst->GetInput2())); + + log_abort(); + } + + bool check_zero_consecutive_repeat(Net *net) + { + Instance *inst = net_to_ast_driver(net); + + if (inst == nullptr) + return false; + + if (inst->Type() != PRIM_SVA_CONSECUTIVE_REPEAT) + return false; + + const char *sva_low_s = inst->GetAttValue("sva:low"); + int sva_low = atoi(sva_low_s); + + return sva_low == 0; + } + + int parse_consecutive_repeat(SvaFsm &fsm, int start_node, Net *net, bool add_pre_delay, bool add_post_delay) + { + Instance *inst = net_to_ast_driver(net); + + log_assert(inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT); + + const char *sva_low_s = inst->GetAttValue("sva:low"); + const char *sva_high_s = inst->GetAttValue("sva:high"); + + int sva_low = atoi(sva_low_s); + int sva_high = atoi(sva_high_s); + bool sva_inf = !strcmp(sva_high_s, "$"); + + Net *body_net = inst->GetInput(); + + if (add_pre_delay || add_post_delay) + log_assert(sva_low == 0); + + if (sva_low == 0) { + if (!add_pre_delay && !add_post_delay) + parser_error("Possibly zero-length consecutive repeat must follow or precede a delay of at least one cycle", inst); + sva_low++; + } + + int node = fsm.createNode(start_node); + start_node = node; + + if (add_pre_delay) { + node = fsm.createNode(start_node); + fsm.createEdge(start_node, node); + } + + int prev_node = node; + node = parse_sequence(fsm, node, body_net); + + for (int i = 1; i < sva_low; i++) + { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + + prev_node = node; + node = parse_sequence(fsm, next_node, body_net); + } + + if (sva_inf) + { + log_assert(prev_node >= 0); + fsm.createEdge(node, prev_node); + } + else + { + for (int i = sva_low; i < sva_high; i++) + { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + + prev_node = node; + node = parse_sequence(fsm, next_node, body_net); + + fsm.createLink(prev_node, node); + } + } + + if (add_post_delay) { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + node = next_node; + } + + if (add_pre_delay || add_post_delay) + fsm.createLink(start_node, node); + + return node; + } + + int parse_sequence(SvaFsm &fsm, int start_node, Net *net) + { + if (check_expression(net)) { + int node = fsm.createNode(); + fsm.createLink(start_node, node, parse_expression(net)); + return node; + } + + Instance *inst = net_to_ast_driver(net); + + if (inst->Type() == PRIM_SVA_AT) + { + VerificClocking new_clocking(importer, net); + log_assert(new_clocking.cond_net == nullptr); + if (!clocking.property_matches_sequence(new_clocking)) + parser_error("Mixed clocking is currently not supported", inst); + return parse_sequence(fsm, start_node, new_clocking.body_net); + } + + if (inst->Type() == PRIM_SVA_FIRST_MATCH) + { + SvaFsm match_fsm(clocking); + match_fsm.createLink(parse_sequence(match_fsm, match_fsm.createStartNode(), inst->GetInput()), match_fsm.acceptNode); + + int node = fsm.createNode(); + match_fsm.getDFsm(fsm, start_node, node); + + if (verific_verbose) { + log(" First Match FSM:\n"); + match_fsm.dump(); + } + + return node; + } + + if (inst->Type() == PRIM_SVA_NEXTTIME || inst->Type() == PRIM_SVA_S_NEXTTIME) + { + const char *sva_low_s = inst->GetAttValue("sva:low"); + const char *sva_high_s = inst->GetAttValue("sva:high"); + + int sva_low = atoi(sva_low_s); + int sva_high = atoi(sva_high_s); + log_assert(sva_low == sva_high); + + int node = start_node; + + for (int i = 0; i < sva_low; i++) { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + node = next_node; + } + + return parse_sequence(fsm, node, inst->GetInput()); + } + + if (inst->Type() == PRIM_SVA_SEQ_CONCAT) + { + const char *sva_low_s = inst->GetAttValue("sva:low"); + const char *sva_high_s = inst->GetAttValue("sva:high"); + + int sva_low = atoi(sva_low_s); + int sva_high = atoi(sva_high_s); + bool sva_inf = !strcmp(sva_high_s, "$"); + + int node = -1; + bool past_add_delay = false; + + if (check_zero_consecutive_repeat(inst->GetInput1()) && sva_low > 0) { + node = parse_consecutive_repeat(fsm, start_node, inst->GetInput1(), false, true); + sva_low--, sva_high--; + } else { + node = parse_sequence(fsm, start_node, inst->GetInput1()); + } + + if (check_zero_consecutive_repeat(inst->GetInput2()) && sva_low > 0) { + past_add_delay = true; + sva_low--, sva_high--; + } + + for (int i = 0; i < sva_low; i++) { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + node = next_node; + } + + if (sva_inf) + { + fsm.createEdge(node, node); + } + else + { + for (int i = sva_low; i < sva_high; i++) + { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + fsm.createLink(node, next_node); + node = next_node; + } + } + + if (past_add_delay) + node = parse_consecutive_repeat(fsm, node, inst->GetInput2(), true, false); + else + node = parse_sequence(fsm, node, inst->GetInput2()); + + return node; + } + + if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT) + { + return parse_consecutive_repeat(fsm, start_node, net, false, false); + } + + if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT || inst->Type() == PRIM_SVA_GOTO_REPEAT) + { + const char *sva_low_s = inst->GetAttValue("sva:low"); + const char *sva_high_s = inst->GetAttValue("sva:high"); + + int sva_low = atoi(sva_low_s); + int sva_high = atoi(sva_high_s); + bool sva_inf = !strcmp(sva_high_s, "$"); + + Net *body_net = inst->GetInput(); + int node = fsm.createNode(start_node); + + SigBit cond = parse_expression(body_net); + SigBit not_cond = module->Not(NEW_ID, cond); + + for (int i = 0; i < sva_low; i++) + { + int wait_node = fsm.createNode(); + fsm.createEdge(wait_node, wait_node, not_cond); + + if (i == 0) + fsm.createLink(node, wait_node); + else + fsm.createEdge(node, wait_node); + + int next_node = fsm.createNode(); + fsm.createLink(wait_node, next_node, cond); + + node = next_node; + } + + if (sva_inf) + { + int wait_node = fsm.createNode(); + fsm.createEdge(wait_node, wait_node, not_cond); + fsm.createEdge(node, wait_node); + fsm.createLink(wait_node, node, cond); + } + else + { + for (int i = sva_low; i < sva_high; i++) + { + int wait_node = fsm.createNode(); + fsm.createEdge(wait_node, wait_node, not_cond); + + if (i == 0) + fsm.createLink(node, wait_node); + else + fsm.createEdge(node, wait_node); + + int next_node = fsm.createNode(); + fsm.createLink(wait_node, next_node, cond); + + fsm.createLink(node, next_node); + node = next_node; + } + } + + if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT) + fsm.createEdge(node, node); + + return node; + } + + if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_OR) + { + int node = parse_sequence(fsm, start_node, inst->GetInput1()); + int node2 = parse_sequence(fsm, start_node, inst->GetInput2()); + fsm.createLink(node2, node); + return node; + } + + if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND) + { + SvaFsm fsm1(clocking); + fsm1.createLink(parse_sequence(fsm1, fsm1.createStartNode(), inst->GetInput1()), fsm1.acceptNode); + + SvaFsm fsm2(clocking); + fsm2.createLink(parse_sequence(fsm2, fsm2.createStartNode(), inst->GetInput2()), fsm2.acceptNode); + + SvaFsm combined_fsm(clocking); + fsm1.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode); + fsm2.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode); + + int node = fsm.createNode(); + combined_fsm.getDFsm(fsm, start_node, -1, node); + + if (verific_verbose) + { + log(" Left And FSM:\n"); + fsm1.dump(); + + log(" Right And FSM:\n"); + fsm1.dump(); + + log(" Combined And FSM:\n"); + combined_fsm.dump(); + } + + return node; + } + + if (inst->Type() == PRIM_SVA_INTERSECT || inst->Type() == PRIM_SVA_WITHIN) + { + SvaFsm intersect_fsm(clocking); + + if (inst->Type() == PRIM_SVA_INTERSECT) + { + intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.createStartNode(), inst->GetInput1()), intersect_fsm.acceptNode); + } + else + { + int n = intersect_fsm.createNode(); + intersect_fsm.createLink(intersect_fsm.createStartNode(), n); + intersect_fsm.createEdge(n, n); + + n = parse_sequence(intersect_fsm, n, inst->GetInput1()); + + intersect_fsm.createLink(n, intersect_fsm.acceptNode); + intersect_fsm.createEdge(n, n); + } + + intersect_fsm.in_cond_mode = true; + intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.createStartNode(), inst->GetInput2()), intersect_fsm.condNode); + intersect_fsm.in_cond_mode = false; + + int node = fsm.createNode(); + intersect_fsm.getDFsm(fsm, start_node, node, -1, false, true); + + if (verific_verbose) { + log(" Intersect FSM:\n"); + intersect_fsm.dump(); + } + + return node; + } + + if (inst->Type() == PRIM_SVA_THROUGHOUT) + { + SigBit expr = parse_expression(inst->GetInput1()); + + fsm.pushThroughout(expr); + int node = parse_sequence(fsm, start_node, inst->GetInput2()); + fsm.popThroughout(); + + return node; + } + + parser_error(inst); + } + + void get_fsm_accept_reject(SvaFsm &fsm, SigBit *accept_p, SigBit *reject_p, bool swap_accept_reject = false) + { + log_assert(accept_p != nullptr || reject_p != nullptr); + + if (swap_accept_reject) + get_fsm_accept_reject(fsm, reject_p, accept_p); + else if (reject_p == nullptr) + *accept_p = fsm.getAccept(); + else if (accept_p == nullptr) + *reject_p = fsm.getReject(); + else + fsm.getFirstAcceptReject(accept_p, reject_p); + } + + bool eventually_property(Net *&net, SigBit &trig) + { + Instance *inst = net_to_ast_driver(net); + + if (inst == nullptr) + return false; + + if (clocking.cond_net != nullptr) + trig = importer->net_map_at(clocking.cond_net); + else + trig = State::S1; + + if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY) + { + if (mode_cover || mode_trigger) + parser_error(inst); + + net = inst->GetInput(); + clocking.cond_net = nullptr; + + return true; + } + + if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION || + inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) + { + Net *antecedent_net = inst->GetInput1(); + Net *consequent_net = inst->GetInput2(); + + Instance *consequent_inst = net_to_ast_driver(consequent_net); + + if (consequent_inst == nullptr) + return false; + + if (consequent_inst->Type() != PRIM_SVA_S_EVENTUALLY && consequent_inst->Type() != PRIM_SVA_EVENTUALLY) + return false; + + if (mode_cover || mode_trigger) + parser_error(consequent_inst); + + int node; + + SvaFsm antecedent_fsm(clocking, trig); + node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net); + if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { + int next_node = antecedent_fsm.createNode(); + antecedent_fsm.createEdge(node, next_node); + node = next_node; + } + antecedent_fsm.createLink(node, antecedent_fsm.acceptNode); + + trig = antecedent_fsm.getAccept(); + net = consequent_inst->GetInput(); + clocking.cond_net = nullptr; + + if (verific_verbose) { + log(" Eventually Antecedent FSM:\n"); + antecedent_fsm.dump(); + } + + return true; + } + + return false; + } + + void parse_property(Net *net, SigBit *accept_p, SigBit *reject_p) + { + Instance *inst = net_to_ast_driver(net); + + SigBit trig = State::S1; + + if (clocking.cond_net != nullptr) + trig = importer->net_map_at(clocking.cond_net); + + if (inst == nullptr) + { + log_assert(trig == State::S1); + + if (accept_p != nullptr) + *accept_p = importer->net_map_at(net); + if (reject_p != nullptr) + *reject_p = module->Not(NEW_ID, importer->net_map_at(net)); + } + else + if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION || + inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) + { + Net *antecedent_net = inst->GetInput1(); + Net *consequent_net = inst->GetInput2(); + int node; + + SvaFsm antecedent_fsm(clocking, trig); + node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net); + if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { + int next_node = antecedent_fsm.createNode(); + antecedent_fsm.createEdge(node, next_node); + node = next_node; + } + + Instance *consequent_inst = net_to_ast_driver(consequent_net); + + if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL || + consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH || + consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS)) + { + bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH; + + Net *until_net = nullptr; + if (consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS) + { + consequent_net = consequent_inst->GetInput(); + consequent_inst = net_to_ast_driver(consequent_net); + } + else + { + until_net = consequent_inst->GetInput2(); + consequent_net = consequent_inst->GetInput1(); + consequent_inst = net_to_ast_driver(consequent_net); + } + + SigBit until_sig = until_net ? parse_expression(until_net) : RTLIL::S0; + SigBit not_until_sig = module->Not(NEW_ID, until_sig); + antecedent_fsm.createEdge(node, node, not_until_sig); + + antecedent_fsm.createLink(node, antecedent_fsm.acceptNode, until_with ? State::S1 : not_until_sig); + } + else + { + antecedent_fsm.createLink(node, antecedent_fsm.acceptNode); + } + + SigBit antecedent_match = antecedent_fsm.getAccept(); + + if (verific_verbose) { + log(" Antecedent FSM:\n"); + antecedent_fsm.dump(); + } + + bool consequent_not = false; + if (consequent_inst && consequent_inst->Type() == PRIM_SVA_NOT) { + consequent_not = true; + consequent_net = consequent_inst->GetInput(); + consequent_inst = net_to_ast_driver(consequent_net); + } + + SvaFsm consequent_fsm(clocking, antecedent_match); + node = parse_sequence(consequent_fsm, consequent_fsm.createStartNode(), consequent_net); + consequent_fsm.createLink(node, consequent_fsm.acceptNode); + + get_fsm_accept_reject(consequent_fsm, accept_p, reject_p, consequent_not); + + if (verific_verbose) { + log(" Consequent FSM:\n"); + consequent_fsm.dump(); + } + } + else + { + bool prop_not = inst->Type() == PRIM_SVA_NOT; + if (prop_not) { + net = inst->GetInput(); + inst = net_to_ast_driver(net); + } + + SvaFsm fsm(clocking, trig); + int node = parse_sequence(fsm, fsm.createStartNode(), net); + fsm.createLink(node, fsm.acceptNode); + + get_fsm_accept_reject(fsm, accept_p, reject_p, prop_not); + + if (verific_verbose) { + log(" Sequence FSM:\n"); + fsm.dump(); + } + } + } + + void import() + { + try + { + module = importer->module; + netlist = root->Owner(); + + if (verific_verbose) + log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(), + LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile())); + + bool is_user_declared = root->IsUserDeclared(); + + // FIXME + if (!is_user_declared) { + const char *name = root->Name(); + for (int i = 0; name[i]; i++) { + if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) { + is_user_declared = true; + break; + } + } + } + + RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID); + + // parse SVA sequence into trigger signal + + clocking = VerificClocking(importer, root->GetInput(), true); + SigBit accept_bit = State::S0, reject_bit = State::S0; + + if (clocking.body_net == nullptr) + { + if (clocking.clock_net != nullptr || clocking.enable_net != nullptr || clocking.disable_net != nullptr || clocking.cond_net != nullptr) + parser_error(stringf("Failed to parse SVA clocking"), root); + + if (mode_assert || mode_assume) { + reject_bit = module->Not(NEW_ID, parse_expression(root->GetInput())); + } else { + accept_bit = parse_expression(root->GetInput()); + } + } + else + { + Net *net = clocking.body_net; + SigBit trig; + + if (eventually_property(net, trig)) + { + SigBit sig_a, sig_en = trig; + parse_property(net, &sig_a, nullptr); + + // add final FF stage + + SigBit sig_a_q, sig_en_q; + + if (clocking.body_net == nullptr) { + sig_a_q = sig_a; + sig_en_q = sig_en; + } else { + sig_a_q = module->addWire(NEW_ID); + sig_en_q = module->addWire(NEW_ID); + clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0); + clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0); + } + + // generate fair/live cell + + RTLIL::Cell *c = nullptr; + + if (mode_assert) c = module->addLive(root_name, sig_a_q, sig_en_q); + if (mode_assume) c = module->addFair(root_name, sig_a_q, sig_en_q); + + importer->import_attributes(c->attributes, root); + + return; + } + else + { + if (mode_assert || mode_assume) { + parse_property(net, nullptr, &reject_bit); + } else { + parse_property(net, &accept_bit, nullptr); + } + } + } + + if (mode_trigger) + { + module->connect(importer->net_map_at(root->GetOutput()), accept_bit); + } + else + { + SigBit sig_a = module->Not(NEW_ID, reject_bit); + SigBit sig_en = module->Or(NEW_ID, accept_bit, reject_bit); + + // add final FF stage + + SigBit sig_a_q, sig_en_q; + + if (clocking.body_net == nullptr) { + sig_a_q = sig_a; + sig_en_q = sig_en; + } else { + sig_a_q = module->addWire(NEW_ID); + sig_en_q = module->addWire(NEW_ID); + clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0); + clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0); + } + + // generate assert/assume/cover cell + + RTLIL::Cell *c = nullptr; + + if (mode_assert) c = module->addAssert(root_name, sig_a_q, sig_en_q); + if (mode_assume) c = module->addAssume(root_name, sig_a_q, sig_en_q); + if (mode_cover) c = module->addCover(root_name, sig_a_q, sig_en_q); + + importer->import_attributes(c->attributes, root); + } + } + catch (ParserErrorException) + { + } + } +}; + +void verific_import_sva_assert(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_assert = true; + worker.import(); +} + +void verific_import_sva_assume(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_assume = true; + worker.import(); +} + +void verific_import_sva_cover(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_cover = true; + worker.import(); +} + +void verific_import_sva_trigger(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_trigger = true; + worker.import(); +} + +bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net) +{ + VerificSvaImporter worker; + worker.importer = importer; + return worker.net_to_ast_driver(net) != nullptr; +} + +YOSYS_NAMESPACE_END |