code wiki / _hdl_build / nx_rv64im_cpu_crosscheck.nx
nx_rv64im_cpu_crosscheck.nx source
↩ module page · 115 lines · 4164 B
1// nx_rv64im_cpu_crosscheck.nx -- 1:1 proof: our sovereign RV64IM CPU sim
2// vs qemu-system-riscv64 (canonical reference) on the SAME ELF.
3//
4// Loads cpu_crosscheck_prog.elf (sum of squares 1..20 = 2870, printed via
5// UART, exercising MUL/DIVU/REMU/branches/loads) into the sim, runs it,
6// and emits the captured UART byte stream to stdout + a proof file. The
7// off-box harness then diffs our UART against qemu's UART and the known
8// answer 2870. Asserts our output contains "SUM=2870".
9//
10// expect_exit: 0
11// license_tier: ORIGINAL
12
13import "nx_syscalls.nx"
14import "nishi_hdl_primitives.nx"
15import "rv64im_min_decoder.nx"
16import "rv64im_min_alu.nx"
17import "rv64im_min_regfile.nx"
18import "rv64im_min_csr.nx"
19import "rv64im_min_clint.nx"
20import "rv64im_min_uart.nx"
21import "rv64im_min_sim.nx"
22import "rv64im_min_elf_loader.nx"
23
24const CC_MEM_BASE: i64 = 0x80000000
25const CC_MEM_SIZE: i64 = 0x400000 // 4 MiB (covers prog + 0x80100000 buf + 0x80200000 stack)
26const CC_TX_CAP: i64 = 4096
27const CC_MAX_STEPS: i64 = 1000000
28
29func _contains(hay: *u8, hlen: i64, needle: *u8, nlen: i64) -> i64 {
30 if nlen == 0 { return 1 }
31 if hlen < nlen { return 0 }
32 let last: i64 = hlen - nlen
33 var i: i64 = 0
34 while i <= last {
35 var j: i64 = 0
36 var ok: i64 = 1
37 while j < nlen {
38 if hay[i + j] != needle[j] { ok = 0; j = nlen }
39 j = j + 1
40 }
41 if ok == 1 { return 1 }
42 i = i + 1
43 }
44 return 0
45}
46
47func _slen(s: *u8) -> i64 {
48 var n: i64 = 0
49 while s[n] != 0 { n = n + 1 }
50 return n
51}
52
53func main() -> i64 {
54 let path: *u8 = "/mnt/c/Users/elder/nishi-browser-proofs/cpu_crosscheck_prog.bin\x00"
55 let elf_len_out: *i64 = (sys_mmap(8)) as *i64
56 elf_len_out[0] = 0
57 let elf_bytes: *u8 = sys_read_file(path, elf_len_out)
58 let elf_size: i64 = elf_len_out[0]
59 if (elf_bytes as i64) == 0 { return 1 }
60 if elf_size < 64 { return 2 }
61
62 let rf_storage: *i64 = (sys_mmap(8 * NX_RV64IM_RF_N_REGS)) as *i64
63 let csr_storage: *i64 = (sys_mmap(8 * NX_CSR_SLOT_N)) as *i64
64 let clint_storage: *i64 = (sys_mmap(8 * NX_CLINT_SLOT_N)) as *i64
65 let uart_storage: *i64 = (sys_mmap(8 * NX_UART_SLOT_N)) as *i64
66 let mem: *u8 = sys_mmap(CC_MEM_SIZE)
67 let tx_buf: *u8 = sys_mmap(CC_TX_CAP)
68
69 let rf: *NxRv64imRegfile = (sys_mmap(64)) as *NxRv64imRegfile
70 let csr: *NxRv64imCsrFile = (sys_mmap(64)) as *NxRv64imCsrFile
71 let clint: *NxClint = (sys_mmap(64)) as *NxClint
72 let uart: *NxUart = (sys_mmap(64)) as *NxUart
73 let sim: *NxRv64imSim = (sys_mmap(128)) as *NxRv64imSim
74
75 nx_rv64im_rf_init(rf, rf_storage)
76 nx_rv64im_csr_init(csr, csr_storage, 0)
77 nx_clint_init(clint, clint_storage)
78 nx_uart_init(uart, uart_storage, tx_buf, CC_TX_CAP)
79 nx_rv64im_sim_init(sim, rf, csr, clint, uart, CC_MEM_BASE, mem, CC_MEM_SIZE, 0)
80
81 // Raw-load the flat program image at mem_base (sim_init already set
82 // pc = mem_base + 0). The ELF's own LOAD segment sits at 0x7ffff000
83 // (it carries the ELF headers) which is below our mem_base, so we use
84 // the objcopy'd flat binary instead -- byte 0 == the instruction at
85 // 0x80000000.
86 if elf_size > CC_MEM_SIZE { return 3 }
87 var ci: i64 = 0
88 while ci < elf_size {
89 mem[ci] = elf_bytes[ci]
90 ci = ci + 1
91 }
92
93 nx_rv64im_sim_run(sim, CC_MAX_STEPS)
94
95 let tx_n: i64 = nx_uart_tx_count(uart)
96 if tx_n == 0 { return 5 }
97
98 // emit captured UART to stdout + proof file
99 let banner: *u8 = "\n[our sovereign RV64IM CPU sim UART output]\n\x00"
100 sys_write(1, banner, 43)
101 sys_write(1, tx_buf, tx_n)
102 sys_write(1, banner, 1)
103
104 let outp: *u8 = "/mnt/c/Users/elder/nishi-browser-proofs/sim_uart_out.txt\x00"
105 let ofd: i64 = sys_openat_wr(outp, 0x1A4)
106 if ofd > 0 { sys_write(ofd, tx_buf, tx_n); sys_close(ofd) }
107
108 let want: *u8 = "SUM=2870\x00"
109 if _contains(tx_buf, tx_n, want, _slen(want)) != 1 { return 80 }
110
111 let pass: *u8 = sys_mmap(16)
112 pass[0]=0x50; pass[1]=0x41; pass[2]=0x53; pass[3]=0x53; pass[4]=0x0A
113 sys_write(2, pass, 5)
114 return 0
115}