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

[bugzilla-daemon at libre-soc.org]

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

--- 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
big-endian?

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