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

[bugzilla-daemon@libre-soc.org]

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

--- Comment #47 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #46)
> (In reply to Cole Poirier from comment #44)
> 
> >   71         #   1. RA[8:64] should always equal 0
> >   72         #   2. If RB[i*8:i*8+8] >= 64 then RA[i] should equal 0
> >   73         #   3. If RB[i*8:i*8+8] < 64 then RA[i] should RS[index]
> > 
> > For 2 and 3 should RB[i*8:i*8+8] actually be RS[i*8:i*8+8]?
> 
> yes.
> 
> > Or am I failing
> > to properly read/interpret the 'formalism'? In other words, I'm very
> > confused and looking for a way to better understand what I am doing, and
> > what I am supposed to be doing.
> 
> you are expressing the expectations about the inputs and outputs of
> the module.
> 
> these you express as assertions that must be true.
> 
> (sby then checks those for you under *all* possible values of input and
> output).
> 
> therefore you not only need to get the code right, you actually need to
> properly understand what it does... and express that in the assertions.
> 
> example.
> 
> from this line of code, is it *ever* possible that bits 8 and above
> will be *anything* other than zero?
> 
>         m.d.comb += self.ra[0:8].eq(perm)
> 
> answer: no it is not.
> 
> *therefore make an assertion about that*:
> 
>         comb += Assert(self.ra[8:] == 0)
> 
> now let us move on to when any given "index" (in rs, not rb) is
> greater than 64.
> 
> is it *ever* possible that perm[i] - which remember is the same
> as ra[i] - that when "index" is >= 64, that perm[i]
> (aka ra[i]) will be anything other than zero?
> 
>             with m.If(idx < 64):
>                 m.d.comb += perm[i].eq(rb64[idx])
> 
> answer: no, it cannot, because when index >= 64, perm[i] is never
> set, and therefore will *always* be zero.
> 
> *therefore make an assertion about that*:
> 
>              with m.If(index >= 64):
>                  comb += Assert(ra[i] == 0)
> 
> and that just leaves the last one, which is annoyingly a little more
> complicated, and best done probably by setting up that array rb64 again,
> which will allow you to get at rb[index]
> 
> i "cheated" by doing a ridiculously-CPU-intensive cycling through
> j=0..64 looking for a match against j == index.

Thank Luke, this is tremendously helpful. I think Michael explained it well,
but I was having a hard time fully comprehending because I'm still learning how
to read and write the 'language' of the cpu/rtl/circuit domain. Going to
re-read this a few times, then review nmigen tutorial by Robert Baruch, Claire
Wolf's 'Yosys  Application Note 011: Interactive Design Investigation', so I
can better understand those 'languages'.

Tomorrow should I move on to trying to understand Wolf's verilog code for the
rvb equivalent of this operation? With regard to copyright, what should I do?
Am I supposed to write to her to ask for permission to use her code? Is that
even a possibility? I don't know how to proceed, what do you advise?

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