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.
6 posts - 5 participants
Read full topic
Login
