diff options
| author | Eddie Hung <eddie@fpgeh.com> | 2020-02-01 02:14:19 -0800 |
|---|---|---|
| committer | Eddie Hung <eddie@fpgeh.com> | 2020-02-01 02:14:19 -0800 |
| commit | 136842b1ef18b850b518705ff3e6df3958f28e0c (patch) | |
| tree | abcdddaf53bafd5e34e9aa278ffbe3d001b60cc4 /tests | |
| parent | 705e520a527864dc32f1934bb4b2b94d75f8f0ec (diff) | |
| parent | a1c840ca5d6e8b580e21ae48550570aa9665741a (diff) | |
| download | yosys-136842b1ef18b850b518705ff3e6df3958f28e0c.tar.gz yosys-136842b1ef18b850b518705ff3e6df3958f28e0c.tar.bz2 yosys-136842b1ef18b850b518705ff3e6df3958f28e0c.zip | |
Merge branch 'master' into eddie/submod_po
Diffstat (limited to 'tests')
83 files changed, 2399 insertions, 175 deletions
diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh index deaf48a3d..8e932b091 100755 --- a/tests/aiger/run-test.sh +++ b/tests/aiger/run-test.sh @@ -33,7 +33,7 @@ design -import gold -as gold design -import gate -as gate miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -show-ports -seq 16 miter -" +" -l ${aag}.log done for aig in *.aig; do @@ -50,5 +50,5 @@ design -import gold -as gold design -import gate -as gate miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -show-ports -seq 16 miter -" +" -l ${aig}.log done diff --git a/tests/aiger/symbols.aag b/tests/aiger/symbols.aag new file mode 100644 index 000000000..93f8989f2 --- /dev/null +++ b/tests/aiger/symbols.aag @@ -0,0 +1,9 @@ +aag 2 1 1 1 0 +2 +4 2 1 +4 +i0 d +l0 q +o0 q +c +Generated by Yosys 0.9+932 (git sha1 baba33fb, clang 9.0.0-2 -fPIC -Os) diff --git a/tests/aiger/symbols.aig b/tests/aiger/symbols.aig new file mode 100644 index 000000000..a7922ab46 --- /dev/null +++ b/tests/aiger/symbols.aig @@ -0,0 +1,8 @@ +aig 2 1 1 1 0 +2 1 +4 +i0 d +l0 q +o0 q +c +Generated by Yosys 0.9+932 (git sha1 baba33fb, clang 9.0.0-2 -fPIC -Os) diff --git a/tests/arch/anlogic/counter.ys b/tests/arch/anlogic/counter.ys index d363ec24e..a6eab248c 100644 --- a/tests/arch/anlogic/counter.ys +++ b/tests/arch/anlogic/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +equiv_opt -assert -multiclock -map +/anlogic/cells_sim.v synth_anlogic # 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 diff --git a/tests/arch/anlogic/memory.ys b/tests/arch/anlogic/lutram.ys index 87b93c2fe..9ebb75443 100644 --- a/tests/arch/anlogic/memory.ys +++ b/tests/arch/anlogic/lutram.ys @@ -1,5 +1,5 @@ -read_verilog ../common/memory.v -hierarchy -top top +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r proc memory -nomap equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic @@ -11,7 +11,7 @@ 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 top +cd lutram_1w1r select -assert-count 8 t:AL_MAP_LUT2 select -assert-count 8 t:AL_MAP_LUT4 diff --git a/tests/arch/common/blockram.v b/tests/arch/common/blockram.v new file mode 100644 index 000000000..dbc6ca65c --- /dev/null +++ b/tests/arch/common/blockram.v @@ -0,0 +1,45 @@ +`default_nettype none +module sync_ram_sp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10) + (input wire write_enable, clk, + input wire [DATA_WIDTH-1:0] data_in, + input wire [ADDRESS_WIDTH-1:0] address_in, + output wire [DATA_WIDTH-1:0] data_out); + + localparam WORD = (DATA_WIDTH-1); + localparam DEPTH = (2**ADDRESS_WIDTH-1); + + reg [WORD:0] data_out_r; + reg [WORD:0] memory [0:DEPTH]; + + always @(posedge clk) begin + if (write_enable) + memory[address_in] <= data_in; + data_out_r <= memory[address_in]; + end + + assign data_out = data_out_r; +endmodule // sync_ram_sp + + +`default_nettype none +module sync_ram_sdp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10) + (input wire clk, write_enable, + input wire [DATA_WIDTH-1:0] data_in, + input wire [ADDRESS_WIDTH-1:0] address_in_r, address_in_w, + output wire [DATA_WIDTH-1:0] data_out); + + localparam WORD = (DATA_WIDTH-1); + localparam DEPTH = (2**ADDRESS_WIDTH-1); + + reg [WORD:0] data_out_r; + reg [WORD:0] memory [0:DEPTH]; + + always @(posedge clk) begin + if (write_enable) + memory[address_in_w] <= data_in; + data_out_r <= memory[address_in_r]; + end + + assign data_out = data_out_r; +endmodule // sync_ram_sdp + diff --git a/tests/arch/common/lutram.v b/tests/arch/common/lutram.v new file mode 100644 index 000000000..9534b7619 --- /dev/null +++ b/tests/arch/common/lutram.v @@ -0,0 +1,42 @@ +module lutram_1w1r +#(parameter D_WIDTH=8, A_WIDTH=6) +( + input [D_WIDTH-1:0] data_a, + input [A_WIDTH:1] addr_a, + input we_a, clk, + output reg [D_WIDTH-1:0] q_a +); + // Declare the RAM variable + reg [D_WIDTH-1:0] ram[(2**A_WIDTH)-1:0]; + + // Port A + always @ (posedge clk) + begin + if (we_a) + ram[addr_a] <= data_a; + q_a <= ram[addr_a]; + end +endmodule + + +module lutram_1w3r +#(parameter D_WIDTH=8, A_WIDTH=5) +( + input [D_WIDTH-1:0] data_a, data_b, data_c, + input [A_WIDTH:1] addr_a, addr_b, addr_c, + input we_a, clk, + output reg [D_WIDTH-1:0] q_a, q_b, q_c +); + // Declare the RAM variable + reg [D_WIDTH-1:0] ram[(2**A_WIDTH)-1:0]; + + // Port A + always @ (posedge clk) + begin + if (we_a) + ram[addr_a] <= data_a; + q_a <= ram[addr_a]; + q_b <= ram[addr_b]; + q_c <= ram[addr_c]; + end +endmodule diff --git a/tests/arch/common/memory.v b/tests/arch/common/memory.v deleted file mode 100644 index cb7753f7b..000000000 --- a/tests/arch/common/memory.v +++ /dev/null @@ -1,21 +0,0 @@ -module top -( - input [7:0] data_a, - input [6:1] addr_a, - input we_a, clk, - output reg [7:0] q_a -); - // Declare the RAM variable - reg [7:0] ram[63:0]; - - // Port A - always @ (posedge clk) - begin - if (we_a) - begin - ram[addr_a] <= data_a; - q_a <= data_a; - end - q_a <= ram[addr_a]; - end -endmodule diff --git a/tests/arch/common/memory_attributes/attributes_test.v b/tests/arch/common/memory_attributes/attributes_test.v new file mode 100644 index 000000000..275800dd0 --- /dev/null +++ b/tests/arch/common/memory_attributes/attributes_test.v @@ -0,0 +1,88 @@ +`default_nettype none +module block_ram #(parameter DATA_WIDTH=4, ADDRESS_WIDTH=10) + (input wire write_enable, clk, + input wire [DATA_WIDTH-1:0] data_in, + input wire [ADDRESS_WIDTH-1:0] address_in, + output wire [DATA_WIDTH-1:0] data_out); + + localparam WORD = (DATA_WIDTH-1); + localparam DEPTH = (2**ADDRESS_WIDTH-1); + + reg [WORD:0] data_out_r; + reg [WORD:0] memory [0:DEPTH]; + + always @(posedge clk) begin + if (write_enable) + memory[address_in] <= data_in; + data_out_r <= memory[address_in]; + end + + assign data_out = data_out_r; +endmodule // block_ram + +`default_nettype none +module distributed_ram #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=4) + (input wire write_enable, clk, + input wire [DATA_WIDTH-1:0] data_in, + input wire [ADDRESS_WIDTH-1:0] address_in, + output wire [DATA_WIDTH-1:0] data_out); + + localparam WORD = (DATA_WIDTH-1); + localparam DEPTH = (2**ADDRESS_WIDTH-1); + + reg [WORD:0] data_out_r; + reg [WORD:0] memory [0:DEPTH]; + + always @(posedge clk) begin + if (write_enable) + memory[address_in] <= data_in; + data_out_r <= memory[address_in]; + end + + assign data_out = data_out_r; +endmodule // distributed_ram + +`default_nettype none +module distributed_ram_manual #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=4) + (input wire write_enable, clk, + input wire [DATA_WIDTH-1:0] data_in, + input wire [ADDRESS_WIDTH-1:0] address_in, + output wire [DATA_WIDTH-1:0] data_out); + + localparam WORD = (DATA_WIDTH-1); + localparam DEPTH = (2**ADDRESS_WIDTH-1); + + reg [WORD:0] data_out_r; + (* ram_style = "block" *) reg [WORD:0] memory [0:DEPTH]; + + always @(posedge clk) begin + if (write_enable) + memory[address_in] <= data_in; + data_out_r <= memory[address_in]; + end + + assign data_out = data_out_r; +endmodule // distributed_ram + +`default_nettype none +module distributed_ram_manual_syn #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=4) + (input wire write_enable, clk, + input wire [DATA_WIDTH-1:0] data_in, + input wire [ADDRESS_WIDTH-1:0] address_in, + output wire [DATA_WIDTH-1:0] data_out); + + localparam WORD = (DATA_WIDTH-1); + localparam DEPTH = (2**ADDRESS_WIDTH-1); + + reg [WORD:0] data_out_r; + (* synthesis, ram_block *) reg [WORD:0] memory [0:DEPTH]; + + always @(posedge clk) begin + if (write_enable) + memory[address_in] <= data_in; + data_out_r <= memory[address_in]; + end + + assign data_out = data_out_r; +endmodule // distributed_ram + diff --git a/tests/arch/ecp5/bug1459.ys b/tests/arch/ecp5/bug1459.ys new file mode 100644 index 000000000..1142ae0b5 --- /dev/null +++ b/tests/arch/ecp5/bug1459.ys @@ -0,0 +1,25 @@ +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, + output reg [63:0] read1_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]; + end +endmodule +EOT + +synth_ecp5 -abc9 diff --git a/tests/arch/ecp5/bug1598.ys b/tests/arch/ecp5/bug1598.ys new file mode 100644 index 000000000..1d1682fcd --- /dev/null +++ b/tests/arch/ecp5/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 +/ecp5/cells_sim.v synth_ecp5 -abc9 diff --git a/tests/arch/ecp5/bug1630.il.gz b/tests/arch/ecp5/bug1630.il.gz Binary files differnew file mode 100644 index 000000000..37bcf2be2 --- /dev/null +++ b/tests/arch/ecp5/bug1630.il.gz diff --git a/tests/arch/ecp5/bug1630.ys b/tests/arch/ecp5/bug1630.ys new file mode 100644 index 000000000..b419fb9bb --- /dev/null +++ b/tests/arch/ecp5/bug1630.ys @@ -0,0 +1,2 @@ +read_ilang bug1630.il.gz +abc9 -lut +/ecp5/abc9_5g.lut diff --git a/tests/arch/ecp5/counter.ys b/tests/arch/ecp5/counter.ys index f9f60fbff..e46001ffe 100644 --- a/tests/arch/ecp5/counter.ys +++ b/tests/arch/ecp5/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check +equiv_opt -assert -multiclock -map +/ecp5/cells_sim.v synth_ecp5 # 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 4 t:CCU2C diff --git a/tests/arch/ecp5/memory.ys b/tests/arch/ecp5/lutram.ys index c82b7b405..e1ae7abd5 100644 --- a/tests/arch/ecp5/memory.ys +++ b/tests/arch/ecp5/lutram.ys @@ -1,5 +1,5 @@ -read_verilog ../common/memory.v -hierarchy -top top +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r proc memory -nomap equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5 @@ -10,7 +10,7 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter design -load postopt -cd top +cd lutram_1w1r select -assert-count 24 t:L6MUX21 select -assert-count 71 t:LUT4 select -assert-count 32 t:PFUMX diff --git a/tests/arch/ecp5/macc.ys b/tests/arch/ecp5/macc.ys index 1863ea4d2..8da8d2f8e 100644 --- a/tests/arch/ecp5/macc.ys +++ b/tests/arch/ecp5/macc.ys @@ -3,8 +3,8 @@ hierarchy -top top proc # Blocked by issue #1358 (Missing ECP5 simulation models) #equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check -equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +synth_ecp5 +#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:MULT18X18D select -assert-count 4 t:CCU2C diff --git a/tests/arch/ecp5/mul.ys b/tests/arch/ecp5/mul.ys index 2105be52c..f887e9585 100644 --- a/tests/arch/ecp5/mul.ys +++ b/tests/arch/ecp5/mul.ys @@ -3,9 +3,9 @@ hierarchy -top top proc # Blocked by issue #1358 (Missing ECP5 simulation models) #equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check -equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check +synth_ecp5 -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +#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:MULT18X18D select -assert-none t:MULT18X18D %% t:* %D diff --git a/tests/arch/ecp5/mux.ys b/tests/arch/ecp5/mux.ys index 92463aa32..22866832d 100644 --- a/tests/arch/ecp5/mux.ys +++ b/tests/arch/ecp5/mux.ys @@ -39,8 +39,8 @@ proc equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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-count 8 t:L6MUX21 -select -assert-count 26 t:LUT4 -select -assert-count 12 t:PFUMX +select -assert-count 12 t:L6MUX21 +select -assert-count 34 t:LUT4 +select -assert-count 17 t:PFUMX select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D diff --git a/tests/arch/efinix/counter.ys b/tests/arch/efinix/counter.ys index d20b8ae27..f8fb29a87 100644 --- a/tests/arch/efinix/counter.ys +++ b/tests/arch/efinix/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -map +/efinix/cells_sim.v synth_efinix # equivalency check +equiv_opt -assert -multiclock -map +/efinix/cells_sim.v synth_efinix # 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 diff --git a/tests/arch/efinix/memory.ys b/tests/arch/efinix/lutram.ys index 6f6acdcde..dcf647ce0 100644 --- a/tests/arch/efinix/memory.ys +++ b/tests/arch/efinix/lutram.ys @@ -1,5 +1,5 @@ -read_verilog ../common/memory.v -hierarchy -top top +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r proc memory -nomap equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix @@ -12,7 +12,7 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter design -load postopt -cd top +cd lutram_1w1r select -assert-count 1 t:EFX_GBUFCE select -assert-count 1 t:EFX_RAM_5K select -assert-none t:EFX_GBUFCE t:EFX_RAM_5K %% t:* %D diff --git a/tests/arch/efinix/mux.ys b/tests/arch/efinix/mux.ys index b46f641e1..a5ab80d8b 100644 --- a/tests/arch/efinix/mux.ys +++ b/tests/arch/efinix/mux.ys @@ -36,6 +36,6 @@ proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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-count 12 t:EFX_LUT4 +select -assert-max 12 t:EFX_LUT4 select -assert-none t:EFX_LUT4 %% t:* %D diff --git a/tests/arch/gowin/adffs.ys b/tests/arch/gowin/adffs.ys index fc7ee01f2..87fba83a6 100644 --- a/tests/arch/gowin/adffs.ys +++ b/tests/arch/gowin/adffs.ys @@ -34,11 +34,12 @@ proc equiv_opt -async2sync -assert -map +/gowin/cells_sim.v synth_gowin # 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:DFFS +select -assert-count 1 t:DFF +select -assert-count 1 t:LUT2 select -assert-count 4 t:IBUF select -assert-count 1 t:OBUF -select -assert-none t:DFFS t:IBUF t:OBUF %% t:* %D +select -assert-none t:DFF t:LUT2 t:IBUF t:OBUF %% t:* %D design -load read diff --git a/tests/arch/gowin/counter.ys b/tests/arch/gowin/counter.ys index 920479d44..bdbc7ee24 100644 --- a/tests/arch/gowin/counter.ys +++ b/tests/arch/gowin/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -map +/gowin/cells_sim.v synth_gowin # equivalency check +equiv_opt -assert -multiclock -map +/gowin/cells_sim.v synth_gowin # 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 diff --git a/tests/arch/gowin/init.v b/tests/arch/gowin/init.v new file mode 100644 index 000000000..3c30f602d --- /dev/null +++ b/tests/arch/gowin/init.v @@ -0,0 +1,224 @@ +module myDFF (output reg Q, input CLK, D); + parameter [0:0] INIT = 1'b0; + initial Q = INIT; + always @(posedge CLK) + Q <= D; +endmodule + +module myDFFE (output reg Q, input D, CLK, CE); + parameter [0:0] INIT = 1'b0; + initial Q = INIT; + always @(posedge CLK) begin + if (CE) + Q <= D; + end +endmodule // DFFE (positive clock edge; clock enable) + + +module myDFFS (output reg Q, input D, CLK, SET); + parameter [0:0] INIT = 1'b1; + initial Q = INIT; + always @(posedge CLK) begin + if (SET) + Q <= 1'b1; + else + Q <= D; + end +endmodule // DFFS (positive clock edge; synchronous set) + + +module myDFFSE (output reg Q, input D, CLK, CE, SET); + parameter [0:0] INIT = 1'b1; + initial Q = INIT; + always @(posedge CLK) begin + if (SET) + Q <= 1'b1; + else if (CE) + Q <= D; +end +endmodule // DFFSE (positive clock edge; synchronous set takes precedence over clock enable) + + +module myDFFR (output reg Q, input D, CLK, RESET); + parameter [0:0] INIT = 1'b0; + initial Q = INIT; + always @(posedge CLK) begin + if (RESET) + Q <= 1'b0; + else + Q <= D; + end +endmodule // DFFR (positive clock edge; synchronous reset) + + +module myDFFRE (output reg Q, input D, CLK, CE, RESET); + parameter [0:0] INIT = 1'b0; + initial Q = INIT; + always @(posedge CLK) begin + if (RESET) + Q <= 1'b0; + else if (CE) + Q <= D; + end +endmodule // DFFRE (positive clock edge; synchronous reset takes precedence over clock enable) + + +module myDFFP (output reg Q, input D, CLK, PRESET); + parameter [0:0] INIT = 1'b1; + initial Q = INIT; + always @(posedge CLK or posedge PRESET) begin + if(PRESET) + Q <= 1'b1; + else + Q <= D; + end +endmodule // DFFP (positive clock edge; asynchronous preset) + + +module myDFFPE (output reg Q, input D, CLK, CE, PRESET); + parameter [0:0] INIT = 1'b1; + initial Q = INIT; + always @(posedge CLK or posedge PRESET) begin + if(PRESET) + Q <= 1'b1; + else if (CE) + Q <= D; + end +endmodule // DFFPE (positive clock edge; asynchronous preset; clock enable) + + +module myDFFC (output reg Q, input D, CLK, CLEAR); + parameter [0:0] INIT = 1'b0; + initial Q = INIT; + always @(posedge CLK or posedge CLEAR) begin + if(CLEAR) + Q <= 1'b0; + else + Q <= D; + end +endmodule // DFFC (positive clock edge; asynchronous clear) + + +module myDFFCE (output reg Q, input D, CLK, CE, CLEAR); + parameter [0:0] INIT = 1'b0; + initial Q = INIT; + always @(posedge CLK or posedge CLEAR) begin + if(CLEAR) + Q <= 1'b0; + else if (CE) + Q <= D; + end +endmodule // DFFCE (positive clock edge; asynchronous clear; clock enable) + + +module myDFFN (output reg Q, input CLK, D); + parameter [0:0] INIT = 1'b0; + initial Q = INIT; + always @(negedge CLK) + Q <= D; +endmodule + +module myDFFNE (output reg Q, input D, CLK, CE); + parameter [0:0] INIT = 1'b0; + initial Q = INIT; + always @(negedge CLK) begin + if (CE) + Q <= D; + end +endmodule // DFFNE (negative clock edge; clock enable) + + +module myDFFNS (output reg Q, input D, CLK, SET); + parameter [0:0] INIT = 1'b1; + initial Q = INIT; + always @(negedge CLK) begin + if (SET) + Q <= 1'b1; + else + Q <= D; + end +endmodule // DFFNS (negative clock edge; synchronous set) + + +module myDFFNSE (output reg Q, input D, CLK, CE, SET); + parameter [0:0] INIT = 1'b1; + initial Q = INIT; + always @(negedge CLK) begin + if (SET) + Q <= 1'b1; + else if (CE) + Q <= D; +end +endmodule // DFFNSE (negative clock edge; synchronous set takes precedence over clock enable) + + +module myDFFNR (output reg Q, input D, CLK, RESET); + parameter [0:0] INIT = 1'b0; + initial Q = INIT; + always @(negedge CLK) begin + if (RESET) + Q <= 1'b0; + else + Q <= D; + end +endmodule // DFFNR (negative clock edge; synchronous reset) + + +module myDFFNRE (output reg Q, input D, CLK, CE, RESET); + parameter [0:0] INIT = 1'b0; + initial Q = INIT; + always @(negedge CLK) begin + if (RESET) + Q <= 1'b0; + else if (CE) + Q <= D; + end +endmodule // DFFNRE (negative clock edge; synchronous reset takes precedence over clock enable) + + +module myDFFNP (output reg Q, input D, CLK, PRESET); + parameter [0:0] INIT = 1'b1; + initial Q = INIT; + always @(negedge CLK or posedge PRESET) begin + if(PRESET) + Q <= 1'b1; + else + Q <= D; + end +endmodule // DFFNP (negative clock edge; asynchronous preset) + + +module myDFFNPE (output reg Q, input D, CLK, CE, PRESET); + parameter [0:0] INIT = 1'b1; + initial Q = INIT; + always @(negedge CLK or posedge PRESET) begin + if(PRESET) + Q <= 1'b1; + else if (CE) + Q <= D; + end +endmodule // DFFNPE (negative clock edge; asynchronous preset; clock enable) + + +module myDFFNC (output reg Q, input D, CLK, CLEAR); + parameter [0:0] INIT = 1'b0; + initial Q = INIT; + always @(negedge CLK or posedge CLEAR) begin + if(CLEAR) + Q <= 1'b0; + else + Q <= D; + end +endmodule // DFFNC (negative clock edge; asynchronous clear) + + +module myDFFNCE (output reg Q, input D, CLK, CE, CLEAR); + parameter [0:0] INIT = 1'b0; + initial Q = INIT; + always @(negedge CLK or posedge CLEAR) begin + if(CLEAR) + Q <= 1'b0; + else if (CE) + Q <= D; + end +endmodule // DFFNCE (negative clock edge; asynchronous clear; clock enable) diff --git a/tests/arch/gowin/init.ys b/tests/arch/gowin/init.ys new file mode 100644 index 000000000..ddc0e4757 --- /dev/null +++ b/tests/arch/gowin/init.ys @@ -0,0 +1,74 @@ +read_verilog init.v +read_verilog -lib +/gowin/cells_sim.v +design -save read + +proc +flatten +synth_gowin -run coarse: + +# check if all init values are handled +check -assert -noinit +# check if every flop mapped correctly +select -assert-count 1 t:DFF +select -assert-count 1 t:DFFC +select -assert-count 1 t:DFFCE +select -assert-count 1 t:DFFE +select -assert-count 1 t:DFFN +select -assert-count 1 t:DFFNC +select -assert-count 1 t:DFFNCE +select -assert-count 1 t:DFFNE +select -assert-count 1 t:DFFNP +select -assert-count 1 t:DFFNPE +select -assert-count 1 t:DFFNR +select -assert-count 1 t:DFFNRE +select -assert-count 1 t:DFFNS +select -assert-count 1 t:DFFNSE +select -assert-count 1 t:DFFP +select -assert-count 1 t:DFFPE +select -assert-count 1 t:DFFR +select -assert-count 1 t:DFFRE +select -assert-count 1 t:DFFS +select -assert-count 1 t:DFFSE + +delete +design -load read + +# these should synth to a flop with reset +chparam -set INIT 1 myDFF myDFFN myDFFE myDFFNE + +# async should give a warning +# sync should synth to a mux +chparam -set INIT 0 myDFF*S* myDFF*P* +chparam -set INIT 1 myDFF*R* myDFF*C* + +proc +flatten +synth_gowin -run coarse: + +# check the flops mapped as expected +select -assert-count 1 t:DFF +select -assert-count 1 t:DFFC +select -assert-count 1 t:DFFCE +select -assert-count 1 t:DFFE +select -assert-count 1 t:DFFN +select -assert-count 1 t:DFFNC +select -assert-count 1 t:DFFNCE +select -assert-count 1 t:DFFNE +select -assert-count 1 t:DFFNP +select -assert-count 1 t:DFFNPE +select -assert-count 0 t:DFFNR +select -assert-count 0 t:DFFNRE +select -assert-count 2 t:DFFNS +select -assert-count 2 t:DFFNSE +select -assert-count 1 t:DFFP +select -assert-count 1 t:DFFPE +select -assert-count 0 t:DFFR +select -assert-count 0 t:DFFRE +select -assert-count 2 t:DFFS +select -assert-count 2 t:DFFSE +select -assert-count 12 t:LUT2 + +# check the expected leftover init values +# this would happen if your reset value is not the initial value +# which would be weird +select -assert-count 8 a:init diff --git a/tests/arch/gowin/memory.ys b/tests/arch/gowin/lutram.ys index 8f88cdd7c..56f69e7c5 100644 --- a/tests/arch/gowin/memory.ys +++ b/tests/arch/gowin/lutram.ys @@ -1,5 +1,5 @@ -read_verilog ../common/memory.v -hierarchy -top top +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r proc memory -nomap equiv_opt -run :prove -map +/gowin/cells_sim.v synth_gowin @@ -12,7 +12,7 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter design -load postopt -cd top +cd lutram_1w1r select -assert-count 8 t:RAM16S4 # other logic present that is not simple #select -assert-none t:RAM16S4 %% t:* %D diff --git a/tests/arch/ice40/bug1597.ys b/tests/arch/ice40/bug1597.ys new file mode 100644 index 000000000..b7983cfa4 --- /dev/null +++ b/tests/arch/ice40/bug1597.ys @@ -0,0 +1,72 @@ +read_verilog <<EOT +module top ( + input CLK, PIN_1, PIN_2, PIN_3, PIN_4, PIN_5, + PIN_6, PIN_7, PIN_8, PIN_9, PIN_10, PIN_11, PIN_12, PIN_13, PIN_25, + output USBPU, PIN_14, PIN_15, PIN_16, PIN_17, PIN_18, + PIN_19, PIN_20, PIN_21, PIN_22, PIN_23, PIN_24, +); + assign USBPU = 0; + + wire[5:0] parOut; + wire[5:0] chrg; + + assign PIN_14 = parOut[0]; + assign PIN_15 = parOut[1]; + assign PIN_16 = parOut[2]; + assign PIN_17 = parOut[3]; + assign PIN_18 = parOut[4]; + assign PIN_19 = parOut[5]; + assign chrg[0] = PIN_3; + assign chrg[1] = PIN_4; + assign chrg[2] = PIN_5; + assign chrg[3] = PIN_6; + assign chrg[4] = PIN_7; + assign chrg[5] = PIN_8; + + SSCounter6o sc6(PIN_1, CLK, PIN_2, PIN_9, chrg, parOut); + +endmodule + +module SSCounter6 (input wire rst, clk, adv, jmp, input wire [5:0] in, output reg[5:0] out); + always @(posedge clk, posedge rst) + if (rst) out <= 0; + else if (adv || jmp) out <= jmp ? in : out + 1; +endmodule + +// Optimized 6 bit counter, it should takes 7 cells. +/* b[5:1] /* b[0] +1010101010101010 in 1010101010101010 in +1100110011001100 jmp 1100110011001100 jmp +1111000011110000 loop 1111000011110000 loop +1111111100000000 carry 1111111100000000 - +---------------------- ---------------------- +1000101110111000 out 1000101110001011 out + 8 B B 8 8 B 8 B +*/ +module SSCounter6o (input wire rst, clk, adv, jmp, input wire [5:0] in, output wire[5:0] out); + wire[4:0] co; + wire[5:0] lo; + wire ien; + SB_LUT4 #(.LUT_INIT(16'hFFF0)) lien (ien, 0, 0, adv, jmp); + SB_CARRY c0 (co[0], jmp, out[0], 1), + c1 (co[1], jmp, out[1], co[0]), + c2 (co[2], jmp, out[2], co[1]), + c3 (co[3], jmp, out[3], co[2]), + c4 (co[4], jmp, out[4], co[3]); + SB_DFFER d0 (out[0], clk, ien, rst, lo[0]), + d1 (out[1], clk, ien, rst, lo[1]), + d2 (out[2], clk, ien, rst, lo[2]), + d3 (out[3], clk, ien, rst, lo[3]), + d4 (out[4], clk, ien, rst, lo[4]), + d5 (out[5], clk, ien, rst, lo[5]); + SB_LUT4 #(.LUT_INIT(16'h8B8B)) l0 (lo[0], in[0], jmp, out[0], 0); + SB_LUT4 #(.LUT_INIT(16'h8BB8)) l1 (lo[1], in[1], jmp, out[1], co[0]); + SB_LUT4 #(.LUT_INIT(16'h8BB8)) l2 (lo[2], in[2], jmp, out[2], co[1]); + SB_LUT4 #(.LUT_INIT(16'h8BB8)) l3 (lo[3], in[3], jmp, out[3], co[2]); + SB_LUT4 #(.LUT_INIT(16'h8BB8)) l4 (lo[4], in[4], jmp, out[4], co[3]); + SB_LUT4 #(.LUT_INIT(16'h8BB8)) l5 (lo[5], in[5], jmp, out[5], co[4]); +endmodule +EOT +hierarchy -top top +flatten +equiv_opt -multiclock -map +/ice40/cells_sim.v synth_ice40 diff --git a/tests/arch/ice40/bug1598.ys b/tests/arch/ice40/bug1598.ys new file mode 100644 index 000000000..8438cb979 --- /dev/null +++ b/tests/arch/ice40/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 +/ice40/cells_sim.v synth_ice40 -abc9 diff --git a/tests/arch/ice40/bug1626.ys b/tests/arch/ice40/bug1626.ys new file mode 100644 index 000000000..27b6fb5e8 --- /dev/null +++ b/tests/arch/ice40/bug1626.ys @@ -0,0 +1,217 @@ +read_ilang <<EOT +# Generated by Yosys 0.9+1706 (git sha1 58ab9f60, clang 6.0.0-1ubuntu2 -fPIC -Os) +autoidx 2815 +attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:9" +attribute \cells_not_processed 1 +attribute \dynports 1 +module \ahb_async_sram_halfwidth + parameter \DEPTH + parameter \W_ADDR + parameter \W_BYTEADDR + parameter \W_DATA + parameter \W_SRAM_ADDR + parameter \W_SRAM_DATA + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71" + wire $0\addr_lsb[0:0] + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71" + wire $0\hready_r[0:0] + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71" + wire $0\long_dphase[0:0] + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71" + wire width 16 $0\rdata_buf[15:0] + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71" + wire $0\read_dph[0:0] + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71" + wire $0\write_dph[0:0] + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:63" + wire width 32 $add$../hdl/mem/ahb_async_sram_halfwidth.v:63$2433_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:62" + wire width 16 $and$../hdl/mem/ahb_async_sram_halfwidth.v:62$2431_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:56" + wire $eq$../hdl/mem/ahb_async_sram_halfwidth.v:56$2424_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2450_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2451_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2452_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2453_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2454_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2455_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2456_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2457_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2458_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2459_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:118" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:118$2444_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:133" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:133$2449_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:140" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:140$2461_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:140" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:140$2463_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:58" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:58$2425_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:59" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:59$2426_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:59" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:59$2427_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:59" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:59$2429_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:91" + wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:91$2441_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:104" + wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:104$2442_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:118" + wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:118$2443_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:125" + wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:125$2446_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:132" + wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:132$2447_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:59" + wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:59$2428_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:72" + wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:72$2437_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:81" + wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:81$2438_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:83" + wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:83$2439_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:91" + wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:91$2440_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:118" + wire $logic_or$../hdl/mem/ahb_async_sram_halfwidth.v:118$2445_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:132" + wire $logic_or$../hdl/mem/ahb_async_sram_halfwidth.v:132$2448_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:59" + wire $logic_or$../hdl/mem/ahb_async_sram_halfwidth.v:59$2430_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:139" + wire width 2 $not$../hdl/mem/ahb_async_sram_halfwidth.v:139$2460_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:139" + wire width 2 $not$../hdl/mem/ahb_async_sram_halfwidth.v:139$2462_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:54" + wire width 2 $not$../hdl/mem/ahb_async_sram_halfwidth.v:54$2421_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:63" + wire width 16 $shiftx$../hdl/mem/ahb_async_sram_halfwidth.v:63$2434_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:54" + wire width 8 $shl$../hdl/mem/ahb_async_sram_halfwidth.v:54$2419_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:54" + wire width 2 $shl$../hdl/mem/ahb_async_sram_halfwidth.v:54$2420_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:55" + wire width 2 $shl$../hdl/mem/ahb_async_sram_halfwidth.v:55$2422_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:56" + wire width 32 $shl$../hdl/mem/ahb_async_sram_halfwidth.v:56$2423_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:63" + wire width 32 $ternary$../hdl/mem/ahb_async_sram_halfwidth.v:63$2432_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:65" + wire width 16 $ternary$../hdl/mem/ahb_async_sram_halfwidth.v:65$2435_Y + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:50" + wire \addr_lsb + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:24" + wire width 32 \ahbls_haddr + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:28" + wire width 3 \ahbls_hburst + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:30" + wire \ahbls_hmastlock + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:29" + wire width 4 \ahbls_hprot + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:32" + wire width 32 \ahbls_hrdata + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:22" + wire \ahbls_hready + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:21" + wire \ahbls_hready_resp + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:23" + wire \ahbls_hresp + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:27" + wire width 3 \ahbls_hsize + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:26" + wire width 2 \ahbls_htrans + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:31" + wire width 32 \ahbls_hwdata + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:25" + wire \ahbls_hwrite + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:56" + wire \aphase_full_width + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:55" + wire width 2 \bytemask + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:54" + wire width 2 \bytemask_noshift + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:17" + wire \clk + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:46" + wire \hready_r + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:47" + wire \long_dphase + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:64" + wire width 16 \rdata_buf + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:49" + wire \read_dph + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:18" + wire \rst_n + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:34" + wire width 11 \sram_addr + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:39" + wire width 2 \sram_byte_n + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:36" + wire \sram_ce_n + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:35" + wire width 16 \sram_dq + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:38" + wire \sram_oe_n + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:61" + wire width 16 \sram_q + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:62" + wire width 16 \sram_rdata + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:63" + wire width 16 \sram_wdata + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:37" + wire \sram_we_n + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:58" + wire \we_next + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:48" + wire \write_dph + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71" + process $proc$../hdl/mem/ahb_async_sram_halfwidth.v:71$2436 + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:72" + switch $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:72$2437_Y + case 1'1 + case + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:78" + switch \ahbls_hready + case 1'1 + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:79" + switch \ahbls_htrans [1] + case 1'1 + case + end + case + attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:91" + switch $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:91$2441_Y + case 1'1 + case + end + end + end + sync posedge \clk + sync negedge \rst_n + end + connect \ahbls_hresp 1'0 + connect \bytemask_noshift $not$../hdl/mem/ahb_async_sram_halfwidth.v:54$2421_Y + connect \bytemask $shl$../hdl/mem/ahb_async_sram_halfwidth.v:55$2422_Y + connect \aphase_full_width $eq$../hdl/mem/ahb_async_sram_halfwidth.v:56$2424_Y + connect \we_next $logic_or$../hdl/mem/ahb_async_sram_halfwidth.v:59$2430_Y + connect \sram_rdata $and$../hdl/mem/ahb_async_sram_halfwidth.v:62$2431_Y + connect \sram_wdata $shiftx$../hdl/mem/ahb_async_sram_halfwidth.v:63$2434_Y + connect \ahbls_hrdata { \sram_rdata $ternary$../hdl/mem/ahb_async_sram_halfwidth.v:65$2435_Y } + connect \ahbls_hready_resp \hready_r +end +EOT + +synth_ice40 -abc2 -abc9 diff --git a/tests/arch/ice40/bug1644.il.gz b/tests/arch/ice40/bug1644.il.gz Binary files differnew file mode 100644 index 000000000..363c510ef --- /dev/null +++ b/tests/arch/ice40/bug1644.il.gz diff --git a/tests/arch/ice40/bug1644.ys b/tests/arch/ice40/bug1644.ys new file mode 100644 index 000000000..5950f0e3c --- /dev/null +++ b/tests/arch/ice40/bug1644.ys @@ -0,0 +1,2 @@ +read_ilang bug1644.il.gz +synth_ice40 -top top -dsp -json adc_dac_pass_through.json -run :map_bram diff --git a/tests/arch/ice40/counter.ys b/tests/arch/ice40/counter.ys index f112eb97d..7bbc4f2c3 100644 --- a/tests/arch/ice40/counter.ys +++ b/tests/arch/ice40/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -map +/ice40/cells_sim.v synth_ice40 # equivalency check +equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 # 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 6 t:SB_CARRY diff --git a/tests/arch/ice40/ice40_dsp.ys b/tests/arch/ice40/ice40_dsp.ys new file mode 100644 index 000000000..250273859 --- /dev/null +++ b/tests/arch/ice40/ice40_dsp.ys @@ -0,0 +1,11 @@ +read_verilog <<EOT +module top(input [15:0] a, b, output [31:0] o1, o2, o5); +SB_MAC16 m1 (.A(a), .B(16'd1234), .O(o1)); +assign o2 = a * 16'd0; +wire [31:0] o3, o4; +SB_MAC16 m2 (.A(a), .B(b), .O(o3)); +assign o4 = a * b; +SB_MAC16 m3 (.A(a), .B(b), .O(o5)); +endmodule +EOT +ice40_dsp diff --git a/tests/arch/ice40/ice40_opt.ys b/tests/arch/ice40/ice40_opt.ys index b17c69c91..71b68431e 100644 --- a/tests/arch/ice40/ice40_opt.ys +++ b/tests/arch/ice40/ice40_opt.ys @@ -6,13 +6,14 @@ module top(input CI, I0, output [1:0] CO, output O); // A[1]: 1100 1100 1100 1100 // A[2]: 1111 0000 1111 0000 // A[3]: 1111 1111 0000 0000 - .LUT(~16'b 0110_1001_1001_0110) + .LUT(~16'b 0110_1001_1001_0110), + .I3_IS_CI(1'b1) ) u0 ( .A(A), .B(B), .CI(CI), .I0(I0), - .I3(CI), + .I3(1'bx), .CO(CO[0]), .O(O) ); @@ -20,7 +21,98 @@ module top(input CI, I0, output [1:0] CO, output O); endmodule EOT -equiv_opt -assert -map +/ice40/cells_map.v -map +/ice40/cells_sim.v ice40_opt +equiv_opt -assert -map +/ice40/abc9_model.v -map +/ice40/cells_sim.v ice40_opt design -load postopt select -assert-count 1 t:* select -assert-count 1 t:$lut + +# https://github.com/YosysHQ/yosys/issues/1543 +design -reset +read_verilog <<EOT +module delay_element (input wire clk, input wire reset, input wire enable, + input wire chainin, output wire chainout, output reg latch); + + + reg const_zero = 0; + reg const_one = 1; + + wire delay_tap; + + + //carry logic + (* keep *) SB_CARRY carry ( .CO(chainout), .I0(const_zero), + .I1(const_one), .CI(chainin)); + + + //flip flop latch + (* keep *) SB_DFFER flipflop( .Q(latch), .C(clk), .E(enable), + .D(delay_tap), .R(reset)); + + + //LUT table + // the LUT should just echo the carry in (I3) + // carry I0 = LUT I1 + // carry I1 = LUT I2 + // carry in = LUT I3 + // LUT_INIT[0] = 0 + // LUT_INIT[1] = 0 + // LUT_INIT[2] = 0 + // LUT_INIT[3] = 0 + // LUT_INIT[4] = 0 + // LUT_INIT[5] = 0 + // LUT_INIT[6] = 0 + // LUT_INIT[7] = 0 + // LUT_INIT[8] = 1 + // LUT_INIT[9] = 1 + // LUT_INIT[10] = 1 + // LUT_INIT[11] = 1 + // LUT_INIT[12] = 1 + // LUT_INIT[13] = 1 + // LUT_INIT[14] = 1 + // LUT_INIT[15] = 1 + + (* keep *) SB_LUT4 lut( .O(delay_tap), .I0(const_zero), .I1(const_zero), + .I2(const_one), .I3(chainin)); + + //TODO: is this the right way round?? + defparam lut.LUT_INIT=16'hFF00; + + +endmodule // delay_element +EOT + +synth_ice40 +select -assert-count 1 t:SB_LUT4 +select -assert-count 1 t:SB_CARRY +select -assert-count 1 t:SB_CARRY a:keep %i +select -assert-count 1 t:SB_CARRY c:carry %i + + +design -reset +read_verilog -icells <<EOT +module top(input I3, I2, I1, I0, output O, O2); + SB_LUT4 #( + .LUT_INIT(8'b 1001_0110) + ) u0 ( + .I0(I0), + .I1(I1), + .I2(I2), + .I3(), + .O(O) + ); + wire CO; + \$__ICE40_CARRY_WRAPPER #( + .LUT(~8'b 1001_0110), + .I3_IS_CI(1'b0) + ) u1 ( + .A(1'b0), + .B(1'b0), + .CI(1'b0), + .I0(), + .I3(), + .CO(CO), + .O(O2) + ); +endmodule +EOT +ice40_opt diff --git a/tests/arch/ice40/ice40_wrapcarry.ys b/tests/arch/ice40/ice40_wrapcarry.ys new file mode 100644 index 000000000..fb9fccc3a --- /dev/null +++ b/tests/arch/ice40/ice40_wrapcarry.ys @@ -0,0 +1,54 @@ +read_verilog <<EOT +module top(input A, B, CI, output O, CO); + SB_CARRY carry ( + .I0(A), + .I1(B), + .CI(CI), + .CO(CO) + ); + SB_LUT4 #( + .LUT_INIT(16'b 0110_1001_1001_0110) + ) adder ( + .I0(1'b0), + .I1(A), + .I2(B), + .I3(1'b0), + .O(O) + ); +endmodule +EOT + +ice40_wrapcarry +select -assert-count 1 t:$__ICE40_CARRY_WRAPPER + +design -reset +read_verilog <<EOT +module top(input A, B, CI, output O, CO); + (* foo = "bar", answer = 42, keep=0 *) + SB_CARRY carry ( + .I0(A), + .I1(B), + .CI(CI), + .CO(CO) + ); + (* keep, blah="blah", answer = 43 *) + SB_LUT4 #( + .LUT_INIT(16'b 0110_1001_1001_0110) + ) adder ( + .I0(1'b0), + .I1(A), + .I2(B), + .I3(1'b0), + .O(O) + ); +endmodule +EOT + +ice40_wrapcarry +select -assert-count 1 t:$__ICE40_CARRY_WRAPPER +select -assert-count 0 t:* t:$__ICE40_CARRY_WRAPPER %d +select -assert-count 1 a:keep=1 a:SB_CARRY.\foo=bar %i a:SB_CARRY.\answer=42 %i a:SB_LUT4.\blah=blah %i a:SB_LUT4.\answer=43 %i + +ice40_wrapcarry -unwrap +select -assert-count 1 c:carry a:src=<<EOT:3 %i a:keep=0 %i a:foo=bar %i a:answer=42 %i +select -assert-count 1 c:adder a:src=<<EOT:10 %i a:keep=1 %i a:blah=blah %i a:answer=43 %i diff --git a/tests/arch/ice40/memory.ys b/tests/arch/ice40/lutram.ys index c356e67fb..1ba40f8ec 100644 --- a/tests/arch/ice40/memory.ys +++ b/tests/arch/ice40/lutram.ys @@ -1,5 +1,5 @@ -read_verilog ../common/memory.v -hierarchy -top top +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r proc memory -nomap equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40 @@ -10,6 +10,6 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter design -load postopt -cd top +cd lutram_1w1r select -assert-count 1 t:SB_RAM40_4K select -assert-none t:SB_RAM40_4K %% t:* %D diff --git a/tests/arch/ice40/mul.ys b/tests/arch/ice40/mul.ys index 9891b77d6..b8c3eb941 100644 --- a/tests/arch/ice40/mul.ys +++ b/tests/arch/ice40/mul.ys @@ -1,6 +1,6 @@ read_verilog ../common/mul.v hierarchy -top top -equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check +equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 -dsp # 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:SB_MAC16 diff --git a/tests/arch/ice40/rom.v b/tests/arch/ice40/rom.v index 0a0f41f37..71459fe38 100644 --- a/tests/arch/ice40/rom.v +++ b/tests/arch/ice40/rom.v @@ -2,7 +2,8 @@ Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 74]. */ module top(data, addr); -output [3:0] data; +output [3:0] data; // Note: this prompts a Yosys warning, but + // vendor doc does not contain 'reg' input [4:0] addr; always @(addr) begin case (addr) diff --git a/tests/arch/ice40/wrapcarry.ys b/tests/arch/ice40/wrapcarry.ys deleted file mode 100644 index 10c029e68..000000000 --- a/tests/arch/ice40/wrapcarry.ys +++ /dev/null @@ -1,22 +0,0 @@ -read_verilog <<EOT -module top(input A, B, CI, output O, CO); - SB_CARRY carry ( - .I0(A), - .I1(B), - .CI(CI), - .CO(CO) - ); - SB_LUT4 #( - .LUT_INIT(16'b 0110_1001_1001_0110) - ) adder ( - .I0(1'b0), - .I1(A), - .I2(B), - .I3(1'b0), - .O(O) - ); -endmodule -EOT - -ice40_wrapcarry -select -assert-count 1 t:$__ICE40_CARRY_WRAPPER 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 index 9dbddce47..70cfe81a3 100644 --- a/tests/arch/xilinx/add_sub.ys +++ b/tests/arch/xilinx/add_sub.ys @@ -1,11 +1,11 @@ read_verilog ../common/add_sub.v hierarchy -top top proc -equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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 14 t:LUT2 -select -assert-count 6 t:MUXCY -select -assert-count 8 t:XORCY -select -assert-none t:LUT2 t:MUXCY t:XORCY %% t:* %D +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 index 12c34415e..3328f9edc 100644 --- a/tests/arch/xilinx/adffs.ys +++ b/tests/arch/xilinx/adffs.ys @@ -3,7 +3,7 @@ design -save read hierarchy -top adff proc -equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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 @@ -15,37 +15,36 @@ 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 # equivalency check +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:LUT1 +select -assert-count 1 t:INV -select -assert-none t:BUFG t:FDCE t:LUT1 %% t:* %D +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 # equivalency check +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:FDRE -select -assert-count 1 t:LUT2 +select -assert-count 1 t:FDSE -select -assert-none t:BUFG t:FDRE t:LUT2 %% t:* %D +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 # equivalency check +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:LUT2 +select -assert-count 1 t:INV -select -assert-none t:BUFG t:FDRE_1 t:LUT2 %% t:* %D +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/various/bug1462.ys b/tests/arch/xilinx/bug1462.ys index 15cab5121..15cab5121 100644 --- a/tests/various/bug1462.ys +++ b/tests/arch/xilinx/bug1462.ys 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 index 57b645d19..064519ce7 100644 --- a/tests/arch/xilinx/counter.ys +++ b/tests/arch/xilinx/counter.ys @@ -2,13 +2,12 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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:LUT1 -select -assert-count 7 t:MUXCY -select -assert-count 8 t:XORCY -select -assert-none t:BUFG t:FDCE t:LUT1 t:MUXCY t:XORCY %% t:* %D +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 index 0bba4858f..dc764b033 100644 --- a/tests/arch/xilinx/dffs.ys +++ b/tests/arch/xilinx/dffs.ys @@ -3,7 +3,7 @@ design -save read hierarchy -top dff proc -equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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 @@ -15,7 +15,7 @@ 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 # equivalency check +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 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/fsm.ys b/tests/arch/xilinx/fsm.ys index 2a72c34e8..a464fcfdb 100644 --- a/tests/arch/xilinx/fsm.ys +++ b/tests/arch/xilinx/fsm.ys @@ -3,16 +3,17 @@ hierarchy -top fsm proc flatten -equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +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 5 t:FDRE -select -assert-count 1 t:LUT3 -select -assert-count 2 t:LUT4 -select -assert-count 4 t:LUT6 -select -assert-none t:BUFG t:FDRE t:LUT3 t:LUT4 t:LUT6 %% t:* %D +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 index fe7887e8d..e226c2ec8 100644 --- a/tests/arch/xilinx/latches.ys +++ b/tests/arch/xilinx/latches.ys @@ -3,7 +3,7 @@ design -save read hierarchy -top latchp proc -equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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 @@ -14,19 +14,19 @@ 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 # equivalency check +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:LUT1 +select -assert-count 1 t:INV -select -assert-none t:LDCE t:LUT1 %% t:* %D +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 # equivalency check +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 diff --git a/tests/arch/xilinx/logic.ys b/tests/arch/xilinx/logic.ys index c0f6da302..61a9314cc 100644 --- a/tests/arch/xilinx/logic.ys +++ b/tests/arch/xilinx/logic.ys @@ -1,11 +1,11 @@ read_verilog ../common/logic.v hierarchy -top top proc -equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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:LUT1 +select -assert-count 1 t:INV select -assert-count 6 t:LUT2 select -assert-count 2 t:LUT4 -select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D +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 index 2272679ee..58b97b646 100644 --- a/tests/arch/xilinx/macc.sh +++ b/tests/arch/xilinx/macc.sh @@ -1,3 +1,6 @@ -../../../yosys -qp "synth_xilinx -top macc2; rename -top macc2_uut" macc.v -o macc_uut.v +../../../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.ys b/tests/arch/xilinx/macc.ys index 6e884b35a..bf2b36320 100644 --- a/tests/arch/xilinx/macc.ys +++ b/tests/arch/xilinx/macc.ys @@ -3,8 +3,8 @@ design -save read hierarchy -top macc proc -#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO -equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +#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) @@ -17,15 +17,16 @@ 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 ### TODO -equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +#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 41 t:LUT3 +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/memory.ys b/tests/arch/xilinx/memory.ys deleted file mode 100644 index da1ed0e49..000000000 --- a/tests/arch/xilinx/memory.ys +++ /dev/null @@ -1,17 +0,0 @@ -read_verilog ../common/memory.v -hierarchy -top top -proc -memory -nomap -equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -memory -opt -full - -miter -equiv -flatten -make_assert -make_outputs gold gate miter -sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter - -design -load postopt -cd top -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 diff --git a/tests/arch/xilinx/mul.ys b/tests/arch/xilinx/mul.ys index d76814966..490846ff1 100644 --- a/tests/arch/xilinx/mul.ys +++ b/tests/arch/xilinx/mul.ys @@ -1,9 +1,21 @@ read_verilog ../common/mul.v hierarchy -top top proc -equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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.ys b/tests/arch/xilinx/mul_unsigned.ys index 62495b90c..980263cbd 100644 --- a/tests/arch/xilinx/mul_unsigned.ys +++ b/tests/arch/xilinx/mul_unsigned.ys @@ -2,10 +2,24 @@ read_verilog mul_unsigned.v hierarchy -top mul_unsigned proc -equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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 index 821d0fab7..99817738d 100644 --- a/tests/arch/xilinx/mux.ys +++ b/tests/arch/xilinx/mux.ys @@ -3,7 +3,7 @@ design -save read hierarchy -top mux2 proc -equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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 @@ -14,7 +14,7 @@ select -assert-none t:LUT3 %% t:* %D design -load read hierarchy -top mux4 proc -equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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 @@ -25,7 +25,7 @@ select -assert-none t:LUT6 %% t:* %D design -load read hierarchy -top mux8 proc -equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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 @@ -37,9 +37,11 @@ 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 # equivalency check +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-count 5 t:LUT6 +select -assert-min 5 t:LUT6 +select -assert-max 7 t:LUT6 +select -assert-max 2 t:MUXF7 -select -assert-none t:LUT6 %% t:* %D +select -assert-none t:LUT6 t:MUXF7 %% t:* %D diff --git a/tests/arch/xilinx/shifter.ys b/tests/arch/xilinx/shifter.ys index 455437f18..3652319a0 100644 --- a/tests/arch/xilinx/shifter.ys +++ b/tests/arch/xilinx/shifter.ys @@ -2,7 +2,7 @@ read_verilog ../common/shifter.v hierarchy -top top proc flatten -equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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 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 index 4697703ca..eaccab126 100644 --- a/tests/arch/xilinx/tribuf.ys +++ b/tests/arch/xilinx/tribuf.ys @@ -7,6 +7,7 @@ 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 -# TODO :: Tristate logic not yet supported; see https://github.com/YosysHQ/yosys/issues/1225 -select -assert-count 1 t:$_TBUF_ -select -assert-none t:$_TBUF_ %% t:* %D +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/opt/bug1525.ys b/tests/opt/bug1525.ys new file mode 100644 index 000000000..972bc0ac7 --- /dev/null +++ b/tests/opt/bug1525.ys @@ -0,0 +1,13 @@ +read_verilog << EOF +module top(...); +input A1, A2, B, S; +output O; + +assign O = S ? (A1 & B) : (A2 & B); + +endmodule +EOF + +simplemap +opt_share +dump diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys index 2079d2f34..1436724b0 100644 --- a/tests/sat/initval.ys +++ b/tests/sat/initval.ys @@ -2,3 +2,14 @@ read_verilog -sv initval.v proc;; sat -seq 10 -prove-asserts + +design -reset +read_verilog -icells <<EOT +module top(input clk, i, output [1:0] o); +(* init = 2'bx0 *) +wire [1:0] o; +assign o[1] = o[0]; +$_DFF_P_ dff (.C(clk), .D(i), .Q(o[0])); +endmodule +EOT +sat -seq 1 diff --git a/tests/simple/mem_arst.v b/tests/simple/mem_arst.v index 9bd38fcb3..88d0553b9 100644 --- a/tests/simple/mem_arst.v +++ b/tests/simple/mem_arst.v @@ -7,11 +7,9 @@ module MyMem #( input Clk_i, input [AddrWidth-1:0] Addr_i, input [DataWidth-1:0] Data_i, - output [DataWidth-1:0] Data_o, + output reg [DataWidth-1:0] Data_o, input WR_i); - reg [DataWidth-1:0] Data_o; - localparam Size = 2**AddrWidth; (* mem2reg *) diff --git a/tests/simple_abc9/abc9.v b/tests/simple_abc9/abc9.v index 64b625efe..e5837d480 100644 --- a/tests/simple_abc9/abc9.v +++ b/tests/simple_abc9/abc9.v @@ -213,17 +213,11 @@ module arbiter (clk, rst, request, acknowledge, grant, grant_valid, grant_encode input rst; endmodule -(* abc_box_id=1 *) +(* abc9_box_id=1, whitebox *) module MUXF8(input I0, I1, S, output O); endmodule // Citation: https://github.com/alexforencich/verilog-ethernet -// TODO: yosys -p "synth_xilinx -abc9 -top abc9_test022" abc9.v -q -// returns before b4321a31 -// Warning: Wire abc9_test022.\m_eth_payload_axis_tkeep [7] is used but has no -// driver. -// Warning: Wire abc9_test022.\m_eth_payload_axis_tkeep [3] is used but has no -// driver. module abc9_test022 ( input wire clk, @@ -237,9 +231,6 @@ module abc9_test022 endmodule // Citation: https://github.com/riscv/riscv-bitmanip -// TODO: yosys -p "synth_xilinx -abc9 -top abc9_test023" abc9.v -q -// returns before 14233843 -// Warning: Wire abc9_test023.\dout [1] is used but has no driver. module abc9_test023 #( parameter integer N = 2, parameter integer M = 2 @@ -267,3 +258,52 @@ module abc9_test026(output [3:0] o, p); assign o = { 1'b1, 1'bx }; assign p = { 1'b1, 1'bx, 1'b0 }; endmodule + +module abc9_test030(input [3:0] d, input en, output reg [3:0] q); +always @* + if (en) + q <= d; +endmodule + +module abc9_test031(input clk1, clk2, d, output reg q1, q2); +always @(posedge clk1) q1 <= d; +always @(negedge clk2) q2 <= q1; +endmodule + +module abc9_test032(input clk, d, r, output reg q); +always @(posedge clk or posedge r) + if (r) q <= 1'b0; + else q <= d; +endmodule + +module abc9_test033(input clk, d, r, output reg q); +always @(negedge clk or posedge r) + if (r) q <= 1'b1; + else q <= d; +endmodule + +module abc9_test034(input clk, d, output reg q1, q2); +always @(posedge clk) q1 <= d; +always @(posedge clk) q2 <= q1; +endmodule + +module abc9_test035(input clk, d, output reg [1:0] q); +always @(posedge clk) q[0] <= d; +always @(negedge clk) q[1] <= q[0]; +endmodule + +module abc9_test036(input A, B, S, output [1:0] O); + (* keep *) + MUXF8 m ( + .I0(I0), + .I1(I1), + .O(O[0]), + .S(S) + ); + MUXF8 m2 ( + .I0(I0), + .I1(I1), + .O(O[1]), + .S(S) + ); +endmodule diff --git a/tests/simple_abc9/run-test.sh b/tests/simple_abc9/run-test.sh index 0d4262005..32d7a80ca 100755 --- a/tests/simple_abc9/run-test.sh +++ b/tests/simple_abc9/run-test.sh @@ -20,10 +20,13 @@ fi cp ../simple/*.v . cp ../simple/*.sv . DOLLAR='?' -exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v EXTRA_FLAGS="-n 300 -p '\ +exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v *.sv EXTRA_FLAGS="-n 300 -p '\ hierarchy; \ synth -run coarse; \ opt -full; \ - techmap; abc9 -lut 4 -box ../abc.box; \ + techmap; \ + abc9 -lut 4 -box ../abc.box; \ + clean; \ check -assert; \ - select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'" + select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%; \ + setattr -mod -unset whitebox'" diff --git a/tests/techmap/abc9.ys b/tests/techmap/abc9.ys new file mode 100644 index 000000000..2140dde26 --- /dev/null +++ b/tests/techmap/abc9.ys @@ -0,0 +1,81 @@ +read_verilog <<EOT +`define N 256 +module top(input [`N-1:0] a, output o); +wire [`N-2:0] w; +assign w[0] = a[0] & a[1]; +genvar i; +generate for (i = 1; i < `N-1; i++) +assign w[i] = w[i-1] & a[i+1]; +endgenerate +assign o = w[`N-2]; +endmodule +EOT +simplemap +dump +design -save gold + +abc9 -lut 4 + +design -load gold +abc9 -lut 4 -fast + +design -load gold +scratchpad -copy abc9.script.default.area abc9.script +abc9 -lut 4 + +design -load gold +scratchpad -copy abc9.script.default.fast abc9.script +abc9 -lut 4 + +design -load gold +scratchpad -copy abc9.script.flow abc9.script +abc9 -lut 4 + +design -load gold +scratchpad -copy abc9.script.flow2 abc9.script +abc9 -lut 4 + +design -load gold +scratchpad -copy abc9.script.flow3 abc9.script +abc9 -lut 4 + +design -reset +read_verilog <<EOT +module top(input a, b, output o); +(* keep *) wire w = a & b; +assign o = ~w; +endmodule +EOT + +simplemap +equiv_opt -assert abc9 -lut 4 +design -load postopt +select -assert-count 2 t:$lut + + +design -reset +read_verilog -icells <<EOT +module top(input a, b, output o); +wire w; +(* keep *) $_AND_ gate (.Y(w), .A(a), .B(b)); +assign o = ~w; +endmodule +EOT + +simplemap +equiv_opt -assert abc9 -lut 4 +design -load postopt +select -assert-count 1 t:$lut +select -assert-count 1 t:$_AND_ + + +design -reset +read_verilog -icells <<EOT +module top(input a, b, output o); +assign o = ~(a & b); +endmodule +EOT +abc9 -lut 4 +clean +select -assert-count 1 t:$lut +select -assert-none t:$lut t:* %D diff --git a/tests/techmap/clkbufmap.ys b/tests/techmap/clkbufmap.ys index f1277864e..b81a35e74 100644 --- a/tests/techmap/clkbufmap.ys +++ b/tests/techmap/clkbufmap.ys @@ -4,6 +4,7 @@ module dff ((* clkbuf_sink *) input clk, input d, output q); endmodule module dffe ((* clkbuf_sink *) input c, input d, e, output q); endmodule module latch (input e, d, output q); endmodule module clkgen (output o); endmodule +module inv ((* clkbuf_inv = "i" *) output o, input i); endmodule module top(input clk1, clk2, clk3, d, e, output [4:0] q); wire clk4, clk5, clk6; @@ -17,12 +18,18 @@ dff s6 (.clk(clk6), .d(d), .q(q[4])); endmodule module sub(output sclk4, output sclk5, output sclk6, input sd, output sq); +wire sclk7, sclk8, sclk9; +wire siq; wire tmp; clkgen s7(.o(sclk4)); clkgen s8(.o(sclk5)); clkgen s9(.o(tmp)); -clkbuf s10(.i(tmp), .o(sclk6)); -dff s11(.clk(sclk4), .d(sd), .q(sq)); +clkbuf s10(.i(tmp), .o(sclk7)); +dff s11(.clk(sclk4), .d(sd), .q(siq)); +inv s15(.i(sclk7), .o(sclk6)); +clkgen s12(.o(sclk8)); +inv s13(.o(sclk9), .i(sclk8)); +dff s14(.clk(sclk9), .d(siq), .q(sq)); endmodule EOT @@ -34,7 +41,7 @@ design -save ref design -load ref clkbufmap -buf clkbuf o:i select -assert-count 3 top/t:clkbuf -select -assert-count 2 sub/t:clkbuf +select -assert-count 3 sub/t:clkbuf select -set clk1 w:clk1 %a %co t:clkbuf %i # Find 'clk1' fanouts that are 'clkbuf' select -assert-count 1 @clk1 # Check there is one such fanout select -assert-count 1 @clk1 %x:+[o] %co c:s* %i # Check that the 'o' of that clkbuf drives one fanout @@ -51,6 +58,10 @@ select -set sclk4 w:sclk4 %a %ci t:clkbuf %i select -assert-count 1 @sclk4 select -assert-count 1 @sclk4 %x:+[o] %co c:s11 %i select -assert-count 1 @sclk4 %x:+[i] %ci c:s7 %i +select -set sclk8 w:sclk8 %a %ci t:clkbuf %i +select -assert-count 1 @sclk8 +select -assert-count 1 @sclk8 %x:+[o] %co c:s13 %i +select -assert-count 1 @sclk8 %x:+[i] %ci c:s12 %i # ---------------------- @@ -72,7 +83,7 @@ setattr -set clkbuf_inhibit 1 w:clk1 setattr -set buffer_type "bufg" w:clk2 clkbufmap -buf clkbuf o:i w:* a:buffer_type=none a:buffer_type=bufr %u %d select -assert-count 3 top/t:clkbuf -select -assert-count 2 sub/t:clkbuf +select -assert-count 3 sub/t:clkbuf select -set clk1 w:clk1 %a %co t:clkbuf %i # Find 'clk1' fanouts that are 'clkbuf' select -assert-count 1 @clk1 # Check there is one such fanout select -assert-count 1 @clk1 %x:+[o] %co c:s* %i # Check that the 'o' of that clkbuf drives one fanout @@ -93,4 +104,4 @@ clkbufmap -buf clkbuf o:i w:* a:buffer_type=none a:buffer_type=bufr %u %d select -assert-count 0 w:clk1 %a %co t:clkbuf %i select -assert-count 0 w:clk2 %a %co t:clkbuf %i select -assert-count 0 top/t:clkbuf -select -assert-count 1 sub/t:clkbuf +select -assert-count 2 sub/t:clkbuf diff --git a/tests/techmap/iopadmap.ys b/tests/techmap/iopadmap.ys new file mode 100644 index 000000000..c058d1607 --- /dev/null +++ b/tests/techmap/iopadmap.ys @@ -0,0 +1,122 @@ +read_verilog << EOT +module ibuf ((* iopad_external_pin *) input i, output o); endmodule +module obuf (input i, (* iopad_external_pin *) output o); endmodule +module obuft (input i, input oe, (* iopad_external_pin *) output o); endmodule +module iobuf (input i, input oe, output o, (* iopad_external_pin *) inout io); endmodule + +module a(input i, output o); +assign o = i; +endmodule + +module b(input i, output o); +assign o = i; +ibuf b (.i(i), .o(o)); +endmodule + +module c(input i, output o); +obuf b (.i(i), .o(o)); +endmodule + +module d(input i, oe, output o, o2, o3); +assign o = oe ? i : 1'bz; +assign o2 = o; +assign o3 = ~o; +endmodule + +module e(input i, oe, inout io, output o2, o3); +assign io = oe ? i : 1'bz; +assign o2 = io; +assign o3 = ~io; +endmodule + +module f(output o, o2); +assign o = 1'bz; +endmodule + +module g(inout io, output o); +assign o = io; +endmodule + +module h(inout io, output o, input i); +assign io = i; +assign o = io; +endmodule + +EOT + +opt_clean +tribuf +simplemap +iopadmap -bits -inpad ibuf o:i -outpad obuf i:o -toutpad obuft oe:i:o -tinoutpad iobuf oe:o:i:io +opt_clean + +select -assert-count 1 a/t:ibuf +select -assert-count 1 a/t:obuf +select -set ib w:i %a %co a/t:ibuf %i +select -set ob w:o %a %ci a/t:obuf %i +select -assert-count 1 @ib +select -assert-count 1 @ob +select -assert-count 1 @ib %co %co @ob %i + +select -assert-count 1 b/t:ibuf +select -assert-count 1 b/t:obuf +select -set ib w:i %a %co b/t:ibuf %i +select -set ob w:o %a %ci b/t:obuf %i +select -assert-count 1 @ib +select -assert-count 1 @ob +select -assert-count 1 @ib %co %co @ob %i + +select -assert-count 1 c/t:ibuf +select -assert-count 1 c/t:obuf +select -set ib w:i %a %co c/t:ibuf %i +select -set ob w:o %a %ci c/t:obuf %i +select -assert-count 1 @ib +select -assert-count 1 @ob +select -assert-count 1 @ib %co %co @ob %i + +select -assert-count 2 d/t:ibuf +select -assert-count 2 d/t:obuf +select -assert-count 1 d/t:obuft +select -set ib w:i %a %co d/t:ibuf %i +select -set oeb w:oe %a %co d/t:ibuf %i +select -set ob w:o %a %ci d/t:obuft %i +select -set o2b w:o2 %a %ci d/t:obuf %i +select -set o3b w:o3 %a %ci d/t:obuf %i +select -assert-count 1 @ib +select -assert-count 1 @oeb +select -assert-count 1 @ob +select -assert-count 1 @o2b +select -assert-count 1 @o3b +select -assert-count 1 @ib %co %co @ob %i +select -assert-count 1 @oeb %co %co @ob %i +select -assert-count 1 @ib %co %co @o2b %i +select -assert-count 1 @ib %co %co t:$_NOT_ %i +select -assert-count 1 @o3b %ci %ci t:$_NOT_ %i + +select -assert-count 2 e/t:ibuf +select -assert-count 2 e/t:obuf +select -assert-count 1 e/t:iobuf +select -set ib w:i %a %co e/t:ibuf %i +select -set oeb w:oe %a %co e/t:ibuf %i +select -set iob w:io %a %ci e/t:iobuf %i +select -set o2b w:o2 %a %ci e/t:obuf %i +select -set o3b w:o3 %a %ci e/t:obuf %i +select -assert-count 1 @ib +select -assert-count 1 @oeb +select -assert-count 1 @iob +select -assert-count 1 @o2b +select -assert-count 1 @o3b +select -assert-count 1 @ib %co %co @iob %i +select -assert-count 1 @oeb %co %co @iob %i +select -assert-count 1 @iob %co %co @o2b %i +select -assert-count 1 @iob %co %co t:$_NOT_ %i +select -assert-count 1 @o3b %ci %ci t:$_NOT_ %i + +select -assert-count 2 f/t:obuft + +select -assert-count 1 g/t:obuf +select -assert-count 1 g/t:iobuf + +select -assert-count 1 h/t:ibuf +select -assert-count 1 h/t:iobuf +select -assert-count 1 h/t:obuf diff --git a/tests/various/abc9.v b/tests/various/abc9.v index 30ebd4e26..f0b3f6837 100644 --- a/tests/various/abc9.v +++ b/tests/various/abc9.v @@ -9,3 +9,10 @@ wire w; unknown u(~i, w); unknown2 u2(w, o); endmodule + +module abc9_test032(input clk, d, r, output reg q); +initial q = 1'b0; +always @(negedge clk or negedge r) + if (!r) q <= 1'b0; + else q <= d; +endmodule diff --git a/tests/various/abc9.ys b/tests/various/abc9.ys index 5c9a4075d..0c7695089 100644 --- a/tests/various/abc9.ys +++ b/tests/various/abc9.ys @@ -14,6 +14,7 @@ design -import gate -as gate miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -show-ports miter + design -load read hierarchy -top abc9_test028 proc @@ -22,3 +23,33 @@ abc9 -lut 4 select -assert-count 1 t:$lut r:LUT=2'b01 r:WIDTH=1 %i %i select -assert-count 1 t:unknown select -assert-none t:$lut t:unknown %% t: %D + + +design -load read +hierarchy -top abc9_test032 +proc +clk2fflogic +design -save gold + +abc9 -lut 4 +check +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -seq 10 -verify -prove-asserts -show-ports miter + + +design -reset +read_verilog -icells <<EOT +module abc9_test036(input clk, d, output q); +(* keep *) reg w; +$__ABC9_FF_ ff(.D(d), .Q(w)); +wire \ff.clock = clk; +wire \ff.init = 1'b0; +assign q = w; +endmodule +EOT +abc9 -lut 4 -dff diff --git a/tests/various/autoname.ys b/tests/various/autoname.ys new file mode 100644 index 000000000..830962e81 --- /dev/null +++ b/tests/various/autoname.ys @@ -0,0 +1,19 @@ +read_ilang <<EOT +autoidx 2 +module \top + wire output 3 $y + wire input 1 \a + wire input 2 \b + cell $and \b_$and_B + parameter \A_SIGNED 0 + parameter \A_WIDTH 1 + parameter \B_SIGNED 0 + parameter \B_WIDTH 1 + parameter \Y_WIDTH 1 + connect \A \a + connect \B \b + connect \Y $y + end +end +EOT +autoname diff --git a/tests/various/bug1531.ys b/tests/various/bug1531.ys new file mode 100644 index 000000000..542223030 --- /dev/null +++ b/tests/various/bug1531.ys @@ -0,0 +1,34 @@ +read_verilog <<EOT +module top (y, clk, w); + output reg y = 1'b0; + input clk, w; + reg [1:0] i = 2'b00; + always @(posedge clk) + // If the constant below is set to 2'b00, the correct output is generated. + // vvvv + for (i = 1'b0; i < 2'b01; i = i + 2'b01) + y <= w || i[1:1]; +endmodule +EOT + +synth +design -stash gate + +read_verilog <<EOT +module gold (y, clk, w); + input clk; + wire [1:0] i; + input w; + output y; + reg y = 1'h0; + always @(posedge clk) + y <= w; + assign i = 2'h0; +endmodule +EOT +proc gold + +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -seq 10 -verify -prove-asserts -show-ports miter diff --git a/tests/various/help.ys b/tests/various/help.ys new file mode 100644 index 000000000..9283ce8f1 --- /dev/null +++ b/tests/various/help.ys @@ -0,0 +1,2 @@ +help -all +help -celltypes diff --git a/tests/various/scratchpad.ys b/tests/various/scratchpad.ys new file mode 100644 index 000000000..dc94081ea --- /dev/null +++ b/tests/various/scratchpad.ys @@ -0,0 +1,5 @@ +scratchpad -set foo "bar baz" +scratchpad -copy foo oof +scratchpad -unset foo +scratchpad -assert oof "bar baz" +scratchpad -assert-unset foo |