Add Renode emulation tests for Cortex-M4F and Cortex-M33#3
Merged
Conversation
Replaces the build-only multi-arch workflow with actual Renode emulation tests. Builds Zephyr+Gale semaphore test for STM32F4 (M4F) and STM32L552/Nucleo (M33), then runs Robot Framework tests via renode-run to verify PROJECT EXECUTION SUCCESSFUL on the emulated hardware. Complements QEMU-based zephyr-tests.yml (M3) with hardware-accurate emulation of the remaining ARM architectures. M3 removed from this workflow to avoid duplication. Also fixes README CI table: Zephyr tests 13→20 suites (Phase 3 modules were added), Multi-Arch Build → Renode Emulation Tests. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Two Verus constructs were not being stripped from exec function bodies:
1. Inline `proof { ... }` blocks — appear inside if/else branches to
carry bit-vector assertions alongside runtime code. Stripped by
detecting Ident("proof") + Group(Brace) (distinct from `proof fn`
which try_skip_verus_item already handles).
2. `let ghost x = ...;` — ghost variable declarations used only in
loop invariants. Stripped by detecting Ident("let") + Ident("ghost")
and consuming through the semicolon.
Regenerate plain/src/*.rs with the fixed verus-strip. Gate test and
cargo test --workspace both pass.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Tests test_strip_inline_proof_block and test_strip_let_ghost verify that the two new verus-strip cases work correctly and prevent future regressions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ackage renode-run is not a real PyPI package. Use direct download of the Renode 1.15.0 dotnet portable from GitHub releases instead. Installs robotframework separately via pip3. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Previously the gate only checked plain/src/*.rs (verus-strip output). The standalone plain/*.rs files (used by rocq_of_rust for theorem proving) had no automated sync check. Adds plain_standalone_matches_stripped_standalone test that verifies all 9 plain/*.rs files match verus-strip --standalone output from src/. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Remove unused is_impl_or_mod_body and skip_clause_simple functions. Remove unused keyword variable in verus clause stripping. Zero warnings in cargo build. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The ghcr.io/zephyrproject-rtos/ci:v0.29.0 Docker image includes Renode 1.16.0 pre-installed at /opt/renode (already in PATH). No download step needed — just install Robot Framework. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
renode-test in Renode 1.16.0 (pre-installed in Zephyr CI Docker image)
does not support --variable or --outputdir flags. Fix by:
- Using %{ELF} (Robot Framework env-var syntax) instead of ${ELF} variable
- Setting ELF as an env var in the workflow step
- Running renode-test from the output directory so results land there
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Renode monitor commands require the @ prefix for file paths. Without it, Renode fails to tokenize the path. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
STM32L552 (nucleo_l552ze_q) emulation hangs in Renode 1.16.0 — the stm32l552.repl is a CPU-only file without proper peripheral emulation, causing Zephyr clock init to stall indefinitely. MPS2/AN521 is the ARM reference Cortex-M33 board with full Renode support (mps2-an521.repl), simple peripheral set, and no TrustZone complexity. Add timeout-minutes: 30 to prevent silent CI hangs. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Need to find what M33 platform files exist in Renode 1.16.0 (mps2-an521.repl not found, stm32l552.repl hangs). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The stm32l552.repl CPU file lacks proper peripheral emulation (RCC/clock). Use the dedicated test platform from Renode 1.16.0: tests/platforms/nucleo_l552ze_q/nucleo_l552ze_q_ns.repl which has complete peripheral support for the Nucleo L552 board in non-secure mode. Also remove the debug file-listing step. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Documents the three test targets as SW architecture decisions so Kiln and Synth can reference them: - SWARCH-TGT-001: QEMU Cortex-M3 (Zephyr integration tests, 20 suites) - SWARCH-TGT-002: STM32F4 Discovery (Renode M4F emulation) - SWARCH-TGT-003: STM32L552 Nucleo (Renode M33 emulation) SWREQ-KILN-003 now links to TGT-002 and TGT-003 via verified-on so Synth codegen requirements can trace to the validation platforms. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
renode-tests.ymlfrom a build-only workflow to actual Renode emulation testsrenode-runto verifyPROJECT EXECUTION SUCCESSFULon the emulated hardwarezephyr-tests.ymlvia QEMU)Test plan
stm32f4_discoELF and passes Robot Framework testnucleo_l552ze_qELF and passes Robot Framework test🤖 Generated with Claude Code