the entire spec goes out the window and the system can do whatever it wants. UB is part of the contract between system and user, and the
-
More seriously, what do you do now? Clearly this change to the ISA has far-reaching consequences for you/seems pretty bad.
I've been requesting comments on the RISC-V formal spec mailing list. We'll see what happens.. But it's clear that I can't implement this
-
-
in riscv-formal. Even a very small bounded and causal version of this would drastically complicate the SMT problems I'm constructing..
-
Definitely beyond me to impl at this point, but I am curious how a casual version would be done. Check insns side effects, if they are >>
- Show replies
New conversation -
-
-
since all executions triggering HW UB trivially fulfill the spec, you can assume that each instruction does not trigger it, no?
-
meaning that you can contextlessly reject nop doing anything other than nothing
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.