On Tue, Aug 26, 2025 at 7:33 AM Daniel Borkmann <daniel@xxxxxxxxxxxxx> wrote: > > On 8/26/25 5:45 AM, Nandakumar Edamana wrote: > > Drop the value-mask decomposition technique and adopt straightforward > > long-multiplication with a twist: when LSB(a) is uncertain, find the > > two partial products (for LSB(a) = known 0 and LSB(a) = known 1) and > > take a union. > > > > Experiment shows that applying this technique in long multiplication > > improves the precision in a significant number of cases (at the cost > > of losing precision in a relatively lower number of cases). > > > > Signed-off-by: Nandakumar Edamana <nandakumar@xxxxxxxxxxxxxxxx> > > Acked-by: Eduard Zingerman <eddyz87@xxxxxxxxx> > > Reviewed-by: Harishankar Vishwanathan <harishankar.vishwanathan@xxxxxxxxx> > > Hari, are you okay if we also add a ... > > Tested-by: Harishankar Vishwanathan <harishankar.vishwanathan@xxxxxxxxx> # Agni > > ... to indicate in the commit log that you also ran the code through Agni? > > Thanks, > Daniel Yes sure Daniel, I'm okay with adding the Tested-by. Just to clarify: since tnum_mul has a loop, I didn't run this directly through Agni, as Agni doesn't yet support loops. I tested this in Z3 via a manual conversion to logic by unrolling the loop for a limited bound. Best, Hari
