Formal modeling of the 64-bit RISC-V instruction set architecture

Context

RISC-V is a modern open standard instruction set architecture (ISA). The ISA is the central interface between the hardware and the software and specifies the instructions supported by a given processor. Commonly, the semantics of these instructions—and edge cases in this regard—are described in natural language. The natural language definition of the RISC-V ISA can be found here.

Problem

Considering that natural language is ambiguous, an implementation of these specified instructions semantics (e.g., for a RISC-V simulator) is a manual process, requiring a transformation of the natural language specification to executable code. Naturally, considering the complexity of the specification, errors can occur during this manual transformation.

In order to prevent such errors, prior work has proposed the use of a formal machine-readable language to describe ISA instruction semantics. These formal languages are unambiguous and thus machine-readable. They are beneficial for various use-case, such as code generation, testing, documentation, or binary analysis. Recognizing the potential of these formal languages, RISC-V provides an official formal specification in the SAIL language.

However, SAIL is a non-executable formal specification requiring the implementation of a compiler to transform it to executable code. For many execution-based tasks (e.g., simulation or binary analysis), this creates a lot of duplicate work. Therefore, executable formal specifications have received increased attention in recent years.

In prior work, we have developed a versatile executable formal model of the RISC-V architecture and have implemented several interpreters for this specification, most recently a symbolic interpreter. Presently, the formal specification only covers 32-bit RISC-V, however as a basis for future work, we would like to extend our symbolic interpreter to 64-bit RISC-V. To this end, our formal executable specification should be extended in this thesis to support 64-bit RISC-V (RV64). This should be achieved by making the specification parameterisable over the word size, thereby requiring only minor changes in the description of instruction semantics. Naturally, correctness aspects of the extended specification should also be examined to some degree in the thesis.

Requirements

• Solid understanding of computer architecture
• Proficiency in functional programming, ideally prior experience with Haskell (or a similar language)
• Analytical skills to evaluate correctness aspects of the formalized RV64 specification

More Information

For more information, you can refer to the following resources

• The Hackage package for our formal RISC-V specification (includes API documentation)
• The source code of our executable formal specification
• The formal description of the RISC-V base instruction set

Further, the following papers might be useful as a starting point:

• Versatile and Flexible Modelling of the RISC-V Instruction Set Architecture
• Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics
• ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS

Recommended reading to get started with Haskell: Learn You a Haskell.⏎