The 7th RISC-V Workshop has rejected my talk on riscv-formal. (They "accepted it as a poster".)
Show this thread
-
You’re saying there is a bug in the spec they are verifying against?
Yes. But they aren't verifying their spec against anything (yet). Their primary focus is on proofing abstract properties of the ISA..
-
-
And that is also very important of course, but I think the first step should be proving that the spec actually matches the implementation.
-
Also, their spec doesn't handle things like illegal instructions yet. It triggers a "fromJust Nothing" that terminates their Haskell app.
End of conversation
New conversation -
-
-
One reason I publish papers about improving ISA spec quality is to try to raise the bar. Must try harder.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Update on
I have now exchanged the information what the bug in the MIT spec is for a commitment to also prioritize fm verification of specThanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.