[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 #20 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
commit 6530c0ccadadf834dc66e95941ae27c01de52da4 (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl at lkcl.net>
Date:   Tue Jul 21 10:50:37 2020 +0100

    corrections to trap proof see
    https://bugs.libre-soc.org/show_bug.cgi?id=421#c17 and
    https://bugs.libre-soc.org/show_bug.cgi?id=421#c18

commit 2595e209a67e8721436bbb4caeadf2ae0e9d90b1
Author: Luke Kenneth Casson Leighton <lkcl at lkcl.net>
Date:   Tue Jul 21 10:45:33 2020 +0100

    use alias for msr_i in trap proof

commit 0949e113f0979adb56e1e8af4106d39bfd56b55f
Author: Luke Kenneth Casson Leighton <lkcl at lkcl.net>
Date:   Tue Jul 21 10:41:36 2020 +0100

    correct trap spec page interrupt ref

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