diff options
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 19 | ||||
| -rw-r--r-- | frontends/verific/Makefile.inc | 1 | ||||
| -rw-r--r-- | frontends/verific/verific.cc | 92 | ||||
| -rw-r--r-- | passes/equiv/equiv_make.cc | 4 |
5 files changed, 81 insertions, 39 deletions
@@ -502,7 +502,7 @@ install: $(TARGETS) $(EXTRA_TARGETS) $(INSTALL_SUDO) mkdir -p $(DESTDIR)$(BINDIR) $(INSTALL_SUDO) cp $(TARGETS) $(DESTDIR)$(BINDIR) ifneq ($(filter yosys,$(TARGETS)),) - $(INSTALL_SUDO) $(STRIP) -d $(DESTDIR)$(BINDIR)/yosys + $(INSTALL_SUDO) $(STRIP) -S $(DESTDIR)$(BINDIR)/yosys endif ifneq ($(filter yosys-abc,$(TARGETS)),) $(INSTALL_SUDO) $(STRIP) $(DESTDIR)$(BINDIR)/yosys-abc @@ -514,7 +514,7 @@ endif $(INSTALL_SUDO) cp -r share/. $(DESTDIR)$(DATDIR)/. ifeq ($(ENABLE_LIBYOSYS),1) $(INSTALL_SUDO) cp libyosys.so $(DESTDIR)$(LIBDIR) - $(INSTALL_SUDO) $(STRIP) -d $(DESTDIR)$(LIBDIR)/libyosys.so + $(INSTALL_SUDO) $(STRIP) -S $(DESTDIR)$(LIBDIR)/libyosys.so $(INSTALL_SUDO) ldconfig endif diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index ec5253205..07bd92265 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -16,7 +16,8 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import sys, subprocess, re, os +import sys, re, os +import resource, subprocess from copy import deepcopy from select import select from time import time @@ -24,6 +25,16 @@ from queue import Queue, Empty from threading import Thread +# This is needed so that the recursive SMT2 S-expression parser +# does not run out of stack frames when parsing large expressions +smtio_reclimit = 64 * 1024 +smtio_stacksize = 128 * 1024 * 1024 +if sys.getrecursionlimit() < smtio_reclimit: + sys.setrecursionlimit(smtio_reclimit) +if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize: + resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1)) + + hex_dict = { "0": "0000", "1": "0001", "2": "0010", "3": "0011", "4": "0100", "5": "0101", "6": "0110", "7": "0111", @@ -150,14 +161,14 @@ class SmtIo: self.setup_done = True + for stmt in self.info_stmts: + self.write(stmt) + if self.produce_models: self.write("(set-option :produce-models true)") self.write("(set-logic %s)" % self.logic) - for stmt in self.info_stmts: - self.write(stmt) - def timestamp(self): secs = int(time() - self.start_time) return "## %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60) diff --git a/frontends/verific/Makefile.inc b/frontends/verific/Makefile.inc index 68ef9aed1..debaac0c5 100644 --- a/frontends/verific/Makefile.inc +++ b/frontends/verific/Makefile.inc @@ -11,6 +11,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/verific.cc b/frontends/verific/verific.cc index 92c7c9e2d..09c379f19 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -719,13 +719,13 @@ struct VerificImporter FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) { - if (inst->Type() == PRIM_SVA_ASSERT) + if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT) asserts.push_back(inst); - if (inst->Type() == PRIM_SVA_ASSUME) + if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) assumes.push_back(inst); - if (inst->Type() == PRIM_SVA_COVER) + if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER) covers.push_back(inst); } @@ -1027,24 +1027,6 @@ struct VerificImporter if (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_ASSERT) { - Net *in = inst->GetInput(); - module->addAssert(NEW_ID, net_map_at(in), State::S1); - continue; - } - - if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) { - Net *in = inst->GetInput(); - module->addAssume(NEW_ID, net_map_at(in), State::S1); - continue; - } - - if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER) { - Net *in = inst->GetInput(); - module->addCover(NEW_ID, net_map_at(in), State::S1); - continue; - } - if (inst->Type() == PRIM_PWR) { module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1); continue; @@ -1131,13 +1113,13 @@ struct VerificImporter continue; } - if (inst->Type() == PRIM_SVA_ASSERT) + if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT) sva_asserts.insert(inst); - if (inst->Type() == PRIM_SVA_ASSUME) + if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) sva_assumes.insert(inst); - if (inst->Type() == PRIM_SVA_COVER) + if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER) sva_covers.insert(inst); if (inst->Type() == OPER_SVA_STABLE && !mode_nosva) @@ -1168,6 +1150,28 @@ struct VerificImporter continue; } + if (inst->Type() == PRIM_SVA_STABLE && !mode_nosva) + { + VerificClockEdge clock_edge(this, inst->GetInput2()->Driver()); + + SigSpec sig_d = net_map_at(inst->GetInput1()); + SigSpec sig_o = net_map_at(inst->GetOutput()); + SigSpec sig_q = module->addWire(NEW_ID); + + if (verbose) { + log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", + log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); + log(" XNOR with A=%s, B=%s, Y=%s.\n", + log_signal(sig_d), log_signal(sig_q), log_signal(sig_o)); + } + + module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge); + module->addXnor(NEW_ID, sig_d, sig_q, sig_o); + + if (!mode_keep) + continue; + } + if (inst->Type() == PRIM_SVA_PAST && !mode_nosva) { VerificClockEdge clock_edge(this, inst->GetInput2()->Driver()); @@ -1336,7 +1340,8 @@ struct VerificSvaPP if (inst == nullptr) return default_net; - if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME) { + if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME || + inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) { Net *new_net = rewrite(get_ast_input(inst)); if (new_net) { inst->Disconnect(inst->View()->GetInput()); @@ -1568,9 +1573,32 @@ struct VerificSvaImporter module = importer->module; netlist = root->Owner(); + RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); + // parse SVA property clock event Instance *at_node = get_ast_input(root); + + // asynchronous immediate assertion/assumption/cover + if (at_node == nullptr && (root->Type() == PRIM_SVA_IMMEDIATE_ASSERT || + root->Type() == PRIM_SVA_IMMEDIATE_COVER || root->Type() == PRIM_SVA_IMMEDIATE_ASSUME)) + { + SigSpec sig_a = importer->net_map_at(root->GetInput()); + RTLIL::Cell *c = nullptr; + + if (eventually) { + if (mode_assert) c = module->addLive(root_name, sig_a, State::S1); + if (mode_assume) c = module->addFair(root_name, sig_a, State::S1); + } else { + if (mode_assert) c = module->addAssert(root_name, sig_a, State::S1); + if (mode_assume) c = module->addAssume(root_name, sig_a, State::S1); + if (mode_cover) c = module->addCover(root_name, sig_a, State::S1); + } + + importer->import_attributes(c->attributes, root); + return; + } + log_assert(at_node && at_node->Type() == PRIM_SVA_AT); VerificClockEdge clock_edge(importer, get_ast_input1(at_node)); @@ -1608,16 +1636,18 @@ struct VerificSvaImporter // generate assert/assume/cover cell - RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); + RTLIL::Cell *c = nullptr; 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 (mode_assert) c = module->addLive(root_name, seq.sig_a, seq.sig_en); + if (mode_assume) c = module->addFair(root_name, seq.sig_a, seq.sig_en); } else { - if (mode_assert) 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); + if (mode_assert) c = module->addAssert(root_name, seq.sig_a, seq.sig_en); + if (mode_assume) c = module->addAssume(root_name, seq.sig_a, seq.sig_en); + if (mode_cover) c = module->addCover(root_name, seq.sig_a, seq.sig_en); } + + importer->import_attributes(c->attributes, root); } }; diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc index 40ca42621..b20463777 100644 --- a/passes/equiv/equiv_make.cc +++ b/passes/equiv/equiv_make.cc @@ -260,11 +260,11 @@ struct EquivMakeWorker for (int i = 0; i < wire->width; i++) { if (undriven_bits.count(assign_map(SigBit(gold_wire, i)))) { - log(" Skipping signal bit %d: undriven on gold side.\n", i); + log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire->name), i); continue; } if (undriven_bits.count(assign_map(SigBit(gate_wire, i)))) { - log(" Skipping signal bit %d: undriven on gate side.\n", i); + log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire->name), i); continue; } equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i)); |