code wiki / _hdl_build / nx_alu_select_mem_test.nx

nx_alu_select_mem_test.nx

buildroot/runtime/_hdl_build/nx_alu_select_mem_test.nx

2292 B74 linesdepth 10pulls 12 transitivereach 0 importersview sourcekind gate/prooftopic alu
docsdependenciesstructsconstsfunctions

about

nx_alu_select_mem_test.nx -- proves the ONE unified builder (nx_alu_build_select) drives the MEM sink correctly in BOTH modes: use_divider=0 reproduces the stub census (17 match) and use_divider=1 the divider+mulh census (24 match: +DIV DIVU REM REMU via the divider, +MULH MULHSU MULHU via the wide multiplier). This is the equivalence proof that the netlist the shipping emitter ships (same builder, TEXT sink) is the one the Verifier proves correct. a=20 b=4. Known answer (FAIL LOUD): "stub=17 div=24" rc=0.

dependencies 2 imports · 0 importers

nx_alu_select.nx rv64im_min_alu.nx nx_alu_select_mem_test.nx

imports: nx_alu_select.nxrv64im_min_alu.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main _run_census nx_sink_init_mem nx_alu_build_select nx_sink_const nx_hdl_wire nx_hdl_signal_alloc nx_hdl_kind_is_valid nx_hdl_width_is_valid nx_div_synth_sink nx_sink_const ↻ nx_sink_cell nx_hdl_wire ↻ sys_mmap nx_alu_mulh_sink nx_mul_wide_sink nx_sink_const ↻ nx_sink_cell ↻ nx_sink_const ↻ nx_sink_cell ↻ nx_wdiv_u_sink nx_sink_const ↻ nx_sink_cell ↻ nx_div_synth_sink ↻ nx_sext32_sink nx_sink_const ↻ nx_sink_cell ↻ nx_wdiv_s_sink nx_sink_const ↻ nx_sext32_sink ↻ nx_sink_cell ↻ nx_div_synth_sink ↻ nx_alu_op_to_gate_kind nx_sink_cell ↻ nx_gsim_run nx_gsim_kind_supported nx_gsim_eval_cell nx_rv64im_alu_compute nx_rv64im_lshr nx_rv64im_ltu

structs

none

consts

none

functions

13func _emit_cstr(s: *u8) -> i64
called by 1: main
19func _emit_dec(v: i64) -> i64
called by 1: main
33func _run_census(g: *NxGsim, a: i64, b: i64, use_div: i64) -> i64
called by 1: main calls 4: nx_sink_init_memnx_alu_build_selectnx_gsim_runnx_rv64im_alu_compute
54func main() -> i64
calls 3: _run_census_emit_cstr_emit_dec