[Libre-soc-bugs] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon at libre-soc.org]

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

--- Comment #12 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Samuel A. Falvo II from comment #11)

> Can you explain the bug?  I see a link to line 50 of the main_stage.py file,
> but without more context, I don't know what I'm looking to fix in the proof.
> Thanks.

ah sorry i should have recorded the diff-commit rather than a link to the line.
the "L" field was previously being completely ignored.

so where for example the pseudocode says this:

* cmp BF,L,RA,RB

    if L = 0 then
        a <-  EXTS((RA)[32:63] )
        b <- EXTS((RB)[32:63])
    else
        a <- (RA)
        b <- (RB)


we were in fact simply doing this:


* cmp BF,L,RA,RB

    a <- (RA)
    b <- (RB)


because this was in the proof *and* the HDL and there was no corresponding unit
test to catch it, the bug went unnoticed for several months.

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