code wiki / _hdl_build / nx_alu_netlist_full_test.nx
`nx_alu_netlist_full_test.nx` source

1// nx_alu_netlist_full_test.nx -- SIL-3 VERIFIER over the FULL 29-op ALU.
2//
3// Builds the ALU op-select netlist via nx_alu_netlist_build (the ONE source the
4// text emitter also derives from), then for EVERY op K in 1..28 runs the
5// gate-level functional sim and diffs vs the behavioral oracle
6// nx_rv64im_alu_compute(K, a, b). This is the closure of "consume the ACTUAL
7// emitter topology + diff vs behavioral over all 29 ops": where the seed
8// emitter is faithful the sim MATCHES; where it stubs (DIV/REM->ADD, mulh->MUL)
9// the sim DIVERGES -- the verifier CATCHES every silent gate-emit hole, not just
10// DIV. That divergence set is the 5W1H feedback the Generator consumes.
11//
12// a=20 b=4. Known answer (FAIL LOUD): "covered=28 match=17 diverge=11" rc=0.
13//   17 faithful: ADD SUB AND OR XOR SLL SRL SRA SLT SLTU MUL ADDW SUBW SLLW
14//                SRLW SRAW MULW   (all single-cell ops the seed lowers exactly)
15//   11 holes:    MULH MULHSU MULHU (low-product MUL, want high) +
16//                DIV DIVU REM REMU DIVW DIVUW REMW REMUW (ADD stub, want divider)
17// When a real divider sub-network replaces the DIV stub in nx_alu_op_to_gate_kind,
18// this same gate flips DIV from DIVERGE to MATCH -- the first HW invention.
19
20import "nx_alu_netlist_build.nx"
21import "rv64im_min_alu.nx"
22
23func _emit_cstr(s: *u8) -> i64 {
24    var n: i64 = 0
25    while s[n] != (0 as u8) { n = n + 1 }
26    sys_write(1, s, n)
27    return 0
28}
29
30func _emit_dec(v: i64) -> i64 {
31    let b: *u8 = sys_mmap(28)
32    let t2: *u8 = sys_mmap(28)
33    var n: i64 = v
34    if n < 0 { n = 0 - n }
35    var t: i64 = 0
36    if n == 0 { t2[0] = 48; t = 1 }
37    while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 }
38    var i: i64 = 0
39    while i < t { b[i] = t2[t - 1 - i]; i = i + 1 }
40    sys_write(1, b, t)
41    return 0
42}
43
44func main() -> i64 {
45    let cells: *NxGsimCell = sys_mmap(48 * 160) as *NxGsimCell
46    let vals:  *i64        = sys_mmap(8 * 160) as *i64
47    let info:  *NxAluNetlist = sys_mmap(64) as *NxAluNetlist
48    let g:     *NxGsim     = sys_mmap(64) as *NxGsim
49
50    nx_alu_netlist_build(cells, info)
51
52    g.vals    = vals
53    g.n_nets  = info.n_nets
54    g.cells   = cells
55    g.n_cells = info.n_cells
56
57    let a: i64 = 20
58    let b: i64 = 4
59
60    var n_match: i64 = 0
61    var n_div:   i64 = 0
62    var add_ok:      i64 = 0
63    var div_caught:  i64 = 0
64    var mulh_caught: i64 = 0
65
66    var op: i64 = 1
67    while op < NX_RV64IM_ALU_N {
68        vals[NX_ALUNL_A]    = a
69        vals[NX_ALUNL_B]    = b
70        vals[NX_ALUNL_OPIN] = op
71        if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(40); return 40 }
72        let got: i64 = vals[info.result]
73        let beh: i64 = nx_rv64im_alu_compute(op, a, b)
74        if got == beh { n_match = n_match + 1 }
75        if got != beh { n_div = n_div + 1 }
76        if op == NX_RV64IM_ALU_ADD  { if got == beh { add_ok = 1 } }
77        if op == NX_RV64IM_ALU_DIV  { if got != beh { div_caught = 1 } }
78        if op == NX_RV64IM_ALU_MULH { if got != beh { mulh_caught = 1 } }
79        op = op + 1
80    }
81
82    _emit_cstr("covered=" as *u8)
83    _emit_dec(NX_RV64IM_ALU_N - 1)
84    _emit_cstr(" match=" as *u8)
85    _emit_dec(n_match)
86    _emit_cstr(" diverge=" as *u8)
87    _emit_dec(n_div)
88    _emit_cstr("\n" as *u8)
89
90    // Anchors: the verifier must (1) accept a faithful op, (2) catch the DIV
91    // stub, (3) catch a mulh stub -- then the exact census counts.
92    if add_ok != 1      { sys_exit(1); return 1 }
93    if div_caught != 1  { sys_exit(2); return 2 }
94    if mulh_caught != 1 { sys_exit(3); return 3 }
95    if n_match != 17    { sys_exit(4); return 4 }
96    if n_div != 11      { sys_exit(5); return 5 }
97    sys_exit(0)
98    return 0
99}
nx_alu_netlist_full_test.nx source

`nx_alu_netlist_full_test.nx` source
