[Libre-soc-bugs] [Bug 904] Formal proof for pop-count

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=904

--- Comment #7 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Jacob Lifshay from comment #6)
> after reading through the Popcount class some more, I'm realizing that it is
> incredibly PowerISA-specific, since it specifically operates on the packed
> simd types u8x8, u32x2, or u64x1 (no u16x4), rather than what most pop-count
> functions do: pop-count only 1 thing.

hmm hmm yeah i really liked how that python code absorbed the first
level. ah well.  needs converting at some point to use nmutil popcount
but not now.

> The more-general pop_count function I added to nmutil also has a formal
> correctness proof in nmutil, therefore I think this task is complete.

makes perfect sense.  i moved pop_count() to popcount.py so that anyone
looking at the top-level directory listing will go "oh, there's a popcount.py"
otherwise the function pop_count() is buried in a file that people will
not at first glance realise is related.

-- 
You are receiving this mail because:
You are on the CC list for the bug.