feat(synth): zero-multiplier proof and area stats (M4 Task 6)

.gitignore

@@ -36,3 +36,4 @@ ternoise.egg-info/
 /host_app
 /test_quantize
 /stb_impl.o
+synth/case04/

Makefile

@@ -145,3 +145,25 @@ rtl_test: build/tb_linebuffer/tb_linebuffer build/tb_requant/tb_requant \
 	$(call TOP_RUN,vectors/case04_network,build/mem/case04_network,case04_network)
 	$(call TOP_RUN,vectors/case05_network_packed,build/mem/case05_network_packed,case05_network_packed)
 	$(call TOP_RUN,build/mem/export64_case,build/mem/export64,export64)
+
+# ---- Synthesis checks (M4 Task 6) ----
+.PHONY: synth_check mem_cases_synth
+
+# synthesis-default .mem files for $readmemh (WFILE/BFILE parameter defaults)
+mem_cases_synth:
+	@mkdir -p synth/case04
+	$(PYTHON) -m tools.case_to_mem vectors/case04_network --out synth/case04
+
+# Source rule note: * / % are banned in DATAPATH expressions; elaboration-time
+# constant math is exempt and enforced by review, not grep (see the plan).
+# No -q on yosys: it silences the log stream carrying the stat block.
+# The tee'd file is the whole yosys log; inferred cells appear only as
+# indented stat rows ("     DSP48E1   N"), so anchor the grep on leading
+# whitespace - the library-loading lines also say DSP48. An if/exit is used
+# because "(...; exit 1) || echo" swallows the failure in a subshell.
+synth_check: mem_cases_synth
+	yosys synth/zero_mult.ys
+	yosys synth/xilinx_stat.ys | tee build/xilinx_stat.txt
+	@if grep -E '^ +DSP' build/xilinx_stat.txt | grep -q .; then \
+	  echo "FAIL: DSP cells inferred"; exit 1; \
+	else echo "synth_check PASS: zero multipliers, zero DSPs"; fi

docs/plans/2026-08-07-phase4-m4-rtl.md

@@ -838,8 +838,12 @@ stat
 synth_check: mem_cases_synth
 	yosys synth/zero_mult.ys
 	yosys synth/xilinx_stat.ys | tee build/xilinx_stat.txt
-	@grep -E "DSP" build/xilinx_stat.txt | grep -qv " 0" && \
-	  (echo "FAIL: DSP cells inferred"; exit 1) || echo "synth_check PASS: zero multipliers, zero DSPs"
+	@if grep -E '^ +DSP' build/xilinx_stat.txt | grep -q .; then \
+	  echo "FAIL: DSP cells inferred"; exit 1; \
+	else echo "synth_check PASS: zero multipliers, zero DSPs"; fi
+	# anchored grep: the log's library-loading lines also mention DSP48;
+	# if/exit because "(...; exit 1) || echo" swallows the subshell failure
+	# (both found during Task 6 execution)
 
 mem_cases_synth:  # synthesis-default .mem files must exist for $readmemh
 	mkdir -p synth/case04

synth/xilinx_stat.ys

@@ -0,0 +1,6 @@
+# Xilinx-mapped area estimate: the LUT/BRAM/DSP numbers that pick the M5
+# board. The DSP row of this stat output must read zero (checked by make).
+read_verilog -sv -DSYNTHESIS rtl/pe.sv rtl/requant.sv rtl/linebuffer.sv rtl/conv3x3.sv rtl/delay_fifo.sv rtl/denoiser_top.sv
+hierarchy -check -top denoiser_top
+synth_xilinx -top denoiser_top
+stat

synth/zero_mult.ys

@@ -0,0 +1,8 @@
+# Technology-independent proof: no multiplier/divider cells anywhere in the
+# netlist. -check is load-bearing: without it a missing module is silently
+# blackboxed and the assertion passes vacuously.
+read_verilog -sv -DSYNTHESIS rtl/pe.sv rtl/requant.sv rtl/linebuffer.sv rtl/conv3x3.sv rtl/delay_fifo.sv rtl/denoiser_top.sv
+hierarchy -check -top denoiser_top
+proc; opt; memory -nomap; opt
+select -assert-count 0 t:$mul t:$div t:$mod t:$pow
+stat