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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #46 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(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.

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