From 2d9484c12cd1fd96eca5253c876ad545ed209f40 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 19 Sep 2019 15:40:28 -0700 Subject: When two boxes connect to each other, need not be a (* keep *) --- backends/aiger/xaiger.cc | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index fa6ba0aca..cbce4c83b 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -405,12 +405,7 @@ struct XAigerWriter if (O != b) alias_map[O] = b; undriven_bits.erase(O); - - auto jt = input_bits.find(b); - if (jt != input_bits.end()) { - log_assert(keep_bits.count(O)); - input_bits.erase(b); - } + input_bits.erase(b); } } } -- cgit v1.2.3 From 4f426c2ac48bbb5ae9e92ca046aa20af35d75a52 Mon Sep 17 00:00:00 2001 From: whitequark Date: Sun, 22 Sep 2019 16:52:06 +0000 Subject: write_verilog: do not print (*init*) attributes on regs. If an init value is emitted for a reg, an (*init*) attribute is never necessary, since it is exactly equivalent. On the other hand, some tools that consume Verilog (ISE, Vivado, Quartus) complain about (*init*) attributes because their interpretation differs from Yosys. All (*init*) attributes that would not become reg init values anyway are emitted as before. --- backends/verilog/verilog_backend.cc | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'backends') diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 7b1db4776..24e397bda 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -371,13 +371,14 @@ void dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig) } } -void dump_attributes(std::ostream &f, std::string indent, dict &attributes, char term = '\n', bool modattr = false, bool as_comment = false) +void dump_attributes(std::ostream &f, std::string indent, dict &attributes, char term = '\n', bool modattr = false, bool regattr = false, bool as_comment = false) { if (noattr) return; if (attr2comment) as_comment = true; for (auto it = attributes.begin(); it != attributes.end(); ++it) { + if (it->first == "\\init" && regattr) continue; f << stringf("%s" "%s %s", indent.c_str(), as_comment ? "/*" : "(*", id(it->first).c_str()); f << stringf(" = "); if (modattr && (it->second == State::S0 || it->second == Const(0))) @@ -392,7 +393,7 @@ void dump_attributes(std::ostream &f, std::string indent, dictattributes); + dump_attributes(f, indent, wire->attributes, '\n', /*modattr=*/false, /*regattr=*/reg_wires.count(wire->name)); #if 0 if (wire->port_input && !wire->port_output) f << stringf("%s" "input %s", indent.c_str(), reg_wires.count(wire->name) ? "reg " : ""); @@ -1521,7 +1522,7 @@ void dump_proc_switch(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw bool got_default = false; for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it) { - dump_attributes(f, indent + " ", (*it)->attributes, '\n', /*modattr=*/false, /*as_comment=*/true); + dump_attributes(f, indent + " ", (*it)->attributes, '\n', /*modattr=*/false, /*regattr=*/false, /*as_comment=*/true); if ((*it)->compare.size() == 0) { if (got_default) continue; @@ -1686,7 +1687,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module) } } - dump_attributes(f, indent, module->attributes, '\n', /*attr2comment=*/true); + dump_attributes(f, indent, module->attributes, '\n', /*modattr=*/true); f << stringf("%s" "module %s(", indent.c_str(), id(module->name, false).c_str()); bool keep_running = true; for (int port_id = 1; keep_running; port_id++) { -- cgit v1.2.3 From c340fbfab23c582103402bbd812d9bca4510dc41 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Mon, 23 Sep 2019 21:58:04 -0700 Subject: Force $inout.out ports to begin with '$' to indicate internal --- backends/aiger/xaiger.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index cbce4c83b..21b281708 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -424,7 +424,7 @@ struct XAigerWriter // inherit existing inout's drivers if ((wire->port_input && wire->port_output && !undriven_bits.count(bit)) || keep_bits.count(bit)) { - RTLIL::IdString wire_name = wire->name.str() + "$inout.out"; + RTLIL::IdString wire_name = stringf("$%s$inout.out", wire->name.c_str()); RTLIL::Wire *new_wire = module->wire(wire_name); if (!new_wire) new_wire = module->addWire(wire_name, GetSize(wire)); -- cgit v1.2.3 From 44374b1b2b0dbc455c9e43d713e133d7d78a5e1a Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Mon, 23 Sep 2019 21:58:40 -0700 Subject: "abc_padding" attr for blackbox outputs that were padded, remove them later --- backends/aiger/xaiger.cc | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 21b281708..5e49f3c80 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -350,6 +350,8 @@ struct XAigerWriter if (!box_module || !box_module->attributes.count("\\abc_box_id")) continue; + bool blackbox = box_module->get_blackbox_attribute(true /* ignore_wb */); + // Fully pad all unused input connections of this box cell with S0 // Fully pad all undriven output connections of this box cell with anonymous wires // NB: Assume box_module->ports are sorted alphabetically @@ -394,7 +396,10 @@ struct XAigerWriter rhs = it->second; } else { - rhs = module->addWire(NEW_ID, GetSize(w)); + Wire *wire = module->addWire(NEW_ID, GetSize(w)); + if (blackbox) + wire->set_bool_attribute(ID(abc_padding)); + rhs = wire; cell->setPort(port_name, rhs); } -- cgit v1.2.3 From 5eebfabe4286d47a75508677e2bc76e8b422a879 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Fri, 27 Sep 2019 12:40:17 -0400 Subject: Corrects btor2 backend --- backends/btor/btor.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 4472993d4..f617b7ec2 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -897,9 +897,12 @@ struct BtorWorker int sid = get_bv_sid(GetSize(s)); int nid = next_nid++; - btorf("%d input %d %s\n", nid, sid); + btorf("%d input %d\n", nid, sid); nid_width[nid] = GetSize(s); + for (int j = 0; j < GetSize(s); j++) + nidbits.push_back(make_pair(nid, j)); + i += GetSize(s)-1; continue; } -- cgit v1.2.3 From d0493925ec739aa13cd72e5aa525e98ca49cc326 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Sat, 28 Sep 2019 09:28:51 +0200 Subject: Support binary files for backends, fixes #1407 --- backends/aiger/xaiger.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index fa6ba0aca..87ba0aedf 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -856,7 +856,7 @@ struct XAigerBackend : public Backend { } break; } - extra_args(f, filename, args, argidx); + extra_args(f, filename, args, argidx, !ascii_mode); Module *top_module = design->top_module(); -- cgit v1.2.3 From 0c380f085576c2cead5e3576825cb60046bfd76b Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Sat, 28 Sep 2019 09:50:29 +0200 Subject: Add aiger and protobuf backends binary support --- backends/aiger/aiger.cc | 2 +- backends/protobuf/protobuf.cc | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'backends') diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 0798fb35d..3e8b14dee 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -777,7 +777,7 @@ struct AigerBackend : public Backend { } break; } - extra_args(f, filename, args, argidx); + extra_args(f, filename, args, argidx, !ascii_mode); Module *top_module = design->top_module(); diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc index fff110bb0..671686173 100644 --- a/backends/protobuf/protobuf.cc +++ b/backends/protobuf/protobuf.cc @@ -266,7 +266,7 @@ struct ProtobufBackend : public Backend { } break; } - extra_args(f, filename, args, argidx); + extra_args(f, filename, args, argidx, !text_mode); log_header(design, "Executing Protobuf backend.\n"); @@ -338,7 +338,7 @@ struct ProtobufPass : public Pass { if (!filename.empty()) { rewrite_filename(filename); std::ofstream *ff = new std::ofstream; - ff->open(filename.c_str(), std::ofstream::trunc); + ff->open(filename.c_str(), text_mode ? std::ofstream::trunc : (std::ofstream::trunc | std::ofstream::binary)); if (ff->fail()) { delete ff; log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno)); -- cgit v1.2.3 From a84a2d74c779b8023c0bbfc02fa4576d8c4cecca Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 2 Oct 2019 12:48:04 +0200 Subject: Fix btor back-end to use "state" instead of "input" for undef init bits Signed-off-by: Clifford Wolf --- backends/btor/btor.cc | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'backends') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index f617b7ec2..9e316a055 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -569,7 +569,7 @@ struct BtorWorker int nid_init_val = -1; if (!initval.is_fully_undef()) - nid_init_val = get_sig_nid(initval); + nid_init_val = get_sig_nid(initval, -1, false, true); int sid = get_bv_sid(GetSize(sig_q)); int nid = next_nid++; @@ -681,7 +681,7 @@ struct BtorWorker { if (verbose) btorf("; initval = %s\n", log_signal(firstword)); - nid_init_val = get_sig_nid(firstword); + nid_init_val = get_sig_nid(firstword, -1, false, true); } else { @@ -693,8 +693,8 @@ struct BtorWorker if (thisword.is_fully_undef()) continue; Const thisaddr(i, abits); - int nid_thisword = get_sig_nid(thisword); - int nid_thisaddr = get_sig_nid(thisaddr); + int nid_thisword = get_sig_nid(thisword, -1, false, true); + int nid_thisaddr = get_sig_nid(thisaddr, -1, false, true); int last_nid_init_val = nid_init_val; nid_init_val = next_nid++; if (verbose) @@ -792,7 +792,7 @@ struct BtorWorker cell_recursion_guard.erase(cell); } - int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false) + int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false, bool is_init = false) { int nid = -1; sigmap.apply(sig); @@ -823,7 +823,10 @@ struct BtorWorker int sid = get_bv_sid(GetSize(sig)); int nid_input = next_nid++; - btorf("%d input %d\n", nid_input, sid); + if (is_init) + btorf("%d state %d\n", nid_input, sid); + else + btorf("%d input %d\n", nid_input, sid); int nid_masked_input; if (sig_mask_undef.is_fully_ones()) { -- cgit v1.2.3 From 2ed2e9c3e8f2d9d6882588857c8556a6e2af57ea Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 3 Oct 2019 14:59:07 +0200 Subject: Change smtbmc "Warmup failed" status to "PREUNSAT" Signed-off-by: Clifford Wolf --- backends/smt2/smtbmc.py | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 445a42e0d..3d6d3e1b3 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1256,7 +1256,7 @@ def smt_check_sat(): return smt.check_sat() if tempind: - retstatus = False + retstatus = "FAILED" skip_counter = step_size for step in range(num_steps, -1, -1): if smt.forall: @@ -1303,7 +1303,7 @@ if tempind: else: print_msg("Temporal induction successful.") - retstatus = True + retstatus = "PASSED" break elif covermode: @@ -1321,7 +1321,7 @@ elif covermode: smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr)) step = 0 - retstatus = False + retstatus = "FAILED" found_failed_assert = False assert step_size == 1 @@ -1365,7 +1365,7 @@ elif covermode: if smt_check_sat() == "unsat": print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) found_failed_assert = True - retstatus = False + retstatus = "FAILED" break reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step))) @@ -1400,7 +1400,7 @@ elif covermode: break if "1" not in cover_mask: - retstatus = True + retstatus = "PASSED" break step += 1 @@ -1412,7 +1412,7 @@ elif covermode: else: # not tempind, covermode step = 0 - retstatus = True + retstatus = "PASSED" while step < num_steps: smt_state(step) smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) @@ -1459,8 +1459,8 @@ else: # not tempind, covermode print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step)) if smt_check_sat() == "unsat": - print("%s Warmup failed!" % smt.timestamp()) - retstatus = False + print("%s Assumptions are unsatisfiable!" % smt.timestamp()) + retstatus = "PREUNSAT" break if not final_only: @@ -1487,13 +1487,13 @@ else: # not tempind, covermode print_msg("Re-solving with appended steps..") if smt_check_sat() == "unsat": print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) - retstatus = False + retstatus = "FAILED" break print_anyconsts(step) for i in range(step, last_check_step+1): print_failed_asserts(i) write_trace(0, last_check_step+1+append_steps, '%') - retstatus = False + retstatus = "FAILED" break smt_pop() @@ -1519,7 +1519,7 @@ else: # not tempind, covermode print_anyconsts(i) print_failed_asserts(i, final=True) write_trace(0, i+1, '%') - retstatus = False + retstatus = "FAILED" break smt_pop() @@ -1534,7 +1534,7 @@ else: # not tempind, covermode print_msg("Solving for step %d.." % (last_check_step)) if smt_check_sat() != "sat": print("%s No solution found!" % smt.timestamp()) - retstatus = False + retstatus = "FAILED" break elif dumpall: @@ -1551,5 +1551,5 @@ else: # not tempind, covermode smt.write("(exit)") smt.wait() -print_msg("Status: %s" % ("PASSED" if retstatus else "FAILED (!)")) -sys.exit(0 if retstatus else 1) +print_msg("Status: %s" % retstatus) +sys.exit(0 if retstatus == "PASSED" else 1) -- cgit v1.2.3 From aae2b9fd9c8dc915fadacc24962436dd7aedff36 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 4 Oct 2019 11:04:10 -0700 Subject: Rename abc_* names/attributes to more precisely be abc9_* --- backends/aiger/xaiger.cc | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 4018cc9de..46890b071 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -203,7 +203,7 @@ struct XAigerWriter // box ordering, but not individual AIG cells dict> bit_drivers, bit_users; TopoSort toposort; - bool abc_box_seen = false; + bool abc9_box_seen = false; for (auto cell : module->selected_cells()) { if (cell->type == "$_NOT_") @@ -242,8 +242,8 @@ struct XAigerWriter log_assert(!holes_mode); RTLIL::Module* inst_module = module->design->module(cell->type); - if (inst_module && inst_module->attributes.count("\\abc_box_id")) { - abc_box_seen = true; + if (inst_module && inst_module->attributes.count("\\abc9_box_id")) { + abc9_box_seen = true; if (!holes_mode) { toposort.node(cell->name); @@ -291,10 +291,10 @@ struct XAigerWriter if (is_output) { int arrival = 0; if (port_wire) { - auto it = port_wire->attributes.find("\\abc_arrival"); + auto it = port_wire->attributes.find("\\abc9_arrival"); if (it != port_wire->attributes.end()) { if (it->second.flags != 0) - log_error("Attribute 'abc_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type)); + log_error("Attribute 'abc9_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type)); arrival = it->second.as_int(); } } @@ -318,7 +318,7 @@ struct XAigerWriter //log_warning("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell)); } - if (abc_box_seen) { + if (abc9_box_seen) { for (auto &it : bit_users) if (bit_drivers.count(it.first)) for (auto driver_cell : bit_drivers.at(it.first)) @@ -347,7 +347,7 @@ struct XAigerWriter log_assert(cell); RTLIL::Module* box_module = module->design->module(cell->type); - if (!box_module || !box_module->attributes.count("\\abc_box_id")) + if (!box_module || !box_module->attributes.count("\\abc9_box_id")) continue; bool blackbox = box_module->get_blackbox_attribute(true /* ignore_wb */); @@ -398,7 +398,7 @@ struct XAigerWriter else { Wire *wire = module->addWire(NEW_ID, GetSize(w)); if (blackbox) - wire->set_bool_attribute(ID(abc_padding)); + wire->set_bool_attribute(ID(abc9_padding)); rhs = wire; cell->setPort(port_name, rhs); } @@ -666,7 +666,7 @@ struct XAigerWriter write_h_buffer(box_inputs); write_h_buffer(box_outputs); - write_h_buffer(box_module->attributes.at("\\abc_box_id").as_int()); + write_h_buffer(box_module->attributes.at("\\abc9_box_id").as_int()); write_h_buffer(box_count++); } -- cgit v1.2.3 From f02623abb5d8338f034d7069844418af8912ab0f Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 23 Oct 2019 00:04:34 +0200 Subject: Bugfix in smtio vcd handling of $-identifiers Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index bac68ac70..1df996aa7 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -1032,12 +1032,17 @@ class MkVcd: print("$var integer 32 t smt_step $end", file=self.f) print("$var event 1 ! smt_clock $end", file=self.f) + def vcdescape(n): + if n.startswith("$") or ":" in n: + return "\\" + n + return n + scope = [] for path in sorted(self.nets): key, width = self.nets[path] uipath = list(path) - if "." in uipath[-1]: + if "." in uipath[-1] and not uipath[-1].startswith("$"): uipath = uipath[0:-1] + uipath[-1].split(".") for i in range(len(uipath)): uipath[i] = re.sub(r"\[([^\]]*)\]", r"<\1>", uipath[i]) @@ -1048,15 +1053,13 @@ class MkVcd: while uipath[:-1] != scope: scopename = uipath[len(scope)] - if scopename.startswith("$"): - scopename = "\\" + scopename - print("$scope module %s $end" % scopename, file=self.f) + print("$scope module %s $end" % vcdescape(scopename), file=self.f) scope.append(uipath[len(scope)]) if path in self.clocks and self.clocks[path][1] == "event": - print("$var event 1 %s %s $end" % (key, uipath[-1]), file=self.f) + print("$var event 1 %s %s $end" % (key, vcdescape(uipath[-1])), file=self.f) else: - print("$var wire %d %s %s $end" % (width, key, uipath[-1]), file=self.f) + print("$var wire %d %s %s $end" % (width, key, vcdescape(uipath[-1])), file=self.f) for i in range(len(scope)): print("$upscope $end", file=self.f) -- cgit v1.2.3 From 5110a34dd74bc96c47d4aef47bc155110de2d87e Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 4 Nov 2019 14:25:13 +0100 Subject: Fix write_aiger bug added in 524af21 Signed-off-by: Clifford Wolf --- backends/aiger/aiger.cc | 3 +++ 1 file changed, 3 insertions(+) (limited to 'backends') diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 3e8b14dee..44718baae 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -91,6 +91,9 @@ struct AigerWriter } else if (alias_map.count(bit)) { a = bit2aig(alias_map.at(bit)); + } else + if (initstate_bits.count(bit)) { + a = initstate_ff; } if (bit == State::Sx || bit == State::Sz) -- cgit v1.2.3 From d88cc139a029764cf62d95b2eaaff99e270a134a Mon Sep 17 00:00:00 2001 From: Makai Mann Date: Mon, 11 Nov 2019 16:40:51 -0800 Subject: Add an info string symbol for bad states in btor backend --- backends/btor/btor.cc | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 9e316a055..2babd454c 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1070,7 +1070,16 @@ struct BtorWorker bad_properties.push_back(nid_en_and_not_a); } else { int nid = next_nid++; - btorf("%d bad %d\n", nid, nid_en_and_not_a); + + string infostr = + cell->attributes.count("\\src") + ? cell->attributes.at("\\src") + .decode_string() + .c_str() + : log_id(cell); + + std::replace(infostr.begin(), infostr.end(), ' ', '_'); + btorf("%d bad %d %s\n", nid, nid_en_and_not_a, infostr.c_str()); } btorf_pop(log_id(cell)); -- cgit v1.2.3 From cd44826d5026316d9b44ae33c1fcf0d8faf550c4 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 14 Nov 2019 11:57:38 +0100 Subject: Use cell name for btor bad state props when it is a public name Signed-off-by: Clifford Wolf --- backends/btor/btor.cc | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) (limited to 'backends') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 2babd454c..c1da4b127 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1070,15 +1070,11 @@ struct BtorWorker bad_properties.push_back(nid_en_and_not_a); } else { int nid = next_nid++; - - string infostr = - cell->attributes.count("\\src") - ? cell->attributes.at("\\src") - .decode_string() - .c_str() - : log_id(cell); - - std::replace(infostr.begin(), infostr.end(), ' ', '_'); + string infostr = log_id(cell); + if (infostr[0] == '$' && cell->attributes.count("\\src")) { + infostr = cell->attributes.at("\\src").decode_string().c_str(); + std::replace(infostr.begin(), infostr.end(), ' ', '_'); + } btorf("%d bad %d %s\n", nid, nid_en_and_not_a, infostr.c_str()); } -- cgit v1.2.3 From 3c643c57dfee9956697e8629a746bc04439be5a2 Mon Sep 17 00:00:00 2001 From: whitequark Date: Fri, 15 Nov 2019 03:11:46 +0000 Subject: write_verilog: add -extmem option, to write split memory init files. Some toolchains (in particular Quartus) are pathologically slow if a large amount of assignments in `initial` blocks are used. --- backends/verilog/verilog_backend.cc | 90 ++++++++++++++++++++++++++++++++----- 1 file changed, 80 insertions(+), 10 deletions(-) (limited to 'backends') diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 24e397bda..54d0f6148 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -33,11 +33,11 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, defparam, decimal, siminit; -int auto_name_counter, auto_name_offset, auto_name_digits; +bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit; +int auto_name_counter, auto_name_offset, auto_name_digits, extmem_counter; std::map auto_name_map; std::set reg_wires, reg_ct; -std::string auto_prefix; +std::string auto_prefix, extmem_prefix; RTLIL::Module *active_module; dict active_initdata; @@ -1069,14 +1069,64 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) f << stringf("%s" "reg [%d:%d] %s [%d:%d];\n", indent.c_str(), width-1, 0, mem_id.c_str(), size+offset-1, offset); if (use_init) { - f << stringf("%s" "initial begin\n", indent.c_str()); - for (int i=0; iparameters["\\INIT"].extract(i*width, width); + for (int j=0; j expressions within that clock domain @@ -1777,8 +1827,16 @@ struct VerilogBackend : public Backend { log(" deactivates this feature and instead will write string constants\n"); log(" as binary numbers.\n"); log("\n"); + log(" -extmem\n"); + log(" instead of initializing memories using assignments to individual\n"); + log(" elements, use the '$readmemh' function to read initialization data\n"); + log(" from a file. This data is written to a file named by appending\n"); + log(" a sequential index to the Verilog filename and replacing the extension\n"); + log(" with '.mem', e.g. 'write_verilog -extmem foo.v' writes 'foo-1.mem',\n"); + log(" 'foo-2.mem' and so on.\n"); + log("\n"); log(" -defparam\n"); - log(" Use 'defparam' statements instead of the Verilog-2001 syntax for\n"); + log(" use 'defparam' statements instead of the Verilog-2001 syntax for\n"); log(" cell parameters.\n"); log("\n"); log(" -blackboxes\n"); @@ -1812,6 +1870,7 @@ struct VerilogBackend : public Backend { nodec = false; nohex = false; nostr = false; + extmem = false; defparam = false; decimal = false; siminit = false; @@ -1885,6 +1944,11 @@ struct VerilogBackend : public Backend { nostr = true; continue; } + if (arg == "-extmem") { + extmem = true; + extmem_counter = 1; + continue; + } if (arg == "-defparam") { defparam = true; continue; @@ -1912,6 +1976,12 @@ struct VerilogBackend : public Backend { break; } extra_args(f, filename, args, argidx); + if (extmem) + { + if (filename.empty()) + log_cmd_error("Option -extmem must be used with a filename.\n"); + extmem_prefix = filename.substr(0, filename.rfind('.')); + } design->sort(); -- cgit v1.2.3