aboutsummaryrefslogtreecommitdiffstats
path: root/tests/verilog
diff options
context:
space:
mode:
Diffstat (limited to 'tests/verilog')
-rw-r--r--tests/verilog/.gitignore1
-rw-r--r--tests/verilog/always_comb_latch_1.ys13
-rw-r--r--tests/verilog/always_comb_latch_2.ys15
-rw-r--r--tests/verilog/always_comb_latch_3.ys20
-rw-r--r--tests/verilog/always_comb_latch_4.ys17
-rw-r--r--tests/verilog/always_comb_nolatch_1.ys16
-rw-r--r--tests/verilog/always_comb_nolatch_2.ys17
-rw-r--r--tests/verilog/always_comb_nolatch_3.ys21
-rw-r--r--tests/verilog/always_comb_nolatch_4.ys16
-rw-r--r--tests/verilog/doubleslash.ys2
-rw-r--r--tests/verilog/size_cast.sv140
-rw-r--r--tests/verilog/size_cast.ys5
12 files changed, 283 insertions, 0 deletions
diff --git a/tests/verilog/.gitignore b/tests/verilog/.gitignore
index 34da23437..96ebe20ba 100644
--- a/tests/verilog/.gitignore
+++ b/tests/verilog/.gitignore
@@ -3,3 +3,4 @@
/run-test.mk
/const_arst.v
/const_sr.v
+/doubleslash.v
diff --git a/tests/verilog/always_comb_latch_1.ys b/tests/verilog/always_comb_latch_1.ys
new file mode 100644
index 000000000..c98c79fa2
--- /dev/null
+++ b/tests/verilog/always_comb_latch_1.ys
@@ -0,0 +1,13 @@
+read_verilog -sv <<EOF
+module top;
+logic x;
+always_comb begin
+ logic y;
+ if (x)
+ y = 1;
+ x = y;
+end
+endmodule
+EOF
+logger -expect error "^Latch inferred for signal `\\top\.\$unnamed_block\$1\.y' from always_comb process" 1
+proc
diff --git a/tests/verilog/always_comb_latch_2.ys b/tests/verilog/always_comb_latch_2.ys
new file mode 100644
index 000000000..567205a53
--- /dev/null
+++ b/tests/verilog/always_comb_latch_2.ys
@@ -0,0 +1,15 @@
+read_verilog -sv <<EOF
+module top;
+logic x;
+always_comb begin
+ logic y;
+ if (x)
+ x = 1;
+ else
+ y = 1;
+ x = y;
+end
+endmodule
+EOF
+logger -expect error "^Latch inferred for signal `\\top\.\$unnamed_block\$1\.y' from always_comb process" 1
+proc
diff --git a/tests/verilog/always_comb_latch_3.ys b/tests/verilog/always_comb_latch_3.ys
new file mode 100644
index 000000000..b9b028ac7
--- /dev/null
+++ b/tests/verilog/always_comb_latch_3.ys
@@ -0,0 +1,20 @@
+read_verilog -sv <<EOF
+module top;
+logic x;
+logic z;
+assign z = 1'b1;
+always_comb begin
+ logic y;
+ case (x)
+ 1'b0:
+ y = 1;
+ endcase
+ if (z)
+ x = y;
+ else
+ x = 1'b0;
+end
+endmodule
+EOF
+logger -expect error "^Latch inferred for signal `\\top\.\$unnamed_block\$1\.y' from always_comb process" 1
+proc
diff --git a/tests/verilog/always_comb_latch_4.ys b/tests/verilog/always_comb_latch_4.ys
new file mode 100644
index 000000000..46b78801b
--- /dev/null
+++ b/tests/verilog/always_comb_latch_4.ys
@@ -0,0 +1,17 @@
+read_verilog -sv <<EOF
+module top;
+parameter AVOID_LATCH = 0;
+logic x, z;
+assign z = 1'b1;
+always_comb begin
+ logic y;
+ if (z)
+ y = 0;
+ for (int i = 1; i == AVOID_LATCH; i++)
+ y = 1;
+ x = z ? y : 1'b0;
+end
+endmodule
+EOF
+logger -expect error "^Latch inferred for signal `\\top\.\$unnamed_block\$3\.y' from always_comb process" 1
+proc
diff --git a/tests/verilog/always_comb_nolatch_1.ys b/tests/verilog/always_comb_nolatch_1.ys
new file mode 100644
index 000000000..4d1952b52
--- /dev/null
+++ b/tests/verilog/always_comb_nolatch_1.ys
@@ -0,0 +1,16 @@
+read_verilog -sv <<EOF
+module top;
+logic [4:0] x;
+logic z;
+assign z = 1'b1;
+always_comb begin
+ x = '0;
+ if (z) begin
+ for (int i = 0; i < 5; i++) begin
+ x[i] = 1'b1;
+ end
+ end
+end
+endmodule
+EOF
+proc
diff --git a/tests/verilog/always_comb_nolatch_2.ys b/tests/verilog/always_comb_nolatch_2.ys
new file mode 100644
index 000000000..2ec6ca0f4
--- /dev/null
+++ b/tests/verilog/always_comb_nolatch_2.ys
@@ -0,0 +1,17 @@
+read_verilog -sv <<EOF
+module top;
+logic [4:0] x;
+logic z;
+assign z = 1'b1;
+always_comb begin
+ x = '0;
+ if (z) begin
+ int i;
+ for (i = 0; i < 5; i++) begin
+ x[i] = 1'b1;
+ end
+ end
+end
+endmodule
+EOF
+proc
diff --git a/tests/verilog/always_comb_nolatch_3.ys b/tests/verilog/always_comb_nolatch_3.ys
new file mode 100644
index 000000000..33f9833a2
--- /dev/null
+++ b/tests/verilog/always_comb_nolatch_3.ys
@@ -0,0 +1,21 @@
+read_verilog -sv <<EOF
+module top;
+logic x;
+logic z;
+assign z = 1'b1;
+always_comb begin
+ logic y;
+ case (x)
+ 1'b0:
+ y = 1;
+ default:
+ y = 0;
+ endcase
+ if (z)
+ x = y;
+ else
+ x = 1'b0;
+end
+endmodule
+EOF
+proc
diff --git a/tests/verilog/always_comb_nolatch_4.ys b/tests/verilog/always_comb_nolatch_4.ys
new file mode 100644
index 000000000..bc29b2771
--- /dev/null
+++ b/tests/verilog/always_comb_nolatch_4.ys
@@ -0,0 +1,16 @@
+read_verilog -sv <<EOF
+module top;
+parameter AVOID_LATCH = 1;
+logic x, z;
+assign z = 1'b1;
+always_comb begin
+ logic y;
+ if (z)
+ y = 0;
+ for (int i = 1; i == AVOID_LATCH; i++)
+ y = 1;
+ x = z ? y : 1'b0;
+end
+endmodule
+EOF
+proc
diff --git a/tests/verilog/doubleslash.ys b/tests/verilog/doubleslash.ys
index 8a51f12c2..c41673ee5 100644
--- a/tests/verilog/doubleslash.ys
+++ b/tests/verilog/doubleslash.ys
@@ -17,3 +17,5 @@ proc
opt -full
write_verilog doubleslash.v
+design -reset
+read_verilog doubleslash.v
diff --git a/tests/verilog/size_cast.sv b/tests/verilog/size_cast.sv
new file mode 100644
index 000000000..1636f8d70
--- /dev/null
+++ b/tests/verilog/size_cast.sv
@@ -0,0 +1,140 @@
+module top;
+ logic L1b0 = 0;
+ logic L1b1 = 1;
+
+ logic signed L1sb0 = 0;
+ logic signed L1sb1 = 1;
+
+ logic [1:0] L2b00 = 0;
+ logic [1:0] L2b01 = 1;
+ logic [1:0] L2b10 = 2;
+ logic [1:0] L2b11 = 3;
+
+ logic signed [1:0] L2sb00 = 0;
+ logic signed [1:0] L2sb01 = 1;
+ logic signed [1:0] L2sb10 = 2;
+ logic signed [1:0] L2sb11 = 3;
+
+ logic y = 1;
+
+ always @* begin
+
+ assert (1'(L1b0 ) == 1'b0);
+ assert (1'(L1b1 ) == 1'b1);
+ assert (1'(L1sb0 ) == 1'b0);
+ assert (1'(L1sb1 ) == 1'b1);
+ assert (1'(L2b00 ) == 1'b0);
+ assert (1'(L2b01 ) == 1'b1);
+ assert (1'(L2b10 ) == 1'b0);
+ assert (1'(L2b11 ) == 1'b1);
+ assert (1'(L2sb00) == 1'b0);
+ assert (1'(L2sb01) == 1'b1);
+ assert (1'(L2sb10) == 1'b0);
+ assert (1'(L2sb11) == 1'b1);
+
+ assert (2'(L1b0 ) == 2'b00);
+ assert (2'(L1b1 ) == 2'b01);
+ assert (2'(L1sb0 ) == 2'b00);
+ assert (2'(L1sb1 ) == 2'b11);
+ assert (2'(L2b00 ) == 2'b00);
+ assert (2'(L2b01 ) == 2'b01);
+ assert (2'(L2b10 ) == 2'b10);
+ assert (2'(L2b11 ) == 2'b11);
+ assert (2'(L2sb00) == 2'b00);
+ assert (2'(L2sb01) == 2'b01);
+ assert (2'(L2sb10) == 2'b10);
+ assert (2'(L2sb11) == 2'b11);
+
+ assert (3'(L1b0 ) == 3'b000);
+ assert (3'(L1b1 ) == 3'b001);
+ assert (3'(L1sb0 ) == 3'b000);
+ assert (3'(L1sb1 ) == 3'b111);
+ assert (3'(L2b00 ) == 3'b000);
+ assert (3'(L2b01 ) == 3'b001);
+ assert (3'(L2b10 ) == 3'b010);
+ assert (3'(L2b11 ) == 3'b011);
+ assert (3'(L2sb00) == 3'b000);
+ assert (3'(L2sb01) == 3'b001);
+ assert (3'(L2sb10) == 3'b110);
+ assert (3'(L2sb11) == 3'b111);
+
+ assert (3'(L1b0 | '1) == 3'b111);
+ assert (3'(L1b1 | '1) == 3'b111);
+ assert (3'(L1sb0 | '1) == 3'b111);
+ assert (3'(L1sb1 | '1) == 3'b111);
+ assert (3'(L2b00 | '1) == 3'b111);
+ assert (3'(L2b01 | '1) == 3'b111);
+ assert (3'(L2b10 | '1) == 3'b111);
+ assert (3'(L2b11 | '1) == 3'b111);
+ assert (3'(L2sb00 | '1) == 3'b111);
+ assert (3'(L2sb01 | '1) == 3'b111);
+ assert (3'(L2sb10 | '1) == 3'b111);
+ assert (3'(L2sb11 | '1) == 3'b111);
+
+ assert (3'(L1b0 | '0) == 3'b000);
+ assert (3'(L1b1 | '0) == 3'b001);
+ assert (3'(L1sb0 | '0) == 3'b000);
+ assert (3'(L1sb1 | '0) == 3'b001);
+ assert (3'(L2b00 | '0) == 3'b000);
+ assert (3'(L2b01 | '0) == 3'b001);
+ assert (3'(L2b10 | '0) == 3'b010);
+ assert (3'(L2b11 | '0) == 3'b011);
+ assert (3'(L2sb00 | '0) == 3'b000);
+ assert (3'(L2sb01 | '0) == 3'b001);
+ assert (3'(L2sb10 | '0) == 3'b010);
+ assert (3'(L2sb11 | '0) == 3'b011);
+
+ assert (3'(y ? L1b0 : '1) == 3'b000);
+ assert (3'(y ? L1b1 : '1) == 3'b001);
+ assert (3'(y ? L1sb0 : '1) == 3'b000);
+ assert (3'(y ? L1sb1 : '1) == 3'b001);
+ assert (3'(y ? L2b00 : '1) == 3'b000);
+ assert (3'(y ? L2b01 : '1) == 3'b001);
+ assert (3'(y ? L2b10 : '1) == 3'b010);
+ assert (3'(y ? L2b11 : '1) == 3'b011);
+ assert (3'(y ? L2sb00 : '1) == 3'b000);
+ assert (3'(y ? L2sb01 : '1) == 3'b001);
+ assert (3'(y ? L2sb10 : '1) == 3'b010);
+ assert (3'(y ? L2sb11 : '1) == 3'b011);
+
+ assert (3'(y ? L1b0 : '0) == 3'b000);
+ assert (3'(y ? L1b1 : '0) == 3'b001);
+ assert (3'(y ? L1sb0 : '0) == 3'b000);
+ assert (3'(y ? L1sb1 : '0) == 3'b001);
+ assert (3'(y ? L2b00 : '0) == 3'b000);
+ assert (3'(y ? L2b01 : '0) == 3'b001);
+ assert (3'(y ? L2b10 : '0) == 3'b010);
+ assert (3'(y ? L2b11 : '0) == 3'b011);
+ assert (3'(y ? L2sb00 : '0) == 3'b000);
+ assert (3'(y ? L2sb01 : '0) == 3'b001);
+ assert (3'(y ? L2sb10 : '0) == 3'b010);
+ assert (3'(y ? L2sb11 : '0) == 3'b011);
+
+ assert (3'(y ? L1b0 : 1'sb0) == 3'b000);
+ assert (3'(y ? L1b1 : 1'sb0) == 3'b001);
+ assert (3'(y ? L1sb0 : 1'sb0) == 3'b000);
+ assert (3'(y ? L1sb1 : 1'sb0) == 3'b111);
+ assert (3'(y ? L2b00 : 1'sb0) == 3'b000);
+ assert (3'(y ? L2b01 : 1'sb0) == 3'b001);
+ assert (3'(y ? L2b10 : 1'sb0) == 3'b010);
+ assert (3'(y ? L2b11 : 1'sb0) == 3'b011);
+ assert (3'(y ? L2sb00 : 1'sb0) == 3'b000);
+ assert (3'(y ? L2sb01 : 1'sb0) == 3'b001);
+ assert (3'(y ? L2sb10 : 1'sb0) == 3'b110);
+ assert (3'(y ? L2sb11 : 1'sb0) == 3'b111);
+
+ assert (3'(y ? L1b0 : 1'sb1) == 3'b000);
+ assert (3'(y ? L1b1 : 1'sb1) == 3'b001);
+ assert (3'(y ? L1sb0 : 1'sb1) == 3'b000);
+ assert (3'(y ? L1sb1 : 1'sb1) == 3'b111);
+ assert (3'(y ? L2b00 : 1'sb1) == 3'b000);
+ assert (3'(y ? L2b01 : 1'sb1) == 3'b001);
+ assert (3'(y ? L2b10 : 1'sb1) == 3'b010);
+ assert (3'(y ? L2b11 : 1'sb1) == 3'b011);
+ assert (3'(y ? L2sb00 : 1'sb1) == 3'b000);
+ assert (3'(y ? L2sb01 : 1'sb1) == 3'b001);
+ assert (3'(y ? L2sb10 : 1'sb1) == 3'b110);
+ assert (3'(y ? L2sb11 : 1'sb1) == 3'b111);
+
+ end
+endmodule
diff --git a/tests/verilog/size_cast.ys b/tests/verilog/size_cast.ys
new file mode 100644
index 000000000..6890cd2d5
--- /dev/null
+++ b/tests/verilog/size_cast.ys
@@ -0,0 +1,5 @@
+read_verilog -sv size_cast.sv
+proc
+opt -full
+select -module top
+sat -verify -prove-asserts -show-all
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-26 19:46:34 +0000