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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Sun May 17 18:19:31 BST 2020


--- Comment #26 from Michael Nolan <mtnolan2640 at gmail.com> ---
(In reply to Cole Poirier from comment #21)
> Yeah.. I have the feeling that I'm wading into quite strange waters here :)
> > I'd be happy to help with formal proofs when you're ready.
> Thanks again Michael, I'm looking forward to working with you and learning
> from your knowledge and experience. I have a prior obligation, so I'll have
> to push writing the unit test until tomorrow. But, for my own understanding,
> once I have the unit test is working, would it be wiser to search for
> optimization opportunities, for example from Claire Wolf's bitmanip code, or
> to write the formal proof? I'm guessing that the formal proof is specific to
> the function's implementation and thus I should wait to write the formal
> proof until the function is optimized but I am not sure.

Cole, I added a skeleton proof module for bperm.py here
with a bunch of comments on how to finish the formal proof. Take a look when
you get around to it, and let me know if you have problems.

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

More information about the libre-riscv-dev mailing list