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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Wed May 20 23:18:49 BST 2020


--- Comment #76 from Cole Poirier <colepoirier at 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.

More information about the libre-riscv-dev mailing list