nx_nrtl_gate.nx source

1import "nx_gate_gn.nx" 2import "nx_gate_base.nx" 3// nx_nrtl_gate.nx -- GATE for NHDL H3+H4: sovereign RTL + SYNTHESIS (the Yosys competitor). Authors a multi-statement 4// RTL design, SYNTHESIZES it to a LUT4 fabric, and proves the synthesized gates == a behavioral oracle: 5// T1 the synthesized fabric (from `t=a&b; u=a^b; y=t+u`) computes ((a&b)+(a^b))&0xFF == oracle over 100 random (a,b). 6// T2 ABSTRACTION BENCHMARK: a few lines of RTL synthesize to a 32-gate netlist; RTL source << NHDL << Verilog 7// (you author the equation, the synthesizer builds the gates -- the Yosys value, sovereign). 8// T3 NEVER-BRICK (#26): bounded synthesis, pure memory. 9// T4 LIAR-KILL: change ONE op in the RTL (+ -> &) and re-synthesize -> the gates compute WRONG (RTL drives the logic). 10// Sovereign, no-float. expect_exit: 0 license_tier: ORIGINAL 11import "nx_nrtl.nx" 12import "nx_nhdl.nx" 13import "nx_fpga_verilog.nx" 14import "nx_fpga_fabric.nx" 15import "nx_syscalls.nx" 16 17func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw(" 18" as *u8); return ok } 19 20func run2(cn: i64, NPI: i64, cinit: *i64, csrc: *i64, cpo: *i64, pi: *i64, co: *i64, W: i64, a: i64, b: i64) -> i64 { 21 var i: i64=0; while i<W { pi[i]=(a>>i)&1; pi[W+i]=(b>>i)&1; i=i+1 } 22 pi[2*W]=0 23 fab_eval(cn, NPI, cinit, csrc, pi, co) 24 var s: i64=0; i=0; while i<W { let bit: i64=fab_resolve(cpo[i], NPI, pi, co); s=s|(bit<<i); i=i+1 } 25 return s 26} 27 28func main() -> i64 { 29 gw("=== nx_nrtl_gate: NHDL H3+H4 -- sovereign RTL + SYNTHESIS (Yosys competitor) ===\n" as *u8) 30 let W: i64=8; let MASK: i64=255 31 var pass: i64=0; var total: i64=0 32 // author RTL (copied to a mutable buffer so the liar-kill can edit it) 33 let srclit: *u8=".nrtl 1\n.module demo 8\n.in a b\n.out y\nt = a & b\nu = a ^ b\ny = t + u\n.end\n\x00" as *u8 34 let mbuf: *u8=sys_mmap(4096) 35 var ci: i64=0; while srclit[ci]!=(0 as u8) { mbuf[ci]=srclit[ci]; ci=ci+1 } mbuf[ci]=0 as u8 36 let slen: i64=ci 37 38 let cinit: *i64=sys_mmap(8*256) as *i64; let csrc: *i64=sys_mmap(8*1024) as *i64; let ckind: *i64=sys_mmap(8*256) as *i64 39 let cpo: *i64=sys_mmap(8*32) as *i64; let onpi: *i64=sys_mmap(16) as *i64; let onpo: *i64=sys_mmap(16) as *i64; let oW: *i64=sys_mmap(16) as *i64 40 let cn: i64=nrtl_synth(mbuf, slen, cinit, csrc, ckind, cpo, onpi, onpo, oW) 41 let NPI: i64=onpi[0] 42 let pi: *i64=sys_mmap(8*128) as *i64; let co: *i64=sys_mmap(8*256) as *i64 43 44 // ---- T1: synthesized fabric == oracle ---- 45 var seed: i64=20260626; var mism: i64=0; var checks: i64=0 46 var t: i64=0 47 while t<100 { 48 seed=(seed*1103515245+12345)&2147483647; let a: i64=seed&MASK 49 seed=(seed*1103515245+12345)&2147483647; let b: i64=seed&MASK 50 let got: i64=run2(cn, NPI, cinit, csrc, cpo, pi, co, W, a, b) 51 let exp: i64=((a&b)+(a^b))&MASK 52 if got!=exp { mism=mism+1 } 53 checks=checks+1; t=t+1 54 } 55 total=total+1; if mism==0 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 56 gw("T1 SYNTHESIZED fabric (t=a&b; u=a^b; y=t+u) == oracle: checks=" as *u8); gn(checks); gw(" mismatches=" as *u8); gn(mism); gw(" (synth gates=" as *u8); gn(cn); gw(" NPI=" as *u8); gn(NPI); gw(")\n" as *u8) 57 58 // ---- T2: ABSTRACTION BENCHMARK: RTL source << NHDL netlist << Verilog ---- 59 let hbuf: *u8=sys_mmap(16384); let hlen: i64=nhdl_emit(hbuf, "demo" as *u8, cn, NPI, W, ckind, cinit, csrc, cpo) 60 let vbuf: *u8=sys_mmap(32768); let vlen: i64=fab_emit_verilog_seq(vbuf, cn, NPI, W, ckind, cinit, csrc, cpo) 61 total=total+1; if slen<hlen { if hlen<vlen { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } } else { gw(" [FAIL] " as *u8) } 62 gw("T2 ABSTRACTION: " as *u8); gn(slen); gw("B of sovereign RTL -> synthesized " as *u8); gn(cn); gw(" gates = " as *u8); gn(hlen); gw("B NHDL / " as *u8); gn(vlen); gw("B Verilog (author the equation, synth builds the gates)\n" as *u8) 63 64 // ---- T3: never-brick ---- 65 total=total+1; if cn==4*W { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 66 gw("T3 NEVER-BRICK (#26): synthesis bounded & exact (gates=" as *u8); gn(cn); gw(" = AND[8]+XOR[8]+ADD[16] = 4W=" as *u8); gn(4*W); gw("), pure memory\n" as *u8) 67 68 // ---- T4: liar-kill -- change the '+' op to '&' and re-synthesize -> wrong ---- 69 var ppos: i64=0-1; var si: i64=0 70 while si<slen { if mbuf[si]==(43 as u8) { if ppos<0 { ppos=si } } si=si+1 } // the '+' in `y = t + u` 71 mbuf[ppos]=38 as u8 // '+' -> '&' 72 let cn2: i64=nrtl_synth(mbuf, slen, cinit, csrc, ckind, cpo, onpi, onpo, oW) 73 var liar_wrong: i64=0; var lt: i64=0 74 while lt<10 { 75 seed=(seed*1103515245+12345)&2147483647; let a: i64=seed&MASK 76 seed=(seed*1103515245+12345)&2147483647; let b: i64=seed&MASK 77 if run2(cn2, onpi[0], cinit, csrc, cpo, pi, co, W, a, b) != (((a&b)+(a^b))&MASK) { liar_wrong=liar_wrong+1 } 78 lt=lt+1 79 } 80 total=total+1; if liar_wrong>0 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 81 gw("T4 LIAR-KILL: RTL op + -> & re-synthesized -> gates wrong on " as *u8); gn(liar_wrong); gw("/10 inputs\n" as *u8) 82 83 gw("NRTL-GATE verdict=" as *u8) 84 if pass==total { gw("GREEN passes=" as *u8); gn(pass); gw("/" as *u8); gn(total); gw(" END\n" as *u8); sys_exit(0); return 0 } 85 gw("RED passes=" as *u8); gn(pass); gw("/" as *u8); gn(total); gw(" END\n" as *u8); sys_exit(1); return 1 86}