From 08b55a20e36a24d09be9016ceda658bc8ba04ad3 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Mon, 30 Sep 2019 14:11:01 -0700 Subject: [PATCH 01/19] module->derive() to be lazy and not touch ast if already derived --- frontends/ast/ast.cc | 82 +++++++++++++++++++++++++++----------------- frontends/ast/ast.h | 2 +- 2 files changed, 51 insertions(+), 33 deletions(-) diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index 21279cbfa..e4539f303 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -1382,10 +1382,10 @@ void AstModule::reprocess_module(RTLIL::Design *design, dict parameters, dict interfaces, dict modports, bool mayfail) +RTLIL::IdString AstModule::derive(RTLIL::Design *design, dict parameters, dict interfaces, dict modports, bool /*mayfail*/) { AstNode *new_ast = NULL; - std::string modname = derive_common(design, parameters, &new_ast, mayfail); + std::string modname = derive_common(design, parameters, &new_ast); // Since interfaces themselves may be instantiated with different parameters, // "modname" must also take those into account, so that unique modules @@ -1455,10 +1455,10 @@ RTLIL::IdString AstModule::derive(RTLIL::Design *design, dict parameters, bool mayfail) +RTLIL::IdString AstModule::derive(RTLIL::Design *design, dict parameters, bool /*mayfail*/) { AstNode *new_ast = NULL; - std::string modname = derive_common(design, parameters, &new_ast, mayfail); + std::string modname = derive_common(design, parameters, &new_ast); if (!design->has(modname)) { new_ast->str = modname; @@ -1473,47 +1473,75 @@ RTLIL::IdString AstModule::derive(RTLIL::Design *design, dict parameters, AstNode **new_ast_out, bool) +std::string AstModule::derive_common(RTLIL::Design *design, dict parameters, AstNode **new_ast_out) { std::string stripped_name = name.str(); if (stripped_name.compare(0, 9, "$abstract") == 0) stripped_name = stripped_name.substr(9); - log_header(design, "Executing AST frontend in derive mode using pre-parsed AST for module `%s'.\n", stripped_name.c_str()); - loadconfig(); - std::string para_info; - AstNode *new_ast = ast->clone(); int para_counter = 0; - int orig_parameters_n = parameters.size(); - for (auto it = new_ast->children.begin(); it != new_ast->children.end(); it++) { - AstNode *child = *it; + for (const auto child : ast->children) { if (child->type != AST_PARAMETER) continue; para_counter++; std::string para_id = child->str; if (parameters.count(para_id) > 0) { log("Parameter %s = %s\n", child->str.c_str(), log_signal(RTLIL::SigSpec(parameters[child->str]))); - rewrite_parameter: para_info += stringf("%s=%s", child->str.c_str(), log_signal(RTLIL::SigSpec(parameters[para_id]))); - delete child->children.at(0); - if ((parameters[para_id].flags & RTLIL::CONST_FLAG_REAL) != 0) { - child->children[0] = new AstNode(AST_REALVALUE); - child->children[0]->realvalue = std::stod(parameters[para_id].decode_string()); - } else if ((parameters[para_id].flags & RTLIL::CONST_FLAG_STRING) != 0) - child->children[0] = AstNode::mkconst_str(parameters[para_id].decode_string()); - else - child->children[0] = AstNode::mkconst_bits(parameters[para_id].bits, (parameters[para_id].flags & RTLIL::CONST_FLAG_SIGNED) != 0); - parameters.erase(para_id); continue; } para_id = stringf("$%d", para_counter); + if (parameters.count(para_id) > 0) { + log("Parameter %d (%s) = %s\n", para_counter, child->str.c_str(), log_signal(RTLIL::SigSpec(parameters[para_id]))); + para_info += stringf("%s=%s", child->str.c_str(), log_signal(RTLIL::SigSpec(parameters[para_id]))); + continue; + } + } + + std::string modname; + if (parameters.size() == 0) + modname = stripped_name; + else if (para_info.size() > 60) + modname = "$paramod$" + sha1(para_info) + stripped_name; + else + modname = "$paramod" + stripped_name + para_info; + + if (design->has(modname)) + return modname; + + log_header(design, "Executing AST frontend in derive mode using pre-parsed AST for module `%s'.\n", stripped_name.c_str()); + loadconfig(); + + AstNode *new_ast = ast->clone(); + para_counter = 0; + for (auto child : new_ast->children) { + if (child->type != AST_PARAMETER) + continue; + para_counter++; + std::string para_id = child->str; + if (parameters.count(para_id) > 0) { + log("Parameter %s = %s\n", child->str.c_str(), log_signal(RTLIL::SigSpec(parameters[child->str]))); + goto rewrite_parameter; + } + para_id = stringf("$%d", para_counter); if (parameters.count(para_id) > 0) { log("Parameter %d (%s) = %s\n", para_counter, child->str.c_str(), log_signal(RTLIL::SigSpec(parameters[para_id]))); goto rewrite_parameter; } + continue; + rewrite_parameter: + delete child->children.at(0); + if ((parameters[para_id].flags & RTLIL::CONST_FLAG_REAL) != 0) { + child->children[0] = new AstNode(AST_REALVALUE); + child->children[0]->realvalue = std::stod(parameters[para_id].decode_string()); + } else if ((parameters[para_id].flags & RTLIL::CONST_FLAG_STRING) != 0) + child->children[0] = AstNode::mkconst_str(parameters[para_id].decode_string()); + else + child->children[0] = AstNode::mkconst_bits(parameters[para_id].bits, (parameters[para_id].flags & RTLIL::CONST_FLAG_SIGNED) != 0); + parameters.erase(para_id); } for (auto param : parameters) { @@ -1526,16 +1554,6 @@ std::string AstModule::derive_common(RTLIL::Design *design, dictchildren.push_back(defparam); } - std::string modname; - - if (orig_parameters_n == 0) - modname = stripped_name; - else if (para_info.size() > 60) - modname = "$paramod$" + sha1(para_info) + stripped_name; - else - modname = "$paramod" + stripped_name + para_info; - - (*new_ast_out) = new_ast; return modname; } diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h index 93fee913e..0ec249ab9 100644 --- a/frontends/ast/ast.h +++ b/frontends/ast/ast.h @@ -296,7 +296,7 @@ namespace AST ~AstModule() YS_OVERRIDE; RTLIL::IdString derive(RTLIL::Design *design, dict parameters, bool mayfail) YS_OVERRIDE; RTLIL::IdString derive(RTLIL::Design *design, dict parameters, dict interfaces, dict modports, bool mayfail) YS_OVERRIDE; - std::string derive_common(RTLIL::Design *design, dict parameters, AstNode **new_ast_out, bool mayfail); + std::string derive_common(RTLIL::Design *design, dict parameters, AstNode **new_ast_out); void reprocess_module(RTLIL::Design *design, dict local_interfaces) YS_OVERRIDE; RTLIL::Module *clone() const YS_OVERRIDE; void loadconfig() const; From 0a1af434e8acfaa692d7990bce68fd23daed9519 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Mon, 30 Sep 2019 14:52:04 -0700 Subject: [PATCH 02/19] Fix for svinterfaces --- frontends/ast/ast.cc | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index e4539f303..37a69d8bf 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -1398,11 +1398,17 @@ RTLIL::IdString AstModule::derive(RTLIL::Design *design, dicthas(modname)) { + if (!design->has(new_modname)) { + if (!new_ast) { + auto mod = dynamic_cast(design->module(modname)); + new_ast = mod->ast->clone(); + } + modname = new_modname; new_ast->str = modname; // Iterate over all interfaces which are ports in this module: From d963e8c2c6207ad98d48dc528922ad58c030173f Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 27 Sep 2019 17:00:19 -0700 Subject: [PATCH 03/19] Fix typo --- kernel/rtlil.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 17be28f78..ded1cd60e 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -1528,7 +1528,7 @@ std::vector RTLIL::Module::selected_wires() const std::vector RTLIL::Module::selected_cells() const { std::vector result; - result.reserve(wires_.size()); + result.reserve(cells_.size()); for (auto &it : cells_) if (design->selected(this, it.second)) result.push_back(it.second); From f2f19df2d4387ae70f5b063f2bd6e7cbdaa1ce75 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 27 Sep 2019 17:44:01 -0700 Subject: [PATCH 04/19] Add -select option to aigmap --- passes/techmap/aigmap.cc | 46 ++++++++++++++++++++++++++++++++++------ 1 file changed, 40 insertions(+), 6 deletions(-) diff --git a/passes/techmap/aigmap.cc b/passes/techmap/aigmap.cc index 1d5e1286b..2ecb2f35a 100644 --- a/passes/techmap/aigmap.cc +++ b/passes/techmap/aigmap.cc @@ -27,6 +27,7 @@ struct AigmapPass : public Pass { AigmapPass() : Pass("aigmap", "map logic to and-inverter-graph circuit") { } void help() YS_OVERRIDE { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); log(" aigmap [options] [selection]\n"); log("\n"); @@ -36,10 +37,15 @@ struct AigmapPass : public Pass { log(" -nand\n"); log(" Enable creation of $_NAND_ cells\n"); log("\n"); + log(" -select\n"); + log(" Overwrite replaced cells in the current selection with new $_AND_,\n"); + log(" $_NOT_, and $_NAND_, cells\n"); + + log("\n"); } void execute(std::vector args, RTLIL::Design *design) YS_OVERRIDE { - bool nand_mode = false; + bool nand_mode = false, select_mode = false; log_header(design, "Executing AIGMAP pass (map logic to AIG).\n"); @@ -50,6 +56,10 @@ struct AigmapPass : public Pass { nand_mode = true; continue; } + if (args[argidx] == "-select") { + select_mode = true; + continue; + } break; } extra_args(args, argidx, design); @@ -62,6 +72,7 @@ struct AigmapPass : public Pass { dict stat_not_replaced; int orig_num_cells = GetSize(module->cells()); + pool new_sel; for (auto cell : module->selected_cells()) { Aig aig(cell); @@ -75,6 +86,8 @@ struct AigmapPass : public Pass { if (aig.name.empty()) { not_replaced_count++; stat_not_replaced[cell->type]++; + if (select_mode) + new_sel.insert(cell->name); continue; } @@ -95,19 +108,33 @@ struct AigmapPass : public Pass { SigBit A = sigs.at(node.left_parent); SigBit B = sigs.at(node.right_parent); if (nand_mode && node.inverter) { - bit = module->NandGate(NEW_ID, A, B); + bit = module->addWire(NEW_ID); + auto gate = module->addNandGate(NEW_ID, A, B, bit); + if (select_mode) + new_sel.insert(gate->name); + goto skip_inverter; } else { pair key(node.left_parent, node.right_parent); if (and_cache.count(key)) bit = and_cache.at(key); - else - bit = module->AndGate(NEW_ID, A, B); + else { + bit = module->addWire(NEW_ID); + auto gate = module->addAndGate(NEW_ID, A, B, bit); + if (select_mode) + new_sel.insert(gate->name); + } } } - if (node.inverter) - bit = module->NotGate(NEW_ID, bit); + if (node.inverter) { + SigBit new_bit = module->addWire(NEW_ID); + auto gate = module->addNotGate(NEW_ID, bit, new_bit); + bit = new_bit; + if (select_mode) + new_sel.insert(gate->name); + + } skip_inverter: for (auto &op : node.outports) @@ -142,6 +169,13 @@ struct AigmapPass : public Pass { for (auto cell : replaced_cells) module->remove(cell); + + if (select_mode) { + log_assert(!design->selection_stack.empty()); + RTLIL::Selection& sel = design->selection_stack.back(); + sel.selected_members[module->name] = std::move(new_sel); + } + } } } AigmapPass; From 8b239ee707a2bf4a868728046d7f64c16d74aa2a Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Mon, 30 Sep 2019 15:34:04 -0700 Subject: [PATCH 05/19] Add quick test --- tests/techmap/aigmap.ys | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 tests/techmap/aigmap.ys diff --git a/tests/techmap/aigmap.ys b/tests/techmap/aigmap.ys new file mode 100644 index 000000000..a40aa39f1 --- /dev/null +++ b/tests/techmap/aigmap.ys @@ -0,0 +1,10 @@ +read_verilog < Date: Mon, 30 Sep 2019 17:20:12 -0700 Subject: [PATCH 06/19] techmap wires named _TECHMAP_REPLACE_. to create alias --- passes/techmap/techmap.cc | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc index 08a1af2d5..8f8cff9fa 100644 --- a/passes/techmap/techmap.cc +++ b/passes/techmap/techmap.cc @@ -257,6 +257,12 @@ struct TechmapWorker w->add_strpool_attribute(ID(src), extra_src_attrs); } design->select(module, w); + + if (it.second->name.begins_with("\\_TECHMAP_REPLACE_.")) { + IdString replace_name = stringf("%s%s", orig_cell_name.c_str(), it.second->name.c_str() + strlen("\\_TECHMAP_REPLACE_")); + Wire *replace_w = module->addWire(replace_name, it.second); + module->connect(replace_w, w); + } } SigMap tpl_sigmap(tpl); @@ -1198,6 +1204,10 @@ struct TechmapPass : public Pass { log("\n"); log("A cell with the name _TECHMAP_REPLACE_ in the map file will inherit the name\n"); log("and attributes of the cell that is being replaced.\n"); + log("A wire with a name of the form `_TECHMAP_REPLACE_.` in the map file will\n"); + log("cause a new wire alias to be created with its name set to the original but with\n"); + log("its `_TECHMAP_REPLACE_' prefix to be substituted with the name of the cell being\n"); + log("replaced.\n"); log("\n"); log("See 'help extract' for a pass that does the opposite thing.\n"); log("\n"); From 369652d4b99181e2f7b875b6c458c1a5a3b0381e Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Mon, 30 Sep 2019 17:20:39 -0700 Subject: [PATCH 07/19] Add test --- tests/techmap/techmap_replace.ys | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 tests/techmap/techmap_replace.ys diff --git a/tests/techmap/techmap_replace.ys b/tests/techmap/techmap_replace.ys new file mode 100644 index 000000000..ee5c6bc7e --- /dev/null +++ b/tests/techmap/techmap_replace.ys @@ -0,0 +1,16 @@ +read_verilog < Date: Tue, 1 Oct 2019 13:46:36 +0100 Subject: [PATCH 08/19] ecp5: Add support for mapping 36-bit wide PDP BRAMs Signed-off-by: David Shah --- techlibs/ecp5/.gitignore | 1 + techlibs/ecp5/Makefile.inc | 2 + techlibs/ecp5/bram.txt | 23 ++++++++ techlibs/ecp5/brams_connect.py | 20 +++++++ techlibs/ecp5/brams_map.v | 42 +++++++++++++++ techlibs/ecp5/cells_bb.v | 96 +++++++++++++++++++++++++++++++++- 6 files changed, 183 insertions(+), 1 deletion(-) diff --git a/techlibs/ecp5/.gitignore b/techlibs/ecp5/.gitignore index 54c329735..9d4723264 100644 --- a/techlibs/ecp5/.gitignore +++ b/techlibs/ecp5/.gitignore @@ -6,4 +6,5 @@ bram_conn_2.vh bram_conn_4.vh bram_conn_9.vh bram_conn_18.vh +bram_conn_36.vh brams_connect.mk diff --git a/techlibs/ecp5/Makefile.inc b/techlibs/ecp5/Makefile.inc index 80eee5004..b03da164c 100644 --- a/techlibs/ecp5/Makefile.inc +++ b/techlibs/ecp5/Makefile.inc @@ -44,6 +44,7 @@ techlibs/ecp5/bram_conn_2.vh: techlibs/ecp5/brams_connect.mk techlibs/ecp5/bram_conn_4.vh: techlibs/ecp5/brams_connect.mk techlibs/ecp5/bram_conn_9.vh: techlibs/ecp5/brams_connect.mk techlibs/ecp5/bram_conn_18.vh: techlibs/ecp5/brams_connect.mk +techlibs/ecp5/bram_conn_36.vh: techlibs/ecp5/brams_connect.mk $(eval $(call add_gen_share_file,share/ecp5,techlibs/ecp5/bram_init_1_2_4.vh)) $(eval $(call add_gen_share_file,share/ecp5,techlibs/ecp5/bram_init_9_18_36.vh)) @@ -53,3 +54,4 @@ $(eval $(call add_gen_share_file,share/ecp5,techlibs/ecp5/bram_conn_2.vh)) $(eval $(call add_gen_share_file,share/ecp5,techlibs/ecp5/bram_conn_4.vh)) $(eval $(call add_gen_share_file,share/ecp5,techlibs/ecp5/bram_conn_9.vh)) $(eval $(call add_gen_share_file,share/ecp5,techlibs/ecp5/bram_conn_18.vh)) +$(eval $(call add_gen_share_file,share/ecp5,techlibs/ecp5/bram_conn_36.vh)) diff --git a/techlibs/ecp5/bram.txt b/techlibs/ecp5/bram.txt index f223a42b8..570960489 100644 --- a/techlibs/ecp5/bram.txt +++ b/techlibs/ecp5/bram.txt @@ -1,3 +1,18 @@ +bram $__ECP5_PDPW16KD + init 1 + + abits 9 + dbits 36 + + groups 2 + ports 1 1 + wrmode 1 0 + enable 4 1 + transp 0 0 + clocks 2 3 + clkpol 2 3 +endbram + bram $__ECP5_DP16KD init 1 @@ -22,6 +37,14 @@ bram $__ECP5_DP16KD clkpol 2 3 endbram +match $__ECP5_PDPW16KD + min bits 2048 + min efficiency 5 + shuffle_enable B + make_transp + or_next_if_better +endmatch + match $__ECP5_DP16KD min bits 2048 min efficiency 5 diff --git a/techlibs/ecp5/brams_connect.py b/techlibs/ecp5/brams_connect.py index f86dcfcf0..098607c59 100755 --- a/techlibs/ecp5/brams_connect.py +++ b/techlibs/ecp5/brams_connect.py @@ -10,6 +10,18 @@ def write_bus_ports(f, ada_bits, adb_bits, dia_bits, dob_bits): print(" %s," % ", ".join(dia_conn), file=f) print(" %s," % ", ".join(dob_conn), file=f) +def write_bus_ports_pdp(f, adw_bits, adr_bits, di_bits, do_bits, be_bits): + adw_conn = [".ADW%d(%s)" % (i, adw_bits[i]) for i in range(len(adw_bits))] + adr_conn = [".ADR%d(%s)" % (i, adr_bits[i]) for i in range(len(adr_bits))] + di_conn = [".DI%d(%s)" % (i, di_bits[i]) for i in range(len(di_bits))] + do_conn = [".DO%d(%s)" % (i, do_bits[i]) for i in range(len(do_bits))] + be_conn = [".BE%d(%s)" % (i, be_bits[i]) for i in range(len(be_bits))] + print(" %s," % ", ".join(adw_conn), file=f) + print(" %s," % ", ".join(adr_conn), file=f) + print(" %s," % ", ".join(di_conn), file=f) + print(" %s," % ", ".join(do_conn), file=f) + print(" %s," % ", ".join(be_conn), file=f) + with open("techlibs/ecp5/bram_conn_1.vh", "w") as f: ada_bits = ["A1ADDR[%d]" % i for i in range(14)] adb_bits = ["B1ADDR[%d]" % i for i in range(14)] @@ -44,3 +56,11 @@ with open("techlibs/ecp5/bram_conn_18.vh", "w") as f: dia_bits = ["A1DATA[%d]" % i for i in range(18)] dob_bits = ["B1DATA[%d]" % i for i in range(18)] write_bus_ports(f, ada_bits, adb_bits, dia_bits, dob_bits) + +with open("techlibs/ecp5/bram_conn_36.vh", "w") as f: + adw_bits = ["A1ADDR[%d]" % i for i in range(9)] + adr_bits = ["1'b0", "1'b0", "1'b0", "1'b0", "1'b0"] + ["B1ADDR[%d]" % i for i in range(9)] + di_bits = ["A1DATA[%d]" % i for i in range(36)] + do_bits = ["B1DATA[%d]" % (i + 18) for i in range(18)] + ["B1DATA[%d]" % i for i in range(18)] + be_bits = ["A1EN[%d]" % i for i in range(4)] + write_bus_ports_pdp(f, adw_bits, adr_bits, di_bits, do_bits, be_bits) diff --git a/techlibs/ecp5/brams_map.v b/techlibs/ecp5/brams_map.v index 0353cbadb..310aedaf2 100644 --- a/techlibs/ecp5/brams_map.v +++ b/techlibs/ecp5/brams_map.v @@ -113,3 +113,45 @@ module \$__ECP5_DP16KD (CLK2, CLK3, A1ADDR, A1DATA, A1EN, B1ADDR, B1DATA, B1EN); wire TECHMAP_FAIL = 1'b1; end endgenerate endmodule + +module \$__ECP5_PDPW16KD (CLK2, CLK3, A1ADDR, A1DATA, A1EN, B1ADDR, B1DATA, B1EN); + parameter CFG_ABITS = 9; + parameter CFG_DBITS = 36; + parameter CFG_ENABLE_A = 4; + + parameter CLKPOL2 = 1; + parameter CLKPOL3 = 1; + parameter [18431:0] INIT = 18432'bx; + + input CLK2; + input CLK3; + + input [CFG_ABITS-1:0] A1ADDR; + input [CFG_DBITS-1:0] A1DATA; + input [CFG_ENABLE_A-1:0] A1EN; + + input [CFG_ABITS-1:0] B1ADDR; + output [CFG_DBITS-1:0] B1DATA; + input B1EN; + + localparam CLKWMUX = CLKPOL2 ? "CLKA" : "INV"; + localparam CLKRMUX = CLKPOL3 ? "CLKB" : "INV"; + + localparam WRITEMODE_A = TRANSP2 ? "WRITETHROUGH" : "READBEFOREWRITE"; + + PDPW16KD #( + `include "bram_init_9_18_36.vh" + .DATA_WIDTH_W(36), + .DATA_WIDTH_R(36), + .CLKWMUX(CLKWMUX), + .CLKRMUX(CLKRMUX), + .GSR("AUTO") + ) _TECHMAP_REPLACE_ ( + `include "bram_conn_36.vh" + .CLKW(CLK2), .CLKR(CLK3), + .CEW(1'b1), + .CER(B1EN), .OCER(1'b1), + .RST(1'b0) + ); + +endmodule diff --git a/techlibs/ecp5/cells_bb.v b/techlibs/ecp5/cells_bb.v index 8557053b6..0a5046db2 100644 --- a/techlibs/ecp5/cells_bb.v +++ b/techlibs/ecp5/cells_bb.v @@ -683,4 +683,98 @@ endmodule module SGSR ( input GSR, CLK ); -endmodule \ No newline at end of file +endmodule + + +(* blackbox *) +module PDPW16KD ( + input DI35, DI34, DI33, DI32, DI31, DI30, DI29, DI28, DI27, DI26, DI25, DI24, DI23, DI22, DI21, DI20, DI19, DI18, + input DI17, DI16, DI15, DI14, DI13, DI12, DI11, DI10, DI9, DI8, DI7, DI6, DI5, DI4, DI3, DI2, DI1, DI0, + input ADW8, ADW7, ADW6, ADW5, ADW4, ADW3, ADW2, ADW1, ADW0, + input BE3, BE2, BE1, BE0, CEW, CLKW, CSW2, CSW1, CSW0, + input ADR13, ADR12, ADR11, ADR10, ADR9, ADR8, ADR7, ADR6, ADR5, ADR4, ADR3, ADR2, ADR1, ADR0, + input CER, OCER, CLKR, CSR2, CSR1, CSR0, RST, + output DO35, DO34, DO33, DO32, DO31, DO30, DO29, DO28, DO27, DO26, DO25, DO24, DO23, DO22, DO21, DO20, DO19, DO18, + output DO17, DO16, DO15, DO14, DO13, DO12, DO11, DO10, DO9, DO8, DO7, DO6, DO5, DO4, DO3, DO2, DO1, DO0 +); + parameter DATA_WIDTH_W = 36; + parameter DATA_WIDTH_R = 36; + parameter GSR = "ENABLED"; + + parameter REGMODE = "NOREG"; + + parameter RESETMODE = "SYNC"; + parameter ASYNC_RESET_RELEASE = "SYNC"; + + parameter CSDECODE_W = "0b000"; + parameter CSDECODE_R = "0b000"; + + parameter INITVAL_00 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_01 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_02 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_03 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_04 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_05 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_06 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_07 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_08 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_09 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_0A = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_0B = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_0C = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_0D = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_0E = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_0F = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_10 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_11 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_12 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_13 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_14 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_15 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_16 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_17 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_18 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_19 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_1A = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_1B = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_1C = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_1D = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_1E = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_1F = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_20 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_21 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_22 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_23 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_24 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_25 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_26 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_27 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_28 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_29 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_2A = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_2B = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_2C = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_2D = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_2E = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_2F = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_30 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_31 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_32 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_33 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_34 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_35 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_36 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_37 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_38 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_39 = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_3A = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_3B = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_3C = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_3D = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_3E = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INITVAL_3F = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; + parameter INIT_DATA = "STATIC"; + parameter CLKWMUX = "CLKW"; + parameter CLKRMUX = "CLKR"; + +endmodule From b424d374db354141afe1f42eead3347e5cb86a04 Mon Sep 17 00:00:00 2001 From: David Shah Date: Tue, 1 Oct 2019 14:14:46 +0100 Subject: [PATCH 09/19] ecp5: Fix shuffle_enable port Signed-off-by: David Shah --- techlibs/ecp5/bram.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/techlibs/ecp5/bram.txt b/techlibs/ecp5/bram.txt index 570960489..777ccaa2e 100644 --- a/techlibs/ecp5/bram.txt +++ b/techlibs/ecp5/bram.txt @@ -40,7 +40,7 @@ endbram match $__ECP5_PDPW16KD min bits 2048 min efficiency 5 - shuffle_enable B + shuffle_enable A make_transp or_next_if_better endmatch @@ -48,5 +48,5 @@ endmatch match $__ECP5_DP16KD min bits 2048 min efficiency 5 - shuffle_enable B + shuffle_enable A endmatch From c026579c207b81092e298858acf131c70115f89f Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 1 Oct 2019 18:45:07 +0200 Subject: [PATCH 10/19] Define environ, fixes #1424 --- frontends/rpc/rpc_frontend.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/frontends/rpc/rpc_frontend.cc b/frontends/rpc/rpc_frontend.cc index b4b2fa3a2..83e1353b0 100644 --- a/frontends/rpc/rpc_frontend.cc +++ b/frontends/rpc/rpc_frontend.cc @@ -34,6 +34,8 @@ #include "libs/sha1/sha1.h" #include "kernel/yosys.h" +extern char **environ; + YOSYS_NAMESPACE_BEGIN #if defined(_WIN32) From a84a2d74c779b8023c0bbfc02fa4576d8c4cecca Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 2 Oct 2019 12:48:04 +0200 Subject: [PATCH 11/19] 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(-) 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()) { From 45e4c040d7bafed59ef46f5cf92e7a2adb802bdc Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 2 Oct 2019 13:35:03 +0200 Subject: [PATCH 12/19] Add "check -mapped" Signed-off-by: Clifford Wolf --- CHANGELOG | 1 + passes/cmds/check.cc | 56 +++++++++++++++++++++++++++----------------- 2 files changed, 36 insertions(+), 21 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index c1ffaa44a..1fc139d49 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -50,6 +50,7 @@ Yosys 0.9 .. Yosys 0.9-dev - "synth_ecp5" to now infer DSP blocks (-nodsp to disable, experimental) - "synth_ice40 -dsp" to infer DSP blocks - Added latch support to synth_xilinx + - Added "check -mapped" Yosys 0.8 .. Yosys 0.9 ---------------------- diff --git a/passes/cmds/check.cc b/passes/cmds/check.cc index 64697c134..87dc34209 100644 --- a/passes/cmds/check.cc +++ b/passes/cmds/check.cc @@ -47,6 +47,9 @@ struct CheckPass : public Pass { log("When called with -initdrv then this command also checks for wires which have\n"); log("the 'init' attribute set and aren't driven by a FF cell type.\n"); log("\n"); + log("When called with -mapped then this command also checks for internal cells\n"); + log("that have not been mapped to cells of the target architecture.\n"); + log("\n"); log("When called with -assert then the command will produce an error if any\n"); log("problems are found in the current design.\n"); log("\n"); @@ -56,6 +59,7 @@ struct CheckPass : public Pass { int counter = 0; bool noinit = false; bool initdrv = false; + bool mapped = false; bool assert_mode = false; size_t argidx; @@ -68,6 +72,10 @@ struct CheckPass : public Pass { initdrv = true; continue; } + if (args[argidx] == "-mapped") { + mapped = true; + continue; + } if (args[argidx] == "-assert") { assert_mode = true; continue; @@ -135,29 +143,35 @@ struct CheckPass : public Pass { TopoSort topo; for (auto cell : module->cells()) - for (auto &conn : cell->connections()) { - SigSpec sig = sigmap(conn.second); - bool logic_cell = yosys_celltypes.cell_evaluable(cell->type); - if (cell->input(conn.first)) - for (auto bit : sig) - if (bit.wire) { + { + if (mapped && cell->type.begins_with("$") && design->module(cell->type) == nullptr) { + log_warning("Cell %s.%s is an unmapped internal cell of type %s.\n", log_id(module), log_id(cell), log_id(cell->type)); + counter++; + } + for (auto &conn : cell->connections()) { + SigSpec sig = sigmap(conn.second); + bool logic_cell = yosys_celltypes.cell_evaluable(cell->type); + if (cell->input(conn.first)) + for (auto bit : sig) + if (bit.wire) { + if (logic_cell) + topo.edge(stringf("wire %s", log_signal(bit)), + stringf("cell %s (%s)", log_id(cell), log_id(cell->type))); + used_wires.insert(bit); + } + if (cell->output(conn.first)) + for (int i = 0; i < GetSize(sig); i++) { if (logic_cell) - topo.edge(stringf("wire %s", log_signal(bit)), - stringf("cell %s (%s)", log_id(cell), log_id(cell->type))); - used_wires.insert(bit); + topo.edge(stringf("cell %s (%s)", log_id(cell), log_id(cell->type)), + stringf("wire %s", log_signal(sig[i]))); + if (sig[i].wire) + wire_drivers[sig[i]].push_back(stringf("port %s[%d] of cell %s (%s)", + log_id(conn.first), i, log_id(cell), log_id(cell->type))); } - if (cell->output(conn.first)) - for (int i = 0; i < GetSize(sig); i++) { - if (logic_cell) - topo.edge(stringf("cell %s (%s)", log_id(cell), log_id(cell->type)), - stringf("wire %s", log_signal(sig[i]))); - if (sig[i].wire) - wire_drivers[sig[i]].push_back(stringf("port %s[%d] of cell %s (%s)", - log_id(conn.first), i, log_id(cell), log_id(cell->type))); - } - if (!cell->input(conn.first) && cell->output(conn.first)) - for (auto bit : sig) - if (bit.wire) wire_drivers_count[bit]++; + if (!cell->input(conn.first) && cell->output(conn.first)) + for (auto bit : sig) + if (bit.wire) wire_drivers_count[bit]++; + } } pool init_bits; From a4f2f7d23cb27f7677236d7a1823f36215c874e9 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 2 Oct 2019 12:43:18 -0700 Subject: [PATCH 13/19] Extend test with renaming cells with prefix too --- tests/techmap/techmap_replace.ys | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/techmap/techmap_replace.ys b/tests/techmap/techmap_replace.ys index ee5c6bc7e..c2f42d50b 100644 --- a/tests/techmap/techmap_replace.ys +++ b/tests/techmap/techmap_replace.ys @@ -2,6 +2,7 @@ read_verilog < Date: Wed, 2 Oct 2019 12:43:35 -0700 Subject: [PATCH 14/19] Also rename cells with _TECHMAP_REPLACE_. prefix, as per @cliffordwolf --- passes/techmap/techmap.cc | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc index 8f8cff9fa..0c57733d4 100644 --- a/passes/techmap/techmap.cc +++ b/passes/techmap/techmap.cc @@ -384,6 +384,8 @@ struct TechmapWorker if (techmap_replace_cell) c_name = orig_cell_name; + else if (it.second->name.begins_with("\\_TECHMAP_REPLACE_.")) + c_name = stringf("%s%s", orig_cell_name.c_str(), c_name.c_str() + strlen("\\_TECHMAP_REPLACE_")); else apply_prefix(cell->name, c_name); @@ -1204,10 +1206,12 @@ struct TechmapPass : public Pass { log("\n"); log("A cell with the name _TECHMAP_REPLACE_ in the map file will inherit the name\n"); log("and attributes of the cell that is being replaced.\n"); - log("A wire with a name of the form `_TECHMAP_REPLACE_.` in the map file will\n"); - log("cause a new wire alias to be created with its name set to the original but with\n"); - log("its `_TECHMAP_REPLACE_' prefix to be substituted with the name of the cell being\n"); - log("replaced.\n"); + log("A cell with a name of the form `_TECHMAP_REPLACE_.` in the map file will\n"); + log("be named thus but with the `_TECHMAP_REPLACE_' prefix substituted with the name\n"); + log("of the cell being replaced.\n"); + log("Similarly, a wire named in the form `_TECHMAP_REPLACE_.` will cause a\n"); + log("new wire alias to be created and named as above but with the `_TECHMAP_REPLACE_'\n"); + log("prefix also substituted.\n"); log("\n"); log("See 'help extract' for a pass that does the opposite thing.\n"); log("\n"); From 62c66406ad69c4cf02c3edc843d80e0e2b05c384 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 2 Oct 2019 17:49:07 -0700 Subject: [PATCH 15/19] log_dump() to support State enum --- kernel/log.cc | 4 ++++ kernel/log.h | 1 + kernel/yosys.h | 1 + 3 files changed, 6 insertions(+) diff --git a/kernel/log.cc b/kernel/log.cc index e0a60ca12..c5ba0d10d 100644 --- a/kernel/log.cc +++ b/kernel/log.cc @@ -551,6 +551,10 @@ void log_dump_val_worker(RTLIL::SigSpec v) { log("%s", log_signal(v)); } +void log_dump_val_worker(RTLIL::State v) { + log("%s", log_signal(v)); +} + const char *log_signal(const RTLIL::SigSpec &sig, bool autoint) { std::stringstream buf; diff --git a/kernel/log.h b/kernel/log.h index 5f53f533a..1f15f3459 100644 --- a/kernel/log.h +++ b/kernel/log.h @@ -292,6 +292,7 @@ static inline void log_dump_val_worker(PerformanceTimer p) { log("%f seconds", p static inline void log_dump_args_worker(const char *p YS_ATTRIBUTE(unused)) { log_assert(*p == 0); } void log_dump_val_worker(RTLIL::IdString v); void log_dump_val_worker(RTLIL::SigSpec v); +void log_dump_val_worker(RTLIL::State v); template static inline void log_dump_val_worker(dict &v) { diff --git a/kernel/yosys.h b/kernel/yosys.h index a80cb00b4..179bfe07a 100644 --- a/kernel/yosys.h +++ b/kernel/yosys.h @@ -210,6 +210,7 @@ namespace RTLIL { struct Module; struct Design; struct Monitor; + enum State : unsigned char; } namespace AST { From 3e27b2846bc7d4178f436035d5007ac598bc194d Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 3 Oct 2019 11:49:56 +0200 Subject: [PATCH 16/19] Add "check -allow-tbuf" Signed-off-by: Clifford Wolf --- passes/cmds/check.cc | 30 ++++++++++++++++++++++-------- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/passes/cmds/check.cc b/passes/cmds/check.cc index 87dc34209..820ecac7b 100644 --- a/passes/cmds/check.cc +++ b/passes/cmds/check.cc @@ -41,17 +41,24 @@ struct CheckPass : public Pass { log("\n"); log(" - used wires that do not have a driver\n"); log("\n"); - log("When called with -noinit then this command also checks for wires which have\n"); - log("the 'init' attribute set.\n"); + log("Options:\n"); log("\n"); - log("When called with -initdrv then this command also checks for wires which have\n"); - log("the 'init' attribute set and aren't driven by a FF cell type.\n"); + log(" -noinit\n"); + log(" Also check for wires which have the 'init' attribute set.\n"); log("\n"); - log("When called with -mapped then this command also checks for internal cells\n"); - log("that have not been mapped to cells of the target architecture.\n"); + log(" -initdrv\n"); + log(" Also check for wires that have the 'init' attribute set and are not\n"); + log(" driven by an FF cell type.\n"); log("\n"); - log("When called with -assert then the command will produce an error if any\n"); - log("problems are found in the current design.\n"); + log(" -mapped\n"); + log(" Also check for internal cells that have not been mapped to cells of the\n"); + log(" target architecture.\n"); + log("\n"); + log(" -allow-tbuf\n"); + log(" Modify the -mapped behavior to still allow $_TBUF_ cells.\n"); + log("\n"); + log(" -assert\n"); + log(" Produce a runtime error if any problems are found in the current design.\n"); log("\n"); } void execute(std::vector args, RTLIL::Design *design) YS_OVERRIDE @@ -60,6 +67,7 @@ struct CheckPass : public Pass { bool noinit = false; bool initdrv = false; bool mapped = false; + bool allow_tbuf = false; bool assert_mode = false; size_t argidx; @@ -76,6 +84,10 @@ struct CheckPass : public Pass { mapped = true; continue; } + if (args[argidx] == "-allow-tbuf") { + allow_tbuf = true; + continue; + } if (args[argidx] == "-assert") { assert_mode = true; continue; @@ -145,8 +157,10 @@ struct CheckPass : public Pass { for (auto cell : module->cells()) { if (mapped && cell->type.begins_with("$") && design->module(cell->type) == nullptr) { + if (allow_tbuf && cell->type == ID($_TBUF_)) goto cell_allowed; log_warning("Cell %s.%s is an unmapped internal cell of type %s.\n", log_id(module), log_id(cell), log_id(cell->type)); counter++; + cell_allowed:; } for (auto &conn : cell->connections()) { SigSpec sig = sigmap(conn.second); From be8efd7c7b52285743c7ff3ae51353e03c39f140 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 3 Oct 2019 12:26:08 +0200 Subject: [PATCH 17/19] Bump version Signed-off-by: Clifford Wolf --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 2644721be..aa3fc8099 100644 --- a/Makefile +++ b/Makefile @@ -115,7 +115,7 @@ LDFLAGS += -rdynamic LDLIBS += -lrt endif -YOSYS_VER := 0.9+899 +YOSYS_VER := 0.9+932 GIT_REV := $(shell cd $(YOSYS_SRC) && git rev-parse --short HEAD 2> /dev/null || echo UNKNOWN) OBJS = kernel/version_$(GIT_REV).o From 17cb916cc87a71d862c7994d44f3031656f18002 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 3 Oct 2019 14:05:21 +0200 Subject: [PATCH 18/19] Update ABC to git rev 623b5e8 Signed-off-by: Clifford Wolf --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index aa3fc8099..33c04cf92 100644 --- a/Makefile +++ b/Makefile @@ -128,7 +128,7 @@ bumpversion: # is just a symlink to your actual ABC working directory, as 'make mrproper' # will remove the 'abc' directory and you do not want to accidentally # delete your work on ABC.. -ABCREV = 5776ad0 +ABCREV = 623b5e8 ABCPULL = 1 ABCURL ?= https://github.com/berkeley-abc/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 From 2ed2e9c3e8f2d9d6882588857c8556a6e2af57ea Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 3 Oct 2019 14:59:07 +0200 Subject: [PATCH 19/19] Change smtbmc "Warmup failed" status to "PREUNSAT" Signed-off-by: Clifford Wolf --- backends/smt2/smtbmc.py | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) 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)