[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 #5 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Samuel A. Falvo II from comment #3)
> There is so much meta-programming happening, I cannot navigate the interface
> of the SPR main stage module. 

the code is designed to set up a massive parallel batch of pipelines.
not "1 lovely pipeline, oo look, innit pretty".

consequently, data paths branch out massively.  to avoid huge code-duplication,
the use of OO is just... necessary.

you will find a file soc/fu/README.md which explains the structure:
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/README.md;hb=HEAD

for example: spr_input_subset.py contains *ONLY* the subset of PowerISA
field information *SPECIFICALLY* relevant to this particular pipeline.

spr/pipe_data.py *ONLY* contains the input and output format of register
data coming into and out of this particular pipeline.

> Is there some place I can go to read up on
> how interfaces are constructed and what their signal meanings are?  E.g.,
> what is the difference between spr1 and fast1?

the docstring at the top of fu/spr/pipe_data.py is worth reading.  it
explains that there are multiple register files.  you've discovered
the regfiles wiki page and that should link you back to regfiles.py

>  Where does the op field come from?

self.i.ctx.op is established by the pipeline code.  it contains
the "operation" - an instance of the Operation Class - in this
case that's CompOpSPRSubset, which you'll find in fu/spr/spr_input_record.py

basically, this is however all context.  the key things to know are:

* the pipelines *do not* themselves read or write to register files.
  they do not even actually know which register port nor which actual
  register they are writing to or reading from.

  all they need to know is: that has *already been taken care of*, and
  they need only, specifically and exclusively to think in terms of InputData
  and OutputData, as defined by "regspecs".

* therefore in this case. all that you need to know is:

  - self.i.ra/fast1/spr1/xer_so/ca/ov is incoming data
  - self.o.o/fast1/spr1/etc is outgoing data

* these are listed in the "convenience variables" in main_stage.py
  and you will see that exact same pattern both in other main_stage.py
  files *and in their corresponding proofs*

  see comment #1 for a link to e.g. the ALU formal proof

* in this particular pipeline, some of the SPRs (and other data) need
  to be accessed much more regularly than others.  these are labelled
  "Fast" Regs.

  these are in an *unary* addressed regfile with *six* read ports and
  five write ports (6R5W).

  all other SPRs are considered "slow" and are in a 2R1W binary-addressed
  regfile.

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