Betreuer | Dr. Sören Tempel |
IBR Gruppe | VSS (Prof. Dietrich) |
Art | Bachelorarbeit |
Status | offen |
ContextRISC-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. ProblemConsidering 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
More InformationFor more information, you can refer to the following resources
Further, the following papers might be useful as a starting point: |