[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 #8 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
i started writing it out (to do the same thing as MSR51) and this:

    MSR[3] <- (MSR[3] & SRR1[3]) | ((¬MSR[3] & MSR[3]))

basically that last part is zero and *reduces* to

    MSR[3] <- (MSR[3] & SRR1[3])

so yes the spec is correct.

therefore, samuel, i suggest ignoring main_stage.py entirely
and converting that pseudo-code into Asserts.  nothing fancy,
no functions called, no use of is_ok, no use of full_function_bits.

just straight line-for-line direct translation.

that way, anyone looking at the pseudo-code and the proof side-by-side
can go "ths line is correct, this line is correct, this line is correct"
and we stand a chance of getting it right.

as you know, the point of the proofs is to have clarity, not speed.

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