From 25a4cd7020c100838e359b393ffb545532e69101 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcelina=20Ko=C5=9Bcielnicka?= Date: Thu, 16 Jun 2022 06:04:04 +0200 Subject: memory_libmap: Fix params emitted for unused ports for consistency. --- passes/memory/memory_libmap.cc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'passes') diff --git a/passes/memory/memory_libmap.cc b/passes/memory/memory_libmap.cc index 898e0af85..d77e4be30 100644 --- a/passes/memory/memory_libmap.cc +++ b/passes/memory/memory_libmap.cc @@ -1706,10 +1706,11 @@ void MemMapping::emit_port(const MemConfig &cfg, std::vector &cells, cons if (pdef.wrbe_separate) { cell->setPort(stringf("\\PORT_%s_WR_EN", name), State::S0); cell->setPort(stringf("\\PORT_%s_WR_BE", name), hw_wren); - cell->setParam(stringf("\\PORT_%s_WR_BE_WIDTH", name), GetSize(hw_wren)); + if (cfg.def->width_mode != WidthMode::Single) + cell->setParam(stringf("\\PORT_%s_WR_BE_WIDTH", name), GetSize(hw_wren)); } else { cell->setPort(stringf("\\PORT_%s_WR_EN", name), hw_wren); - if (cfg.def->byte != 0) + if (cfg.def->byte != 0 && cfg.def->width_mode != WidthMode::Single) cell->setParam(stringf("\\PORT_%s_WR_EN_WIDTH", name), GetSize(hw_wren)); } } -- cgit v1.2.3 From d69091806ad29c3720e478d965354f44bd266d7f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcelina=20Ko=C5=9Bcielnicka?= Date: Fri, 17 Jun 2022 01:20:33 +0200 Subject: memory_libmap: Fix wrprio handling. --- passes/memory/memory_libmap.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'passes') diff --git a/passes/memory/memory_libmap.cc b/passes/memory/memory_libmap.cc index d77e4be30..9e147b0bf 100644 --- a/passes/memory/memory_libmap.cc +++ b/passes/memory/memory_libmap.cc @@ -837,7 +837,7 @@ void MemMapping::handle_priority() { if (!port2.priority_mask[p1idx]) continue; for (auto &cfg: cfgs) { - auto &p1cfg = cfg.rd_ports[p1idx]; + auto &p1cfg = cfg.wr_ports[p1idx]; auto &p2cfg = cfg.wr_ports[p2idx]; bool found = false; for (auto &pgi: p2cfg.def->wrprio) { -- cgit v1.2.3 From 01daa077a2837830914f3d99f351918d690b9093 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcelina=20Ko=C5=9Bcielnicka?= Date: Fri, 17 Jun 2022 14:11:04 +0200 Subject: memory_map: Use const drivers instead of FFs for ROMs. --- passes/memory/memory_map.cc | 111 +++++++++++++++++++++++--------------------- 1 file changed, 59 insertions(+), 52 deletions(-) (limited to 'passes') diff --git a/passes/memory/memory_map.cc b/passes/memory/memory_map.cc index ca1ca483d..21c7a761e 100644 --- a/passes/memory/memory_map.cc +++ b/passes/memory/memory_map.cc @@ -191,6 +191,10 @@ struct MemoryMapWorker data_reg_out[idx] = static_cells_map[addr]; count_static++; } + else if (mem.wr_ports.empty()) + { + data_reg_out[idx] = init_data.extract(i*mem.width, mem.width); + } else { RTLIL::Cell *c = module->addCell(genid(mem.memid, "", addr), ID($dff)); @@ -266,69 +270,72 @@ struct MemoryMapWorker log(" read interface: %d $dff and %d $mux cells.\n", count_dff, count_mux); - for (int i = 0; i < mem.size; i++) + if (!mem.wr_ports.empty()) { - int addr = i + mem.start_offset; - int idx = addr & ((1 << abits) - 1); - if (static_cells_map.count(addr) > 0) - continue; - - RTLIL::SigSpec sig = data_reg_out[idx]; - - for (int j = 0; j < GetSize(mem.wr_ports); j++) + for (int i = 0; i < mem.size; i++) { - auto &port = mem.wr_ports[j]; - RTLIL::SigSpec wr_addr = port.addr.extract_end(port.wide_log2); - RTLIL::Wire *w_seladdr = addr_decode(wr_addr, RTLIL::SigSpec(addr >> port.wide_log2, GetSize(wr_addr))); + int addr = i + mem.start_offset; + int idx = addr & ((1 << abits) - 1); + if (static_cells_map.count(addr) > 0) + continue; - int sub = addr & ((1 << port.wide_log2) - 1); + RTLIL::SigSpec sig = data_reg_out[idx]; - int wr_offset = 0; - while (wr_offset < mem.width) + for (int j = 0; j < GetSize(mem.wr_ports); j++) { - int wr_width = 1; - RTLIL::SigSpec wr_bit = port.en.extract(wr_offset + sub * mem.width, 1); - - while (wr_offset + wr_width < mem.width) { - RTLIL::SigSpec next_wr_bit = port.en.extract(wr_offset + wr_width + sub * mem.width, 1); - if (next_wr_bit != wr_bit) - break; - wr_width++; - } + auto &port = mem.wr_ports[j]; + RTLIL::SigSpec wr_addr = port.addr.extract_end(port.wide_log2); + RTLIL::Wire *w_seladdr = addr_decode(wr_addr, RTLIL::SigSpec(addr >> port.wide_log2, GetSize(wr_addr))); - RTLIL::Wire *w = w_seladdr; + int sub = addr & ((1 << port.wide_log2) - 1); - if (wr_bit != State::S1) + int wr_offset = 0; + while (wr_offset < mem.width) { - RTLIL::Cell *c = module->addCell(genid(mem.memid, "$wren", addr, "", j, "", wr_offset), ID($and)); - c->parameters[ID::A_SIGNED] = RTLIL::Const(0); - c->parameters[ID::B_SIGNED] = RTLIL::Const(0); - c->parameters[ID::A_WIDTH] = RTLIL::Const(1); - c->parameters[ID::B_WIDTH] = RTLIL::Const(1); - c->parameters[ID::Y_WIDTH] = RTLIL::Const(1); - c->setPort(ID::A, w); - c->setPort(ID::B, wr_bit); - - w = module->addWire(genid(mem.memid, "$wren", addr, "", j, "", wr_offset, "$y")); - c->setPort(ID::Y, RTLIL::SigSpec(w)); + int wr_width = 1; + RTLIL::SigSpec wr_bit = port.en.extract(wr_offset + sub * mem.width, 1); + + while (wr_offset + wr_width < mem.width) { + RTLIL::SigSpec next_wr_bit = port.en.extract(wr_offset + wr_width + sub * mem.width, 1); + if (next_wr_bit != wr_bit) + break; + wr_width++; + } + + RTLIL::Wire *w = w_seladdr; + + if (wr_bit != State::S1) + { + RTLIL::Cell *c = module->addCell(genid(mem.memid, "$wren", addr, "", j, "", wr_offset), ID($and)); + c->parameters[ID::A_SIGNED] = RTLIL::Const(0); + c->parameters[ID::B_SIGNED] = RTLIL::Const(0); + c->parameters[ID::A_WIDTH] = RTLIL::Const(1); + c->parameters[ID::B_WIDTH] = RTLIL::Const(1); + c->parameters[ID::Y_WIDTH] = RTLIL::Const(1); + c->setPort(ID::A, w); + c->setPort(ID::B, wr_bit); + + w = module->addWire(genid(mem.memid, "$wren", addr, "", j, "", wr_offset, "$y")); + c->setPort(ID::Y, RTLIL::SigSpec(w)); + } + + RTLIL::Cell *c = module->addCell(genid(mem.memid, "$wrmux", addr, "", j, "", wr_offset), ID($mux)); + c->parameters[ID::WIDTH] = wr_width; + c->setPort(ID::A, sig.extract(wr_offset, wr_width)); + c->setPort(ID::B, port.data.extract(wr_offset + sub * mem.width, wr_width)); + c->setPort(ID::S, RTLIL::SigSpec(w)); + + w = module->addWire(genid(mem.memid, "$wrmux", addr, "", j, "", wr_offset, "$y"), wr_width); + c->setPort(ID::Y, w); + + sig.replace(wr_offset, w); + wr_offset += wr_width; + count_wrmux++; } - - RTLIL::Cell *c = module->addCell(genid(mem.memid, "$wrmux", addr, "", j, "", wr_offset), ID($mux)); - c->parameters[ID::WIDTH] = wr_width; - c->setPort(ID::A, sig.extract(wr_offset, wr_width)); - c->setPort(ID::B, port.data.extract(wr_offset + sub * mem.width, wr_width)); - c->setPort(ID::S, RTLIL::SigSpec(w)); - - w = module->addWire(genid(mem.memid, "$wrmux", addr, "", j, "", wr_offset, "$y"), wr_width); - c->setPort(ID::Y, w); - - sig.replace(wr_offset, w); - wr_offset += wr_width; - count_wrmux++; } - } - module->connect(RTLIL::SigSig(data_reg_in[idx], sig)); + module->connect(RTLIL::SigSig(data_reg_in[idx], sig)); + } } log(" write interface: %d write mux blocks.\n", count_wrmux); -- cgit v1.2.3 From ab3a9325c33b5b1b9de6971b6931ee12c3e3871c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcelina=20Ko=C5=9Bcielnicka?= Date: Fri, 17 Jun 2022 15:29:37 +0200 Subject: memory_map: Add -rom-only option. --- passes/memory/memory_map.cc | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) (limited to 'passes') diff --git a/passes/memory/memory_map.cc b/passes/memory/memory_map.cc index 21c7a761e..ccfb8c94f 100644 --- a/passes/memory/memory_map.cc +++ b/passes/memory/memory_map.cc @@ -30,6 +30,7 @@ PRIVATE_NAMESPACE_BEGIN struct MemoryMapWorker { bool attr_icase = false; + bool rom_only = false; dict> attributes; RTLIL::Design *design; @@ -107,11 +108,8 @@ struct MemoryMapWorker SigSpec init_data = mem.get_init_data(); - // delete unused memory cell - if (mem.rd_ports.empty()) { - mem.remove(); + if (!mem.wr_ports.empty() && rom_only) return; - } // check if attributes allow us to infer FFRAM for this memory for (const auto &attr : attributes) { @@ -143,6 +141,12 @@ struct MemoryMapWorker } } + // delete unused memory cell + if (mem.rd_ports.empty()) { + mem.remove(); + return; + } + // all write ports must share the same clock RTLIL::SigSpec refclock; bool refclock_pol = false; @@ -373,10 +377,14 @@ struct MemoryMapPass : public Pass { log(" -iattr\n"); log(" for -attr, ignore case of .\n"); log("\n"); + log(" -rom-only\n"); + log(" only perform conversion for ROMs (memories with no write ports).\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { bool attr_icase = false; + bool rom_only = false; dict> attributes; log_header(design, "Executing MEMORY_MAP pass (converting memories to logic and flip-flops).\n"); @@ -413,6 +421,11 @@ struct MemoryMapPass : public Pass { attr_icase = true; continue; } + if (args[argidx] == "-rom-only") + { + rom_only = true; + continue; + } break; } extra_args(args, argidx, design); @@ -421,6 +434,7 @@ struct MemoryMapPass : public Pass { MemoryMapWorker worker(design, mod); worker.attr_icase = attr_icase; worker.attributes = attributes; + worker.rom_only = rom_only; worker.run(); } } -- cgit v1.2.3 From c16c0288311ba9aef95b3d5fcdde63bbc05a5b08 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Wed, 22 Jun 2022 20:53:10 -0700 Subject: add hierarchy -smtcheck like -simcheck, but allow smtlib2_module modules. --- passes/hierarchy/hierarchy.cc | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) (limited to 'passes') diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc index d40d6e59f..d27fddf1c 100644 --- a/passes/hierarchy/hierarchy.cc +++ b/passes/hierarchy/hierarchy.cc @@ -439,7 +439,8 @@ void check_cell_connections(const RTLIL::Module &module, RTLIL::Cell &cell, RTLI } } -bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check, bool flag_simcheck, std::vector &libdirs) +bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check, bool flag_simcheck, bool flag_smtcheck, + std::vector &libdirs) { bool did_something = false; std::map> array_cells; @@ -477,7 +478,7 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check RTLIL::Module *mod = design->module(cell->type); if (!mod) { - mod = get_module(*design, *cell, *module, flag_check || flag_simcheck, libdirs); + mod = get_module(*design, *cell, *module, flag_check || flag_simcheck || flag_smtcheck, libdirs); // If we still don't have a module, treat the cell as a black box and skip // it. Otherwise, we either loaded or derived something so should set the @@ -495,11 +496,11 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check // interfaces. if_expander.visit_connections(*cell, *mod); - if (flag_check || flag_simcheck) + if (flag_check || flag_simcheck || flag_smtcheck) check_cell_connections(*module, *cell, *mod); if (mod->get_blackbox_attribute()) { - if (flag_simcheck) + if (flag_simcheck || (flag_smtcheck && !mod->get_bool_attribute(ID::smtlib2_module))) log_error("Module `%s' referenced in module `%s' in cell `%s' is a blackbox/whitebox module.\n", cell->type.c_str(), module->name.c_str(), cell->name.c_str()); continue; @@ -737,6 +738,9 @@ struct HierarchyPass : public Pass { log(" like -check, but also throw an error if blackbox modules are\n"); log(" instantiated, and throw an error if the design has no top module.\n"); log("\n"); + log(" -smtcheck\n"); + log(" like -simcheck, but allow smtlib2_module modules.\n"); + log("\n"); log(" -purge_lib\n"); log(" by default the hierarchy command will not remove library (blackbox)\n"); log(" modules. use this option to also remove unused blackbox modules.\n"); @@ -803,6 +807,7 @@ struct HierarchyPass : public Pass { bool flag_check = false; bool flag_simcheck = false; + bool flag_smtcheck = false; bool purge_lib = false; RTLIL::Module *top_mod = NULL; std::string load_top_mod; @@ -821,7 +826,7 @@ struct HierarchyPass : public Pass { size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { - if (args[argidx] == "-generate" && !flag_check && !flag_simcheck && !top_mod) { + if (args[argidx] == "-generate" && !flag_check && !flag_simcheck && !flag_smtcheck && !top_mod) { generate_mode = true; log("Entering generate mode.\n"); while (++argidx < args.size()) { @@ -868,6 +873,10 @@ struct HierarchyPass : public Pass { flag_simcheck = true; continue; } + if (args[argidx] == "-smtcheck") { + flag_smtcheck = true; + continue; + } if (args[argidx] == "-purge_lib") { purge_lib = true; continue; @@ -1013,7 +1022,7 @@ struct HierarchyPass : public Pass { } } - if (flag_simcheck && top_mod == nullptr) + if ((flag_simcheck || flag_smtcheck) && top_mod == nullptr) log_error("Design has no top module.\n"); if (top_mod != NULL) { @@ -1039,7 +1048,7 @@ struct HierarchyPass : public Pass { } for (auto module : used_modules) { - if (expand_module(design, module, flag_check, flag_simcheck, libdirs)) + if (expand_module(design, module, flag_check, flag_simcheck, flag_smtcheck, libdirs)) did_something = true; } -- cgit v1.2.3 From d78d807a7fa1747b40da8bac9e278183cf86d3cc Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 27 Jun 2022 15:47:55 +0200 Subject: memory_map: -keepdc option for formal Use it when invoking memory_map -rom-only from write_{smt2,btor}. --- passes/memory/memory_map.cc | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) (limited to 'passes') diff --git a/passes/memory/memory_map.cc b/passes/memory/memory_map.cc index ccfb8c94f..5ec717733 100644 --- a/passes/memory/memory_map.cc +++ b/passes/memory/memory_map.cc @@ -31,6 +31,7 @@ struct MemoryMapWorker { bool attr_icase = false; bool rom_only = false; + bool keepdc = false; dict> attributes; RTLIL::Design *design; @@ -190,14 +191,15 @@ struct MemoryMapWorker { int addr = i + mem.start_offset; int idx = addr & ((1 << abits) - 1); + SigSpec w_init = init_data.extract(i*mem.width, mem.width); if (static_cells_map.count(addr) > 0) { data_reg_out[idx] = static_cells_map[addr]; count_static++; } - else if (mem.wr_ports.empty()) + else if (mem.wr_ports.empty() && (!keepdc || w_init.is_fully_def())) { - data_reg_out[idx] = init_data.extract(i*mem.width, mem.width); + data_reg_out[idx] = w_init; } else { @@ -220,7 +222,6 @@ struct MemoryMapWorker w_out_name = genid(mem.memid, "", addr, "$q"); RTLIL::Wire *w_out = module->addWire(w_out_name, mem.width); - SigSpec w_init = init_data.extract(i*mem.width, mem.width); if (!w_init.is_fully_undef()) w_out->attributes[ID::init] = w_init.as_const(); @@ -380,11 +381,15 @@ struct MemoryMapPass : public Pass { log(" -rom-only\n"); log(" only perform conversion for ROMs (memories with no write ports).\n"); log("\n"); + log(" -keepdc\n"); + log(" when mapping ROMs, keep x-bits shared across read ports.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { bool attr_icase = false; bool rom_only = false; + bool keepdc = false; dict> attributes; log_header(design, "Executing MEMORY_MAP pass (converting memories to logic and flip-flops).\n"); @@ -426,6 +431,11 @@ struct MemoryMapPass : public Pass { rom_only = true; continue; } + if (args[argidx] == "-keepdc") + { + keepdc = true; + continue; + } break; } extra_args(args, argidx, design); @@ -435,6 +445,7 @@ struct MemoryMapPass : public Pass { worker.attr_icase = attr_icase; worker.attributes = attributes; worker.rom_only = rom_only; + worker.keepdc = keepdc; worker.run(); } } -- cgit v1.2.3 From a6b440b5c9c4fb0472c01aec84961c3f1b40c954 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 28 Jun 2022 19:05:35 +0200 Subject: memory_map: avoid undriven unused FF inputs for -keepdc --- passes/memory/memory_map.cc | 3 +++ 1 file changed, 3 insertions(+) (limited to 'passes') diff --git a/passes/memory/memory_map.cc b/passes/memory/memory_map.cc index 5ec717733..fd5b1f1ad 100644 --- a/passes/memory/memory_map.cc +++ b/passes/memory/memory_map.cc @@ -228,6 +228,9 @@ struct MemoryMapWorker data_reg_out[idx] = w_out; c->setPort(ID::Q, w_out); + + if (mem.wr_ports.empty()) + module->connect(RTLIL::SigSig(w_in, w_out)); } } -- cgit v1.2.3 From a47254bd106b0cce210bd0ce282d84b44ceb07f1 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 29 Jun 2022 15:35:28 +0200 Subject: opt_dff: With -keepdc, never turn undef init vals into const drivers --- passes/opt/opt_dff.cc | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) (limited to 'passes') diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 0ad4acec2..6ff2d1b4b 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -491,12 +491,17 @@ struct OptDffWorker ff.has_srst = false; ff.sig_d = ff.val_srst; changed = true; - } else { + } else if (!opt.keepdc || ff.val_init.is_fully_def()) { log("Handling never-active EN on %s (%s) from module %s (removing D path).\n", log_id(cell), log_id(cell->type), log_id(module)); // The D input path is effectively useless, so remove it (this will be a D latch, SR latch, or a const driver). ff.has_ce = ff.has_clk = ff.has_srst = false; changed = true; + } else { + // We need to keep the undefined initival around as such + ff.sig_d = ff.sig_q; + ff.has_ce = ff.has_srst = false; + changed = true; } } else if (ff.sig_ce == (ff.pol_ce ? State::S1 : State::S0)) { // Always-active enable. Just remove it. @@ -508,13 +513,20 @@ struct OptDffWorker } } - if (ff.has_clk) { - if (ff.sig_clk.is_fully_const()) { + if (ff.has_clk && ff.sig_clk.is_fully_const()) { + if (!opt.keepdc || ff.val_init.is_fully_def()) { // Const clock — the D input path is effectively useless, so remove it (this will be a D latch, SR latch, or a const driver). log("Handling const CLK on %s (%s) from module %s (removing D path).\n", log_id(cell), log_id(cell->type), log_id(module)); ff.has_ce = ff.has_clk = ff.has_srst = false; changed = true; + } else { + // Const clock, but we need to keep the undefined initval around as such + if (ff.has_ce || ff.has_srst || ff.sig_d != ff.sig_q) { + ff.sig_d = ff.sig_q; + ff.has_ce = ff.has_srst = false; + changed = true; + } } } @@ -550,7 +562,7 @@ struct OptDffWorker ff.has_srst = false; ff.sig_d = ff.val_srst; changed = true; - } else { + } else if (!opt.keepdc || ff.val_init.is_fully_def()) { // The D input path is effectively useless, so remove it (this will be a const-input D latch, SR latch, or a const driver). log("Handling D = Q on %s (%s) from module %s (removing D path).\n", log_id(cell), log_id(cell->type), log_id(module)); @@ -567,7 +579,7 @@ struct OptDffWorker } // The cell has been simplified as much as possible already. Now try to spice it up with enables / sync resets. - if (ff.has_clk) { + if (ff.has_clk && ff.sig_d != ff.sig_q) { if (!ff.has_arst && !ff.has_sr && (!ff.has_srst || !ff.has_ce || ff.ce_over_srst) && !opt.nosdff) { // Try to merge sync resets. std::map> groups; -- cgit v1.2.3 From 5db542742b8f69405417e5a715b4b72ce4c78534 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 29 Jun 2022 17:53:58 +0200 Subject: async2sync: turn FFs with const clks into gclk FFs with feedback The formal backends do not support multiple clocks. This includes constant clocks. Constant clocks do appear in what isn't a proper multiclock design, for example when mapping not fully initialized ROMs. As converting FFs with constant clocks to FFs using the global is doable even in a single clock flow, make async2sync do this. --- passes/sat/async2sync.cc | 3 +++ 1 file changed, 3 insertions(+) (limited to 'passes') diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc index 46c76eba9..6fdf470b1 100644 --- a/passes/sat/async2sync.cc +++ b/passes/sat/async2sync.cc @@ -75,6 +75,9 @@ struct Async2syncPass : public Pass { if (ff.has_gclk) continue; + if (ff.has_clk && ff.sig_clk.is_fully_const()) + ff.has_ce = ff.has_clk = ff.has_srst = false; + if (ff.has_clk) { if (ff.has_sr) { -- cgit v1.2.3 From 502b96fe53e82b5454fbbd032cbf6b13ad2dad6d Mon Sep 17 00:00:00 2001 From: Catherine Date: Thu, 7 Jul 2022 08:08:17 +0000 Subject: Fix external ABC build after commit 0ca0932b5. --- passes/techmap/abc.cc | 6 ++++-- passes/techmap/abc9_exe.cc | 6 ++++-- 2 files changed, 8 insertions(+), 4 deletions(-) (limited to 'passes') diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index 61ee99ee7..0b9c327c0 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -65,7 +65,9 @@ #include "frontends/blif/blifparse.h" #ifdef YOSYS_LINK_ABC -extern "C" int Abc_RealMain(int argc, char *argv[]); +namespace abc { + int Abc_RealMain(int argc, char *argv[]); +} #endif USING_YOSYS_NAMESPACE @@ -1098,7 +1100,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin abc_argv[2] = strdup("-f"); abc_argv[3] = strdup(tmp_script_name.c_str()); abc_argv[4] = 0; - int ret = Abc_RealMain(4, abc_argv); + int ret = abc::Abc_RealMain(4, abc_argv); free(abc_argv[0]); free(abc_argv[1]); free(abc_argv[2]); diff --git a/passes/techmap/abc9_exe.cc b/passes/techmap/abc9_exe.cc index a66e95e21..7dc0a364b 100644 --- a/passes/techmap/abc9_exe.cc +++ b/passes/techmap/abc9_exe.cc @@ -31,7 +31,9 @@ #endif #ifdef YOSYS_LINK_ABC -extern "C" int Abc_RealMain(int argc, char *argv[]); +namespace abc { + int Abc_RealMain(int argc, char *argv[]); +} #endif std::string fold_abc9_cmd(std::string str) @@ -277,7 +279,7 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe abc9_argv[2] = strdup("-f"); abc9_argv[3] = strdup(tmp_script_name.c_str()); abc9_argv[4] = 0; - int ret = Abc_RealMain(4, abc9_argv); + int ret = abc::Abc_RealMain(4, abc9_argv); free(abc9_argv[0]); free(abc9_argv[1]); free(abc9_argv[2]); -- cgit v1.2.3 From 14ba50908bd53186b13845499635fb3f9ddc60c1 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 22 Jul 2022 14:47:00 +0200 Subject: sim: Fix $anyseq in nested modules --- passes/sat/sim.cc | 32 +++++++++++++++++++++----------- 1 file changed, 21 insertions(+), 11 deletions(-) (limited to 'passes') diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index d085fab2d..53644c6b7 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -157,6 +157,7 @@ struct SimInstance dict> signal_database; dict fst_handles; + dict fst_inputs; dict> fst_memories; SimInstance(SimShared *shared, std::string scope, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) : @@ -820,7 +821,7 @@ struct SimInstance return did_something; } - void addAdditionalInputs(std::map &inputs) + void addAdditionalInputs() { for (auto cell : module->cells()) { @@ -831,7 +832,7 @@ struct SimInstance for(auto &item : fst_handles) { if (item.second==0) continue; // Ignore signals not found if (sig_y == sigmap(item.first)) { - inputs[sig_y.as_wire()] = item.second; + fst_inputs[sig_y.as_wire()] = item.second; found = true; break; } @@ -842,7 +843,21 @@ struct SimInstance } } for (auto child : children) - child.second->addAdditionalInputs(inputs); + child.second->addAdditionalInputs(); + } + + bool setInputs() + { + bool did_something = false; + for(auto &item : fst_inputs) { + std::string v = shared->fst->valueOf(item.second); + did_something |= set_state(item.first, Const::from_string(v)); + } + + for (auto child : children) + did_something |= child.second->setInputs(); + + return did_something; } void setState(dict> bits, std::string values) @@ -1095,18 +1110,17 @@ struct SimWorker : SimShared } SigMap sigmap(topmod); - std::map inputs; for (auto wire : topmod->wires()) { if (wire->port_input) { fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name)); if (id==0) log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(wire->name)).c_str()); - inputs[wire] = id; + top->fst_inputs[wire] = id; } } - top->addAdditionalInputs(inputs); + top->addAdditionalInputs(); uint64_t startCount = 0; uint64_t stopCount = 0; @@ -1152,11 +1166,7 @@ struct SimWorker : SimShared fst->reconstructAllAtTimes(fst_clock, startCount, stopCount, [&](uint64_t time) { if (verbose) log("Co-simulating %s %d [%lu%s].\n", (all_samples ? "sample" : "cycle"), cycle, (unsigned long)time, fst->getTimescaleString()); - bool did_something = false; - for(auto &item : inputs) { - std::string v = fst->valueOf(item.second); - did_something |= top->set_state(item.first, Const::from_string(v)); - } + bool did_something = top->setInputs(); if (initial) { did_something |= top->setInitState(); -- cgit v1.2.3 From f679b756d8f9af44654132d3fd4e3a3465afea89 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcelina=20Ko=C5=9Bcielnicka?= Date: Sat, 23 Jul 2022 16:42:54 +0200 Subject: opt_reduce: Fix use-after-free. Fixes #3418. --- passes/opt/opt_reduce.cc | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'passes') diff --git a/passes/opt/opt_reduce.cc b/passes/opt/opt_reduce.cc index 1a7c93fbd..c36a38dae 100644 --- a/passes/opt/opt_reduce.cc +++ b/passes/opt/opt_reduce.cc @@ -594,11 +594,9 @@ struct OptReduceWorker if (cell->type.in(ID($mux), ID($pmux))) opt_pmux(cell); - - if (cell->type == ID($bmux)) + else if (cell->type == ID($bmux)) opt_bmux(cell); - - if (cell->type == ID($demux)) + else if (cell->type == ID($demux)) opt_demux(cell); } } -- cgit v1.2.3 From a48dcd1d40a845cfb8b18cbe986faf0b780880be Mon Sep 17 00:00:00 2001 From: Lofty Date: Mon, 11 Apr 2022 13:21:47 +0100 Subject: rename: add -scramble-name option to randomly rename selections --- passes/cmds/rename.cc | 56 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) (limited to 'passes') diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index 81da35ffe..b49d5cdc2 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -20,6 +20,7 @@ #include "kernel/register.h" #include "kernel/rtlil.h" #include "kernel/log.h" +#include "kernel/hashlib.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -156,6 +157,13 @@ struct RenamePass : public Pass { log("\n"); log("Rename top module.\n"); log("\n"); + log("\n"); + log(" rename -scramble-name [-seed ] [selection]\n"); + log("\n"); + log("Assign randomly-generated names to all selected wires and cells. The seed option\n"); + log("can be used to change the random number generator seed from the default, but it\n"); + log("must be non-zero.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { @@ -167,7 +175,9 @@ struct RenamePass : public Pass { bool flag_hide = false; bool flag_top = false; bool flag_output = false; + bool flag_scramble_name = false; bool got_mode = false; + unsigned int seed = 1; size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) @@ -203,6 +213,11 @@ struct RenamePass : public Pass { got_mode = true; continue; } + if (arg == "-scramble-name" && !got_mode) { + flag_scramble_name = true; + got_mode = true; + continue; + } if (arg == "-pattern" && argidx+1 < args.size() && args[argidx+1].find('%') != std::string::npos) { int pos = args[++argidx].find('%'); pattern_prefix = args[argidx].substr(0, pos); @@ -211,6 +226,11 @@ struct RenamePass : public Pass { } if (arg == "-suffix" && argidx + 1 < args.size()) { cell_suffix = args[++argidx]; + continue; + } + if (arg == "-seed" && argidx+1 < args.size()) { + seed = std::stoi(args[++argidx]); + continue; } break; } @@ -329,6 +349,42 @@ struct RenamePass : public Pass { design->rename(module, new_name); } else + if (flag_scramble_name) + { + extra_args(args, argidx, design); + + if (seed == 0) + log_error("Seed for -scramble-name cannot be zero.\n"); + + for (auto module : design->selected_modules()) + { + if (module->memories.size() != 0 || module->processes.size() != 0) { + log_warning("Skipping module %s with unprocessed memories or processes\n", log_id(module)); + continue; + } + + dict new_wire_names; + dict new_cell_names; + + for (auto wire : module->selected_wires()) + if (wire->port_id == 0) { + seed = mkhash_xorshift(seed); + new_wire_names[wire] = stringf("$_%u_", seed); + } + + for (auto cell : module->selected_cells()) { + seed = mkhash_xorshift(seed); + new_cell_names[cell] = stringf("$_%u_", seed); + } + + for (auto &it : new_wire_names) + module->rename(it.first, it.second); + + for (auto &it : new_cell_names) + module->rename(it.first, it.second); + } + } + else { if (argidx+2 != args.size()) log_cmd_error("Invalid number of arguments!\n"); -- cgit v1.2.3 From f4a1906721507c512050f62080a999c4147d92d6 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 8 Aug 2022 20:30:50 +0200 Subject: support file locations containing spaces --- passes/sat/qbfsat.cc | 2 +- passes/techmap/abc.cc | 10 +++++----- passes/techmap/abc9_exe.cc | 6 +++--- 3 files changed, 9 insertions(+), 9 deletions(-) (limited to 'passes') diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 864d6f05d..1302b3383 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -216,7 +216,7 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, QbfSolutionType ret; const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; const std::string smtbmc_warning = "z3: WARNING:"; - const std::string smtbmc_cmd = stringf("%s -s %s %s -t 1 -g --binary %s %s/problem%d.smt2 2>&1", + const std::string smtbmc_cmd = stringf("\"%s\" -s %s %s -t 1 -g --binary %s %s/problem%d.smt2 2>&1", yosys_smtbmc_exe.c_str(), opt.get_solver_name().c_str(), (opt.timeout != 0? stringf("--timeout %d", opt.timeout) : "").c_str(), (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file : "").c_str(), diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index 0b9c327c0..656c36b84 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -789,15 +789,15 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin log_header(design, "Extracting gate netlist of module `%s' to `%s/input.blif'..\n", module->name.c_str(), replace_tempdir(tempdir_name, tempdir_name, show_tempdir).c_str()); - std::string abc_script = stringf("read_blif %s/input.blif; ", tempdir_name.c_str()); + std::string abc_script = stringf("read_blif \"%s/input.blif\"; ", tempdir_name.c_str()); if (!liberty_files.empty() || !genlib_files.empty()) { for (std::string liberty_file : liberty_files) - abc_script += stringf("read_lib -w %s; ", liberty_file.c_str()); + abc_script += stringf("read_lib -w \"%s\"; ", liberty_file.c_str()); for (std::string liberty_file : genlib_files) - abc_script += stringf("read_library %s; ", liberty_file.c_str()); + abc_script += stringf("read_library \"%s\"; ", liberty_file.c_str()); if (!constr_file.empty()) - abc_script += stringf("read_constr -v %s; ", constr_file.c_str()); + abc_script += stringf("read_constr -v \"%s\"; ", constr_file.c_str()); } else if (!lut_costs.empty()) abc_script += stringf("read_lut %s/lutdefs.txt; ", tempdir_name.c_str()); @@ -1085,7 +1085,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin fclose(f); } - buffer = stringf("%s -s -f %s/abc.script 2>&1", exe_file.c_str(), tempdir_name.c_str()); + buffer = stringf("\"%s\" -s -f %s/abc.script 2>&1", exe_file.c_str(), tempdir_name.c_str()); log("Running ABC command: %s\n", replace_tempdir(buffer, tempdir_name, show_tempdir).c_str()); #ifndef YOSYS_LINK_ABC diff --git a/passes/techmap/abc9_exe.cc b/passes/techmap/abc9_exe.cc index 7dc0a364b..2f46c89f4 100644 --- a/passes/techmap/abc9_exe.cc +++ b/passes/techmap/abc9_exe.cc @@ -175,12 +175,12 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe if (!lut_costs.empty()) abc9_script += stringf("read_lut %s/lutdefs.txt; ", tempdir_name.c_str()); else if (!lut_file.empty()) - abc9_script += stringf("read_lut %s; ", lut_file.c_str()); + abc9_script += stringf("read_lut \"%s\"; ", lut_file.c_str()); else log_abort(); log_assert(!box_file.empty()); - abc9_script += stringf("read_box %s; ", box_file.c_str()); + abc9_script += stringf("read_box \"%s\"; ", box_file.c_str()); abc9_script += stringf("&read %s/input.xaig; &ps; ", tempdir_name.c_str()); if (!script_file.empty()) { @@ -264,7 +264,7 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe fclose(f); } - buffer = stringf("%s -s -f %s/abc.script 2>&1", exe_file.c_str(), tempdir_name.c_str()); + buffer = stringf("\"%s\" -s -f %s/abc.script 2>&1", exe_file.c_str(), tempdir_name.c_str()); log("Running ABC command: %s\n", replace_tempdir(buffer, tempdir_name, show_tempdir).c_str()); #ifndef YOSYS_LINK_ABC -- cgit v1.2.3 From 59facfa98c82ad019980ecbc92d74e01e0bc3e7a Mon Sep 17 00:00:00 2001 From: Lofty Date: Thu, 28 Jul 2022 13:05:34 +0100 Subject: stat: add option for machine-readable json output --- passes/cmds/stat.cc | 147 ++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 109 insertions(+), 38 deletions(-) (limited to 'passes') diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc index c858c8631..a4984597d 100644 --- a/passes/cmds/stat.cc +++ b/passes/cmds/stat.cc @@ -17,10 +17,13 @@ * */ +#include + #include "kernel/yosys.h" #include "kernel/celltypes.h" #include "passes/techmap/libparse.h" #include "kernel/cost.h" +#include "libs/json11/json11.hpp" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -32,14 +35,14 @@ struct statdata_t #define STAT_NUMERIC_MEMBERS STAT_INT_MEMBERS X(area) - #define X(_name) int _name; + #define X(_name) unsigned int _name; STAT_INT_MEMBERS #undef X double area; string tech; std::map techinfo; - std::map num_cells_by_type; + std::map num_cells_by_type; std::set unknown_cell_area; statdata_t operator+(const statdata_t &other) const @@ -53,7 +56,7 @@ struct statdata_t return sum; } - statdata_t operator*(int other) const + statdata_t operator*(unsigned int other) const { statdata_t sum = *this; #define X(_name) sum._name *= other; @@ -148,17 +151,17 @@ struct statdata_t void log_data(RTLIL::IdString mod_name, bool top_mod) { - log(" Number of wires: %6d\n", num_wires); - log(" Number of wire bits: %6d\n", num_wire_bits); - log(" Number of public wires: %6d\n", num_pub_wires); - log(" Number of public wire bits: %6d\n", num_pub_wire_bits); - log(" Number of memories: %6d\n", num_memories); - log(" Number of memory bits: %6d\n", num_memory_bits); - log(" Number of processes: %6d\n", num_processes); - log(" Number of cells: %6d\n", num_cells); + log(" Number of wires: %6u\n", num_wires); + log(" Number of wire bits: %6u\n", num_wire_bits); + log(" Number of public wires: %6u\n", num_pub_wires); + log(" Number of public wire bits: %6u\n", num_pub_wire_bits); + log(" Number of memories: %6u\n", num_memories); + log(" Number of memory bits: %6u\n", num_memory_bits); + log(" Number of processes: %6u\n", num_processes); + log(" Number of cells: %6u\n", num_cells); for (auto &it : num_cells_by_type) if (it.second) - log(" %-26s %6d\n", log_id(it.first), it.second); + log(" %-26s %6u\n", log_id(it.first), it.second); if (!unknown_cell_area.empty()) { log("\n"); @@ -173,13 +176,13 @@ struct statdata_t if (tech == "xilinx") { - int lut6_cnt = num_cells_by_type[ID(LUT6)]; - int lut5_cnt = num_cells_by_type[ID(LUT5)]; - int lut4_cnt = num_cells_by_type[ID(LUT4)]; - int lut3_cnt = num_cells_by_type[ID(LUT3)]; - int lut2_cnt = num_cells_by_type[ID(LUT2)]; - int lut1_cnt = num_cells_by_type[ID(LUT1)]; - int lc_cnt = 0; + unsigned int lut6_cnt = num_cells_by_type[ID(LUT6)]; + unsigned int lut5_cnt = num_cells_by_type[ID(LUT5)]; + unsigned int lut4_cnt = num_cells_by_type[ID(LUT4)]; + unsigned int lut3_cnt = num_cells_by_type[ID(LUT3)]; + unsigned int lut2_cnt = num_cells_by_type[ID(LUT2)]; + unsigned int lut1_cnt = num_cells_by_type[ID(LUT1)]; + unsigned int lc_cnt = 0; lc_cnt += lut6_cnt; @@ -221,12 +224,12 @@ struct statdata_t lc_cnt += (lut2_cnt + lut1_cnt + 1) / 2; log("\n"); - log(" Estimated number of LCs: %10d\n", lc_cnt); + log(" Estimated number of LCs: %10u\n", lc_cnt); } if (tech == "cmos") { - int tran_cnt = 0; + unsigned int tran_cnt = 0; bool tran_cnt_exact = true; auto &gate_costs = CellCosts::cmos_gate_cost(); @@ -243,20 +246,48 @@ struct statdata_t } log("\n"); - log(" Estimated number of transistors: %10d%s\n", tran_cnt, tran_cnt_exact ? "" : "+"); + log(" Estimated number of transistors: %10u%s\n", tran_cnt, tran_cnt_exact ? "" : "+"); } } + + void log_data_json(const char *mod_name, bool first_module) + { + if (!first_module) + log(",\n"); + log(" %s: {\n", json11::Json(mod_name).dump().c_str()); + log(" \"num_wires\": %u,\n", num_wires); + log(" \"num_wire_bits\": %u,\n", num_wire_bits); + log(" \"num_pub_wires\": %u,\n", num_pub_wires); + log(" \"num_pub_wire_bits\": %u,\n", num_pub_wire_bits); + log(" \"num_memories\": %u,\n", num_memories); + log(" \"num_memory_bits\": %u,\n", num_memory_bits); + log(" \"num_processes\": %u,\n", num_processes); + log(" \"num_cells\": %u,\n", num_cells); + log(" \"num_cells_by_type\": {\n"); + bool first_line = true; + for (auto &it : num_cells_by_type) + if (it.second) { + if (!first_line) + log(",\n"); + log(" %s: %u", json11::Json(log_id(it.first)).dump().c_str(), it.second); + first_line = false; + } + log("\n"); + log(" }\n"); + log(" }"); + } }; -statdata_t hierarchy_worker(std::map &mod_stat, RTLIL::IdString mod, int level) +statdata_t hierarchy_worker(std::map &mod_stat, RTLIL::IdString mod, int level, bool quiet = false) { statdata_t mod_data = mod_stat.at(mod); - std::map num_cells_by_type; + std::map num_cells_by_type; num_cells_by_type.swap(mod_data.num_cells_by_type); for (auto &it : num_cells_by_type) if (mod_stat.count(it.first) > 0) { - log(" %*s%-*s %6d\n", 2*level, "", 26-2*level, log_id(it.first), it.second); + if (!quiet) + log(" %*s%-*s %6u\n", 2*level, "", 26-2*level, log_id(it.first), it.second); mod_data = mod_data + hierarchy_worker(mod_stat, it.first, level+1) * it.second; mod_data.num_cells -= it.second; } else { @@ -314,12 +345,16 @@ struct StatPass : public Pass { log(" annotate internal cell types with their word width.\n"); log(" e.g. $add_8 for an 8 bit wide $add cell.\n"); log("\n"); + log(" -json\n"); + log(" output the statistics in a machine-readable JSON format.\n"); + log(" this is output to the console; use \"tee\" to output to a file.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { log_header(design, "Printing statistics.\n"); - bool width_mode = false; + bool width_mode = false, json_mode = false; RTLIL::Module *top_mod = nullptr; std::map mod_stat; dict cell_area; @@ -348,13 +383,27 @@ struct StatPass : public Pass { top_mod = design->module(RTLIL::escape_id(args[++argidx])); continue; } + if (args[argidx] == "-json") { + json_mode = true; + continue; + } break; } extra_args(args, argidx, design); - if (techname != "" && techname != "xilinx" && techname != "cmos") + if (techname != "" && techname != "xilinx" && techname != "cmos" && !json_mode) log_cmd_error("Unsupported technology: '%s'\n", techname.c_str()); + if (json_mode) { + log("{\n"); + log(" \"creator\": %s,\n", json11::Json(yosys_version_str).dump().c_str()); + std::stringstream invocation; + std::copy(args.begin(), args.end(), std::ostream_iterator(invocation, " ")); + log(" \"invocation\": %s,\n", json11::Json(invocation.str()).dump().c_str()); + log(" \"modules\": {\n"); + } + + bool first_module = true; for (auto mod : design->selected_modules()) { if (!top_mod && design->full_selection()) @@ -364,23 +413,40 @@ struct StatPass : public Pass { statdata_t data(design, mod, width_mode, cell_area, techname); mod_stat[mod->name] = data; + if (json_mode) { + data.log_data_json(mod->name.c_str(), first_module); + first_module = false; + } else { + log("\n"); + log("=== %s%s ===\n", log_id(mod->name), design->selected_whole_module(mod->name) ? "" : " (partially selected)"); + log("\n"); + data.log_data(mod->name, false); + } + } + + if (json_mode) { log("\n"); - log("=== %s%s ===\n", log_id(mod->name), design->selected_whole_module(mod->name) ? "" : " (partially selected)"); - log("\n"); - data.log_data(mod->name, false); + log(" },\n"); } - if (top_mod != nullptr && GetSize(mod_stat) > 1) + if (top_mod != nullptr) { - log("\n"); - log("=== design hierarchy ===\n"); - log("\n"); + if (!json_mode && GetSize(mod_stat) > 1) { + log("\n"); + log("=== design hierarchy ===\n"); + log("\n"); + log(" %-28s %6d\n", log_id(top_mod->name), 1); + } - log(" %-28s %6d\n", log_id(top_mod->name), 1); - statdata_t data = hierarchy_worker(mod_stat, top_mod->name, 0); + statdata_t data = hierarchy_worker(mod_stat, top_mod->name, 0, /*quiet=*/json_mode); + + if (json_mode) + data.log_data_json("design", true); + else if (GetSize(mod_stat) > 1) { + log("\n"); + data.log_data(top_mod->name, true); + } - log("\n"); - data.log_data(top_mod->name, true); design->scratchpad_set_int("stat.num_wires", data.num_wires); design->scratchpad_set_int("stat.num_wire_bits", data.num_wire_bits); design->scratchpad_set_int("stat.num_pub_wires", data.num_pub_wires); @@ -392,6 +458,11 @@ struct StatPass : public Pass { design->scratchpad_set_int("stat.area", data.area); } + if (json_mode) { + log("\n"); + log("}\n"); + } + log("\n"); } } StatPass; -- cgit v1.2.3 From c0063288d699f4f3edf5e0ff6ee1bd5cfa9ac884 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 21 Jul 2022 14:22:15 +0200 Subject: Add the $anyinit cell and the formalff pass These can be used to protect undefined flip-flop initialization values from optimizations that are not sound for formal verification and can help mapping all solver-provided values in witness traces for flows that use different backends simultaneously. --- passes/cmds/show.cc | 1 + passes/fsm/fsm_detect.cc | 1 + passes/hierarchy/submod.cc | 1 + passes/opt/opt_clean.cc | 2 + passes/sat/Makefile.inc | 1 + passes/sat/formalff.cc | 192 +++++++++++++++++++++++++++++++++++++++++++++ passes/sat/sim.cc | 2 +- 7 files changed, 199 insertions(+), 1 deletion(-) create mode 100644 passes/sat/formalff.cc (limited to 'passes') diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc index 43deba47b..4d5605932 100644 --- a/passes/cmds/show.cc +++ b/passes/cmds/show.cc @@ -574,6 +574,7 @@ struct ShowWorker { ct.setup_internals(); ct.setup_internals_mem(); + ct.setup_internals_anyinit(); ct.setup_stdcells(); ct.setup_stdcells_mem(); ct.setup_design(design); diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc index a2d38a0bd..f829714c4 100644 --- a/passes/fsm/fsm_detect.cc +++ b/passes/fsm/fsm_detect.cc @@ -280,6 +280,7 @@ struct FsmDetectPass : public Pass { CellTypes ct; ct.setup_internals(); + ct.setup_internals_anyinit(); ct.setup_internals_mem(); ct.setup_stdcells(); ct.setup_stdcells_mem(); diff --git a/passes/hierarchy/submod.cc b/passes/hierarchy/submod.cc index 845dc850f..c0c40671d 100644 --- a/passes/hierarchy/submod.cc +++ b/passes/hierarchy/submod.cc @@ -260,6 +260,7 @@ struct SubmodWorker } ct.setup_internals(); + ct.setup_internals_anyinit(); ct.setup_internals_mem(); ct.setup_stdcells(); ct.setup_stdcells_mem(); diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index cb2c261c4..dde7c5299 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -633,6 +633,7 @@ struct OptCleanPass : public Pass { keep_cache.reset(design); ct_reg.setup_internals_mem(); + ct_reg.setup_internals_anyinit(); ct_reg.setup_stdcells_mem(); ct_all.setup(design); @@ -694,6 +695,7 @@ struct CleanPass : public Pass { keep_cache.reset(design); ct_reg.setup_internals_mem(); + ct_reg.setup_internals_anyinit(); ct_reg.setup_stdcells_mem(); ct_all.setup(design); diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc index da6d49433..ebe3dc536 100644 --- a/passes/sat/Makefile.inc +++ b/passes/sat/Makefile.inc @@ -10,6 +10,7 @@ OBJS += passes/sat/expose.o OBJS += passes/sat/assertpmux.o OBJS += passes/sat/clk2fflogic.o OBJS += passes/sat/async2sync.o +OBJS += passes/sat/formalff.o OBJS += passes/sat/supercover.o OBJS += passes/sat/fmcombine.o OBJS += passes/sat/mutate.o diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc new file mode 100644 index 000000000..fe6f98c16 --- /dev/null +++ b/passes/sat/formalff.cc @@ -0,0 +1,192 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Jannis Harder + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/yosys.h" +#include "kernel/sigtools.h" +#include "kernel/ffinit.h" +#include "kernel/ff.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct FormalFfPass : public Pass { + FormalFfPass() : Pass("formalff", "prepare FFs for formal") { } + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" formalff [options] [selection]\n"); + log("\n"); + log("This pass transforms clocked flip-flops to prepare a design for formal\n"); + log("verification. If a design contains latches and/or multiple different clocks run\n"); + log("the async2sync or clk2fflogic passes before using this pass.\n"); + log("\n"); + log(" -clk2ff\n"); + log(" Replace all clocked flip-flops with $ff cells that use the implicit\n"); + log(" global clock. This assumes, without checking, that the design uses a\n"); + log(" single global clock. If that is not the case, the clk2fflogic pass\n"); + log(" should be used instead.\n"); + log("\n"); + log(" -ff2anyinit\n"); + log(" Replace uninitialized bits of $ff cells with $anyinit cells. An\n"); + log(" $anyinit cell behaves exactly like an $ff cell with an undefined\n"); + log(" initialization value. The difference is that $anyinit inhibits\n"); + log(" don't-care optimizations and is used to track solver-provided values\n"); + log(" in witness traces.\n"); + log("\n"); + log(" If combined with -clk2ff this also affects newly created $ff cells.\n"); + log("\n"); + log(" -anyinit2ff\n"); + log(" Replaces $anyinit cells with uninitialized $ff cells. This performs the\n"); + log(" reverse of -ff2anyinit and can be used, before running a backend pass\n"); + log(" (or similar) that is not yet aware of $anyinit cells.\n"); + log("\n"); + log(" Note that after running -anyinit2ff, in general, performing don't-care\n"); + log(" optimizations is not sound in a formal verification setting.\n"); + log("\n"); + log(" -fine\n"); + log(" Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for\n"); + log(" -anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit.\n"); + log("\n"); + + // TODO: An option to check whether all FFs use the same clock before changing it to the global clock + } + void execute(std::vector args, RTLIL::Design *design) override + { + bool flag_clk2ff = false; + bool flag_ff2anyinit = false; + bool flag_anyinit2ff = false; + bool flag_fine = false; + + log_header(design, "Executing FORMALFF pass.\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + if (args[argidx] == "-clk2ff") { + flag_clk2ff = true; + continue; + } + if (args[argidx] == "-ff2anyinit") { + flag_ff2anyinit = true; + continue; + } + if (args[argidx] == "-anyinit2ff") { + flag_anyinit2ff = true; + continue; + } + if (args[argidx] == "-fine") { + flag_fine = true; + continue; + } + break; + } + extra_args(args, argidx, design); + + if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff)) + log_cmd_error("One of the options -clk2ff, -ff2anyinit, or -anyinit2ff must be specified.\n"); + + if (flag_ff2anyinit && flag_anyinit2ff) + log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n"); + + if (flag_fine && !flag_anyinit2ff) + log_cmd_error("The option -fine requries the -anyinit2ff option.\n"); + + if (flag_fine && flag_clk2ff) + log_cmd_error("The options -fine and -clk2ff are exclusive.\n"); + + for (auto module : design->selected_modules()) + { + SigMap sigmap(module); + FfInitVals initvals(&sigmap, module); + + + for (auto cell : module->selected_cells()) + { + if (flag_anyinit2ff && cell->type == ID($anyinit)) + { + FfData ff(&initvals, cell); + ff.remove(); + ff.is_anyinit = false; + ff.is_fine = flag_fine; + if (flag_fine) + for (int i = 0; i < ff.width; i++) + ff.slice({i}).emit(); + else + ff.emit(); + + continue; + } + + if (!RTLIL::builtin_ff_cell_types().count(cell->type)) + continue; + + FfData ff(&initvals, cell); + bool emit = false; + + if (flag_clk2ff && ff.has_clk) { + if (ff.sig_clk.is_fully_const()) + log_error("Const CLK on %s (%s) from module %s, run async2sync first.\n", + log_id(cell), log_id(cell->type), log_id(module)); + + ff.unmap_ce_srst(); + ff.has_clk = false; + ff.has_gclk = true; + emit = true; + } + + if (!ff.has_gclk) { + continue; + } + + if (flag_ff2anyinit && !ff.val_init.is_fully_def()) + { + ff.remove(); + emit = false; + + int cursor = 0; + while (cursor < ff.val_init.size()) + { + bool is_anyinit = ff.val_init[cursor] == State::Sx; + std::vector bits; + bits.push_back(cursor++); + while (cursor < ff.val_init.size() && (ff.val_init[cursor] == State::Sx) == is_anyinit) + bits.push_back(cursor++); + + if ((int)bits.size() == ff.val_init.size()) { + // This check is only to make the private names more helpful for debugging + ff.is_anyinit = true; + emit = true; + break; + } + + auto slice = ff.slice(bits); + slice.is_anyinit = is_anyinit; + slice.emit(); + } + } + + if (emit) + ff.emit(); + } + } + } +} FormalFfPass; + +PRIVATE_NAMESPACE_END diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 53644c6b7..ea64dce06 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -231,7 +231,7 @@ struct SimInstance } } - if (RTLIL::builtin_ff_cell_types().count(cell->type)) { + if (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit)) { FfData ff_data(nullptr, cell); ff_state_t ff; ff.past_d = Const(State::Sx, ff_data.width); -- cgit v1.2.3 From a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 15:49:51 +0200 Subject: formalff: Set new replaced_by_gclk attribute on removed dff's clks This attribute can be used by formal backends to indicate which clocks were mapped to the global clock. Update the btor and smt2 backend which already handle clock inputs to understand this attribute. --- passes/sat/formalff.cc | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'passes') diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc index fe6f98c16..0c85c3442 100644 --- a/passes/sat/formalff.cc +++ b/passes/sat/formalff.cc @@ -145,6 +145,28 @@ struct FormalFfPass : public Pass { log_error("Const CLK on %s (%s) from module %s, run async2sync first.\n", log_id(cell), log_id(cell->type), log_id(module)); + auto clk_wire = ff.sig_clk.is_wire() ? ff.sig_clk.as_wire() : nullptr; + + if (clk_wire == nullptr) { + clk_wire = module->addWire(NEW_ID); + module->connect(RTLIL::SigBit(clk_wire), ff.sig_clk); + } + + auto clk_polarity = ff.pol_clk ? State::S1 : State::S0; + + std::string attribute = clk_wire->get_string_attribute(ID::replaced_by_gclk); + + auto &attr = clk_wire->attributes[ID::replaced_by_gclk]; + + if (!attr.empty() && attr != clk_polarity) + log_error("CLK %s on %s (%s) from module %s also used with opposite polarity, run clk2fflogic instead.\n", + log_id(clk_wire), log_id(cell), log_id(cell->type), log_id(module)); + + attr = clk_polarity; + clk_wire->set_bool_attribute(ID::keep); + + // TODO propagate the replaced_by_gclk attribute upwards throughout the hierarchy + ff.unmap_ce_srst(); ff.has_clk = false; ff.has_gclk = true; -- cgit v1.2.3 From 95db5a9d3899973c0c7bcfa887f8404ac017d53f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 5 Aug 2022 15:43:08 +0200 Subject: formalff: New -setundef option Find FFs with undefined initialization values for which changing the initialization does not change the observable behavior and initialize them. For -ff2anyinit, this reduces the number of generated $anyinit cells that drive wires with private names. --- passes/sat/formalff.cc | 335 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 335 insertions(+) (limited to 'passes') diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc index 0c85c3442..209486a37 100644 --- a/passes/sat/formalff.cc +++ b/passes/sat/formalff.cc @@ -21,10 +21,302 @@ #include "kernel/sigtools.h" #include "kernel/ffinit.h" #include "kernel/ff.h" +#include "kernel/modtools.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN + +// Finds signal values with known constant or known unused values in the initial state +struct InitValWorker +{ + Module *module; + + ModWalker modwalker; + SigMap &sigmap; + FfInitVals initvals; + + dict initconst_bits; + dict used_bits; + + InitValWorker(Module *module) : module(module), modwalker(module->design), sigmap(modwalker.sigmap) + { + modwalker.setup(module); + initvals.set(&modwalker.sigmap, module); + + for (auto wire : module->wires()) + if (wire->name.isPublic() || wire->get_bool_attribute(ID::keep)) + for (auto bit : SigSpec(wire)) + used_bits[sigmap(bit)] = true; + } + + // Sign/Zero-extended indexing of individual port bits + static SigBit bit_in_port(RTLIL::Cell *cell, RTLIL::IdString port, RTLIL::IdString sign, int index) + { + auto sig_port = cell->getPort(port); + if (index < GetSize(sig_port)) + return sig_port[index]; + else if (cell->getParam(sign).as_bool()) + return GetSize(sig_port) > 0 ? sig_port[GetSize(sig_port) - 1] : State::Sx; + else + return State::S0; + } + + // Has the signal a known constant value in the initial state? + // + // For sync-only FFs outputs, this is their initval. For logic loops, + // multiple drivers or unknown cells this is Sx. For a small number of + // handled cells we recurse through their inputs. All results are cached. + RTLIL::State initconst(SigBit bit) + { + sigmap.apply(bit); + + if (!bit.is_wire()) + return bit.data; + + auto it = initconst_bits.find(bit); + if (it != initconst_bits.end()) + return it->second; + + // Setting this temporarily to x takes care of any logic loops + initconst_bits[bit] = State::Sx; + + pool portbits; + modwalker.get_drivers(portbits, {bit}); + + if (portbits.size() != 1) + return State::Sx; + + ModWalker::PortBit portbit = *portbits.begin(); + RTLIL::Cell *cell = portbit.cell; + + if (RTLIL::builtin_ff_cell_types().count(cell->type)) + { + FfData ff(&initvals, cell); + + if (ff.has_aload || ff.has_sr || ff.has_arst || (!ff.has_clk && !ff.has_gclk)) { + for (auto bit_q : ff.sig_q) { + initconst_bits[sigmap(bit_q)] = State::Sx; + } + return State::Sx; + } + + for (int i = 0; i < ff.width; i++) { + initconst_bits[sigmap(ff.sig_q[i])] = ff.val_init[i]; + } + + return ff.val_init[portbit.offset]; + } + + if (cell->type.in(ID($mux), ID($and), ID($or), ID($eq), ID($eqx), ID($initstate))) + { + if (cell->type == ID($mux)) + { + SigBit sig_s = sigmap(cell->getPort(ID::S)); + State init_s = initconst(sig_s); + State init_y; + + if (init_s == State::S0) { + init_y = initconst(cell->getPort(ID::A)[portbit.offset]); + } else if (init_s == State::S1) { + init_y = initconst(cell->getPort(ID::B)[portbit.offset]); + } else { + State init_a = initconst(cell->getPort(ID::A)[portbit.offset]); + State init_b = initconst(cell->getPort(ID::B)[portbit.offset]); + init_y = init_a == init_b ? init_a : State::Sx; + } + initconst_bits[bit] = init_y; + return init_y; + } + + if (cell->type.in(ID($and), ID($or))) + { + State init_a = initconst(bit_in_port(cell, ID::A, ID::A_SIGNED, portbit.offset)); + State init_b = initconst(bit_in_port(cell, ID::B, ID::B_SIGNED, portbit.offset)); + State init_y; + if (init_a == init_b) + init_y = init_a; + else if (cell->type == ID($and) && (init_a == State::S0 || init_b == State::S0)) + init_y = State::S0; + else if (cell->type == ID($or) && (init_a == State::S1 || init_b == State::S1)) + init_y = State::S1; + else + init_y = State::Sx; + + initconst_bits[bit] = init_y; + return init_y; + } + + if (cell->type.in(ID($eq), ID($eqx))) // Treats $eqx as $eq + { + if (portbit.offset > 0) { + initconst_bits[bit] = State::S0; + return State::S0; + } + + SigSpec sig_a = cell->getPort(ID::A); + SigSpec sig_b = cell->getPort(ID::B); + + State init_y = State::S1; + + for (int i = 0; init_y != State::S0 && i < GetSize(sig_a); i++) { + State init_ai = initconst(bit_in_port(cell, ID::A, ID::A_SIGNED, i)); + if (init_ai == State::Sx) { + init_y = State::Sx; + continue; + } + State init_bi = initconst(bit_in_port(cell, ID::B, ID::B_SIGNED, i)); + if (init_bi == State::Sx) + init_y = State::Sx; + else if (init_ai != init_bi) + init_y = State::S0; + } + + initconst_bits[bit] = init_y; + return init_y; + } + + if (cell->type == ID($initstate)) + { + initconst_bits[bit] = State::S1; + return State::S1; + } + + log_assert(false); + } + + return State::Sx; + } + + RTLIL::Const initconst(SigSpec sig) + { + std::vector bits; + for (auto bit : sig) + bits.push_back(initconst(bit)); + return bits; + } + + // Is the initial value of this signal used? + // + // An initial value of a signal is considered as used if it a) aliases a + // wire with a public name, an output wire or with a keep attribute b) + // combinationally drives such a wire or c) drive an input to an unknown + // cell. + // + // This recurses into driven cells for a small number of known handled + // celltypes. Results are cached and initconst is used to detect unused + // inputs for the handled celltypes. + bool is_initval_used(SigBit bit) + { + if (!bit.is_wire()) + return false; + + auto it = used_bits.find(bit); + if (it != used_bits.end()) + return it->second; + + used_bits[bit] = true; // Temporarily set to guard against logic loops + + pool portbits; + modwalker.get_consumers(portbits, {bit}); + + for (auto portbit : portbits) { + RTLIL::Cell *cell = portbit.cell; + if (!cell->type.in(ID($mux), ID($and), ID($or), ID($mem_v2)) && !RTLIL::builtin_ff_cell_types().count(cell->type)) { + return true; + } + } + + for (auto portbit : portbits) + { + RTLIL::Cell *cell = portbit.cell; + if (RTLIL::builtin_ff_cell_types().count(cell->type)) + { + FfData ff(&initvals, cell); + if (ff.has_aload || ff.has_sr || ff.has_arst || ff.has_gclk || !ff.has_clk) + return true; + if (ff.has_ce && initconst(ff.sig_ce.as_bit()) == (ff.pol_ce ? State::S0 : State::S1)) + continue; + if (ff.has_srst && initconst(ff.sig_ce.as_bit()) == (ff.pol_srst ? State::S1 : State::S0)) + continue; + + return true; + } + else if (cell->type == ID($mux)) + { + State init_s = initconst(cell->getPort(ID::S).as_bit()); + if (init_s == State::S0 && portbit.port == ID::B) + continue; + if (init_s == State::S1 && portbit.port == ID::A) + continue; + auto sig_y = cell->getPort(ID::Y); + + if (is_initval_used(sig_y[portbit.offset])) + return true; + } + else if (cell->type.in(ID($and), ID($or))) + { + auto sig_a = cell->getPort(ID::A); + auto sig_b = cell->getPort(ID::B); + auto sig_y = cell->getPort(ID::Y); + if (GetSize(sig_y) != GetSize(sig_a) || GetSize(sig_y) != GetSize(sig_b)) + return true; // TODO handle more of this + State absorbing = cell->type == ID($and) ? State::S0 : State::S1; + if (portbit.port == ID::A && initconst(sig_b[portbit.offset]) == absorbing) + continue; + if (portbit.port == ID::B && initconst(sig_a[portbit.offset]) == absorbing) + continue; + + if (is_initval_used(sig_y[portbit.offset])) + return true; + } + else if (cell->type == ID($mem_v2)) + { + // TODO Use mem.h instead to uniformily cover all cases, most + // likely requires processing all memories when initializing + // the worker + if (!portbit.port.in(ID::WR_DATA, ID::WR_ADDR, ID::RD_ADDR)) + return true; + + if (portbit.port == ID::WR_DATA) + { + if (initconst(cell->getPort(ID::WR_EN)[portbit.offset]) == State::S0) + continue; + } + else if (portbit.port == ID::WR_ADDR) + { + int port = portbit.offset / cell->getParam(ID::ABITS).as_int(); + auto sig_en = cell->getPort(ID::WR_EN); + int width = cell->getParam(ID::WIDTH).as_int(); + + for (int i = port * width; i < (port + 1) * width; i++) + if (initconst(sig_en[i]) != State::S0) + return true; + + continue; + } + else if (portbit.port == ID::RD_ADDR) + { + int port = portbit.offset / cell->getParam(ID::ABITS).as_int(); + auto sig_en = cell->getPort(ID::RD_EN); + + if (initconst(sig_en[port]) != State::S0) + return true; + + continue; + } + else + return true; + } + else + log_assert(false); + } + + used_bits[bit] = false; + return false; + } +}; + struct FormalFfPass : public Pass { FormalFfPass() : Pass("formalff", "prepare FFs for formal") { } void help() override @@ -64,6 +356,12 @@ struct FormalFfPass : public Pass { log(" Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for\n"); log(" -anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit.\n"); log("\n"); + log(" -setundef\n"); + log(" Find FFs with undefined initialization values for which changing the\n"); + log(" initialization does not change the observable behavior and initialize\n"); + log(" them. For -ff2anyinit, this reduces the number of generated $anyinit\n"); + log(" cells that drive wires with private names.\n"); + log("\n"); // TODO: An option to check whether all FFs use the same clock before changing it to the global clock } @@ -73,6 +371,7 @@ struct FormalFfPass : public Pass { bool flag_ff2anyinit = false; bool flag_anyinit2ff = false; bool flag_fine = false; + bool flag_setundef = false; log_header(design, "Executing FORMALFF pass.\n"); @@ -95,6 +394,10 @@ struct FormalFfPass : public Pass { flag_fine = true; continue; } + if (args[argidx] == "-setundef") { + flag_setundef = true; + continue; + } break; } extra_args(args, argidx, design); @@ -113,6 +416,38 @@ struct FormalFfPass : public Pass { for (auto module : design->selected_modules()) { + if (flag_setundef) + { + InitValWorker worker(module); + + for (auto cell : module->selected_cells()) + { + if (RTLIL::builtin_ff_cell_types().count(cell->type)) + { + FfData ff(&worker.initvals, cell); + if (ff.has_aload || ff.has_sr || ff.has_arst || ff.val_init.is_fully_def()) + continue; + + if (ff.has_ce && // CE can make the initval stick around + worker.initconst(ff.sig_ce.as_bit()) != (ff.pol_ce ? State::S1 : State::S0) && // unless it's known active + (!ff.has_srst || ff.ce_over_srst || + worker.initconst(ff.sig_srst.as_bit()) != (ff.pol_srst ? State::S1 : State::S0))) // or a srst with priority is known active + continue; + + auto before = ff.val_init; + for (int i = 0; i < ff.width; i++) + if (ff.val_init[i] == State::Sx && !worker.is_initval_used(ff.sig_q[i])) + ff.val_init[i] = State::S0; + + if (ff.val_init != before) { + log("Setting unused undefined initial value of %s.%s (%s) from %s to %s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_const(before), log_const(ff.val_init)); + worker.initvals.set_init(ff.sig_q, ff.val_init); + } + } + } + } SigMap sigmap(module); FfInitVals initvals(&sigmap, module); -- cgit v1.2.3 From 428ad5b9fd1861d7943c29e7927969a02b14926b Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 20 Jul 2022 11:31:06 +0200 Subject: wreduce: Keep more x-bits with -keepdc --- passes/opt/wreduce.cc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'passes') diff --git a/passes/opt/wreduce.cc b/passes/opt/wreduce.cc index 08ab6de6f..8fd4c788c 100644 --- a/passes/opt/wreduce.cc +++ b/passes/opt/wreduce.cc @@ -166,8 +166,8 @@ struct WreduceWorker for (int i = GetSize(sig_q)-1; i >= 0; i--) { - if (zero_ext && sig_d[i] == State::S0 && (initval[i] == State::S0 || initval[i] == State::Sx) && - (!has_reset || i >= GetSize(rst_value) || rst_value[i] == State::S0 || rst_value[i] == State::Sx)) { + if (zero_ext && sig_d[i] == State::S0 && (initval[i] == State::S0 || (!config->keepdc && initval[i] == State::Sx)) && + (!has_reset || i >= GetSize(rst_value) || rst_value[i] == State::S0 || (!config->keepdc && rst_value[i] == State::Sx))) { module->connect(sig_q[i], State::S0); initvals.remove_init(sig_q[i]); sig_d.remove(i); @@ -175,8 +175,8 @@ struct WreduceWorker continue; } - if (sign_ext && i > 0 && sig_d[i] == sig_d[i-1] && initval[i] == initval[i-1] && - (!has_reset || i >= GetSize(rst_value) || rst_value[i] == rst_value[i-1])) { + if (sign_ext && i > 0 && sig_d[i] == sig_d[i-1] && initval[i] == initval[i-1] && (!config->keepdc || initval[i] != State::Sx) && + (!has_reset || i >= GetSize(rst_value) || (rst_value[i] == rst_value[i-1] && (!config->keepdc || rst_value[i] != State::Sx)))) { module->connect(sig_q[i], sig_q[i-1]); initvals.remove_init(sig_q[i]); sig_d.remove(i); -- cgit v1.2.3 From 0cdb14df41be53f770390d6ad01cf650f1bc49da Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 15:36:29 +0200 Subject: setundef: Do not add anyseq / anyconst to unused memory port clocks Instead set those unused clocks to zero. --- passes/cmds/setundef.cc | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'passes') diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc index a078b0b1c..590a7eb1d 100644 --- a/passes/cmds/setundef.cc +++ b/passes/cmds/setundef.cc @@ -20,6 +20,7 @@ #include "kernel/register.h" #include "kernel/celltypes.h" #include "kernel/sigtools.h" +#include "kernel/mem.h" #include "kernel/rtlil.h" #include "kernel/log.h" @@ -478,6 +479,29 @@ struct SetundefPass : public Pass { log_assert(ffbits.empty()); } + if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST) + { + // Do not add anyseq / anyconst to unused memory port clocks + std::vector memories = Mem::get_selected_memories(module); + for (auto &mem : memories) { + bool changed = false; + for (auto &rd_port : mem.rd_ports) { + if (!rd_port.clk_enable && rd_port.clk.is_fully_undef()) { + changed = true; + rd_port.clk = State::S0; + } + } + for (auto &wr_port : mem.rd_ports) { + if (!wr_port.clk_enable && wr_port.clk.is_fully_undef()) { + changed = true; + wr_port.clk = State::S0; + } + } + if (changed) + mem.emit(); + } + } + module->rewrite_sigspecs(worker); if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST) -- cgit v1.2.3 From a2f9ebe43a287233917947851e0d0dff803a4675 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 16:07:28 +0200 Subject: memory_map: Add -formal option This maps memories for a global clock based formal verification flow. This implies -keepdc, uses $ff cells for ROMs and sets hdlname attributes. --- passes/memory/memory_map.cc | 84 ++++++++++++++++++++++++++++++++++++--------- 1 file changed, 67 insertions(+), 17 deletions(-) (limited to 'passes') diff --git a/passes/memory/memory_map.cc b/passes/memory/memory_map.cc index fd5b1f1ad..e2f74c2e1 100644 --- a/passes/memory/memory_map.cc +++ b/passes/memory/memory_map.cc @@ -32,6 +32,7 @@ struct MemoryMapWorker bool attr_icase = false; bool rom_only = false; bool keepdc = false; + bool formal = false; dict> attributes; RTLIL::Design *design; @@ -151,6 +152,8 @@ struct MemoryMapWorker // all write ports must share the same clock RTLIL::SigSpec refclock; bool refclock_pol = false; + bool async_wr = false; + bool static_only = true; for (int i = 0; i < GetSize(mem.wr_ports); i++) { auto &port = mem.wr_ports[i]; if (port.en.is_fully_const() && !port.en.as_bool()) { @@ -164,10 +167,20 @@ struct MemoryMapWorker static_ports.insert(i); continue; } - log("Not mapping memory %s in module %s (write port %d has no clock).\n", - mem.memid.c_str(), module->name.c_str(), i); - return; + static_only = false; + if (GetSize(refclock) != 0) + log("Not mapping memory %s in module %s (mixed clocked and async write ports).\n", + mem.memid.c_str(), module->name.c_str()); + if (!formal) + log("Not mapping memory %s in module %s (write port %d has no clock).\n", + mem.memid.c_str(), module->name.c_str(), i); + async_wr = true; + continue; } + static_only = false; + if (async_wr) + log("Not mapping memory %s in module %s (mixed clocked and async write ports).\n", + mem.memid.c_str(), module->name.c_str()); if (refclock.size() == 0) { refclock = port.clk; refclock_pol = port.clk_polarity; @@ -185,6 +198,8 @@ struct MemoryMapWorker std::vector data_reg_in(1 << abits); std::vector data_reg_out(1 << abits); + std::vector &data_read = async_wr ? data_reg_in : data_reg_out; + int count_static = 0; for (int i = 0; i < mem.size; i++) @@ -194,24 +209,36 @@ struct MemoryMapWorker SigSpec w_init = init_data.extract(i*mem.width, mem.width); if (static_cells_map.count(addr) > 0) { - data_reg_out[idx] = static_cells_map[addr]; + data_read[idx] = static_cells_map[addr]; count_static++; } - else if (mem.wr_ports.empty() && (!keepdc || w_init.is_fully_def())) + else if (static_only && (!keepdc || w_init.is_fully_def())) { - data_reg_out[idx] = w_init; + data_read[idx] = w_init; } else { - RTLIL::Cell *c = module->addCell(genid(mem.memid, "", addr), ID($dff)); - c->parameters[ID::WIDTH] = mem.width; - if (GetSize(refclock) != 0) { + RTLIL::Cell *c; + auto ff_id = genid(mem.memid, "", addr); + + if (static_only) { + // non-static part is a ROM, we only reach this with keepdc + if (formal) { + c = module->addCell(ff_id, ID($ff)); + } else { + c = module->addCell(ff_id, ID($dff)); + c->parameters[ID::CLK_POLARITY] = RTLIL::Const(RTLIL::State::S1); + c->setPort(ID::CLK, RTLIL::SigSpec(RTLIL::State::S0)); + } + } else if (async_wr) { + log_assert(formal); // General async write not implemented yet, checked against above + c = module->addCell(ff_id, ID($ff)); + } else { + c = module->addCell(ff_id, ID($dff)); c->parameters[ID::CLK_POLARITY] = RTLIL::Const(refclock_pol); c->setPort(ID::CLK, refclock); - } else { - c->parameters[ID::CLK_POLARITY] = RTLIL::Const(RTLIL::State::S1); - c->setPort(ID::CLK, RTLIL::SigSpec(RTLIL::State::S0)); } + c->parameters[ID::WIDTH] = mem.width; RTLIL::Wire *w_in = module->addWire(genid(mem.memid, "", addr, "$d"), mem.width); data_reg_in[idx] = w_in; @@ -223,18 +250,27 @@ struct MemoryMapWorker RTLIL::Wire *w_out = module->addWire(w_out_name, mem.width); + if (formal && mem.packed && mem.cell->name.c_str()[0] == '\\') { + auto hdlname = mem.cell->get_hdlname_attribute(); + if (hdlname.empty()) + hdlname.push_back(mem.cell->name.c_str() + 1); + hdlname.push_back(stringf("[%d]", addr)); + w_out->set_hdlname_attribute(hdlname); + } + if (!w_init.is_fully_undef()) w_out->attributes[ID::init] = w_init.as_const(); data_reg_out[idx] = w_out; c->setPort(ID::Q, w_out); - if (mem.wr_ports.empty()) + if (static_only) module->connect(RTLIL::SigSig(w_in, w_out)); } } - log(" created %d $dff cells and %d static cells of width %d.\n", mem.size-count_static, count_static, mem.width); + log(" created %d %s cells and %d static cells of width %d.\n", + mem.size-count_static, formal && (static_only || async_wr) ? "$ff" : "$dff", count_static, mem.width); int count_dff = 0, count_mux = 0, count_wrmux = 0; @@ -272,13 +308,13 @@ struct MemoryMapWorker } for (int j = 0; j < (1 << abits); j++) - if (data_reg_out[j] != SigSpec()) - module->connect(RTLIL::SigSig(rd_signals[j >> port.wide_log2].extract((j & ((1 << port.wide_log2) - 1)) * mem.width, mem.width), data_reg_out[j])); + if (data_read[j] != SigSpec()) + module->connect(RTLIL::SigSig(rd_signals[j >> port.wide_log2].extract((j & ((1 << port.wide_log2) - 1)) * mem.width, mem.width), data_read[j])); } log(" read interface: %d $dff and %d $mux cells.\n", count_dff, count_mux); - if (!mem.wr_ports.empty()) + if (!static_only) { for (int i = 0; i < mem.size; i++) { @@ -387,12 +423,19 @@ struct MemoryMapPass : public Pass { log(" -keepdc\n"); log(" when mapping ROMs, keep x-bits shared across read ports.\n"); log("\n"); + log(" -formal\n"); + log(" map memories for a global clock based formal verification flow.\n"); + log(" This implies -keepdc, uses $ff cells for ROMs and sets hdlname\n"); + log(" attributes. It also has limited support for async write ports\n"); + log(" as generated by clk2fflogic.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { bool attr_icase = false; bool rom_only = false; bool keepdc = false; + bool formal = false; dict> attributes; log_header(design, "Executing MEMORY_MAP pass (converting memories to logic and flip-flops).\n"); @@ -439,6 +482,12 @@ struct MemoryMapPass : public Pass { keepdc = true; continue; } + if (args[argidx] == "-formal") + { + formal = true; + keepdc = true; + continue; + } break; } extra_args(args, argidx, design); @@ -449,6 +498,7 @@ struct MemoryMapPass : public Pass { worker.attributes = attributes; worker.rom_only = rom_only; worker.keepdc = keepdc; + worker.formal = formal; worker.run(); } } -- cgit v1.2.3 From 65145db7e7bec998a194aa0f6335de50df00e550 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 3 Aug 2022 17:27:06 +0200 Subject: rename: Add -witness mode --- passes/cmds/rename.cc | 81 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 81 insertions(+) (limited to 'passes') diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index b49d5cdc2..45576c91c 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -106,6 +106,60 @@ static IdString derive_name_from_cell_output_wire(const RTLIL::Cell *cell, strin return name + suffix; } +static bool rename_witness(RTLIL::Design *design, dict &cache, RTLIL::Module *module) +{ + auto cached = cache.find(module); + if (cached != cache.end()) { + if (cached->second == -1) + log_error("Cannot rename witness signals in a design containing recursive instantiations.\n"); + return cached->second; + } + cache.emplace(module, -1); + + bool has_witness_signals = false; + for (auto cell : module->cells()) + { + RTLIL::Module *impl = design->module(cell->type); + if (impl != nullptr) { + bool witness_in_cell = rename_witness(design, cache, impl); + has_witness_signals |= witness_in_cell; + if (witness_in_cell && !cell->name.isPublic()) { + std::string name = cell->name.c_str() + 1; + for (auto &c : name) + if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_') + c = '_'; + auto new_id = module->uniquify("\\_witness_." + name); + cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); + module->rename(cell, new_id); + } + } + + if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) { + has_witness_signals = true; + auto QY = cell->type == ID($anyinit) ? ID::Q : ID::Y; + auto sig_out = cell->getPort(QY); + + for (auto chunk : sig_out.chunks()) { + if (chunk.is_wire() && !chunk.wire->name.isPublic()) { + std::string name = stringf("%s_%s", cell->type.c_str() + 1, cell->name.c_str() + 1); + for (auto &c : name) + if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_') + c = '_'; + auto new_id = module->uniquify("\\_witness_." + name); + auto new_wire = module->addWire(new_id, GetSize(sig_out)); + new_wire->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); + module->connect({sig_out, new_wire}); + cell->setPort(QY, new_wire); + break; + } + } + } + } + + cache[module] = has_witness_signals; + return has_witness_signals; +} + struct RenamePass : public Pass { RenamePass() : Pass("rename", "rename object in the design") { } void help() override @@ -147,6 +201,14 @@ struct RenamePass : public Pass { log("pattern is '_%%_'.\n"); log("\n"); log("\n"); + log(" rename -witness\n"); + log("\n"); + log("Assigns auto-generated names to all $any*/$all* output wires and containing\n"); + log("cells that do not have a public name. This ensures that, during formal\n"); + log("verification, a solver-found trace can be fully specified using a public\n"); + log("hierarchical names.\n"); + log("\n"); + log("\n"); log(" rename -hide [selection]\n"); log("\n"); log("Assign private names (the ones with $-prefix) to all selected wires and cells\n"); @@ -172,6 +234,7 @@ struct RenamePass : public Pass { bool flag_src = false; bool flag_wire = false; bool flag_enumerate = false; + bool flag_witness = false; bool flag_hide = false; bool flag_top = false; bool flag_output = false; @@ -203,6 +266,11 @@ struct RenamePass : public Pass { got_mode = true; continue; } + if (arg == "-witness" && !got_mode) { + flag_witness = true; + got_mode = true; + continue; + } if (arg == "-hide" && !got_mode) { flag_hide = true; got_mode = true; @@ -309,6 +377,19 @@ struct RenamePass : public Pass { } } else + if (flag_witness) + { + extra_args(args, argidx, design, false); + + RTLIL::Module *module = design->top_module(); + + if (module == nullptr) + log_cmd_error("No top module found!\n"); + + dict cache; + rename_witness(design, cache, module); + } + else if (flag_hide) { extra_args(args, argidx, design); -- cgit v1.2.3 From 4ad13c647e2789268aed06d528bc2a40c6196133 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 5 Aug 2022 15:34:14 +0200 Subject: clk2fflogic: Generate less unused logic when using verific Verific generates a lot of FFs with an unused async load and we cannot always optimize that away before running clk2fflogic, so check for that special case here. --- passes/sat/clk2fflogic.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'passes') diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index b1b0567a0..2384ffced 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -233,7 +233,10 @@ struct Clk2fflogicPass : public Pass { qval = past_q; } - if (ff.has_aload) { + // The check for a constant sig_aload is also done by opt_dff, but when using verific and running + // clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids + // generating a lot of extra logic. + if (ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1)) { SigSpec sig_aload = wrap_async_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine, NEW_ID); if (!ff.is_fine) -- cgit v1.2.3 From f7023d06a2bda56467c8f07cc44d3b92f0eab2ba Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 9 Aug 2022 15:43:26 +0200 Subject: sim: -hdlname option to preserve flattened hierarchy in sim output --- passes/sat/sim.cc | 50 +++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 41 insertions(+), 9 deletions(-) (limited to 'passes') diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index ea64dce06..18a25a097 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -81,6 +81,7 @@ struct SimShared bool hide_internal = true; bool writeback = false; bool zinit = false; + bool hdlname = false; int rstlen = 1; FstData *fst = nullptr; double start_time = 0; @@ -738,9 +739,17 @@ struct SimInstance child.second->register_signals(id); } - void write_output_header(std::function enter_scope, std::function exit_scope, std::function register_signal) + void write_output_header(std::function enter_scope, std::function exit_scope, std::function register_signal) { - enter_scope(name()); + int exit_scopes = 1; + if (shared->hdlname && instance != nullptr && instance->name.isPublic() && instance->has_attribute(ID::hdlname)) { + auto hdlname = instance->get_hdlname_attribute(); + log_assert(!hdlname.empty()); + for (auto name : hdlname) + enter_scope("\\" + name); + exit_scopes = hdlname.size(); + } else + enter_scope(name()); dict registers; for (auto cell : module->cells()) @@ -756,13 +765,25 @@ struct SimInstance for (auto signal : signal_database) { - register_signal(signal.first, signal.second.first, registers.count(signal.first)!=0); + if (shared->hdlname && signal.first->name.isPublic() && signal.first->has_attribute(ID::hdlname)) { + auto hdlname = signal.first->get_hdlname_attribute(); + log_assert(!hdlname.empty()); + auto signal_name = std::move(hdlname.back()); + hdlname.pop_back(); + for (auto name : hdlname) + enter_scope("\\" + name); + register_signal(signal_name.c_str(), signal.first, signal.second.first, registers.count(signal.first)!=0); + for (auto name : hdlname) + exit_scope(); + } else + register_signal(log_id(signal.first->name), signal.first, signal.second.first, registers.count(signal.first)!=0); } for (auto child : children) child.second->write_output_header(enter_scope, exit_scope, register_signal); - exit_scope(); + for (int i = 0; i < exit_scopes; i++) + exit_scope(); } void register_output_step_values(std::map *data) @@ -1712,7 +1733,11 @@ struct VCDWriter : public OutputWriter worker->top->write_output_header( [this](IdString name) { vcdfile << stringf("$scope module %s $end\n", log_id(name)); }, [this]() { vcdfile << stringf("$upscope $end\n");}, - [this,use_signal](Wire *wire, int id, bool is_reg) { if (use_signal.at(id)) vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, wire->name[0] == '$' ? "\\" : "", log_id(wire)); } + [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) { + if (use_signal.at(id)) { + vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, name[0] == '$' ? "\\" : "", name); + } + } ); vcdfile << stringf("$enddefinitions $end\n"); @@ -1770,11 +1795,10 @@ struct FSTWriter : public OutputWriter worker->top->write_output_header( [this](IdString name) { fstWriterSetScope(fstfile, FST_ST_VCD_MODULE, stringf("%s",log_id(name)).c_str(), nullptr); }, [this]() { fstWriterSetUpscope(fstfile); }, - [this,use_signal](Wire *wire, int id, bool is_reg) { + [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) { if (!use_signal.at(id)) return; fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire), - stringf("%s%s", wire->name[0] == '$' ? "\\" : "", log_id(wire)).c_str(), 0); - + name, 0); mapping.emplace(id, fst_id); } ); @@ -1856,7 +1880,7 @@ struct AIWWriter : public OutputWriter worker->top->write_output_header( [](IdString) {}, []() {}, - [this](Wire *wire, int id, bool) { mapping[wire] = id; } + [this](const char */*name*/, Wire *wire, int id, bool) { mapping[wire] = id; } ); std::map current; @@ -1945,6 +1969,10 @@ struct SimPass : public Pass { log(" write the simulation results to an AIGER witness file\n"); log(" (requires a *.aim file via -map)\n"); log("\n"); + log(" -hdlname\n"); + log(" use the hdlname attribute when writing simulation results\n"); + log(" (preserves hierarchy in a flattened design)\n"); + log("\n"); log(" -x\n"); log(" ignore constant x outputs in simulation file.\n"); log("\n"); @@ -2057,6 +2085,10 @@ struct SimPass : public Pass { worker.outputfiles.emplace_back(std::unique_ptr(new AIWWriter(&worker, aiw_filename.c_str()))); continue; } + if (args[argidx] == "-hdlname") { + worker.hdlname = true; + continue; + } if (args[argidx] == "-n" && argidx+1 < args.size()) { numcycles = atoi(args[++argidx].c_str()); worker.cycles_set = true; -- cgit v1.2.3