Function simt_sliced_pp_to_bounded 

pub fn simt_sliced_pp_to_bounded(select_slice: usize, width: u32) -> BoundedExpr

The BoundedExpr of ONE emitted sliced partial product pp — the fan-out-bounded image of the single-select mux mp[0] ? mc : 0. It models the emitted Verilog exactly: pp = { {G{s}} & mc[hi:lo] , ... } over select_slice groups of G = width / select_slice bits, where every msel copy equals the ONE select bit s = mp0. Group g occupies bits [g*G .. g*G+G-1], and its value is s==1 ? mc[hi:lo] : 0 (a G-wide select). Building pp from these per-group selects and proving pp == (s==1 ? mc : 0) CERTIFIES the byte-slicing drops or misaligns no bit — closing the gap where the slice was previously only iverilog-checked.

s = BitVecVar("mp0", 1), mc = BitVecVar("mc", width). width % select_slice must be 0 (the same tiling invariant the emitter asserts). Groups are concatenated high-to-low so group 0 lands at the LSB, matching { group[N-1], ..., group[1], group[0] }.