From b89a969be4b94cb2af29ab71e546926e1727d02f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 06:44:46 +0200 Subject: [PATCH] =?UTF-8?q?feature:=20inter-core=20NavState=20crossing=20o?= =?UTF-8?q?racle=20=E2=80=94=2016xf32=20crosses=20M4->SHMEM->M7=20byte-exa?= =?UTF-8?q?ct=20on=20dual-core=20RT1176=20(TEST-PIX-030,=20REQ-PIX-007)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Proves the payload-fidelity half of REQ-PIX-007: the 3-core partition's sole M7<->M4 crossing is the NavState message (16xf32 = 64B), and it must cross the shared-SRAM ring BYTE-EXACT or the M7 flight core acts on a torn estimator state. Built on the proven dual-core RT1176 model (vehicle/rt1176-dualcore.repl: cpu_m7 + cpu_m4 on the shared sysbus, SHMEM ring @0x20400000, NXP MU doorbell): - nav_producer_m4.S — cpu_m4 writes 16-word NavState to SHMEM, then a READY flag LAST. - nav_consumer_m7.S — cpu_m7 spins on the flag (acquire), copies 16 words to DTCM. - navstate-crossing.robot — asserts ALL 16 DTCM words == producer pattern 0x4E560000+i. - build.sh — regenerates both ELFs (arm-none-eabi); rivet TEST-PIX-030 (verifies REQ-PIX-007, traces DD-025); WIRED into CI renode-smoke. Verified: rivet validate PASS; renode-test 16/16 words byte-exact (Renode 1.16.1). The inter-core IPC foundation the FIRST-FLASH 3-core model needs — distinct from the single-core gust oracle (TEST-PIX-028): this is the cross-core payload crossing. The MU doorbell datapath is separately exercised by the vehicle multinode demo (TEST-PIX-019). Next rung: WIT-type the NavState record (spar codegen) + swap in relay's real estimator NavState when the M4 estimator lowers on-target. RELEASE-WATCH (same tick): no new releases; falcon still 14 skips (AFD-035). No inbound. Co-Authored-By: Claude Opus 4.8 --- .github/workflows/ci.yml | 2 ++ artifacts/phase2-pixhawk.yaml | 29 ++++++++++++++++ hardware/renode/navstate-xcore/build.sh | 12 +++++++ .../renode/navstate-xcore/nav_consumer_m7.S | 29 ++++++++++++++++ .../renode/navstate-xcore/nav_consumer_m7.elf | Bin 0 -> 4748 bytes .../renode/navstate-xcore/nav_consumer_m7.ld | 5 +++ .../renode/navstate-xcore/nav_producer_m4.S | 29 ++++++++++++++++ .../renode/navstate-xcore/nav_producer_m4.elf | Bin 0 -> 4728 bytes .../renode/navstate-xcore/nav_producer_m4.ld | 4 +++ .../navstate-xcore/navstate-crossing.robot | 31 ++++++++++++++++++ 10 files changed, 141 insertions(+) create mode 100755 hardware/renode/navstate-xcore/build.sh create mode 100644 hardware/renode/navstate-xcore/nav_consumer_m7.S create mode 100755 hardware/renode/navstate-xcore/nav_consumer_m7.elf create mode 100644 hardware/renode/navstate-xcore/nav_consumer_m7.ld create mode 100644 hardware/renode/navstate-xcore/nav_producer_m4.S create mode 100755 hardware/renode/navstate-xcore/nav_producer_m4.elf create mode 100644 hardware/renode/navstate-xcore/nav_producer_m4.ld create mode 100644 hardware/renode/navstate-xcore/navstate-crossing.robot diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5fa0f5d..8d1ea88 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -153,6 +153,8 @@ jobs: run: /tmp/renode/renode-test hardware/renode/synth507-brtable/brtable-507.robot - name: gust F100/M3 byte-exact pass-through oracle (REQ-PIX-004 PART-P02, TEST-PIX-028) run: /tmp/renode/renode-test hardware/renode/gust-m3/passthrough-m3.robot + - name: inter-core NavState crossing oracle (REQ-PIX-007, TEST-PIX-030) + run: /tmp/renode/renode-test hardware/renode/navstate-xcore/navstate-crossing.robot # REQ-PIX-018 leg b (TEST-PIX-022) — the DO-333 sound-static-analysis leg of # the V, on the CONSUMED (stripped) falcon wasm: fetch a pinned falcon diff --git a/artifacts/phase2-pixhawk.yaml b/artifacts/phase2-pixhawk.yaml index d957296..1680ecf 100644 --- a/artifacts/phase2-pixhawk.yaml +++ b/artifacts/phase2-pixhawk.yaml @@ -1008,6 +1008,35 @@ artifacts: - type: traces-to target: REQ-PIX-021 + - id: TEST-PIX-030 + type: test-spec + title: Inter-core NavState crossing - the 16xf32 NavState message crosses M4 -> shared SRAM -> M7 byte-exact on the dual-core RT1176 Renode model (REQ-PIX-007) + status: valid + release: v0.9.0 + description: > + hardware/renode/navstate-xcore/ - proves the payload-fidelity half of REQ-PIX-007: the 3-core + partition's sole M7<->M4 crossing is the NavState message (16 x f32 = 64 B, DD-025/PART), and it + must cross the shared-SRAM ring BYTE-EXACT (no corruption, no partial read) or the M7 flight core + acts on a torn estimator state. Built on the proven dual-core RT1176 model + (hardware/renode/vehicle/rt1176-dualcore.repl: cpu_m7 + cpu_m4 on the shared sysbus, SHMEM ring + @0x20400000, full NXP MU doorbell). cpu_m4 (estimator core) writes the 16-word NavState to SHMEM + then publishes a READY flag @0x20400040 LAST (flag-last release order); cpu_m7 (flight core) spins + on the flag (acquire), copies the 16 words to its DTCM @0x20010000. ORACLE (navstate-crossing.robot, + renode-test): asserts ALL 16 DTCM output words == the producer pattern 0x4E560000+i - so the + NavState survived M4 -> shared-SRAM -> M7 bit-for-bit. CONFIRMED GREEN 2026-07-23 (jess local, + Renode 1.16.1; 16/16 words byte-exact). WIRED into .github/workflows/ci.yml renode-smoke job. + Hermetic: committed producer/consumer ELFs (arm-none-eabi, build.sh regenerates; ELF addresses + + the robot are a matched pair). This is the inter-core IPC foundation the FIRST-FLASH 3-core model + needs; the MU doorbell datapath (M4->M7 RR0) is separately exercised by the vehicle multinode demo + (TEST-PIX-019). NEXT RUNG: WIT-type the NavState record (REQ-PIX-007 / spar codegen) + swap the + fixed pattern for relay's real estimator NavState when the M4 estimator lowers on-target. + tags: [phase-2, inter-core, ipc, navstate, shmem, dual-core, rt1176, byte-exact, on-target, ci-gate, oracle, verification, req-pix-007] + links: + - type: verifies + target: REQ-PIX-007 + - type: traces-to + target: DD-025 + - id: REQ-PIX-018 type: requirement title: jess CI gates the falcon wasm with witness (MC/DC branch coverage) + scry (sound abstract interpretation), on the meld-fused core diff --git a/hardware/renode/navstate-xcore/build.sh b/hardware/renode/navstate-xcore/build.sh new file mode 100755 index 0000000..bc93c72 --- /dev/null +++ b/hardware/renode/navstate-xcore/build.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash +# Build the M4 producer + M7 consumer images for the NavState inter-core crossing +# oracle (TEST-PIX-030). Committed ELFs + the robot's addresses are a matched pair. +set -euo pipefail +D="$(cd "$(dirname "$0")" && pwd)" +CC="${CC:-arm-none-eabi-gcc}"; LD="${LD:-arm-none-eabi-ld}" +"$CC" -c -mcpu=cortex-m4 -mthumb "$D/nav_producer_m4.S" -o "$D/nav_producer_m4.o" +"$LD" -T "$D/nav_producer_m4.ld" "$D/nav_producer_m4.o" -o "$D/nav_producer_m4.elf" +"$CC" -c -mcpu=cortex-m7 -mthumb "$D/nav_consumer_m7.S" -o "$D/nav_consumer_m7.o" +"$LD" -T "$D/nav_consumer_m7.ld" "$D/nav_consumer_m7.o" -o "$D/nav_consumer_m7.elf" +rm -f "$D"/*.o +echo "built nav_producer_m4.elf + nav_consumer_m7.elf" diff --git a/hardware/renode/navstate-xcore/nav_consumer_m7.S b/hardware/renode/navstate-xcore/nav_consumer_m7.S new file mode 100644 index 0000000..b7e7b05 --- /dev/null +++ b/hardware/renode/navstate-xcore/nav_consumer_m7.S @@ -0,0 +1,29 @@ +@ NavState consumer (M7 flight core) for the inter-core crossing oracle (REQ-PIX-007, +@ TEST-PIX-030). Polls the READY flag @0x20400040 (acquire), then copies the 16-word +@ NavState message from the SHMEM ring @0x20400000 to its own DTCM output @0x20010000, +@ byte-exact. Vectors/text in ITCM @0x0 (M7 boots here). The robot asserts the DTCM +@ output equals the producer's pattern word[i]=0x4E560000+i — proving the NavState +@ crossed M4->SHMEM->M7 byte-exact over shared SRAM. + .syntax unified + .cpu cortex-m7 + .thumb + .section .vectors, "a" + .word _m7_stack_top + .word reset + 1 + .text + .thumb_func + .global reset +reset: + ldr sp, =_m7_stack_top + ldr r3, =0x20400040 @ READY flag +1: ldr r1, [r3] @ spin until producer publishes (acquire) + cmp r1, #0 + beq 1b + ldr r0, =0x20400000 @ SHMEM NavState src + ldr r4, =0x20010000 @ M7 DTCM output dst + movs r2, #16 +2: ldr r1, [r0], #4 + str r1, [r4], #4 + subs r2, #1 + bne 2b +3: b 3b diff --git a/hardware/renode/navstate-xcore/nav_consumer_m7.elf b/hardware/renode/navstate-xcore/nav_consumer_m7.elf new file mode 100755 index 0000000000000000000000000000000000000000..cf99bab6a8ef17d7e9cdedaec2029f200475ed81 GIT binary patch literal 4748 zcmeHLO-lk%6usk&qe6id1mdD8Tv+7LLeN|(eQZ*a*1<5^fD$$_^ORckm-;F83tG0V zok3LR&X*PuEnB<;@7;UuJ9FR6+0DH>Y9A|#LNQWQCT2OTDwbHmmZEf(4Aje%Aw4*! zJn9kZh`iFw7wSwUqyy3c>40=VIv^d84oC;21JVKMfOJ4QARYJ*4rm7d>p#wnY4)Tr zpzXKm>9f+++xe~TOe-E@DUH{M_a}Z=&1h27AX1DLcCsD2HzZ{pY5KtRgmY8r)JR{> zbaE-weuElL5hxppR16swp;D{}s~Ww0tRao{Je1&jcan!fzWa?Q6!#TC_*)sPczz?u zG=oDP{pre{Sbg`(ACDZ*8r4jfN`guk ITCM .text : { *(.text*) *(.rodata*) } > ITCM } diff --git a/hardware/renode/navstate-xcore/nav_producer_m4.S b/hardware/renode/navstate-xcore/nav_producer_m4.S new file mode 100644 index 0000000..c55e529 --- /dev/null +++ b/hardware/renode/navstate-xcore/nav_producer_m4.S @@ -0,0 +1,29 @@ +@ NavState producer (M4 estimator core, FPv4-SP) for the inter-core crossing oracle +@ (REQ-PIX-007, TEST-PIX-030). Writes the 16-word (64 B) NavState message to the +@ M7<->M4 SHMEM ring @0x20400000, then publishes a READY flag @0x20400040 LAST so the +@ consumer only reads a fully-written message (flag-last release order). Vectors/text +@ in OCRAM @0x20240000 (shared RT1176 sysbus). Pattern word[i]=0x4E560000+i (distinct, +@ "NV"+i) — the oracle asserts the M7 side reproduces it byte-exact. + .syntax unified + .cpu cortex-m4 + .thumb + .section .vectors, "a" + .word _m4_stack_top + .word reset + 1 + .text + .thumb_func + .global reset +reset: + ldr sp, =_m4_stack_top + ldr r0, =0x20400000 @ SHMEM NavState base + movw r1, #0x0000 + movt r1, #0x4E56 @ r1 = 0x4E560000 + movs r2, #16 +1: str r1, [r0], #4 @ publish NavState word i + adds r1, #1 + subs r2, #1 + bne 1b + ldr r0, =0x20400040 @ READY flag, written LAST + movs r1, #1 + str r1, [r0] +2: b 2b diff --git a/hardware/renode/navstate-xcore/nav_producer_m4.elf b/hardware/renode/navstate-xcore/nav_producer_m4.elf new file mode 100755 index 0000000000000000000000000000000000000000..a1e5e22fc909f6b87ea522382eb74c2323d03f03 GIT binary patch literal 4728 zcmeHLJxc>Y5S`6;3Lz>8lERBzAV_i`T$SpAC>93ALhO=Da$t~n;cgSO@~`+~`~mt4 zEN#_7f`$4fn@u8ESX%7B?tI*vna%6+ZugH4gb<`HK^5XGPqyX4w^wl`DD9GkdWEu- znSQ4Nci0vm#_>txs5%G63GHFkl!k3>XFs1BL;^fMLKeU>Nv643sVYum3c$ z9*$qciT6h0{{74^YGPtfa zUCOLvoB0H4zZ>fXL`kI}P;ROpaQ?F+IY+1|DSG`{N2u{ENbuh3tY7C!kKi6bo4EOR zakd8h76*7g-v!L0D}US?MqzK%4Wib-bwaWw**%JaIFN)&E0%uuvL(YIkrUqxq~C#; zk@6Qh8V6k&Mlm^HK$6oqZ92Y`QNJ^iLCo9!W<|hQcTr5>-OyKZORZX=v1hmpJoAwQ zuDXOv&Eg&SBoW@O%muEb6L>vuu~U6K2ks7G8i)7uJe0uYbRKSH6BKJYf!Fg`F2dfq Ll~JhAvjy%Ohbu_C literal 0 HcmV?d00001 diff --git a/hardware/renode/navstate-xcore/nav_producer_m4.ld b/hardware/renode/navstate-xcore/nav_producer_m4.ld new file mode 100644 index 0000000..7fe89ce --- /dev/null +++ b/hardware/renode/navstate-xcore/nav_producer_m4.ld @@ -0,0 +1,4 @@ +MEMORY { OCRAM (rwx) : ORIGIN = 0x20240000, LENGTH = 0x10000 } +ENTRY(reset) +_m4_stack_top = 0x20250000; +SECTIONS { .vectors 0x20240000 : { KEEP(*(.vectors)) } > OCRAM .text : { *(.text*) *(.rodata*) } > OCRAM } diff --git a/hardware/renode/navstate-xcore/navstate-crossing.robot b/hardware/renode/navstate-xcore/navstate-crossing.robot new file mode 100644 index 0000000..3895428 --- /dev/null +++ b/hardware/renode/navstate-xcore/navstate-crossing.robot @@ -0,0 +1,31 @@ +*** Settings *** +Resource ${RENODEKEYWORDS} + +# Hermetic inter-core NavState crossing oracle (REQ-PIX-007, TEST-PIX-030) on the +# dual-core RT1176 model. The 3-core partition's sole M7<->M4 crossing is the NavState +# message (16 x f32 = 64 B). This proves it crosses BYTE-EXACT over the shared-SRAM ring: +# - cpu_m4 (estimator core) writes the 16-word NavState to SHMEM @0x20400000, then +# publishes a READY flag @0x20400040 LAST (flag-last release order). +# - cpu_m7 (flight core) spins on the flag (acquire), then copies the 16 words from +# SHMEM to its own DTCM @0x20010000. +# The robot asserts every DTCM output word == the producer pattern 0x4E560000+i — so the +# NavState survived the M4 -> shared-SRAM -> M7 crossing bit-for-bit (no corruption, no +# partial read). This is the payload-fidelity half of REQ-PIX-007; the MU doorbell +# datapath is separately exercised by the vehicle multinode demo (TEST-PIX-019). +# ELFs are committed; rebuild both together via build.sh if addresses change. + +*** Test Cases *** +NavState crosses M4 -> shared SRAM -> M7 byte-exact (16 x f32) + Execute Command mach create "rt1176" + Execute Command machine LoadPlatformDescription @${CURDIR}/../vehicle/rt1176-dualcore.repl + Execute Command sysbus LoadELF @${CURDIR}/nav_consumer_m7.elf cpu=cpu_m7 + Execute Command sysbus LoadELF @${CURDIR}/nav_producer_m4.elf cpu=cpu_m4 + Execute Command cpu_m7 VectorTableOffset 0x0 + Execute Command cpu_m4 VectorTableOffset 0x20240000 + Execute Command emulation RunFor "0.01" + FOR ${i} IN RANGE 0 16 + ${addr}= Evaluate ${0x20010000} + ${i} * 4 + ${exp}= Evaluate ${0x4E560000} + ${i} + ${got}= Execute Command sysbus ReadDoubleWord ${addr} + Should Be Equal As Integers ${got} ${exp} NavState word ${i} did not cross byte-exact + END