[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 #8 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #5)

> * 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.

and (forgot to mention) there are 5 (6 but one is ignored) bits from
the XER SPR which are accessed so frequently (carry, overflow, sticky)
that if we did not have a separate dedicated register file for them,
where each register is only 2 bits (!) then the pipelines would be
completely incapable of any reasonable level of parallelism / overlap.

this means however that in this *particular* pipeline, which implements
"transfer arbitrary SPR to register" and "transfer register to arbitrary
SPR", when that SPR is "XER" it becomes necessary to *construct* the
response - not from a Fast Reg - not from a slow SPR reg - but from
the *XER Regfile*.

microwatt does exactly the same thing.

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