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

[bugzilla-daemon at libre-soc.org]

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
confused by this so your clarification would be very helpful.

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.