diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/opt/bug2318.ys | 12 | ||||
| -rw-r--r-- | tests/opt/opt_dff_dffmux.ys | 129 | ||||
| -rw-r--r-- | tests/opt/opt_share_bug2334.ys | 13 | ||||
| -rw-r--r-- | tests/opt/opt_share_bug2335.ys | 27 | ||||
| -rw-r--r-- | tests/opt/opt_share_bug2336.ys | 14 | ||||
| -rw-r--r-- | tests/svtypes/struct_array.sv | 22 | ||||
| -rw-r--r-- | tests/techmap/bug2321.ys | 15 | ||||
| -rw-r--r-- | tests/techmap/bug2332.ys | 11 | ||||
| -rw-r--r-- | tests/techmap/dff2dffs.ys | 50 | ||||
| -rw-r--r-- | tests/various/peepopt.ys | 143 |
10 files changed, 242 insertions, 194 deletions
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/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/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/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 |