This repository contains an Ada/SPARK driver for the DecaWave DW1000 ultra-wideband (UWB) radio chip.

The driver code written and verified using the SPARK language (a subset of Ada). GNATprove is used to prove the absence of runtime errors such as: numerical overflow, infinite loops, division by zero, and out-of-bounds array accesses.

The API is currently considered unstable. You may need to update your code to to reflect API changes as the driver is developed.

All files are licensed under the MIT license.

To use the driver, include the contents of the src directory into your project, as well as the appropriate BSP directory under bsp-examples (or provide your own implementation for your own hardware).

Check out the Wiki for more information on using the driver.

Parts of the driver require certain runtime features that are not available on all bare-board Ada runtimes. In particular, the following features are used:

• Protected objects are used by the DecaDriver. This requires an Ada runtime supporting tasking (e.g. a Ravenscar runtime).
• The Ada.Real_Time.Clock function is used by the DW1000.Driver package. This feature is also supported in Ravenscar runtimes.
• The package Ada.Numerics.Generic_Elementary_Functions is used by the package DW1000.Reception_Quality. Small footprint (SFP) Ravenscar runtimes don't support these math functions, but they are implemented in the full Ravenscar runtimes.

Typically, this means that a full Ravenscar runtime is required as a minimum. AdaCore's bb-runtimes repository has runtimes available for a variety of bare-bones embedded targets. The exact runtime needed depends on your target board.

If you don't use all of the features of this driver, then you can use a reduced runtime. For example, if you don't use the DecaDriver then you don't need a Ravenscar runtime (unless other parts of your code use Ravenscar features).

This driver currently supports the DWM1001 module. This module is used in the DWM1001-DEV development board and the MDEK1001 development kit.

Previously, the EVB1000 was supported and an old port to this board is still present in the bsp-examples directory. This port is currently obsolete/broken due to lack of EVB1000 hardware available to develop with.

Porting the driver to a new target consists of re-implementing the dw1000-bsp.adb file, which implements the DW1000.BSP package. This package implements everything necessary to actually communicate with the DW1000 including: sending and receiving data via SPI, managing the DW1000 interrupt request (IRQ), resetting the DW1000, and waking it up from its sleep mode.

The package spec is already defined in the package spec in the file src/dw1000-bsp.ads. This stays the same for all targets; only the package body needs to be re-implemented.

An reference implementation for the DWM1001 target can be found in bsp-examples/dwm1001/dw1000-bsp.adb. This is a useful starting point when porting to a new target.

If you are using the DecaWave EVB1000 evaluation board then there are the following two SPARK and Ada projects on GitHub which are useful:

• EVB1000: SPARK drivers for the LCD, LED, and switch peripherals on the EVB1000.
• Ravenscar-full-evb1000: a full Ravenscar runtime for the STM32F105 ARM Cortex-M3 microcontroller, configured for the EVB1000.

See the examples directory for various example programs using the driver.