|
|
|---|
|
|
|
|---|
Executable refinement of the RISC-V specification.
The specification is aimed at clarity, and not at efficient execution. In fact, since decoding is specified as inverse of encoding, the specification is not fully executable. Here we provide an executable refinement of the specification. In particular, we define an executable decoding function decodex and we prove it equivalent to the declaratively defined decode.
In the future, we may investigate synthesizing the executable decoder using APT.
We use apt::simplify to obtain executable versions of step and stepn, which call decodex instead of decode.
The semnantic functions do not depend on decoding and thus do not need to be refined to be fully executable.