Porting Ironclad to RISC-V architecture

Overview

AdaCore supports the propagation and development of Ada-based software. Ironclad is a partially formally verified kernel for x86-64 platforms written in Ada and AdaCore wants it ported to the RISC-V architecture to expand Ironclad’s usability for embedded systems and platforms.

Objectives

The objectives of this project were to port key Ironclad functionality from the x86-64 architecture to the RISC-V architecture, and to provide clear documentation for end-users to modify the kernel to their specifications. Additionally, one goal was to allow the end user to enter a development environment of build-run-debug with minimal steps after downloading the project.

Approach

• Assess use cases and user requirements

• Design system functional and non-functional requirements from the use cases and user requirements.

• Determine existing kernel design.

• Assess existing x86-64 functionality

• Architect RISC-V kernel implementation.

• Assess platform emulation tools and learn Ada.

• Port one kernel functionality at a time.

• Perform Unit and Integration testing ported functionality.

• Move to the next functionality.

• Perform System testing.

• Deliver project to sponsor.

Outcomes

As a result of this project:

• Development processes were streamlined for the Ironclad kernel

• The Ironclad kernel boots to the idle mode on RISC-V, initializing key functionalities

• This project enables future developers to get a development environment running faster, automating several key tasks.