From c075486c59155d16ed278922a3752366a95246ff Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Sun, 28 Jul 2019 16:03:54 +0200 Subject: [PATCH] Reimplement opt_share to work on $alu and $pmux --- passes/opt/opt_share.cc | 320 ++++++++++++------ tests/opt/opt_share_add_sub.v | 10 + tests/opt/opt_share_add_sub.ys | 13 + tests/opt/opt_share_cat.v | 2 +- tests/opt/opt_share_cat.ys | 18 +- tests/opt/opt_share_cat_multiuser.v | 22 ++ tests/opt/opt_share_cat_multiuser.ys | 13 + tests/opt/opt_share_diff_port_widths.v | 21 ++ tests/opt/opt_share_diff_port_widths.ys | 13 + tests/opt/opt_share_extend.v | 19 ++ tests/opt/opt_share_extend.ys | 13 + tests/opt/opt_share_large_pmux_cat.v | 22 ++ tests/opt/opt_share_large_pmux_cat.ys | 13 + .../opt/opt_share_large_pmux_cat_multipart.v | 25 ++ .../opt/opt_share_large_pmux_cat_multipart.ys | 15 + tests/opt/opt_share_large_pmux_multipart.v | 24 ++ tests/opt/opt_share_large_pmux_multipart.ys | 13 + tests/opt/opt_share_large_pmux_part.v | 22 ++ tests/opt/opt_share_large_pmux_part.ys | 13 + tests/opt/opt_share_mux_tree.v | 2 +- tests/opt/opt_share_mux_tree.ys | 19 +- 21 files changed, 520 insertions(+), 112 deletions(-) create mode 100644 tests/opt/opt_share_add_sub.v create mode 100644 tests/opt/opt_share_add_sub.ys create mode 100644 tests/opt/opt_share_cat_multiuser.v create mode 100644 tests/opt/opt_share_cat_multiuser.ys create mode 100644 tests/opt/opt_share_diff_port_widths.v create mode 100644 tests/opt/opt_share_diff_port_widths.ys create mode 100644 tests/opt/opt_share_extend.v create mode 100644 tests/opt/opt_share_extend.ys create mode 100644 tests/opt/opt_share_large_pmux_cat.v create mode 100644 tests/opt/opt_share_large_pmux_cat.ys create mode 100644 tests/opt/opt_share_large_pmux_cat_multipart.v create mode 100644 tests/opt/opt_share_large_pmux_cat_multipart.ys create mode 100644 tests/opt/opt_share_large_pmux_multipart.v create mode 100644 tests/opt/opt_share_large_pmux_multipart.ys create mode 100644 tests/opt/opt_share_large_pmux_part.v create mode 100644 tests/opt/opt_share_large_pmux_part.ys diff --git a/passes/opt/opt_share.cc b/passes/opt/opt_share.cc index 9f6f59b64..e9a2f05f9 100644 --- a/passes/opt/opt_share.cc +++ b/passes/opt/opt_share.cc @@ -31,12 +31,21 @@ PRIVATE_NAMESPACE_BEGIN SigMap assign_map; +struct InPort { + RTLIL::SigSpec sig; + RTLIL::Cell *pmux; + int port_id; + RTLIL::Cell *alu; + + InPort(RTLIL::SigSpec s, RTLIL::Cell *c, int p, RTLIL::Cell *a = NULL) : sig(s), pmux(c), port_id(p), alu(a) {} +}; + // Helper class that to track whether a SigSpec is signed and whether it is // connected to the \\B port of the $sub cell, which makes its sign prefix // negative. struct ExtSigSpec { RTLIL::SigSpec sig; - bool sign; + RTLIL::SigSpec sign; bool is_signed; ExtSigSpec() {} @@ -45,7 +54,7 @@ struct ExtSigSpec { ExtSigSpec(RTLIL::Cell *cell, RTLIL::IdString port_name, SigMap *sigmap) { - sign = (cell->type == "$sub") && (port_name == "\\B"); + sign = (port_name == "\\B") ? cell->getPort("\\BI") : RTLIL::Const(0, 1); sig = (*sigmap)(cell->getPort(port_name)); is_signed = false; @@ -67,23 +76,22 @@ struct ExtSigSpec { return is_signed < other.is_signed; } - bool operator==(const RTLIL::SigSpec &other) const { return sign ? false : sig == other; } + bool operator==(const RTLIL::SigSpec &other) const { return (sign != RTLIL::Const(0, 1)) ? false : sig == other; } bool operator==(const ExtSigSpec &other) const { return is_signed == other.is_signed && sign == other.sign && sig == other.sig; } }; -void merge_operators(RTLIL::Module *module, RTLIL::Cell *mux, const std::vector &operators, int offset, int width, +void merge_operators(RTLIL::Module *module, RTLIL::Cell *mux, const std::vector &ports, int offset, int width, const ExtSigSpec &operand) { std::vector muxed_operands; int max_width = 0; - for (auto op : operators) { - for (auto &conn : op->connections()) { - if (op->output(conn.first)) - continue; + for (const auto& p : ports) { + auto op = p.alu; - if (conn.second != operand.sig) { - auto operand = ExtSigSpec(op, conn.first, &assign_map); + for (RTLIL::IdString port_name : {"\\A", "\\B"}) { + if (op->getPort(port_name) != operand.sig) { + auto operand = ExtSigSpec(op, port_name, &assign_map); if (operand.sig.size() > max_width) { max_width = operand.sig.size(); } @@ -97,29 +105,60 @@ void merge_operators(RTLIL::Module *module, RTLIL::Cell *mux, const std::vector< operand.sig.extend_u0(max_width, operand.is_signed); } - auto shared_op = operators[0]; + auto shared_op = ports[0].alu; - for (auto op : operators) { + for (const auto& p : ports) { + auto op = p.alu; if (op == shared_op) continue; module->remove(op); } - RTLIL::SigSpec mux_out = mux->getPort("\\Y"); + for (auto &muxed_op : muxed_operands) { + if (muxed_op.sign != muxed_operands[0].sign) { + muxed_op = ExtSigSpec(module->Neg(NEW_ID, muxed_op.sig, muxed_op.is_signed)); + } + } + + RTLIL::SigSpec mux_y = mux->getPort("\\Y"); + RTLIL::SigSpec mux_a = mux->getPort("\\A"); + RTLIL::SigSpec mux_b = mux->getPort("\\B"); + RTLIL::SigSpec mux_s = mux->getPort("\\S"); + + RTLIL::SigSpec alu_x = shared_op->getPort("\\X"); + RTLIL::SigSpec alu_co = shared_op->getPort("\\CO"); - if (muxed_operands[0].sign != muxed_operands[1].sign) { - muxed_operands[1] = ExtSigSpec(module->Neg(NEW_ID, muxed_operands[1].sig, muxed_operands[1].is_signed)); + RTLIL::SigSpec shared_pmux_a = RTLIL::Const(RTLIL::State::Sx, max_width); + RTLIL::SigSpec shared_pmux_b; + RTLIL::SigSpec shared_pmux_s; + + shared_op->setPort("\\Y", shared_op->getPort("\\Y").extract(0, width)); + + if (mux->type == "$pmux") { + shared_pmux_s = RTLIL::SigSpec(); + + for (const auto&p: ports) { + shared_pmux_s.append(mux_s[p.port_id]); + mux_b.replace(p.port_id * mux_a.size() + offset, shared_op->getPort("\\Y")); + } + } else { + shared_pmux_s = RTLIL::SigSpec{mux_s, module->Not(NEW_ID, mux_s)}; + mux_a.replace(offset, shared_op->getPort("\\Y")); + mux_b.replace(offset, shared_op->getPort("\\Y")); } - auto mux_to_oper = module->Mux(NEW_ID, muxed_operands[0].sig, muxed_operands[1].sig, mux->getPort("\\S")); + mux->setPort("\\Y", mux_y); + mux->setPort("\\S", mux_s); + mux->setPort("\\B", mux_b); - shared_op->setPort("\\Y", mux_out.extract(offset, width)); - shared_op->setParam("\\Y_WIDTH", width); + for (const auto &op : muxed_operands) + shared_pmux_b.append(op.sig); - auto dummy = module->addWire(NEW_ID, width); + auto mux_to_oper = module->Pmux(NEW_ID, shared_pmux_a, shared_pmux_b, shared_pmux_s); - mux_out.replace(offset, dummy); - mux->setPort("\\Y", mux_out); + shared_op->setPort("\\X", alu_x.extract(0, width)); + shared_op->setPort("\\CO", alu_co.extract(0, width)); + shared_op->setParam("\\Y_WIDTH", width); if (shared_op->getPort("\\A") == operand.sig) { shared_op->setPort("\\B", mux_to_oper); @@ -128,81 +167,132 @@ void merge_operators(RTLIL::Module *module, RTLIL::Cell *mux, const std::vector< shared_op->setPort("\\A", mux_to_oper); shared_op->setParam("\\A_WIDTH", max_width); } + } typedef struct { RTLIL::Cell *mux; - std::vector operators; + std::vector ports; int offset; int width; ExtSigSpec shared_operand; } shared_op_t; -bool find_op_res_width(int offset, int &width, RTLIL::SigSpec porta, RTLIL::SigSpec portb, - const dict &op_outbit_to_outsig, const dict &op_outbit_user_cnt) + +template void remove_val(std::vector &v, const std::vector &vals) +{ + auto val_iter = vals.rbegin(); + for (auto i = v.rbegin(); i != v.rend(); ++i) + if ((val_iter != vals.rend()) && (*i == *val_iter)) { + v.erase(i.base() - 1); + ++val_iter; + } +} + +bool find_op_res_width(int offset, int &width, std::vector& ports, const dict &op_outbit_to_outsig) { - std::array op_outsigs{op_outbit_to_outsig.at(porta[offset]), op_outbit_to_outsig.at(portb[offset])}; + std::vector op_outsigs; + dict> op_outsig_span; + + std::transform(ports.begin(), ports.end(), std::back_inserter(op_outsigs), [&](InPort *p) { return op_outbit_to_outsig.at(p->sig[offset]); }); + + std::vector finished(ports.size(), false); width = 0; - bool multi_user = false; - while (true) { - for (const auto &op_outsig : op_outsigs) - if (op_outbit_user_cnt.at(op_outsig[width]) > 1) - multi_user = true; + std::function all_finished = [&] { return std::find(std::begin(finished), std::end(finished), false) == end(finished);}; + while (!all_finished()) + { ++offset; ++width; - if ((offset >= porta.size()) || (width >= op_outsigs[0].size()) || (width >= op_outsigs[1].size())) - break; + if (offset >= ports[0]->sig.size()) { + for (size_t i = 0; i < op_outsigs.size(); ++i) { + if (finished[i]) + continue; + + op_outsig_span[width].insert(ports[i]); + finished[i] = true; + } - if ((porta[offset] != op_outsigs[0][width]) || (portb[offset] != op_outsigs[1][width])) break; + } + + for (size_t i = 0; i < op_outsigs.size(); ++i) { + if (finished[i]) + continue; + + if ((width >= op_outsigs[i].size()) || (ports[i]->sig[offset] != op_outsigs[i][width])) { + op_outsig_span[width].insert(ports[i]); + finished[i] = true; + } + } } - if (multi_user) - return false; + for (auto w: op_outsig_span) { + if (w.second.size() > 1) { + width = w.first; + + ports.erase(std::remove_if(ports.begin(), ports.end(), [&](InPort *p) { return !w.second.count(p); }), ports.end()); - for (const auto &outsig : op_outsigs) - for (int i = width; i < outsig.size(); i++) - if (op_outbit_user_cnt.count(outsig[i])) - return false; + return true; + } + } - return true; + return false; } -ExtSigSpec find_shared_operand(const std::vector &operators, const std::map> &operand_to_users) +ExtSigSpec find_shared_operand(InPort* seed, std::vector &ports, const std::map> &operand_to_users) { + std::set alus_using_operand; + std::set alus_set; + for(const auto& p: ports) + alus_set.insert(p->alu); - std::set operators_set(operators.begin(), operators.end()); ExtSigSpec oper; - auto op_a = operators[0]; - for (auto &conn : op_a->connections()) { - if (op_a->output(conn.first)) + auto op_a = seed->alu; + + for (RTLIL::IdString port_name : {"\\A", "\\B"}) { + oper = ExtSigSpec(op_a, port_name, &assign_map); + auto operand_users = operand_to_users.at(oper); + + if (operand_users.size() == 1) continue; - oper = ExtSigSpec(op_a, conn.first, &assign_map); - auto bundle = operand_to_users.at(oper); + alus_using_operand.clear(); + std::set_intersection(operand_users.begin(), operand_users.end(), alus_set.begin(), alus_set.end(), + std::inserter(alus_using_operand, alus_using_operand.begin())); - if (std::includes(bundle.begin(), bundle.end(), operators_set.begin(), operators_set.end())) - break; + if (alus_using_operand.size() > 1) { + ports.erase(std::remove_if(ports.begin(), ports.end(), [&](InPort *p) { return !alus_using_operand.count(p->alu); }), + ports.end()); + return oper; + } } - return oper; + return ExtSigSpec(); } -dict find_op_outbit_user_cnt(RTLIL::Module *module, const dict &op_outbit_to_outsig) +void remove_multi_user_outbits(RTLIL::Module *module, dict &op_outbit_to_outsig) { dict op_outbit_user_cnt; std::function update_op_outbit_user_cnt = [&](SigSpec sig) { auto outsig = assign_map(sig); - for (auto outbit : outsig) - if (op_outbit_to_outsig.count(outbit)) - op_outbit_user_cnt[outbit]++; + for (auto outbit : outsig) { + if (!op_outbit_to_outsig.count(outbit)) + continue; + + if (++op_outbit_user_cnt[outbit] > 1) { + auto alu_outsig = op_outbit_to_outsig.at(outbit); + + for (auto outbit : alu_outsig) + op_outbit_to_outsig.erase(outbit); + } + } }; for (auto cell : module->cells()) @@ -216,8 +306,6 @@ dict find_op_outbit_user_cnt(RTLIL::Module *module, const di update_op_outbit_user_cnt(w); } - - return op_outbit_user_cnt; } struct OptRmdffPass : public Pass { @@ -246,24 +334,31 @@ struct OptRmdffPass : public Pass { dict outsig_to_operator; dict op_outbit_to_outsig; bool any_shared_operands = false; + std::vector op_insigs; for (auto cell : module->cells()) { - if (!cell->type.in("$add", "$sub")) + if (!cell->type.in("$alu")) continue; - for (auto &conn : cell->connections()) { - if (cell->output(conn.first)) { - auto outsig = assign_map(conn.second); - for (auto outbit : outsig) - op_outbit_to_outsig[outbit] = outsig; - - outsig_to_operator[outsig] = cell; - } else { - auto op_insig = ExtSigSpec(cell, conn.first, &assign_map); - operand_to_users[op_insig].insert(cell); - if (operand_to_users[op_insig].size() > 1) - any_shared_operands = true; - } + RTLIL::SigSpec sig_bi = cell->getPort("\\BI"); + RTLIL::SigSpec sig_ci = cell->getPort("\\CI"); + + if ((!sig_bi.is_fully_const()) || (!sig_ci.is_fully_const()) || (sig_bi != sig_ci)) + continue; + + RTLIL::SigSpec sig_y = cell->getPort("\\A"); + + auto outsig = assign_map(cell->getPort("\\Y")); + outsig_to_operator[outsig] = cell; + for (auto outbit : outsig) + op_outbit_to_outsig[outbit] = outsig; + + for (RTLIL::IdString port_name : {"\\A", "\\B"}) { + auto op_insig = ExtSigSpec(cell, port_name, &assign_map); + op_insigs.push_back(op_insig); + operand_to_users[op_insig].insert(cell); + if (operand_to_users[op_insig].size() > 1) + any_shared_operands = true; } } @@ -272,42 +367,77 @@ struct OptRmdffPass : public Pass { // Operator outputs need to be exclusively connected to the $mux inputs in order to be mergeable. Hence we count to // how many points are operator output bits connected. - dict op_outbit_user_cnt = find_op_outbit_user_cnt(module, op_outbit_to_outsig); + remove_multi_user_outbits(module, op_outbit_to_outsig); + std::vector shared_ops; for (auto cell : module->cells()) { - if (!cell->type.in("$mux", "$_MUX_")) + if (!cell->type.in("$mux", "$_MUX_", "$pmux")) continue; - auto porta = assign_map(cell->getPort("\\A")); - auto portb = assign_map(cell->getPort("\\B")); + RTLIL::SigSpec sig_a = cell->getPort("\\A"); + RTLIL::SigSpec sig_b = cell->getPort("\\B"); + RTLIL::SigSpec sig_s = cell->getPort("\\S"); + + std::vector ports; + + if (cell->type.in("$mux", "$_MUX_")) { + ports.push_back(InPort(assign_map(sig_a), cell, 0)); + ports.push_back(InPort(assign_map(sig_b), cell, 1)); + } else { + RTLIL::SigSpec sig_s = cell->getPort("\\S"); + for (int i = 0; i < sig_s.size(); i++) { + auto inp = sig_b.extract(i * sig_a.size(), sig_a.size()); + ports.push_back(InPort(assign_map(inp), cell, i)); + } + } // Look through the bits of the $mux inputs and see which of them are connected to the operator // results. Operator results can be concatenated with other signals before led to the $mux. - for (int i = 0; i < porta.size(); ++i) { - std::array mux_inbits{porta[i], portb[i]}; + for (int i = 0; i < sig_a.size(); ++i) { + std::vector alu_ports; + for (auto& p: ports) + if (op_outbit_to_outsig.count(p.sig[i])) { + p.alu = outsig_to_operator.at(op_outbit_to_outsig.at(p.sig[i])); + alu_ports.push_back(&p); + } + + int alu_port_width = 0; + + while (alu_ports.size() > 1) { + std::vector shared_ports(alu_ports); + + auto seed = alu_ports[0]; + alu_ports.erase(alu_ports.begin()); - // Are the results of an $add or $sub operators connected to both of this $mux inputs? - if (!op_outbit_to_outsig.count(mux_inbits[0]) or !op_outbit_to_outsig.count(mux_inbits[1])) - continue; + // Find ports whose $alu-s share an operand with $alu connected to the seed port + auto shared_operand = find_shared_operand(seed, shared_ports, operand_to_users); - std::vector operators; - for (const auto &b : mux_inbits) - operators.push_back(outsig_to_operator.at(op_outbit_to_outsig.at(b))); + if (shared_operand.empty()) + continue; - // Do these operators share an operand? - auto shared_operand = find_shared_operand(operators, operand_to_users); - if (shared_operand.empty()) - continue; + // Some bits of the operator results might be unconnected. Calculate the number of conneted + // bits. + if (!find_op_res_width(i, alu_port_width, shared_ports, op_outbit_to_outsig)) + break; - // Some bits of the operator results might be unconnected. Calculate the number of conneted - // bits. - int width; + if (shared_ports.size() < 2) + break; - if (find_op_res_width(i, width, porta, portb, op_outbit_to_outsig, op_outbit_user_cnt)) - shared_ops.push_back(shared_op_t{cell, operators, i, width, shared_operand}); + // Remember the combination for the merger + std::vector shared_p; + for (auto p: shared_ports) + shared_p.push_back(*p); - i += width - 1; + shared_ops.push_back(shared_op_t{cell, shared_p, i, alu_port_width, shared_operand}); + + // Remove merged ports from the list and try to find other mergers for the mux + remove_val(alu_ports, shared_ports); + } + + if (alu_port_width) + i += alu_port_width - 1; } + } for (auto &shared : shared_ops) { @@ -315,11 +445,11 @@ struct OptRmdffPass : public Pass { "of " "them:\n", log_id(shared.mux->type), log_id(shared.mux)); - for (auto op : shared.operators) - log(" %s\n", log_id(op)); + for (const auto& op : shared.ports) + log(" %s\n", log_id(op.alu)); log("\n"); - merge_operators(module, shared.mux, shared.operators, shared.offset, shared.width, shared.shared_operand); + merge_operators(module, shared.mux, shared.ports, shared.offset, shared.width, shared.shared_operand); } } } diff --git a/tests/opt/opt_share_add_sub.v b/tests/opt/opt_share_add_sub.v new file mode 100644 index 000000000..30e093a39 --- /dev/null +++ b/tests/opt/opt_share_add_sub.v @@ -0,0 +1,10 @@ +module opt_share_test( + input [15:0] a, + input [15:0] b, + input sel, + output [15:0] res, + ); + + assign res = {sel ? a + b : a - b}; + +endmodule diff --git a/tests/opt/opt_share_add_sub.ys b/tests/opt/opt_share_add_sub.ys new file mode 100644 index 000000000..4a5406791 --- /dev/null +++ b/tests/opt/opt_share_add_sub.ys @@ -0,0 +1,13 @@ +read_verilog opt_share_add_sub.v +proc;; +copy opt_share_test merged + +alumacc merged +opt merged +opt_share merged +opt_clean merged + +miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter +sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter + +select -assert-count 1 -module merged t:$alu diff --git a/tests/opt/opt_share_cat.v b/tests/opt/opt_share_cat.v index c32073360..605dcfe59 100644 --- a/tests/opt/opt_share_cat.v +++ b/tests/opt/opt_share_cat.v @@ -1,4 +1,4 @@ -module add_sub( +module opt_share_test( input [15:0] a, input [15:0] b, input [15:0] c, diff --git a/tests/opt/opt_share_cat.ys b/tests/opt/opt_share_cat.ys index c3f2f5a2f..7de69bfde 100644 --- a/tests/opt/opt_share_cat.ys +++ b/tests/opt/opt_share_cat.ys @@ -1,9 +1,13 @@ read_verilog opt_share_cat.v -prep -flatten -opt -pmuxtree -opt_share -opt_clean +proc;; +copy opt_share_test merged -select -assert-count 2 t:$sub -select -assert-count 0 t:$add +alumacc merged +opt merged +opt_share merged +opt_clean merged + +miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter +sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter + +select -assert-count 2 -module merged t:$alu diff --git a/tests/opt/opt_share_cat_multiuser.v b/tests/opt/opt_share_cat_multiuser.v new file mode 100644 index 000000000..9ac0ceec8 --- /dev/null +++ b/tests/opt/opt_share_cat_multiuser.v @@ -0,0 +1,22 @@ +module opt_share_test( + input [15:0] a, + input [15:0] b, + input [15:0] c, + input [15:0] d, + input sel, + output reg [47:0] res, + ); + + wire [15:0] add_res = a+b; + wire [15:0] sub_res = a-b; + wire [31: 0] cat1 = {add_res, c+d}; + wire [31: 0] cat2 = {sub_res, c-d}; + + always @* begin + case(sel) + 0: res = {cat1, add_res}; + 1: res = {cat2, add_res}; + endcase + end + +endmodule diff --git a/tests/opt/opt_share_cat_multiuser.ys b/tests/opt/opt_share_cat_multiuser.ys new file mode 100644 index 000000000..6a82fbd79 --- /dev/null +++ b/tests/opt/opt_share_cat_multiuser.ys @@ -0,0 +1,13 @@ +read_verilog opt_share_cat_multiuser.v +proc;; +copy opt_share_test merged + +alumacc merged +opt merged +opt_share merged +opt_clean merged + +miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter +sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter + +select -assert-count 3 -module merged t:$alu diff --git a/tests/opt/opt_share_diff_port_widths.v b/tests/opt/opt_share_diff_port_widths.v new file mode 100644 index 000000000..5e2971e30 --- /dev/null +++ b/tests/opt/opt_share_diff_port_widths.v @@ -0,0 +1,21 @@ +module opt_share_test( + input [15:0] a, + input [15:0] b, + input [15:0] c, + input [1:0] sel, + output reg [15:0] res + ); + + wire [15:0] add0_res = a+b; + wire [15:0] add1_res = a+c; + + always @* begin + case(sel) + 0: res = add0_res[10:0]; + 1: res = add1_res[10:0]; + 2: res = a - b; + default: res = 32'bx; + endcase + end + +endmodule diff --git a/tests/opt/opt_share_diff_port_widths.ys b/tests/opt/opt_share_diff_port_widths.ys new file mode 100644 index 000000000..ec5e9f7b0 --- /dev/null +++ b/tests/opt/opt_share_diff_port_widths.ys @@ -0,0 +1,13 @@ +read_verilog opt_share_diff_port_widths.v +proc;; +copy opt_share_test merged + +alumacc merged +opt merged +opt_share merged +opt_clean merged + +miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter +sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter + +select -assert-count 2 -module merged t:$alu diff --git a/tests/opt/opt_share_extend.v b/tests/opt/opt_share_extend.v new file mode 100644 index 000000000..5ed6bde6f --- /dev/null +++ b/tests/opt/opt_share_extend.v @@ -0,0 +1,19 @@ +module opt_share_test( + input signed [7:0] a, + input signed [10:0] b, + input signed [15:0] c, + input [1:0] sel, + output reg signed [15:0] res + ); + + + always @* begin + case(sel) + 0: res = a + b; + 1: res = a - b; + 2: res = a + c; + default: res = 16'bx; + endcase + end + +endmodule diff --git a/tests/opt/opt_share_extend.ys b/tests/opt/opt_share_extend.ys new file mode 100644 index 000000000..c553ee0fb --- /dev/null +++ b/tests/opt/opt_share_extend.ys @@ -0,0 +1,13 @@ +read_verilog opt_share_extend.v +proc;; +copy opt_share_test merged + +alumacc merged +opt merged +opt_share merged +opt_clean merged + +miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter +sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter + +select -assert-count 1 -module merged t:$alu diff --git a/tests/opt/opt_share_large_pmux_cat.v b/tests/opt/opt_share_large_pmux_cat.v new file mode 100644 index 000000000..6208c796b --- /dev/null +++ b/tests/opt/opt_share_large_pmux_cat.v @@ -0,0 +1,22 @@ +module opt_share_test( + input [15:0] a, + input [15:0] b, + input [15:0] c, + input [2:0] sel, + output reg [31:0] res + ); + + + always @* begin + case(sel) + 0: res = {a + b, a}; + 1: res = {a - b, b}; + 2: res = {a + c, c}; + 3: res = {a - c, a}; + 4: res = {b, b}; + 5: res = {c, c}; + default: res = 32'bx; + endcase + end + +endmodule diff --git a/tests/opt/opt_share_large_pmux_cat.ys b/tests/opt/opt_share_large_pmux_cat.ys new file mode 100644 index 000000000..4186ca52e --- /dev/null +++ b/tests/opt/opt_share_large_pmux_cat.ys @@ -0,0 +1,13 @@ +read_verilog opt_share_large_pmux_cat.v +proc;; +copy opt_share_test merged + +alumacc merged +opt merged +opt_share merged +opt_clean merged + +miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter +sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter + +select -assert-count 1 -module merged t:$alu diff --git a/tests/opt/opt_share_large_pmux_cat_multipart.v b/tests/opt/opt_share_large_pmux_cat_multipart.v new file mode 100644 index 000000000..f97971bf6 --- /dev/null +++ b/tests/opt/opt_share_large_pmux_cat_multipart.v @@ -0,0 +1,25 @@ +module opt_share_test( + input [15:0] a, + input [15:0] b, + input [15:0] c, + input [15:0] d, + input [2:0] sel, + output reg [31:0] res + ); + + wire [15:0] add0_res = a+d; + + always @* begin + case(sel) + 0: res = {add0_res, a}; + 1: res = {a - b, add0_res[7], 15'b0}; + 2: res = {b-a, b}; + 3: res = {d, b - c}; + 4: res = {d, b - a}; + 5: res = {c, d}; + 6: res = {a - c, b-d}; + default: res = 32'bx; + endcase + end + +endmodule diff --git a/tests/opt/opt_share_large_pmux_cat_multipart.ys b/tests/opt/opt_share_large_pmux_cat_multipart.ys new file mode 100644 index 000000000..54d200dc7 --- /dev/null +++ b/tests/opt/opt_share_large_pmux_cat_multipart.ys @@ -0,0 +1,15 @@ +read_verilog opt_share_large_pmux_cat_multipart.v +proc;; +copy opt_share_test merged + +alumacc merged +opt merged + +opt_share merged +opt_clean merged +opt -full + +miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter +sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter + +select -assert-count 4 -module merged t:$alu diff --git a/tests/opt/opt_share_large_pmux_multipart.v b/tests/opt/opt_share_large_pmux_multipart.v new file mode 100644 index 000000000..e7ba318ef --- /dev/null +++ b/tests/opt/opt_share_large_pmux_multipart.v @@ -0,0 +1,24 @@ +module opt_share_test( + input [15:0] a, + input [15:0] b, + input [15:0] c, + input [15:0] d, + input [2:0] sel, + output reg [15:0] res + ); + + + always @* begin + case(sel) + 0: res = a + d; + 1: res = a - b; + 2: res = b; + 3: res = b - c; + 4: res = b - a; + 5: res = c; + 6: res = a - c; + default: res = 16'bx; + endcase + end + +endmodule diff --git a/tests/opt/opt_share_large_pmux_multipart.ys b/tests/opt/opt_share_large_pmux_multipart.ys new file mode 100644 index 000000000..11182df1a --- /dev/null +++ b/tests/opt/opt_share_large_pmux_multipart.ys @@ -0,0 +1,13 @@ +read_verilog opt_share_large_pmux_multipart.v +proc;; +copy opt_share_test merged + +alumacc merged +opt merged +opt_share merged +opt_clean merged + +miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter +sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter + +select -assert-count 2 -module merged t:$alu diff --git a/tests/opt/opt_share_large_pmux_part.v b/tests/opt/opt_share_large_pmux_part.v new file mode 100644 index 000000000..138be0cd6 --- /dev/null +++ b/tests/opt/opt_share_large_pmux_part.v @@ -0,0 +1,22 @@ +module opt_share_test( + input [15:0] a, + input [15:0] b, + input [15:0] c, + input [2:0] sel, + output reg [15:0] res + ); + + + always @* begin + case(sel) + 0: res = a + b; + 1: res = a - b; + 2: res = a + c; + 3: res = a - c; + 4: res = b; + 5: res = c; + default: res = 16'bx; + endcase + end + +endmodule diff --git a/tests/opt/opt_share_large_pmux_part.ys b/tests/opt/opt_share_large_pmux_part.ys new file mode 100644 index 000000000..6b594a3d6 --- /dev/null +++ b/tests/opt/opt_share_large_pmux_part.ys @@ -0,0 +1,13 @@ +read_verilog opt_share_large_pmux_part.v +proc;; +copy opt_share_test merged + +alumacc merged +opt merged +opt_share merged +opt_clean merged + +miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter +sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter + +select -assert-count 1 -module merged t:$alu diff --git a/tests/opt/opt_share_mux_tree.v b/tests/opt/opt_share_mux_tree.v index 807ed2978..c90826204 100644 --- a/tests/opt/opt_share_mux_tree.v +++ b/tests/opt/opt_share_mux_tree.v @@ -1,4 +1,4 @@ -module add_sub( +module opt_share_test( input [15:0] a, input [15:0] b, input [15:0] c, diff --git a/tests/opt/opt_share_mux_tree.ys b/tests/opt/opt_share_mux_tree.ys index 94d6aa7d2..58473039f 100644 --- a/tests/opt/opt_share_mux_tree.ys +++ b/tests/opt/opt_share_mux_tree.ys @@ -1,10 +1,13 @@ read_verilog opt_share_mux_tree.v -prep -flatten -opt -pmuxtree -opt_share; -opt_share; -opt_clean +proc;; +copy opt_share_test merged -select -assert-count 1 t:$add -select -assert-count 0 t:$sub +alumacc merged +opt merged +opt_share merged +opt_clean merged + +miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp opt_share_test merged miter +sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter + +select -assert-count 1 -module merged t:$alu -- 2.30.2