From 30c510041a66b89f9f4fceedf2713c43fdc272d2 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Tue, 9 Jun 2026 00:34:13 -0700 Subject: [PATCH 1/4] Fix opt_compact_prefix up --- passes/silimate/opt_compact_prefix.cc | 98 ++++++++++++++----- tests/silimate/opt_compact_prefix.ys | 64 ++++++++++++ tests/silimate/opt_compact_prefix_renamed.sv | 32 ++++++ .../opt_compact_prefix_yosys_frontend.v | 38 +++++++ 4 files changed, 205 insertions(+), 27 deletions(-) create mode 100644 tests/silimate/opt_compact_prefix_renamed.sv create mode 100644 tests/silimate/opt_compact_prefix_yosys_frontend.v diff --git a/passes/silimate/opt_compact_prefix.cc b/passes/silimate/opt_compact_prefix.cc index e9b82f18b..e367e0ee3 100644 --- a/passes/silimate/opt_compact_prefix.cc +++ b/passes/silimate/opt_compact_prefix.cc @@ -60,9 +60,22 @@ struct OptCompactPrefixWorker } } - Wire *port(const char *name) + vector input_ports() { - return module->wire(RTLIL::escape_id(name)); + vector ports; + for (auto wire : module->wires()) + if (wire->port_input) + ports.push_back(wire); + return ports; + } + + vector output_ports() + { + vector ports; + for (auto wire : module->wires()) + if (wire->port_output) + ports.push_back(wire); + return ports; } int count_cells(IdString type) @@ -195,19 +208,36 @@ struct OptCompactPrefixWorker return result; } - bool bmux_selects_stay_in_range(Wire *data, int loop_width) + int output_bits_controlled_by(Wire *control, Wire *output) { - bool saw_data_bmux = false; + pool bits; for (auto cell : module->cells()) { - if (cell->type != ID($bmux)) + if (cell->type != ID($mux)) + continue; + SigSpec sel = sigmap(cell->getPort(ID::S)); + if (GetSize(sel) != 1 || sel[0].wire != control) + continue; + for (auto bit : sigmap(cell->getPort(ID::Y))) + if (bit.wire == output) + bits.insert(bit.offset); + } + return GetSize(bits); + } + + bool indexed_reads_stay_in_range(Wire *data, int loop_width) + { + bool saw_data_read = false; + for (auto cell : module->cells()) { + if (!cell->type.in(ID($bmux), ID($shiftx))) continue; if (sigmap(cell->getPort(ID::A)) != sigmap(SigSpec(data))) continue; - saw_data_bmux = true; - if (eval_sig_at_zero(cell->getPort(ID::S)) >= loop_width) + saw_data_read = true; + IdString select_port = cell->type == ID($bmux) ? ID::S : ID::B; + if (eval_sig_at_zero(cell->getPort(select_port)) >= loop_width) return false; } - return saw_data_bmux; + return saw_data_read; } SigSpec zext(SigSpec sig, int width) @@ -311,12 +341,12 @@ struct OptCompactPrefixWorker bool rewrite_forward_dense_pack() { - Wire *sig = port("sig"); - Wire *sig2 = port("sig2"); - if (!sig || !sig2) - return false; - if (!sig->port_input || !sig2->port_output) + vector inputs = input_ports(); + vector outputs = output_ports(); + if (GetSize(inputs) != 1 || GetSize(outputs) != 1) return false; + Wire *sig = inputs[0]; + Wire *sig2 = outputs[0]; if (GetSize(sig) != GetSize(sig2)) return false; if (GetSize(sig) < 4 || GetSize(sig) > max_width) @@ -325,8 +355,6 @@ struct OptCompactPrefixWorker return false; if (count_binop_const(ID($add), 1) < GetSize(sig) - 2) return false; - if (count_cells(ID($shl)) < GetSize(sig) - 2) - return false; if (count_cells(ID($mux)) < GetSize(sig)) return false; if (!eval_sig_is_zero(SigSpec(sig2))) @@ -357,29 +385,45 @@ struct OptCompactPrefixWorker bool rewrite_reverse_suffix_read() { - Wire *disable = port("disable_in"); - Wire *data = port("data_in"); - Wire *mask = port("mask"); - if (!disable || !data || !mask) + vector inputs = input_ports(); + vector outputs = output_ports(); + if (GetSize(inputs) != 2 || GetSize(outputs) != 1) return false; - if (!disable->port_input || !data->port_input || !mask->port_output) - return false; - if (GetSize(disable) != GetSize(data) || GetSize(mask) != GetSize(data)) - return false; - if (GetSize(module->ports) != 3) + Wire *mask = outputs[0]; + if (GetSize(inputs[0]) != GetSize(inputs[1]) || GetSize(mask) != GetSize(inputs[0])) return false; int dec_count = std::max(count_binop_const(ID($sub), 1), count_binop_const(ID($add), -1)); int loop_width = dec_count + 1; - if (loop_width < 4 || loop_width > max_width || loop_width > GetSize(data)) - return false; if (count_cells(ID($mux)) < loop_width) return false; if (has_binop_const_other_than(ID($sub), 1) || has_binop_const_other_than(ID($add), -1)) return false; - if (!bmux_selects_stay_in_range(data, loop_width)) + + Wire *disable = nullptr; + int controlled_width = 0; + for (auto input : inputs) { + int n = output_bits_controlled_by(input, mask); + if (n == 0) + continue; + if (disable != nullptr) + return false; + disable = input; + controlled_width = n; + } + if (disable == nullptr) + return false; + if (controlled_width > 0) + loop_width = controlled_width; + if (loop_width < 4 || loop_width > max_width || loop_width > GetSize(mask)) + return false; + if (dec_count < loop_width - 1) + return false; + Wire *data = (inputs[0] == disable) ? inputs[1] : inputs[0]; + + if (!indexed_reads_stay_in_range(data, loop_width)) return false; if (!eval_sig_is_zero(SigSpec(mask))) return false; diff --git a/tests/silimate/opt_compact_prefix.ys b/tests/silimate/opt_compact_prefix.ys index 94148be0c..4ed9f0044 100644 --- a/tests/silimate/opt_compact_prefix.ys +++ b/tests/silimate/opt_compact_prefix.ys @@ -114,6 +114,23 @@ select -assert-count 32 t:$gt design -reset log -pop +log -header "Renamed ports: forward dense pack" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_compact_prefix_renamed.sv +verific -import opt_compact_prefix_pack_renamed +proc; opt_clean +opt_compact_prefix +opt_clean +select -assert-none t:$shl +select -assert-none t:$mux +select -assert-count 7 t:$add +select -assert-count 8 t:$gt +design -reset +log -pop + log -header "Exact regression size: 16-entry reverse suffix read" log -push design -reset @@ -131,6 +148,53 @@ select -assert-min 1 t:$eq design -reset log -pop +log -header "Renamed ports: reverse suffix read" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_compact_prefix_renamed.sv +verific -import opt_compact_prefix_sub_renamed +proc; opt_clean +opt_compact_prefix +opt_clean +select -assert-none t:$sub +select -assert-none t:$mux +select -assert-min 1 t:$add +select -assert-min 1 t:$eq +design -reset +log -pop + +log -header "Yosys frontend: forward dense pack" +log -push +design -reset +read_verilog -sv opt_compact_prefix_yosys_frontend.v +hierarchy -top opt_compact_prefix_yosys_pack +proc; opt_clean +opt_compact_prefix +opt_clean +select -assert-none t:$shl +select -assert-none t:$mux +select -assert-count 7 t:$add +select -assert-count 8 t:$gt +design -reset +log -pop + +log -header "Yosys frontend: reverse suffix read" +log -push +design -reset +read_verilog -sv opt_compact_prefix_yosys_frontend.v +hierarchy -top opt_compact_prefix_yosys_sub +proc; opt_clean +opt_compact_prefix +opt_clean +select -assert-none t:$sub +select -assert-none t:$mux +select -assert-min 1 t:$add +select -assert-min 1 t:$eq +design -reset +log -pop + log -header "Reverse suffix read with add-by-minus-one decrement" log -push design -reset diff --git a/tests/silimate/opt_compact_prefix_renamed.sv b/tests/silimate/opt_compact_prefix_renamed.sv new file mode 100644 index 000000000..72e75a60b --- /dev/null +++ b/tests/silimate/opt_compact_prefix_renamed.sv @@ -0,0 +1,32 @@ +module opt_compact_prefix_pack_renamed ( + input logic [7:0] in_bits, + output logic [7:0] packed_bits +); + always_comb begin + packed_bits = '0; + for (int I = 0, indx = 0; I < 8; I++) begin + if (in_bits[I]) begin + packed_bits[indx] = in_bits[I]; + indx += 1; + end + end + end +endmodule + +module opt_compact_prefix_sub_renamed ( + input logic [15:0] stall_vec, + input logic [15:0] payload_vec, + output logic [15:0] allow_mask +); + always_comb begin + allow_mask = '0; + for (int I = 8, indx = 8; I > 0; I--) begin + if (stall_vec[I-1]) begin + allow_mask[I-1] = 1'b0; + end else begin + allow_mask[I-1] = payload_vec[indx-1]; + indx = indx - 1; + end + end + end +endmodule diff --git a/tests/silimate/opt_compact_prefix_yosys_frontend.v b/tests/silimate/opt_compact_prefix_yosys_frontend.v new file mode 100644 index 000000000..3f8968a9a --- /dev/null +++ b/tests/silimate/opt_compact_prefix_yosys_frontend.v @@ -0,0 +1,38 @@ +module opt_compact_prefix_yosys_pack ( + input wire [7:0] in_bits, + output reg [7:0] packed_bits +); + integer I; + integer indx; + always @* begin + packed_bits = 8'b0; + indx = 0; + for (I = 0; I < 8; I = I + 1) begin + if (in_bits[I]) begin + packed_bits[indx] = in_bits[I]; + indx = indx + 1; + end + end + end +endmodule + +module opt_compact_prefix_yosys_sub ( + input wire [15:0] stall_vec, + input wire [15:0] payload_vec, + output reg [15:0] allow_mask +); + integer I; + integer indx; + always @* begin + allow_mask = 16'b0; + indx = 8; + for (I = 8; I > 0; I = I - 1) begin + if (stall_vec[I-1]) begin + allow_mask[I-1] = 1'b0; + end else begin + allow_mask[I-1] = payload_vec[indx-1]; + indx = indx - 1; + end + end + end +endmodule From 4a35c0ab87aaf70667e205329effe712c3331da9 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Tue, 9 Jun 2026 01:57:11 -0700 Subject: [PATCH 2/4] opt_argmax fixes --- passes/opt/opt_argmax.cc | 56 ++++++++++++++++++++++++++++-------- tests/silimate/opt_argmax.sv | 36 +++++++++++++++++++++++ tests/silimate/opt_argmax.ys | 43 +++++++++++++++++++++++++++ 3 files changed, 123 insertions(+), 12 deletions(-) diff --git a/passes/opt/opt_argmax.cc b/passes/opt/opt_argmax.cc index 8c685e902..59f7bde76 100644 --- a/passes/opt/opt_argmax.cc +++ b/passes/opt/opt_argmax.cc @@ -75,6 +75,7 @@ struct OptArgmaxWorker SigSpec values_sig; std::string index_name; std::string values_name; + bool identity_index = false; int width = 0; int index_width = 0; int value_width = 0; @@ -240,9 +241,10 @@ struct OptArgmaxWorker for (auto bit : sigmap(cand.valid_sig)) if (bit.wire) allowed.insert(bit); - for (auto bit : sigmap(cand.index_sig)) - if (bit.wire) - allowed.insert(bit); + if (!cand.identity_index) + for (auto bit : sigmap(cand.index_sig)) + if (bit.wire) + allowed.insert(bit); for (auto bit : sigmap(cand.values_sig)) if (bit.wire) allowed.insert(bit); @@ -344,16 +346,16 @@ struct OptArgmaxWorker return vectors; } - int expected_argmax(const TestVector &tv, int width, int value_width) + int expected_argmax(const TestVector &tv, int width, int value_width, bool identity_index) { uint64_t mask = value_mask(value_width); int best_idx = 0; bool best_valid = tv.valid[0] != 0; - uint64_t best_value = tv.values[tv.index[0]] & mask; + uint64_t best_value = tv.values[identity_index ? 0 : tv.index[0]] & mask; for (int k = 1; k < width; k++) { bool cand_valid = tv.valid[k] != 0; - uint64_t cand_value = tv.values[tv.index[k]] & mask; + uint64_t cand_value = tv.values[identity_index ? k : tv.index[k]] & mask; if (!best_valid && cand_valid) { best_idx = k; best_valid = true; @@ -372,14 +374,15 @@ struct OptArgmaxWorker ConstEval ce(module); SigSpec out_sig = sigmap(SigSpec(cand.out_wire)); SigSpec valid_sig = sigmap(cand.valid_sig); - SigSpec index_sig = sigmap(cand.index_sig); + SigSpec index_sig = cand.identity_index ? SigSpec() : sigmap(cand.index_sig); SigSpec values_sig = sigmap(cand.values_sig); vector vectors = make_test_vectors(cand.width, cand.value_width); for (auto &tv : vectors) { ce.push(); ce.set(valid_sig, packed_valid_const(tv.valid)); - ce.set(index_sig, packed_table_const(tv.index, cand.index_width)); + if (!cand.identity_index) + ce.set(index_sig, packed_table_const(tv.index, cand.index_width)); ce.set(values_sig, packed_table_const(tv.values, cand.value_width)); SigSpec out = out_sig; @@ -390,7 +393,7 @@ struct OptArgmaxWorker return false; int actual = out.as_const().as_int(); - int expected = expected_argmax(tv, cand.width, cand.value_width); + int expected = expected_argmax(tv, cand.width, cand.value_width, cand.identity_index); if (actual != expected) return false; } @@ -481,12 +484,17 @@ struct OptArgmaxWorker { vector leaves; SigSpec valid = sigmap(cand.valid_sig); - SigSpec index_map = sigmap(cand.index_sig); + SigSpec index_map = cand.identity_index ? SigSpec() : sigmap(cand.index_sig); SigSpec values = sigmap(cand.values_sig); for (int k = 0; k < cand.width; k++) { - SigSpec index = index_map.extract(k * cand.index_width, cand.index_width); - SigSpec value = emit_bmux(cand.anchor, values, index); + SigSpec value; + if (cand.identity_index) + value = values.extract(k * cand.value_width, cand.value_width); + else { + SigSpec index = index_map.extract(k * cand.index_width, cand.index_width); + value = emit_bmux(cand.anchor, values, index); + } leaves.push_back({valid[k], value, SigSpec(Const(k, cand.index_width))}); } @@ -666,6 +674,29 @@ struct OptArgmaxWorker values_buses.push_back(bus); } + for (auto &values : values_buses) { + Candidate cand; + cand.out_wire = out; + cand.valid_wire = valid; + cand.valid_sig = SigSpec(valid); + cand.values_sig = values.sig; + cand.index_name = ""; + cand.values_name = values.name; + cand.identity_index = true; + cand.width = width; + cand.index_width = out_width; + cand.value_width = values.elem_width; + if (!check_candidate(cand, cone)) + continue; + + rewrites.push_back(cand); + claimed_outputs.insert(out); + log(" %s: %s <- argmax(valid=%s, index=, values=%s) [N=%d, IW=%d, VW=%d]\n", + log_id(module), log_id(out), log_id(valid), values.name.c_str(), + cand.width, cand.index_width, cand.value_width); + goto next_output; + } + for (auto &index : index_buses) { for (auto &values : values_buses) { if (index.sig == values.sig) @@ -678,6 +709,7 @@ struct OptArgmaxWorker cand.values_sig = values.sig; cand.index_name = index.name; cand.values_name = values.name; + cand.identity_index = false; cand.width = width; cand.index_width = out_width; cand.value_width = values.elem_width; diff --git a/tests/silimate/opt_argmax.sv b/tests/silimate/opt_argmax.sv index eacfae99f..f02c4c3ca 100644 --- a/tests/silimate/opt_argmax.sv +++ b/tests/silimate/opt_argmax.sv @@ -55,6 +55,42 @@ module opt_argmax_w32 ( end endmodule +module opt_argmax_identity_w8 ( + input wire [7:0] valid_in, + input wire [7:0][4:0] val_in, + output reg [2:0] best_idx +); + always_comb begin + best_idx = '0; + for (int k = 1; k < 8; k++) begin + if (!valid_in[best_idx] && valid_in[k]) begin + best_idx = k; + end else if (valid_in[best_idx] && valid_in[k] && + (val_in[best_idx] < val_in[k])) begin + best_idx = k; + end + end + end +endmodule + +module opt_argmax_identity_w16 ( + input wire [15:0] valid_in, + input wire [15:0][7:0] val_in, + output reg [3:0] best_idx +); + always_comb begin + best_idx = '0; + for (int k = 1; k < 16; k++) begin + if (!valid_in[best_idx] && valid_in[k]) begin + best_idx = k; + end else if (valid_in[best_idx] && valid_in[k] && + (val_in[best_idx] < val_in[k])) begin + best_idx = k; + end + end + end +endmodule + module opt_argmax_flat ( input wire [7:0] sig, input wire [23:0] sig3, diff --git a/tests/silimate/opt_argmax.ys b/tests/silimate/opt_argmax.ys index 79c61ebc5..bf96482f8 100644 --- a/tests/silimate/opt_argmax.ys +++ b/tests/silimate/opt_argmax.ys @@ -74,6 +74,49 @@ sat -prove-asserts -verify design -reset log -pop +log -header "Identity-index masked argmax self-equivalence" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_argmax.sv +verific -import opt_argmax_identity_w8 +proc; opt_clean +rename opt_argmax_identity_w8 gold + +read -sv opt_argmax.sv +verific -import opt_argmax_identity_w8 +proc; opt_clean +select -module opt_argmax_identity_w8 +opt_argmax +select -clear +opt_clean +select -assert-min 1 w:*argmax* +rename opt_argmax_identity_w8 gate + +miter -equiv -flatten -make_assert gold gate miter +hierarchy -top miter +proc; opt; memory; opt +sat -prove-asserts -verify +design -reset +log -pop + +log -header "Identity-index masked argmax structural rewrite" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_argmax.sv +verific -import opt_argmax_identity_w16 +proc; opt_clean +opt_argmax +opt_clean +select -assert-min 1 w:*argmax* +select -assert-none c:*argmax_val* +select -assert-none c:LessThan_* +design -reset +log -pop + log -header "Scaled masked argmax: 8 entries structural" log -push design -reset From faea2d904aba193259a32e331e1b78be2141d596 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Tue, 9 Jun 2026 10:55:10 -0700 Subject: [PATCH 3/4] Make opt_compact_prefix match more --- passes/silimate/opt_compact_prefix.cc | 231 ++++++++++++++++++++++- tests/silimate/opt_compact_prefix.ys | 114 +++++++++++ tests/silimate/opt_compact_prefix_mod.sv | 86 +++++++++ 3 files changed, 424 insertions(+), 7 deletions(-) create mode 100644 tests/silimate/opt_compact_prefix_mod.sv diff --git a/passes/silimate/opt_compact_prefix.cc b/passes/silimate/opt_compact_prefix.cc index e367e0ee3..59b8a62c4 100644 --- a/passes/silimate/opt_compact_prefix.cc +++ b/passes/silimate/opt_compact_prefix.cc @@ -19,6 +19,7 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" +#include "kernel/consteval.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -44,6 +45,7 @@ struct OptCompactPrefixWorker int forward_rewrites = 0; int reverse_rewrites = 0; + int modulo_rewrites = 0; int old_cells_removed = 0; int new_cells_emitted = 0; @@ -329,6 +331,25 @@ struct OptCompactPrefixWorker return SigBit(out); } + SigBit emit_bmux(SigSpec table, SigSpec sel) + { + Cell *cell = ref_cell; + log_assert(cell != nullptr); + Wire *out = module->addWire(NEW_ID2_SUFFIX("compact_div"), 1); + module->addBmux(NEW_ID2_SUFFIX("compact_bmux"), table, sel, out); + new_cells_emitted++; + return SigBit(out); + } + + static Const const_u64(uint64_t value, int width) + { + vector bits(width, State::S0); + for (int i = 0; i < width && i < 64; i++) + if ((value >> i) & 1ULL) + bits[i] = State::S1; + return Const(bits); + } + void remove_old_cells(const vector &old_cells) { for (auto cell : old_cells) { @@ -468,13 +489,200 @@ struct OptCompactPrefixWorker return true; } + // Reference function for the modulo-n decimation loop: scanning the enable + // vector from one end, mark every n-th enabled bit. Equivalent closed form: + // mask[I] = en[I] && n>0 && (inclusive_popcount(I) % n == 0) + // where the popcount runs from the scan's leading end down to (incl.) I. + uint64_t expected_modulo_mask(uint64_t en, uint64_t n, int width, bool msb_first) + { + if (n == 0) + return 0; + uint64_t mask = 0; + for (int i = 0; i < width; i++) { + if (!((en >> i) & 1ULL)) + continue; + uint64_t v = 0; + if (msb_first) + for (int k = i; k < width; k++) + v += (en >> k) & 1ULL; + else + for (int k = 0; k <= i; k++) + v += (en >> k) & 1ULL; + if (v % n == 0) + mask |= (1ULL << i); + } + return mask; + } + + // Confirm the combinational function from (en, n) to mask matches the modulo + // decimation reference for the given scan direction, using ConstEval over a + // structured + pseudo-random vector set (cf. opt_argmax's fingerprint). + bool fingerprint_modulo(Wire *en, Wire *n, Wire *mask, int width, bool msb_first) + { + if (width <= 0 || width > 62) + return false; + ConstEval ce(module); + SigSpec en_sig = sigmap(SigSpec(en)); + SigSpec n_sig = sigmap(SigSpec(n)); + SigSpec mask_sig = sigmap(SigSpec(mask)); + int nw = GetSize(n); + + vector nvals; + uint64_t nmax = (nw >= 64) ? ~0ULL : ((1ULL << nw) - 1); + for (uint64_t v = 0; v <= (uint64_t)width + 1 && v <= nmax; v++) + nvals.push_back(v); + if (nmax > (uint64_t)width + 1) + nvals.push_back(nmax); + + uint64_t full = (width >= 64) ? ~0ULL : ((1ULL << width) - 1); + vector envals; + envals.push_back(0); + envals.push_back(full); + envals.push_back(full & 0x5555555555555555ULL); + envals.push_back(full & 0xAAAAAAAAAAAAAAAAULL); + for (int i = 0; i < width; i++) + envals.push_back(1ULL << i); + uint64_t lfsr = 0x1234567089abcdefULL; + for (int r = 0; r < 64; r++) { + lfsr ^= lfsr << 13; + lfsr ^= lfsr >> 7; + lfsr ^= lfsr << 17; + envals.push_back(lfsr & full); + } + + for (uint64_t nv : nvals) + for (uint64_t ev : envals) { + ce.push(); + ce.set(en_sig, const_u64(ev, width)); + ce.set(n_sig, const_u64(nv, nw)); + SigSpec out = mask_sig; + SigSpec undef; + bool ok = ce.eval(out, undef); + ce.pop(); + if (!ok || !out.is_fully_const()) + return false; + Const cv = out.as_const(); + uint64_t actual = 0; + for (int i = 0; i < width && i < 64; i++) + if (cv[i] == State::S1) + actual |= (1ULL << i); + if (actual != expected_modulo_mask(ev, nv, width, msb_first)) + return false; + } + return true; + } + + bool rewrite_modulo_decimation() + { + vector inputs = input_ports(); + vector outputs = output_ports(); + if (GetSize(inputs) != 2 || GetSize(outputs) != 1) + return false; + if (GetSize(module->ports) != 3) + return false; + + Wire *mask = outputs[0]; + int width = GetSize(mask); + if (width < 4 || width > max_width) + return false; + + // en matches the mask width; n (the modulus) is a distinct, narrower bus. + // Requiring different widths also disambiguates from the reverse suffix + // read form, whose two inputs share the mask width. + Wire *en = nullptr, *n = nullptr; + for (auto in : inputs) { + if (GetSize(in) == width && en == nullptr) + en = in; + else + n = in; + } + if (en == nullptr || n == nullptr || en == n || GetSize(n) == width) + return false; + + bool msb_first; + if (fingerprint_modulo(en, n, mask, width, true)) + msb_first = true; + else if (fingerprint_modulo(en, n, mask, width, false)) + msb_first = false; + else + return false; + + vector old_cells(module->cells().begin(), module->cells().end()); + if (old_cells.empty()) + return false; + ref_cell = old_cells.front(); + + int cnt_width = ceil_log2_int(width + 1); + int table_size = 1 << cnt_width; + int cmp_width = std::max(GetSize(n), cnt_width); + + auto en_bit = [&](int i) { return sigmap(SigBit(en, i)); }; + + // 1) Inclusive prefix popcount as a naive linear $add cascade. Each + // running sum is consumed below, so the downstream opt_parallel_prefix + // pass rebuilds the cascade into a shared log-depth prefix network. + vector popcount(width); + Cell *cell = ref_cell; + int start = msb_first ? width - 1 : 0; + int step = msb_first ? -1 : 1; + int last = msb_first ? 0 : width - 1; + SigSpec acc = SigSpec(en_bit(start)); + popcount[start] = zext(acc, cnt_width); + for (int i = start + step; i != last + step; i += step) { + Wire *sum = module->addWire(NEW_ID2_SUFFIX("compact_pop"), cnt_width); + module->addAdd(NEW_ID2_SUFFIX("compact_pop_add"), acc, SigSpec(en_bit(i)), sum); + new_cells_emitted++; + acc = SigSpec(sum); + popcount[i] = SigSpec(sum); + } + + // 2) Decode the modulus once: eq_d = (n == d) for d in [1..width]. + vector eqd(width + 1, State::S0); + for (int d = 1; d <= width; d++) + eqd[d] = emit_eq(SigSpec(n), d, cmp_width); + + // 3) Divisibility per popcount value: div_k = OR_{d | k} eq_d. n>0 and + // n>width fall out for free (no divisor in range matches). + vector divisible(table_size, State::S0); + divisible[0] = State::S1; // gated away by en[]; defined to size the table + for (int k = 1; k <= width; k++) { + SigSpec terms; + for (int d = 1; d <= k; d++) + if (k % d == 0) + terms.append(SigSpec(eqd[d])); + divisible[k] = emit_reduce_or(terms); + } + + // 4) Shared divisibility table; select per bit by its popcount value. + SigSpec table; + for (int k = 0; k < table_size; k++) + table.append(SigSpec(divisible[k])); + + SigSpec out_bits; + for (int i = 0; i < width; i++) { + SigBit sel_divisible = emit_bmux(table, popcount[i]); + out_bits.append(emit_and(en_bit(i), sel_divisible)); + } + + module->connect(SigSpec(mask), out_bits); + remove_old_cells(old_cells); + + log(" Modulo decimation: en=%s, n=%s -> %s, width=%d, %s scan.\n", + log_id(en->name), log_id(n->name), log_id(mask->name), width, + msb_first ? "MSB-first" : "LSB-first"); + modulo_rewrites++; + return true; + } + void run() { if (module->has_processes_warn()) return; if (rewrite_forward_dense_pack()) return; - rewrite_reverse_suffix_read(); + if (rewrite_reverse_suffix_read()) + return; + rewrite_modulo_decimation(); } }; @@ -492,9 +700,16 @@ struct OptCompactPrefixPass : public Pass log("lowering of SystemVerilog loops and replace their long loop-carried\n"); log("index/update cones with balanced prefix-count and routing logic.\n"); log("\n"); - log("Currently this pass handles the dense bit-pack and reverse suffix-read\n"); - log("forms used by the qor_spi_ra_add_chain and qor_spi_ra_sub_chain\n"); - log("regressions. Non-matching modules are left unchanged.\n"); + log("Currently this pass handles the dense bit-pack, reverse suffix-read,\n"); + log("and modulo-n decimation forms used by the qor_spi_ra_add_chain,\n"); + log("qor_spi_ra_sub_chain, and qor_spi_ra_add_chain2 regressions.\n"); + log("Non-matching modules are left unchanged.\n"); + log("\n"); + log("The modulo decimation form (mark every n-th enabled bit while scanning\n"); + log("the enable vector) is lowered to a prefix-popcount plus divisor-decode\n"); + log("divisibility check. The popcount is emitted as a plain linear $add\n"); + log("cascade so a subsequent opt_parallel_prefix pass can rebuild it into a\n"); + log("shared log-depth network.\n"); log("\n"); log(" -max_width \n"); log(" Maximum compaction width to rewrite. Default: 64.\n"); @@ -518,6 +733,7 @@ struct OptCompactPrefixPass : public Pass int total_forward = 0; int total_reverse = 0; + int total_modulo = 0; int total_removed = 0; int total_emitted = 0; @@ -526,15 +742,16 @@ struct OptCompactPrefixPass : public Pass worker.run(); total_forward += worker.forward_rewrites; total_reverse += worker.reverse_rewrites; + total_modulo += worker.modulo_rewrites; total_removed += worker.old_cells_removed; total_emitted += worker.new_cells_emitted; } - log("Rewrote %d forward pack(s), %d reverse suffix read(s); " + log("Rewrote %d forward pack(s), %d reverse suffix read(s), %d modulo decimation(s); " "removed %d old cell(s), emitted %d new cell(s).\n", - total_forward, total_reverse, total_removed, total_emitted); + total_forward, total_reverse, total_modulo, total_removed, total_emitted); - if (total_forward || total_reverse) + if (total_forward || total_reverse || total_modulo) Yosys::run_pass("clean -purge"); } } OptCompactPrefixPass; diff --git a/tests/silimate/opt_compact_prefix.ys b/tests/silimate/opt_compact_prefix.ys index 4ed9f0044..c93c6342d 100644 --- a/tests/silimate/opt_compact_prefix.ys +++ b/tests/silimate/opt_compact_prefix.ys @@ -350,3 +350,117 @@ select -assert-none opt_compact_prefix_multi_match/t:$mux select -assert-count 1 opt_compact_prefix_multi_keep/t:$mux design -reset log -pop + +log -header "Modulo decimation self-equivalence (MSB-first)" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_compact_prefix_mod.sv +verific -import opt_compact_prefix_mod8 +proc; opt_clean +rename opt_compact_prefix_mod8 gold + +read -sv opt_compact_prefix_mod.sv +verific -import opt_compact_prefix_mod8 +proc; opt_clean +opt_compact_prefix +opt_clean +bmuxmap +rename opt_compact_prefix_mod8 gate + +miter -equiv -flatten -make_assert gold gate miter +hierarchy -top miter +proc; opt; memory; opt +sat -prove-asserts -verify +design -reset +log -pop + +log -header "Modulo decimation self-equivalence (LSB-first)" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_compact_prefix_mod.sv +verific -import opt_compact_prefix_mod_lsb8 +proc; opt_clean +rename opt_compact_prefix_mod_lsb8 gold + +read -sv opt_compact_prefix_mod.sv +verific -import opt_compact_prefix_mod_lsb8 +proc; opt_clean +opt_compact_prefix +opt_clean +bmuxmap +rename opt_compact_prefix_mod_lsb8 gate + +miter -equiv -flatten -make_assert gold gate miter +hierarchy -top miter +proc; opt; memory; opt +sat -prove-asserts -verify +design -reset +log -pop + +log -header "Modulo decimation structural rewrite" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_compact_prefix_mod.sv +verific -import opt_compact_prefix_mod16 +proc; opt_clean +opt_compact_prefix +opt_clean +select -assert-none t:$mux +select -assert-none t:$sub +select -assert-min 1 t:$add +select -assert-min 1 t:$eq +select -assert-min 1 t:$bmux +design -reset +log -pop + +log -header "Modulo decimation: opt_parallel_prefix collapses the popcount cascade" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_compact_prefix_mod.sv +verific -import opt_compact_prefix_mod16 +proc; opt_clean +opt_compact_prefix +opt_clean +opt_parallel_prefix -arith +opt_clean +select -assert-none t:$mux +select -assert-none t:$sub +select -assert-min 1 t:$add +design -reset +log -pop + +log -header "Negative: modulo off-by-one near miss unchanged" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_compact_prefix_mod.sv +verific -import opt_compact_prefix_mod_offbyone +proc; opt_clean +opt_compact_prefix +select -assert-none w:*compact* +design -reset +log -pop + +log -header "Max width: modulo decimation left unchanged" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_compact_prefix_mod.sv +verific -import opt_compact_prefix_mod16 +proc; opt_clean +select -assert-min 1 t:$mux +opt_compact_prefix -max_width 8 +select -assert-min 1 t:$mux +select -assert-none w:*compact* +design -reset +log -pop diff --git a/tests/silimate/opt_compact_prefix_mod.sv b/tests/silimate/opt_compact_prefix_mod.sv new file mode 100644 index 000000000..9fbc0001e --- /dev/null +++ b/tests/silimate/opt_compact_prefix_mod.sv @@ -0,0 +1,86 @@ +// Modulo-n decimation loops: scanning the enable vector, mark every n-th +// enabled bit. Exercised by opt_compact_prefix's modulo decimation rewrite +// (cf. the qor_spi_ra_add_chain2 regression). + +module opt_compact_prefix_mod8 ( + input logic [7:0] en, + input logic [3:0] n, + output logic [7:0] mask +); + always_comb begin + mask = '0; + for (int I = 7, cnt = 0; I >= 0; I--) begin + if (en[I] && (n > 0)) begin + if (cnt == (n - 1)) begin + mask[I] = 1'b1; + cnt = 0; + end else begin + cnt++; + end + end + end + end +endmodule + +module opt_compact_prefix_mod16 ( + input logic [15:0] en, + input logic [4:0] n, + output logic [15:0] mask +); + always_comb begin + mask = '0; + for (int I = 15, cnt = 0; I >= 0; I--) begin + if (en[I] && (n > 0)) begin + if (cnt == (n - 1)) begin + mask[I] = 1'b1; + cnt = 0; + end else begin + cnt++; + end + end + end + end +endmodule + +// Same function, but scanned LSB-first (exercises the mirrored direction). +module opt_compact_prefix_mod_lsb8 ( + input logic [7:0] en, + input logic [3:0] n, + output logic [7:0] mask +); + always_comb begin + mask = '0; + for (int I = 0, cnt = 0; I < 8; I++) begin + if (en[I] && (n > 0)) begin + if (cnt == (n - 1)) begin + mask[I] = 1'b1; + cnt = 0; + end else begin + cnt++; + end + end + end + end +endmodule + +// Negative near-miss: marks every (n+1)-th enabled bit (reset on cnt == n), +// a different function that must NOT be rewritten. +module opt_compact_prefix_mod_offbyone ( + input logic [7:0] en, + input logic [3:0] n, + output logic [7:0] mask +); + always_comb begin + mask = '0; + for (int I = 7, cnt = 0; I >= 0; I--) begin + if (en[I] && (n > 0)) begin + if (cnt == n) begin + mask[I] = 1'b1; + cnt = 0; + end else begin + cnt++; + end + end + end + end +endmodule From 3743c4795a1088f0a2e41e83aca3755df43b4525 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Tue, 9 Jun 2026 22:18:20 -0700 Subject: [PATCH 4/4] opt_priority_onehot --- passes/opt/Makefile.inc | 1 + passes/opt/opt_priority_onehot.cc | 828 ++++++++++++++++++++++++++ tests/silimate/opt_priority_onehot.sv | 235 ++++++++ tests/silimate/opt_priority_onehot.ys | 301 ++++++++++ 4 files changed, 1365 insertions(+) create mode 100644 passes/opt/opt_priority_onehot.cc create mode 100644 tests/silimate/opt_priority_onehot.sv create mode 100644 tests/silimate/opt_priority_onehot.ys diff --git a/passes/opt/Makefile.inc b/passes/opt/Makefile.inc index 62f2c537c..6636e9d10 100644 --- a/passes/opt/Makefile.inc +++ b/passes/opt/Makefile.inc @@ -29,6 +29,7 @@ OBJS += passes/opt/opt_argmax.o OBJS += passes/opt/opt_balance_tree.o OBJS += passes/opt/opt_parallel_prefix.o OBJS += passes/opt/opt_prienc.o +OBJS += passes/opt/opt_priority_onehot.o OBJS += passes/opt/peepopt.o GENFILES += passes/opt/peepopt_pm.h diff --git a/passes/opt/opt_priority_onehot.cc b/passes/opt/opt_priority_onehot.cc new file mode 100644 index 000000000..367276c70 --- /dev/null +++ b/passes/opt/opt_priority_onehot.cc @@ -0,0 +1,828 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2026 Akash Levy + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/yosys.h" +#include "kernel/sigtools.h" +#include "kernel/consteval.h" +#include +#include +#include +#include +#include + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +static int clog2_int(int x) +{ + int r = 0; + while ((1 << r) < x) + r++; + return r; +} + +static bool is_power_of_two(int x) +{ + return x > 0 && (x & (x - 1)) == 0; +} + +// Pack a per-lane integer vector into a Const with elem_w bits per lane. +static Const pack_lanes(const vector &vals, int elem_w) +{ + vector bits(vals.size() * elem_w, State::S0); + for (int k = 0; k < GetSize(vals); k++) + for (int b = 0; b < elem_w && b < 31; b++) + if ((vals[k] >> b) & 1) + bits[k * elem_w + b] = State::S1; + return Const(bits); +} + +struct OptPriorityOnehotWorker { + // One detected priority-onehot region ready to be rewritten. + struct Candidate { + Wire *out_wire = nullptr; // one-hot output O (width W = 2^idx_w) + Wire *valid_wire = nullptr; // request / valid bus V (width N) + SigSpec valid_sig; // N bits + SigSpec field_sig; // N * idx_w bits: concatenated per-lane index fields + std::string index_name; + int n = 0; // number of lanes + int w = 0; // output width (power of two) + int idx_w = 0; // clog2(w) == per-lane field width + bool msb_first = false; // priority direction (false: lowest index wins) + Cell *anchor = nullptr; // a driver cell of O, used for naming/src + }; + + struct TestVector { + vector valid; + vector field; + }; + + Module *module; + SigMap sigmap; + dict bit_to_driver; + pool input_port_bits; + Cell *cell = nullptr; + + int min_width = 4; + int max_width = 64; + int regions_rewritten = 0; + int cells_added = 0; + + OptPriorityOnehotWorker(Module *module) : module(module), sigmap(module) + { + build_indexes(); + } + + bool is_sequential(Cell *c) + { + return c->type.in( + ID($ff), ID($dff), ID($dffe), ID($adff), ID($adffe), + ID($sdff), ID($sdffe), ID($sdffce), ID($dffsr), ID($dffsre), + ID($_DFF_P_), ID($_DFF_N_), + ID($_DFFE_PP_), ID($_DFFE_PN_), ID($_DFFE_NP_), ID($_DFFE_NN_), + ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_), + ID($_DFF_NP0_), ID($_DFF_NP1_), ID($_DFF_NN0_), ID($_DFF_NN1_), + ID($dlatch), ID($adlatch), ID($dlatchsr), + ID($mem), ID($mem_v2), ID($meminit), ID($meminit_v2), + ID($memrd), ID($memrd_v2), ID($memwr), ID($memwr_v2), + ID($fsm), + ID($assert), ID($assume), ID($cover), ID($live), ID($fair), + ID($print), ID($check), + ID($anyconst), ID($anyseq), ID($allconst), ID($allseq), + ID($initstate)); + } + + void build_indexes() + { + for (auto c : module->cells()) { + if (is_sequential(c)) + continue; + for (auto &conn : c->connections()) { + if (!c->output(conn.first)) + continue; + for (auto bit : sigmap(conn.second)) { + if (!bit.wire) + continue; + auto it = bit_to_driver.find(bit); + if (it == bit_to_driver.end()) + bit_to_driver[bit] = c; + else if (it->second != c) + it->second = nullptr; + } + } + } + + for (auto w : module->wires()) { + if (!w->port_input) + continue; + for (auto bit : sigmap(SigSpec(w))) + if (bit.wire) + input_port_bits.insert(bit); + } + } + + // Combinational fanin cone of `from`. Leaves are port-input bits or bits + // driven by sequential cells / undriven. Returns false if size limits are + // exceeded. + bool get_cone(SigSpec from, pool &cone_cells, pool &leaf_bits, + int max_cone_cells, int max_leaf_bits) + { + pool visited; + std::queue worklist; + for (auto bit : sigmap(from)) { + if (!bit.wire) + continue; + if (visited.insert(bit).second) + worklist.push(bit); + } + + while (!worklist.empty()) { + SigBit bit = worklist.front(); + worklist.pop(); + + if (input_port_bits.count(bit)) { + leaf_bits.insert(bit); + if (GetSize(leaf_bits) > max_leaf_bits) + return false; + continue; + } + + Cell *drv = bit_to_driver.at(bit, nullptr); + if (drv == nullptr) { + leaf_bits.insert(bit); + if (GetSize(leaf_bits) > max_leaf_bits) + return false; + continue; + } + + if (!cone_cells.insert(drv).second) + continue; + if (GetSize(cone_cells) > max_cone_cells) + return false; + + for (auto &conn : drv->connections()) { + if (!drv->input(conn.first)) + continue; + for (auto in_bit : sigmap(conn.second)) { + if (!in_bit.wire) + continue; + if (visited.insert(in_bit).second) + worklist.push(in_bit); + } + } + } + + return true; + } + + // Discover the per-lane index field within candidate bus `d_sig_in`. The bus + // is viewed as `n` lanes of stride `s = width/n`; each lane must contribute + // exactly `idx_w` contiguous bits to the cone at a common within-lane offset + // (handles packed fields, where s == idx_w, and sub-fields like id[*][4:1]). + // `d_sig_in` may be a single flat input wire or a concatenation of per-lane + // split-port wires (see collect_split_input_buses). + bool infer_field(const SigSpec &d_sig_in, int n, int idx_w, int s, + const pool &leaf_bits, SigSpec &field_sig) + { + SigSpec d_sig = sigmap(d_sig_in); + dict d_offset; + for (int i = 0; i < GetSize(d_sig); i++) + if (d_sig[i].wire) + d_offset[d_sig[i]] = i; + + vector> lane_used(n); + for (auto lb : leaf_bits) { + auto it = d_offset.find(lb); + if (it == d_offset.end()) + continue; + int off = it->second; + lane_used[off / s].insert(off % s); + } + + int field_lo = -1; + for (int k = 0; k < n; k++) { + auto &used = lane_used[k]; + if (GetSize(used) != idx_w) + return false; + int lo = *used.begin(); + int expect = lo; + for (int v : used) { + if (v != expect) + return false; + expect++; + } + if (lo + idx_w > s) + return false; + if (field_lo < 0) + field_lo = lo; + else if (field_lo != lo) + return false; + } + if (field_lo < 0) + return false; + + field_sig = SigSpec(); + for (int k = 0; k < n; k++) + field_sig.append(d_sig.extract(k * s + field_lo, idx_w)); + return true; + } + + bool leaves_are_candidate_inputs(const pool &leaf_bits, const SigSpec &valid_sig, + const SigSpec &field_sig) + { + pool allowed; + for (auto bit : sigmap(valid_sig)) + if (bit.wire) + allowed.insert(bit); + for (auto bit : sigmap(field_sig)) + if (bit.wire) + allowed.insert(bit); + for (auto bit : leaf_bits) + if (!allowed.count(bit)) + return false; + return true; + } + + struct InputBus { + SigSpec sig; + std::string name; + int entries = 0; + int elem_width = 0; + }; + + // Parse a split-port name of the form "base[index]" (Verific lowers packed + // multi-dimensional ports into per-lane wires named this way). + bool parse_indexed_port_name(Wire *wire, std::string &base, int &index) + { + std::string name = wire->name.str(); + size_t rbrack = name.size(); + if (rbrack == 0 || name[rbrack - 1] != ']') + return false; + size_t lbrack = name.rfind('['); + if (lbrack == std::string::npos || lbrack + 1 >= rbrack - 1) + return false; + for (size_t i = lbrack + 1; i < rbrack - 1; i++) + if (!isdigit(name[i])) + return false; + base = name.substr(0, lbrack); + index = atoi(name.substr(lbrack + 1, rbrack - lbrack - 2).c_str()); + return true; + } + + // Group per-lane split-port wires into contiguous, equal-width buses. The + // run may start at any base index (Verific lowers both [N-1:0] -> id[0..N-1] + // and [N:1] -> id[1..N]); we only require consecutive indices and matching + // widths. The resulting sig is the ascending-index concatenation, so lane k + // is sig[k*elem_width ...] = the (base+k)-th port. + vector collect_split_input_buses(const vector &inputs) + { + std::map>> groups; + for (auto w : inputs) { + std::string base; + int index = -1; + if (parse_indexed_port_name(w, base, index)) + groups[base].push_back({index, w}); + } + + vector buses; + for (auto &it : groups) { + auto entries = it.second; + std::sort(entries.begin(), entries.end(), + [](const std::pair &a, const std::pair &b) { + return a.first < b.first; + }); + if (entries.empty()) + continue; + bool contiguous = true; + int base_index = entries.front().first; + int elem_width = GetSize(entries.front().second); + for (int i = 0; i < GetSize(entries); i++) { + if (entries[i].first != base_index + i || + GetSize(entries[i].second) != elem_width) { + contiguous = false; + break; + } + } + if (!contiguous) + continue; + + SigSpec sig; + for (auto &entry : entries) + sig.append(SigSpec(entry.second)); + buses.push_back({sig, it.first, GetSize(entries), elem_width}); + } + + return buses; + } + + bool find_anchor_driver(Wire *out_wire, Cell *&anchor) + { + for (auto bit : sigmap(SigSpec(out_wire))) { + Cell *drv = bit_to_driver.at(bit, nullptr); + if (drv != nullptr) { + anchor = drv; + return true; + } + } + return false; + } + + vector make_test_vectors(int n, int w) + { + vector vs; + auto base_field = [&](int mul, int add) { + vector f(n); + for (int k = 0; k < n; k++) + f[k] = ((k * mul + add) % w + w) % w; + return f; + }; + + // All invalid: output must be all-zero. + { + TestVector t; + t.valid.assign(n, 0); + t.field = base_field(1, 0); + vs.push_back(t); + } + + // Single valid lane: exercises every lane's field routing. + for (int k = 0; k < n; k++) { + TestVector t; + t.valid.assign(n, 0); + t.valid[k] = 1; + t.field = base_field(1, 0); + t.field[k] = k % w; + vs.push_back(t); + TestVector t2; + t2.valid = t.valid; + t2.field = base_field(3, 1); + vs.push_back(t2); + } + + // All valid: distinguishes priority direction. + { + TestVector t; + t.valid.assign(n, 1); + t.field = base_field(1, 0); + vs.push_back(t); + } + { + TestVector t; + t.valid.assign(n, 1); + t.field = base_field(-1, w - 1); + vs.push_back(t); + } + + // Prefix masks valid[k..n-1]: lowest-index winner is k (LSB-first). + for (int k = 0; k < n; k++) { + TestVector t; + t.valid.assign(n, 0); + for (int j = k; j < n; j++) + t.valid[j] = 1; + t.field = base_field(5, 2); + vs.push_back(t); + } + + // Suffix masks valid[0..k]: highest-index winner is k (MSB-first). + for (int k = 0; k < n; k++) { + TestVector t; + t.valid.assign(n, 0); + for (int j = 0; j <= k; j++) + t.valid[j] = 1; + t.field = base_field(7, 3); + vs.push_back(t); + } + + // Pairs with distinct fields: rejects OR-of-all and wrong direction. + for (int i = 0; i < n; i++) + for (int j = i + 1; j < n && j < i + 3; j++) { + TestVector t; + t.valid.assign(n, 0); + t.valid[i] = 1; + t.valid[j] = 1; + t.field = base_field(2, 0); + t.field[i] = (i + 1) % w; + t.field[j] = (j + 5) % w; + vs.push_back(t); + } + + // Pseudo-random coverage. + uint64_t lfsr = 0x1234567089abcdefULL; + for (int r = 0; r < 32; r++) { + lfsr ^= lfsr << 13; + lfsr ^= lfsr >> 7; + lfsr ^= lfsr << 17; + TestVector t; + t.valid.resize(n); + t.field.resize(n); + for (int k = 0; k < n; k++) + t.valid[k] = (lfsr >> (k % 64)) & 1; + uint64_t f = lfsr * 2654435761ULL; + for (int k = 0; k < n; k++) + t.field[k] = (int)((f >> ((k * 3) % 60)) % (uint64_t)w); + vs.push_back(t); + } + + return vs; + } + + int expected_winner(const vector &valid, int n, bool msb_first) + { + if (!msb_first) { + for (int k = 0; k < n; k++) + if (valid[k]) + return k; + } else { + for (int k = n - 1; k >= 0; k--) + if (valid[k]) + return k; + } + return -1; + } + + bool fingerprint(const Candidate &cand, bool msb_first) + { + ConstEval ce(module); + SigSpec out_sig = sigmap(SigSpec(cand.out_wire)); + SigSpec valid_sig = sigmap(cand.valid_sig); + SigSpec field_sig = sigmap(cand.field_sig); + + vector vectors = make_test_vectors(cand.n, cand.w); + for (auto &tv : vectors) { + ce.push(); + ce.set(valid_sig, pack_lanes(tv.valid, 1)); + ce.set(field_sig, pack_lanes(tv.field, cand.idx_w)); + + SigSpec out = out_sig; + SigSpec undef; + bool ok = ce.eval(out, undef); + ce.pop(); + if (!ok || !out.is_fully_const()) + return false; + + Const oc = out.as_const(); + int winner = expected_winner(tv.valid, cand.n, msb_first); + for (int p = 0; p < cand.w; p++) { + bool expect = (winner >= 0) && (p == (tv.field[winner] % cand.w)); + bool actual = (p < GetSize(oc)) && (oc[p] == State::S1); + if (expect != actual) + return false; + } + } + return true; + } + + bool check_candidate(Candidate &cand, const pool &leaf_bits) + { + if (cand.n < min_width || cand.n > max_width) + return false; + if (!is_power_of_two(cand.w) || (1 << cand.idx_w) != cand.w) + return false; + if (!leaves_are_candidate_inputs(leaf_bits, cand.valid_sig, cand.field_sig)) { + log_debug(" reject %s (valid=%s index=%s): cone leaves outside valid+field\n", + log_id(cand.out_wire), log_id(cand.valid_wire), cand.index_name.c_str()); + return false; + } + if (!find_anchor_driver(cand.out_wire, cand.anchor)) + return false; + if (fingerprint(cand, false)) { + cand.msb_first = false; + return true; + } + if (fingerprint(cand, true)) { + cand.msb_first = true; + return true; + } + log_debug(" reject %s (valid=%s index=%s): fingerprint mismatch (both directions)\n", + log_id(cand.out_wire), log_id(cand.valid_wire), cand.index_name.c_str()); + return false; + } + + struct Record { + SigBit valid; + SigSpec index; + }; + + // Priority merge of two records: the left (higher-priority) record wins + // unless it is invalid. + Record combine(Cell *anchor, const Record &lhs, const Record &rhs) + { + Cell *cell = anchor; + SigBit lhs_invalid = module->Not(NEW_ID2_SUFFIX("prionehot_ninv"), SigSpec(lhs.valid))[0]; + cells_added++; + SigBit take_rhs = module->And(NEW_ID2_SUFFIX("prionehot_take"), + SigSpec(lhs_invalid), SigSpec(rhs.valid))[0]; + cells_added++; + + Record out; + out.valid = module->Or(NEW_ID2_SUFFIX("prionehot_orv"), + SigSpec(lhs.valid), SigSpec(rhs.valid))[0]; + cells_added++; + out.index = module->Mux(NEW_ID2_SUFFIX("prionehot_mux"), lhs.index, rhs.index, + SigSpec(take_rhs)); + cells_added++; + return out; + } + + Record emit_tree_rec(Cell *anchor, const vector &leaves, int begin, int end) + { + log_assert(begin < end); + if (begin + 1 == end) + return leaves[begin]; + int mid = begin + (end - begin) / 2; + Record lhs = emit_tree_rec(anchor, leaves, begin, mid); + Record rhs = emit_tree_rec(anchor, leaves, mid, end); + return combine(anchor, lhs, rhs); + } + + // Log-depth binary decoder gated by `valid`: returns a w-bit one-hot where + // bit p is set iff valid && index == p. + SigSpec emit_decode(Cell *anchor, SigSpec index, SigBit valid, int w, int idx_w) + { + Cell *cell = anchor; + vector cur; + cur.push_back(valid); + for (int b = 0; b < idx_w; b++) { + SigSpec idx_bit(index[b]); + SigBit idx_bit_n = module->Not(NEW_ID2_SUFFIX("prionehot_ndec"), idx_bit)[0]; + cells_added++; + int group = GetSize(cur); + vector nxt(group * 2); + for (int g = 0; g < group; g++) { + nxt[g] = module->And(NEW_ID2_SUFFIX("prionehot_dec0"), + SigSpec(cur[g]), SigSpec(idx_bit_n))[0]; + cells_added++; + nxt[g + group] = module->And(NEW_ID2_SUFFIX("prionehot_dec1"), + SigSpec(cur[g]), idx_bit)[0]; + cells_added++; + } + cur = std::move(nxt); + } + + SigSpec out; + for (int p = 0; p < w; p++) + out.append(cur[p]); + return out; + } + + SigSpec emit_priority_onehot(const Candidate &cand) + { + vector leaves; + for (int k = 0; k < cand.n; k++) { + // Leftmost leaf has the highest priority. + int lane = cand.msb_first ? (cand.n - 1 - k) : k; + Record r; + r.valid = cand.valid_sig[lane]; + r.index = cand.field_sig.extract(lane * cand.idx_w, cand.idx_w); + leaves.push_back(r); + } + Record root = emit_tree_rec(cand.anchor, leaves, 0, GetSize(leaves)); + return emit_decode(cand.anchor, root.index, root.valid, cand.w, cand.idx_w); + } + + void disconnect_old_output(const Candidate &cand) + { + pool target_bits; + for (auto bit : sigmap(SigSpec(cand.out_wire))) + if (bit.wire) + target_bits.insert(bit); + + pool seen_cells; + for (auto target : target_bits) { + Cell *drv = bit_to_driver.at(target, nullptr); + if (drv == nullptr || seen_cells.count(drv)) + continue; + seen_cells.insert(drv); + + for (auto &conn : drv->connections()) { + if (!drv->output(conn.first)) + continue; + SigSpec orig = conn.second; + SigSpec replacement = orig; + bool changed = false; + Cell *cell = drv; + Wire *dangling = module->addWire(NEW_ID2_SUFFIX("prionehot_dangling"), + GetSize(orig)); + for (int i = 0; i < GetSize(orig); i++) { + if (target_bits.count(sigmap(orig[i]))) { + replacement[i] = SigBit(dangling, i); + changed = true; + } + } + if (changed) + drv->setPort(conn.first, replacement); + } + } + } + + void run() + { + if (module->has_processes_warn()) + return; + + vector inputs; + vector outputs; + for (auto w : module->wires()) { + if (w->port_input) + inputs.push_back(w); + if (w->port_output && !w->port_input) + outputs.push_back(w); + } + + // Per-lane split-port buses ("id[0]".."id[N-1]") are grouped once. + vector split_buses = collect_split_input_buses(inputs); + + vector rewrites; + pool claimed_outputs; + for (auto out : outputs) { + if (claimed_outputs.count(out)) + continue; + int w = GetSize(out); + if (w < 2 || !is_power_of_two(w)) + continue; + int idx_w = clog2_int(w); + + pool cone_cells; + pool leaf_bits; + int max_cone_cells = std::max(256, max_width * 96); + int max_leaf_bits = max_width * max_width + max_width * w + max_width; + if (!get_cone(SigSpec(out), cone_cells, leaf_bits, max_cone_cells, max_leaf_bits)) { + log_debug("output %s (w=%d): cone exceeds size limits\n", log_id(out), w); + continue; + } + if (cone_cells.empty()) + continue; + log_debug("output %s (w=%d, idx_w=%d): cone %d cells, %d leaf bits\n", + log_id(out), w, idx_w, GetSize(cone_cells), GetSize(leaf_bits)); + + bool done = false; + for (auto valid : inputs) { + if (done) + break; + int n = GetSize(valid); + if (n < min_width || n > max_width) + continue; + + // Candidate index sources: a flat input bus split into n lanes, + // or a per-lane split-port bus with n entries. + vector> sources; + for (auto d : inputs) { + if (d == valid) + continue; + if (GetSize(d) % n == 0) + sources.push_back({SigSpec(d), d->name.str()}); + } + for (auto &bus : split_buses) + if (bus.entries == n) + sources.push_back({bus.sig, bus.name}); + + for (auto &src : sources) { + int total = GetSize(src.first); + if (total % n != 0) + continue; + int s = total / n; + if (s < idx_w) + continue; + + SigSpec field_sig; + if (!infer_field(src.first, n, idx_w, s, leaf_bits, field_sig)) { + log_debug(" valid=%s index=%s (n=%d, s=%d): field layout inference failed\n", + log_id(valid), src.second.c_str(), n, s); + continue; + } + + Candidate cand; + cand.out_wire = out; + cand.valid_wire = valid; + cand.valid_sig = SigSpec(valid); + cand.field_sig = field_sig; + cand.index_name = src.second; + cand.n = n; + cand.w = w; + cand.idx_w = idx_w; + if (!check_candidate(cand, leaf_bits)) + continue; + + rewrites.push_back(cand); + claimed_outputs.insert(out); + log(" %s: %s <- priority_onehot(valid=%s, index=%s) " + "[N=%d, W=%d, IDX_W=%d, %s]\n", + log_id(module), log_id(out), log_id(valid), src.second.c_str(), + cand.n, cand.w, cand.idx_w, + cand.msb_first ? "MSB-first" : "LSB-first"); + done = true; + break; + } + } + } + + for (auto &cand : rewrites) { + cell = cand.anchor; + SigSpec new_out = emit_priority_onehot(cand); + disconnect_old_output(cand); + module->connect(SigSpec(cand.out_wire), new_out); + regions_rewritten++; + } + } +}; + +struct OptPriorityOnehotPass : public Pass { + OptPriorityOnehotPass() : Pass("opt_priority_onehot", + "rewrite priority-select + one-hot index scatter into balanced trees") {} + + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" opt_priority_onehot [options] [selection]\n"); + log("\n"); + log("This pass uses functional fingerprinting to detect combinational regions\n"); + log("that compute a priority (first-set) select of a per-lane index field and\n"); + log("scatter the winning field into a one-hot output, regardless of how the\n"); + log("RTL was written (unrolled for-loops, leading-one chains, |= scatter, etc.).\n"); + log("\n"); + log("Concretely, for a request/valid bus of N lanes and a per-lane index field,\n"); + log("the region computes:\n"); + log("\n"); + log(" winner = first lane with valid[lane] set (lowest index by default)\n"); + log(" out = (winner exists) ? (1 << field[winner]) : 0\n"); + log("\n"); + log("where out has power-of-two width W = 2^idx_w and field is idx_w bits wide.\n"); + log("Each detected region is replaced with a balanced (log-depth) priority\n"); + log("selection tree feeding a log-depth one-hot decoder, replacing the\n"); + log("linear leading-one and scatter chains in the original RTL.\n"); + log("\n"); + log("The per-lane index field may be a sub-slice of a wider flat input bus\n"); + log("(e.g. id[*][4:1] of a packed [N][5] bus); the lane stride and field\n"); + log("offset are inferred from the fanin cone. Both LSB-first (lowest index\n"); + log("wins) and MSB-first priority directions are detected.\n"); + log("\n"); + log(" -max-width N, -max_width N\n"); + log(" maximum lane count to consider (default 64).\n"); + log("\n"); + log(" -min-width N, -min_width N\n"); + log(" minimum lane count to consider (default 4).\n"); + log("\n"); + log("After rewriting, the original cone cells become unused and are removed\n"); + log("by the trailing 'clean -purge'.\n"); + log("\n"); + } + + void execute(std::vector args, RTLIL::Design *design) override + { + log_header(design, "Executing OPT_PRIORITY_ONEHOT pass (priority select + one-hot scatter).\n"); + + int max_width = 64; + int min_width = 4; + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + if ((args[argidx] == "-max-width" || args[argidx] == "-max_width") && + argidx + 1 < args.size()) { + max_width = std::stoi(args[++argidx]); + continue; + } + if ((args[argidx] == "-min-width" || args[argidx] == "-min_width") && + argidx + 1 < args.size()) { + min_width = std::stoi(args[++argidx]); + continue; + } + break; + } + extra_args(args, argidx, design); + + int total_regions = 0; + int total_cells_added = 0; + for (auto module : design->selected_modules()) { + OptPriorityOnehotWorker worker(module); + worker.max_width = max_width; + worker.min_width = min_width; + worker.run(); + total_regions += worker.regions_rewritten; + total_cells_added += worker.cells_added; + } + + log("Rewrote %d region(s); emitted %d new cell(s).\n", + total_regions, total_cells_added); + + if (total_regions) + Yosys::run_pass("clean -purge"); + } +} OptPriorityOnehotPass; + +PRIVATE_NAMESPACE_END diff --git a/tests/silimate/opt_priority_onehot.sv b/tests/silimate/opt_priority_onehot.sv new file mode 100644 index 000000000..d3f7b9221 --- /dev/null +++ b/tests/silimate/opt_priority_onehot.sv @@ -0,0 +1,235 @@ +// Test designs for opt_priority_onehot. +// +// Each "positive" module computes a lowest/highest-index priority select of a +// per-lane index field and scatters the winning field into a one-hot output, +// mirroring the qor_spi_ra_binary_tree shape. The "negative" modules look +// similar but compute a different function and must be left untouched. + +// Main shape: N=16 lanes, 5-bit id lanes, 4-bit field id[*][4:1], LSB-first. +module pri_onehot_basic ( + input wire [15:0] req, + input wire [15:0][4:0] id, + output reg [15:0] oneh +); + always_comb begin + reg [15:0] acc, sel; + acc = '0; sel = '0; oneh = '0; + for (int I = 0; I < 16; I++) begin + sel[I] = req[I] & ~(|acc); + acc[I] = req[I]; + oneh[id[I][4:1]] |= sel[I]; + end + end +endmodule + +// One-based ports [N:1] / id[I][IDX_W:1], matching the qor_spi_ra_binary_tree +// regression exactly (Verific splits id into id[1]..id[16]). +module pri_onehot_onebased ( + input wire [16:1] req, + input wire [16:1][4:0] id, + output reg [15:0] oneh +); + always_comb begin + reg [16:1] acc, sel; + acc = '0; sel = '0; oneh = '0; + for (int I = 1; I <= 16; I++) begin + sel[I] = req[I] & ~(|acc); + acc[I] = req[I]; + oneh[id[I][4:1]] |= sel[I]; + end + end +endmodule + +// Packed field: no per-lane gap (ID_W == IDX_W == 4), field id[*][3:0]. +module pri_onehot_packed ( + input wire [15:0] req, + input wire [15:0][3:0] id, + output reg [15:0] oneh +); + always_comb begin + reg [15:0] acc, sel; + acc = '0; sel = '0; oneh = '0; + for (int I = 0; I < 16; I++) begin + sel[I] = req[I] & ~(|acc); + acc[I] = req[I]; + oneh[id[I][3:0]] |= sel[I]; + end + end +endmodule + +// Scaled down: N=8, 4-bit id lanes, 3-bit field id[*][3:1], W=8. +module pri_onehot_w8 ( + input wire [7:0] req, + input wire [7:0][3:0] id, + output reg [7:0] oneh +); + always_comb begin + reg [7:0] acc, sel; + acc = '0; sel = '0; oneh = '0; + for (int I = 0; I < 8; I++) begin + sel[I] = req[I] & ~(|acc); + acc[I] = req[I]; + oneh[id[I][3:1]] |= sel[I]; + end + end +endmodule + +// Scaled up: N=32, 6-bit id lanes, 5-bit field id[*][5:1], W=32. +module pri_onehot_w32 ( + input wire [31:0] req, + input wire [31:0][5:0] id, + output reg [31:0] oneh +); + always_comb begin + reg [31:0] acc, sel; + acc = '0; sel = '0; oneh = '0; + for (int I = 0; I < 32; I++) begin + sel[I] = req[I] & ~(|acc); + acc[I] = req[I]; + oneh[id[I][5:1]] |= sel[I]; + end + end +endmodule + +// Lane count != output width: N=8 lanes, 4-bit field, W=16. +module pri_onehot_n8_w16 ( + input wire [7:0] req, + input wire [7:0][4:0] id, + output reg [15:0] oneh +); + always_comb begin + reg [7:0] acc, sel; + acc = '0; sel = '0; oneh = '0; + for (int I = 0; I < 8; I++) begin + sel[I] = req[I] & ~(|acc); + acc[I] = req[I]; + oneh[id[I][4:1]] |= sel[I]; + end + end +endmodule + +// MSB-first priority: highest set index wins (W=8 to keep SAT cheap). +module pri_onehot_msb ( + input wire [7:0] req, + input wire [7:0][3:0] id, + output reg [7:0] oneh +); + always_comb begin + reg [7:0] acc, sel; + acc = '0; sel = '0; oneh = '0; + for (int I = 7; I >= 0; I--) begin + sel[I] = req[I] & ~(|acc); + acc[I] = req[I]; + oneh[id[I][3:1]] |= sel[I]; + end + end +endmodule + +// Two independent priority-onehot regions in one module. +module pri_onehot_two_regions ( + input wire [7:0] req_a, + input wire [7:0][3:0] id_a, + input wire [7:0] req_b, + input wire [7:0][3:0] id_b, + output reg [7:0] oneh_a, + output reg [7:0] oneh_b +); + always_comb begin + reg [7:0] acc, sel; + acc = '0; sel = '0; oneh_a = '0; + for (int I = 0; I < 8; I++) begin + sel[I] = req_a[I] & ~(|acc); + acc[I] = req_a[I]; + oneh_a[id_a[I][3:1]] |= sel[I]; + end + end + always_comb begin + reg [7:0] acc2, sel2; + acc2 = '0; sel2 = '0; oneh_b = '0; + for (int I = 0; I < 8; I++) begin + sel2[I] = req_b[I] & ~(|acc2); + acc2[I] = req_b[I]; + oneh_b[id_b[I][3:1]] |= sel2[I]; + end + end +endmodule + +// One-hot output also consumed by a downstream parity output. +module pri_onehot_shared_consumer ( + input wire [7:0] req, + input wire [7:0][3:0] id, + output reg [7:0] oneh, + output wire par +); + always_comb begin + reg [7:0] acc, sel; + acc = '0; sel = '0; oneh = '0; + for (int I = 0; I < 8; I++) begin + sel[I] = req[I] & ~(|acc); + acc[I] = req[I]; + oneh[id[I][3:1]] |= sel[I]; + end + end + assign par = ^oneh; +endmodule + +// --------------------------------------------------------------------------- +// Negative / near-miss modules: must NOT be rewritten. +// --------------------------------------------------------------------------- + +// No priority: OR of all decoded fields (output is generally not one-hot). +module pri_onehot_orall ( + input wire [15:0] req, + input wire [15:0][4:0] id, + output reg [15:0] oneh +); + always_comb begin + oneh = '0; + for (int I = 0; I < 16; I++) + oneh[id[I][4:1]] |= req[I]; + end +endmodule + +// Nonzero default when no request: function is not "0 when all-invalid". +module pri_onehot_nonzero_default ( + input wire [15:0] req, + input wire [15:0][4:0] id, + output reg [15:0] oneh +); + always_comb begin + reg [15:0] acc, sel; + acc = '0; sel = '0; oneh = '1; + for (int I = 0; I < 16; I++) begin + sel[I] = req[I] & ~(|acc); + acc[I] = req[I]; + oneh[id[I][4:1]] |= sel[I]; + end + end +endmodule + +// Non-power-of-two output width. +module pri_onehot_nonpow2 ( + input wire [11:0] req, + input wire [11:0][3:0] id, + output reg [11:0] oneh +); + always_comb begin + reg [11:0] acc, sel; + acc = '0; sel = '0; oneh = '0; + for (int I = 0; I < 12; I++) begin + sel[I] = req[I] & ~(|acc); + acc[I] = req[I]; + oneh[id[I][3:1]] |= sel[I]; + end + end +endmodule + +// Unrelated mux logic. +module pri_onehot_unrelated ( + input wire [15:0] a, + input wire [15:0] b, + input wire s, + output wire [15:0] y +); + assign y = s ? a : b; +endmodule diff --git a/tests/silimate/opt_priority_onehot.ys b/tests/silimate/opt_priority_onehot.ys new file mode 100644 index 000000000..a2e0726c2 --- /dev/null +++ b/tests/silimate/opt_priority_onehot.ys @@ -0,0 +1,301 @@ +# Tests for opt_priority_onehot. + +# Helper pattern per positive module: import a gold copy, import a gate copy, +# rewrite the gate, assert the rewrite fired, then prove gold == gate by SAT. + +log -header "Basic priority-onehot self-equivalence (N=16, field id[*][4:1])" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_basic +proc; opt_clean +rename pri_onehot_basic gold + +read -sv opt_priority_onehot.sv +verific -import pri_onehot_basic +proc; opt_clean +select -module pri_onehot_basic +opt_priority_onehot +select -clear +opt_clean +select -assert-min 1 w:*prionehot* +rename pri_onehot_basic gate + +miter -equiv -flatten -make_assert gold gate miter +hierarchy -top miter +proc; opt; memory; opt +sat -prove-asserts -verify +design -reset +log -pop + +log -header "One-based [N:1] ports self-equivalence (regression shape)" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_onebased +proc; opt_clean +rename pri_onehot_onebased gold + +read -sv opt_priority_onehot.sv +verific -import pri_onehot_onebased +proc; opt_clean +select -module pri_onehot_onebased +opt_priority_onehot +select -clear +opt_clean +select -assert-min 1 w:*prionehot* +rename pri_onehot_onebased gate + +miter -equiv -flatten -make_assert gold gate miter +hierarchy -top miter +proc; opt; memory; opt +sat -prove-asserts -verify +design -reset +log -pop + +log -header "Packed field self-equivalence (ID_W == IDX_W, no gap)" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_packed +proc; opt_clean +rename pri_onehot_packed gold + +read -sv opt_priority_onehot.sv +verific -import pri_onehot_packed +proc; opt_clean +select -module pri_onehot_packed +opt_priority_onehot +select -clear +opt_clean +select -assert-min 1 w:*prionehot* +rename pri_onehot_packed gate + +miter -equiv -flatten -make_assert gold gate miter +hierarchy -top miter +proc; opt; memory; opt +sat -prove-asserts -verify +design -reset +log -pop + +log -header "Scaled N=8 self-equivalence" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_w8 +proc; opt_clean +rename pri_onehot_w8 gold + +read -sv opt_priority_onehot.sv +verific -import pri_onehot_w8 +proc; opt_clean +select -module pri_onehot_w8 +opt_priority_onehot +select -clear +opt_clean +select -assert-min 1 w:*prionehot* +rename pri_onehot_w8 gate + +miter -equiv -flatten -make_assert gold gate miter +hierarchy -top miter +proc; opt; memory; opt +sat -prove-asserts -verify +design -reset +log -pop + +log -header "Lane count != output width self-equivalence (N=8, W=16)" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_n8_w16 +proc; opt_clean +rename pri_onehot_n8_w16 gold + +read -sv opt_priority_onehot.sv +verific -import pri_onehot_n8_w16 +proc; opt_clean +select -module pri_onehot_n8_w16 +opt_priority_onehot +select -clear +opt_clean +select -assert-min 1 w:*prionehot* +rename pri_onehot_n8_w16 gate + +miter -equiv -flatten -make_assert gold gate miter +hierarchy -top miter +proc; opt; memory; opt +sat -prove-asserts -verify +design -reset +log -pop + +log -header "MSB-first priority self-equivalence" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_msb +proc; opt_clean +rename pri_onehot_msb gold + +read -sv opt_priority_onehot.sv +verific -import pri_onehot_msb +proc; opt_clean +select -module pri_onehot_msb +opt_priority_onehot +select -clear +opt_clean +select -assert-min 1 w:*prionehot* +rename pri_onehot_msb gate + +miter -equiv -flatten -make_assert gold gate miter +hierarchy -top miter +proc; opt; memory; opt +sat -prove-asserts -verify +design -reset +log -pop + +log -header "Two independent regions self-equivalence" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_two_regions +proc; opt_clean +rename pri_onehot_two_regions gold + +read -sv opt_priority_onehot.sv +verific -import pri_onehot_two_regions +proc; opt_clean +select -module pri_onehot_two_regions +opt_priority_onehot +select -clear +opt_clean +select -assert-min 2 w:*prionehot* +rename pri_onehot_two_regions gate + +miter -equiv -flatten -make_assert gold gate miter +hierarchy -top miter +proc; opt; memory; opt +sat -prove-asserts -verify +design -reset +log -pop + +log -header "Shared consumer of one-hot output stays equivalent" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_shared_consumer +proc; opt_clean +rename pri_onehot_shared_consumer gold + +read -sv opt_priority_onehot.sv +verific -import pri_onehot_shared_consumer +proc; opt_clean +select -module pri_onehot_shared_consumer +opt_priority_onehot +select -clear +opt_clean +select -assert-min 1 w:*prionehot* +rename pri_onehot_shared_consumer gate + +miter -equiv -flatten -make_assert gold gate miter +hierarchy -top miter +proc; opt; memory; opt +sat -prove-asserts -verify +design -reset +log -pop + +log -header "Scaled N=32 structural rewrite" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_w32 +proc; opt_clean +opt_priority_onehot +opt_clean +select -assert-min 1 w:*prionehot* +design -reset +log -pop + +log -header "Negative: OR-of-all (no priority) unchanged" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_orall +proc; opt_clean +opt_priority_onehot +select -assert-none w:*prionehot* +design -reset +log -pop + +log -header "Negative: nonzero all-invalid default unchanged" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_nonzero_default +proc; opt_clean +opt_priority_onehot +select -assert-none w:*prionehot* +design -reset +log -pop + +log -header "Negative: non-power-of-two output width unchanged" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_nonpow2 +proc; opt_clean +opt_priority_onehot +select -assert-none w:*prionehot* +design -reset +log -pop + +log -header "Negative: unrelated mux logic unchanged" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_unrelated +proc; opt_clean +select -assert-count 1 t:$mux +opt_priority_onehot +select -assert-none w:*prionehot* +select -assert-count 1 t:$mux +design -reset +log -pop + +log -header "Max-width below lane count leaves design unchanged" +log -push +design -reset +verific -cfg veri_optimize_wide_selector 1 +verific -cfg db_infer_wide_muxes_post_elaboration 0 +read -sv opt_priority_onehot.sv +verific -import pri_onehot_basic +proc; opt_clean +opt_priority_onehot -max_width 8 +select -assert-none w:*prionehot* +design -reset +log -pop