[Libre-soc-bugs] [Bug 340] formal proof of POWER9 SHIFTROT pipeline needed

[bugzilla-daemon at libre-soc.org]

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

--- Comment #11 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
*click*.

no, you might be right.... no wait... nope :)

ok it's confusing.

* immediates come in on the imm_data part of the input record
* however it is the *CompUnit* that notices if imm_data.ok is set
* the *CompUnit* redirects imm_data into RB if imm_data.ok is set

therefore yes, by the time the pipeline receives anything, there
*are* no "immediates", and there's definitely no change of behaviour
based on whether it's a rlxxxxi

i'm going to expand out the for-loop here because the debug
reports from the formal proof are masked. every port there
is given the same line number from the source file, with no
"name"

38:        for p in rec.ports():
39:            comb += p.eq(AnyConst(p.width))

Value for anyconst in top (fu/shift_rot/formal/proof_main_stage.py:39): 1
Value for anyconst in top (fu/shift_rot/formal/proof_main_stage.py:39): 56
Value for anyconst in top (fu/shift_rot/formal/proof_main_stage.py:39): 1064

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