|
|
|---|
|
|
|
|---|
Specification of the RISC-V ISA.
We formalize the RISC-V ISA, based on [ISA] and [ISAP].
Since RISC-V is a family of ISAs, depending on base and extensions, we define a notion of features that determine the exact family member. We define a data type (like an abstract syntax) for instructions, and the encoding of these instructions; we define instruction decoding declaratively, as the inverse of encoding. We formalize the possible states of execution, the semantics of the instructions, and how execution proceeds in steps.
This specification is high-level, aimed at maximizing clarity. It is not aimed at being efficiently executable; in fact, since decoding is specified as inverse of encoding, this specification is not fully executable. See executable for an executable refinement.