From 3f01d7a33ae27df8f1d120dce082b02e526e8a0c Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Tue, 3 Feb 2026 14:41:08 -0800
Subject: [PATCH] Add test

---
 tests/arch/xilinx/dsp_preadder_sub.ys | 41 +++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 tests/arch/xilinx/dsp_preadder_sub.ys

diff --git a/tests/arch/xilinx/dsp_preadder_sub.ys b/tests/arch/xilinx/dsp_preadder_sub.ys
new file mode 100644
index 000000000..04e5e9da0
--- /dev/null
+++ b/tests/arch/xilinx/dsp_preadder_sub.ys
@@ -0,0 +1,41 @@
+read_verilog <<EOT
+module top(
+	// NOTE: This test is intentionally "bitwidth-shaped" to match the current
+	// pre-subtractor matcher in `techlibs/xilinx/xilinx_dsp.pmg`.
+	//
+	// The `preSub` pattern requires `port(preSub, \\Y) === sigA` (SigSpec identity),
+	// where `sigA` is the (typically 25-bit) signal feeding the DSP multiplier
+	// A-side after sign-extension into the DSP input port width.
+	//
+	// If the `$sub` result is narrower (e.g. 9-bit for 8-bit operands) and only
+	// later sign-extended up to 25 bits, that identity check fails even though the
+	// values are equivalent. Therefore we explicitly compute a 25-bit signed
+	// subtraction here so the `$sub` output is already the same SigSpec that the
+	// DSP mapping uses for the A-side input.
+	input  signed [7:0] A,
+	input  signed [7:0] D,
+	input  signed [7:0] B,
+	output signed [16:0] P
+);
+	assign P = ($signed({{17{A[7]}}, A}) - $signed({{17{D[7]}}, D})) * B;
+endmodule
+EOT
+
+proc
+design -save gold
+synth_xilinx -noiopad
+design -save gate
+cd top
+select -assert-count 1 t:DSP48E1
+select -assert-count 1 t:DSP48E1 r:USE_DPORT=TRUE %i
+select -assert-none t:DSP48E1 %% t:* %D
+
+# Now prove functional equivalence of the mapped netlist against the original
+# (saved as `gold` above).
+design -reset
+design -copy-from gold -as gold top
+design -copy-from gate -as gate top
+techmap -wb -D EQUIV -autoproc -map +/xilinx/cells_sim.v
+equiv_make gold gate equiv
+equiv_induct equiv
+equiv_status -assert equiv