aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/opt/bug2318.ys12
-rw-r--r--tests/opt/opt_dff_dffmux.ys129
-rw-r--r--tests/simple/const_branch_finish.v39
-rw-r--r--tests/simple/generate.v85
-rw-r--r--tests/simple/string_format.v7
-rw-r--r--tests/svtypes/struct_array.sv22
-rw-r--r--tests/techmap/bug2321.ys15
-rw-r--r--tests/techmap/bug2332.ys11
-rw-r--r--tests/techmap/dff2dffs.ys50
-rw-r--r--tests/various/const_func.v12
-rw-r--r--tests/various/const_func_block_var.v23
-rw-r--r--tests/various/const_func_block_var.ys1
-rw-r--r--tests/various/peepopt.ys143
13 files changed, 355 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/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..dcd450e47 100644
--- a/tests/simple/generate.v
+++ b/tests/simple/generate.v
@@ -159,3 +159,88 @@ 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)
+ 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)
+ 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)
+ end
+ endgenerate
+
+ `ASSERT(x == 3)
+ `ASSERT(A.x == 2)
+ `ASSERT(A.C.x == 1)
+ `ASSERT(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/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/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..98e83aa5b
--- /dev/null
+++ b/tests/various/const_func_block_var.v
@@ -0,0 +1,23 @@
+module top(out);
+ function integer operation;
+ input integer num;
+ begin
+ operation = 0;
+ begin : op_i
+ integer i;
+ for (i = 0; i < 2; i = i + 1)
+ begin : op_j
+ integer j;
+ for (j = i; j < i * 2; j = j + 1)
+ num = num + 1;
+ 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
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-04 00:34:51 +0000