diff --git a/.github/workflows/proof.yml b/.github/workflows/proof.yml index 3e4998ac..c6b9368c 100644 --- a/.github/workflows/proof.yml +++ b/.github/workflows/proof.yml @@ -72,7 +72,7 @@ jobs: with: cross_files: ${{ format('{0}/{1}', env.MESON_CROSS_FILES, 'arm-none-eabi-gcc.ini') }} actions: '["prefetch", "setup"]' - options: '-Dconfig=.config -Ddts=dts/examples/nucleo_u5a5.dts -Ddts-include-dirs=dts -Dwith_proof=true' + options: '-Dconfig=.config -Ddts=dts/examples/nucleo_u5a5_autotest.dts -Ddts-include-dirs=dts -Dwith_proof=true' - name: run framaC run: | why3 config detect diff --git a/dts/examples/nucleo_u5a5.dts b/dts/examples/nucleo_u5a5.dts index b5d797f0..f5b6cb04 100644 --- a/dts/examples/nucleo_u5a5.dts +++ b/dts/examples/nucleo_u5a5.dts @@ -29,32 +29,6 @@ /{ reserved-memory { - shm_autotest_1: memory@2000a000 { - // mappable, dma allowed - reg = <0x2000a000 0x256>; - dma-pool; - outpost,shm; - outpost,label = <0xf00>; - outpost,owner = <0xbabe>; - }; - - shm_autotest_2: memory@2000b000 { - // not mappable, dma allowed - reg = <0x2000b000 0x100>; - outpost,shm; - dma-pool; - outpost,no-map; - outpost,label = <0xf01>; - outpost,owner = <0xbabe>; - }; - - shm_autotest_3: memory@2000b100 { - // mappable, dma refused - reg = <0x2000b100 0x100>; - outpost,shm; - outpost,label = <0xf02>; - outpost,owner = <0xbabe>; - }; }; }; diff --git a/dts/examples/nucleo_u5a5_autotest.dts b/dts/examples/nucleo_u5a5_autotest.dts deleted file mode 120000 index 5b6d9509..00000000 --- a/dts/examples/nucleo_u5a5_autotest.dts +++ /dev/null @@ -1 +0,0 @@ -nucleo_u5a5.dts \ No newline at end of file diff --git a/dts/examples/nucleo_u5a5_autotest.dts b/dts/examples/nucleo_u5a5_autotest.dts new file mode 100644 index 00000000..b5d797f0 --- /dev/null +++ b/dts/examples/nucleo_u5a5_autotest.dts @@ -0,0 +1,207 @@ +/* + * Copyright (c) 2023,Ledger SAS + * + * SPDX-License-Identifier: Apache-2.0 + */ + +/dts-v1/; + +#include +#include +#include + +/{ + chosen { + sentry,debug_stdout = <&usart1>; + }; + + aliases { + pll = &pll1; + }; + + led0: led_0 { + compatible = "gpio-leds"; + outpost,owner = <0xbabe>; + pinctrl-0 = <&led_pc7 &led_pc7>; + status = "disabled"; + }; +}; + +/{ + reserved-memory { + shm_autotest_1: memory@2000a000 { + // mappable, dma allowed + reg = <0x2000a000 0x256>; + dma-pool; + outpost,shm; + outpost,label = <0xf00>; + outpost,owner = <0xbabe>; + }; + + shm_autotest_2: memory@2000b000 { + // not mappable, dma allowed + reg = <0x2000b000 0x100>; + outpost,shm; + dma-pool; + outpost,no-map; + outpost,label = <0xf01>; + outpost,owner = <0xbabe>; + }; + + shm_autotest_3: memory@2000b100 { + // mappable, dma refused + reg = <0x2000b100 0x100>; + outpost,shm; + outpost,label = <0xf02>; + outpost,owner = <0xbabe>; + }; + }; +}; + +&led0 { + status = "okay"; +}; + +&flash0 { + reg = <0x08000000 DT_SIZE_M(4)>; +}; + +&sram0 { + reg = <0x20000000 DT_SIZE_K(2514)>; +}; + +&gpdma1 { + status = "okay"; +}; + +&clk_lsi { + status = "okay"; +}; + +&clk_hsi { + status = "okay"; +}; + +&clk_hse { + status = "okay"; +}; + +&clk_msis { + status = "okay"; +}; + +&pll1 { + status = "okay"; +}; + +&pll3 { + status = "okay"; +}; + +&flash { + wait-state = <4>; /* According to voltage supply and sysclock */ + status = "okay"; +}; + +&i2c1 { + status = "okay"; + outpost,owner = <0xbabe>; + dma-rx = <&gpdma1 13>; + dma-tx = <&gpdma1 12>; +}; + +&rcc { + clocks = <&pll1>; + clock-frequency = ; + bus-prescalers = <0>, <0>, <0>, <0>; + bus-names = "ahb", "apb1", "apb2", "apb3"; + status = "okay"; +}; + +&exti { + events = <26>; + status = "okay"; +}; + +&gpioa { + status = "okay"; +}; + +&gpiob { + status = "okay"; +}; + +&gpioc { + status = "okay"; +}; + +&gpiod { + status = "okay"; +}; + +&gpioe { + status = "okay"; +}; + +&gpiof { + status = "okay"; +}; + +&gpiog { + status = "okay"; +}; + +&usart1{ + status = "okay"; + pinctrl-0 = <&usart1_tx_pa9>, <&usart1_rx_pa10>; +}; + +&lpuart1{ + status = "disabled"; + pinctrl-0 = <&lpuart1_tx>, <&lpuart1_rx>; +}; + +&pinctrl { + usart1_tx_pa9: usart1_tx_pa9 { + pinmux = <&gpioa 9 STM32_DT_PIN_MODE_ALTFUNC(7)>; + pincfg = ; + }; + + usart1_rx_pa10: usart1_rx_pa10 { + pinmux = <&gpioa 10 STM32_DT_PIN_MODE_ALTFUNC(7)>; + pincfg = ; + }; + + lpuart1_tx: lpuart1_tx { + pinmux = <&gpioc 1 STM32_DT_PIN_MODE_ALTFUNC(8)>; + pincfg = ; + }; + + lpuart1_rx: lpuart1_rx { + pinmux = <&gpioc 0 STM32_DT_PIN_MODE_ALTFUNC(8)>; + pincfg = ; + }; + + led_pc7: led_pc7 { + pinmux = <&gpioc 7 STM32_DT_PIN_MODE_OUTPUT>; + pincfg = ; + }; +}; + +&rng { + status = "okay"; +}; + +&syscfg { + status = "okay"; +}; diff --git a/dts/examples/stm32f429i_disc1.dts b/dts/examples/stm32f429i_disc1.dts index fd93fb12..b1de20cb 100644 --- a/dts/examples/stm32f429i_disc1.dts +++ b/dts/examples/stm32f429i_disc1.dts @@ -16,32 +16,6 @@ }; reserved-memory { - shm_autotest_1: memory@2000a000 { - // mappable, dma allowed - reg = <0x2000a000 0x256>; - dma-pool; - outpost,shm; - outpost,label = <0xf00>; - outpost,owner = <0xbabe>; - }; - - shm_autotest_2: memory@2000b000 { - // not mappable, dma allowed - reg = <0x2000b000 0x100>; - outpost,shm; - dma-pool; - outpost,no-map; - outpost,label = <0xf01>; - outpost,owner = <0xbabe>; - }; - - shm_autotest_3: memory@2000b100 { - // mappable, dma refused - reg = <0x2000b100 0x100>; - outpost,shm; - outpost,label = <0xf02>; - outpost,owner = <0xbabe>; - }; }; }; diff --git a/dts/examples/stm32f429i_disc1_autotest.dts b/dts/examples/stm32f429i_disc1_autotest.dts deleted file mode 120000 index 1e23051d..00000000 --- a/dts/examples/stm32f429i_disc1_autotest.dts +++ /dev/null @@ -1 +0,0 @@ -stm32f429i_disc1.dts \ No newline at end of file diff --git a/dts/examples/stm32f429i_disc1_autotest.dts b/dts/examples/stm32f429i_disc1_autotest.dts new file mode 100644 index 00000000..fd93fb12 --- /dev/null +++ b/dts/examples/stm32f429i_disc1_autotest.dts @@ -0,0 +1,160 @@ +/* + * Copyright (c) 2023,Ledger SAS + * + * SPDX-License-Identifier: Apache-2.0 + */ + +/dts-v1/; + +#include +#include +#include + +/{ + chosen { + sentry,debug_stdout = <&usart1>; + }; + + reserved-memory { + shm_autotest_1: memory@2000a000 { + // mappable, dma allowed + reg = <0x2000a000 0x256>; + dma-pool; + outpost,shm; + outpost,label = <0xf00>; + outpost,owner = <0xbabe>; + }; + + shm_autotest_2: memory@2000b000 { + // not mappable, dma allowed + reg = <0x2000b000 0x100>; + outpost,shm; + dma-pool; + outpost,no-map; + outpost,label = <0xf01>; + outpost,owner = <0xbabe>; + }; + + shm_autotest_3: memory@2000b100 { + // mappable, dma refused + reg = <0x2000b100 0x100>; + outpost,shm; + outpost,label = <0xf02>; + outpost,owner = <0xbabe>; + }; + }; +}; + +&clk_lsi { + status = "okay"; +}; + +&clk_hsi { + status = "okay"; +}; + +/* TODO: checks binding, this is our very own property for plls */ +&pll { + vco_m_div = <8>; + vco_n_mul = <144>; + pq_div = <2>, <6>; + clocks = <&clk_hsi>; + status = "okay"; + compatible = "st,stm32f4xx-pll"; +}; + +&flash { + wait-state = <5>; /* According to voltage supply and sysclock */ + status = "okay"; +}; + +&rcc { + clocks = <&pll>; + clock-frequency = ; + bus-prescalers = <0>, <2>, <1>; + bus-names = "ahb", "apb1", "apb2"; + status = "okay"; + + mco1 { + pinctrl-0 = <&rcc_mco1_pa8>; + clockout = <&pll>; /* XXX use reg value from svd */ + prescaler = <5>; + status = "okay"; + }; +}; + +&exti { + events = <22>; + status = "okay"; +}; + +&gpioa { + status = "okay"; +}; + +&gpiob { + status = "okay"; +}; + +&gpioc { + status = "okay"; +}; + +&gpiod { + status = "okay"; +}; + +&gpioe { + status = "okay"; +}; + +&gpiof { + status = "okay"; +}; + +&gpiog { + status = "okay"; +}; + +&pinctrl { + rcc_mco1_pa8: rcc_mco1_pa8 { + pinmux = <&gpioa 8 STM32_DT_PIN_MODE_ALTFUNC(0)>; + pincfg = ; + }; + + rcc_mco2_pc9: rcc_mco2_pc9 { + pinmux = <&gpioc 9 STM32_DT_PIN_MODE_ALTFUNC(0)>; + pincfg = ; + }; + + usart1_tx_pb6: usart1_tx_pb6 { + pinmux = <&gpiob 6 STM32_DT_PIN_MODE_ALTFUNC(7)>; + pincfg = ; + }; + + usart1_rx_pb7: usart1_rx_pb7 { + pinmux = <&gpiob 7 STM32_DT_PIN_MODE_ALTFUNC(7)>; + pincfg = ; + }; +}; + +&usart1 { + status = "okay"; + pinctrl-0 = <&usart1_tx_pb6>, <&usart1_rx_pb7>; +}; + +&rng { + status = "okay"; +}; + +&syscfg { + status = "okay"; +};