Make with Ada 2017- A "Swiss Army Knife" Watch

Summary

The Hexiwear is an IoT wearable development board that has two NXP Kinetis microcontrollers. One is a K64F (Cortex-M4 core) for running the main embedded application software. The other one is a KW40 (Cortex M0+ core) for running a wireless connectivity stack (e.g., Bluetooth BLE or Thread). The Hexiwear board also has a rich set of peripherals, including OLED display, accelerometer, magnetometer, gryroscope, pressure sensor, temperature sensor and heart-rate sensor. This blog article describes the development of a "Swiss Army Knife" watch on the Hexiwear platform. It is a bare-metal embedded application developed 100% in Ada 2012, from the lowest level device drivers all the way up to the application-specific code, for the Hexiwear's K64F microcontroller. I developed Ada drivers for Hexiwear-specific peripherals from scratch, as they were not supported by AdaCore's Ada drivers library. Also, since I wanted to use the GNAT GPL 2017 Ada compiler but the GNAT GPL distribution did not include a port of the Ada Runtime for the Hexiwear board, I also had to port the GNAT GPL 2017 Ada runtime to the Hexiwear. All this application-independent code can be leveraged by anyone interested in developing Ada applications for the Hexiwear wearable device.

Project Overview

The purpose of this project is to develop the embedded software of a "Swiss Army Knife" watch in Ada 2012 on the Hexiwear wearable device.

The Hexiwear is an IoT wearable development board that has two NXP Kinetis microcontrollers. One is a K64F (Cortex-M4 core) for running the main embedded application software. The other one is a KW40 (Cortex M0+ core) for running a wireless connectivity stack (e.g., Bluetooth BLE or Thread). The Hexiwear board also has a rich set of peripherals, including OLED display, accelerometer, magnetometer, gryroscope, pressure sensor, temperature sensor and heart-rate sensor.

The motivation of this project is two-fold. First, to demonstrate that the whole bare-metal embedded software of this kind of IoT wearable device can be developed 100% in Ada, from the lowest level device drivers all the way up to the application-specific code. Second, software development for this project will produce a series of reusable modules that can be used in the future as a basis for creating "labs" for teaching an Ada 2012 embedded software development class using the Hexiwear platform. Given the fact that the Hexiwear platform is a very attractive platform for embedded software development, its appeal can be used to attract more embedded developers to learn Ada.

The scope of the project will be to develop only the firmware that runs on the application microcontroller (K64F). Ada drivers for Hexiwear-specific peripherals need to be developed from scratch, as they are not supported by AdaCore’s Ada drivers library. Also, since I will be using the GNAT GPL 2017 Ada compiler and the GNAT GPL distribution does not include a port of the Ada Runtime for the Hexiwear board, the GNAT GPL 2017 Ada runtime needs to be ported to the Hexiwear board.

The specific functionality of the watch application for the time frame of "Make with Ada 2017" will include:

• Watch mode: show current time, date, altitude and temperature

• Heart rate monitor mode: show heart rate (when Hexiwear worn on the wrist)

• G-Forces monitor mode: show G forces in the three axis (X, Y, Z).

In addition, when the Hexiwear is plugged to a docking station, a command-line interface will be provided over the UART port of the docking station. This interface can be used to set configurable parameters of the watch and to dump debugging information.

Summary of Accomplishments

I designed and implemented the "Swiss Army Knife" watch application and all necessary peripheral drivers 100% in Ada 2012. The only third-party code used in this project, besides the GNAT GPL Ravenscar SFP Ada runtime library, is the following:

• A font generator, leveraged from AdaCore’s Ada drivers library.

• Ada package specification files, generated by the the svd2ada tool, containing declarations for the I/O registers of the Kinetis K64F’s peripherals.

Below are some diagrams depicting the software architecture of the "Swiss Army Knife" watch:

• Hardware Context Diagram

• Source Code Architecture

• Ada Task Architecture

The current implementation of the "Swiss Army Knife" watch firmware, delivered for "Make with Ada 2017" has the following functionality:

• Three operating modes:

• Watch mode: show current time, date, altitude and temperature

• Heart rate monitor mode: show heart rate monitor raw reading, when Hexiwear worn on the wrist.

• G-Forces monitor mode: show G forces in the three axis (X, Y, Z).

• To switch between modes, the user just needs to do a double-tap on the watch’s display. When the watch is first powered on, it starts in "watch mode".

• To make the battery charge last longer, the microcontroller is put in deep-sleep mode (low-leakage stop mode) and the display is turned off, after 5 seconds. A quick tap on the watch’s display, will wake it up. Using the deep-sleep mode, makes it possible to extend the battery life from 2 hours to 12 hours, on a single charge. Indeed, now I can use the Hexiwear as my personal watch during the day, and just need to charge it at night.

• A command-line interface over UART, available when the Hexiwear device is plugged to its docking station. This interface is used for configuring the following attributes of the watch:

• Current time (not persistent on power loss, but persistent across board resets)

• Current date (not persistent on power loss, but persistent across board resets)

• Background color (persistent on the K64F microcontroller’s NOR flash, unless firmware is re-imaged)

• Foreground color (persistent on the K64F microcontroller’s NOR flash, unless firmware is re-imaged)

Also, the command-line interface can be used for dumping the different debugging logs: info, error and debug.

• Picture of the watch’s display.

• Video of the watch in action.

• The final version of the code of the watch application and the associated peripheral drivers submitted to the "Make with Ada 2017" programming competition can be found in GitHub at: https://github.com/jgrivera67/make-with-ada/releases/tag/Make-with-Ada-2017-final

The top-level code of the watch application can be found at: https://github.com/jgrivera67/make-with-ada/tree/master/hexiwear_watch

I ported the GNAT GPL 2017 Ravenscar Small-Foot-Print Ada runtime library to the Hexiwear board and modify it to support the memory protection unit (MPU) of the K64 microcontroller, and more specifically to support MPU-aware tasks. This port of the Ravenscar Ada runtime can be found in GitHub at https://github.com/jgrivera67/embedded-runtimes

The relevant folders are:

• https://github.com/jgrivera67/embedded-runtimes/tree/master/ravenscar-kinetis_k64f_hexiwear

• https://github.com/jgrivera67/embedded-runtimes/tree/master/bsps/kinetis_k64f_hexiwear

• https://github.com/jgrivera67/embedded-runtimes/tree/master/bsps/kinetis_k64f_common/bsp

I developed device drivers for the following peripherals of the Kinetis K64 micrcontroller as part of this project and contributed their open-source Ada code in GitHub at https://github.com/jgrivera67/make-with-ada/tree/master/drivers/mcu_specific/nxp_kinetis_k64f:

• DMA Engine

• SPI controller

• I2C controller

• Real-time Clock (RTC)

• Low power management

• NOR flash

These drivers are application-independent and can be easily reused for other Ada embedded applications that use the Kinetis K64F microcontroller.

I developed device drivers for the following peripherals of the Hexiwear board as part of this project and contributed their open-source Ada code in GitHub at https://github.com/jgrivera67/make-with-ada/tree/master/drivers/board_specific/hexiwear:

• OLED graphics display (on top of the SPI and DMA engine drivers, and making use of the advanced DMA channel linking functionality of the Kinetis DMA engine)

• 3-axis accelerometer (on top of the I2C driver)

• Heart rate monitor (on top of the I2C driver)

• Barometric pressure sensor (on top of the I2C driver)

These drivers are application-independent and can be easily reused for other Ada embedded applications that use the Hexiwear board.

I designed the watch application and its peripheral drivers, to use the memory protection unit (MPU) of the K64F microcontroller, from the beginning, not as an afterthought. Data protection at the individual data object level is enforced using the MPU, for the private data structures from every Ada package linked into the application. For this, I leveraged the MPU framework I developed earlier and which I presented in the Ada Europe 2017 Conference. Using this MPU framework for the whole watch application demonstrates that the framework scales well for a realistic-size application. The code of this MPU framework is part of a modified Ravenscar small-foot-print Ada runtime library port for the Kinetis K64F microcontroller, whose open-source Ada code I contributed at https://github.com/jgrivera67/embedded-runtimes/tree/master/bsps/kinetis_k64f_common/bsp

I developed a CSP model of the Ada task architecture of the watch firmware with the goal of formally verifying that it is deadlock free, using the FDR4 tool. Although I ran out of time to successfully run the CSP model through the FDR tool, developing the model helped me gain confidence about the overall completeness of the Ada task architecture as well as the completeness of the watch_task’s state machine. Also, the CSP model itself is a form a documentation that provides a high-level formal specification of the Ada task architecture of the watch code.

Open

My Project’s code is under the BSD license It’s hosted on Github. The project is divided in two repositories:

• Application + Drivers RepositoryThe relevant folders are:

• https://github.com/jgrivera67/make-with-ada/tree/master/hexiwear_watch

• https://github.com/jgrivera67/make-with-ada/tree/master/drivers/portable

• https://github.com/jgrivera67/make-with-ada/tree/master/drivers/board_specific/hexiwear

• https://github.com/jgrivera67/make-with-ada/tree/master/drivers/mcu_specific/nxp_kinetis_k64f

• GNAT Ravenscar SFP Ada Runtime Library Port for the Hexiwear Board with Memory Protection Unit Support RepositoryThe relevant Folders are:

• https://github.com/jgrivera67/embedded-runtimes/tree/master/ravenscar-kinetis_k64f_hexiwear

• https://github.com/jgrivera67/embedded-runtimes/tree/master/bsps/kinetis_k64f_hexiwear

• https://github.com/jgrivera67/embedded-runtimes/tree/master/bsps/kinetis_k64f_common/bsp

To do the development, I used the GNAT GPL 2017 toolchain - ARM ELF format (hosted on Windows 10 or Linux), including the GPS IDE. I also used the svd2ada tool to generate Ada code from SVD XML files for the Kinetis microcontrollers I used.

Collaborative

I designed this Ada project to make it easy for others to leverage my code. Anyone interested in developing their own flavor of "smart" watch for the Hexiwear platform can leverage code from my project. Also, anyone interested in developing any type of embedded application in Ada/SPARK for the Hexiwear platform can leverage parts of the software stack I have developed in Ada 2012 for the Hexiwear, particularly device drivers and platform-independent/application-independent infrastructure code, without having to start from scratch as I had to. All you need is to get your own Hexiwear development kit (http://www.hexiwear.com/shop/), clone my Git repositories mentioned above and get the GNAT GPL 2017 toolchain for ARM Cortex-M (http://libre.adacore.com/download/, choose ARM ELF format).

The Hexiwear platform is an excellent platform to teach embedded software development in general, and in Ada/SPARK in particular, given its rich set of peripherals and reasonable cost. The Ada software stack that I have developed for the Hexiwear platform can be used as a base to create a series of programming labs as a companion to courses in Embedded and Real-time programming in Ada/SPARK, from basic concepts and embedded programming techniques, to more advanced topics such as using DMA engines, power management, connectivity, memory protection and so on.

Dependable

• I used the memory protection unit to enforce data protection at the granularity of individual non-local data objects, throughout the code of the watch application and its associated device drivers.

• I developed a CSP model of the Ada task architecture of the watch firmware with the goal of formally verifying that it is deadlock free, using the FDR4 tool. Although I ran out of time to successfully run the CSP model through the FDR tool, developing the model helped me gain confidence about the completeness of the watch_task’s state machine and the overall completeness of the Ada task architecture of the watch code.

• I consistently used the information hiding principles to architect the code to ensure high levels of maintainability and portability, and to avoid code duplication across projects and across platforms.

• I leveraged extensively the data encapsulation and modularity features of the Ada language in general, such as private types and child units including private child units, and in some cases subunits and nested subprograms.

• I used gnatdoc comments to document key data structures and subprograms.

• I used Ada 2012 contract-based programming features and assertions extensively

• I used range-based types extensively to leverage the Ada power to detect invalid integer values.

• I Used Ada 2012 aspect constructs wherever possible

• I Used GNAT coding style. I use the -gnaty3abcdefhiklmnoOprstux GNAT compiler option to check compliance with this standard.

• I used GNAT flags to enable rigorous compile-time checks, such as -gnato13 -gnatf -gnatwa -gnatVa -Wall.

Inventive

• The most innovative aspect of my project is the use of the memory protection unit (MPU) to enforce data protection at the granularity of individual data objects throughout the entire code of the project (both application code and device drivers). Although the firmware of a watch is not a safety-critical application, it serves as a concrete example of a realistic-size piece of embedded software that uses the memory protection unit to enforce data protection at this level of granularity. Indeed, this project demonstrates the feasibility and scalability of using the MPU-based data protection approach that I presented at the Ada Europe 2017 conference earlier this year, for true safety-critical applications.

CSP model of the Ada task architecture of the watch code, with the goal of formally verifying that the task architecture was deadlock free, using the FDR4 model checking tool. Although I ran out of time to successfully run the CSP model through the FDR tool, the model itself provides a high-level formal specification of the Ada task architecture of the watch firmware, which is useful as a concise form of documentation of the task architecture, that is more precise than the task architecture diagram alone.

Future Work

Short-Term Future Plans

Implement software enhancements to existing features of the "Swiss Army Knife" watch:

• Calibrate accuracy of altitude and temperature readings

• Calibrate accuracy of heart rate monitor reading

• Display heart rate in BPM units instead of just showing the raw sensor reading

• Calibrate accuracy of G-force readings

Develop new features of the "Swiss Army Knife" watch:

• Display compass information (in watch mode). This entails extending the accelerometer driver to support the built-in magnetometer

• Display battery charge remaining. This entails writing a driver for the K64F’s A/D converter to interface with the battery sensor

• Display gyroscope reading. This entails writing a driver for the Hexiwear’s Gyroscope peripheral

• Develop Bluetooth connectivity support, to enable the Hexiwear to talk to a cell phone over blue tooth as a slave and to talk to other Bluetooth slaves as a master. As part of this, a Bluetooth "glue" protocol will need to be developed for the K64Fto communicate with the Bluetooth BLE stack running on the KW40, over a UART. For the BLE stack itself, the one provided by the chip manufacturer will be used. A future challenge could entail to write an entire Bluetooth BLE stack in Ada to replace the manufacturer’s KW40 firmware.

Finish the formal analysis of the Ada task architecture of the watch code, by successfully running its CSP model through the FDR tool to verify that the architecture is deadlock free, divergence free and that it satisfies other applicable safety and liveness properties.

Long-Term Future Plans

Develop more advanced features of the "Swiss Army Knife" watch:

• Use sensor fusion algorithms combining readings from accelerometer and gyroscope

• Add Thread connectivity support, to enable the watch to be an edge device in an IoT network (Thread mesh). This entails developing a UART-based interface to the Hexiwear’s KW40 (which would need to be running a Thread (804.15) stack).

• Use the Hexiwear device as a dash-mounted G-force recorder in a car. Sense variations of the 3D G-forces as the car moves, storing the G-force readings in a circular buffer in memory, to capture the last 10 seconds (or more depending on available memory) of car motion. This information can be extracted over bluetooth.

• Remote control of a Crazyflie 2.0 drone, from the watch, over Bluetooth. Wrist movements will be translated into steering commands for the drone.

Develop a lab-based Ada/SPARK embedded software development course using the Hexiwear platform, leveraging the code developed in this project. This course could include the following topics and corresponding programming labs:

• Accessing I/O registers in Ada.

• Lab: Layout of I/O registers in Ada and the svd2ada tool

• Pin-level I/O: Pin Muxer and GPIO.

• Lab: A Traffic light using the Hexiwear’s RGB LED

• Embedded Software Architectures: Cyclic Executive.

• Lab: A watch using the real-time clock (RTC) peripheral with polling

• Embedded Software Architectures: Main loop with Interrupts.

• Lab: A watch using the real-time clock (RTC) with interrupts

• Embedded Software Architectures: Tasks.

• Lab: A watch using the real-time clock (RTC) with tasks

• Serial Console.

• Lab: UART driver with polling and with interrupts)

• Sensors: A/D converter.

• Lab: Battery charge sensor

• Actuators: Pulse Width Modulation (PWM).

• Lab: Vibration motor and light dimmer

• Writing to NOR flash.

• Lab: Saving config data in NOR Flash

• Inter-chip communication and complex peripherals: I2C.

• Lab: Using I2C to interface with an accelerometer

• Inter-chip communication and complex peripherals: SPI.

• Lab: OLED display

• Direct Memory Access I/O (DMA).

• Lab: Measuring execution time and making OLED display rendering faster with DMA

• The Memory Protection Unit (MPU).

• Lab: Using the memory protection unit

• Power Management.

• Lab: Using a microcontroller’s deep sleep mode

• Cortex-M Architecture and Ada Startup Code.

• Lab: Modifying the Ada startup code in the Ada runtime library to add a reset counter)

• Recovering from failure.

• Lab: Watchdog timer and software-triggered resets

• Bluetooth Connectivity

• Lab: transmit accelerometer readings to a cell phone over Bluetooth