diff options
Diffstat (limited to 'tests')
31 files changed, 539 insertions, 250 deletions
diff --git a/tests/aiger/.gitignore b/tests/aiger/.gitignore index b76bdb653..54b4a279b 100644 --- a/tests/aiger/.gitignore +++ b/tests/aiger/.gitignore @@ -1,3 +1,3 @@ /*_ref.v -/*.aag.log -/*.aig.log +/*.log +/neg.out/ diff --git a/tests/arch/anlogic/dffs.ys b/tests/arch/anlogic/dffs.ys index d3281ab89..deb90e051 100644 --- a/tests/arch/anlogic/dffs.ys +++ b/tests/arch/anlogic/dffs.ys @@ -15,6 +15,5 @@ proc equiv_opt -assert -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 dffe # Constrain all select calls below inside the top module -select -assert-count 1 t:AL_MAP_LUT3 select -assert-count 1 t:AL_MAP_SEQ -select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D +select -assert-none t:AL_MAP_SEQ %% t:* %D diff --git a/tests/arch/common/mul.v b/tests/arch/common/mul.v index 437a91cfc..baed64fcd 100644 --- a/tests/arch/common/mul.v +++ b/tests/arch/common/mul.v @@ -1,9 +1,10 @@ module top +#(parameter X_WIDTH=6, Y_WIDTH=6, A_WIDTH=12) ( - input [5:0] x, - input [5:0] y, + input [X_WIDTH-1:0] x, + input [Y_WIDTH-1:0] y, - output [11:0] A, + output [A_WIDTH-1:0] A, ); assign A = x * y; endmodule diff --git a/tests/arch/ecp5/fsm.ys b/tests/arch/ecp5/fsm.ys index ba91e5fc0..a77986bbc 100644 --- a/tests/arch/ecp5/fsm.ys +++ b/tests/arch/ecp5/fsm.ys @@ -10,8 +10,8 @@ sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 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 15 t:LUT4 -select -assert-count 6 t:PFUMX +select -assert-max 1 t:L6MUX21 +select -assert-max 16 t:LUT4 +select -assert-max 7 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/adffs.ys b/tests/arch/efinix/adffs.ys index 49dc7f256..86d446439 100644 --- a/tests/arch/efinix/adffs.ys +++ b/tests/arch/efinix/adffs.ys @@ -32,9 +32,8 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p cd dffs # Constrain all select calls below inside the top module select -assert-count 1 t:EFX_FF select -assert-count 1 t:EFX_GBUFCE -select -assert-count 1 t:EFX_LUT4 -select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D +select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D design -load read @@ -45,6 +44,5 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p cd ndffnr # Constrain all select calls below inside the top module select -assert-count 1 t:EFX_FF select -assert-count 1 t:EFX_GBUFCE -select -assert-count 1 t:EFX_LUT4 -select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D +select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D diff --git a/tests/arch/efinix/dffs.ys b/tests/arch/efinix/dffs.ys index af787ab67..f9111873c 100644 --- a/tests/arch/efinix/dffs.ys +++ b/tests/arch/efinix/dffs.ys @@ -19,6 +19,5 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p cd dffe # Constrain all select calls below inside the top module select -assert-count 1 t:EFX_FF select -assert-count 1 t:EFX_GBUFCE -select -assert-count 1 t:EFX_LUT4 -select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D +select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D diff --git a/tests/arch/gowin/init.ys b/tests/arch/gowin/init.ys index 88e88c15a..fba7c2fa5 100644 --- a/tests/arch/gowin/init.ys +++ b/tests/arch/gowin/init.ys @@ -45,24 +45,25 @@ flatten synth_gowin -run coarse: # check the flops mapped as expected -select -assert-count 1 t:DFF +select -assert-count 2 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 0 t:DFFE +select -assert-count 2 t:DFFN select -assert-count 1 t:DFFNC select -assert-count 1 t:DFFNCE -select -assert-count 1 t:DFFNE +select -assert-count 0 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 3 t:DFFNS +select -assert-count 1 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 +select -assert-count 3 t:DFFS +select -assert-count 1 t:DFFSE +select -assert-count 4 t:LUT2 +select -assert-count 4 t:LUT4 diff --git a/tests/arch/intel_alm/adffs.ys b/tests/arch/intel_alm/adffs.ys index 04fa2ad24..4565dcc64 100644 --- a/tests/arch/intel_alm/adffs.ys +++ b/tests/arch/intel_alm/adffs.ys @@ -77,10 +77,9 @@ equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm 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:MISTRAL_FF -select -assert-count 1 t:MISTRAL_NOT -select -assert-count 1 t:MISTRAL_ALUT2 +select -assert-count 2 t:MISTRAL_NOT -select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 %% t:* %D +select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D design -load read @@ -90,7 +89,6 @@ equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm 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:MISTRAL_FF -select -assert-count 1 t:MISTRAL_NOT -select -assert-count 1 t:MISTRAL_ALUT2 +select -assert-count 2 t:MISTRAL_NOT -select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 %% t:* %D +select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D diff --git a/tests/arch/intel_alm/fsm.ys b/tests/arch/intel_alm/fsm.ys index 6491b2e08..e54b5c21e 100644 --- a/tests/arch/intel_alm/fsm.ys +++ b/tests/arch/intel_alm/fsm.ys @@ -12,12 +12,13 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p cd fsm # Constrain all select calls below inside the top module select -assert-count 6 t:MISTRAL_FF +select -assert-max 1 t:MISTRAL_NOT select -assert-max 2 t:MISTRAL_ALUT2 # Clang returns 2, GCC returns 1 -select -assert-count 1 t:MISTRAL_ALUT3 -select -assert-max 1 t:MISTRAL_ALUT4 # Clang returns 0, GCC returns 1 +select -assert-max 1 t:MISTRAL_ALUT3 +select -assert-max 2 t:MISTRAL_ALUT4 # Clang returns 0, GCC returns 1 select -assert-max 6 t:MISTRAL_ALUT5 # Clang returns 5, GCC returns 4 select -assert-max 2 t:MISTRAL_ALUT6 # Clang returns 1, GCC returns 2 -select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D +select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D design -reset read_verilog ../common/fsm.v @@ -34,9 +35,10 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p cd fsm # Constrain all select calls below inside the top module select -assert-count 6 t:MISTRAL_FF +select -assert-max 1 t:MISTRAL_NOT select -assert-max 2 t:MISTRAL_ALUT2 # Clang returns 2, GCC returns 1 select -assert-max 2 t:MISTRAL_ALUT3 # Clang returns 2, GCC returns 1 -select -assert-max 1 t:MISTRAL_ALUT4 # Clang returns 0, GCC returns 1 +select -assert-max 2 t:MISTRAL_ALUT4 # Clang returns 0, GCC returns 1 select -assert-max 6 t:MISTRAL_ALUT5 # Clang returns 5, GCC returns 4 select -assert-max 2 t:MISTRAL_ALUT6 # Clang returns 1, GCC returns 2 -select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D +select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D diff --git a/tests/arch/intel_alm/mul.ys b/tests/arch/intel_alm/mul.ys index 92f00156a..49934740f 100644 --- a/tests/arch/intel_alm/mul.ys +++ b/tests/arch/intel_alm/mul.ys @@ -1,23 +1,60 @@ read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 hierarchy -top top proc equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev # 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:MISTRAL_MUL9X9 select -assert-none t:MISTRAL_MUL9X9 %% t:* %D +# Cyclone 10 GX does not have 9x9 multipliers. + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 17 -set Y_WIDTH 17 -set A_WIDTH 34 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev # 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:MISTRAL_MUL18X18 +select -assert-none t:MISTRAL_MUL18X18 %% t:* %D + design -reset read_verilog ../common/mul.v +chparam -set X_WIDTH 17 -set Y_WIDTH 17 -set A_WIDTH 34 hierarchy -top top proc equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclone10gx # 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 -# Cyclone 10 GX does not have 9x9 multipliers, so we use 18x18. select -assert-count 1 t:MISTRAL_MUL18X18 select -assert-none t:MISTRAL_MUL18X18 %% t:* %D + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 26 -set Y_WIDTH 26 -set A_WIDTH 52 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev # 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:MISTRAL_MUL27X27 +select -assert-none t:MISTRAL_MUL27X27 %% t:* %D + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 26 -set Y_WIDTH 26 -set A_WIDTH 52 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclone10gx # 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:MISTRAL_MUL27X27 +select -assert-none t:MISTRAL_MUL27X27 %% t:* %D diff --git a/tests/arch/intel_alm/mux.ys b/tests/arch/intel_alm/mux.ys index 01cc78e1b..ac3b9b08f 100644 --- a/tests/arch/intel_alm/mux.ys +++ b/tests/arch/intel_alm/mux.ys @@ -70,8 +70,9 @@ equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cycl 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 1 t:MISTRAL_ALUT3 -select -assert-count 5 t:MISTRAL_ALUT6 -select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT6 %% t:* %D +select -assert-max 2 t:MISTRAL_ALUT5 +select -assert-max 5 t:MISTRAL_ALUT6 +select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D design -load read diff --git a/tests/opt/bug2318.ys b/tests/opt/bug2318.ys new file mode 100644 index 000000000..9de6f88ec --- /dev/null +++ b/tests/opt/bug2318.ys @@ -0,0 +1,12 @@ +read_verilog <<EOT +module t(input [3:0] A, input [3:0] B, output signed [3:0] Y); + +wire [7:0] P = A * B; +wire signed [7:0] SP = P; +wire signed [3:0] SB = B; +assign Y = SP / SB; + +endmodule +EOT + +equiv_opt -assert peepopt diff --git a/tests/opt/opt_dff_dffmux.ys b/tests/opt/opt_dff_dffmux.ys new file mode 100644 index 000000000..43190cc31 --- /dev/null +++ b/tests/opt/opt_dff_dffmux.ys @@ -0,0 +1,129 @@ +design -reset +read_verilog <<EOT +module opt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o); + always @(posedge clk) if (ce) o <= i; +endmodule +EOT + +proc +equiv_opt -assert opt +design -load postopt +select -assert-count 1 t:$dffe r:WIDTH=2 %i +select -assert-count 0 t:$dffe %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module opt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o); + always @(posedge clk) if (ce) o <= i; +endmodule +EOT + +proc +equiv_opt -assert opt +design -load postopt +wreduce +select -assert-count 1 t:$dffe r:WIDTH=2 %i +select -assert-count 0 t:$dffe %% t:* %D + +################### + +design -reset +read_verilog <<EOT +module opt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o); + always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; +endmodule +EOT + +proc +equiv_opt -assert opt +design -load postopt +select -assert-count 1 t:$dffe r:WIDTH=2 %i +select -assert-count 0 t:$dffe %% t:* %D + +################### + +design -reset +read_verilog <<EOT +module opt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o); + always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; +endmodule +EOT + +proc +equiv_opt -assert opt +design -load postopt +select -assert-count 1 t:$dffe r:WIDTH=4 %i +select -assert-count 0 t:$dffe %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module opt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o); + always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i; +endmodule +EOT + +proc +equiv_opt -assert opt +design -load postopt +wreduce +select -assert-count 1 t:$sdffe r:WIDTH=2 %i +select -assert-count 0 t:$sdffe %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module opt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); + always @(posedge clk) begin + if (ce) o <= i; + if (!rstn) o <= 4'b1111; + end +endmodule +EOT + +proc +equiv_opt -assert opt +design -load postopt +wreduce +select -assert-count 1 t:$sdffe r:WIDTH=2 %i +select -assert-count 0 t:$sdffe %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module opt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); + initial o <= 4'b0010; + always @(posedge clk) begin + if (ce) o <= i; + if (!rstn) o <= 4'b1111; + end +endmodule +EOT + +proc +# NB: equiv_opt uses equiv_induct which covers +# only the induction half of temporal induction +# --- missing the base-case half +# This makes it akin to `sat -tempinduct-inductonly` +# instead of `sat -tempinduct-baseonly` or +# `sat -tempinduct` which is necessary for this +# testcase +#equiv_opt -assert opt + +design -save gold +opt +wreduce +design -stash gate +design -import gold -as gold +design -import gate -as gate +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -tempinduct -verify -prove-asserts -show-ports miter + +design -load gate +select -assert-count 1 t:$sdffe r:WIDTH=3 %i +select -assert-count 0 t:$sdffe %% t:* %D diff --git a/tests/opt/opt_share_bug2334.ys b/tests/opt/opt_share_bug2334.ys new file mode 100644 index 000000000..004d98349 --- /dev/null +++ b/tests/opt/opt_share_bug2334.ys @@ -0,0 +1,13 @@ +read_verilog <<EOT + +module t(input [3:0] A, input [3:0] B, input [3:0] C, input S, output [3:0] Y); + +wire [3:0] t = A + C; + +assign Y = S ? A + B : {4{t[0]}}; + +endmodule + +EOT + +equiv_opt -assert opt_share diff --git a/tests/opt/opt_share_bug2335.ys b/tests/opt/opt_share_bug2335.ys new file mode 100644 index 000000000..0846a9ec3 --- /dev/null +++ b/tests/opt/opt_share_bug2335.ys @@ -0,0 +1,27 @@ +read_verilog <<EOT + +module top(...); + +input [3:0] A, B, C; +input S; +input [1:0] T; +output [3:0] X; +output reg [3:0] Y; + +wire [3:0] D = A + B; + +assign X = S ? D : A + C; +always @* begin + case(T) + 2'b01: Y <= A; + 2'b10: Y <= B; + default: Y <= D; + endcase +end + +endmodule + +EOT + +proc +equiv_opt -assert opt_share diff --git a/tests/opt/opt_share_bug2336.ys b/tests/opt/opt_share_bug2336.ys new file mode 100644 index 000000000..cd472ef46 --- /dev/null +++ b/tests/opt/opt_share_bug2336.ys @@ -0,0 +1,14 @@ +read_verilog <<EOT + +module top(input [3:0] A, B, C, input S, output [2:0] O); + +wire [3:0] tb = A + B; +wire [3:0] tc = A + C; + +assign O = S ? tb[3:1] : tc[3:1]; + +endmodule + +EOT + +equiv_opt -assert opt_share diff --git a/tests/simple/const_branch_finish.v b/tests/simple/const_branch_finish.v new file mode 100644 index 000000000..8166688e6 --- /dev/null +++ b/tests/simple/const_branch_finish.v @@ -0,0 +1,39 @@ +`define CONSTANT_CHECK \ + if (WIDTH === 'bx) begin \ + $display("FAIL"); \ + $finish; \ + end + +module top; + parameter WIDTH = 32; + integer j; + initial begin + `CONSTANT_CHECK + if (WIDTH == 32) begin : procedural_conditional_block + `CONSTANT_CHECK + end + case (WIDTH) + 32: `CONSTANT_CHECK + default: ; + endcase + for (j = 0; j < 2; j = j + 1) begin : procedural_loop_block + `CONSTANT_CHECK + end + end + generate + begin : unconditional_block + initial `CONSTANT_CHECK + end + if (WIDTH == 32) begin : conditional_block + initial `CONSTANT_CHECK + end + case (WIDTH) + 32: initial `CONSTANT_CHECK + default: ; + endcase + genvar i; + for (i = 0; i < 2; i = i + 1) begin : loop_block + initial `CONSTANT_CHECK + end + endgenerate +endmodule diff --git a/tests/simple/generate.v b/tests/simple/generate.v index 0e353ad9b..12327b36e 100644 --- a/tests/simple/generate.v +++ b/tests/simple/generate.v @@ -159,3 +159,104 @@ generate end endgenerate endmodule + +// ------------------------------------------ + +module gen_test7; + reg [2:0] out1; + reg [2:0] out2; + wire [2:0] out3; + generate + begin : cond + reg [2:0] sub_out1; + reg [2:0] sub_out2; + wire [2:0] sub_out3; + initial begin : init + reg signed [31:0] x; + x = 2 ** 2; + out1 = x; + sub_out1 = x; + end + always @* begin : proc + reg signed [31:0] x; + x = 2 ** 1; + out2 = x; + sub_out2 = x; + end + genvar x; + for (x = 0; x < 3; x = x + 1) begin + assign out3[x] = 1; + assign sub_out3[x] = 1; + end + end + endgenerate + +// `define VERIFY +`ifdef VERIFY + assert property (out1 == 4); + assert property (out2 == 2); + assert property (out3 == 7); + assert property (cond.sub_out1 == 4); + assert property (cond.sub_out2 == 2); + assert property (cond.sub_out3 == 7); +`endif +endmodule + +// ------------------------------------------ + +module gen_test8; + +// `define VERIFY +`ifdef VERIFY + `define ASSERT(expr) assert property (expr); +`else + `define ASSERT(expr) +`endif + + wire [1:0] x = 2'b11; + generate + begin : A + wire [1:0] x; + begin : B + wire [1:0] x = 2'b00; + `ASSERT(x == 0) + `ASSERT(A.x == 2) + `ASSERT(A.C.x == 1) + `ASSERT(A.B.x == 0) + `ASSERT(gen_test8.x == 3) + `ASSERT(gen_test8.A.x == 2) + `ASSERT(gen_test8.A.C.x == 1) + `ASSERT(gen_test8.A.B.x == 0) + end + begin : C + wire [1:0] x = 2'b01; + `ASSERT(x == 1) + `ASSERT(A.x == 2) + `ASSERT(A.C.x == 1) + `ASSERT(A.B.x == 0) + `ASSERT(gen_test8.x == 3) + `ASSERT(gen_test8.A.x == 2) + `ASSERT(gen_test8.A.C.x == 1) + `ASSERT(gen_test8.A.B.x == 0) + end + assign x = B.x ^ 2'b11 ^ C.x; + `ASSERT(x == 2) + `ASSERT(A.x == 2) + `ASSERT(A.C.x == 1) + `ASSERT(A.B.x == 0) + `ASSERT(gen_test8.x == 3) + `ASSERT(gen_test8.A.x == 2) + `ASSERT(gen_test8.A.C.x == 1) + `ASSERT(gen_test8.A.B.x == 0) + end + endgenerate + + `ASSERT(x == 3) + `ASSERT(A.x == 2) + `ASSERT(A.C.x == 1) + `ASSERT(A.B.x == 0) + `ASSERT(gen_test8.x == 3) + `ASSERT(gen_test8.A.x == 2) + `ASSERT(gen_test8.A.C.x == 1) + `ASSERT(gen_test8.A.B.x == 0) +endmodule diff --git a/tests/simple/string_format.v b/tests/simple/string_format.v new file mode 100644 index 000000000..ce45ca1e9 --- /dev/null +++ b/tests/simple/string_format.v @@ -0,0 +1,7 @@ +module top; + parameter STR = "something interesting"; + initial begin + $display("A: %s", STR); + $display("B: %0s", STR); + end +endmodule diff --git a/tests/svtypes/struct_array.sv b/tests/svtypes/struct_array.sv index 022ad56c6..873f7befd 100644 --- a/tests/svtypes/struct_array.sv +++ b/tests/svtypes/struct_array.sv @@ -1,7 +1,7 @@ // test for array indexing in structures module top; - + struct packed { bit [5:0] [7:0] a; // 6 element packed array of bytes bit [15:0] b; // filler for non-zero offset @@ -19,4 +19,24 @@ module top; always_comb assert(s==64'h4200_0012_3400_FFFC); + struct packed { + bit [7:0] [7:0] a; // 8 element packed array of bytes + bit [15:0] b; // filler for non-zero offset + } s2; + + initial begin + s2 = '0; + + s2.a[2:1] = 16'h1234; + s2.a[5] = 8'h42; + + s2.a[7] = '1; + s2.a[7][1:0] = '0; + + s2.b = '1; + s2.b[1:0] = '0; + end + + always_comb assert(s2==80'hFC00_4200_0012_3400_FFFC); + endmodule diff --git a/tests/techmap/bug2183.ys b/tests/techmap/bug2183.ys new file mode 100644 index 000000000..8dd09458e --- /dev/null +++ b/tests/techmap/bug2183.ys @@ -0,0 +1,11 @@ +read_verilog <<EOT +module foo(inout a, b); + assign a = b; +endmodule +module bar(output c); + foo f(c, 1'b0); +endmodule +EOT + +hierarchy -auto-top +flatten diff --git a/tests/techmap/bug2321.ys b/tests/techmap/bug2321.ys new file mode 100644 index 000000000..637528b21 --- /dev/null +++ b/tests/techmap/bug2321.ys @@ -0,0 +1,15 @@ +read_verilog <<EOT +module m (input i, output o); +wire [1023:0] _TECHMAP_DO_00_ = "CONSTMAP; "; +endmodule +EOT + +design -stash map + +read_verilog <<EOT +module top(output o); +m m (.o(o), .i(o)); +endmodule +EOT + +techmap -map %map diff --git a/tests/techmap/bug2332.ys b/tests/techmap/bug2332.ys new file mode 100644 index 000000000..ed6b35eb2 --- /dev/null +++ b/tests/techmap/bug2332.ys @@ -0,0 +1,11 @@ +read_verilog <<EOT +module top(input [31:0] a, input signed [2:0] x, output [2:0] o); + +wire [5:0] t = x * 3; +assign o = a >> t; + +endmodule +EOT + +wreduce +equiv_opt -assert peepopt diff --git a/tests/techmap/dff2dffs.ys b/tests/techmap/dff2dffs.ys deleted file mode 100644 index 105a89400..000000000 --- a/tests/techmap/dff2dffs.ys +++ /dev/null @@ -1,50 +0,0 @@ -read_verilog << EOT -module top(...); -input clk; -input d; -input sr; -output reg q0, q1, q2, q3, q4, q5; - -initial q0 = 1'b0; -initial q1 = 1'b0; -initial q2 = 1'b1; -initial q3 = 1'b1; -initial q4 = 1'bx; -initial q5 = 1'bx; - -always @(posedge clk) begin - q0 <= sr ? 1'b0 : d; - q1 <= sr ? 1'b1 : d; - q2 <= sr ? 1'b0 : d; - q3 <= sr ? 1'b1 : d; - q4 <= sr ? 1'b0 : d; - q5 <= sr ? 1'b1 : d; -end - -endmodule -EOT - -proc -simplemap -design -save ref - -dff2dffs -clean - -select -assert-count 1 w:q0 %x t:$_SDFF_PP0_ %i -select -assert-count 1 w:q1 %x t:$_SDFF_PP1_ %i -select -assert-count 1 w:q2 %x t:$_SDFF_PP0_ %i -select -assert-count 1 w:q3 %x t:$_SDFF_PP1_ %i -select -assert-count 1 w:q4 %x t:$_SDFF_PP0_ %i -select -assert-count 1 w:q5 %x t:$_SDFF_PP1_ %i - -design -load ref -dff2dffs -match-init -clean - -select -assert-count 1 w:q0 %x t:$_SDFF_PP0_ %i -select -assert-count 0 w:q1 %x t:$_SDFF_PP1_ %i -select -assert-count 0 w:q2 %x t:$_SDFF_PP0_ %i -select -assert-count 1 w:q3 %x t:$_SDFF_PP1_ %i -select -assert-count 1 w:q4 %x t:$_SDFF_PP0_ %i -select -assert-count 1 w:q5 %x t:$_SDFF_PP1_ %i diff --git a/tests/techmap/shiftx2mux.ys b/tests/techmap/shiftx2mux.ys index eb29680f6..f749e79b2 100644 --- a/tests/techmap/shiftx2mux.ys +++ b/tests/techmap/shiftx2mux.ys @@ -74,12 +74,6 @@ design -save gold design -load gold -techmap -D NO_LSB_FIRST_SHIFT_SHIFTX -abc -lut 6 -select -assert-min 17 t:$lut - - -design -load gold techmap abc -lut 6 select -assert-count 16 t:$lut @@ -92,12 +86,6 @@ sat -verify -prove-asserts -show-ports miter design -load gold -techmap -D NO_LSB_FIRST_SHIFT_SHIFTX -abc9 -lut 6 -select -assert-min 17 t:$lut - - -design -load gold techmap abc9 -lut 6 select -assert-count 16 t:$lut diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh index 4d3478628..72a3d51eb 100755 --- a/tests/tools/autotest.sh +++ b/tests/tools/autotest.sh @@ -193,13 +193,13 @@ do elif [ "$frontend" = "verific_gates" ]; then test_passes -p "verific -vlog2k ${bn}_ref.${refext}; verific -import -gates -all; opt; memory;;" else - test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.${refext} + test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt -nodffe -nosdff; fsm; opt; memory; opt -full -fine" ${bn}_ref.${refext} test_passes -f "$frontend $include_opts" -p "hierarchy; synth -run coarse; techmap; opt; abc -dff" ${bn}_ref.${refext} if [ -n "$firrtl2verilog" ]; then if test -z "$xfirrtl" || ! grep "$fn" "$xfirrtl" ; then - "$toolsdir"/../../yosys -b "firrtl" -o ${bn}_ref.fir -f "$frontend $include_opts" -p "prep -nordff; proc; opt; memory; opt; fsm; opt -full -fine; pmuxtree" ${bn}_ref.${refext} + "$toolsdir"/../../yosys -b "firrtl" -o ${bn}_ref.fir -f "$frontend $include_opts" -p "prep -nordff; proc; opt -nodffe -nosdff; fsm; opt; memory; opt -full -fine; pmuxtree" ${bn}_ref.${refext} $firrtl2verilog -i ${bn}_ref.fir -o ${bn}_ref.fir.v - test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.fir.v + test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt -nodffe -nosdff; fsm; opt; memory; opt -full -fine" ${bn}_ref.fir.v fi fi fi diff --git a/tests/various/const_arg_loop.v b/tests/various/const_arg_loop.v index 85318562f..3bfff4acd 100644 --- a/tests/various/const_arg_loop.v +++ b/tests/various/const_arg_loop.v @@ -23,6 +23,22 @@ module top; end endfunction + function automatic [31:0] operation3; + input [4:0] rounds; + input integer num; + reg [4:0] rounds; + integer i; + begin + begin : shadow + integer rounds; + rounds = 0; + end + for (i = 0; i < rounds; i = i + 1) + num = num * 2; + operation3 = num; + end + endfunction + wire [31:0] a; assign a = 2; @@ -34,11 +50,15 @@ module top; wire [31:0] x2; assign x2 = operation2(A, a); + wire [31:0] x3; + assign x3 = operation3(A, a); + // `define VERIFY `ifdef VERIFY assert property (a == 2); assert property (A == 3); assert property (x1 == 16); assert property (x2 == 4); + assert property (x3 == 16); `endif endmodule diff --git a/tests/various/const_func.v b/tests/various/const_func.v index 76cdc385d..541e63b19 100644 --- a/tests/various/const_func.v +++ b/tests/various/const_func.v @@ -53,6 +53,15 @@ module top(out); c1, c2, c3, c4, d1, d2, d3, d4}; + function signed [31:0] negate; + input integer inp; + negate = ~inp; + endfunction + parameter W = 10; + parameter X = 3; + localparam signed Y = $floor(W / X); + localparam signed Z = negate($floor(W / X)); + // `define VERIFY `ifdef VERIFY assert property (a1 == 0); @@ -71,5 +80,8 @@ module top(out); assert property (d2 == 0); assert property (d3 == 1); assert property (d4 == 1); + + assert property (Y == 3); + assert property (Z == ~3); `endif endmodule diff --git a/tests/various/const_func_block_var.v b/tests/various/const_func_block_var.v new file mode 100644 index 000000000..cb60844ab --- /dev/null +++ b/tests/various/const_func_block_var.v @@ -0,0 +1,26 @@ +module top(out); + function integer operation; + input integer num; + localparam incr = 1; + localparam mult = 1; + begin + operation = 0; + begin : op_i + integer i; + for (i = 0; i * mult < 2; i = i + incr) + begin : op_j + integer j; + localparam other_mult = 2; + for (j = i; j < i * other_mult; j = j + incr) + num = num + incr; + end + num = num * 2; + end + operation = num; + end + endfunction + + localparam res = operation(4); + output wire [31:0] out; + assign out = res; +endmodule diff --git a/tests/various/const_func_block_var.ys b/tests/various/const_func_block_var.ys new file mode 100644 index 000000000..7c2e85c64 --- /dev/null +++ b/tests/various/const_func_block_var.ys @@ -0,0 +1 @@ +read_verilog const_func_block_var.v diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index ee5ad8a1a..45e936a21 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -68,146 +68,3 @@ equiv_opt -assert peepopt design -load postopt clean select -assert-count 0 t:* - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o); - always @(posedge clk) if (ce) o <= i; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -clean -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 1 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o); - always @(posedge clk) if (ce) o <= i; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -clean -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 1 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o); - always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 1 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o); - always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -select -assert-count 1 t:$dff r:WIDTH=4 %i -select -assert-count 1 t:$mux r:WIDTH=4 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o); - always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -wreduce -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 2 t:$mux -select -assert-count 2 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); - always @(posedge clk) begin - if (ce) o <= i; - if (!rstn) o <= 4'b1111; - end -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -wreduce -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 2 t:$mux -select -assert-count 2 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); - initial o <= 4'b0010; - always @(posedge clk) begin - if (ce) o <= i; - if (!rstn) o <= 4'b1111; - end -endmodule -EOT - -proc -# NB: equiv_opt uses equiv_induct which covers -# only the induction half of temporal induction -# --- missing the base-case half -# This makes it akin to `sat -tempinduct-inductonly` -# instead of `sat -tempinduct-baseonly` or -# `sat -tempinduct` which is necessary for this -# testcase -#equiv_opt -assert peepopt - -design -save gold -peepopt -wreduce -design -stash gate -design -import gold -as gold -design -import gate -as gate -miter -equiv -flatten -make_assert -make_outputs gold gate miter -sat -tempinduct -verify -prove-asserts -show-ports miter - -design -load gate -select -assert-count 1 t:$dff r:WIDTH=4 %i -select -assert-count 2 t:$mux -select -assert-count 2 t:$mux r:WIDTH=4 %i -select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D |