have not formally verified their model against ANYTHING yet. I'm not telling them bc I want to "find it with riscv-formal" first. :) 2/2
-
Target audience should include asm programmers, people writing tests, people writing compilers and OS, hardware designers, ...
Yep. I didn't propose my Verilog spec as the official spec for two reasons: (1) I thought it was too domain specific and
-
-
I think that having multiple users is so important that I think ISA specs should be written in a DSL (not Verilog, Coq, HOL, ...).
-
And should natively support state changes (no monads, no getRegister/setRegister function, ...). So like SAIL, L2, ASL, ...
End of conversation
New conversation -
-
-
(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.)
-
Yes, any existing language will tend to tie your hands over the ability to deliberately underspecify the architecture.
End of conversation
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.