[Libre-soc-bugs] [Bug 418] SPR pipeline formal correctness proof needed

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Sat Jul 11 10:43:56 BST 2020


--- Comment #2 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
so the purpose of the SPR pipeline is dead simple: there are only two
instructions.  they copy SPRs (special purpose registers) to / from
GPRs (general purpose registers).

that's it.  end of story.

the minor complication is that as you can see from main_stage.py the
SPRs are *not* in "one single register file", they're spread out across
*three* separate register files:

* XER   (implemented)
* FAST  (implemented)

when we add SLOW SPRs, a re-mapping will need to be used (see PowerDecoder2
SPRMap) which transforms the 10-bit PowerISA numbering scheme into a binary
index into the SPR SRAM (which has only 70 or so entries, not 1024).

so yes: a very dumb, very straightforward, very obvious and well-documented
formal proof is needed.  combinatorial.  nothing fancy at all.

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

More information about the libre-soc-bugs mailing list