aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/verilog/net_types.sv34
-rw-r--r--tests/verilog/net_types.ys5
-rw-r--r--tests/verilog/prefix.sv95
-rw-r--r--tests/verilog/prefix.ys5
4 files changed, 139 insertions, 0 deletions
diff --git a/tests/verilog/net_types.sv b/tests/verilog/net_types.sv
new file mode 100644
index 000000000..7226a7ee5
--- /dev/null
+++ b/tests/verilog/net_types.sv
@@ -0,0 +1,34 @@
+module top;
+ wire logic wire_logic_0; assign wire_logic_0 = 0;
+ wire logic wire_logic_1; assign wire_logic_1 = 1;
+ wand logic wand_logic_0; assign wand_logic_0 = 0; assign wand_logic_0 = 1;
+ wand logic wand_logic_1; assign wand_logic_1 = 1; assign wand_logic_1 = 1;
+ wor logic wor_logic_0; assign wor_logic_0 = 0; assign wor_logic_0 = 0;
+ wor logic wor_logic_1; assign wor_logic_1 = 1; assign wor_logic_1 = 0;
+
+ wire integer wire_integer; assign wire_integer = 4'b1001;
+ wand integer wand_integer; assign wand_integer = 4'b1001; assign wand_integer = 4'b1010;
+ wor integer wor_integer; assign wor_integer = 4'b1001; assign wor_integer = 4'b1010;
+
+ typedef logic [3:0] typename;
+ wire typename wire_typename; assign wire_typename = 4'b1001;
+ wand typename wand_typename; assign wand_typename = 4'b1001; assign wand_typename = 4'b1010;
+ wor typename wor_typename; assign wor_typename = 4'b1001; assign wor_typename = 4'b1010;
+
+ always @* begin
+ assert (wire_logic_0 == 0);
+ assert (wire_logic_1 == 1);
+ assert (wand_logic_0 == 0);
+ assert (wand_logic_1 == 1);
+ assert (wor_logic_0 == 0);
+ assert (wor_logic_1 == 1);
+
+ assert (wire_integer == 4'b1001);
+ assert (wand_integer == 4'b1000);
+ assert (wor_integer == 4'b1011);
+
+ assert (wire_typename == 4'b1001);
+ assert (wand_typename == 4'b1000);
+ assert (wor_typename == 4'b1011);
+ end
+endmodule
diff --git a/tests/verilog/net_types.ys b/tests/verilog/net_types.ys
new file mode 100644
index 000000000..9f75812ea
--- /dev/null
+++ b/tests/verilog/net_types.ys
@@ -0,0 +1,5 @@
+read_verilog -sv net_types.sv
+hierarchy
+proc
+opt -full
+sat -verify -prove-asserts -show-all
diff --git a/tests/verilog/prefix.sv b/tests/verilog/prefix.sv
new file mode 100644
index 000000000..2d7fbb134
--- /dev/null
+++ b/tests/verilog/prefix.sv
@@ -0,0 +1,95 @@
+module top;
+ genvar i, j;
+ if (1) begin : blk1
+ integer a = 1;
+ for (i = 0; i < 2; i = i + 1) begin : blk2
+ integer b = i;
+ for (j = 0; j < 2; j = j + 1) begin : blk3
+ integer c = j;
+ localparam x = i;
+ localparam y = j;
+ always @* begin
+ assert (1 == a);
+ assert (1 == blk1.a);
+ assert (1 == top.blk1.a);
+ assert (i == b);
+ assert (i == blk2[i].b);
+ assert (i == blk1.blk2[i].b);
+ assert (i == top.blk1.blk2[i].b);
+ assert (i == blk2[x].b);
+ assert (i == blk1.blk2[x].b);
+ assert (i == top.blk1.blk2[x].b);
+ assert (j == c);
+ assert (j == blk3[j].c);
+ assert (j == blk2[x].blk3[j].c);
+ assert (j == blk1.blk2[x].blk3[j].c);
+ assert (j == top.blk1.blk2[x].blk3[j].c);
+ assert (j == c);
+ assert (j == blk3[y].c);
+ assert (j == blk2[x].blk3[y].c);
+ assert (j == blk1.blk2[x].blk3[y].c);
+ assert (j == top.blk1.blk2[x].blk3[y].c);
+ assert (j == top.blk1.blk2[x].blk3[y].c[0]);
+ assert (0 == top.blk1.blk2[x].blk3[y].c[1]);
+ assert (0 == top.blk1.blk2[x].blk3[y].c[j]);
+ end
+ end
+ always @* begin
+ assert (1 == a);
+ assert (1 == blk1.a);
+ assert (1 == top.blk1.a);
+ assert (i == b);
+ assert (i == blk2[i].b);
+ assert (i == blk1.blk2[i].b);
+ assert (i == top.blk1.blk2[i].b);
+ assert (0 == blk3[0].c);
+ assert (0 == blk2[i].blk3[0].c);
+ assert (0 == blk1.blk2[i].blk3[0].c);
+ assert (0 == top.blk1.blk2[i].blk3[0].c);
+ assert (1 == blk3[1].c);
+ assert (1 == blk2[i].blk3[1].c);
+ assert (1 == blk1.blk2[i].blk3[1].c);
+ assert (1 == top.blk1.blk2[i].blk3[1].c);
+ end
+ end
+ always @* begin
+ assert (1 == a);
+ assert (1 == blk1.a);
+ assert (1 == top.blk1.a);
+ assert (0 == blk2[0].b);
+ assert (0 == blk1.blk2[0].b);
+ assert (0 == top.blk1.blk2[0].b);
+ assert (1 == blk2[1].b);
+ assert (1 == blk1.blk2[1].b);
+ assert (1 == top.blk1.blk2[1].b);
+ assert (0 == blk2[0].blk3[0].c);
+ assert (0 == blk1.blk2[0].blk3[0].c);
+ assert (0 == top.blk1.blk2[0].blk3[0].c);
+ assert (1 == blk2[0].blk3[1].c);
+ assert (1 == blk1.blk2[0].blk3[1].c);
+ assert (1 == top.blk1.blk2[0].blk3[1].c);
+ assert (0 == blk2[1].blk3[0].c);
+ assert (0 == blk1.blk2[1].blk3[0].c);
+ assert (0 == top.blk1.blk2[1].blk3[0].c);
+ assert (1 == blk2[1].blk3[1].c);
+ assert (1 == blk1.blk2[1].blk3[1].c);
+ assert (1 == top.blk1.blk2[1].blk3[1].c);
+ end
+ end
+ always @* begin
+ assert (1 == blk1.a);
+ assert (1 == top.blk1.a);
+ assert (0 == blk1.blk2[0].b);
+ assert (0 == top.blk1.blk2[0].b);
+ assert (1 == blk1.blk2[1].b);
+ assert (1 == top.blk1.blk2[1].b);
+ assert (0 == blk1.blk2[0].blk3[0].c);
+ assert (0 == top.blk1.blk2[0].blk3[0].c);
+ assert (1 == blk1.blk2[0].blk3[1].c);
+ assert (1 == top.blk1.blk2[0].blk3[1].c);
+ assert (0 == blk1.blk2[1].blk3[0].c);
+ assert (0 == top.blk1.blk2[1].blk3[0].c);
+ assert (1 == blk1.blk2[1].blk3[1].c);
+ assert (1 == top.blk1.blk2[1].blk3[1].c);
+ end
+endmodule
diff --git a/tests/verilog/prefix.ys b/tests/verilog/prefix.ys
new file mode 100644
index 000000000..ed3b3a111
--- /dev/null
+++ b/tests/verilog/prefix.ys
@@ -0,0 +1,5 @@
+read_verilog -sv prefix.sv
+hierarchy
+proc
+select -module top
+sat -verify -seq 1 -prove-asserts -show-all