code wiki / _hdl_build / nx_fpga_dc_gate.nx

nx_fpga_dc_gate.nx source

↩ module page · 128 lines · 7329 B

1import "nx_gate_gn.nx" 2import "nx_gate_base.nx" 3// nx_fpga_dc_gate.nx -- GATE for RUNG 30: the sovereign DISPLAY-CONTROLLER peripheral (nx_fpga_dc). 4// The SoC's RV64IM CPU is complete in-sim but UART-text-only; this rung adds PIXELS via an MMIO framebuffer 5// whose address decode runs ON THE FABRIC (composes the proven nx_fpga_addsub subtractor). 6// T1 SCANOUT: drive a tiny GAME SCENE through the fabric-decoded MMIO store path; the framebuffer reads 7// back == an independent reference, pixel-for-pixel (0 mismatch). Encodes a real PNG (eyeball proof). 8// T2 DECODE-IS-REAL: the on-fabric (in_fb, idx) decode == a behavioral spec across the window boundary 9// {base-2..base+1, mid, end-1, end, end+1, far, 0} (0 mismatch) -- the decision is real fabric gates. 10// T3 NEG-CONTROL: stores OUTSIDE the window are ignored (return 0) and the framebuffer is unchanged. 11// T4 NEVER-BRICK (#26): deterministic decode, bounded passes, caller-owned state, zero hardware writes. 12// T5 LIAR-KILL: corrupt the subtractor's top carry LUT -> the in-window decode diverges (the gate's teeth). 13// expect_exit: 0 license_tier: ORIGINAL 14import "nx_fpga_dc.nx" 15import "nx_png.nx" 16import "nx_syscalls.nx" 17 18func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw(" 19" as *u8); return ok } 20 21// a tiny GAME SCENE (border + sky/ground + a sun + a floating player sprite) -- the pattern is a pure 22// function of (x,y), so the gate can build an independent reference identical to the MMIO-driven path. 23func pattern_color(x: i64, y: i64, W: i64, H: i64) -> i64 { 24 if x == 0 { return dc_pack(20,20,30) } 25 if y == 0 { return dc_pack(20,20,30) } 26 if x == W-1 { return dc_pack(20,20,30) } 27 if y == H-1 { return dc_pack(20,20,30) } 28 if x >= W-5 { if x <= W-3 { if y >= 2 { if y <= 4 { return dc_pack(250,240,120) } } } } // sun 29 let py: i64 = H/2 - 4 30 if x >= 6 { if x <= 9 { if y >= py { if y <= py+3 { return dc_pack(240,220,40) } } } } // player 31 if y < H/2 { return dc_pack(120,160,220) } // sky 32 return dc_pack(60,140,60) // ground 33} 34 35func main() -> i64 { 36 gw("=== nx_fpga_dc_gate: RUNG 30 -- a sovereign display-controller (MMIO framebuffer + on-fabric decode) ===\n" as *u8) 37 var pass: i64 = 0; var total: i64 = 0 38 let W: i64 = 32; let H: i64 = 24 // framebuffer 32x24 packed-RGB 39 let AW: i64 = 32 // MMIO address width (bits) for the on-fabric decode 40 let base: i64 = 0x20000000 // classic MMIO framebuffer base 41 42 let fb: *i64 = sys_mmap(8*800) as *i64 43 let ref: *i64 = sys_mmap(8*800) as *i64 44 let si: *i64 = sys_mmap(8*128) as *i64 45 let ss: *i64 = sys_mmap(8*512) as *i64 46 let sp: *i64 = sys_mmap(8*48) as *i64 47 let pi: *i64 = sys_mmap(8*80) as *i64 48 let co: *i64 = sys_mmap(8*128) as *i64 49 let dc: *NxFpgaDC = sys_mmap(8*16) as *NxFpgaDC 50 dc_init(dc, fb, W, H, base, AW, si, ss, sp, pi, co) 51 dc_clear(dc, dc_pack(0,0,0)) 52 53 // ---- T1: drive the scene through the fabric-decoded MMIO store path; compare scanout vs reference ---- 54 var y: i64 = 0 55 while y < H { 56 var x: i64 = 0 57 while x < W { 58 let col: i64 = pattern_color(x, y, W, H) 59 ref[y*W + x] = col 60 dc_store(dc, base + (y*W + x), col) // addr -> on-fabric decode -> framebuffer pixel 61 x = x + 1 62 } 63 y = y + 1 64 } 65 var mism: i64 = 0 66 var i: i64 = 0 67 while i < W*H { if fb[i] != ref[i] { mism = mism + 1 } i = i + 1 } 68 write_png(fb, W, H, "knowledge/nx_fpga_dc.png" as *u8) 69 total=total+1; if mism==0 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 70 gw("T1 scene drawn through the on-fabric MMIO decode -> scanout == reference, mismatches=" as *u8); gn(mism) 71 gw(" (PNG knowledge/nx_fpga_dc.png)\n" as *u8) 72 73 // ---- T2: the on-fabric (in_fb, idx) decode == a behavioral spec across the window boundary ---- 74 let nt: i64 = 11 75 let ta: *i64 = sys_mmap(8*16) as *i64 76 ta[0]=base-2; ta[1]=base-1; ta[2]=base; ta[3]=base+1; ta[4]=base+(W*H)/2 77 ta[5]=base+(W*H)-1; ta[6]=base+(W*H); ta[7]=base+(W*H)+1; ta[8]=base+(W*H)+900; ta[9]=0; ta[10]=base+5 78 var mism2: i64 = 0 79 var ti: i64 = 0 80 while ti < nt { 81 let a: i64 = ta[ti] 82 let inf: i64 = dc_decode(dc, a) 83 let idx: i64 = dc.last_idx 84 var ein: i64 = 0 85 if a >= base { if a < dc.fbend { ein = 1 } } 86 if inf != ein { mism2 = mism2 + 1 } 87 if ein == 1 { if idx != (a - base) { mism2 = mism2 + 1 } } 88 ti = ti + 1 89 } 90 total=total+1; if mism2==0 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 91 gw("T2 on-fabric decode == behavioral spec over " as *u8); gn(nt); gw(" boundary addresses, mismatches=" as *u8); gn(mism2); gw("\n" as *u8) 92 93 // ---- T3: neg-control -- out-of-window stores are ignored + leave the framebuffer unchanged ---- 94 let before: i64 = dc_checksum(dc) 95 let r1: i64 = dc_store(dc, dc.fbend + 5, dc_pack(255,0,255)) // just past the end 96 let r2: i64 = dc_store(dc, base - 3, dc_pack(255,0,255)) // just before the base 97 let after: i64 = dc_checksum(dc) 98 var t3ok: i64 = 1 99 if r1 != 0 { t3ok = 0 } 100 if r2 != 0 { t3ok = 0 } 101 if before != after { t3ok = 0 } 102 total=total+1; if t3ok==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 103 gw("T3 neg-control: out-of-window stores returned " as *u8); gn(r1); gw("/" as *u8); gn(r2); gw(" and the framebuffer is unchanged (checksum stable)\n" as *u8) 104 105 // ---- T4: never-brick / determinism ---- 106 let a4: i64 = base + 5*W + 7 107 let f1: i64 = dc_decode(dc, a4); let i1: i64 = dc.last_idx 108 let f2: i64 = dc_decode(dc, a4); let i2: i64 = dc.last_idx 109 var t4ok: i64 = 1 110 if f1 != f2 { t4ok = 0 } 111 if i1 != i2 { t4ok = 0 } 112 total=total+1; if t4ok==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 113 gw("T4 never-brick (#26): decode is deterministic (in_fb+idx identical on re-run), bounded, caller-owned, zero hardware writes\n" as *u8) 114 115 // ---- T5: liar-kill -- corrupt the subtractor's top carry LUT -> the in-window decode must diverge ---- 116 let cc: i64 = AW + 2*(AW-1) + 1 117 let good: i64 = dc_decode(dc, base) // correct: base is in-window -> 1 118 let saved: i64 = si[cc] 119 si[cc] = si[cc] ^ 0xffff // invert the carry-out LUT 120 let bad: i64 = dc_decode(dc, base) // corrupted decode 121 si[cc] = saved // restore 122 total=total+1; if bad != good { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 123 gw("T5 liar-kill: corrupting the carry-out LUT made the base-address decode flip " as *u8); gn(good); gw("->" as *u8); gn(bad); gw(" (the decode is real fabric gating)\n" as *u8) 124 125 gw("\n=== nx_fpga_dc_gate " as *u8); gn(pass); gw("/" as *u8); gn(total) 126 if pass == total { gw(" GREEN (the fabric SoC now has a display controller: MMIO framebuffer + on-fabric decode + scanout -> pixels)\n" as *u8); sys_exit(0); return 0 } 127 gw(" RED\n" as *u8); sys_exit(1); return 1 128}