aboutsummaryrefslogtreecommitdiffstats
path: root/tests/various
diff options
context:
space:
mode:
Diffstat (limited to 'tests/various')
-rw-r--r--tests/various/.gitignore1
-rw-r--r--tests/various/const_arg_loop.sv (renamed from tests/various/const_arg_loop.v)27
-rw-r--r--tests/various/const_arg_loop.ys7
-rw-r--r--tests/various/const_func.sv (renamed from tests/various/const_func.v)41
-rw-r--r--tests/various/const_func.ys8
-rw-r--r--tests/various/countbits.sv69
-rw-r--r--tests/various/countbits.ys7
-rw-r--r--tests/various/fib_tern.v70
-rw-r--r--tests/various/fib_tern.ys6
-rw-r--r--tests/various/gen_if_null.v12
-rw-r--r--tests/various/gen_if_null.ys4
-rw-r--r--tests/various/port_sign_extend.v22
-rw-r--r--tests/various/port_sign_extend.ys13
-rw-r--r--tests/various/rand_const.sv8
-rw-r--r--tests/various/rand_const.ys1
15 files changed, 246 insertions, 50 deletions
diff --git a/tests/various/.gitignore b/tests/various/.gitignore
index 12d4e5048..2bb6c7179 100644
--- a/tests/various/.gitignore
+++ b/tests/various/.gitignore
@@ -4,3 +4,4 @@
/write_gzip.v.gz
/run-test.mk
/plugin.so
+/plugin.so.dSYM
diff --git a/tests/various/const_arg_loop.v b/tests/various/const_arg_loop.sv
index 358fb439a..f28d06e68 100644
--- a/tests/various/const_arg_loop.v
+++ b/tests/various/const_arg_loop.sv
@@ -20,11 +20,11 @@ module top;
endfunction
function automatic [31:0] operation2;
- input [4:0] var;
+ input [4:0] inp;
input integer num;
begin
- var[0] = var[0] ^ 1;
- operation2 = num * var;
+ inp[0] = inp[0] ^ 1;
+ operation2 = num * inp;
end
endfunction
@@ -79,15 +79,14 @@ module top;
wire [31:0] x5;
assign x5 = operation5(64);
-// `define VERIFY
-`ifdef VERIFY
- assert property (a == 2);
- assert property (A == 3);
- assert property (x1 == 16);
- assert property (x1b == 16);
- assert property (x2 == 4);
- assert property (x3 == 16);
- assert property (x4 == a << 1);
- assert property (x5 == 64);
-`endif
+ always_comb begin
+ assert(a == 2);
+ assert(A == 3);
+ assert(x1 == 16);
+ assert(x1b == 16);
+ assert(x2 == 4);
+ assert(x3 == 16);
+ assert(x4 == a << 1);
+ assert(x5 == 64);
+ end
endmodule
diff --git a/tests/various/const_arg_loop.ys b/tests/various/const_arg_loop.ys
index b039bda10..392532213 100644
--- a/tests/various/const_arg_loop.ys
+++ b/tests/various/const_arg_loop.ys
@@ -1 +1,6 @@
-read_verilog const_arg_loop.v
+read_verilog -sv const_arg_loop.sv
+hierarchy
+proc
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all
diff --git a/tests/various/const_func.v b/tests/various/const_func.sv
index 541e63b19..af65f5c73 100644
--- a/tests/various/const_func.v
+++ b/tests/various/const_func.sv
@@ -62,26 +62,25 @@ module top(out);
localparam signed Y = $floor(W / X);
localparam signed Z = negate($floor(W / X));
-// `define VERIFY
-`ifdef VERIFY
- assert property (a1 == 0);
- assert property (a2 == 0);
- assert property (a3 == "BAR");
- assert property (a4 == 0);
- assert property (b1 == "FOO");
- assert property (b2 == "FOO");
- assert property (b3 == 0);
- assert property (b4 == "HI");
- assert property (c1 == 1);
- assert property (c2 == 1);
- assert property (c3 == 0);
- assert property (c4 == 0);
- assert property (d1 == 0);
- assert property (d2 == 0);
- assert property (d3 == 1);
- assert property (d4 == 1);
+ always_comb begin
+ assert(a1 == 0);
+ assert(a2 == 0);
+ assert(a3 == "BAR");
+ assert(a4 == 0);
+ assert(b1 == "FOO");
+ assert(b2 == "FOO");
+ assert(b3 == 0);
+ assert(b4 == "HI");
+ assert(c1 == 1);
+ assert(c2 == 1);
+ assert(c3 == 0);
+ assert(c4 == 0);
+ assert(d1 == 0);
+ assert(d2 == 0);
+ assert(d3 == 1);
+ assert(d4 == 1);
- assert property (Y == 3);
- assert property (Z == ~3);
-`endif
+ assert(Y == 3);
+ assert(Z == ~3);
+ end
endmodule
diff --git a/tests/various/const_func.ys b/tests/various/const_func.ys
index 5e3c04105..2f60acfe6 100644
--- a/tests/various/const_func.ys
+++ b/tests/various/const_func.ys
@@ -1 +1,7 @@
-read_verilog const_func.v
+read_verilog -sv const_func.sv
+hierarchy
+proc
+flatten
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all
diff --git a/tests/various/countbits.sv b/tests/various/countbits.sv
new file mode 100644
index 000000000..5762217bb
--- /dev/null
+++ b/tests/various/countbits.sv
@@ -0,0 +1,69 @@
+module top;
+
+ assert property ($countbits(15'b011xxxxzzzzzzzz, '0 ) == 1);
+ assert property ($countbits(15'b011xxxxzzzzzzzz, '1 ) == 2);
+ assert property ($countbits(15'b011xxxxzzzzzzzz, 'x ) == 4);
+ assert property ($countbits(15'b011xxxxzzzzzzzz, 'z ) == 8);
+ assert property ($countbits(15'b011xxxxzzzzzzzz, '0, '1 ) == 3);
+ assert property ($countbits(15'b011xxxxzzzzzzzz, '1, '1, '0 ) == 3);
+ assert property ($countbits(15'b011xxxxzzzzzzzz, '0, 'x ) == 5);
+ assert property ($countbits(15'b011xxxxzzzzzzzz, '0, 'z ) == 9);
+ assert property ($countbits(15'bz1x10xzxzzxzzzz, '0, 'z ) == 9);
+ assert property ($countbits(15'b011xxxxzzzzzzzz, 'x, 'z ) == 12);
+ assert property ($countbits(15'b011xxxxzzzzzzzz, '1, 'z ) == 10);
+ assert property ($countbits(15'b011xxxxzzzzzzzz, '1, 'x, 'z ) == 14);
+ assert property ($countbits(15'b011xxxxzzzzzzzz, '1, 'x, 'z, '0) == 15);
+
+ assert property ($countbits(0, '0) == 32); // test integers
+ assert property ($countbits(0, '1) == 0);
+ assert property ($countbits(80'b0, '0) == 80); // test something bigger than integer
+ assert property ($countbits(80'bx0, 'x) == 79);
+
+ always_comb begin
+ logic one;
+ logic [1:0] two;
+ logic [3:0] four;
+
+ // Make sure that the width of the whole expression doesn't affect the width of the shift
+ // operations inside the function.
+ one = $countbits(3'b100, '1) & 1'b1;
+ two = $countbits(3'b111, '1) & 2'b11;
+ four = $countbits(3'b111, '1) & 4'b1111;
+
+ assert (one == 1);
+ assert (two == 3);
+ assert (four == 3);
+ end
+
+ assert property ($countones(8'h00) == 0);
+ assert property ($countones(8'hff) == 8);
+ assert property ($countones(8'ha5) == 4);
+ assert property ($countones(8'h13) == 3);
+
+ logic test1 = 1'b1;
+ logic [4:0] test5 = 5'b10101;
+
+ assert property ($countones(test1) == 1);
+ assert property ($countones(test5) == 3);
+
+ assert property ($isunknown(8'h00) == 0);
+ assert property ($isunknown(8'hff) == 0);
+ assert property ($isunknown(8'hx0) == 1);
+ assert property ($isunknown(8'h1z) == 1);
+ assert property ($isunknown(8'hxz) == 1);
+
+ assert property ($onehot(8'h00) == 0);
+ assert property ($onehot(8'hff) == 0);
+ assert property ($onehot(8'h01) == 1);
+ assert property ($onehot(8'h80) == 1);
+ assert property ($onehot(8'h81) == 0);
+ assert property ($onehot(8'h20) == 1);
+
+ assert property ($onehot0(8'h00) == 1);
+ assert property ($onehot0(8'hff) == 0);
+ assert property ($onehot0(8'h01) == 1);
+ assert property ($onehot0(8'h80) == 1);
+ assert property ($onehot0(8'h81) == 0);
+ assert property ($onehot0(8'h20) == 1);
+
+endmodule
diff --git a/tests/various/countbits.ys b/tests/various/countbits.ys
new file mode 100644
index 000000000..a556f7c5d
--- /dev/null
+++ b/tests/various/countbits.ys
@@ -0,0 +1,7 @@
+read_verilog -sv countbits.sv
+hierarchy
+proc
+flatten
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all
diff --git a/tests/various/fib_tern.v b/tests/various/fib_tern.v
new file mode 100644
index 000000000..fefde74ce
--- /dev/null
+++ b/tests/various/fib_tern.v
@@ -0,0 +1,70 @@
+module gate(
+ off, fib0, fib1, fib2, fib3, fib4, fib5, fib6, fib7, fib8, fib9
+);
+ input wire signed [31:0] off;
+
+ function automatic blah(
+ input x
+ );
+ blah = x;
+ endfunction
+
+ function automatic integer fib(
+ input integer k
+ );
+ fib = k == 0
+ ? 0
+ : k == 1
+ ? 1
+ : fib(k - 1) + fib(k - 2);
+ endfunction
+
+ function automatic integer fib_wrap(
+ input integer k,
+ output integer o
+ );
+ o = off + fib(k);
+ endfunction
+
+ output integer fib0;
+ output integer fib1;
+ output integer fib2;
+ output integer fib3;
+ output integer fib4;
+ output integer fib5;
+ output integer fib6;
+ output integer fib7;
+ output integer fib8;
+ output integer fib9;
+
+ initial begin : blk
+ integer unused;
+ unused = fib_wrap(0, fib0);
+ unused = fib_wrap(1, fib1);
+ unused = fib_wrap(2, fib2);
+ unused = fib_wrap(3, fib3);
+ unused = fib_wrap(4, fib4);
+ unused = fib_wrap(5, fib5);
+ unused = fib_wrap(6, fib6);
+ unused = fib_wrap(7, fib7);
+ unused = fib_wrap(8, fib8);
+ unused = fib_wrap(9, fib9);
+ end
+endmodule
+
+module gold(
+ off, fib0, fib1, fib2, fib3, fib4, fib5, fib6, fib7, fib8, fib9
+);
+ input wire signed [31:0] off;
+
+ output integer fib0 = off + 0;
+ output integer fib1 = off + 1;
+ output integer fib2 = off + 1;
+ output integer fib3 = off + 2;
+ output integer fib4 = off + 3;
+ output integer fib5 = off + 5;
+ output integer fib6 = off + 8;
+ output integer fib7 = off + 13;
+ output integer fib8 = off + 21;
+ output integer fib9 = off + 34;
+endmodule
diff --git a/tests/various/fib_tern.ys b/tests/various/fib_tern.ys
new file mode 100644
index 000000000..e5bf186e1
--- /dev/null
+++ b/tests/various/fib_tern.ys
@@ -0,0 +1,6 @@
+read_verilog fib_tern.v
+hierarchy
+proc
+equiv_make gold gate equiv
+equiv_simple
+equiv_status -assert
diff --git a/tests/various/gen_if_null.v b/tests/various/gen_if_null.v
index a12ac6288..992bc68b3 100644
--- a/tests/various/gen_if_null.v
+++ b/tests/various/gen_if_null.v
@@ -1,13 +1,17 @@
-module test(x, y, z);
+`default_nettype none
+module test;
localparam OFF = 0;
generate
if (OFF) ;
- else input x;
- if (!OFF) input y;
+ else wire x;
+ if (!OFF) wire y;
else ;
if (OFF) ;
else ;
if (OFF) ;
- input z;
+ wire z;
endgenerate
+ assign genblk1.x = 0;
+ assign genblk2.y = 0;
+ assign z = 0;
endmodule
diff --git a/tests/various/gen_if_null.ys b/tests/various/gen_if_null.ys
index 31dfc444b..0733e3a94 100644
--- a/tests/various/gen_if_null.ys
+++ b/tests/various/gen_if_null.ys
@@ -1,4 +1,4 @@
read_verilog gen_if_null.v
-select -assert-count 1 test/x
-select -assert-count 1 test/y
+select -assert-count 1 test/genblk1.x
+select -assert-count 1 test/genblk2.y
select -assert-count 1 test/z
diff --git a/tests/various/port_sign_extend.v b/tests/various/port_sign_extend.v
index 446268268..813ceb503 100644
--- a/tests/various/port_sign_extend.v
+++ b/tests/various/port_sign_extend.v
@@ -24,8 +24,8 @@ module PassThrough(a, b);
assign b = a;
endmodule
-module act(o1, o2, o3, o4, o5, o6, yay1, nay1, yay2, nay2);
- output wire [3:0] o1, o2, o3, o4, o5, o6;
+module act(o1, o2, o3, o4, o5, o6, o7, o8, o9, yay1, nay1, yay2, nay2);
+ output wire [3:0] o1, o2, o3, o4, o5, o6, o7, o8, o9;
// unsigned constant
PassThrough pt1(1'b1, o1);
@@ -52,6 +52,17 @@ module act(o1, o2, o3, o4, o5, o6, yay1, nay1, yay2, nay2);
wire signed [2:0] tmp6b = 3'b001;
PassThrough pt6(tmp6a ? tmp6a : tmp6b, o6);
+ wire signed [2:0] tmp7 = 3'b011;
+ PassThrough pt7(~tmp7, o7);
+
+ reg signed [2:0] tmp8 [0:0];
+ initial tmp8[0] = 3'b101;
+ PassThrough pt8(tmp8[0], o8);
+
+ wire signed [2:0] tmp9a = 3'b100;
+ wire signed [1:0] tmp9b = 2'b11;
+ PassThrough pt9(0 ? tmp9a : tmp9b, o9);
+
output wire [2:0] yay1, nay1;
GeneratorSigned1 os1(yay1);
GeneratorUnsigned1 ou1(nay1);
@@ -61,8 +72,8 @@ module act(o1, o2, o3, o4, o5, o6, yay1, nay1, yay2, nay2);
GeneratorUnsigned2 ou2(nay2);
endmodule
-module ref(o1, o2, o3, o4, o5, o6, yay1, nay1, yay2, nay2);
- output wire [3:0] o1, o2, o3, o4, o5, o6;
+module ref(o1, o2, o3, o4, o5, o6, o7, o8, o9, yay1, nay1, yay2, nay2);
+ output wire [3:0] o1, o2, o3, o4, o5, o6, o7, o8, o9;
assign o1 = 4'b0001;
assign o2 = 4'b0001;
@@ -70,6 +81,9 @@ module ref(o1, o2, o3, o4, o5, o6, yay1, nay1, yay2, nay2);
assign o4 = 4'b1111;
assign o5 = 4'b1110;
assign o6 = 4'b1100;
+ assign o7 = 4'b1100;
+ assign o8 = 4'b1101;
+ assign o9 = 4'b1111;
output wire [2:0] yay1, nay1;
assign yay1 = 3'b111;
diff --git a/tests/various/port_sign_extend.ys b/tests/various/port_sign_extend.ys
index 0a6a93810..6d1adf7f3 100644
--- a/tests/various/port_sign_extend.ys
+++ b/tests/various/port_sign_extend.ys
@@ -1,22 +1,29 @@
-read_verilog port_sign_extend.v
+read_verilog -nomem2reg port_sign_extend.v
hierarchy
flatten
+proc
+memory
equiv_make ref act equiv
equiv_simple
equiv_status -assert
delete
-read_verilog port_sign_extend.v
+read_verilog -nomem2reg port_sign_extend.v
flatten
+proc
+memory
equiv_make ref act equiv
equiv_simple
equiv_status -assert
delete
-read_verilog port_sign_extend.v
+read_verilog -nomem2reg port_sign_extend.v
hierarchy
+proc
+memory
equiv_make ref act equiv
prep -flatten -top equiv
+equiv_induct
equiv_status -assert
diff --git a/tests/various/rand_const.sv b/tests/various/rand_const.sv
new file mode 100644
index 000000000..be00812c0
--- /dev/null
+++ b/tests/various/rand_const.sv
@@ -0,0 +1,8 @@
+module top;
+ rand const reg rx;
+ const reg ry;
+ rand reg rz;
+ rand const integer ix;
+ const integer iy;
+ rand integer iz;
+endmodule
diff --git a/tests/various/rand_const.ys b/tests/various/rand_const.ys
new file mode 100644
index 000000000..74e43c7cc
--- /dev/null
+++ b/tests/various/rand_const.ys
@@ -0,0 +1 @@
+read_verilog -sv rand_const.sv
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-08 19:44:53 +0000