Skip to content

ARMv6-M target (cortex-m0 / cortex-m0plus): no profile exists; 7346 of 13187 instructions in gale's 22 driver objects are ARMv7-M-only #1301

Description

@avrabe

[fathom (gale) — ARMv6-M target request, from real hardware]

What is missing

synth 0.65.0 (varve layer 2026.09.3) offers ARM targets cortex-m3, cortex-m4, cortex-m4f, cortex-m7, cortex-m7dp. There is no ARMv6-M profile (cortex-m0, cortex-m0plus), so a dissolved gust driver cannot run on a Cortex-M0+ part at all.

Why now

gale's shared bench now has a NUCLEO-G031K8 (STM32G031, Cortex-M0+ r0p1, CPUID 0x410cc601, 8 regions of MPU, 64 KB flash, 8 KB SRAM, all measured on the board, gale#397). gale's native-Rust verified core builds for thumbv6m-none-eabi. The dissolved drivers do not, because every object synth emits is ARMv7-M.

Measured: how far the current output is from ARMv6-M

Across the 22 committed benches/gust/drivers/*/…-cm3.o objects (synth --target cortex-m3), counted with arm-none-eabi-objdump -d:

instruction class count legal on ARMv6-M?
16-bit instructions 5514 mostly (only the ARMv6-M Thumb subset)
32-bit, excluding BL 7346 no (ARMv6-M's only 32-bit instructions are BL, MRS, MSR, MRS/MSR, DMB/DSB/ISB and UDF)
of which MOVW/MOVT 1917 no, needs literal pools or shift/add sequences
IT blocks 350 no
UDIV/SDIV 2 no, needs a libcall (__aeabi_uidiv/__aeabi_idiv)
BL 327 yes

For one driver, wdg-thin-cm3.o, the 32-bit set is movw 74, str.w 59, ldr.w 53, movt 32, add.w 25, and.w 15, stmdb 13, ldmia.w 13, sub.w 11, orr.w 7, strb.w 6, ldrb.w 6, cmp.w 2, mov.w 1.

So this is a real backend profile, not a flag: register-offset addressing past the 16-bit immediate ranges, constant materialisation without MOVW/MOVT, conditionals without IT, flag-setting 16-bit data processing (ADDS/SUBS/ANDS…), push/pop instead of STMDB/LDMIA wide forms, and division via EABI helpers.

Proposed scope, and what "done" means

  • --target cortex-m0plus (and cortex-m0, identical for codegen) on the thumb-2 selector path and the --relocatable path gale uses.
  • Kill criterion 1 (static, mechanical): for every function in the output, every instruction decodes in the ARMv6-M instruction set. A disassembler run with an ARMv6-M-only decoder over the object finds zero wide non-BL/MRS/MSR/barrier instructions, zero IT, zero UDIV/SDIV. gale will add this as a CI gate over the 22 drivers as soon as the target exists.
  • Kill criterion 2 (silicon): wdg-thin dissolved for cortex-m0plus arms the real IWDG on the G031K8 and the chip resets (RCC_CSR.IWDGRSTF=1). That is the same two-boot proof gale already passes on F100 silicon.
  • Semantics oracle: the existing spec/differential tests, re-run on the new profile (qemu mps2-an386/microbit M0 machines exist for execution).

gale is the first consumer and can validate on physical Cortex-M0+ hardware immediately.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions