code wiki / _hdl_build / nx_decode_kind_test.nx
nx_decode_kind_test.nx source
↩ module page · 50 lines · 1907 B
1// nx_decode_kind_test.nx -- EXHAUSTIVE proof of the RV64IM decoder gate-network
2// (nx_decode_kind_synth) vs the behavioral nx_rv64im_decode_kind. decode_kind
3// depends only on {opcode[6:0], funct3[14:12], funct7[31:25]} (17 bits), so this
4// sweeps ALL 2^17 = 131072 combinations -- a complete proof, not a sample.
5// Known answer: "131072 131072" (ok total), exit 0.
6
7import "nx_decode_kind.nx"
8
9func _emit_dec(v: i64) -> i64 {
10 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n }
11 let t: *u8 = sys_mmap(28); var k: i64 = 0
12 if n == 0 { t[0] = 48; k = 1 }
13 while n > 0 { t[k] = 48 + (n % 10); n = n / 10; k = k + 1 }
14 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 }
15 b[k] = 32; sys_write(1, b, k + 1); return 0
16}
17func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
18
19func main() -> i64 {
20 let vals: *i64 = sys_mmap(8 * 256) as *i64
21 let cells: *NxGsimCell = sys_mmap(48 * 256) as *NxGsimCell
22 let g: *NxGsim = sys_mmap(64) as *NxGsim
23 g.vals = vals; g.n_nets = 1; g.cells = cells; g.n_cells = 0
24 let knet: i64 = nx_decode_kind_synth(g, 0) // inst = net 0
25
26 var total: i64 = 0
27 var ok: i64 = 0
28 var oc: i64 = 0
29 while oc < 128 {
30 var f3: i64 = 0
31 while f3 < 8 {
32 var f7: i64 = 0
33 while f7 < 128 {
34 let inst: i64 = oc | (f3 << 12) | (f7 << 25)
35 g.vals[0] = inst
36 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(40); return 40 }
37 total = total + 1
38 if g.vals[knet] == nx_rv64im_decode_kind(inst) { ok = ok + 1 }
39 f7 = f7 + 1
40 }
41 f3 = f3 + 1
42 }
43 oc = oc + 1
44 }
45
46 _emit_dec(ok); _emit_dec(total); _nl()
47 if ok != total { sys_exit(1); return 1 }
48 if total != 131072 { sys_exit(2); return 2 }
49 sys_exit(0); return 0
50}