3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-02-14 12:51:48 +00:00
This commit is contained in:
Gus Smith 2026-02-03 14:41:08 -08:00
parent 44afd4bbdd
commit 3f01d7a33a

View file

@ -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