What Firmware Emulation Needs to Get Right

A correct assertion can pass when the model removes the condition that would make it fail.

Consider a team changing a sensor driver. They might check parsing logic in host-side unit tests, boot the firmware against an emulated sensor in CI, and flash a development board to inspect the bus. A normal read can pass in each setup without exercising recovery after a reset halfway through a transaction.

For that recovery test, the important question is which state survives the reset. For other tests, it might be when DMA reads a buffer or when a storage write becomes durable. The hardware model determines which of those conditions the firmware encounters.

Three dimensions of hardware fidelity

We use hardware fidelity to mean preserving the hardware behavior that matters to the check. Three dimensions help explain the examples below:

• Ordering: which accesses can overlap, and when their effects become observable.
• Independence: which components retain state across a particular reset or power transition.
• Persistence: which changes survive an interruption.

These dimensions overlap; they are not a complete classification of hardware behavior. Fidelity also depends on the task. Register behavior may be sufficient for an initialization check, while DMA ownership needs access ordering. Electrical behavior requires a different kind of model. More detail is useful only when it represents the relevant behavior correctly.

The Renode examples below name specific models and source revisions. A simplification can be appropriate for many tests while excluding a failure another test needs to expose.

DMA reads a buffer the CPU has already reused

A nonblocking transmit API starts work without waiting for completion. It does not guarantee that work remains pending when the call returns. For an API that retains the caller’s buffer, unsent data must remain unchanged until ownership returns, as Arm’s USART driver contract specifies.

This illustrative C-like pseudocode assumes DMA-accessible memory and appropriate cache maintenance. Here, dma_start retains tx as its source:

uint8_t tx[8];
fill_packet(tx);
dma_start(tx, sizeof tx);  // DMA retains the source buffer.
prepare_next_packet(tx);  // Reuses it without completion synchronization.

Keep the expected received payload fixed at ABCDEFGH. An eager-copy model consumes the source before the CPU reuses it, so the receiver gets the expected packet.

For a controller configuration that permits outstanding source reads, another ordering is possible: DMA reads ABCD, the CPU replaces the buffer with 12345678, and DMA reads the remaining positions afterward. The receiver gets ABCD5678; the unchanged packet check fails.

Legal orderings depend on transfer width, bursts, FIFO buffering, bus arbitration, and memory visibility. ST’s DMA application note, for example, describes prefetch into a FIFO. A model must respect the selected controller’s constraints, rather than introduce arbitrary interleavings.

In the cited STM32DMA enable path, a memory-to-peripheral transfer invokes a synchronous copy. For an incrementing RAM source, DmaEngine consumes the source before that enable-write callback returns. Delaying only the completion indication would not restore overlap with that CPU’s later writes.

The MCU restarts, but the bus stays stuck

Consider an I²C target holding SDA low during an interrupted transaction. The MCU and its I²C controller reset, but the target stays powered outside that reset domain. The restarted firmware can encounter a bus that is still blocked. TI describes this external-device hang.

MCU reset, controller reset, target reset, and target power cycling are distinct events. A powered target can still have a separate reset input. If a test resets it into an idle state along with the MCU, it can clear the condition on the firmware’s behalf.

The cited STM32F7_I2C model uses transaction callbacks. BUSY and several error fields are tags, rather than consequences of resolved SDA/SCL line state. It implements other outcomes, including NACK for an absent target; that differs from modeling a target holding SDA across reset.

The recovery check should verify fresh, valid communication and any recovery action the requirement specifies. NXP’s bus-clear guidance distinguishes recovery clocks, hardware reset, and power cycling. A retry can be valid where the device behavior permits it; the model must not silently clear the condition. A boot message alone cannot establish recovery.

The update loses the data it needs to recover

An interrupted update can leave a device without a bootable application. Two different mechanisms matter here.

When a completed copy is not yet durable

A buffered write can return while data remains in RAM. An updater that consumes its staging image before the required copies are durable can lose its recovery path.

In this schematic ordering, copy(source, destination) names the image movement:

copy(primary, recovery);
copy(staging, primary);
erase(staging);

Durability barriers make the dependency explicit:

copy(primary, recovery);
flush(recovery);
copy(staging, primary);
flush(primary);
erase(staging);

Here, flush means a successful durability barrier for the relevant storage stack, with guarantees established through its buffering layers and device contract. Error handling is omitted; these lines are not a complete safe-update algorithm.

A NuttX kernel fix addressed an FTL path that ignored O_DIRECT. A related nxboot fix added flush barriers and full-image CRC validation before boot.

Source note: the nxboot author reports that barriers and CRC validation reduced persistent boot failures from 92/94 to 0/94 tested fault points in a Renode campaign on nucleo-h743zi nxboot with FTL write buffering enabled. This is an attributed campaign result, not comprehensive physical-flash validation.

When power interrupts the flash operation

A campaign can interrupt before erase, during erase, after erase but before metadata is committed, during programming, or after programming but before completion is recorded. These are different device and updater states.

The surviving contents must follow the selected device’s documented guarantees or qualified observations. If interruption leaves contents unspecified, a model must not assume that the operation rolled back or invent a convenient partial-write pattern.

The cited STM32F4 flash model erases a sector with a synchronous backing-memory write and has a tagged BSY flag. That path exposes no erase-busy interval or partial-erase state in virtual time.

The NuttX campaign demonstrates that Renode-based interruption between software operations can already expose real defects. Testing interruption inside an erase requires additional operation and interruption semantics.

Validating a hardware model

A more elaborate model can introduce impossible behavior. Validation starts with a particular device, configuration, and test requirement:

• Constrain ordering, reset behavior, and storage guarantees using the device specification.
• Compare relevant observations from equivalent firmware scenarios on hardware and in emulation, with stated timing and measurement limits.
• Test invariants that reject forbidden states or transitions, alongside expected successful behavior.
• Record the conditions covered and the behavior still unqualified.

Vendor drivers and reference implementations can guide tests, but are not substitutes for device behavior. Matching one trace does not qualify every configuration. An unexplained difference needs investigation before the model is used as evidence for that check.

Our approach at Vinaka

Our direction is operation-aware modeling combined with controlled, repeatable experiments. An operation needs more than an eventual completion flag: its outstanding work and intermediate effects must be explicit where a test depends on them.

Three responsibilities follow:

• Operation semantics: define accesses, state changes, and ownership, including intermediate effects.
• Execution scheduling: make those effects observable alongside CPU execution under the controller’s constraints.
• Interruption semantics: apply the appropriate reset, power, or fault behavior to the state reached so far.

For DMA, that means retaining outstanding source accesses when the controller requires them. For reset recovery, it means preserving unaffected components. For storage, it means restarting from the contents that survive the specified interruption.

An illustrative DMA ownership experiment would start a transfer under a configuration that permits outstanding source reads, exercise a legal ordering where the driver reuses the buffer before those reads finish, and compare the received bytes against the expected packet. After correcting ownership handling, rerun with the same inputs and controller configuration.

These are modeling requirements guiding Vinaka’s development, not a statement that every illustrated mechanism is currently implemented or hardware-qualified. Support must be established for the selected device and configuration.

Questions to ask of your model

Use the behavior under test to choose the relevant questions:

The implementation observations here refer to the linked Renode revision cd7f870, not every Renode model or extension. The packet ordering is hypothetical; the NuttX figures are the upstream author’s reported results.

Emulation cannot establish correctness for behavior its model makes impossible. The goal is to preserve the hardware behavior the firmware depends on, and show why the modeled outcomes are valid.