Using the MSP432 DriverLib ROM with Ada and SPARK

Texas Instruments’ (TI) MSP432 is a neat little microcontroller based on a 32-bit, Arm Cortex-M4F processor. It’s found on SimpleLink MSP432P401R Launchpad that’s the smarts behind TI’s TI-RSLK robotics kit. MSP432 board mates with a Pololu Robotics & Electronics’ Romi robot chassis.

The MSP432 is supported by Code Composer Studio (CCS), which provides C and C++ compilers. I built one of the robots and programmed it using the applications highlighted in a very nice set of labs and training sessions developed by TI.

Ada/SPARK Support

As it turns out, the problem can be approached in three ways. One is to simply provide access to the peripherals, and there are quite a few. AdaCore, a major Ada/SPARK compiler vendor, has a program that takes the CMSIS definition file for the MSP432 and kicks out an Ada header file. This, in theory, provides definitions for accessing all of the registers on the chip. The challenge is that the definitions aren’t necessarily easy to use, since much of the information that would be brought to you by the symbols are actually found in comments. Translating this large amount of code was going to be very time-consuming.

The next way is to recode the TI’s driver library (driverlib). That’s a good bit of source code and it would really help to have the CMSIS support translated first.

The last choice was to take advantage of another MSP432 feature: driverlib in ROM. In theory, this should not be too hard. It’s primarily generating procedure and function templates for the matching ROM procedure and functions. That was relatively easy, but most of the arguments for the C functions in ROM use arguments that are defined with types like uint32_t and uint_fast8_t.

Unfortunately, this open-ended argument usage doesn’t take advantage of Ada/SPARK’s strength. In particular, most of the arguments have a much more limited scope. Here’s an excerpt from the general-purpose IO (GPIO) section.

type ROM_GPIOTABLE is
     record
      setAsOutputPin : access procedure ( 
                              selectedPort : GPIO_PORT ;
                              selectedPins : GPIO_PINS ) ;
         setOutputHighOnPin : access procedure (
                              selectedPort : GPIO_PORT ;
                              selectedPins : GPIO_PINS ) ;
     end record
        with Contention => C ;

The GPIO_PORT and GPIO_PINS types were originally uint_fast8_t and unint_fast16_t C types. The reason for changing these is the GPIO_PORT is only supposed to be a limited number of options with unpredictable results if the values are invalid.

The C definitions for the parameters look like this:

   #define GPIO_PORT_P1 1
   #define GPIO_PORT_P2 2
   #define GPIO_PORT_P3 3
   #define GPIO_PORT_P4 4
   #define GPIO_PORT_P5 5
   #define GPIO_PORT_P6 6
   #define GPIO_PORT_P7 7
   #define GPIO_PORT_P8 8
   #define GPIO_PORT_P9 9
   #define GPIO_PORT_P10 10
   #define GPIO_PORT_P11 11

The Ada/SPARK definition is a bit longer:

   type GPIO_Port is (
             GPIO_PORT_P1,
             GPIO_PORT_P2,
             GPIO_PORT_P3,
             GPIO_PORT_P4,
             GPIO_PORT_P5,
             GPIO_PORT_P6,
             GPIO_PORT_P7,
             GPIO_PORT_P8,
             GPIO_PORT_P9,
             GPIO_PORT_P10,
             GPIO_PORT_P11
             );

   for GPIO_Port'Size use uint_fast8_t'Size;

   for GPIO_Port use ( 
            GPIO_PORT_P1 => 1,
            GPIO_PORT_P2 => 2,
            GPIO_PORT_P3 => 3,
            GPIO_PORT_P4 => 4,
            GPIO_PORT_P5 => 5,
            GPIO_PORT_P6 => 6,
            GPIO_PORT_P7 => 7,
            GPIO_PORT_P8 => 8,
            GPIO_PORT_P9 => 9,
            GPIO_PORT_P10 => 10,
            GPIO_PORT_P11 => 11
            );

The definition is longer for two reasons. First, the second section is used to set the enumerated names to specific values. The size definition indicates that the enumerated values fit in a specific space.

One may argue that the verbose aspects of Ada/SPARK are an impediment, but the adding checking that the compiler does is well worth the effort. For example, if one should forget the order of parameters and swap the pin and port definitions, then it would be caught by Ada/SPARK but not by C/C++. Likewise, the C/C++ defined constants could be used anywhere while the Ada/SPARK enumerated constants can only be used where a matching type is used as in the arguments to the functions.

The strict interpretation that Ada/SPARK follows can pick out errors that might otherwise be overlooked. For example, the driverlib ROM definition I worked off of had a uint8_t argument and a matching function that returned this type, but the value that was supposed to be used in these spots was 16#0800#, which requires a 16-bit value. It should have been defined using unit16_t.

This usually isn’t an issue with C implementation because the function arguments are passed in 32-bit registers as are the results. The compiler isn’t checking for these types of errors, but it could cause problems if data is moved to and from packed records where a byte would be used for a uint8_t value.

Bit-Mapped Registers

Most of the configuration records used with the ROM routines have values that map to byte or word boundaries. However, some bit fields match the type of bit fields needed for many peripheral registers.

Typically, C programmers provide #define constants for values that can be ORed together. This results in function calls that look like this:

    C_Set_Port_Example ( Port1, Bit_Field1_1 | Bit_Field2_3 | 32 ) ;

This is simple, but the #define values don’t really describe what bits are involved. There’s no additional checking either. For example, the last value in the OR section is 32. If the field for this value is only 4 bits and the maximum value is 15, then the use of 32 is an error. Still, the compiler would not catch the error. The problem could be masked because the bit from this value may match one of the other values in the equation. Then again, it could cause a major problem because an unintended bit is set.

Ada/SPARK allows bit-mapped fields to be defined as records. It might look something like this:

    type MyBitFields is
      record
        Bit_Field1 : Integer range 0 .. 3 ;
        Bit_Field2 : Integer range 0 .. 7 ;
        Value : Integer range 0 .. 63;
      end record ;

    Ada_Set_Port_Example ( Port1, ( Bit_Field1 => 1, Bit_Field2 => 3, Value => 32 )) ;

The second argument to the function would be the MyBitFields type. There would be an additional set of definitions to specify the size and placement of the fields at the bit level if desired, but that would just complicate the example.

On the flip side, the compiler will be checking the field values to make sure that the values used are within the specified range. Likewise, it would construct the value efficiently. This value would fit into a 16-bit slot, so it would be a 16-bit constant that would be akin to the matching constant used in the C example.

In addition, the compiler will be checking the constant values at compile time. It can also check assignments done at run-time. This type of checking could be added to a C program, and probably should, but such checking must be done explicitly.

Run-time checking can be turned off in Ada/SPARK using pragmas; I actually did this with the jump table. The ROM driverlib uses two levels of indirection. There’s a table where each entry points to a table with a set of jump vectors that point to the actual routines in ROM.

Normally, Ada/SPARK would check that each pointer reference was not null before using the value. That’s not necessary in this case, because the ROM never changes and the ROM values are set up properly on every chip. Turning off the normal compile time checks required definitions like this:

   -- Jump table definition

   type ROM_ADC14 is
     record
       enableModule : access procedure ;
       disableModule : access function return bool ;

       -- more definitions here
     end record

     with Convention => C ;

   -- Jump table definition

   type ROM_ADC14_Access is access constant ROM_ADC14;

   pragma Suppress (Access_Check, On => ROM_ADC14_Access);  

   -- Jump table definition

   type ROM is
      record
         version : uint32_t ;
         ADC14 : ROM_ADC14 ;

        -- more definitions here

      end

        with Convention => C ;

The overhead for using the ROM is the same now regardless of whether C or Ada/SPARK is used. The added benefit of the latter is the ability to take advantage of Ada/SPARK’s superior development. A programmer will be able to take advantage of this BSP and know that the arguments used in calling the routines will be checked rather than hoping the right values are provided.

Work in Progress

The Ada for the C++ or Java Developer section on learn.adacore.com is a good place to find out how Ada/SPARK words with records and bit fields.

As noted, this is still a work in progress. There are over a dozen modules with about a dozen functions per module that need to be defined and checked. I have done about 20 so far. Eventually this will be added to the GitHub site.