nx_fpga_dc.nx source

1// nx_fpga_dc.nx -- LIB: RUNG 30 of the sovereign FPGA-boot sim -- the DISPLAY-CONTROLLER peripheral 2// (an MMIO-mapped framebuffer + scanout). This is the missing rung between the (complete in-sim) RV64IM 3// CPU and a GAME with graphics: the SoC modeled so far has UART text only; this adds pixels. 4// 5// THE HONEST HARDWARE MODEL (what is "real gates" vs what is a memory block): 6// - FRAMEBUFFER STORAGE = a caller-owned memory block of W*H packed-RGB i64 words. In real silicon a 7// framebuffer is BRAM / external DRAM -- a memory block -- NOT a LUT4/DFF fabric (the fabric RAM tops 8// out at 16 words by its single-LUT4 address decode). So modeling storage as a memory block is the 9// FAITHFUL hardware model, not a shortcut. 10// - THE MMIO ADDRESS DECODE runs ON THE FABRIC -- this is the gate-level logic a display controller adds 11// to the bus. It composes the PROVEN nx_fpga_addsub subtractor (rungs R6/R7, gate-verified == the 12// behavioral ALU): for a store address `addr`, 13// idx = addr - FB_BASE (fabric subtractor result = the linear pixel index) 14// ge_base = carry_out(addr - FB_BASE) (== 1 iff addr >= FB_BASE; the R8b SLTU convention: 15// carry-out of a-b is 1 iff a >= b unsigned) 16// ge_end = carry_out(addr - FB_END) (== 1 iff addr >= FB_END) 17// in_fb = ge_base AND (NOT ge_end) (FB_BASE <= addr < FB_END) 18// The substantive decision (two wide unsigned compares + the index subtraction) is a real fabric 19// computation driven only from the subtractor's bitstream via fab_eval; the final 1-bit AND of the two 20// decoded flags is orchestration (exactly as the fabric-CPU gates read fabric POs and orchestrate). 21// 22// SCANOUT: read the framebuffer block -> the games' i64 packed-RGB format (R | G<<8 | B<<16) -> the gate 23// encodes it to a PNG (write_png) so the fabric's pixels are eyeball-verifiable. 24// 25// NEVER-BRICK (#26): pure integer, bounded (exactly 2 subtractor passes per decoded store, each O(W) cells), 26// total, deterministic, caller-owned state, ZERO persistent/hardware writes. A framebuffer pixel write is 27// volatile VRAM -- a `gui`-axis capability that cannot corrupt firmware/CMOS/NVRAM/EEPROM BY CONSTRUCTION, 28// so it carries no brick risk even when this peripheral is later bound to a real linear framebuffer. 29// license_tier: ORIGINAL 30import "nx_fpga_addsub.nx" 31import "nx_fpga_fabric.nx" 32import "nx_syscalls.nx" 33const K_MAGIC_2654435761: i64 = 2654435761 34 35// A display controller instance: an MMIO framebuffer + the on-fabric address decode it adds to the bus. 36struct NxFpgaDC { 37 fb: *i64 // W*H packed-RGB framebuffer words (the BRAM/DRAM analog -- a memory block) 38 fbw: i64 39 fbh: i64 40 base: i64 // MMIO window base (FB_BASE) 41 fbend: i64 // MMIO window end (FB_BASE + W*H), one past the last pixel addr 42 addr_w: i64 // address width in bits for the on-fabric decode 43 sub_npi: i64 // the subtractor fabric's primary-input count (from fab_build_addsub) 44 sub_init: *i64 // subtractor bitstream: per-cell LUT init 45 sub_src: *i64 // subtractor bitstream: per-cell wire sources 46 sub_po: *i64 // subtractor primary-output sources 47 pi: *i64 // scratch primary-input vector (caller-owned -> no per-call mmap) 48 co: *i64 // scratch cell-output vector (caller-owned) 49 last_idx: i64 // the pixel index produced by the most recent dc_decode (set in-place, no out-ptr) 50} 51 52// pack an RGB triple into the games' i64 framebuffer format (R low byte, then G, then B). 53func dc_pack(r: i64, g: i64, b: i64) -> i64 { 54 return (r & 0xff) | ((g & 0xff) << 8) | ((b & 0xff) << 16) 55} 56 57// build the on-fabric MMIO-decode subtractor + bind the framebuffer block. Caller allocates everything: 58// fb[fbw*fbh], sub_init[3*addr_w], sub_src[3*addr_w*4], sub_po[addr_w], pi[2*addr_w+1], co[3*addr_w]. 59func dc_init(dc: *NxFpgaDC, fb: *i64, fbw: i64, fbh: i64, base: i64, addr_w: i64, 60 sub_init: *i64, sub_src: *i64, sub_po: *i64, pi: *i64, co: *i64) -> i64 { 61 dc.fb = fb 62 dc.fbw = fbw 63 dc.fbh = fbh 64 dc.base = base 65 dc.fbend = base + fbw * fbh 66 dc.addr_w = addr_w 67 dc.sub_init = sub_init 68 dc.sub_src = sub_src 69 dc.sub_po = sub_po 70 dc.pi = pi 71 dc.co = co 72 dc.last_idx = 0 73 dc.sub_npi = fab_build_addsub(addr_w, sub_init, sub_src, sub_po) 74 return 0 75} 76 77// DECODE an MMIO store address ON THE FABRIC. Returns in_fb (0/1); sets dc.last_idx = the pixel index. 78// Two subtractor passes (addr-base, addr-end); the top carry cell of nx_fpga_addsub holds carry-out. 79func dc_decode(dc: *NxFpgaDC, addr: i64) -> i64 { 80 let W: i64 = dc.addr_w 81 let cc: i64 = W + 2 * (W - 1) + 1 // top-bit carry cell (carry-out of the subtraction) 82 let idx: i64 = fab_addsub_run(W, dc.sub_npi, dc.sub_init, dc.sub_src, dc.sub_po, dc.pi, dc.co, addr, dc.base, 1) 83 let ge_base: i64 = dc.co[cc] & 1 // 1 iff addr >= FB_BASE 84 fab_addsub_run(W, dc.sub_npi, dc.sub_init, dc.sub_src, dc.sub_po, dc.pi, dc.co, addr, dc.fbend, 1) 85 let ge_end: i64 = dc.co[cc] & 1 // 1 iff addr >= FB_END 86 dc.last_idx = idx 87 var in_fb: i64 = 0 88 if ge_base == 1 { if ge_end == 0 { in_fb = 1 } } // FB_BASE <= addr < FB_END 89 return in_fb 90} 91 92// MMIO STORE: if the on-fabric decode places `addr` in the framebuffer window, write the pixel. 93// Returns in_fb (1 = the store hit a framebuffer pixel, 0 = ignored -- the peripheral does not claim it). 94// Bounds-checked at the device/memory boundary (#12: defensive at the boundary). 95func dc_store(dc: *NxFpgaDC, addr: i64, value: i64) -> i64 { 96 let in_fb: i64 = dc_decode(dc, addr) 97 if in_fb == 1 { 98 let idx: i64 = dc.last_idx 99 let n: i64 = dc.fbw * dc.fbh 100 if idx >= 0 { if idx < n { dc.fb[idx] = value & 0xffffffff } } 101 } 102 return in_fb 103} 104 105// fill the whole framebuffer with one packed color (clear-to-color). 106func dc_clear(dc: *NxFpgaDC, color: i64) -> i64 { 107 let n: i64 = dc.fbw * dc.fbh 108 var i: i64 = 0 109 while i < n { dc.fb[i] = color; i = i + 1 } 110 return 0 111} 112 113// SCANOUT helper: an xor-fold checksum over the framebuffer (used by gates to prove "nothing changed"). 114func dc_checksum(dc: *NxFpgaDC) -> i64 { 115 let n: i64 = dc.fbw * dc.fbh 116 var s: i64 = 0 117 var i: i64 = 0 118 while i < n { s = s ^ (dc.fb[i] + i * K_MAGIC_2654435761); i = i + 1 } 119 return s 120}