diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 5 | ||||
| -rw-r--r-- | frontends/verific/verific.cc | 33 | ||||
| -rw-r--r-- | passes/cmds/show.cc | 7 | ||||
| -rw-r--r-- | passes/opt/opt_ffinv.cc | 4 | ||||
| -rw-r--r-- | passes/techmap/iopadmap.cc | 28 |
6 files changed, 69 insertions, 10 deletions
@@ -129,7 +129,7 @@ LDFLAGS += -rdynamic LDLIBS += -lrt endif -YOSYS_VER := 0.17+72 +YOSYS_VER := 0.17+76 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 14feec30d..3d8a51d8b 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -176,7 +176,10 @@ class SmtIo: self.unroll = False if self.solver == "yices": - if self.noincr or self.forall: + if self.forall: + self.noincr = True + + if self.noincr: self.popen_vargs = ['yices-smt2'] + self.solver_opts else: self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 328593099..a9adb5a17 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -53,6 +53,9 @@ USING_YOSYS_NAMESPACE #include "VhdlUnits.h" #endif +#include "VerificStream.h" +#include "FileSystem.h" + #ifdef YOSYSHQ_VERIFIC_EXTENSIONS #include "InitialAssertions.h" #endif @@ -118,6 +121,34 @@ string get_full_netlist_name(Netlist *nl) return nl->CellBaseName(); } +class YosysStreamCallBackHandler : public VerificStreamCallBackHandler +{ +public: + YosysStreamCallBackHandler() : VerificStreamCallBackHandler() { } + virtual ~YosysStreamCallBackHandler() { } + + virtual verific_stream *GetSysCallStream(const char *file_path) + { + if (!file_path) return nullptr; + + linefile_type src_loc = GetFromLocation(); + + char *this_file_name = nullptr; + if (src_loc && !FileSystem::IsAbsolutePath(file_path)) { + const char *src_file_name = LineFile::GetFileName(src_loc); + char *dir_name = FileSystem::DirectoryPath(src_file_name); + if (dir_name) { + this_file_name = Strings::save(dir_name, "/", file_path); + Strings::free(dir_name); + file_path = this_file_name; + } + } + verific_stream *strm = new verific_ifstream(file_path); + Strings::free(this_file_name); + return strm; + } +}; + // ================================================================== VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) : @@ -2648,6 +2679,8 @@ struct VerificPass : public Pass { int argidx = 1; std::string work = "work"; + YosysStreamCallBackHandler cb; + veri_file::RegisterCallBackVerificStream(&cb); if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" || args[argidx] == "-set-info" || args[argidx] == "-set-ignore")) diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc index 35aa410e4..43deba47b 100644 --- a/passes/cmds/show.cc +++ b/passes/cmds/show.cc @@ -191,7 +191,12 @@ struct ShowWorker std::string str; for (char ch : id) { - if (ch == '\\' || ch == '"') + if (ch == '\\') { + // new graphviz have bug with escaping '\' + str += "╲"; + continue; + } + if (ch == '"') str += "\\"; str += ch; } diff --git a/passes/opt/opt_ffinv.cc b/passes/opt/opt_ffinv.cc index fd76dd2be..fe5b59fa5 100644 --- a/passes/opt/opt_ffinv.cc +++ b/passes/opt/opt_ffinv.cc @@ -72,6 +72,8 @@ struct OptFfInvWorker for (auto &port: q_ports) { if (port.cell == ff.cell && port.port == ID::Q) continue; + if (port.cell == d_inv) + return false; if (port.port != ID::A) return false; if (!port.cell->type.in(ID($not), ID($_NOT_), ID($lut))) @@ -148,6 +150,8 @@ struct OptFfInvWorker for (auto &port: q_ports) { if (port.cell == ff.cell && port.port == ID::Q) continue; + if (port.cell == d_lut) + return false; if (port.port != ID::A) return false; if (port.cell->type.in(ID($not), ID($_NOT_))) { diff --git a/passes/techmap/iopadmap.cc b/passes/techmap/iopadmap.cc index 437ad5156..322eb7779 100644 --- a/passes/techmap/iopadmap.cc +++ b/passes/techmap/iopadmap.cc @@ -240,13 +240,13 @@ struct IopadmapPass : public Pass { for (auto module : design->selected_modules()) { dict<Wire *, dict<int, pair<Cell *, IdString>>> rewrite_bits; - pool<SigSig> remove_conns; + dict<SigSig, pool<int>> remove_conns; if (!toutpad_celltype.empty() || !tinoutpad_celltype.empty()) { dict<SigBit, Cell *> tbuf_bits; pool<SigBit> driven_bits; - dict<SigBit, SigSig> z_conns; + dict<SigBit, std::pair<SigSig, int>> z_conns; // Gather tristate buffers and always-on drivers. for (auto cell : module->cells()) @@ -266,7 +266,7 @@ struct IopadmapPass : public Pass { SigBit dstbit = conn.first[i]; SigBit srcbit = conn.second[i]; if (!srcbit.wire && srcbit.data == State::Sz) { - z_conns[dstbit] = conn; + z_conns[dstbit] = {conn, i}; continue; } driven_bits.insert(dstbit); @@ -317,8 +317,9 @@ struct IopadmapPass : public Pass { // enable. en_sig = SigBit(State::S0); data_sig = SigBit(State::Sx); - if (z_conns.count(wire_bit)) - remove_conns.insert(z_conns[wire_bit]); + auto it = z_conns.find(wire_bit); + if (it != z_conns.end()) + remove_conns[it->second.first].insert(it->second.second); } if (wire->port_input) @@ -477,9 +478,22 @@ struct IopadmapPass : public Pass { if (!remove_conns.empty()) { std::vector<SigSig> new_conns; - for (auto &conn : module->connections()) - if (!remove_conns.count(conn)) + for (auto &conn : module->connections()) { + auto it = remove_conns.find(conn); + if (it == remove_conns.end()) { new_conns.push_back(conn); + } else { + SigSpec lhs, rhs; + for (int i = 0; i < GetSize(conn.first); i++) { + if (!it->second.count(i)) { + lhs.append(conn.first[i]); + rhs.append(conn.second[i]); + } + } + new_conns.push_back(SigSig(lhs, rhs)); + + } + } module->new_connections(new_conns); } |