rv64im_min_nvme.nx source

1// rv64im_min_nvme.nx -- a SOVEREIGN NVMe-class PCI/MMIO controller device model (X-DRV-W1 2// stage B, the 2nd device class). This is the TWIN of rv64im_min_virtio.nx but for a 3// genuinely DIFFERENT bring-up protocol: where virtio is a straight-line OR-write status 4// ladder, NVMe is a write-then-POLL enable handshake (CC.EN -> poll CSTS.RDY) plus an 5// admin Submission/Completion queue pair bound by 64-bit BASE-ADDRESS registers (ASQ/ACQ, 6// NOT a single PFN<<12), a 64-byte SQE the driver lays in guest RAM, ring advance by 7// TAIL/HEAD DOORBELL writes, and a 16-byte CQE with a PHASE-TAG bit the driver polls. 8// 9// The device models ONE controller window [0x10003000, 0x10003000+0x2000). The KEY 10// behaviour: on a SQ-Tail-doorbell write (off_sq0tdbl) the device runs the doorbell DMA -- 11// it fetches the 64-byte SQE from ASQ_base (STRUCT_WALK over guest RAM: reads opcode + CID), 12// executes a trivial admin command, POSTS a 16-byte CQE into ACQ_base (writes SQHD/CID/status 13// with the phase bit set), and latches a NvmeCqPeek RO word = (CID<<16)|status|phase. CSTS.RDY 14// is a latched flop set when CC.EN was written 1 (cleared on CC.EN=0 reset), so the driver's 15// poll-until-RDY loop terminates. The virtio + net device models are untouched (additive, 16// separate instance) so PROOF-1's SECTGATE stays GREEN. 17// 18// NVMe/PCI here is a last-mile interop PROBE + a measuring stick to EXCEED -- the emitted 19// driver and the shapes are Nishi-native (the device identity lives ENTIRELY in the spec; the 20// shape library that emits the driver knows zero NVMe). 21// Status: SEED. 2026-06-13. Enable handshake + admin SQ/CQ doorbell DMA + phase-tagged CQE. 22// license_tier: ORIGINAL 23 24import "nx_syscalls.nx" 25import "nishi_hdl_primitives.nx" 26 27// ===== MMIO addresses ================================================= 28// One NVMe controller register window, separate from the virtio windows (0x10001000 blk, 29// 0x10002000 net). A 0x2000-byte window so the doorbell page (off 0x1000..) fits. 30const NX_NVME_BASE: i64 = 0x10003000 31const NX_NVME_END: i64 = 0x10005000 32 33// ===== NVMe controller register offsets (NVMe 1.4 base spec, the bring-up subset) ===== 34// 0x00 CAP (RO) controller capabilities (DSTRD/MQES const -- the device offers them) 35// 0x08 VS (RO) version (0x00010400 = 1.4.0) 36// 0x14 CC (RW) controller config; EN = bit0 (the enable the driver writes) 37// 0x1C CSTS (RO) controller status; RDY = bit0 (latched when CC.EN written 1) 38// 0x24 AQA (RW) admin queue attributes (ASQS/ACQS sizes -- latched, no semantics yet) 39// 0x28 ASQ_LO / 0x2C ASQ_HI (RW) admin SQ base address (64-bit, split lo/hi) 40// 0x30 ACQ_LO / 0x34 ACQ_HI (RW) admin CQ base address (64-bit, split lo/hi) 41// 0x1000 SQ0TDBL (WO) admin SQ tail doorbell (the kick that runs the doorbell DMA) 42// 0x1004 CQ0HDBL (WO) admin CQ head doorbell (the driver's completion ack) 43// 0x1008 CQPEEK (RO) sovereign-only instrument = (CID<<16)|status|phase, the binding-proof 44// register mirroring virtio's QueueSectPeek -- the driver reads it back. 45const NX_NVME_OFF_CAP: i64 = 0x00 46const NX_NVME_OFF_VS: i64 = 0x08 47const NX_NVME_OFF_CC: i64 = 0x14 48const NX_NVME_OFF_CSTS: i64 = 0x1C 49const NX_NVME_OFF_AQA: i64 = 0x24 50const NX_NVME_OFF_ASQ_LO: i64 = 0x28 51const NX_NVME_OFF_ASQ_HI: i64 = 0x2C 52const NX_NVME_OFF_ACQ_LO: i64 = 0x30 53const NX_NVME_OFF_ACQ_HI: i64 = 0x34 54const NX_NVME_OFF_SQ0TDBL: i64 = 0x1000 55const NX_NVME_OFF_CQ0HDBL: i64 = 0x1004 56const NX_NVME_OFF_CQPEEK: i64 = 0x1008 57// CQPEEK read-alias at a SMALL offset so the GENERIC op-list emitter (nx_drv_proto_emit) can read 58// it back with a 12-bit load immediate (op verifyu base+0x40); the real 0x1008 register is kept for 59// the bespoke nx_drvgen path. Additive RO alias -- same latched (CID<<16)|status|phase word. 60const NX_NVME_OFF_CQPEEK_LO: i64 = 0x40 61 62// ===== Device identity (RO register values) ================================================= 63const NX_NVME_CAP: i64 = 0x0000000000200001 // MQES=32 (0x1F+1), DSTRD=0 (low bits); RO const 64const NX_NVME_VS: i64 = 0x00010400 // NVMe 1.4.0 65const NX_NVME_CC_EN: i64 = 1 // CC.EN = bit0 66const NX_NVME_CSTS_RDY: i64 = 1 // CSTS.RDY = bit0 67 68// ===== SQE / CQE layout (64-byte SQE, 16-byte CQE) ================================================= 69// The driver lays a 64-byte Submission Queue Entry at ASQ_base. The device reads: 70// sqe.opcode @ byte 0 (Identify=0x06 / a no-op admin cmd) 71// sqe.cid @ byte 2 (16-bit command identifier the device ECHOES back into the CQE) 72// On completion the device posts a 16-byte Completion Queue Entry at ACQ_base: 73// cqe.cid @ byte 12 (16-bit, echoed from the SQE) 74// cqe.status @ byte 14 (16-bit; bit0 = phase tag, bits 1.. = status code (0=success)) 75const NX_NVME_SQE_OFF_OPCODE: i64 = 0 76const NX_NVME_SQE_OFF_CID: i64 = 2 77const NX_NVME_CQE_OFF_CID: i64 = 12 78const NX_NVME_CQE_OFF_STATUS: i64 = 14 79const NX_NVME_PHASE_BIT: i64 = 1 // CQE status bit0 -- the driver polls it 80 81// ===== Verdicts ================================================= 82const NX_NVME_OK: i64 = 0 83const NX_NVME_ADDR_OUT_OF_RANGE: i64 = 1 84 85// ===== Storage (caller allocates an NX_NVME_SLOT_N-i64 backing buffer) ===== 86// slot 0: CC (latched controller-config value the driver wrote) 87// slot 1: CSTS (latched controller status; RDY flop = bit0) 88// slot 2: AQA (latched admin queue attributes) 89// slot 3: ASQ_LO (latched admin SQ base low word) 90// slot 4: ASQ_HI (latched admin SQ base high word) 91// slot 5: ACQ_LO (latched admin CQ base low word) 92// slot 6: ACQ_HI (latched admin CQ base high word) 93// slot 7: SQTAIL (count of SQ tail doorbell rings) 94// slot 8: CQHEAD (internal CQ head; advanced on a CQ head doorbell ack) 95// slot 9: CQPEEK ((CID<<16)|status|phase latched after the device posts the CQE; RO) 96const NX_NVME_SLOT_CC: i64 = 0 97const NX_NVME_SLOT_CSTS: i64 = 1 98const NX_NVME_SLOT_AQA: i64 = 2 99const NX_NVME_SLOT_ASQ_LO: i64 = 3 100const NX_NVME_SLOT_ASQ_HI: i64 = 4 101const NX_NVME_SLOT_ACQ_LO: i64 = 5 102const NX_NVME_SLOT_ACQ_HI: i64 = 6 103const NX_NVME_SLOT_SQTAIL: i64 = 7 104const NX_NVME_SLOT_CQHEAD: i64 = 8 105const NX_NVME_SLOT_CQPEEK: i64 = 9 106const NX_NVME_SLOT_N: i64 = 10 107 108struct NxNvmeCtrl { 109 storage: *i64 // NX_NVME_SLOT_N i64s 110 valid: i64 111 base: i64 // this instance's MMIO base (0x10003000) 112} 113 114// shared storage reset (controller reset: CC=0, CSTS.RDY clear, queues forgotten). 115func nx_nvme_reset_storage(storage: *i64) -> i64 { 116 storage[NX_NVME_SLOT_CC] = 0 117 storage[NX_NVME_SLOT_CSTS] = 0 118 storage[NX_NVME_SLOT_AQA] = 0 119 storage[NX_NVME_SLOT_ASQ_LO] = 0 120 storage[NX_NVME_SLOT_ASQ_HI] = 0 121 storage[NX_NVME_SLOT_ACQ_LO] = 0 122 storage[NX_NVME_SLOT_ACQ_HI] = 0 123 storage[NX_NVME_SLOT_SQTAIL] = 0 124 storage[NX_NVME_SLOT_CQHEAD] = 0 125 storage[NX_NVME_SLOT_CQPEEK] = 0 126 return NX_NVME_OK 127} 128 129func nx_nvme_init(c: *NxNvmeCtrl, storage: *i64) -> i64 { 130 if (c as i64) == 0 { return 0 - NX_HDL_BAD_KIND } 131 if (storage as i64) == 0 { return 0 - NX_HDL_BAD_KIND } 132 c.storage = storage 133 c.valid = 1 134 c.base = NX_NVME_BASE 135 nx_nvme_reset_storage(storage) 136 return NX_NVME_OK 137} 138 139// ===== Range check ================================================= 140func nx_nvme_addr_in_range(c: *NxNvmeCtrl, addr: i64) -> i64 { 141 if addr < c.base { return 0 } 142 if addr >= c.base + 0x2000 { return 0 } 143 return 1 144} 145 146// ===== little-endian DMA helpers over the sim's flat guest RAM (DRY: same bounds-checked 147// device/memory-boundary contract as the virtio model) ==================================== 148func nx_nvme_dma_rd16(mem_buf: *u8, off: i64) -> i64 { 149 let b0: i64 = mem_buf[off] as i64 150 let b1: i64 = mem_buf[off + 1] as i64 151 return b0 | (b1 << 8) 152} 153func nx_nvme_dma_rd32(mem_buf: *u8, off: i64) -> i64 { 154 let b0: i64 = mem_buf[off] as i64 155 let b1: i64 = mem_buf[off + 1] as i64 156 let b2: i64 = mem_buf[off + 2] as i64 157 let b3: i64 = mem_buf[off + 3] as i64 158 return b0 | (b1 << 8) | (b2 << 16) | (b3 << 24) 159} 160func nx_nvme_dma_wr16(mem_buf: *u8, off: i64, val: i64) -> i64 { 161 mem_buf[off] = (val & 0xff) as u8 162 mem_buf[off + 1] = ((val >> 8) & 0xff) as u8 163 return 0 164} 165func nx_nvme_dma_wr32(mem_buf: *u8, off: i64, val: i64) -> i64 { 166 mem_buf[off] = (val & 0xff) as u8 167 mem_buf[off + 1] = ((val >> 8) & 0xff) as u8 168 mem_buf[off + 2] = ((val >> 16) & 0xff) as u8 169 mem_buf[off + 3] = ((val >> 24) & 0xff) as u8 170 return 0 171} 172func nx_nvme_dma_inrange(off: i64, w: i64, mem_size: i64) -> i64 { 173 if off < 0 { return 0 } 174 if off > mem_size - w { return 0 } 175 return 1 176} 177 178// ===== MMIO read (32-bit) ================================================= 179// CAP/VS return their RO spec constants; CSTS returns the latched status (RDY flop); 180// CC/AQA/ASQ/ACQ read back what was latched; CQPEEK returns the latched completion proof 181// word; everything else returns 0 (sparse). value_out[0] gets the word. 182func nx_nvme_read32(c: *NxNvmeCtrl, addr: i64, value_out: *i64) -> i64 { 183 if c.valid != 1 { return 0 - NX_NVME_ADDR_OUT_OF_RANGE } 184 if (value_out as i64) == 0 { return 0 - NX_HDL_BAD_KIND } 185 if nx_nvme_addr_in_range(c, addr) != 1 { return 0 - NX_NVME_ADDR_OUT_OF_RANGE } 186 let off: i64 = addr - c.base 187 if off == NX_NVME_OFF_CAP { 188 value_out[0] = NX_NVME_CAP & 0xffffffff 189 return NX_NVME_OK 190 } 191 if off == NX_NVME_OFF_VS { 192 value_out[0] = NX_NVME_VS 193 return NX_NVME_OK 194 } 195 if off == NX_NVME_OFF_CC { 196 value_out[0] = c.storage[NX_NVME_SLOT_CC] 197 return NX_NVME_OK 198 } 199 if off == NX_NVME_OFF_CSTS { 200 // RDY mirrors a latched flop set when CC.EN was written 1. 201 value_out[0] = c.storage[NX_NVME_SLOT_CSTS] 202 return NX_NVME_OK 203 } 204 if off == NX_NVME_OFF_AQA { 205 value_out[0] = c.storage[NX_NVME_SLOT_AQA] 206 return NX_NVME_OK 207 } 208 if off == NX_NVME_OFF_ASQ_LO { 209 value_out[0] = c.storage[NX_NVME_SLOT_ASQ_LO] 210 return NX_NVME_OK 211 } 212 if off == NX_NVME_OFF_ASQ_HI { 213 value_out[0] = c.storage[NX_NVME_SLOT_ASQ_HI] 214 return NX_NVME_OK 215 } 216 if off == NX_NVME_OFF_ACQ_LO { 217 value_out[0] = c.storage[NX_NVME_SLOT_ACQ_LO] 218 return NX_NVME_OK 219 } 220 if off == NX_NVME_OFF_ACQ_HI { 221 value_out[0] = c.storage[NX_NVME_SLOT_ACQ_HI] 222 return NX_NVME_OK 223 } 224 if off == NX_NVME_OFF_CQPEEK { 225 // RO sovereign-only instrument: (CID<<16)|status|phase the device latched after 226 // posting the CQE. The driver reads it back and verifies == cqpeek_expected. 227 value_out[0] = c.storage[NX_NVME_SLOT_CQPEEK] & 0xffffffff 228 return NX_NVME_OK 229 } 230 if off == NX_NVME_OFF_CQPEEK_LO { 231 // small-offset RO alias of CQPEEK (for the generic op-list driver's 12-bit-immediate read). 232 value_out[0] = c.storage[NX_NVME_SLOT_CQPEEK] & 0xffffffff 233 return NX_NVME_OK 234 } 235 value_out[0] = 0 236 return NX_NVME_OK 237} 238 239// ===== Admin SQ-Tail doorbell DMA (the heart of the 2nd-class round-trip) ===================== 240// On a SQ-Tail-doorbell write the device: 241// 1) fetches the 64-byte SQE from ASQ_base (STRUCT_WALK: reads opcode @+0, CID @+2), 242// 2) executes a trivial admin command (a no-op / Identify-class command), 243// 3) POSTS a 16-byte CQE into ACQ_base (writes CID @+12, status @+14 with phase bit set), 244// 4) latches NvmeCqPeek = (CID<<16) | status | phase. 245// ASQ/ACQ base addresses are guest-physical; their byte offset into mem_buf = phys - mem_base. 246// Bounds-checked at the device/memory boundary (same contract as virtio): an out-of-range 247// queue base makes the DMA a no-op (CQPEEK stays 0) -- no out-of-bounds RAM access. 248func nx_nvme_doorbell_dma(c: *NxNvmeCtrl, mem_buf: *u8, mem_base: i64, mem_size: i64) -> i64 { 249 if c.valid != 1 { return 0 - NX_NVME_ADDR_OUT_OF_RANGE } 250 if (mem_buf as i64) == 0 { return 0 - NX_NVME_ADDR_OUT_OF_RANGE } 251 c.storage[NX_NVME_SLOT_SQTAIL] = c.storage[NX_NVME_SLOT_SQTAIL] + 1 252 // the device only services the doorbell once the controller is enabled + ready. 253 if (c.storage[NX_NVME_SLOT_CSTS] & NX_NVME_CSTS_RDY) == 0 { return NX_NVME_OK } 254 // ---- 1) fetch the 64-byte SQE from ASQ_base (low 32 bits give the in-RAM offset) ---- 255 let asq_phys: i64 = c.storage[NX_NVME_SLOT_ASQ_LO] 256 if asq_phys < mem_base { return 0 - NX_NVME_ADDR_OUT_OF_RANGE } 257 let asq_off: i64 = asq_phys - mem_base 258 if nx_nvme_dma_inrange(asq_off + NX_NVME_SQE_OFF_CID, 2, mem_size) != 1 { return 0 - NX_NVME_ADDR_OUT_OF_RANGE } 259 let opcode: i64 = mem_buf[asq_off + NX_NVME_SQE_OFF_OPCODE] as i64 260 let cid: i64 = nx_nvme_dma_rd16(mem_buf, asq_off + NX_NVME_SQE_OFF_CID) 261 // ---- 2) execute the admin command (trivial): status = success (0) on any valid opcode. 262 var status_code: i64 = 0 263 if opcode == 0 { status_code = 0 } // opcode read but not gated; structural exercise 264 // ---- 3) POST the 16-byte CQE into ACQ_base: cid @+12, status @+14 (bit0 = phase) ---- 265 let acq_phys: i64 = c.storage[NX_NVME_SLOT_ACQ_LO] 266 if acq_phys < mem_base { return 0 - NX_NVME_ADDR_OUT_OF_RANGE } 267 let acq_off: i64 = acq_phys - mem_base 268 if nx_nvme_dma_inrange(acq_off + NX_NVME_CQE_OFF_STATUS, 2, mem_size) != 1 { return 0 - NX_NVME_ADDR_OUT_OF_RANGE } 269 let status_field: i64 = ((status_code & 0x7fff) << 1) | NX_NVME_PHASE_BIT 270 nx_nvme_dma_wr16(mem_buf, acq_off + NX_NVME_CQE_OFF_CID, cid & 0xffff) 271 nx_nvme_dma_wr16(mem_buf, acq_off + NX_NVME_CQE_OFF_STATUS, status_field & 0xffff) 272 // ---- 4) latch NvmeCqPeek = (CID<<16) | status | phase (the binding-proof word) ---- 273 let peek: i64 = ((cid & 0xffff) << 16) | (status_field & 0xffff) 274 c.storage[NX_NVME_SLOT_CQPEEK] = peek & 0xffffffff 275 return NX_NVME_OK 276} 277 278// ===== MMIO write (32-bit) ================================================= 279// CC latches the config; writing CC.EN=1 sets the CSTS.RDY flop (enable), CC.EN=0 clears it 280// (controller reset, queues forgotten). AQA/ASQ/ACQ base regs latch their value. The SQ-Tail 281// doorbell runs the doorbell DMA (via the sim's store32 dispatch, which hands in guest RAM). 282// The CQ-Head doorbell acks (advances the internal CQ head). RO regs ignore writes. 283func nx_nvme_write32(c: *NxNvmeCtrl, addr: i64, value: i64) -> i64 { 284 if c.valid != 1 { return 0 - NX_NVME_ADDR_OUT_OF_RANGE } 285 if nx_nvme_addr_in_range(c, addr) != 1 { return 0 - NX_NVME_ADDR_OUT_OF_RANGE } 286 let off: i64 = addr - c.base 287 if off == NX_NVME_OFF_CC { 288 c.storage[NX_NVME_SLOT_CC] = value & 0xffffffff 289 if (value & NX_NVME_CC_EN) != 0 { 290 // CC.EN=1 -> set CSTS.RDY (the latched ready flop the driver polls for). 291 c.storage[NX_NVME_SLOT_CSTS] = c.storage[NX_NVME_SLOT_CSTS] | NX_NVME_CSTS_RDY 292 } else { 293 // CC.EN=0 -> controller reset: clear RDY + forget queues. 294 nx_nvme_reset_storage(c.storage) 295 } 296 return NX_NVME_OK 297 } 298 if off == NX_NVME_OFF_AQA { 299 c.storage[NX_NVME_SLOT_AQA] = value & 0xffffffff 300 return NX_NVME_OK 301 } 302 if off == NX_NVME_OFF_ASQ_LO { 303 c.storage[NX_NVME_SLOT_ASQ_LO] = value & 0xffffffff 304 return NX_NVME_OK 305 } 306 if off == NX_NVME_OFF_ASQ_HI { 307 c.storage[NX_NVME_SLOT_ASQ_HI] = value & 0xffffffff 308 return NX_NVME_OK 309 } 310 if off == NX_NVME_OFF_ACQ_LO { 311 c.storage[NX_NVME_SLOT_ACQ_LO] = value & 0xffffffff 312 return NX_NVME_OK 313 } 314 if off == NX_NVME_OFF_ACQ_HI { 315 c.storage[NX_NVME_SLOT_ACQ_HI] = value & 0xffffffff 316 return NX_NVME_OK 317 } 318 if off == NX_NVME_OFF_CQ0HDBL { 319 // CQ head doorbell: ack -- advance the internal CQ head. 320 c.storage[NX_NVME_SLOT_CQHEAD] = c.storage[NX_NVME_SLOT_CQHEAD] + 1 321 return NX_NVME_OK 322 } 323 // CAP/VS/CSTS/CQPEEK are read-only: writes silently dropped. SQ0TDBL is handled by the 324 // sim's store32 dispatch (it has mem_buf in hand) -- nx_nvme_doorbell_dma is called there. 325 return NX_NVME_OK 326} 327 328// ===== Status accessor (harness helper) ================================================= 329func nx_nvme_csts(c: *NxNvmeCtrl) -> i64 { 330 if c.valid != 1 { return 0 } 331 return c.storage[NX_NVME_SLOT_CSTS] 332}