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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #21 from Cole Poirier <colepoirier at gmail.com> ---
(In reply to Michael Nolan from comment #19)
> (In reply to Cole Poirier from comment #16)
> > 
> > I have committed the changes. Now I am going to go over Robert Baruch's
> > nmigen tutorials and search out resources on writing unit tests, and formal
> > proofs for hardware. Then I will attempt to write an appropriate unit test
> > for this class.
> 
> For writing unit tests, take a look at
> https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/shift_rot/test/
> test_maskgen.py;h=1a4d34e676154b250f95ef120932a9b88fcaf937;
> hb=3c65f5ff7893bb34696c476abacfe34ad739bf18 for decent starting place

Thanks Michael! This looks like it will be really helpful.

(In reply to Michael Nolan from comment #18)
> (In reply to Luke Kenneth Casson Leighton from comment #17)
> > (In reply to Cole Poirier from comment #16)
> 
> > 
> > btw notice in cr/main_stage.py, michael also does the same "indexing" trick
> > :)
> > in particular notice what he does with the name argument:
> > 
> >    cr_out_arr = Array([Signal(name=f"cr_out_{i}") for i in range(32)])
> > 
> > if you try that out you will end up with actual properly-named Signals rather
> > than "stuff that's randomly named $1, $2, $3.... $64".
> 
> ROFL, I got the idea of using Arrays from your conversations yesterday.

I just pushed I commit where I have tried to copy this, although I'm unsure if
I did it correctly, because rb_{n} shows up correctly in the graph, but I see
no idx_{n}'s. I took a second look at my code after using yosys to examine it,
and I'm not able to discern why idx would not show up... I just took a third
look and realized it was because I had neglected to delete my temporary
assignment of an 8-bit wide Signal from my first iteration to the variable
index, which I was actually using within the body of the for loop that makes up
the bulk of the function. Now both labels show up correctly. I have pushed this
new commit.

> > great.  formal proofs are... odd.  i can barely get my head round them.

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.

(In reply to Luke Kenneth Casson Leighton from comment #17)
> (In reply to Cole Poirier from comment #16)
> 
> > I have committed the changes.
> 
> fantastic: feel free to do another "git pull" because i just made some
> PEP8-like
> changes.

Thanks Luke, and apologies for not perfectly conforming to PEP8 yet, I'm
working on getting my autopep8 working but have run into a problem, I should
have it sorted tomorrow.

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