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

[bugzilla-daemon@libre-soc.org]

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

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

Thanks Michael, your help is yet again very helpful :) Unfortunately I won't be
able to do this until tomorrow morning because an exterminator appointment is
forcing me to be away from my computer. Looking forward to tackling this.

-- 
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