But I can't yet. Because so far they can't interface their model with anything that would actually allow me to use formal methods on it..
-
-
Replying to @oe1cxw @whitequark
You’re saying there is a bug in the spec they are verifying against?
1 reply 0 retweets 0 likes -
Replying to @alastair_d_reid @whitequark
Yes. But they aren't verifying their spec against anything (yet). Their primary focus is on proofing abstract properties of the ISA..
3 replies 0 retweets 0 likes -
And that is also very important of course, but I think the first step should be proving that the spec actually matches the implementation.
2 replies 0 retweets 0 likes -
Replying to @oe1cxw @whitequark
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%
2 replies 1 retweet 2 likes -
Replying to @alastair_d_reid @whitequark
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.
3 replies 0 retweets 4 likes -
Replying to @oe1cxw @whitequark
Why would you write spec in a language that many programmer find obscure and hard (for humans) to parse???
2 replies 0 retweets 4 likes -
Replying to @alastair_d_reid @whitequark
I asked exactly that question in the workgroup. Answer: Target audience is formal people, for them Haskell is easy. (paraphrased)
3 replies 0 retweets 0 likes -
Replying to @oe1cxw @whitequark
Target audience should include asm programmers, people writing tests, people writing compilers and OS, hardware designers, ...
2 replies 0 retweets 5 likes -
Replying to @alastair_d_reid @whitequark
Yep. I didn't propose my Verilog spec as the official spec for two reasons: (1) I thought it was too domain specific and
2 replies 0 retweets 0 likes
(2) I have no plans for modelling of concurrent memory accesses in my ISA models. (Which was agreed is necessary and I think it is.)
-
-
Replying to @oe1cxw @whitequark
Yes, any existing language will tend to tie your hands over the ability to deliberately underspecify the architecture.
0 replies 1 retweet 1 likeThanks. 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.