[Libre-soc-bugs] [Bug 421] TRAP pipeline formal correctness proof needed

[bugzilla-daemon at libre-soc.org]

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

--- Comment #33 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
gaah, that was a handful :)

first, i had to put in a series of individual Asserts rather than
assign to expected_msr then check it in one go.  this allowed me
to tell which *part* of the MSR field was wrong, and i confirmed
that yes it was something to do with bit 30.

after doing that i found that um actually there wasn't a "problem",
until i added the "else" clause:

                    with m.Else():
                        comb += Assert(F(msr_od, 29, 31) == F(msr_i, 29, 31))

*then* it failed, and at that point i went "oink" and found that this
was *missing* from trap main_stage.py

                    # put *back* bits 29-31 (MSB0 notation)
                    bits = field_slice(29, 31)
                    with m.If((msr_i[bits] == Const(0b010, 3)) &
                               (a_i[bits] == Const(0b000, 3))):
                         comb += msr_o.data[bits].eq(msr_i[bits])

and that was the source of the problem.

hurrah for formal correctness proofs!

oh - OP_RFID pseudo-code, which i reviewed at the same time, turned out to be
an accidental amalgamation of V3.1B and v3.0B spec (MSR.S - bit 41 - is not
examined in v3.0B, where it is for v3.0B)

all in all a good outcome.  i think we can close this one soon.


commit 944dc6b7129d06a936643863bfb572a5ba70b19f (HEAD -> master)
Author: Luke Kenneth Casson Leighton <lkcl at lkcl.net>
Date:   Mon Jul 27 12:44:44 2020 +0100

    fix trap proof, and trap main_stage, and pseudocode for rfid
    all a bit of a mess, really :)

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