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

[bugzilla-daemon at libre-soc.org]

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

--- 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)
* SLOW  (TODO)

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.