Since the early days of my embedded Ada/SPARK adventures, starting the Ada Drivers Library project, making demos on various micro-controllers or publishing projects on this blog, my goal has always been to develop pure Ada/SPARK embedded software, drivers and support libraries.

It is not necessarily the most effective way of integrating Ada/SPARK in a project. Writing a binding for a tried and tested C library will often be a smarter choice. But my drive is not always a short term solution, I want to show the capabilities of Ada/SPARK for embedded systems and build an ecosystem.

This is why a couple years ago I started to tackle what was probably my most daunting project at the time, an embedded USB Device stack written 100% in Ada.

USB is a complex protocol stack without a lot of beginner-friendly documentation available online. And up until a few years ago, USB stacks provided by hardware vendors were the only option.

Things are changing now with, for instance, the TinyUSB project. The turning point for me was the discovery of the “USB in a nutshell” website. Reading this guide to the internals of the USB protocol gave me the confidence I needed to start this project, and I highly recommend it to anyone interested in USB.

I had a first working version of the USB stack for the STM32F405 micro-controller about four years ago, but I couldn’t find the time to make this implementation clean and micro-controller agnostic until last year. I resumed my work, this time on the Microchip SAMD51, with the goal of making the stack reusable and available in the Alire ecosystem.

Scope and State of the Project

I call the project presented here an “embedded USB Device stack”.

“Embedded” because it can run on resource limited systems (micro-controllers) and it is compatible with limited Ada run-times including a Zero-FootPrint (ZFP).

“Device” because there are two sides to the USB protocol: devices (keyboards, webcams, external drives, printers, etc.) and hosts (computers to plug devices into). The stack presented here implements the device side, meaning it can be used to implement a USB device (keyboard, webcam, etc.). Some micro-controllers are also capable of acting as USB hosts, therefore the stack could be improved in the future to also support this mode.

About the state of the project, I want to say that it is mostly a prototype at this stage and therefore not recommended for production use.

Design

The overall design of my USB stack is inspired by both the libopencm3 and TinyUSB implementations, which are written in C. It is of course adapted for the strengths and weaknesses of the Ada language. The main difference is probably in the heavy use of C preprocessing in many USB stacks. It is very convenient for assembling USB descriptors or enabling/disabling features at compile time.

Even if, in theory, preprocessing is possible in Ada, I decided to stay away from it and embrace the difference. The stack will, for instance, build device descriptors at run-time, which will use more CPU, but that means it can be reconfigured to provide different USB device classes depending on the run-time context.

Part of the design decisions also originate from my desire to move this implementation to SPARK at some point. Right now I am far from it, but I did avoid some Ada features that are not available in SPARK.

Control Transfer State Machine

The main part of the USB Stack is the handling of control transfers. It is based on a state machine that handles Setup Requests and the data payload associated with them. The payload can be either sent by the Host with the Setup Packet (Host to Device), or sent by the Device as an answer to the Setup Packet (Device to Host). A zero-length-packet (ZLP) is sometimes used for acknowledgement of the Setup Request. If the Device doesn't support a given Setup Packet sent by the Host, the control end-points are stalled to indicate an error.

Some standard Setup Requests are handled directly by the stack, while others are dispatched to the USB classes.

USB Classes

In the USB protocol, a class is a standardized service that a USB device can provide to the host. In a way, they are comparable to HTTP or FTP for the TCP/IP stack.

Some of the most common classes are:

• Human Interface Device (HID): for mice, keyboard, joystick, game pads, etc.

• Mass Storage Class (MSC): for memory stick or external hard drives

• Video: for webcam

• Audio: for sound cards, microphones but also MIDI controllers

A USB device can implement one or more classes, this is how your webcam can do both video and audio.

As long as a device implements standard classes, it can be used on any host with the corresponding class support. This is a key part of USB’s success in my opinion, devices are portable across operating systems (Windows, Linux, macOS) as long as standard class drivers are available.

The standard also allows for vendor specific classes. One should stay away from implementing vendor classes because they require specific drivers on the host and therefore lose the portability of USB.

In my USB stack, classes are implementations of a limited Ada interface called “USB_Device_Class”. To implement a new class, a set of primitives have to be overridden:

• Initialize: to request resources from the USB stack such as end-points and transfer buffers

• Fill_Config_Descriptor: to provide the class specific descriptor during enumeration

• Setup_Read_Request and Setup_Write_Request: to handle class specific USB setup requests

• Transfer_Complete: to handle the completion of a transfer on one of the class endpoint

• etc.

Users of the stack can then dynamically register classes to compose the services of their device. For instance, combining HID and MSC.

A couple of common off-the-shelf classes are already implemented in the stack and can be used as is:

• HID (keyboard, mouse, and gamepad)

• Serial over USB

• MIDI (instrument).

The plan is to provide more off-the-shelf classes in the future.

Porting the USB Device stack

The stack is based on a Hardware Abstraction Layer (HAL) that defines an Ada interface called USB.HAL.Device.USB_Device_Controller. To use the USB Device stack on a micro-controller, one must provide an implementation of this interface.

Here are some of the primitives to be overridden:

• Poll: this function returns a record that notifies an event from the USB bus (e.g. transfer complete, setup request)

• EP_Write_Packet: this procedure configures an End-Point (EP) to send data to the host

• EP_Ready_For_Data: this procedure configures an End-Point to be ready to receive data from the host

• Set_Address: this procedure sets the address of the device on the bus

• etc.

Testing the USB Device stack

In theory, testing USB involves at least two machines with kernel code on one side for host drivers. That is difficult to put in place and maintain. It is also not very compatible with Continuous Integration setups. Instead I decided to create a framework to simulate USB exchanges.

The framework plays predefined scenarios, such as descriptor requests, set address, enumeration and checks that the stack behaves as expected. It can also test the stack behavior when the host requests unknown descriptors. More test scenarios can be added in the future as soon as problems are detected.

This framework is very good for regression testing and it is easy to run, on the other hand it is not easy to write scenarios. Therefore I am looking at other options for testing the stack against a real host, like using the Linux Raw_Gadget interface to simulate a USB device from Linux userland, or the QEMU emulator.

Example

The stack is now available in Alire under this usb_embedded crate: https://alire.ada.dev/crates/usb_embedded

A USB_Device_Controller implementation is available for the Microchip samd51 in the samd51_hal Alire crate. And if you own one of the AdaFruit PyGamer boards, you can try the example project I made which makes the PyGamer act as a USB gamepad:

Jere­my Gross­er is also imple­ment­ing the required sup­port in the Rasp­ber­ry Pi RP2040 Alire crate. So stay tuned for that. It is now avail­able in Alire: https://alire.ada.dev/crates/rp2040_hal