Unusual hardware register behavior

General
1

On the RP2040, each GPIO pin can trigger four different interrupts: high level, low level, rising edge, and falling edge. Each pin has a 4-bit field for selecting which of these interrupts is enabled. I modeled it as an array of records.

with System;

procedure Main is
    type INT_Field is record
        Low_Level, High_Level, Falling_Edge, Rising_Edge : Boolean := False;
    end record
        with Size => 4;
    for INT_Field use record
        Low_Level    at 0 range 0 .. 0;
        High_Level   at 0 range 1 .. 1;
        Falling_Edge at 0 range 2 .. 2;
        Rising_Edge  at 0 range 3 .. 3;
    end record;

    type GPIO_Pin is range 0 .. 30;
    type INT_Register is array (GPIO_Pin) of INT_Field
        with Component_Size => 4;

    type GPIO_Peripheral is record
        INTE : INT_Register; --  Write to enable interrupts
        INTS : INT_Register; --  Masked status of enabled interrupts
        INTR : INT_Register; --  Unmasked interrupt status, write to clear
    end record;

    GPIO : GPIO_Peripheral
        with Import, Address => System'To_Address (16#4001_40F0#);
begin
    GPIO.INTE (7).Rising_Edge := True;
end Main;

I’m simplifying things a bit here for clarity. You can find the actual implementation on GitHub

On the surface, this looks like it should work. Compiling with GNAT, this results in a strb (Store Byte) instruction after shifting some bits around.

Now this is where the bug comes in… The RP2040 datasheet explains:

2.1.4. Narrow IO Register Writes

Memory-mapped IO registers on RP2040 ignore the width of bus read/write accesses. They treat all writes as though they were 32 bits in size. This means software can not use byte or halfword writes to modify part of an IO register: any write to an address where the 30 address MSBs match the register address will affect the contents of the entire register.

By “affect the contents of the entire register,” it means that an 8-bit write to a 32-bit register will change all of the bytes of the register to the same value.

If our register value is 16#0000_0000# and the strb instruction is setting bit 8 so that we have 16#0000_0100#, the resulting value is 16#0101_0101# instead.

My solution is to add another array to group fields into 32-bit array elements, so that we can use the Volatile_Full_Access aspect to guarantee that the whole word is written using the str instruction.

    type INT_Register is array (0 .. 7) of INT_Field
        with Volatile_Full_Access, Component_Size => 4, Size => 32;

    type INT_Group is array (0 .. 3) of INT_Register
        with Component_Size => 32;

This solution works, but has left me wondering how we can prevent this from happening again in the future. This is not the first bug I’ve encountered caused by the narrow write behavior of the I/O memory.

I have a few questions for discussion:

  • Is there a way to tell the compiler that a memory range only supports writes of a specific size?
  • If not, can we at least generate a warning?
  • SPARK has the Async_Writers aspect, which indicates that some external process can modify the register value. If we were to verify this code, it seems like every register would need this aspect due to this narrow write behavior.
  • Philosophically, is it possible to make any guarantees about the software without access to the hardware HDL sources? It seems like there’s a bit too much human error possible in the process of writing and interpreting documentation about hardware behavior.
2

The problem with

    type GPIO_Pin is range 0 .. 30;
    type INT_Register is array (GPIO_Pin) of INT_Field
        with Component_Size => 4;

is that it is a “virtual” modeling.
Very appealing from programmer’s perspective but not modeling the actual way the hardware works.

I myself wondered many times how this problem could be smartly modeled (in C or in Ada) but never found an answer.

3

Volatile_Full_Access was introduced specifically for this case. I don’t know if other approaches can work, the compiler has to know what to do with the other bytes of the register.

4

How does the compiler knows which size to use for the underlining registers ?

5

I would assume from Size => 32?

As far as the CPU is concerned it is just one big memory space with even bit access instructions though an MPU may be consulted for again overlayed permissions.

6

The Datasheet clearly defines each array of 8 INT_Fields as a distinct 32-bit register, with its own address, so I think we have to model that.

That said, there appears to be a GCC 12 compiler bug around your revised INT_Register to do with it being an array of records. More investigation needed.

1 Like