I recent­ly watched the talks from the 28^th Ada-Europe Inter­na­tion­al Con­fer­ence on Reli­able Soft­ware Tech­nolo­gies (AEiC 2024), which was held in Barcelona last June.

One talk that stood out was HiR­TOS: a Mul­ti­core RTOS Writ­ten in SPARK Ada by J. Ger­man Rivera. In his pre­sen­ta­tion, he men­tioned run­ning HiR­TOS on Ren­ode, an open-source sim­u­la­tion and vir­tu­al devel­op­ment frame­work for com­plex embed­ded systems .

Like many, I’ve pri­mar­i­ly dab­bled with QEMU, but my curios­i­ty led me to explore an intrigu­ing talk by Sean Cross, Ren­ode: Easy CI for your Weird Hard­ware. He show­cased just how easy and pow­er­ful Ren­ode is for con­fig­ur­ing and sim­u­lat­ing com­plex embed­ded hard­ware. The Ren­ode team even assem­bled a com­plete graph­i­cal sim­u­la­tion — includ­ing vec­tor tables, timers, frame­buffer, and firmware — with­in an hour, all while attend­ing a con­fer­ence talk!

After watch­ing the pre­sen­ta­tion (at 1.5x speed), I was eager to try some­thing hands-on with Ren­ode. How­ev­er, after some search­ing, I found that up-to-date, straight­for­ward guides on using Ren­ode with­out div­ing into the source code or exten­sive doc­u­men­ta­tion took a lot of work.

I pre­vi­ous­ly port­ed the Ada Dri­ver Library for the Cap­stone projects I men­tor, cre­at­ing a repro­ducible Alire build chain for the STM32F429 dis­cov­ery dev board. With this set­up, I quick­ly built an STM32F429 blinky app firmware direct­ly using Alire. Armed with a cof­fee and some out­dat­ed videos, I took on the chal­lenge of load­ing and run­ning the firmware ELF in Renode.

Before div­ing into the details, If you’re eager to jump straight into the action, the Ren­ode files need­ed for this sim­u­la­tion are avail­able in the Ren­ode fold­er of the stm32_​blinky_​demo repos­i­to­ry. You can sim­ply clone the repo and fol­low the README​.md to build the firmware using Alire and launch it on Renode.

For those who want to dig deep­er, the fol­low­ing sec­tions will walk you through the con­tent and set­up of the Ren­ode files need­ed to devel­op a suc­cess­ful simulation.

The Ada Code #

This is your typ­i­cal ​“Hel­lo World” for embed­ded sys­tems, cross-com­piled for the ARM Cor­tex-M4 using the embed­ded-stm32f429dis­cov­ery Ada run­time avail­able in Alire:

This simple program toggles all LEDs on the STM32F429 discovery board every second. To obtain the ELF binary, just run

$ alr build

Setting Up the Renode Hardware Configuration #

Renode is written in C# and can be extended primarily to add new hardware peripherals or configure more complex simulation scenarios. However, Renode also provides its hardware description language and scripting language. The .repl (REnode PLatform) files define your hardware configuration. Many existing device descriptions for various development boards and CPUs are included in the Renode distribution, typically found in the platforms/boards and platforms/cpus directories within your Renode installation.

Let’s set up our stm32f429_custom.repl file step by step. A .repl file can include other hardware configurations, so we’ll start by incorporating the STM32 ARM device used on the STM32F429 discovery board, which Renode already provides:

using "platforms/cpus/stm32f429.repl"

After thoroughly searching the Renode distribution, I found no pre-configured GPIO Port G connected to an LED. Since our Ada firmware relies on this connection, we’ll first need to enhance our custom Renode hardware description by setting up the GPIO Port G:

gpioPortG: GPIOPort.STM32_GPIOPort @ sysbus <0x40021800, +0x400> 
numberOfAFs: 16 
[0-15] -> exti@[0-15]

In this snippet:

• sysbus is the central object where you typically connect components in Renode. It’s also the object you interact with in the Renode console to inspect and manipulate everything tied to your simulated system.

• <0x40021800, +0x400> indicates that the GPIO Port is memory-mapped at address 0x40021800 with a memory range of 0x400. This mapping corresponds directly to the device datasheet, making verifying it easy.

• numberOfAFs: 16 line shows that this GPIO port supports 16 alternate functions.

• [0-15] -> exti@[0-15] line maps each of the GPIO pins (0-15) to the corresponding external interrupt lines (exti), allowing the GPIO pins to trigger interrupts.

This setup defines how the GPIO Port interacts with the system bus, mapping it into the simulated system’s memory space.

Adding the LED Con­fig­u­ra­tion #

Now, let’s add the LED configuration:

UserLED: Miscellaneous.LED @ gpioPortG

gpioPortG:
    13 -> UserLED@0

In this snippet:

• UserLED: Miscellaneous.LED @ gpioPortG defines an LED con­nect­ed to gpioPortG, our pre­vi­ous­ly con­fig­ured GPIO port.

• gpioPortG: 13 -> UserLED@0 maps pin 13 of gpioPortG to the UserLED. The @0 is an inter­nal iden­ti­fi­er for the UserLED instance, allow­ing Ren­ode to dis­tin­guish between mul­ti­ple instances of LEDs if need­ed. Pin 13 on the GPIO port, spec­i­fied in our Ada firmware if you fol­low the code def­i­n­i­tion of All_​LEDs, will con­trol this par­tic­u­lar instance of the UserLED.

This con­fig­u­ra­tion ensures that acti­vat­ing pin 13 of gpioPortG in your sim­u­la­tion will trig­ger the UserLED, sim­u­lat­ing the behav­ior of an actu­al LED con­nect­ed to that pin on your hardware.

Mov­ing to the Ren­ode Sim­u­la­tion Script #

We can now move on to the sim­u­la­tion script .resc (REn­ode SCript) using our pre­vi­ous hard­ware setup. 

Ren­ode offers a pow­er­ful inter­ac­tive con­sole where you can cre­ate, manip­u­late, and inspect your sim­u­la­tion or its var­i­ous com­po­nents. You can inter­act with your sim­u­la­tion direct­ly, mak­ing real-time adjust­ments, or script these inter­ac­tions for automa­tion. This is where our stm32f429_startup.resc file comes into play.

Let’s walk through set­ting up the sim­u­la­tion instruc­tions step by step:

Start by cre­at­ing a new machine named stm32f429_custom:

mach create "stm32f429_custom"

Next, load the cus­tom plat­form descrip­tion for the STM32F429 dis­cov­ery board:

machine LoadPlatformDescription @/path/to/stm32_blinky_demo/renode/stm32f429_custom.repl

Now, load the ELF firmware for the blinky application:

sysbus LoadELF @/path/to/stm32_blinky_demo/bin/stm32_blinky_demo

To mon­i­tor the state changes of the UserLED, set up logging:

logLevel -1 gpioPortG.UserLED

Final­ly, start the machine:

start

Run­ning the Script #

As said, these pre­vi­ous instruc­tions are part of the stm32f429_startup.resc script file. To actu­al­ly run the sim­u­la­tion, start the Ren­ode console:

$ renode --console

Run the script by includ­ing it in the console

include @/path/to/stm32_blinky_demo/renode/stm32f429_startup.resc

If every­thing goes as planned, you should see the LED state changes being logged at one-sec­ond intervals:

Clos­ing Remarks #

This process takes you from set­ting up your sim­u­la­tion envi­ron­ment to run­ning and observ­ing the behav­ior of your STM32F429 firmware, all with­in Renode.

I hope you found this crash course on run­ning Ada code over Ren­ode help­ful and that you enjoy watch­ing your LED blink in the vir­tu­al world!