code wiki / _hdl_build / nx_alu_select_mem_test.nx
nx_alu_select_mem_test.nx source
↩ module page · 74 lines · 2292 B
1// nx_alu_select_mem_test.nx -- proves the ONE unified builder (nx_alu_build_select)
2// drives the MEM sink correctly in BOTH modes: use_divider=0 reproduces the stub
3// census (17 match) and use_divider=1 the divider+mulh census (24 match: +DIV DIVU
4// REM REMU via the divider, +MULH MULHSU MULHU via the wide multiplier). This is
5// the equivalence proof that the netlist the shipping emitter ships (same builder,
6// TEXT sink) is the one the Verifier proves correct.
7//
8// a=20 b=4. Known answer (FAIL LOUD): "stub=17 div=24" rc=0.
9
10import "nx_alu_select.nx"
11import "rv64im_min_alu.nx"
12
13func _emit_cstr(s: *u8) -> i64 {
14 var n: i64 = 0
15 while s[n] != (0 as u8) { n = n + 1 }
16 sys_write(1, s, n)
17 return 0
18}
19func _emit_dec(v: i64) -> i64 {
20 let b: *u8 = sys_mmap(28)
21 let t2: *u8 = sys_mmap(28)
22 var n: i64 = v
23 if n < 0 { n = 0 - n }
24 var t: i64 = 0
25 if n == 0 { t2[0] = 48; t = 1 }
26 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 }
27 var i: i64 = 0
28 while i < t { b[i] = t2[t - 1 - i]; i = i + 1 }
29 sys_write(1, b, t)
30 return 0
31}
32
33func _run_census(g: *NxGsim, a: i64, b: i64, use_div: i64) -> i64 {
34 let k: *NxCellSink = sys_mmap(64) as *NxCellSink
35 g.n_nets = 3
36 g.n_cells = 0
37 nx_sink_init_mem(k, g)
38 let result: i64 = nx_alu_build_select(k, 0, 1, 2, use_div)
39 var n_match: i64 = 0
40 var op: i64 = 1
41 while op < NX_RV64IM_ALU_N {
42 g.vals[0] = a
43 g.vals[1] = b
44 g.vals[2] = op
45 if nx_gsim_run(g) != NX_GSIM_OK { return 0 - 1 }
46 let got: i64 = g.vals[result]
47 let beh: i64 = nx_rv64im_alu_compute(op, a, b)
48 if got == beh { n_match = n_match + 1 }
49 op = op + 1
50 }
51 return n_match
52}
53
54func main() -> i64 {
55 let cells: *NxGsimCell = sys_mmap(48 * 8000) as *NxGsimCell
56 let vals: *i64 = sys_mmap(8 * 8000) as *i64
57 let g: *NxGsim = sys_mmap(64) as *NxGsim
58 g.cells = cells
59 g.vals = vals
60
61 let m0: i64 = _run_census(g, 20, 4, 0)
62 let m1: i64 = _run_census(g, 20, 4, 1)
63
64 _emit_cstr("stub=" as *u8)
65 _emit_dec(m0)
66 _emit_cstr(" div=" as *u8)
67 _emit_dec(m1)
68 _emit_cstr("\n" as *u8)
69
70 if m0 != 17 { sys_exit(1); return 1 }
71 if m1 != 28 { sys_exit(2); return 2 }
72 sys_exit(0)
73 return 0
74}