[libre-riscv-dev] [Bug 316] bperm TODO

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Tue May 19 20:30:51 BST 2020


--- Comment #51 from Cole Poirier <colepoirier at gmail.com> ---
(In reply to Michael Nolan from comment #50)
> I'm not sure I would. To me, a proof should be as simple as possible to
> understand, because you need to be able to check the proof against the
> specification. The existing proof is clear enough to allow it to be checked
> against the pseudocode, and doesn't take an inordinate amount of time, so I
> think it's fine to leave it as is.

Makes sense to me!

> So yeah, I'd say try hooking it up to main_stage and adding a test for it
> would be better than trying to "optimize" the proof. Especially since
> there's a bug in the module that the proof hasn't revealed (hint: it has to
> do with power's numbering of bits).

Is this the big-endian comment you left in the pseudo-code? Is that documented
in the spec? Looking at POWERISA v3.1 doesn't look like it notes this, unless
there is some esoteric notation that denotes this? Or POWERISA is just always

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

More information about the libre-riscv-dev mailing list