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

[bugzilla-daemon@libre-soc.org]

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

--- Comment #75 from Michael Nolan <mtnolan2640@gmail.com> ---
(In reply to Cole Poirier from comment #74)
> Test passes, and code has been commit-pushed. Moving on to your suggestion
> on today's kanban update of integrating the formal proof of bpermd:
> 
Cool. I've modified test_bpermd a bit so it exercises the module a bit better.
Previously, you only had it do one iteration with two constants, and those
constants made bpermd evaluate to 0. This isn't *really* sufficient to
establish much confidence in the module, so I modified it to do ~20 iterations
of something that would evaluate to something other than 0. 




> How should I go about integrating the formal proof of bpermd into the
> logical pipeline? I've thought about it, and I am unsure as to how to
> proceed. Is there a model I can follow as before?
> 
> I also want to follow up on a comment of Michael's from yesterday:
> 
> ```
> From comment #50 of this bug
> 
> Michael Nolan 2020-05-19 20:24:19 BST
> 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 my proof of bpermd in fact not a proper proof, and incorrect because it's
> making an mistake with endian-ness?

Well kinda. Your proof is written to match the Power ISA spec, and from a
glance it looks like it does that. However, Power bit indices go from left to
right, which is opposite what python and nmigen do. So although your proof
looks like it matches the spec, it doesn't give correct results when it's
actually tested. That's why I suggested you hook it up to the testbench ,
because the testbench compares it to some python pseudocode that *does* index
bits correctly. 

So what I think you should do now is pull and run the testbench again, and see
if you can't figure out how to get it to pass those tests. Then modify the
proof correspondingly.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev