From 818b25d1dfdb4b1c546fb9dabb7d31f61fd88c68 Mon Sep 17 00:00:00 2001 From: jackthepunished Date: Sat, 8 Aug 2026 15:16:23 +0300 Subject: [PATCH] feat(synth): yosys zero-multiplier assertion and xilinx area stats zero_mult.ys: hierarchy -check + assert-count 0 on $mul/$div/$mod/$pow - passes. synth_xilinx stat: LUT 63697 (45181 LUT6), FF 11624, RAMB36E1 24, DSP 0, MUXF7/8 20133, CARRY4 3894. LUTs land ~3x the plan estimate: the per-tap dynamic weight-code part-selects synthesize as 144 parallel byte-mux trees per layer. M5 note: reorganizing weight ROMs as C_OUT-indexed wide-word BRAM reads should reclaim most of the LUT6/MUXF budget. Also fixes the plan's DSP guard (anchored grep - the yosys log mentions DSP48 while loading the cell library - and if/exit instead of a subshell exit that || silently swallowed). --- .gitignore | 1 + Makefile | 22 ++++++++++++++++++++++ docs/plans/2026-08-07-phase4-m4-rtl.md | 8 ++++++-- synth/xilinx_stat.ys | 6 ++++++ synth/zero_mult.ys | 8 ++++++++ 5 files changed, 43 insertions(+), 2 deletions(-) create mode 100644 synth/xilinx_stat.ys create mode 100644 synth/zero_mult.ys diff --git a/.gitignore b/.gitignore index 2596afd..6c66752 100644 --- a/.gitignore +++ b/.gitignore @@ -36,3 +36,4 @@ ternoise.egg-info/ /host_app /test_quantize /stb_impl.o +synth/case04/ diff --git a/Makefile b/Makefile index 80ff2dd..5a72759 100644 --- a/Makefile +++ b/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 diff --git a/docs/plans/2026-08-07-phase4-m4-rtl.md b/docs/plans/2026-08-07-phase4-m4-rtl.md index 311a06d..aa10a57 100644 --- a/docs/plans/2026-08-07-phase4-m4-rtl.md +++ b/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 diff --git a/synth/xilinx_stat.ys b/synth/xilinx_stat.ys new file mode 100644 index 0000000..be8c360 --- /dev/null +++ b/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 diff --git a/synth/zero_mult.ys b/synth/zero_mult.ys new file mode 100644 index 0000000..17b4e2d --- /dev/null +++ b/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