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

[bugzilla-daemon at libre-soc.org]

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

--- 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
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/logical/formal/proof_bperm.py;h=da198940f75b3868ca864f1d75c6e99c55b1f073;hb=HEAD
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.