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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Tue May 19 00:34:17 BST 2020

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

--- Comment #44 from Cole Poirier <colepoirier at gmail.com> ---
(In reply to Michael Nolan from comment #43)
> (In reply to Cole Poirier from comment #42)
> For a combinatorial circuit like this one, the inputs (rs and rb) are set to
> their initial values, and the outputs (ra) are set to whatever the circuit
> calculates from the inputs.

Thank you for this clarification, I think I am missing some of the basic
background knowledge of registers/assembly, should I just do some background
reading on wikipedia, or is there a better resource you or luke can point me
to, or should I simply study OPF ISA Spec v3.1?

> In the proof, you're generating the index from rb, but in the actual module
> and the Power spec, it's generated from rs. That's why the proof fails. If
> you look at the index variables (for me it's index 6), you'll notice that
> one is less than 64 - that's how I figured it out.

That makes sense. I didn't catch this because all other idx_n's were 00, and
idx_6 was 37. 37 is less than 64, but is 00 not also less than 64 correct? I'm

I'd like to clarify one other thing so I don't repeat this same mistake.
In the skeleton you provided the below pseudo code and assertion properties.

# The pseudocode in the Power ISA manual (v3.1) is as follows:
61         # do i = 0 to 7
62         #    index <- RS[8*i:8*i+8]
63         #    if index < 64:
64         #        perm[i] <- RB[index]
65         #    else:
66         #        perm[i] <- 0
67         # RA <- 56'b0 || perm[0:8]  # big endian though
68
69         # Looking at this, I can identify 3 properties that the bperm
70         # module should keep:
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]? 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 receiving this mail because:
You are on the CC list for the bug.
```