STM32F4.GPIO.Set raises assertion failure about ada_drivers_library HOT 10 CLOSED

On 1/12/2016 2:27 PM, Austin wrote:

When running this test program on an STM32F405:

with Ada.Real_Time; use Ada.Real_Time;
with STM32F4;       use STM32F4;
with STM32F4.GPIO;  use STM32F4.GPIO;
with STM32F40xxx;   use STM32F40xxx;

procedure LEDTest is
    Period     : constant Time_Span := Milliseconds (200);  -- arbitrary
    Next_Start : Time := Clock;
begin
    Configure_IO(Port => GPIO_A, Pin => Pin_8, Config =>
       (Mode         => Mode_Out,
        Output_Type  => Push_Pull,
        Speed        => Speed_2MHz,
        Resistors    => Floating));

    Set(GPIO_A, Pin_8);

    loop
       Clear(GPIO_A, Pin_8);

       Next_Start := Next_Start + Period;
       delay until Next_Start;

       Set(GPIO_A, Pin_8);

       Next_Start := Next_Start + Period;
       delay until Next_Start;
    end loop;
end LEDTest;

I get an assertion failure.

If I place a breakpoint in the system assertion handler (ravenscar-sfp-stm32f4.build/common/s-assert.adb:42), I'm able to extract the assertion message:

(gdb) c
Continuing.

Breakpoint 8, system.assertions.raise_assert_failure (msg=...) at /beuvry.a/gnatmail/sandbox/gnat-7.4.0/arm-elf-linux/recompilablerts/src/bb-runtimes/obj/ravenscar-sfp-stm32f4.build/common/s-assert.adb:42
42    in /beuvry.a/gnatmail/sandbox/gnat-7.4.0/arm-elf-linux/recompilablerts/src/bb-runtimes/obj/ravenscar-sfp-stm32f4.build/common/s-assert.adb
(gdb) print Msg
$5 = "failed postcondition from stm32f4-gpio.ads:131"

It looks like that postcondition is checking that the corresponding bit is set in the input register, but I'm not sure if the state of the output register actually affects the state of the input register.

Thoughts?

Yes, I agree. That implementation expectation is not supported by the
STM RM (RM0090). I ran into this a couple of nights ago and have
removed the postconditions on all such routines (ie procedures Set,
Clear, and Toggle), but have not yet pushed it.

I'll likely push the change tonight.

Best regards,

Pat

Patrick Rogers, PhD
AdaCore Senior Technical Staff
[email protected]
+1 646 375 0739 office
+1 646 358 3289 fax

Experience Ada 2012 in GNAT Pro today: www.adacore.com

from ada_drivers_library.

Thanks!

from ada_drivers_library.

I've removed the post functions in my local copy of stm32-gpio.ads and confirmed that it no longer throws this assertion.

from ada_drivers_library.

On 1/12/2016 3:12 PM, Austin wrote:

I've removed the post functions in my local copy of stm32-gpio.ads and confirmed that it no longer throws this assertion.

Great, thanks for the confirmation.

Best regards,

Pat Rogers

Patrick Rogers, PhD
AdaCore Senior Technical Staff
[email protected]
+1 646 375 0739 office
+1 646 358 3289 fax

Experience Ada 2012 in GNAT Pro today: www.adacore.com

from ada_drivers_library.

My LEDs still didn't light up, even with the post conditions disabled, so I kept debugging.

I enabled the clock for GPIOA, put the post conditions back, and now the LED blinks and the post conditions pass.

from ada_drivers_library.

Looking at the STM32F405 datasheet, I think the IDR should reflect the state of the ODR register, but only if the pin is in the output state, and only if the clock for that port is enabled. Should those be additional preconditions for Set/Clear/Toggle?

from ada_drivers_library.

It's essentially the same effect, but I would express it the other way round: The IDR always*) reflects the state of the I/O pin. That happens to correspond to the state of the ODR if and only if the pin is configured as output.
The clock for a GPIO port (or any other peripheral) has to be enabled before any access to a register. The peripheral in question is not working at all without clock.

*) with one exception: The input buffer ('TTL Schmitt trigger' in the schematic) is disabled when the pin is configured as analog I/O.

Anyway, I am pretty sure I don't want that data written to a output is always read back just to verify that it's really written. GPIO operations are often more or less time-critical. Normally, I trust the µC that 'it does that right'. If I really have to check that there is the correct level on the pin, I would program this check explicitly.

Regards,

Matthias

from ada_drivers_library.

On 1/13/2016 12:37 PM, Matthias Richter wrote:

It's essentially the same effect, but I would express it the other
way round: The IDR always*) reflects the state of the I/O pin. That
happens to correspond to the state of the ODR if and only if the pin
is configured as output. The clock for a GPIO port (or any other
peripheral) has to be enabled before any access to a register. The
peripheral in question is not working at all without clock.

*) with one exception: The input buffer ('TTL Schmitt trigger' in the
schematic) is disabled when the pin is configured as analog I/O.

Anyway, I am pretty sure I don't want that data written to a output
is always read back just to verify that it's really written. GPIO
operations are often more or less time-critical. Normally, I trust
the µC that 'it does that right'. If I really have to check that
there is the correct level on the pin, I would program this check
explicitly.

Agreed, those postconditions are gone now.

from ada_drivers_library.

Sounds like a good solution to me.

from ada_drivers_library.

from ada_drivers_library.