Raspberry Pi Pico board contract (Phase 4)

The third microcontroller, and the first on the Cortex-M engine. One kernel component (pico in crates/parts) wraps an RP2040 SoC model (crates/rp2040) built on the Cortex-M core (crates/cortexm-core, Profile::V6M, proven in proofs/cortexm/REPORT.md). Firmware is a Thumb ELF that talks to the peripherals below at their real RP2040 addresses, so a program built for Mokxi runs on a real Pico.

The catalog type is pico (Raspberry Pi Pico, RP2040). Three agents build against this file: the SoC and part (Rust), the firmware runtime and examples (C++, clang for thumbv6m-none-eabi), the board visual (TypeScript). Change it only by editing this file first. Everything in docs/esp32c3.md about how a board part behaves (slices, host channel, reset, crash line) applies here unless this file says otherwise.

Running binaries built with the Raspberry Pi Pico SDK is not a goal for Phase 4: the SDK's crt0 expects the second-stage bootloader, the clock tree, the XOSC and the PLLs, and none of those are modeled. What is modeled is the set of peripherals pinMode, digitalWrite, digitalRead, analogWrite, millis, micros, delay, Serial and attachInterrupt need, at their real addresses, so the same source built against firmware/pico/ produces an image that also runs on the hardware.

1. Board pins (catalog order)

The 40-pin header, top view with the USB connector at the top. The left column is physical pins 1..20 read downwards; the right column is physical pins 40..21 read downwards, which is how the pins line up when the board is held that way.

Left column (pins 1..20): GP0, GP1, GND, GP2, GP3, GP4, GP5, GNDb, GP6, GP7, GP8, GP9, GNDc, GP10, GP11, GP12, GP13, GNDd, GP14, GP15.

Right column (pins 40..21): VBUS, VSYS, GNDe, 3V3_EN, 3V3, ADC_VREF, GP28, AGND, GP27, GP26, RUN, GP22, GNDf, GP21, GP20, GP19, GP18, GNDg, GP17, GP16.

40 pins. Duplicate names carry a letter suffix because catalog pin names are unique; the board silkscreens GND on all seven and AGND on pin 33. The three test points (TP1..TP6) and the SWD header are not pins.

Electrical:

• 3V3 drives 3.3 V at R_SUPPLY and every GND* and AGND drives 0 V at R_SUPPLY. VBUS drives 5 V at R_SUPPLY and VSYS drives 4.7 V (5 V through the Schottky diode the board has between them), because the board is always USB powered. ADC_VREF drives 3.3 V through 200 R, which is the filtered reference the board brings out. The board is a supply for the rest of the circuit.
• 3V3_EN is an input with a 100 k pull-up to VSYS; pulling it below 1.2 V turns the regulator off, which halts the chip and releases every pad. That is the only thing it does here.
• RUN is an input with a 50 k internal pull-up to 3.3 V; driven below 1.65 V it holds the CPU in reset, and releasing it restarts from the vector table.
• GP0..GP22, GP26..GP28 are inout GPIO. Output enabled (SIO.GPIO_OE bit set and the function select is SIO or PWM): push-pull at 3.3 V or 0 V through R_STRONG. Output disabled: high-Z, plus a 55 k pull-up to 3.3 V when PADS_BANK0.GPIOn.PUE is set, a 55 k pull-down when PDE is set (both set is a bus-keeper, modeled as high-Z). Input reads the net voltage against 1.65 V; Unknown and Floating both read 0 with no error, as on the ESP32-C3. PADS_BANK0.GPIOn.OD disables the output driver whatever the selected peripheral asks for, and IE clear makes the input read 0. An RP2040 pad has no open-drain mode; a driver that wants one drives low and goes to input for high.
• GP23, GP24 and GP25 exist in the model but are not on the header, as on the real board: GP23 is the SMPS power-save control, GP24 is VBUS sense (reads 1, because the model is always USB powered) and GP25 is the on-board green LED. The LED is shown from a probe bit (section 5), and the pad carries a 1 k load to ground so the volts are honest.
• GP26, GP27 and GP28 are ADC0..ADC2 on the real part. The ADC is not modeled in Phase 4 (section 6); they are plain GPIO here and ADC_VREF and AGND are a supply and a ground.
• GP0/GP1 are UART0 TX/RX on the real board. Here UART0 talks to the host channel (section 4) and the two pads stay GPIO, exactly as docs/esp32c3.md does it.

2. Memory map (real RP2040 addresses)

region	address	size	notes
ROM	0x0000_0000	16 KB	not modeled: reads 0, writes ignored, counted
XIP flash	0x1000_0000	up to 2 MB	the program image; read-only to the core
SRAM (striped)	0x2000_0000	256 KB	SRAM0..SRAM3, four banks word-interleaved
SRAM4	0x2004_0000	4 KB
SRAM5	0x2004_1000	4 KB
RESETS	0x4000_C000	4 KB	section 3.1
IO_BANK0	0x4001_4000	4 KB	section 3.2
PADS_BANK0	0x4001_C000	4 KB	section 3.3
UART0	0x4003_4000	4 KB	section 3.5
PWM	0x4005_0000	4 KB	section 3.6
TIMER	0x4005_4000	4 KB	section 3.4
SIO	0xD000_0000	4 KB (not APB)	section 3.7
PPB	0xE000_0000	1 MB	SysTick, NVIC and the SCB, inside the core

SRAM is 264 KB and contiguous from 0x2000_0000 to 0x2004_2000. The striping of SRAM0..SRAM3 is an arbitration detail with no software-visible effect at one core, so the model is one flat array; 0x2100_0000 and 0x2110_0000, the non-striped aliases of the same banks, are not mapped, and neither is the 0x4002_0000 XIP cache-maintenance window. Anything outside a mapped region is a bus fault, which on ARMv6-M escalates to HardFault; the part counts faults and reports a crash (section 5). An unimplemented register inside a mapped block reads 0 and ignores writes, with a counter for diagnostics.

Every APB peripheral block is also aliased at +0x1000 (atomic XOR), +0x2000 (atomic set) and +0x3000 (atomic clear), which is how RP2040 firmware sets one bit without a read-modify-write. The model implements all three for every peripheral it implements. SIO is not an APB block and has no aliases, as on the chip.

Firmware ELF. loadProgram takes an ELF32 little-endian ARM executable (e_machine 40). Every PT_LOAD segment must fall inside XIP flash or SRAM; .data is loaded at its p_paddr (in flash) and the runtime's crt0 copies it down, as on the hardware. There is no second-stage bootloader: the model does not require, execute or checksum a boot2 block, and a 256-byte .boot2 section in the image is simply loaded and never run. Reset takes the vector table at the lowest loaded flash address: VTOR is set there, SP_main comes from word 0 and the entry point from word 1, exactly as the processor does out of reset. The ELF's e_entry is not used; a vector table is required. A load at run time resets the board.

3. Peripheral registers (subset, real offsets, real bit positions)

Registers are 32 bits and word aligned. Byte and halfword access to a peripheral register is unsupported (a read returns the aligned word narrowed, a write writes the whole word from the narrow value); firmware must not do it. SRAM and flash take every width.

3.1 RESETS (0x4000_C000)

offset	name	bits
0x00	RESET	1 = block held in reset
0x04	WDSEL	stored, read back
0x08	RESET_DONE	1 = block out of reset and ready

Bit numbering is the datasheet's: 5 io_bank0, 8 pads_bank0, 14 pwm, 21 timer, 22 uart0, 23 uart1. RESET_DONE is the inverse of RESET, with no delay: a block comes out of reset the instant its bit is cleared, so the usual while (!(resets_hw->reset_done & bits)) loop falls straight through. Out of reset every block here reads its power-on values; holding a block in reset returns it to them, and while io_bank0 or pads_bank0 is held every pad is high-Z. Blocks the model does not implement accept their bits and report done.

3.2 IO_BANK0 (0x4001_4000)

offset	name	bits
0x00 + 8n	GPIOn_STATUS	bit 8 OUTTOPAD, bit 13 OETOPAD, bit 17 INFROMPAD, read-only
0x04 + 8n	GPIOn_CTRL	bits 4..0 FUNCSEL, 9..8 OUTOVER, 13..12 OEOVER, 17..16 INOVER
0x0F0 + 4m	INTRm	raw interrupt for GPIOs 8m..8m+7, four bits each
0x100 + 4m	PROC0_INTEm	enable, same layout
0x110 + 4m	PROC0_INTFm	force, same layout
0x120 + 4m	PROC0_INTSm	raw AND enable, OR force

FUNCSEL: 4 = PWM, 5 = SIO, 31 = NULL (the pad is released). Everything else (SPI 1, UART 2, I2C 3, PIO0 6, PIO1 7, clocks 8, USB 9) is accepted, stored and read back, but leaves the pad released, because those peripherals are not modeled. Power-on value is 31 on every pin, as on the chip, so firmware has to select SIO before a pad does anything, and firmware/pico/ does.

OUTOVER/OEOVER: 0 = the peripheral's signal, 1 = inverted, 2 = drive low (OEOVER 2 = disable), 3 = drive high (OEOVER 3 = enable). INOVER is the same four for the input.

The four interrupt bits per GPIO are 0 LEVEL_LOW, 1 LEVEL_HIGH, 2 EDGE_LOW, 3 EDGE_HIGH. Edge bits latch and are cleared by writing 1 to them in INTRm; level bits follow the pad and cannot be cleared. Any bit set in a PROC0_INTSm raises IO_IRQ_BANK0 (IRQ 13).

3.3 PADS_BANK0 (0x4001_C000)

offset	name	bits
0x00	VOLTAGE_SELECT	stored, read back
0x04 + 4n	GPIOn	0 SLEWFAST, 1 SCHMITT, 2 PDE, 3 PUE, 4..5 DRIVE, 6 IE, 7 OD

Power-on is IE clear, PUE clear, PDE set, SCHMITT set, DRIVE = 1 (4 mA) on every pad, as the datasheet gives it. IE clear makes the input read 0 whatever the net is doing; OD set releases the pad whatever the selected peripheral asks for; DRIVE and SLEWFAST are stored and read back but do not change the source impedance, which is always R_STRONG.

3.4 TIMER (0x4005_4000)

A 64-bit microsecond counter and four 32-bit alarms. This is the part's clock: micros() and millis() read it and delay() sleeps on an alarm.

offset	name	bits
0x00 0x04	TIMEHW TIMELW	write-only, latched write of the whole counter
0x08	TIMEHR	high word, latched by the last TIMELR read
0x0C	TIMELR	low word; reading it latches the high word into TIMEHR
0x10 + 4n	ALARMn	n = 0..3; writing arms it, writing also clears its INTR bit
0x20	ARMED	bit n = alarm n armed; write 1 to disarm
0x24 0x28	TIMERAWH TIMERAWL	the counter with no latching
0x2C	DBGPAUSE	stored, read back
0x30	PAUSE	bit 0 stops the counter
0x34	INTR	bit n = alarm n fired; write 1 to clear
0x38 0x3C 0x40	INTE INTF INTS	enable, force, and raw AND enable OR force

The counter is derived from kernel time: microseconds = (now_ps - origin_ps) / 1_000_000, with the origin fixed at the first slice. It never drifts from the circuit. An alarm fires when the low 32 bits of the counter reach the armed value, disarms itself and sets its INTR bit; INTS bit n raises TIMER_IRQ_n (IRQ 0..3). Writing an alarm also clears its INTR bit. The comparator only ever sees the low 32 bits, so an alarm armed at a value that has just gone by does not fire for 71.6 minutes, exactly as on the hardware, and why firmware/pico/ re-reads the clock after arming and before it parks.

3.5 UART0 (0x4003_4000)

A PL011. This is the host channel; the pads are not involved.

offset	name	bits
0x00	UARTDR	write: transmit; read: receive (low 8 bits, error bits read 0)
0x04	UARTRSR	reads 0
0x18	UARTFR	3 BUSY, 4 RXFE, 5 TXFF, 6 RXFF, 7 TXFE
0x24 0x28	UARTIBRD UARTFBRD	baud = 125 MHz / (16 (IBRD + FBRD/64)); stored and used for TX pacing
0x2C	UARTLCR_H	stored; bit 4 FEN enables the FIFOs (clearing it flushes them)
0x30	UARTCR	0 UARTEN, 8 TXE, 9 RXE
0x34	UARTIFLS	stored, read back
0x38	UARTIMSC	4 RXIM, 5 TXIM, 6 RTIM
0x3C 0x40	UARTRIS UARTMIS	raw and masked interrupt status
0x44	UARTICR	write 1 to clear
0x48	UARTDMACR	stored, read back

Both FIFOs are 32 entries, as on the chip, and one entry deep with FEN clear. TX bytes leave the FIFO into the host channel at the configured baud (an unprogrammed divisor falls back to 115200: one byte, ten bits, every 86.8 us) and BUSY is set while any byte is still going out; a write to a full TX FIFO is dropped, which is what the hardware does. RX bytes arrive from the host channel instantly. RXRIS is raised while the RX FIFO is at or above its trigger level (half, the UARTIFLS reset value, so 16 entries) and RTRIS whenever RX has anything at all and no byte has arrived for 32 bit times, so a driver that waits on either sees a single typed character. Any bit set in UARTMIS raises UART0_IRQ (IRQ 20). UART1 is not modeled and its block is unmapped.

Behind the receive FIFO is a 256-byte host backlog, which is not hardware: it drains into the FIFO as the program empties it, so pasting a line into the serial monitor while the sketch is between Serial.read() calls does not lose characters. The Uno model has the same thing for the same reason. A backlog that is also full drops, as a real overrun would.

3.6 PWM (0x4005_0000)

Eight slices, two channels each. GPIO n is channel A of slice (n / 2) % 8 when n is even and channel B when it is odd, so GP25, the on-board LED, is slice 4 channel B.

offset	name	bits
0x00 + 0x14 s	CHs_CSR	0 EN, 1 PH_CORRECT, 2 A_INV, 3 B_INV, 5..4 DIVMODE, 6 PH_RET, 7 PH_ADV
0x04 + 0x14 s	CHs_DIV	11..4 integer, 3..0 fraction: the counter steps once per DIV/16 system clocks
0x08 + 0x14 s	CHs_CTR	the counter, 16 bits; writable
0x0C + 0x14 s	CHs_CC	15..0 channel A compare, 31..16 channel B
0x10 + 0x14 s	CHs_TOP	15..0 wrap value; reset 0xFFFF
0xA0	EN	bit s enables slice s, the same bit as its CSR.EN
0xA4 0xA8 0xAC 0xB0	INTR INTE INTF INTS	wrap interrupt per slice

A channel's output is high while CTR < CC and low from CTR == CC to the wrap, so CC = 0 is always low and CC > TOP is always high. That is why analogWrite(pin, 255) sets CC to TOP + 1 rather than to TOP. A_INV and B_INV invert the output. The output reaches the pad whenever that GPIO's FUNCSEL is 4: the PWM block asserts the pad's output enable itself, so selecting the function is all a program has to do, and SIO.GPIO_OE is not consulted.

DIVMODE 0 (free-running) is modeled. Modes 1..3 count gated by or triggered from the B pin, which needs an input the model does not route, so they are accepted and stored but count as free-running. PH_CORRECT is not modeled: a slice with it set counts trailing-edge anyway, which halves its period. Any bit set in INTS raises PWM_IRQ_WRAP (IRQ 4).

3.7 SIO (0xD000_0000)

Single-cycle I/O: the GPIO the core actually writes, plus the hardware divider.

offset	name	bits
0x000	CPUID	reads 0: core 0 is the only core (section 5)
0x004	GPIO_IN	bit n = input level of GPIO n (needs PADS.IE)
0x008	GPIO_HI_IN	the six QSPI pads; reads 0
0x010 0x014 0x018 0x01C	GPIO_OUT _SET _CLR _XOR	output level, bits 0..29
0x020 0x024 0x028 0x02C	GPIO_OE _SET _CLR _XOR	output enable, bits 0..29
0x030..0x04C	GPIO_HI_OUT/_OE and their aliases	stored; no pad
0x050	FIFO_ST	reads 2 (RDY set, VLD clear): core 1 never answers
0x054 0x058	FIFO_WR FIFO_RD	the write is discarded, the read gives 0
0x05C	SPINLOCK_ST	bit n = spinlock n held
0x060..0x078	DIV_UDIVIDEND DIV_UDIVISOR DIV_SDIVIDEND DIV_SDIVISOR DIV_QUOTIENT DIV_REMAINDER DIV_CSR	the hardware divider
0x100 + 4n	SPINLOCKn	read to claim (0 when already held), write to release

The divider completes immediately: a read of DIV_CSR always shows READY (bit 0) set, and DIRTY (bit 1) is set by writing an operand and cleared by reading DIV_REMAINDER. Division by zero gives the hardware's answer (quotient all ones for unsigned, +/-1 for signed by the dividend's sign, remainder the dividend). Reading DIV_QUOTIENT before DIV_REMAINDER is the SDK's order and both are readable in any order here. The interpolators (INTERP0/INTERP1 at 0x080 and 0x0C0) are not modeled: they read 0.

3.8 Interrupts

The NVIC, SysTick and the SCB are inside cortexm-core at their architectural PPB addresses; the bus never sees them. ARMv6-M gives two priority bits and 32 external interrupt lines. The lines this model drives:

IRQ	name	raised by
0..3	TIMER_IRQ_0..3	TIMER.INTS bit n
4	PWM_IRQ_WRAP	PWM.INTS non-zero
13	IO_IRQ_BANK0	any IO_BANK0.PROC0_INTS* non-zero
20	UART0_IRQ	UART0.UARTMIS non-zero

Each is a level, held high while the peripheral's status says so, so a handler that does not clear the source is re-entered, exactly as on the hardware. Every other IRQ number exists in the NVIC and is never raised.

WFI parks the core until any enabled interrupt is pending (section 5). WFE behaves the same, plus the event register the architecture defines; SEV is accepted and sets it.

4. Host channel

host = "utf-8 bytes on UART0". readHost returns UART0 TX bytes as they leave the FIFO at the configured baud; writeHost pushes bytes into the UART0 RX FIFO (overflow drops, as on the chip). The serial monitor shows bytes as text, decoding UTF-8 and treating \n as a line end (\r ignored). Same semantics as the ESP32-C3 channel.

5. Time model and the part

One core at 125 MHz. The SoC runs in slices of 10 us = 1250 cycles, with the core's cycle counter as the clock: cortexm-core charges the datasheet cycle count of every instruction, so simulated time is the cycle count divided by 125 MHz. The cycle counter is anchored to kernel time at the start of every slice, the way the ATmega328P model anchors its own, so a timer can never drift away from the circuit however the slices fall.

The second core is not modeled. SIO.CPUID reads 0, the inter-core FIFO is permanently empty and never ready to read, and there is no way to launch core 1: a program that writes the launch sequence to FIFO_WR and waits for a response waits for ever. proofs/cortexm/REPORT.md measures the one core we do have at 0.85x a real 125 MHz RP2040 in a browser, so a second interpreted core would halve that; it is a Phase 5 decision, not a Phase 4 omission to be papered over. Everything in firmware/pico/ is single core.

Slices, not single steps. Unlike the Uno model, the core is not stepped one instruction at a time: there is no headroom for it. A slice is run in chunks of 128 cycles (1.024 us), which bounds the error on the time stamped on a pin change; several changes inside one chunk keep their order and are spread across it so they never coincide. A chunk is cut short at the exact cycle of the next timed peripheral event (a timer alarm, a PWM edge, a UART byte leaving), so those land on the cycle they belong to and micros() is exact.

Sleep parks. WFI stops the slicing: the part schedules its next wake at the earliest of the armed timer alarms, the next PWM edge on a driven pad and the next UART event, and a pin change or a host byte wakes it immediately. An idle sketch costs the kernel a handful of events a second rather than 125 million cycles, which is the whole reason delay() in the runtime sleeps.

Reads of SIO.GPIO_IN see the pin levels as of the start of the chunk, plus any change the sketch itself made in it.

Probe: a bitmask, 0 with no program.

bit	meaning
1	running (executing, not in reset, not crashed)
2	parked in WFI
4	the on-board LED on GP25 is lit
8	serial transmit in the last 20 ms
16	serial receive in the last 20 ms

Poke: 1 = press BOOTSEL, 0 = release (the model has no bootsel button function: pressing it only lights the visual, because BOOTSEL is read through the QSPI chip-select pad, which is not modeled); 2 = hold RUN low, 3 = release.

Crash handling as in docs/esp32c3.md section 5. On ARMv6-M every fault is a HardFault, and a fault taken at HardFault priority is Lockup, which cortexm-core reports as Trap::Lockup. The part halts on a Trap (a Lockup or a BKPT with no debugger) and prints one line on the host channel:

firmware crashed at pc=0x100002a4, lockup in exception 3

6. What is not modeled

PIO, DMA, the ADC, SPI, I2C, the USB controller, the watchdog, the RTC, the clock tree (CLOCKS, XOSC, PLL_SYS, PLL_USB: the system clock is 125 MHz from reset), the QSPI pads and the flash interface beyond reading the image, the second core, the on-chip ROM and its function table, and the interpolators. Their address blocks are unmapped, so touching one is a bus fault rather than a silent zero. The exceptions are the blocks listed in section 3, where an unimplemented register inside an implemented block reads 0 and is counted.

7. Firmware runtime (firmware/pico/)

A freestanding C and C++ runtime for the RP2040 built with clang 18 (--target=thumbv6m-none-eabi -mcpu=cortex-m0plus -mthumb -Os) and ld.lld, no Pico SDK, no newlib, no libgcc or compiler-rt, nothing GPL:

• crt0.S: the vector table (16 system entries plus 32 IRQs), Reset_Handler (copy .data from flash, clear .bss, run the C++ constructors, call main), and the AEABI helpers a Cortex-M0+ needs because it has no divide instruction and no long multiply: __aeabi_uidiv, __aeabi_uidivmod, __aeabi_idiv, __aeabi_idivmod, __aeabi_lmul, __aeabi_llsr, __aeabi_llsl and the memory helpers.
• link.ld: .text and .rodata in XIP flash at 0x1000_0000, .data and .bss in SRAM at 0x2000_0000, the stack from the top of SRAM (0x2004_2000) down. No boot2.
• include/rp2040.h: the registers of section 3 as macros with their real names.
• include/arduino.h: the same sketch surface as the other two runtimes: pinMode, digitalWrite, digitalRead, analogWrite, delay, delayMicroseconds, millis, micros, shiftOut, attachInterrupt, Serial with begin/print/println/write/available/read/peek, with LED_BUILTIN = 25.
• analogWrite(pin, 0..255) works on every GPIO, because each one has a PWM channel: FUNCSEL goes to 4 and the slice is set to TOP = 32767 with the divider at 3.8125, so the period is 125 MHz / (3.8125 x 32768) = 1000.6 Hz. The CC value is the duty scaled by 128, because the divider is 8.4 fixed point and cannot reach 1 kHz with a 255-count period. 0 and 255 disconnect the PWM and drive the pin low or high, so analogWrite(pin, 0) really is off.
• millis()/micros() read the TIMER, so they are exact and never drift. delay() and a delayMicroseconds() of 50 us or more arm timer alarm 0 and WFI until it fires; shorter waits spin on TIMERAWL.
• attachInterrupt(pin, handler, mode) uses IO_IRQ_BANK0 with RISING, FALLING, CHANGE, ONLOW and ONHIGH mapped to the four INTR bits. digitalPinToInterrupt(pin) is the pin itself: every GPIO has one.

Examples under firmware/pico/examples/<name>/sketch.ino, built to web/public/firmware/pico/<name>.elf with web/public/firmware/pico/index.json in the same shape as the Uno index, each entry carrying "program": "elf32 arm rp2040": blink (GP25), button (GP15 with the internal pull-up lighting GP25), serial (prints millis() once a second and echoes what it receives), fade (PWM on GP25).

The UI picks the firmware list by the part's catalog program string: "elf32 riscv32imc" reads /firmware/index.json, "elf32 avr atmega328p" reads /firmware/uno/index.json, "elf32 arm rp2040" reads /firmware/pico/index.json.

8. What this model is sure of, and what it is not

Three groups, the same sorting docs/esp32c6.md section 7 uses. It exists because a board model that quietly guesses an address is worse than one that says it did not know.

Taken from the data sheet, and run through by real firmware. Every base address, register offset and bit position in sections 2 and 3 is from the RP2040 Datasheet (Raspberry Pi Ltd), including the three atomic aliases at +0x1000, +0x2000 and +0x3000 that make hw_set_bits work. The forty-pin header order in section 1 is the Pico's own. crates/rp2040/tests/firmware.rs loads real ELFs and drives RESETS, IO_BANK0, PADS_BANK0, SIO, TIMER, UART0 and the PWM slices through them.

Modeled, but not held to the data sheet's numbers. Behaviors rather than addresses:

• The core runs in 128-cycle chunks, not one instruction at a time. A chunk is 1.024 us and is cut short at the exact cycle of the next timed peripheral event, so a timer alarm, a PWM edge and a UART byte all land where they belong, but a pin change made by software carries the chunk's rounding and can be up to 1.024 us late. The Uno model stamps every pad change on its exact cycle; this one cannot, because there is no headroom at 125 MHz (proofs/cortexm/REPORT.md: 0.85x real time in a browser).
• The system clock is 125 MHz from reset and never changes. The clock tree is not modeled, so clocks_init, the crystal, both PLLs and any frequency the sketch sets are all ignored and the answer is always 125 MHz. Flash wait states and the XIP cache are not there either, so execute-in-place runs at SRAM speed.
• The pads are three states and a threshold. Push-pull at 3.3 V, high-Z, or a 55 kΩ internal pull (the data sheet gives about 50 kΩ to 80 kΩ), read back against half the supply, with no hysteresis, no drive-strength setting, no slew-rate control, no rise time and no current limit.
• The power pins are numbers rather than a power tree. VSYS is 4.7 V, which is VBUS less the Schottky drop; 3V3_EN is a 100 kΩ pull-up and pulling it below 1.2 V stops the board; RUN is a 50 kΩ pull-up; ADC_VREF is 3.3 V behind 200 Ω. None of the regulator's behavior is modeled, nothing sags and nothing browns out, and VBUS sense on GP24 is simply tied high.
• Startup is a microsecond, with no boot ROM and no second-stage bootloader: the image is placed and run. Holding BOOTSEL is a poke that the model reports; there is no mass-storage device behind it.

Deliberately absent, as section 6 lists: the second core, PIO, DMA, the ADC, SPI, I2C, USB, the watchdog, the RTC, the clock tree, the QSPI pads and the flash interface beyond reading the image, the on-chip ROM and its function table, and the interpolators. Their address blocks are unmapped, so touching one is a bus fault rather than a silent zero. Note what that costs: GP26 to GP28 and ADC_VREF are on the header and in the part, but there is no converter behind them, so analogRead has nothing to read.