read_verilog <<EOT
module top(
	input  signed [7:0] A,
	input  signed [7:0] D,
	input  signed [7:0] B,
	output signed [16:0] P
);
	assign P = (A - 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
