1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
# 36 — GSP device model (in development)
> **Status: in development (2026-10-03, S1 work package).** This page
> documents the `sim/devices/` device model, the versioned
> `sim/profiles/` documents and the real-firmware boot-ladder results. It is
> the companion to `35-GREENEYE-SIMULATOR-DESIGN.md` §3 (Phase S) and
> `06-ACCURACY.md`. Development-only: nothing here authorises GPU hardware,
> kernel modules, mdev, guest access or reboots.
>
> **See also:** `37-SIM-QEMU-LINE.md` (the B0–B2 device model on the frozen
> simulator-vs-QEMU checks) and `40-NEW-VERSION-TRIAGE.md` (one-command triage
> of a new image through this ladder).
## 1. What this is
The device model gives the native RV64 core (`sim/machine.py`) real MMIO
semantics for the windows the real GSP firmware touches while booting, so a
bounded run advances **past the QEMU first fault** with evidence instead of
lenient zero-reads. Modeled devices take precedence over the lenient
device-map/unknown fallback; an access inside a modeled window that the
device does not implement is still reported as unknown (never silently
zeroed). Every modeled register carries an **evidence kind**:
* **header** — a hardware register/field map (offset, width, access type,
field positions, reset/alignment);
* **firmware use** — the disassembled firmware code that reads/writes it;
* **observed access** — the address/width/direction/PC/value sequence seen in
a real run;
* **shim** — reset-time state the real SEC2 booter/host would provide; always
an explicit, session-recorded assumption, never a device claim.
If a window cannot be proven, none of it is modeled and it is listed as an
unknown (§6).
## 2. Architecture
```
sim/profiles/<name>.json versioned profile: windows, chip id, load layout,
│ DMA aperture windows, boot-shim values
▼
sim/devices/__init__.py registry_from_profile(profile, machine)
│
├─ base.py DeviceRegistry: range+size decode, access log,
│ JSON state/snapshot, peek() debugger surface
├─ pmc.py PMC/master block (NV_PMC_BOOT_42 chip ID)
├─ falcon.py falcon block: IRQ, MAILBOX0/1, DEBUGINFO, DMA,
│ FBIF control/transcfg
├─ priscv.py RISC-V-local block: IRQ mask, trace, error regs
├─ timer.py PTIMER (modeled virtual time; opt-in)
├─ csb.py CSB/TRANSCOM message window seam (B3 landing)
├─ fwsec.py WPR2 address pair (FWSEC state unmodeled)
├─ pmu.py PMU stub: observes, never fakes
├─ dma.py aperture → RAM translation seam (FBGPA/SYSGPA)
└─ irq.py falcon + RISC-V-local IRQ aggregation
▼
sim/machine.py Machine(devices=..., translator=..., reset_regs=...)
▼
sim/gsp_boot.py bounded real-firmware run + session + rung
```
`Machine` consults devices after RAM/UART and before the device map/lenient
fallback; the aperture translator (`dma.py`) is consulted first so
FBGPA/SYSGPA memory accesses resolve to RAM. Overlapping device windows
resolve last-registered-first, and a window that does not model an access
defers to the next matching window (safe fallback), so a narrow overlay can
serve some offsets without hiding the wider device. `Machine.device_state()`
and the `greeneye-sim-devices/1` snapshot expose all device state as
serialisable data (snapshot/restore support is additive and not yet wired to
moments).
## 3. Modeled inventory
Offsets are relative to each block base. `RW` semantics are storage unless
noted; every unlisted offset is unhandled and logged.
| Block | Window(s) (PRIV unless noted) | Modeled registers | Evidence |
|---|---|---|---|
| PMC | `+0x0` (size 0x1000) | `BOOT_42` @0xA00: ARCHITECTURE 28:24, IMPLEMENTATION 23:20, MAJOR 19:16, MINOR 15:12, MINOR_EXT 11:8, CHIP_ID 28:20 (TU104 = 0x164), read-only | header + firmware use + observed (first MMIO) |
| Falcon | `+0x110000`, alias `0x300000000` | `IRQSSET` 0x000 (`irq_status \|=`), `IRQSCLR` 0x004 (`&= ~`), `IRQSTAT` 0x008 (read), `MAILBOX0/1` 0x040/0x044, `OS` 0x080, `DEBUGINFO` 0x094, `CPUCTL` 0x100, `BOOTVEC` 0x104, `DMACTL` 0x10c, `DMATRFBASE` 0x110, `DMATRFMOFFS` 0x114, `DMATRFCMD` 0x118 (transfer on write), `DMATRFFBOFFS` 0x11c, `DMATRFBASE1` 0x128, `FBIF_TRANSCFG(0..7)` 0x600, `FBIF_CTL` 0x624 | header + firmware use + observed |
| RISC-V local | `+0x111000`, alias `0x300001000` | `IRQMSET` 0x2ac, `IRQMCLR` 0x2b0, `IRQMASK` 0x2b4 (read), `IRQDEST` 0x2b8, `IRQTYPE` 0x2bc, `TRACECTL` 0x344, `TRACE_RDIDX` 0x348, `TRACE_WTIDX` 0x34c, `PRIV_ERR_STAT` 0x360, `PRIV_ERR_INFO` 0x364 (read), `PRIV_ERR_ADDR` 0x368 (read), `HUB_ERR_STAT` 0x36c | header + observed |
| PTIMER | `+0x9000` | `TIME_0` aperture 0x9400 / block `+0x400` (NSEC 31:5), `TIME_1` aperture 0x9410 / block `+0x410` (NSEC 28:0); value = instruction count × `ns_per_insn` (**modeled**, not calibrated) | header + **modeled** time |
| WPR2 | `+0x1FA000` | `WPR2_ADDR_LO` 0x1FA824, `WPR2_ADDR_HI` 0x1FA828 (4 KiB alignment; HI points at the last 128 KiB block) | header + firmware use |
| CSB/TRANSCOM | profile-declared | none by default; a profile may declare individual registers with width/value and `rw`/`ro`/`wo`/`w1c`/`set`/`clear` semantics | none yet (B3 landing point) |
| PMU | profile-declared | none; the stub records accesses and returns unhandled | none yet |
| DMA seam | FBGPA/SYSGPA (profile) | GPU-physical → RAM windows for falcon DMA and aperture loads/stores; unmapped transfers are refused and recorded | address-map header + firmware use |
Falcon DMA follows the header field semantics: `size = 1 << (SIZE+2)`,
`IMEM`/`DMEM` aperture select, `WRITE` direction, address
`((BASE1<<32 | BASE) << 8) + FBOFFS`, `IDLE` set on success and `ERROR` on a
refused transfer. Which FB/SYS aperture a DMA address targets (the
`FBIF_TRANSCFG.TARGET` decode) is **not proven yet** and is listed in §6.
### 3.1 Boot shim (declared assumptions)
The firmware's `_start` consumes boot arguments the real SEC2 booter/host
writes; the simulator reconstructs them from the documented structure layout
and records each as an assumption in `session.json.boot_shim.assumptions`:
* `NV_RISCV_BOOT_PARAMS` at a RAM address (bootType `NVRM`, size 120,
version 1, core-dump buffer, one `WPRM` libos init arg);
* a `GspFwWprMeta` (magic/revision/verified and a self-consistent FB layout);
* raw-image mirror at the DMEM aperture base so the app's own relocation copy
is self-consistent (it is not: see §6);
* `a0`–`a5` register arguments (bootargs PA/VA, ELF PA/size, load base, WPR
id).
The DEBUGINFO **host-consume** behaviour is also a shim: the firmware writes a
boot-stage marker and polls bits 22:20 until they clear, and no self-clearing
path exists in the firmware, so the host side is modelled as consuming the
stage marker on read. The device never changes a read value except for this
documented shim, and the shim is profile-enabled and session-recorded.
## 4. Boot ladder results (observed, 2026-10-03)
| Rung | Claim | Evidence |
|---|---|---|
| **B0** | flat image loads; first MMIO is the unmodelled PMC `BOOT_42` read at `0x2000_0000_0000_0A00` | `tests/test_sim_devices.py` (B0 classification) |
| **B1** | device model serves the whole boot path: **0 unknown MMIO, 0 unhandled in windows**, deterministic 2M-instruction run stopping at the boot-halt/report loop (`0x4010928`) | `run_boot(use_shim=False)`; sessions `dumps/gsp-boot-b1-run1`, `dumps/gsp-boot-b1-run2`; test `test_no_shim_b1_device_model_serves_boot` |
| **B2** | with the shim, the firmware passes the chip gate, MPU/vector setup, the bootargs consumer (`0x4007A30`) and reaches its **relocation copy** (`0x4007B7C`), then stops at a known unknown (DMEM runspace) | sessions `dumps/gsp-boot-b2-run1`, `dumps/gsp-boot-b2-run2`; test `test_shim_reaches_relocation_b2` |
Reproduction (read-only; no hardware):
```bash
cd open-iov/debug/risc-v-gsp-rm-vm
python3 -m sim.gsp_boot --instructions 2000000 --record dumps/gsp-boot-b2-run1
python3 -m unittest tests.test_sim_devices -v
```
Two-run determinism is asserted by `test_two_runs_identical` and was checked
at the recorded B2 sessions: identical instruction count (14 682), stop
reason/PC (`fault @ 0x400EA0C`), device-state SHA-256
(`3fa264b9…`) and register file. The B1 no-shim run is likewise identical
across runs (2 000 000 instructions, budget stop at `0x4010928`, device-state
SHA-256 `88eb07b7…`).
## 5. Session evidence
Each `run_boot` invocation writes a `greeneye-session/1` directory with:
* `session.json` — firmware SHA-256, profile name, load layout, rung,
milestones, stop reason/PC, unknown-MMIO counts, device-state SHA-256,
device-access counts and the full boot-shim assumption list;
* `blobs/device-state.json` — the `greeneye-sim-devices/1` snapshot of every
device (registers, IRQ state, DMA windows/counters, shim flags);
* `events.jsonl` — the normal session event stream (`gsp_boot` note).
## 6. Unknowns (explicitly not modeled / not verified)
1. **DMEM runspace content.** The app's relocation copy reads the DMEM
aperture (`0x1_0000_0000+`) and writes it to the `0x400E000` runtime
region; the bootloader-provided content is not reconstructed, so the copy
writes zeros and the run stops at `0x400EA0C` (illegal instruction). This
is the B2 ceiling today.
2. **CSB/TRANSCOM register semantics.** No message-window poll has been
observed yet, so no register is modeled. B3 waits for the first observed
poll; the `csb.py` seam and profile register declarations are in place.
3. **PMU.** No PMU register access observed; stub only.
4. **FWSEC state machine.** Only the WPR2 address pair is modeled; FWSEC
execution is not.
5. **DMA aperture selection.** `FBIF_TRANSCFG.TARGET`/`MEM_TYPE` decode is
not proven; only the profile's DMA windows decide what an address means.
6. **Interrupt delivery.** Falcon/RISC-V IRQ state is aggregated and
serialisable, but mstatus/mie/mip/mtvec trap entry and interrupt injection
are not modelled.
7. **PTIMER calibration.** Values are modeled from the instruction count with
a placeholder `ns_per_insn`; no firmware PTIMER read has been observed and
no timing claim is made.
8. **MPU translation.** The firmware programs its MPU CSRs (observed), but
the machine does not enforce translations; the libos private mapping is
served by explicit device aliases and the FBGPA/SYSGPA seam, not by an MPU
model.
Nothing in this page is a silicon-accuracy claim; `06-ACCURACY.md` fidelity
levels apply (L0/L1 modelled, L2 modelled-not-calibrated, L3 partial and
listed above).
|
