diff options
| -rw-r--r-- | CHANGELOG | 8 | ||||
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | backends/btor/btor.cc | 2 | ||||
| -rw-r--r-- | kernel/fstdata.cc | 38 | ||||
| -rw-r--r-- | kernel/fstdata.h | 2 | ||||
| -rw-r--r-- | manual/command-reference-manual.tex | 44 | ||||
| -rw-r--r-- | passes/memory/memory_share.cc | 2 | ||||
| -rw-r--r-- | passes/opt/opt_mem.cc | 156 | ||||
| -rw-r--r-- | passes/sat/sim.cc | 20 | ||||
| -rw-r--r-- | passes/techmap/abc.cc | 28 | ||||
| -rw-r--r-- | tests/sva/runtest.sh | 7 | ||||
| -rw-r--r-- | tests/techmap/.gitignore | 1 | ||||
| -rw-r--r-- | tests/techmap/mem_simple_4x1_runtest.sh | 16 |
13 files changed, 276 insertions, 54 deletions
@@ -2,9 +2,15 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.16 .. Yosys 0.16-dev +Yosys 0.17 .. Yosys 0.17-dev -------------------------- +Yosys 0.16 .. Yosys 0.17 +-------------------------- + * New commands and options + - Added "write_jny" ( JSON netlist metadata format ) + - Added "tribuf -formal" + * SystemVerilog - Fixed automatic `nosync` inference for local variables in `always_comb` procedures not applying to nested blocks and blocks in functions @@ -129,12 +129,12 @@ LDFLAGS += -rdynamic LDLIBS += -lrt endif -YOSYS_VER := 0.16+63 +YOSYS_VER := 0.17+0 GIT_REV := $(shell git -C $(YOSYS_SRC) rev-parse --short HEAD 2> /dev/null || echo UNKNOWN) OBJS = kernel/version_$(GIT_REV).o bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline b63e0a0.. | wc -l`/;" Makefile + sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 6f9602b.. | wc -l`/;" Makefile # set 'ABCREV = default' to use abc/ as it is # @@ -142,7 +142,7 @@ bumpversion: # is just a symlink to your actual ABC working directory, as 'make mrproper' # will remove the 'abc' directory and you do not want to accidentally # delete your work on ABC.. -ABCREV = 3da9357 +ABCREV = 09a7e6d ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 VERBOSE=$(Q) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 73e88c049..7de5deadd 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1220,6 +1220,8 @@ struct BtorWorker int this_nid = next_nid++; btorf("%d uext %d %d %d%s\n", this_nid, sid, nid, 0, getinfo(wire).c_str()); + if (info_clocks.count(nid)) + info_clocks[this_nid] |= info_clocks[nid]; btorf_pop(stringf("wire %s", log_id(wire))); continue; diff --git a/kernel/fstdata.cc b/kernel/fstdata.cc index 2bec58bcf..fea8ee3c3 100644 --- a/kernel/fstdata.cc +++ b/kernel/fstdata.cc @@ -85,6 +85,13 @@ fstHandle FstData::getHandle(std::string name) { return 0; }; +dict<int,fstHandle> FstData::getMemoryHandles(std::string name) { + if (memory_to_handle.find(name) != memory_to_handle.end()) + return memory_to_handle[name]; + else + return dict<int,fstHandle>(); +}; + static std::string remove_spaces(std::string str) { str.erase(std::remove(str.begin(), str.end(), ' '), str.end()); @@ -126,7 +133,36 @@ void FstData::extractVarNames() } if (clean_name[0]=='\\') clean_name = clean_name.substr(1); - + size_t pos = clean_name.find_last_of("<"); + if (pos != std::string::npos) { + std::string mem_cell = clean_name.substr(0, pos); + std::string addr = clean_name.substr(pos+1); + addr.pop_back(); // remove closing bracket + char *endptr; + int mem_addr = strtol(addr.c_str(), &endptr, 16); + if (*endptr) { + log_warning("Error parsing memory address in : %s\n", clean_name.c_str()); + } else { + memory_to_handle[var.scope+"."+mem_cell][mem_addr] = var.id; + name_to_handle[stringf("%s.%s[%d]",var.scope.c_str(),mem_cell.c_str(),mem_addr)] = h->u.var.handle; + continue; + } + } + pos = clean_name.find_last_of("["); + if (pos != std::string::npos) { + std::string mem_cell = clean_name.substr(0, pos); + std::string addr = clean_name.substr(pos+1); + addr.pop_back(); // remove closing bracket + char *endptr; + int mem_addr = strtol(addr.c_str(), &endptr, 10); + if (*endptr) { + log_warning("Error parsing memory address in : %s\n", clean_name.c_str()); + } else { + memory_to_handle[var.scope+"."+mem_cell][mem_addr] = var.id; + name_to_handle[stringf("%s.%s[%d]",var.scope.c_str(),mem_cell.c_str(),mem_addr)] = h->u.var.handle; + continue; + } + } name_to_handle[var.scope+"."+clean_name] = h->u.var.handle; break; } diff --git a/kernel/fstdata.h b/kernel/fstdata.h index d8dca5fb0..f5cf1d48d 100644 --- a/kernel/fstdata.h +++ b/kernel/fstdata.h @@ -54,6 +54,7 @@ class FstData std::string valueOf(fstHandle signal); fstHandle getHandle(std::string name); + dict<int,fstHandle> getMemoryHandles(std::string name); double getTimescale() { return timescale; } const char *getTimescaleString() { return timescale_str.c_str(); } private: @@ -63,6 +64,7 @@ private: std::vector<FstVar> vars; std::map<fstHandle, FstVar> handle_to_var; std::map<std::string, fstHandle> name_to_handle; + std::map<std::string, dict<int, fstHandle>> memory_to_handle; std::map<fstHandle, std::string> last_data; uint64_t last_time; std::map<fstHandle, std::string> past_data; diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index e68da3318..bafce6de6 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -2592,6 +2592,28 @@ the resulting cells to more sophisticated PAD cells. Tristate PADS (-toutpad, -tinoutpad) always operate in -bits mode. \end{lstlisting} +\section{jny -- write design and metadata} +\label{cmd:jny} +\begin{lstlisting}[numbers=left,frame=single] + jny [options] [selection] + +Write a JSON netlist metadata for the current design + + -o <filename> + write to the specified file. + + -no-connections + Don't include connection information in the netlist output. + + -no-attributes + Don't include attributed information in the netlist output. + + -no-properties + Don't include property information in the netlist output. + +See 'help write_jny' for a description of the JSON format used. +\end{lstlisting} + \section{json -- write design in JSON format} \label{cmd:json} \begin{lstlisting}[numbers=left,frame=single] @@ -7647,6 +7669,11 @@ This pass transforms $mux cells with 'z' inputs to tristate buffers. -logic convert tri-state buffers that do not drive output ports to non-tristate logic. this option implies -merge. + + -formal + convert all tri-state buffers to non-tristate logic and + add a formal assertion that no two buffers are driving the + same net simultaneously. this option implies -merge. \end{lstlisting} \section{uniquify -- create unique copies of modules} @@ -8428,6 +8455,23 @@ a tool for Coarse-Grain Example-Driven Interconnect Synthesis. http://bygone.clairexen.net/intersynth/ \end{lstlisting} +\section{write\_jny -- generate design metadata} +\label{cmd:write_jny} +\begin{lstlisting}[numbers=left,frame=single] + jny [options] [selection] + + -no-connections + Don't include connection information in the netlist output. + + -no-attributes + Don't include attributed information in the netlist output. + + -no-properties + Don't include property information in the netlist output. + +Write a JSON metadata for the current design +\end{lstlisting} + \section{write\_json -- write design to a JSON file} \label{cmd:write_json} \begin{lstlisting}[numbers=left,frame=single] diff --git a/passes/memory/memory_share.cc b/passes/memory/memory_share.cc index 1ddc13f90..5cb11d62b 100644 --- a/passes/memory/memory_share.cc +++ b/passes/memory/memory_share.cc @@ -555,7 +555,7 @@ struct MemorySharePass : public Pass { } break; } - extra_args(args, 1, design); + extra_args(args, argidx, design); MemoryShareWorker msw(design, flag_widen, flag_sat); for (auto module : design->selected_modules()) diff --git a/passes/opt/opt_mem.cc b/passes/opt/opt_mem.cc index edadf2c7b..885b6f97d 100644 --- a/passes/opt/opt_mem.cc +++ b/passes/opt/opt_mem.cc @@ -20,6 +20,7 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" #include "kernel/mem.h" +#include "kernel/ff.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -54,31 +55,160 @@ struct OptMemPass : public Pass { SigMap sigmap(module); FfInitVals initvals(&sigmap, module); for (auto &mem : Mem::get_selected_memories(module)) { + std::vector<bool> always_0(mem.width, true); + std::vector<bool> always_1(mem.width, true); bool changed = false; for (auto &port : mem.wr_ports) { if (port.en.is_fully_zero()) { port.removed = true; changed = true; total_count++; + } else { + for (int sub = 0; sub < (1 << port.wide_log2); sub++) { + for (int i = 0; i < mem.width; i++) { + int bit = sub * mem.width + i; + if (port.en[bit] != State::S0) { + if (port.data[bit] != State::Sx && port.data[bit] != State::S0) { + always_0[i] = false; + } + if (port.data[bit] != State::Sx && port.data[bit] != State::S1) { + always_1[i] = false; + } + } else { + if (port.data[bit] != State::Sx) { + port.data[bit] = State::Sx; + changed = true; + total_count++; + } + } + } + } } } - if (changed) { - mem.emit(); + for (auto &init : mem.inits) { + for (int i = 0; i < GetSize(init.data); i++) { + State bit = init.data.bits[i]; + int lane = i % mem.width; + if (bit != State::Sx && bit != State::S0) { + always_0[lane] = false; + } + if (bit != State::Sx && bit != State::S1) { + always_1[lane] = false; + } + } } - - if (mem.wr_ports.empty() && mem.inits.empty()) { - // The whole memory array will contain - // only State::Sx, but the embedded read - // registers could have reset or init values. - // They will probably be optimized away by - // opt_dff later. - for (int i = 0; i < GetSize(mem.rd_ports); i++) { - mem.extract_rdff(i, &initvals); - auto &port = mem.rd_ports[i]; - module->connect(port.data, Const(State::Sx, GetSize(port.data))); + std::vector<int> swizzle; + for (int i = 0; i < mem.width; i++) { + if (!always_0[i] && !always_1[i]) { + swizzle.push_back(i); + continue; } + State bit; + if (!always_0[i]) { + log("%s.%s: removing const-1 lane %d\n", log_id(module->name), log_id(mem.memid), i); + bit = State::S1; + } else if (!always_1[i]) { + log("%s.%s: removing const-0 lane %d\n", log_id(module->name), log_id(mem.memid), i); + bit = State::S0; + } else { + log("%s.%s: removing const-x lane %d\n", log_id(module->name), log_id(mem.memid), i); + bit = State::Sx; + } + // Reconnect read port data. + for (auto &port: mem.rd_ports) { + for (int sub = 0; sub < (1 << port.wide_log2); sub++) { + int bidx = sub * mem.width + i; + if (!port.clk_enable) { + module->connect(port.data[bidx], bit); + } else { + // The FF will most likely be redundant, but it's up to opt_dff to deal with this. + FfData ff(module, &initvals, NEW_ID); + ff.width = 1; + ff.has_clk = true; + ff.sig_clk = port.clk; + ff.pol_clk = port.clk_polarity; + if (port.en != State::S1) { + ff.has_ce = true; + ff.pol_ce = true; + ff.sig_ce = port.en; + } + if (port.arst != State::S0) { + ff.has_arst = true; + ff.pol_arst = true; + ff.sig_arst = port.arst; + ff.val_arst = port.arst_value[bidx]; + } + if (port.srst != State::S0) { + ff.has_srst = true; + ff.pol_srst = true; + ff.sig_srst = port.srst; + ff.val_srst = port.srst_value[bidx]; + } + ff.sig_d = bit; + ff.sig_q = port.data[bidx]; + ff.val_init = port.init_value[bidx]; + ff.emit(); + } + } + } + } + if (GetSize(swizzle) == 0) { mem.remove(); total_count++; + continue; + } + if (GetSize(swizzle) != mem.width) { + for (auto &port: mem.wr_ports) { + SigSpec new_data; + SigSpec new_en; + for (int sub = 0; sub < (1 << port.wide_log2); sub++) { + for (auto i: swizzle) { + new_data.append(port.data[sub * mem.width + i]); + new_en.append(port.en[sub * mem.width + i]); + } + } + port.data = new_data; + port.en = new_en; + } + for (auto &port: mem.rd_ports) { + SigSpec new_data; + Const new_init; + Const new_arst; + Const new_srst; + for (int sub = 0; sub < (1 << port.wide_log2); sub++) { + for (auto i: swizzle) { + int bidx = sub * mem.width + i; + new_data.append(port.data[bidx]); + new_init.bits.push_back(port.init_value.bits[bidx]); + new_arst.bits.push_back(port.arst_value.bits[bidx]); + new_srst.bits.push_back(port.srst_value.bits[bidx]); + } + } + port.data = new_data; + port.init_value = new_init; + port.arst_value = new_arst; + port.srst_value = new_srst; + } + for (auto &init: mem.inits) { + Const new_data; + Const new_en; + for (int s = 0; s < GetSize(init.data); s += mem.width) { + for (auto i: swizzle) { + new_data.bits.push_back(init.data.bits[s + i]); + } + } + for (auto i: swizzle) { + new_en.bits.push_back(init.en.bits[i]); + } + init.data = new_data; + init.en = new_en; + } + mem.width = GetSize(swizzle); + changed = true; + total_count++; + } + if (changed) { + mem.emit(); } } } diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 7b52b85cd..d085fab2d 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -157,6 +157,7 @@ struct SimInstance dict<Wire*, pair<int, Const>> signal_database; dict<Wire*, fstHandle> fst_handles; + dict<IdString, dict<int,fstHandle>> fst_memories; SimInstance(SimShared *shared, std::string scope, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) : shared(shared), scope(scope), module(module), instance(instance), parent(parent), sigmap(module) @@ -243,7 +244,10 @@ struct SimInstance if (cell->is_mem_cell()) { - mem_cells[cell] = cell->parameters.at(ID::MEMID).decode_string(); + std::string name = cell->parameters.at(ID::MEMID).decode_string(); + mem_cells[cell] = name; + if (shared->fst) + fst_memories[name] = shared->fst->getMemoryHandles(scope + "." + RTLIL::unescape_id(name)); } if (cell->type.in(ID($assert), ID($cover), ID($assume))) { formal_database.insert(cell); @@ -336,7 +340,7 @@ struct SimInstance int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width; for (int i = 0; i < GetSize(data); i++) - if (0 <= i+offset && i+offset < GetSize(data)) + if (0 <= i+offset && i+offset < state.mem->size * state.mem->width) state.data.bits[i+offset] = data.bits[i]; } @@ -799,6 +803,18 @@ struct SimInstance did_something |= true; } } + for (auto cell : module->cells()) + { + if (cell->is_mem_cell()) { + std::string memid = cell->parameters.at(ID::MEMID).decode_string(); + for (auto &data : fst_memories[memid]) + { + std::string v = shared->fst->valueOf(data.second); + set_memory_state(memid, Const(data.first), Const::from_string(v)); + } + } + } + for (auto child : children) did_something |= child.second->setInitState(); return did_something; diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index a37b2a0f3..ff98a6e36 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -115,7 +115,7 @@ int map_autoidx; SigMap assign_map; RTLIL::Module *module; std::vector<gate_t> signal_list; -std::map<RTLIL::SigBit, int> signal_map; +dict<RTLIL::SigBit, int> signal_map; FfInitVals initvals; pool<std::string> enabled_gates; bool cmos_cost; @@ -409,7 +409,7 @@ std::string remap_name(RTLIL::IdString abc_name, RTLIL::Wire **orig_wire = nullp return stringf("$abc$%d$%s", map_autoidx, abc_name.c_str()+1); } -void dump_loop_graph(FILE *f, int &nr, std::map<int, std::set<int>> &edges, std::set<int> &workpool, std::vector<int> &in_counts) +void dump_loop_graph(FILE *f, int &nr, dict<int, pool<int>> &edges, pool<int> &workpool, std::vector<int> &in_counts) { if (f == nullptr) return; @@ -420,7 +420,7 @@ void dump_loop_graph(FILE *f, int &nr, std::map<int, std::set<int>> &edges, std: fprintf(f, " label=\"slide%d\";\n", nr); fprintf(f, " rankdir=\"TD\";\n"); - std::set<int> nodes; + pool<int> nodes; for (auto &e : edges) { nodes.insert(e.first); for (auto n : e.second) @@ -443,9 +443,9 @@ void handle_loops() // http://en.wikipedia.org/wiki/Topological_sorting // (Kahn, Arthur B. (1962), "Topological sorting of large networks") - std::map<int, std::set<int>> edges; + dict<int, pool<int>> edges; std::vector<int> in_edges_count(signal_list.size()); - std::set<int> workpool; + pool<int> workpool; FILE *dot_f = nullptr; int dot_nr = 0; @@ -1135,7 +1135,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin SigMap mapped_sigmap(mapped_mod); FfInitVals mapped_initvals(&mapped_sigmap, mapped_mod); - std::map<std::string, int> cell_stats; + dict<std::string, int> cell_stats; for (auto c : mapped_mod->cells()) { if (builtin_lib) @@ -2000,18 +2000,18 @@ struct AbcPass : public Pass { CellTypes ct(design); std::vector<RTLIL::Cell*> all_cells = mod->selected_cells(); - std::set<RTLIL::Cell*> unassigned_cells(all_cells.begin(), all_cells.end()); + pool<RTLIL::Cell*> unassigned_cells(all_cells.begin(), all_cells.end()); - std::set<RTLIL::Cell*> expand_queue, next_expand_queue; - std::set<RTLIL::Cell*> expand_queue_up, next_expand_queue_up; - std::set<RTLIL::Cell*> expand_queue_down, next_expand_queue_down; + pool<RTLIL::Cell*> expand_queue, next_expand_queue; + pool<RTLIL::Cell*> expand_queue_up, next_expand_queue_up; + pool<RTLIL::Cell*> expand_queue_down, next_expand_queue_down; typedef tuple<bool, RTLIL::SigSpec, bool, RTLIL::SigSpec, bool, RTLIL::SigSpec, bool, RTLIL::SigSpec> clkdomain_t; - std::map<clkdomain_t, std::vector<RTLIL::Cell*>> assigned_cells; - std::map<RTLIL::Cell*, clkdomain_t> assigned_cells_reverse; + dict<clkdomain_t, std::vector<RTLIL::Cell*>> assigned_cells; + dict<RTLIL::Cell*, clkdomain_t> assigned_cells_reverse; - std::map<RTLIL::Cell*, std::set<RTLIL::SigBit>> cell_to_bit, cell_to_bit_up, cell_to_bit_down; - std::map<RTLIL::SigBit, std::set<RTLIL::Cell*>> bit_to_cell, bit_to_cell_up, bit_to_cell_down; + dict<RTLIL::Cell*, pool<RTLIL::SigBit>> cell_to_bit, cell_to_bit_up, cell_to_bit_down; + dict<RTLIL::SigBit, pool<RTLIL::Cell*>> bit_to_cell, bit_to_cell_up, bit_to_cell_down; for (auto cell : all_cells) { diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh index 1b65ca9c9..8ed7f8cbc 100644 --- a/tests/sva/runtest.sh +++ b/tests/sva/runtest.sh @@ -22,18 +22,17 @@ generate_sby() { if [ -f $prefix.sv ]; then if [ "$1" = "fail" ]; then - echo "verific -sv ${prefix}_fail.sv" + echo "read -sv ${prefix}_fail.sv" else - echo "verific -sv $prefix.sv" + echo "read -sv $prefix.sv" fi fi if [ -f $prefix.vhd ]; then - echo "verific -vhdl $prefix.vhd" + echo "read -vhdl $prefix.vhd" fi cat <<- EOT - verific -import -extnets -all top prep -top top chformal -early -assume diff --git a/tests/techmap/.gitignore b/tests/techmap/.gitignore index cfed22fc5..56c9ba8f9 100644 --- a/tests/techmap/.gitignore +++ b/tests/techmap/.gitignore @@ -1,2 +1,3 @@ *.log +*.out /*.mk diff --git a/tests/techmap/mem_simple_4x1_runtest.sh b/tests/techmap/mem_simple_4x1_runtest.sh index b486de5c7..5b5838b9d 100644 --- a/tests/techmap/mem_simple_4x1_runtest.sh +++ b/tests/techmap/mem_simple_4x1_runtest.sh @@ -1,17 +1,3 @@ #!/bin/bash -set -e - -../../yosys -b 'verilog -noattr' -o mem_simple_4x1_synth.v -p 'read_verilog mem_simple_4x1_uut.v; proc; opt; memory -nomap; techmap -map mem_simple_4x1_map.v;; techmap; opt; abc;; stat' - -iverilog -o mem_simple_4x1_gold_tb mem_simple_4x1_tb.v mem_simple_4x1_uut.v -iverilog -o mem_simple_4x1_gate_tb mem_simple_4x1_tb.v mem_simple_4x1_synth.v mem_simple_4x1_cells.v - -./mem_simple_4x1_gold_tb > mem_simple_4x1_gold_tb.out -./mem_simple_4x1_gate_tb > mem_simple_4x1_gate_tb.out - -diff -u mem_simple_4x1_gold_tb.out mem_simple_4x1_gate_tb.out -rm -f mem_simple_4x1_synth.v mem_simple_4x1_tb.vcd -rm -f mem_simple_4x1_{gold,gate}_tb{,.out} -: OK - +exec ../tools/autotest.sh -G -j $@ -p 'proc; opt; memory -nomap; techmap -map ../mem_simple_4x1_map.v;; techmap; opt; abc;; stat' mem_simple_4x1_uut.v |