From 171c425cf9addb61ef3f03596fd26355ed8af76d Mon Sep 17 00:00:00 2001 From: Jim Lawson Date: Mon, 25 Feb 2019 16:18:13 -0800 Subject: Fix FIRRTL to Verilog process instance subfield assignment. Don't emit subfield assignments: bits(x, y, z) <= ... - but instead, add them to the reverse-wire-map where they'll be treated at the end of the module. Enable tests which were disabled due to incorrect treatment of subfields. Assume the `$firrtl2verilog` variable contains any additional switches to control verilog generation (i.e. `--no-dedup -X mverilog`) --- backends/firrtl/firrtl.cc | 28 ++++++++++++++++++++-------- 1 file changed, 20 insertions(+), 8 deletions(-) (limited to 'backends') diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc index 0917ecba6..88c1038b7 100644 --- a/backends/firrtl/firrtl.cc +++ b/backends/firrtl/firrtl.cc @@ -169,7 +169,6 @@ struct FirrtlWorker return *str == '\\' ? str + 1 : str; } - std::string cellname(RTLIL::Cell *cell) { return fid(cell->name).c_str(); @@ -219,29 +218,42 @@ struct FirrtlWorker if (it->second.size() > 0) { const SigSpec &secondSig = it->second; const std::string firstName = cell_name + "." + make_id(it->first); - const std::string secondName = make_expr(secondSig); + const std::string secondExpr = make_expr(secondSig); // Find the direction for this port. FDirection dir = getPortFDirection(it->first, instModule); - std::string source, sink; + std::string sourceExpr, sinkExpr; + const SigSpec *sinkSig = nullptr; switch (dir) { case FD_INOUT: log_warning("Instance port connection %s.%s is INOUT; treating as OUT\n", cell_type.c_str(), log_signal(it->second)); case FD_OUT: - source = firstName; - sink = secondName; + sourceExpr = firstName; + sinkExpr = secondExpr; + sinkSig = &secondSig; break; case FD_NODIRECTION: log_warning("Instance port connection %s.%s is NODIRECTION; treating as IN\n", cell_type.c_str(), log_signal(it->second)); /* FALL_THROUGH */ case FD_IN: - source = secondName; - sink = firstName; + sourceExpr = secondExpr; + sinkExpr = firstName; break; default: log_error("Instance port %s.%s unrecognized connection direction 0x%x !\n", cell_type.c_str(), log_signal(it->second), dir); break; } - wire_exprs.push_back(stringf("\n%s%s <= %s", indent.c_str(), sink.c_str(), source.c_str())); + // Check for subfield assignment. + std::string bitsString = "bits("; + if (sinkExpr.substr(0, bitsString.length()) == bitsString ) { + if (sinkSig == nullptr) + log_error("Unknown subfield %s.%s\n", cell_type.c_str(), sinkExpr.c_str()); + // Don't generate the assignment here. + // Add the source and sink to the "reverse_wire_map" and we'll output the assignment + // as part of the coalesced subfield assignments for this wire. + register_reverse_wire_map(sourceExpr, *sinkSig); + } else { + wire_exprs.push_back(stringf("\n%s%s <= %s", indent.c_str(), sinkExpr.c_str(), sourceExpr.c_str())); + } } } wire_exprs.push_back(stringf("\n")); -- cgit v1.2.3 From f570aa5e1d3ac201089da2198f8e5084185fd92f Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 28 Feb 2019 12:15:58 -0800 Subject: Fix smt2 code generation for partially initialized memowy words, fixes #831 Signed-off-by: Clifford Wolf --- backends/smt2/smt2.cc | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 418f8d766..7f3cc94ca 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -1103,20 +1103,27 @@ struct Smt2Worker break; Const initword = init_data.extract(i*width, width, State::Sx); + Const initmask = initword; bool gen_init_constr = false; - for (auto bit : initword.bits) - if (bit == State::S0 || bit == State::S1) + for (int k = 0; k < GetSize(initword); k++) { + if (initword[k] == State::S0 || initword[k] == State::S1) { gen_init_constr = true; + initmask[k] = State::S1; + } else { + initmask[k] = State::S0; + initword[k] = State::S0; + } + } if (gen_init_constr) { if (statebv) /* FIXME */; else - init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]", + init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]", get_id(module), arrayid, Const(i, abits).as_string().c_str(), - initword.as_string().c_str(), get_id(cell), i)); + initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i)); } } } -- cgit v1.2.3 From e2fc18f27b5e9f506724a486787c2106b9f7fb4f Mon Sep 17 00:00:00 2001 From: Larry Doolittle Date: Tue, 26 Feb 2019 10:28:42 -0800 Subject: Reduce amount of trailing whitespace in code base --- backends/protobuf/protobuf.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backends') diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc index f56147cef..549fc73ae 100644 --- a/backends/protobuf/protobuf.cc +++ b/backends/protobuf/protobuf.cc @@ -48,7 +48,7 @@ struct ProtobufDesignSerializer ProtobufDesignSerializer(bool use_selection, bool aig_mode) : aig_mode_(aig_mode), use_selection_(use_selection) { } - + string get_name(IdString name) { return RTLIL::unescape_id(name); @@ -60,7 +60,7 @@ struct ProtobufDesignSerializer { for (auto ¶m : parameters) { std::string key = get_name(param.first); - + yosys::pb::Parameter pb_param; @@ -207,7 +207,7 @@ struct ProtobufDesignSerializer (*models)[aig.name] = pb_model; } } - + void serialize_design(yosys::pb::Design *pb, Design *design) { GOOGLE_PROTOBUF_VERIFY_VERSION; -- cgit v1.2.3 From 241901461ae02c6a41837e254088f277b8167476 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 28 Feb 2019 14:56:55 -0800 Subject: Add "write_verilog -siminit" Signed-off-by: Clifford Wolf --- backends/verilog/verilog_backend.cc | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'backends') diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index d351a6266..6818edb7a 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -33,7 +33,7 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, defparam, decimal; +bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, defparam, decimal, siminit; int auto_name_counter, auto_name_offset, auto_name_digits; std::map auto_name_map; std::set reg_wires, reg_ct; @@ -1310,7 +1310,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell) } } - if (reg_ct.count(cell->type) && cell->hasPort("\\Q")) { + if (siminit && reg_ct.count(cell->type) && cell->hasPort("\\Q")) { std::stringstream ss; dump_reg_init(ss, cell->getPort("\\Q")); if (!ss.str().empty()) { @@ -1607,6 +1607,10 @@ struct VerilogBackend : public Backend { log(" without this option all internal cells are converted to Verilog\n"); log(" expressions.\n"); log("\n"); + log(" -siminit\n"); + log(" add initial statements with hierarchical refs to initialize FFs when\n"); + log(" in -noexpr mode.\n"); + log("\n"); log(" -nodec\n"); log(" 32-bit constant values are by default dumped as decimal numbers,\n"); log(" not bit pattern. This option deactivates this feature and instead\n"); @@ -1663,6 +1667,7 @@ struct VerilogBackend : public Backend { nostr = false; defparam = false; decimal = false; + siminit = false; auto_prefix = ""; bool blackboxes = false; @@ -1739,6 +1744,10 @@ struct VerilogBackend : public Backend { decimal = true; continue; } + if (arg == "-siminit") { + siminit = true; + continue; + } if (arg == "-blackboxes") { blackboxes = true; continue; -- cgit v1.2.3 From 03237de68605bb6eae73b96379faab0af6f8ce73 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 1 Mar 2019 12:59:07 -0800 Subject: Fix "write_edif -gndvccy" Signed-off-by: Clifford Wolf --- backends/edif/edif.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc index 2d25f879d..7e30b67af 100644 --- a/backends/edif/edif.cc +++ b/backends/edif/edif.cc @@ -130,7 +130,7 @@ struct EdifBackend : public Backend { bool port_rename = false; bool attr_properties = false; std::map> lib_cell_ports; - bool nogndvcc = false, gndvccy = true; + bool nogndvcc = false, gndvccy = false; CellTypes ct(design); EdifNames edif_names; -- cgit v1.2.3 From d6c4dfb9020ee19eebe3adadca89b65627184d81 Mon Sep 17 00:00:00 2001 From: Jim Lawson Date: Mon, 4 Mar 2019 13:23:58 -0800 Subject: Ensure fid() calls make_id() for consistency; tests/simple/dff_init.v fails Mark dff_init.v as expected to fail since it uses "initial value". --- backends/firrtl/firrtl.cc | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'backends') diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc index 88c1038b7..eef6401b2 100644 --- a/backends/firrtl/firrtl.cc +++ b/backends/firrtl/firrtl.cc @@ -165,8 +165,7 @@ struct FirrtlWorker std::string fid(RTLIL::IdString internal_id) { - const char *str = internal_id.c_str(); - return *str == '\\' ? str + 1 : str; + return make_id(internal_id); } std::string cellname(RTLIL::Cell *cell) -- cgit v1.2.3 From 5dfc7becca1f1faf6e77fb3b5d07d97171613d90 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 7 Mar 2019 11:31:46 -0800 Subject: Use SVA label in smt export if available Signed-off-by: Clifford Wolf --- backends/smt2/smt2.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 7f3cc94ca..a26bff57b 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -887,8 +887,8 @@ struct Smt2Worker string name_a = get_bool(cell->getPort("\\A")); string name_en = get_bool(cell->getPort("\\EN")); - decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, - cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell))); + string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\src").decode_string() : get_id(cell); + decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str())); if (cell->type == "$cover") decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n", -- cgit v1.2.3 From 94f995ee3784e1a94a484fd399be2be4793d4e41 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 9 Mar 2019 13:19:41 -0800 Subject: Fix signed $shift/$shiftx handling in write_smt2 Signed-off-by: Clifford Wolf --- backends/smt2/smt2.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a26bff57b..688535f33 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -416,6 +416,7 @@ struct Smt2Worker for (char ch : expr) { if (ch == 'A') processed_expr += get_bv(sig_a); else if (ch == 'B') processed_expr += get_bv(sig_b); + else if (ch == 'P') processed_expr += get_bv(cell->getPort("\\B")); else if (ch == 'L') processed_expr += is_signed ? "a" : "l"; else if (ch == 'U') processed_expr += is_signed ? "s" : "u"; else processed_expr += ch; @@ -554,7 +555,7 @@ struct Smt2Worker if (cell->type.in("$shift", "$shiftx")) { if (cell->getParam("\\B_SIGNED").as_bool()) { - return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) " + return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) " "(bvlshr A B) (bvlshr A (bvneg B)))", GetSize(cell->getPort("\\B")), 0), 's'); } else { -- cgit v1.2.3 From 20c6a8c9b0abb384517c4cc6f58cd29a90bda6ff Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 11 Mar 2019 20:12:28 +0100 Subject: Improve determinism of IdString DB for similar scripts Signed-off-by: Clifford Wolf --- backends/verilog/verilog_backend.cc | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'backends') diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 6818edb7a..83d83f488 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -1673,6 +1673,8 @@ struct VerilogBackend : public Backend { bool blackboxes = false; bool selected = false; + auto_name_map.clear(); + reg_wires.clear(); reg_ct.clear(); reg_ct.insert("$dff"); @@ -1779,6 +1781,8 @@ struct VerilogBackend : public Backend { dump_module(*f, "", it->second); } + auto_name_map.clear(); + reg_wires.clear(); reg_ct.clear(); } } VerilogBackend; -- cgit v1.2.3 From ff15cf9b1f8208d8c6e22beb9aebedc8bdae213f Mon Sep 17 00:00:00 2001 From: "William D. Jones" Date: Tue, 12 Mar 2019 17:55:47 -0400 Subject: Install launcher executable when running yosys-smtbmc on Windows. Signed-off-by: William D. Jones --- backends/smt2/Makefile.inc | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc index dce82f01a..92941d4cf 100644 --- a/backends/smt2/Makefile.inc +++ b/backends/smt2/Makefile.inc @@ -3,14 +3,30 @@ OBJS += backends/smt2/smt2.o ifneq ($(CONFIG),mxe) ifneq ($(CONFIG),emcc) + +# MSYS targets support yosys-smtbmc, but require a launcher script +ifeq ($(CONFIG),$(filter $(CONFIG),msys2 msys2-64)) +TARGETS += yosys-smtbmc.exe yosys-smtbmc-script.py +# Needed to find the Python interpreter for yosys-smtbmc scripts. +# Override if necessary, it is only used for msys2 targets. +PYTHON := $(shell cygpath -w -m $(PREFIX)/bin/python3) + +yosys-smtbmc-script.py: backends/smt2/smtbmc.py + $(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' \ + -e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@ + +yosys-smtbmc.exe: misc/launcher.c yosys-smtbmc-script.py + $(P) gcc -DGUI=0 -O -s -o $@ $< +# Other targets +else TARGETS += yosys-smtbmc yosys-smtbmc: backends/smt2/smtbmc.py $(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new $(Q) chmod +x $@.new $(Q) mv $@.new $@ +endif $(eval $(call add_share_file,share/python3,backends/smt2/smtio.py)) endif endif - -- cgit v1.2.3 From 04e920337b1b984929d3d69fb2ab1f8b1e92f032 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 14 Mar 2019 17:50:20 +0100 Subject: Fix a syntax bug in ilang backend related to process case statements Signed-off-by: Clifford Wolf --- backends/ilang/ilang_backend.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc index 4c58ea087..dc39e5e08 100644 --- a/backends/ilang/ilang_backend.cc +++ b/backends/ilang/ilang_backend.cc @@ -204,7 +204,7 @@ void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const f << stringf("%s case ", indent.c_str()); for (size_t i = 0; i < (*it)->compare.size(); i++) { if (i > 0) - f << stringf(", "); + f << stringf(" , "); dump_sigspec(f, (*it)->compare[i]); } f << stringf("\n"); -- cgit v1.2.3 From bacca5753775bfabed955a9772a5d86d85007c58 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 13 Mar 2019 19:27:17 +0100 Subject: Fix smtbmc.py handling of zero appended steps Signed-off-by: Clifford Wolf --- backends/smt2/smtbmc.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 94a5e2da0..445a42e0d 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1484,11 +1484,11 @@ else: # not tempind, covermode smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i)) - print_msg("Re-solving with appended steps..") - if smt_check_sat() == "unsat": - print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) - retstatus = False - break + print_msg("Re-solving with appended steps..") + if smt_check_sat() == "unsat": + print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) + retstatus = False + break print_anyconsts(step) for i in range(step, last_check_step+1): print_failed_asserts(i) -- cgit v1.2.3