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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #28 from Cole Poirier <colepoirier at gmail.com> ---
(In reply to Michael Nolan from comment #26)
> (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.

Thank you! Thank you! Thank you! This is honestly unbelievable Michael, I am so
grateful for your very generous help. I'm going over the proof skeleton now,
about to start working on the second proof assertion that you've given me a
very good starting point for. I'll be sure to let you know once I have
something... or if I have a significant problem.

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