diff options
Diffstat (limited to 'tests/arch')
30 files changed, 886 insertions, 49 deletions
diff --git a/tests/arch/anlogic/fsm.ys b/tests/arch/anlogic/fsm.ys index f45951b13..0bcc4e011 100644 --- a/tests/arch/anlogic/fsm.ys +++ b/tests/arch/anlogic/fsm.ys @@ -1,12 +1,15 @@ read_verilog ../common/fsm.v hierarchy -top fsm proc -#flatten -#ERROR: Found 4 unproven $equiv cells in 'equiv_status -assert'. -#equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # equivalency check -equiv_opt -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +flatten + +equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic +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 + select -assert-count 1 t:AL_MAP_LUT2 select -assert-count 5 t:AL_MAP_LUT5 select -assert-count 1 t:AL_MAP_LUT6 diff --git a/tests/arch/common/blockram_params.v b/tests/arch/common/blockram_params.v new file mode 100644 index 000000000..dbc6ca65c --- /dev/null +++ b/tests/arch/common/blockram_params.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/ecp5/fsm.ys b/tests/arch/ecp5/fsm.ys index f834a4c6b..ba91e5fc0 100644 --- a/tests/arch/ecp5/fsm.ys +++ b/tests/arch/ecp5/fsm.ys @@ -2,11 +2,16 @@ read_verilog ../common/fsm.v hierarchy -top fsm proc flatten -equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check + +equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5 +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 + select -assert-count 1 t:L6MUX21 -select -assert-count 13 t:LUT4 -select -assert-count 5 t:PFUMX -select -assert-count 5 t:TRELLIS_FF +select -assert-count 15 t:LUT4 +select -assert-count 6 t:PFUMX +select -assert-count 6 t:TRELLIS_FF select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_FF %% t:* %D diff --git a/tests/arch/efinix/fsm.ys b/tests/arch/efinix/fsm.ys index a8ba70fdb..a2db2ad98 100644 --- a/tests/arch/efinix/fsm.ys +++ b/tests/arch/efinix/fsm.ys @@ -2,9 +2,11 @@ read_verilog ../common/fsm.v hierarchy -top fsm proc flatten -#ERROR: Found 4 unproven $equiv cells in 'equiv_status -assert'. -#equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check -equiv_opt -map +/efinix/cells_sim.v synth_efinix # equivalency check + +equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix +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 diff --git a/tests/arch/gowin/.gitignore b/tests/arch/gowin/.gitignore new file mode 100644 index 000000000..b48f808a1 --- /dev/null +++ b/tests/arch/gowin/.gitignore @@ -0,0 +1,3 @@ +/*.log +/*.out +/run-test.mk diff --git a/tests/arch/gowin/add_sub.ys b/tests/arch/gowin/add_sub.ys new file mode 100644 index 000000000..9b53dc0a9 --- /dev/null +++ b/tests/arch/gowin/add_sub.ys @@ -0,0 +1,13 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +proc +equiv_opt -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 top # Constrain all select calls below inside the top module +select -assert-count 8 t:ALU +select -assert-count 8 t:OBUF +select -assert-count 8 t:IBUF +select -assert-count 1 t:GND +select -assert-count 1 t:VCC +select -assert-none t:ALU t:OBUF t:IBUF t:GND t:VCC %% t:* %D + diff --git a/tests/arch/gowin/adffs.ys b/tests/arch/gowin/adffs.ys new file mode 100644 index 000000000..87fba83a6 --- /dev/null +++ b/tests/arch/gowin/adffs.ys @@ -0,0 +1,56 @@ +read_verilog ../common/adffs.v +design -save read + +hierarchy -top adff +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 adff # Constrain all select calls below inside the top module +stat +select -assert-count 1 t:DFFC +select -assert-count 3 t:IBUF +select -assert-count 1 t:OBUF + +select -assert-none t:DFFC t:IBUF t:OBUF %% t:* %D + + +design -load read +hierarchy -top adffn +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 adffn # Constrain all select calls below inside the top module +select -assert-count 1 t:DFFC +select -assert-count 1 t:LUT1 +select -assert-count 3 t:IBUF +select -assert-count 1 t:OBUF + +select -assert-none t:DFFC t:IBUF t:OBUF t:LUT1 %% t:* %D + + +design -load read +hierarchy -top dffs +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:DFF +select -assert-count 1 t:LUT2 +select -assert-count 4 t:IBUF +select -assert-count 1 t:OBUF + +select -assert-none t:DFF t:LUT2 t:IBUF t:OBUF %% t:* %D + + +design -load read +hierarchy -top ndffnr +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 ndffnr # Constrain all select calls below inside the top module +select -assert-count 1 t:DFFNR +select -assert-count 1 t:LUT1 +select -assert-count 4 t:IBUF +select -assert-count 1 t:OBUF + +select -assert-none t:DFFNR t:IBUF t:OBUF t:LUT1 %% t:* %D diff --git a/tests/arch/gowin/counter.ys b/tests/arch/gowin/counter.ys new file mode 100644 index 000000000..920479d44 --- /dev/null +++ b/tests/arch/gowin/counter.ys @@ -0,0 +1,15 @@ +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -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 + +select -assert-count 8 t:DFFC +select -assert-count 8 t:ALU +select -assert-count 1 t:GND +select -assert-count 1 t:VCC +select -assert-count 2 t:IBUF +select -assert-count 8 t:OBUF +select -assert-none t:DFFC t:ALU t:GND t:VCC t:IBUF t:OBUF %% t:* %D diff --git a/tests/arch/gowin/dffs.ys b/tests/arch/gowin/dffs.ys new file mode 100644 index 000000000..9c012213f --- /dev/null +++ b/tests/arch/gowin/dffs.ys @@ -0,0 +1,25 @@ +read_verilog ../common/dffs.v +design -save read + +hierarchy -top dff +proc +equiv_opt -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 dff # Constrain all select calls below inside the top module +select -assert-count 1 t:DFF +select -assert-count 2 t:IBUF +select -assert-count 1 t:OBUF + +select -assert-none t:DFF t:IBUF t:OBUF %% t:* %D + +design -load read +hierarchy -top dffe +proc +equiv_opt -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 dffe # Constrain all select calls below inside the top module +select -assert-count 1 t:DFFE +select -assert-count 3 t:IBUF +select -assert-count 1 t:OBUF + +select -assert-none t:DFFE t:IBUF t:OBUF %% t:* %D diff --git a/tests/arch/gowin/fsm.ys b/tests/arch/gowin/fsm.ys new file mode 100644 index 000000000..ce4504522 --- /dev/null +++ b/tests/arch/gowin/fsm.ys @@ -0,0 +1,11 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten + +equiv_opt -run :prove -map +/gowin/cells_sim.v synth_gowin # equivalency check +miter -equiv -make_assert -flatten gold gate miter +sat -verify -show-all -dump_vcd x.vcd -prove-asserts -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter + +#design -load postopt +#shell 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/logic.ys b/tests/arch/gowin/logic.ys new file mode 100644 index 000000000..d2b9e4540 --- /dev/null +++ b/tests/arch/gowin/logic.ys @@ -0,0 +1,13 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -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 top # Constrain all select calls below inside the top module + +select -assert-count 1 t:LUT1 +select -assert-count 6 t:LUT2 +select -assert-count 2 t:LUT4 +select -assert-count 8 t:IBUF +select -assert-count 10 t:OBUF +select -assert-none t:LUT1 t:LUT2 t:LUT4 t:IBUF t:OBUF %% t:* %D diff --git a/tests/arch/gowin/memory.ys b/tests/arch/gowin/memory.ys new file mode 100644 index 000000000..8f88cdd7c --- /dev/null +++ b/tests/arch/gowin/memory.ys @@ -0,0 +1,18 @@ +read_verilog ../common/memory.v +hierarchy -top top +proc +memory -nomap +equiv_opt -run :prove -map +/gowin/cells_sim.v synth_gowin +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +#ERROR: Called with -verify and proof did fail! +#sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter +sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd top +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/gowin/mux.ys b/tests/arch/gowin/mux.ys new file mode 100644 index 000000000..afad29a89 --- /dev/null +++ b/tests/arch/gowin/mux.ys @@ -0,0 +1,49 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -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 mux2 # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT3 +select -assert-count 3 t:IBUF +select -assert-count 1 t:OBUF + +select -assert-none t:LUT3 t:IBUF t:OBUF %% t:* %D + +design -load read +hierarchy -top mux4 +proc +equiv_opt -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 mux4 # Constrain all select calls below inside the top module +select -assert-count 4 t:LUT4 +select -assert-count 2 t:MUX2_LUT5 +select -assert-count 1 t:MUX2_LUT6 +select -assert-count 6 t:IBUF +select -assert-count 1 t:OBUF + +select -assert-none t:LUT4 t:MUX2_LUT6 t:MUX2_LUT5 t:IBUF t:OBUF %% t:* %D + +design -load read +hierarchy -top mux8 +proc +equiv_opt -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 mux8 # Constrain all select calls below inside the top module +select -assert-count 11 t:IBUF +select -assert-count 1 t:OBUF + +select -assert-none t:LUT4 t:MUX2_LUT6 t:MUX2_LUT5 t:IBUF t:OBUF %% t:* %D + +design -load read +hierarchy -top mux16 +proc +equiv_opt -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 mux16 # Constrain all select calls below inside the top module +select -assert-count 20 t:IBUF +select -assert-count 1 t:OBUF + +select -assert-none t:LUT4 t:MUX2_LUT6 t:MUX2_LUT5 t:MUX2_LUT6 t:MUX2_LUT7 t:MUX2_LUT8 t:IBUF t:OBUF %% t:* %D diff --git a/tests/arch/gowin/run-test.sh b/tests/arch/gowin/run-test.sh new file mode 100755 index 000000000..bf19b887d --- /dev/null +++ b/tests/arch/gowin/run-test.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +set -e +{ +echo "all::" +for x in *.ys; do + echo "all:: run-$x" + echo "run-$x:" + echo " @echo 'Running $x..'" + echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" +done +for s in *.sh; do + if [ "$s" != "run-test.sh" ]; then + echo "all:: run-$s" + echo "run-$s:" + echo " @echo 'Running $s..'" + echo " @bash $s" + fi +done +} > run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/arch/gowin/shifter.ys b/tests/arch/gowin/shifter.ys new file mode 100644 index 000000000..b43b1e869 --- /dev/null +++ b/tests/arch/gowin/shifter.ys @@ -0,0 +1,12 @@ +read_verilog ../common/shifter.v +hierarchy -top top +proc +flatten +equiv_opt -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 top # Constrain all select calls below inside the top module + +select -assert-count 8 t:DFF +select -assert-count 2 t:IBUF +select -assert-count 8 t:OBUF +select -assert-none t:DFF t:IBUF t:OBUF %% t:* %D diff --git a/tests/arch/gowin/tribuf.ys b/tests/arch/gowin/tribuf.ys new file mode 100644 index 000000000..5855b9d97 --- /dev/null +++ b/tests/arch/gowin/tribuf.ys @@ -0,0 +1,13 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/gowin/cells_sim.v -map +/simcells.v synth_gowin # 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 +#Internal cell type used. Need support it. +select -assert-count 1 t:TBUF +select -assert-count 2 t:IBUF +select -assert-none t:TBUF t:IBUF %% t:* %D diff --git a/tests/arch/ice40/fsm.ys b/tests/arch/ice40/fsm.ys index 5aacc6c73..223ba070e 100644 --- a/tests/arch/ice40/fsm.ys +++ b/tests/arch/ice40/fsm.ys @@ -2,12 +2,15 @@ read_verilog ../common/fsm.v hierarchy -top fsm proc flatten -equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check + +equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40 +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 +select -assert-count 4 t:SB_DFF select -assert-count 2 t:SB_DFFESR -select -assert-count 2 t:SB_DFFSR -select -assert-count 1 t:SB_DFFSS -select -assert-count 13 t:SB_LUT4 -select -assert-none t:SB_DFFESR t:SB_DFFSR t:SB_DFFSS t:SB_LUT4 %% t:* %D +select -assert-count 15 t:SB_LUT4 +select -assert-none t:SB_DFFESR t:SB_DFF t:SB_LUT4 %% t:* %D diff --git a/tests/arch/ice40/ice40_opt.ys b/tests/arch/ice40/ice40_opt.ys index b17c69c91..5186d4800 100644 --- a/tests/arch/ice40/ice40_opt.ys +++ b/tests/arch/ice40/ice40_opt.ys @@ -1,4 +1,24 @@ read_verilog -icells -formal <<EOT +module \$__ICE40_CARRY_WRAPPER (output CO, O, input A, B, CI, I0, I3); + parameter LUT = 0; + SB_CARRY carry ( + .I0(A), + .I1(B), + .CI(CI), + .CO(CO) + ); + \$lut #( + .WIDTH(4), + .LUT(LUT) + ) lut ( + .A({I0,A,B,I3}), + .Y(O) + ); +endmodule +EOT +design -stash unmap + +read_verilog -icells -formal <<EOT module top(input CI, I0, output [1:0] CO, output O); wire A = 1'b0, B = 1'b0; \$__ICE40_CARRY_WRAPPER #( @@ -20,7 +40,68 @@ 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 %unmap -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 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/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/adffs.ys b/tests/arch/xilinx/adffs.ys index 12c34415e..e73bfe0b9 100644 --- a/tests/arch/xilinx/adffs.ys +++ b/tests/arch/xilinx/adffs.ys @@ -20,9 +20,9 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p 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 diff --git a/tests/arch/xilinx/blockram_params.ys b/tests/arch/xilinx/blockram_params.ys new file mode 100644 index 000000000..27a94834e --- /dev/null +++ b/tests/arch/xilinx/blockram_params.ys @@ -0,0 +1,47 @@ +## 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_params.v +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 1 sync_ram_sdp +synth_xilinx -top sync_ram_sdp +cd sync_ram_sdp +select -assert-count 1 t:RAMB18E1 + +design -reset +read_verilog ../common/blockram_params.v +chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 18 sync_ram_sdp +synth_xilinx -top sync_ram_sdp +cd sync_ram_sdp +select -assert-count 1 t:RAMB18E1 + +design -reset +read_verilog ../common/blockram_params.v +chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp +synth_xilinx -top sync_ram_sdp +cd sync_ram_sdp +select -assert-count 1 t:RAMB18E1 + +design -reset +read_verilog ../common/blockram_params.v +chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp +synth_xilinx -top sync_ram_sdp +cd sync_ram_sdp +select -assert-count 1 t:RAMB18E1 + +# Anything memory bits < 1024 -> LUTRAM +design -reset +read_verilog ../common/blockram_params.v +chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 2 sync_ram_sdp +synth_xilinx -top sync_ram_sdp +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_params.v +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 36 sync_ram_sdp +synth_xilinx -top sync_ram_sdp +cd sync_ram_sdp +select -assert-count 1 t:RAMB36E1 + diff --git a/tests/arch/xilinx/counter.ys b/tests/arch/xilinx/counter.ys index 57b645d19..604acdbfc 100644 --- a/tests/arch/xilinx/counter.ys +++ b/tests/arch/xilinx/counter.ys @@ -8,7 +8,7 @@ cd top # Constrain all select calls below inside the top module select -assert-count 1 t:BUFG select -assert-count 8 t:FDCE -select -assert-count 1 t:LUT1 +select -assert-count 1 t:INV 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-none t:BUFG t:FDCE t:INV t:MUXCY t:XORCY %% t:* %D diff --git a/tests/arch/xilinx/dsp_fastfir.ys b/tests/arch/xilinx/dsp_fastfir.ys new file mode 100644 index 000000000..0067a822b --- /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 +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 d2b481421..2a72c34e8 100644 --- a/tests/arch/xilinx/fsm.ys +++ b/tests/arch/xilinx/fsm.ys @@ -2,7 +2,11 @@ read_verilog ../common/fsm.v hierarchy -top fsm proc flatten -equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check + +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +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 diff --git a/tests/arch/xilinx/latches.ys b/tests/arch/xilinx/latches.ys index fe7887e8d..c87a8e38b 100644 --- a/tests/arch/xilinx/latches.ys +++ b/tests/arch/xilinx/latches.ys @@ -18,9 +18,9 @@ equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalen 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 diff --git a/tests/arch/xilinx/logic.ys b/tests/arch/xilinx/logic.ys index c0f6da302..d5b5c1a37 100644 --- a/tests/arch/xilinx/logic.ys +++ b/tests/arch/xilinx/logic.ys @@ -5,7 +5,7 @@ equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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/macc.sh b/tests/arch/xilinx/macc.sh index 2272679ee..154a29848 100644 --- a/tests/arch/xilinx/macc.sh +++ b/tests/arch/xilinx/macc.sh @@ -1,3 +1,3 @@ -../../../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 |