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 0000000..cf99bab Binary files /dev/null and b/hardware/renode/navstate-xcore/nav_consumer_m7.elf differ diff --git a/hardware/renode/navstate-xcore/nav_consumer_m7.ld b/hardware/renode/navstate-xcore/nav_consumer_m7.ld new file mode 100644 index 0000000..9ae71a3 --- /dev/null +++ b/hardware/renode/navstate-xcore/nav_consumer_m7.ld @@ -0,0 +1,5 @@ +MEMORY { ITCM (rwx) : ORIGIN = 0x00000000, LENGTH = 0x40000 + DTCM (rwx) : ORIGIN = 0x20000000, LENGTH = 0x40000 } +ENTRY(reset) +_m7_stack_top = 0x20040000; +SECTIONS { .vectors 0x00000000 : { KEEP(*(.vectors)) } > 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 0000000..a1e5e22 Binary files /dev/null and b/hardware/renode/navstate-xcore/nav_producer_m4.elf differ 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