The 7th RISC-V Workshop has rejected my talk on riscv-formal. (They "accepted it as a poster".)
Show this thread
-
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.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
But but but... all the hard bits of specs and of processors are in exception handling. If you skip that bit, you’re doing the easy 10%
-
This is the MIT Spec: https://github.com/mit-plv/riscv-semantics … Contains parser for subset of Haskell with >200 shift-reduce (and some r-r) conflicts.
- Show replies
New conversation -
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.