diff options
Diffstat (limited to 'tests/arch/xilinx')
38 files changed, 1630 insertions, 0 deletions
diff --git a/tests/arch/xilinx/.gitignore b/tests/arch/xilinx/.gitignore new file mode 100644 index 000000000..c99b79371 --- /dev/null +++ b/tests/arch/xilinx/.gitignore @@ -0,0 +1,5 @@ +/*.log +/*.out +/run-test.mk +/*_uut.v +/test_macc diff --git a/tests/arch/xilinx/abc9_dff.ys b/tests/arch/xilinx/abc9_dff.ys new file mode 100644 index 000000000..b457cefce --- /dev/null +++ b/tests/arch/xilinx/abc9_dff.ys @@ -0,0 +1,32 @@ +read_verilog <<EOT +module top(input C, D, output [7:0] Q); +FDRE fd1(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[0])); +FDSE fd2(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[1])); +FDCE fd3(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[2])); +FDPE fd4(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[3])); +FDRE_1 fd5(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[4])); +FDSE_1 fd6(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[5])); +FDCE_1 fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6])); +FDPE_1 fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7])); +endmodule +EOT +equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf +design -load postopt +select -assert-none t:FD* + +design -reset +read_verilog <<EOT +module top(input C, D, output [7:0] Q); +FDRE fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0])); +FDSE fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1])); +FDCE fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2])); +FDPE fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3])); +FDRE_1 fd5(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[4])); +FDSE_1 fd6(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[5])); +FDCE_1 fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6])); +FDPE_1 fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7])); +endmodule +EOT +equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf +design -load postopt +select -assert-none t:FD* diff --git a/tests/arch/xilinx/abc9_map.ys b/tests/arch/xilinx/abc9_map.ys new file mode 100644 index 000000000..4a7b9384a --- /dev/null +++ b/tests/arch/xilinx/abc9_map.ys @@ -0,0 +1,91 @@ +read_verilog <<EOT +module top(input C, CE, D, R, output [1:0] Q); +FDRE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[0])); +FDRE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[1])); +endmodule +EOT +design -save gold + +techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE +techmap -map +/xilinx/abc9_unmap.v +select -assert-count 1 t:FDSE +select -assert-count 1 t:FDSE_1 +techmap -autoproc -map +/xilinx/cells_sim.v +design -stash gate + +design -import gold -as gold +design -import gate -as gate +techmap -autoproc -map +/xilinx/cells_sim.v + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -seq 2 -verify -prove-asserts -show-ports miter + +design -reset +read_verilog <<EOT +module top(input C, CE, D, S, output [1:0] Q); +FDSE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[0])); +FDSE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[1])); +endmodule +EOT +design -save gold + +techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE +techmap -map +/xilinx/abc9_unmap.v +select -assert-count 1 t:FDRE +select -assert-count 1 t:FDRE_1 +techmap -autoproc -map +/xilinx/cells_sim.v +design -stash gate + +design -import gold -as gold +design -import gate -as gate +techmap -autoproc -map +/xilinx/cells_sim.v + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter + +design -reset +read_verilog <<EOT +module top(input C, CE, D, PRE, output [1:0] Q); +FDPE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[0])); +FDPE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[1])); +endmodule +EOT +design -save gold + +techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE +techmap -map +/xilinx/abc9_unmap.v +select -assert-count 1 t:FDCE +select -assert-count 1 t:FDCE_1 +techmap -autoproc -map +/xilinx/cells_sim.v +design -stash gate + +design -import gold -as gold +design -import gate -as gate +techmap -autoproc -map +/xilinx/cells_sim.v +clk2fflogic + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter + +design -reset +read_verilog <<EOT +module top(input C, CE, D, CLR, output [1:0] Q); +FDCE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[0])); +FDCE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[1])); +endmodule +EOT +design -save gold + +techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE +techmap -map +/xilinx/abc9_unmap.v +select -assert-count 1 t:FDPE +techmap -autoproc -map +/xilinx/cells_sim.v +design -stash gate + +design -import gold -as gold +design -import gate -as gate +techmap -autoproc -map +/xilinx/cells_sim.v +clk2fflogic + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter diff --git a/tests/arch/xilinx/add_sub.ys b/tests/arch/xilinx/add_sub.ys new file mode 100644 index 000000000..70cfe81a3 --- /dev/null +++ b/tests/arch/xilinx/add_sub.ys @@ -0,0 +1,11 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +stat +select -assert-count 16 t:LUT2 +select -assert-count 2 t:CARRY4 +select -assert-none t:LUT2 t:CARRY4 %% t:* %D + diff --git a/tests/arch/xilinx/adffs.ys b/tests/arch/xilinx/adffs.ys new file mode 100644 index 000000000..3328f9edc --- /dev/null +++ b/tests/arch/xilinx/adffs.ys @@ -0,0 +1,50 @@ +read_verilog ../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd adff # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDCE + +select -assert-none t:BUFG t:FDCE %% t:* %D + + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd adffn # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDCE +select -assert-count 1 t:INV + +select -assert-none t:BUFG t:FDCE t:INV %% t:* %D + + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd dffs # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDSE + +select -assert-none t:BUFG t:FDSE %% t:* %D + + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd ndffnr # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDRE_1 +select -assert-count 1 t:INV + +select -assert-none t:BUFG t:FDRE_1 t:INV %% t:* %D diff --git a/tests/arch/xilinx/attributes_test.ys b/tests/arch/xilinx/attributes_test.ys new file mode 100644 index 000000000..7bdd94a63 --- /dev/null +++ b/tests/arch/xilinx/attributes_test.ys @@ -0,0 +1,47 @@ +# Check that blockram memory without parameters is not modified +read_verilog ../common/memory_attributes/attributes_test.v +hierarchy -top block_ram +synth_xilinx -top block_ram -noiopad +cd block_ram # Constrain all select calls below inside the top module +select -assert-count 1 t:RAMB18E1 + +# Check that distributed memory without parameters is not modified +design -reset +read_verilog ../common/memory_attributes/attributes_test.v +hierarchy -top distributed_ram +synth_xilinx -top distributed_ram -noiopad +cd distributed_ram # Constrain all select calls below inside the top module +select -assert-count 8 t:RAM32X1D + +# Set ram_style distributed to blockram memory; will be implemented as distributed +design -reset +read_verilog ../common/memory_attributes/attributes_test.v +prep +setattr -mod -set ram_style "distributed" block_ram +synth_xilinx -top block_ram -noiopad +cd block_ram # Constrain all select calls below inside the top module +select -assert-count 32 t:RAM128X1D + +# Set synthesis, logic_block to blockram memory; will be implemented as distributed +design -reset +read_verilog ../common/memory_attributes/attributes_test.v +prep +setattr -mod -set logic_block 1 block_ram +synth_xilinx -top block_ram -noiopad +cd block_ram # Constrain all select calls below inside the top module +select -assert-count 0 t:RAMB18E1 +select -assert-count 32 t:RAM128X1D + +# Set ram_style block to a distributed memory; will be implemented as blockram +design -reset +read_verilog ../common/memory_attributes/attributes_test.v +synth_xilinx -top distributed_ram_manual -noiopad +cd distributed_ram_manual # Constrain all select calls below inside the top module +select -assert-count 1 t:RAMB18E1 + +# Set synthesis, ram_block block to a distributed memory; will be implemented as blockram +design -reset +read_verilog ../common/memory_attributes/attributes_test.v +synth_xilinx -top distributed_ram_manual_syn -noiopad +cd distributed_ram_manual_syn # Constrain all select calls below inside the top module +select -assert-count 1 t:RAMB18E1 diff --git a/tests/arch/xilinx/blockram.ys b/tests/arch/xilinx/blockram.ys new file mode 100644 index 000000000..ed743cf44 --- /dev/null +++ b/tests/arch/xilinx/blockram.ys @@ -0,0 +1,97 @@ +### TODO: Not running equivalence checking because BRAM models does not exists +### currently. Checking instance counts instead. +# Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RAMB18E1 +read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 1 sync_ram_sdp +synth_xilinx -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 1 t:RAMB18E1 + +design -reset +read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 18 sync_ram_sdp +synth_xilinx -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 1 t:RAMB18E1 + +design -reset +read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp +synth_xilinx -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 1 t:RAMB18E1 + +design -reset +read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp +synth_xilinx -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 1 t:RAMB18E1 + +# Anything memory bits < 1024 -> LUTRAM +design -reset +read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 2 sync_ram_sdp +synth_xilinx -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 0 t:RAMB18E1 +select -assert-count 4 t:RAM128X1D + +# More than 18K bits, data width <= 36 (TDP), and address width from 10 to 15b (non-cascaded) -> RAMB36E1 +design -reset +read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 36 sync_ram_sdp +synth_xilinx -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 1 t:RAMB36E1 + + +### With parameters + +design -reset +read_verilog ../common/blockram.v +hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 +setattr -set ram_style "block" m:memory +synth_xilinx -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 1 t:RAMB18E1 + +design -reset +read_verilog ../common/blockram.v +hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 +setattr -set ram_block 1 m:memory +synth_xilinx -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 1 t:RAMB18E1 + +design -reset +read_verilog ../common/blockram.v +hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 +setattr -set ram_style "dont_infer_a_ram_pretty_please" m:memory +synth_xilinx -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 0 t:RAMB18E1 + +design -reset +read_verilog ../common/blockram.v +hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 +setattr -set logic_block 1 m:memory +synth_xilinx -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 0 t:RAMB18E1 + +design -reset +read_verilog ../common/blockram.v +hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1 +setattr -set ram_style "block" m:memory +synth_xilinx -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 1 t:RAMB18E1 + +design -reset +read_verilog ../common/blockram.v +hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1 +setattr -set ram_block 1 m:memory +synth_xilinx -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 1 t:RAMB18E1 diff --git a/tests/arch/xilinx/bug1460.ys b/tests/arch/xilinx/bug1460.ys new file mode 100644 index 000000000..09935ccd8 --- /dev/null +++ b/tests/arch/xilinx/bug1460.ys @@ -0,0 +1,34 @@ +read_verilog <<EOT +module register_file( + input wire clk, + input wire write_enable, + input wire [63:0] write_data, + input wire [4:0] write_reg, + input wire [4:0] read1_reg, + input wire [4:0] read2_reg, + input wire [4:0] read3_reg, + output reg [63:0] read1_data, + output reg [63:0] read2_data, + output reg [63:0] read3_data + ); + + reg [63:0] registers[0:31]; + + always @(posedge clk) begin + if (write_enable == 1'b1) begin + registers[write_reg] <= write_data; + end + end + + always @(all) begin + read1_data <= registers[read1_reg]; + read2_data <= registers[read2_reg]; + read3_data <= registers[read3_reg]; + end +endmodule +EOT + +synth_xilinx -noiopad +cd register_file +select -assert-count 32 t:RAM32M +select -assert-none t:* t:BUFG %d t:RAM32M %d diff --git a/tests/arch/xilinx/bug1462.ys b/tests/arch/xilinx/bug1462.ys new file mode 100644 index 000000000..15cab5121 --- /dev/null +++ b/tests/arch/xilinx/bug1462.ys @@ -0,0 +1,11 @@ +read_verilog << EOF +module top(...); +input wire [31:0] A; +output wire [31:0] P; + +assign P = A * 32'h12300000; + +endmodule +EOF + +synth_xilinx diff --git a/tests/arch/xilinx/bug1598.ys b/tests/arch/xilinx/bug1598.ys new file mode 100644 index 000000000..1175380b1 --- /dev/null +++ b/tests/arch/xilinx/bug1598.ys @@ -0,0 +1,16 @@ +read_verilog <<EOT +module led_blink ( + input clk, + output ledc + ); + + reg [6:0] led_counter = 0; + always @( posedge clk ) begin + led_counter <= led_counter + 1; + end + assign ledc = !led_counter[ 6:3 ]; + +endmodule +EOT +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -abc9 diff --git a/tests/arch/xilinx/bug1605.ys b/tests/arch/xilinx/bug1605.ys new file mode 100644 index 000000000..4be659860 --- /dev/null +++ b/tests/arch/xilinx/bug1605.ys @@ -0,0 +1,19 @@ +read_verilog <<EOT +module top(inout io); + wire in; + wire t; + wire o; + + IOBUF IOBUF( + .I(in), + .T(t), + .IO(io), + .O(o) + ); +endmodule +EOT + +synth_xilinx +cd top +select -assert-count 1 t:IOBUF +select -assert-none t:* t:IOBUF %d diff --git a/tests/arch/xilinx/counter.ys b/tests/arch/xilinx/counter.ys new file mode 100644 index 000000000..064519ce7 --- /dev/null +++ b/tests/arch/xilinx/counter.ys @@ -0,0 +1,13 @@ +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +stat +select -assert-count 1 t:BUFG +select -assert-count 8 t:FDCE +select -assert-count 1 t:INV +select -assert-count 2 t:CARRY4 +select -assert-none t:BUFG t:FDCE t:INV t:CARRY4 %% t:* %D diff --git a/tests/arch/xilinx/dffs.ys b/tests/arch/xilinx/dffs.ys new file mode 100644 index 000000000..dc764b033 --- /dev/null +++ b/tests/arch/xilinx/dffs.ys @@ -0,0 +1,25 @@ +read_verilog ../common/dffs.v +design -save read + +hierarchy -top dff +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd dff # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDRE + +select -assert-none t:BUFG t:FDRE %% t:* %D + + +design -load read +hierarchy -top dffe +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd dffe # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDRE + +select -assert-none t:BUFG t:FDRE %% t:* %D + diff --git a/tests/arch/xilinx/dsp_cascade.ys b/tests/arch/xilinx/dsp_cascade.ys new file mode 100644 index 000000000..ca6b619b9 --- /dev/null +++ b/tests/arch/xilinx/dsp_cascade.ys @@ -0,0 +1,89 @@ +design -reset +read_verilog <<EOT +module cascade(input clk, input [4:0] a, input [4:0] b, output reg [9:0] o); +reg [4:0] ar1, ar2, ar3, br1, br2, br3; +reg [9:0] m, n; +always @(posedge clk) begin +ar1 <= a; +ar2 <= ar1; +ar3 <= ar2; +br1 <= b; +br2 <= br1; +br3 <= br2; +m <= ar1 * br1; +n <= ar2 * br2 + m; +o <= ar3 * br3 + n; +end +endmodule +EOT +proc +design -save read + +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad +design -load postopt +cd cascade +select -assert-count 3 t:DSP48E1 +select -assert-none t:DSP48E1 t:BUFG %% t:* %D +# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN +# (i.e. Take all DSP48E1s, expand to find all wires connected +# to its PCOUT port, then remove all DSP48E1s from this +# selection, then expand again to find all cells where +# those wires are connected to the PCIN port, then remove +# all wires from this selection, and lastly intersect +# this selection with all DSP48E1 cells (to check that +# the connected cells are indeed DSPs) +select -assert-count 2 t:DSP48E1 %co:+[PCOUT] t:DSP48E1 %d %co:+[PCIN] w:* %d t:DSP48E1 %i + +design -load read +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad +design -load postopt +cd cascade +select -assert-count 3 t:DSP48A1 +select -assert-count 5 t:FDRE # No cascade for A input +select -assert-none t:DSP48A1 t:BUFG t:FDRE %% t:* %D +# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN +# (see above for explanation) +select -assert-count 2 t:DSP48A1 %co:+[PCOUT] t:DSP48A1 %d %co:+[PCIN] w:* %d t:DSP48A1 %i + +design -reset +read_verilog <<EOT +module cascade(input clk, input [4:0] a, input [4:0] b, output reg [9:0] o); +reg [4:0] ar1, ar2, ar3, br1, br2, br3; +reg [9:0] m; +always @(posedge clk) begin +ar1 <= a; +ar2 <= ar1; +ar3 <= ar2; +br1 <= b; +br2 <= br1; +br3 <= br2; +m <= ar2 * br2; +o <= ar3 * br3 + m; +end +endmodule +EOT +proc +design -save read + +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad +design -load postopt +cd cascade +select -assert-count 2 t:DSP48E1 +select -assert-none t:DSP48E1 t:BUFG %% t:* %D +# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN +# (see above for explanation) +select -assert-count 1 t:DSP48E1 %co:+[PCOUT] t:DSP48E1 %d %co:+[PCIN] w:* %d t:DSP48E1 %i + +design -load read +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad +design -load postopt +cd cascade +select -assert-count 2 t:DSP48A1 +select -assert-count 10 t:FDRE # Cannot cascade because first 'm' DSP + # uses both B0REG and B1REG, whereas 'o' + # only requires 1 +select -assert-none t:DSP48A1 t:BUFG t:FDRE %% t:* %D +# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN +# (see above for explanation) +select -assert-count 1 t:DSP48A1 %co:+[PCOUT] t:DSP48A1 %d %co:+[PCIN] w:* %d t:DSP48A1 %i + diff --git a/tests/arch/xilinx/dsp_fastfir.ys b/tests/arch/xilinx/dsp_fastfir.ys new file mode 100644 index 000000000..57fe49bde --- /dev/null +++ b/tests/arch/xilinx/dsp_fastfir.ys @@ -0,0 +1,69 @@ +read_verilog <<EOT +// Citation https://github.com/ZipCPU/dspfilters/blob/master/rtl/fastfir.v +module fastfir_dynamictaps(i_clk, i_reset, i_tap_wr, i_tap, i_ce, i_sample, o_result); + wire [30:0] _00_; + wire [23:0] _01_; + wire [11:0] _02_; + wire [30:0] _03_; + wire [23:0] _04_; + wire [30:0] _05_; + wire [23:0] _06_; + wire [30:0] _07_; + wire [23:0] _08_; + wire [11:0] _09_; + wire [30:0] _10_; + wire [23:0] _11_; + wire [30:0] _12_; + wire [23:0] _13_; + wire [11:0] \fir.FILTER[0].tapk.delayed_sample ; + reg [30:0] \fir.FILTER[0].tapk.o_acc = 31'h00000000; + wire [11:0] \fir.FILTER[0].tapk.o_sample ; + reg [23:0] \fir.FILTER[0].tapk.product ; + reg [11:0] \fir.FILTER[0].tapk.tap = 12'h000; + wire [11:0] \fir.FILTER[1].tapk.delayed_sample ; + wire [30:0] \fir.FILTER[1].tapk.o_acc ; + wire [11:0] \fir.FILTER[1].tapk.o_sample ; + reg [23:0] \fir.FILTER[1].tapk.product ; + reg [11:0] \fir.FILTER[1].tapk.tap = 12'h000; + input i_ce; + input i_clk; + input i_reset; + input [11:0] i_sample; + input [11:0] i_tap; + input i_tap_wr; + output [30:0] o_result; + reg [30:0] o_result; + assign _03_ = 31'h00000000 + { \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product }; + assign _04_ = $signed(\fir.FILTER[0].tapk.tap ) * $signed(i_sample); + always @(posedge i_clk) + \fir.FILTER[0].tapk.tap <= _02_; + always @(posedge i_clk) + \fir.FILTER[0].tapk.o_acc <= _00_; + always @(posedge i_clk) + \fir.FILTER[0].tapk.product <= _01_; + assign _02_ = i_tap_wr ? i_tap : \fir.FILTER[0].tapk.tap ; + assign _05_ = i_ce ? _03_ : \fir.FILTER[0].tapk.o_acc ; + assign _00_ = i_reset ? 31'h00000000 : _05_; + assign _06_ = i_ce ? _04_ : \fir.FILTER[0].tapk.product ; + assign _01_ = i_reset ? 24'h000000 : _06_; + assign _10_ = \fir.FILTER[0].tapk.o_acc + { \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product }; + assign _11_ = $signed(\fir.FILTER[1].tapk.tap ) * $signed(i_sample); + always @(posedge i_clk) + \fir.FILTER[1].tapk.tap <= _09_; + always @(posedge i_clk) + o_result <= _07_; + always @(posedge i_clk) + \fir.FILTER[1].tapk.product <= _08_; + assign _09_ = i_tap_wr ? \fir.FILTER[0].tapk.tap : \fir.FILTER[1].tapk.tap ; + assign _12_ = i_ce ? _10_ : o_result; + assign _07_ = i_reset ? 31'h00000000 : _12_; + assign _13_ = i_ce ? _11_ : \fir.FILTER[1].tapk.product ; + assign _08_ = i_reset ? 24'h000000 : _13_; + assign \fir.FILTER[1].tapk.o_acc = o_result; +endmodule +EOT + +synth_xilinx -noiopad +cd fastfir_dynamictaps +select -assert-count 2 t:DSP48E1 +select -assert-none t:* t:DSP48E1 %d t:BUFG %d diff --git a/tests/arch/xilinx/dsp_simd.ys b/tests/arch/xilinx/dsp_simd.ys new file mode 100644 index 000000000..956952327 --- /dev/null +++ b/tests/arch/xilinx/dsp_simd.ys @@ -0,0 +1,25 @@ +read_verilog <<EOT +module simd(input [12*4-1:0] a, input [12*4-1:0] b, (* use_dsp="simd" *) output [7*12-1:0] o12, (* use_dsp="simd" *) output [2*24-1:0] o24); +generate + genvar i; + // 4 x 12-bit adder + for (i = 0; i < 4; i++) + assign o12[i*12+:12] = a[i*12+:12] + b[i*12+:12]; + // 2 x 24-bit subtract + for (i = 0; i < 2; i++) + assign o24[i*24+:24] = a[i*24+:24] - b[i*24+:24]; +endgenerate +reg [3*12-1:0] ro; +always @* begin + ro[0*12+:12] = a[0*10+:10] + b[0*10+:10]; + ro[1*12+:12] = a[1*10+:10] + b[1*10+:10]; + ro[2*12+:12] = a[2*8+:8] + b[2*8+:8]; +end +assign o12[4*12+:3*12] = ro; +endmodule +EOT + +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx +design -load postopt +select -assert-count 3 t:DSP48E1 diff --git a/tests/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys new file mode 100644 index 000000000..a464fcfdb --- /dev/null +++ b/tests/arch/xilinx/fsm.ys @@ -0,0 +1,19 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten + +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad +miter -equiv -make_assert -flatten gold gate miter +sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter + +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd fsm # Constrain all select calls below inside the top module +stat +select -assert-count 1 t:BUFG +select -assert-count 4 t:FDRE +select -assert-count 1 t:FDSE +select -assert-count 1 t:LUT2 +select -assert-count 3 t:LUT5 +select -assert-count 1 t:LUT6 +select -assert-none t:BUFG t:FDRE t:FDSE t:LUT2 t:LUT5 t:LUT6 %% t:* %D diff --git a/tests/arch/xilinx/latches.ys b/tests/arch/xilinx/latches.ys new file mode 100644 index 000000000..e226c2ec8 --- /dev/null +++ b/tests/arch/xilinx/latches.ys @@ -0,0 +1,35 @@ +read_verilog ../common/latches.v +design -save read + +hierarchy -top latchp +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd latchp # Constrain all select calls below inside the top module +select -assert-count 1 t:LDCE + +select -assert-none t:LDCE %% t:* %D + + +design -load read +hierarchy -top latchn +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:LDCE +select -assert-count 1 t:INV + +select -assert-none t:LDCE t:INV %% t:* %D + + +design -load read +hierarchy -top latchsr +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd latchsr # Constrain all select calls below inside the top module +select -assert-count 1 t:LDCE +select -assert-count 2 t:LUT3 + +select -assert-none t:LDCE t:LUT3 %% t:* %D diff --git a/tests/arch/xilinx/logic.ys b/tests/arch/xilinx/logic.ys new file mode 100644 index 000000000..61a9314cc --- /dev/null +++ b/tests/arch/xilinx/logic.ys @@ -0,0 +1,11 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:INV +select -assert-count 6 t:LUT2 +select -assert-count 2 t:LUT4 +select -assert-none t:INV t:LUT2 t:LUT4 %% t:* %D diff --git a/tests/arch/xilinx/lutram.ys b/tests/arch/xilinx/lutram.ys new file mode 100644 index 000000000..3f127a77e --- /dev/null +++ b/tests/arch/xilinx/lutram.ys @@ -0,0 +1,137 @@ +#read_verilog ../common/lutram.v +#hierarchy -top lutram_1w1r -chparam A_WIDTH 4 +#proc +#memory -nomap +#equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad +#memory +#opt -full +# +#miter -equiv -flatten -make_assert -make_outputs gold gate miter +#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter +# +#design -load postopt +#cd lutram_1w1r +#select -assert-count 1 t:BUFG +#select -assert-count 8 t:FDRE +#select -assert-count 8 t:RAM16X1D +#select -assert-none t:BUFG t:FDRE t:RAM16X1D %% t:* %D + + +design -reset +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r -chparam A_WIDTH 5 +proc +memory -nomap +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd lutram_1w1r +select -assert-count 1 t:BUFG +select -assert-count 8 t:FDRE +select -assert-count 8 t:RAM32X1D +select -assert-none t:BUFG t:FDRE t:RAM32X1D %% t:* %D + + +design -reset +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r +proc +memory -nomap +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd lutram_1w1r +select -assert-count 1 t:BUFG +select -assert-count 8 t:FDRE +select -assert-count 8 t:RAM64X1D +select -assert-none t:BUFG t:FDRE t:RAM64X1D %% t:* %D + + +design -reset +read_verilog ../common/lutram.v +hierarchy -top lutram_1w3r +proc +memory -nomap +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd lutram_1w3r +select -assert-count 1 t:BUFG +select -assert-count 24 t:FDRE +select -assert-count 4 t:RAM32M +select -assert-none t:BUFG t:FDRE t:RAM32M %% t:* %D + + +design -reset +read_verilog ../common/lutram.v +hierarchy -top lutram_1w3r -chparam A_WIDTH 6 +proc +memory -nomap +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd lutram_1w3r +select -assert-count 1 t:BUFG +select -assert-count 24 t:FDRE +select -assert-count 8 t:RAM64M +select -assert-none t:BUFG t:FDRE t:RAM64M %% t:* %D + + +design -reset +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6 +proc +memory -nomap +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd lutram_1w1r +select -assert-count 1 t:BUFG +select -assert-count 6 t:FDRE +select -assert-count 1 t:RAM32M +select -assert-none t:BUFG t:FDRE t:RAM32M %% t:* %D + + +design -reset +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6 +proc +memory -nomap +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd lutram_1w1r +select -assert-count 1 t:BUFG +select -assert-count 6 t:FDRE +select -assert-count 2 t:RAM64M +select -assert-none t:BUFG t:FDRE t:RAM64M %% t:* %D diff --git a/tests/arch/xilinx/macc.sh b/tests/arch/xilinx/macc.sh new file mode 100644 index 000000000..58b97b646 --- /dev/null +++ b/tests/arch/xilinx/macc.sh @@ -0,0 +1,6 @@ +../../../yosys -qp "synth_xilinx -top macc2; rename -top macc2_uut" -o macc_uut.v macc.v +iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../../techlibs/xilinx/cells_sim.v +vvp -N ./test_macc +../../../yosys -qp "synth_xilinx -family xc6s -top macc2; rename -top macc2_uut" -o macc_uut.v macc.v +iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../../techlibs/xilinx/cells_sim.v +vvp -N ./test_macc diff --git a/tests/arch/xilinx/macc.v b/tests/arch/xilinx/macc.v new file mode 100644 index 000000000..e36b2bab1 --- /dev/null +++ b/tests/arch/xilinx/macc.v @@ -0,0 +1,84 @@ +// Signed 40-bit streaming accumulator with 16-bit inputs +// File: HDL_Coding_Techniques/multipliers/multipliers4.v +// +// Source: +// https://www.xilinx.com/support/documentation/sw_manuals/xilinx2014_2/ug901-vivado-synthesis.pdf p.90 +// +module macc # (parameter SIZEIN = 16, SIZEOUT = 40) ( + input clk, ce, sload, + input signed [SIZEIN-1:0] a, b, + output signed [SIZEOUT-1:0] accum_out +); +// Declare registers for intermediate values +reg signed [SIZEIN-1:0] a_reg, b_reg; +reg sload_reg; +reg signed [2*SIZEIN-1:0] mult_reg; +reg signed [SIZEOUT-1:0] adder_out, old_result; +always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch + if (sload_reg) + old_result <= 0; + else + // 'sload' is now active (=low) and opens the accumulation loop. + // The accumulator takes the next multiplier output in + // the same cycle. + old_result <= adder_out; +end + +always @(posedge clk) + if (ce) + begin + a_reg <= a; + b_reg <= b; + mult_reg <= a_reg * b_reg; + sload_reg <= sload; + // Store accumulation result into a register + adder_out <= old_result + mult_reg; + end + +// Output accumulation result +assign accum_out = adder_out; + +endmodule + +// Adapted variant of above +module macc2 # (parameter SIZEIN = 16, SIZEOUT = 40) ( + input clk, + input ce, + input rst, + input signed [SIZEIN-1:0] a, b, + output signed [SIZEOUT-1:0] accum_out, + output overflow +); +// Declare registers for intermediate values +reg signed [SIZEIN-1:0] a_reg, b_reg, a_reg2, b_reg2; +reg signed [2*SIZEIN-1:0] mult_reg = 0; +reg signed [SIZEOUT:0] adder_out = 0; +reg overflow_reg; +always @(posedge clk) begin + //if (ce) + begin + a_reg <= a; + b_reg <= b; + a_reg2 <= a_reg; + b_reg2 <= b_reg; + mult_reg <= a_reg2 * b_reg2; + // Store accumulation result into a register + adder_out <= adder_out + mult_reg; + overflow_reg <= overflow; + end + if (rst) begin + a_reg <= 0; + a_reg2 <= 0; + b_reg <= 0; + b_reg2 <= 0; + mult_reg <= 0; + adder_out <= 0; + overflow_reg <= 1'b0; + end +end +assign overflow = (adder_out >= 2**(SIZEOUT-1)) | overflow_reg; + +// Output accumulation result +assign accum_out = overflow ? 2**(SIZEOUT-1)-1 : adder_out; + +endmodule diff --git a/tests/arch/xilinx/macc.ys b/tests/arch/xilinx/macc.ys new file mode 100644 index 000000000..bf2b36320 --- /dev/null +++ b/tests/arch/xilinx/macc.ys @@ -0,0 +1,32 @@ +read_verilog macc.v +design -save read + +hierarchy -top macc +proc +#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd macc # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDRE +select -assert-count 1 t:DSP48E1 +select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D + +design -load read +hierarchy -top macc2 +proc +#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd macc2 # Constrain all select calls below inside the top module + +select -assert-count 1 t:BUFG +select -assert-count 1 t:DSP48E1 +select -assert-count 1 t:FDRE +select -assert-count 1 t:LUT2 +select -assert-count 40 t:LUT3 +select -assert-none t:BUFG t:DSP48E1 t:FDRE t:LUT2 t:LUT3 %% t:* %D diff --git a/tests/arch/xilinx/macc_tb.v b/tests/arch/xilinx/macc_tb.v new file mode 100644 index 000000000..64aed05c4 --- /dev/null +++ b/tests/arch/xilinx/macc_tb.v @@ -0,0 +1,96 @@ +`timescale 1ns / 1ps + +module testbench; + + parameter SIZEIN = 16, SIZEOUT = 40; + reg clk, ce, rst; + reg signed [SIZEIN-1:0] a, b; + output signed [SIZEOUT-1:0] REF_accum_out, accum_out; + output REF_overflow, overflow; + + integer errcount = 0; + + reg ERROR_FLAG = 0; + + task clkcycle; + begin + #5; + clk = ~clk; + #10; + clk = ~clk; + #2; + ERROR_FLAG = 0; + if (REF_accum_out !== accum_out) begin + $display("ERROR at %1t: REF_accum_out=%b UUT_accum_out=%b DIFF=%b", $time, REF_accum_out, accum_out, REF_accum_out ^ accum_out); + errcount = errcount + 1; + ERROR_FLAG = 1; + end + if (REF_overflow !== overflow) begin + $display("ERROR at %1t: REF_overflow=%b UUT_overflow=%b DIFF=%b", $time, REF_overflow, overflow, REF_overflow ^ overflow); + errcount = errcount + 1; + ERROR_FLAG = 1; + end + #3; + end + endtask + + initial begin + //$dumpfile("test_macc.vcd"); + //$dumpvars(0, testbench); + + #2; + clk = 1'b0; + ce = 1'b0; + a = 0; + b = 0; + + rst = 1'b1; + repeat (10) begin + #10; + clk = 1'b1; + #10; + clk = 1'b0; + #10; + clk = 1'b1; + #10; + clk = 1'b0; + end + rst = 1'b0; + + repeat (10000) begin + clkcycle; + ce = 1; //$urandom & $urandom; + //rst = $urandom & $urandom & $urandom & $urandom & $urandom & $urandom; + a = $urandom & ~(1 << (SIZEIN-1)); + b = $urandom & ~(1 << (SIZEIN-1)); + end + + if (errcount == 0) begin + $display("All tests passed."); + $finish; + end else begin + $display("Caught %1d errors.", errcount); + $stop; + end + end + + macc2 ref ( + .clk(clk), + .ce(ce), + .rst(rst), + .a(a), + .b(b), + .accum_out(REF_accum_out), + .overflow(REF_overflow) + ); + + macc2_uut uut ( + .clk(clk), + .ce(ce), + .rst(rst), + .a(a), + .b(b), + .accum_out(accum_out), + .overflow(overflow) + ); +endmodule diff --git a/tests/arch/xilinx/mul.ys b/tests/arch/xilinx/mul.ys new file mode 100644 index 000000000..490846ff1 --- /dev/null +++ b/tests/arch/xilinx/mul.ys @@ -0,0 +1,21 @@ +read_verilog ../common/mul.v +hierarchy -top top +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:DSP48E1 +select -assert-none t:DSP48E1 %% t:* %D + +design -reset + +read_verilog ../common/mul.v +hierarchy -top top +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:DSP48A1 +select -assert-none t:DSP48A1 %% t:* %D diff --git a/tests/arch/xilinx/mul_unsigned.v b/tests/arch/xilinx/mul_unsigned.v new file mode 100644 index 000000000..e3713a642 --- /dev/null +++ b/tests/arch/xilinx/mul_unsigned.v @@ -0,0 +1,30 @@ +/* +Example from: https://www.xilinx.com/support/documentation/sw_manuals/xilinx2019_1/ug901-vivado-synthesis.pdf [p. 89]. +*/ + +// Unsigned 16x24-bit Multiplier +// 1 latency stage on operands +// 3 latency stage after the multiplication +// File: multipliers2.v +// +module mul_unsigned (clk, A, B, RES); +parameter WIDTHA = /*16*/ 6; +parameter WIDTHB = /*24*/ 9; +input clk; +input [WIDTHA-1:0] A; +input [WIDTHB-1:0] B; +output [WIDTHA+WIDTHB-1:0] RES; +reg [WIDTHA-1:0] rA; +reg [WIDTHB-1:0] rB; +reg [WIDTHA+WIDTHB-1:0] M [3:0]; +integer i; +always @(posedge clk) + begin + rA <= A; + rB <= B; + M[0] <= rA * rB; + for (i = 0; i < 3; i = i+1) + M[i+1] <= M[i]; + end +assign RES = M[3]; +endmodule diff --git a/tests/arch/xilinx/mul_unsigned.ys b/tests/arch/xilinx/mul_unsigned.ys new file mode 100644 index 000000000..980263cbd --- /dev/null +++ b/tests/arch/xilinx/mul_unsigned.ys @@ -0,0 +1,25 @@ +read_verilog mul_unsigned.v +hierarchy -top mul_unsigned +proc + +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mul_unsigned # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:DSP48E1 +select -assert-count 30 t:FDRE +select -assert-none t:DSP48E1 t:FDRE t:BUFG %% t:* %D + +design -reset + +read_verilog mul_unsigned.v +hierarchy -top mul_unsigned +proc + +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mul_unsigned # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:DSP48A1 +select -assert-count 30 t:FDRE +select -assert-none t:DSP48A1 t:FDRE t:BUFG %% t:* %D diff --git a/tests/arch/xilinx/mux.ys b/tests/arch/xilinx/mux.ys new file mode 100644 index 000000000..99817738d --- /dev/null +++ b/tests/arch/xilinx/mux.ys @@ -0,0 +1,47 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux2 # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT3 + +select -assert-none t:LUT3 %% t:* %D + + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux4 # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT6 + +select -assert-none t:LUT6 %% t:* %D + + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux8 # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT3 +select -assert-count 2 t:LUT6 + +select -assert-none t:LUT3 t:LUT6 %% t:* %D + + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux16 # Constrain all select calls below inside the top module +select -assert-min 5 t:LUT6 +select -assert-max 7 t:LUT6 +select -assert-max 2 t:MUXF7 + +select -assert-none t:LUT6 t:MUXF7 %% t:* %D diff --git a/tests/arch/xilinx/pmgen_xilinx_srl.ys b/tests/arch/xilinx/pmgen_xilinx_srl.ys new file mode 100644 index 000000000..ea2f20487 --- /dev/null +++ b/tests/arch/xilinx/pmgen_xilinx_srl.ys @@ -0,0 +1,57 @@ +read_verilog -icells <<EOT +module \$__XILINX_SHREG_ (input C, input D, input [31:0] L, input E, output Q, output SO); + parameter DEPTH = 1; + parameter [DEPTH-1:0] INIT = 0; + parameter CLKPOL = 1; + parameter ENPOL = 2; + + wire pos_clk = C == CLKPOL; + reg pos_en; + always @(E) + if (ENPOL == 2) pos_en = 1'b1; + else pos_en = (E == ENPOL[0]); + + reg [DEPTH-1:0] r; + always @(posedge pos_clk) + if (pos_en) + r <= {r[DEPTH-2:0], D}; + + assign Q = r[L]; + assign SO = r[DEPTH-1]; +endmodule +EOT +read_verilog +/xilinx/cells_sim.v +proc +design -save model + +test_pmgen -generate xilinx_srl.fixed +hierarchy -top pmtest_xilinx_srl_pm_fixed +flatten; opt_clean + +design -save gold +xilinx_srl -fixed +techmap -autoproc -map %model +design -stash gate + +design -copy-from gold -as gold pmtest_xilinx_srl_pm_fixed +design -copy-from gate -as gate pmtest_xilinx_srl_pm_fixed +dff2dffe -unmap # sat does not support flops-with-enable yet +miter -equiv -flatten -make_assert gold gate miter +sat -set-init-zero -seq 5 -verify -prove-asserts miter + +design -load model + +test_pmgen -generate xilinx_srl.variable +hierarchy -top pmtest_xilinx_srl_pm_variable +flatten; opt_clean + +design -save gold +xilinx_srl -variable +techmap -autoproc -map %model +design -stash gate + +design -copy-from gold -as gold pmtest_xilinx_srl_pm_variable +design -copy-from gate -as gate pmtest_xilinx_srl_pm_variable +dff2dffe -unmap # sat does not support flops-with-enable yet +miter -equiv -flatten -make_assert gold gate miter +sat -set-init-zero -seq 5 -verify -prove-asserts miter diff --git a/tests/arch/xilinx/run-test.sh b/tests/arch/xilinx/run-test.sh new file mode 100755 index 000000000..bf19b887d --- /dev/null +++ b/tests/arch/xilinx/run-test.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +set -e +{ +echo "all::" +for x in *.ys; do + echo "all:: run-$x" + echo "run-$x:" + echo " @echo 'Running $x..'" + echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" +done +for s in *.sh; do + if [ "$s" != "run-test.sh" ]; then + echo "all:: run-$s" + echo "run-$s:" + echo " @echo 'Running $s..'" + echo " @bash $s" + fi +done +} > run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/arch/xilinx/shifter.ys b/tests/arch/xilinx/shifter.ys new file mode 100644 index 000000000..3652319a0 --- /dev/null +++ b/tests/arch/xilinx/shifter.ys @@ -0,0 +1,11 @@ +read_verilog ../common/shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:BUFG +select -assert-count 8 t:FDRE +select -assert-none t:BUFG t:FDRE %% t:* %D diff --git a/tests/arch/xilinx/tribuf.sh b/tests/arch/xilinx/tribuf.sh new file mode 100644 index 000000000..636aed12a --- /dev/null +++ b/tests/arch/xilinx/tribuf.sh @@ -0,0 +1,5 @@ +! ../../../yosys ../common/tribuf.v -qp "synth_xilinx" +../../../yosys ../common/tribuf.v -qp "synth_xilinx -iopad; \ +select -assert-count 2 t:IBUF; \ +select -assert-count 1 t:INV; \ +select -assert-count 1 t:OBUFT" diff --git a/tests/arch/xilinx/tribuf.ys b/tests/arch/xilinx/tribuf.ys new file mode 100644 index 000000000..eaccab126 --- /dev/null +++ b/tests/arch/xilinx/tribuf.ys @@ -0,0 +1,13 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd tristate # Constrain all select calls below inside the top module +select -assert-count 2 t:IBUF +select -assert-count 1 t:INV +select -assert-count 1 t:OBUFT +select -assert-none t:IBUF t:INV t:OBUFT %% t:* %D diff --git a/tests/arch/xilinx/xilinx_dffopt.ys b/tests/arch/xilinx/xilinx_dffopt.ys new file mode 100644 index 000000000..dc036acfd --- /dev/null +++ b/tests/arch/xilinx/xilinx_dffopt.ys @@ -0,0 +1,216 @@ +read_verilog << EOT + +// FDRE, mergeable CE and R. + +module t0 (...); +input wire clk; +input wire [7:0] i; +output wire [7:0] o; + +wire [7:0] tmp ; + +LUT2 #(.INIT(4'h6)) lut0 (.I0(i[0]), .I1(i[1]), .O(tmp[0])); +LUT2 #(.INIT(4'h6)) lut1 (.I0(i[1]), .I1(i[2]), .O(tmp[1])); +LUT2 #(.INIT(4'h6)) lut2 (.I0(i[3]), .I1(i[4]), .O(tmp[2])); + +FDRE ff (.D(tmp[0]), .CE(tmp[1]), .R(tmp[2]), .Q(o[0])); + +endmodule + +EOT + +design -save t0 + +equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt +design -load postopt +clean + +select -assert-count 1 t:FDRE +select -assert-count 1 t:LUT6 +select -assert-count 3 t:LUT2 +select -assert-none t:FDRE t:LUT6 t:LUT2 %% t:* %D + +design -load t0 + +equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt -lut4 +design -load postopt +clean + +select -assert-count 1 t:FDRE +select -assert-count 1 t:LUT4 +select -assert-count 3 t:LUT2 +select -assert-none t:FDRE t:LUT4 t:LUT2 %% t:* %D + +design -reset + + +read_verilog << EOT + +// FDSE, mergeable CE and S, inversions. + +module t0 (...); +input wire clk; +input wire [7:0] i; +output wire [7:0] o; + +wire [7:0] tmp ; + +LUT2 #(.INIT(4'h6)) lut0 (.I0(i[0]), .I1(i[1]), .O(tmp[0])); +LUT2 #(.INIT(4'h6)) lut1 (.I0(i[1]), .I1(i[2]), .O(tmp[1])); +LUT2 #(.INIT(4'h6)) lut2 (.I0(i[3]), .I1(i[4]), .O(tmp[2])); + +FDSE #(.IS_D_INVERTED(1'b1), .IS_S_INVERTED(1'b1)) ff (.D(tmp[0]), .CE(tmp[1]), .S(tmp[2]), .Q(o[0])); + +endmodule + +EOT + +design -save t0 + +equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt +design -load postopt +clean + +select -assert-count 1 t:FDSE +select -assert-count 1 t:LUT6 +select -assert-count 3 t:LUT2 +select -assert-none t:FDSE t:LUT6 t:LUT2 %% t:* %D + +design -load t0 + +equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt -lut4 +design -load postopt +clean + +select -assert-count 1 t:FDSE +select -assert-count 1 t:LUT4 +select -assert-count 3 t:LUT2 +select -assert-none t:FDSE t:LUT4 t:LUT2 %% t:* %D + +design -reset + + +read_verilog << EOT + +// FDCE, mergeable CE. + +module t0 (...); +input wire clk; +input wire [7:0] i; +output wire [7:0] o; + +wire [7:0] tmp ; + +LUT2 #(.INIT(4'h6)) lut0 (.I0(i[0]), .I1(i[1]), .O(tmp[0])); +LUT2 #(.INIT(4'h6)) lut1 (.I0(i[1]), .I1(i[2]), .O(tmp[1])); +LUT2 #(.INIT(4'h6)) lut2 (.I0(i[3]), .I1(i[4]), .O(tmp[2])); + +FDCE ff (.D(tmp[0]), .CE(tmp[1]), .CLR(tmp[2]), .Q(o[0])); + +endmodule + +EOT + +design -save t0 + +equiv_opt -async2sync -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt +design -load postopt +clean + +select -assert-count 1 t:FDCE +select -assert-count 1 t:LUT4 +select -assert-count 3 t:LUT2 +select -assert-none t:FDCE t:LUT4 t:LUT2 %% t:* %D + +design -reset + + +read_verilog << EOT + +// FDSE, mergeable CE and S, but CE only not worth it. + +module t0 (...); +input wire clk; +input wire [7:0] i; +output wire [7:0] o; + +wire [7:0] tmp ; + +LUT2 #(.INIT(4'h6)) lut0 (.I0(i[0]), .I1(i[1]), .O(tmp[0])); +LUT2 #(.INIT(4'h6)) lut1 (.I0(i[1]), .I1(i[2]), .O(tmp[1])); + +FDSE ff (.D(tmp[0]), .CE(i[7]), .S(tmp[1]), .Q(o[0])); + +endmodule + +EOT + +design -save t0 + +equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt +design -load postopt +clean + +select -assert-count 1 t:FDSE +select -assert-count 1 t:LUT5 +select -assert-count 2 t:LUT2 +select -assert-none t:FDSE t:LUT5 t:LUT2 %% t:* %D + +design -load t0 + +equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt -lut4 +design -load postopt +clean + +select -assert-count 1 t:FDSE +select -assert-count 2 t:LUT2 +select -assert-none t:FDSE t:LUT2 %% t:* %D + +design -reset + + +read_verilog << EOT + +// FDRSE, mergeable CE, S, R. + +module t0 (...); +input wire clk; +input wire [7:0] i; +output wire [7:0] o; + +wire [7:0] tmp ; + +LUT2 #(.INIT(4'h6)) lut0 (.I0(i[0]), .I1(i[1]), .O(tmp[0])); +LUT2 #(.INIT(4'h6)) lut1 (.I0(i[1]), .I1(i[2]), .O(tmp[1])); +LUT2 #(.INIT(4'h8)) lut2 (.I0(i[2]), .I1(i[0]), .O(tmp[2])); +LUT2 #(.INIT(4'h6)) lut3 (.I0(i[3]), .I1(i[4]), .O(tmp[3])); + +FDRSE ff (.D(tmp[0]), .CE(tmp[1]), .S(tmp[2]), .R(tmp[3]), .Q(o[0])); + +endmodule + +EOT + +design -save t0 + +equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt +design -load postopt +clean + +select -assert-count 1 t:FDRSE +select -assert-count 1 t:LUT6 +select -assert-count 4 t:LUT2 +select -assert-none t:FDRSE t:LUT6 t:LUT2 %% t:* %D + +design -load t0 + +equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt -lut4 +design -load postopt +clean + +select -assert-count 1 t:FDRSE +select -assert-count 1 t:LUT4 +select -assert-count 4 t:LUT2 +select -assert-none t:FDRSE t:LUT4 t:LUT2 %% t:* %D + +design -reset diff --git a/tests/arch/xilinx/xilinx_dffopt_blacklist.txt b/tests/arch/xilinx/xilinx_dffopt_blacklist.txt new file mode 100644 index 000000000..6a31a0cd3 --- /dev/null +++ b/tests/arch/xilinx/xilinx_dffopt_blacklist.txt @@ -0,0 +1,13 @@ +lut0 +lut1 +lut2 +lut3 +ff +ff.D +ff.R +ff.S +ff.CE +ff.d +ff.r +ff.s +ff.ce diff --git a/tests/arch/xilinx/xilinx_dsp.ys b/tests/arch/xilinx/xilinx_dsp.ys new file mode 100644 index 000000000..3b9f52930 --- /dev/null +++ b/tests/arch/xilinx/xilinx_dsp.ys @@ -0,0 +1,11 @@ +read_verilog <<EOT +module top(input [24:0] a, input [17:0] b, output [42:0] o1, o2, o5); +DSP48E1 m1 (.A(a), .B(16'd1234), .P(o1)); +assign o2 = a * 16'd0; +wire [42:0] o3, o4; +DSP48E1 m2 (.A(a), .B(b), .P(o3)); +assign o4 = a * b; +DSP48E1 m3 (.A(a), .B(b), .P(o5)); +endmodule +EOT +xilinx_dsp diff --git a/tests/arch/xilinx/xilinx_srl.v b/tests/arch/xilinx/xilinx_srl.v new file mode 100644 index 000000000..bc2a15ab2 --- /dev/null +++ b/tests/arch/xilinx/xilinx_srl.v @@ -0,0 +1,40 @@ +module xilinx_srl_static_test(input i, clk, output [1:0] q); +reg head = 1'b0; +reg [3:0] shift1 = 4'b0000; +reg [3:0] shift2 = 4'b0000; + +always @(posedge clk) begin + head <= i; + shift1 <= {shift1[2:0], head}; + shift2 <= {shift2[2:0], head}; +end + +assign q = {shift2[3], shift1[3]}; +endmodule + +module xilinx_srl_variable_test(input i, clk, input [1:0] l1, l2, output [1:0] q); +reg head = 1'b0; +reg [3:0] shift1 = 4'b0000; +reg [3:0] shift2 = 4'b0000; + +always @(posedge clk) begin + head <= i; + shift1 <= {shift1[2:0], head}; + shift2 <= {shift2[2:0], head}; +end + +assign q = {shift2[l2], shift1[l1]}; +endmodule + +module $__XILINX_SHREG_(input C, D, E, input [1:0] L, output Q); +parameter CLKPOL = 1; +parameter ENPOL = 1; +parameter DEPTH = 1; +parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}}; +reg [DEPTH-1:0] r = INIT; +wire clk = C ^ CLKPOL; +always @(posedge C) + if (E) + r <= { r[DEPTH-2:0], D }; +assign Q = r[L]; +endmodule diff --git a/tests/arch/xilinx/xilinx_srl.ys b/tests/arch/xilinx/xilinx_srl.ys new file mode 100644 index 000000000..b8df0e55a --- /dev/null +++ b/tests/arch/xilinx/xilinx_srl.ys @@ -0,0 +1,67 @@ +read_verilog xilinx_srl.v +design -save read + +design -copy-to model $__XILINX_SHREG_ +hierarchy -top xilinx_srl_static_test +prep +design -save gold + +techmap +xilinx_srl -fixed +opt + +# stat +# show -width +select -assert-count 1 t:$_DFF_P_ +select -assert-count 2 t:$__XILINX_SHREG_ + +design -stash gate + +design -import gold -as gold +design -import gate -as gate +design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_ +prep + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +dump gate +sat -verify -prove-asserts -show-ports -seq 5 miter + +#design -load gold +#stat + +#design -load gate +#stat + +########## + +design -load read +design -copy-to model $__XILINX_SHREG_ +hierarchy -top xilinx_srl_variable_test +prep +design -save gold + +xilinx_srl -variable +opt + +#stat +# show -width +# write_verilog -noexpr -norename +select -assert-count 1 t:$dff +select -assert-count 1 t:$dff r:WIDTH=1 %i +select -assert-count 2 t:$__XILINX_SHREG_ + +design -stash gate + +design -import gold -as gold +design -import gate -as gate +design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_ +prep + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports -seq 5 miter + +# design -load gold +# stat + +# design -load gate +# stat |