Merge branch 'master' into clk2ff-better-names

67 files changed, 1307 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/absurd_width.ys b/tests/verilog/absurd_width.ys
new file mode 100644
index 000000000..c0d2af4c2
--- /dev/null
+++ b/tests/verilog/absurd_width.ys
@@ -0,0 +1,17 @@
+logger -expect error "Expression width 1073741824 exceeds implementation limit of 16777216!" 1
+read_verilog <<EOF
+module top(
+    input inp,
+    output out
+);
+    assign out =
+        {1024 {
+        {1024 {
+        {1024 {
+        inp
+        }}
+        }}
+        }}
+        ;
+endmodule
+EOF
diff --git a/tests/verilog/absurd_width_const.ys b/tests/verilog/absurd_width_const.ys
new file mode 100644
index 000000000..b7191fd0d
--- /dev/null
+++ b/tests/verilog/absurd_width_const.ys
@@ -0,0 +1,16 @@
+logger -expect error "Expression width 1073741824 exceeds implementation limit of 16777216!" 1
+read_verilog <<EOF
+module top(
+    output out
+);
+    assign out =
+        {1024 {
+        {1024 {
+        {1024 {
+        1'b1
+        }}
+        }}
+        }}
+        ;
+endmodule
+EOF
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/block_end_label_only.ys b/tests/verilog/block_end_label_only.ys
new file mode 100644
index 000000000..5db1c7879
--- /dev/null
+++ b/tests/verilog/block_end_label_only.ys
@@ -0,0 +1,9 @@
+logger -expect error "Begin label missing where end label \(incorrect_name\) was given\." 1
+read_verilog -sv <<EOF
+module top;
+initial
+    begin
+        $display("HI");
+    end : incorrect_name
+endmodule
+EOF
diff --git a/tests/verilog/block_end_label_wrong.ys b/tests/verilog/block_end_label_wrong.ys
new file mode 100644
index 000000000..47dbbe32f
--- /dev/null
+++ b/tests/verilog/block_end_label_wrong.ys
@@ -0,0 +1,9 @@
+logger -expect error "Begin label \(correct_name\) and end label \(incorrect_name\) don't match\." 1
+read_verilog -sv <<EOF
+module top;
+initial
+    begin : correct_name
+        $display("HI");
+    end : incorrect_name
+endmodule
+EOF
diff --git a/tests/verilog/doubleslash.ys b/tests/verilog/doubleslash.ys
new file mode 100644
index 000000000..c41673ee5
--- /dev/null
+++ b/tests/verilog/doubleslash.ys
@@ -0,0 +1,21 @@
+read_verilog -sv <<EOT
+module doubleslash
+  (input  logic   a,
+   input  logic   b,
+   output logic   z);
+
+  logic \a//b ;
+
+  assign \a//b = a & b;
+  assign z = ~\a//b ;
+
+endmodule : doubleslash
+EOT
+
+hierarchy
+proc
+opt -full
+
+write_verilog doubleslash.v
+design -reset
+read_verilog doubleslash.v
diff --git a/tests/verilog/for_decl_no_init.ys b/tests/verilog/for_decl_no_init.ys
new file mode 100644
index 000000000..68c1584e0
--- /dev/null
+++ b/tests/verilog/for_decl_no_init.ys
@@ -0,0 +1,9 @@
+logger -expect error "For loop variable declaration is missing initialization!" 1
+read_verilog -sv <<EOT
+module top;
+    integer z;
+    initial
+        for (integer i; i < 10; i = i + 1)
+            z = i;
+endmodule
+EOT
diff --git a/tests/verilog/for_decl_no_sv.ys b/tests/verilog/for_decl_no_sv.ys
new file mode 100644
index 000000000..34edddff7
--- /dev/null
+++ b/tests/verilog/for_decl_no_sv.ys
@@ -0,0 +1,9 @@
+logger -expect error "For loop inline variable declaration is only supported in SystemVerilog mode!" 1
+read_verilog <<EOT
+module top;
+    integer z;
+    initial
+        for (integer i = 1; i < 10; i = i + 1)
+            z = i;
+endmodule
+EOT
diff --git a/tests/verilog/for_decl_shadow.sv b/tests/verilog/for_decl_shadow.sv
new file mode 100644
index 000000000..f6948f97e
--- /dev/null
+++ b/tests/verilog/for_decl_shadow.sv
@@ -0,0 +1,32 @@
+module gate(x);
+	output reg [15:0] x;
+	if (1) begin : gen
+		integer x;
+		initial begin
+			for (integer x = 5; x < 10; x++)
+				if (x == 5)
+					gen.x = 0;
+				else
+					gen.x += 2 ** x;
+			x = x * 2;
+		end
+	end
+	initial x = gen.x;
+endmodule
+
+module gold(x);
+	output reg [15:0] x;
+	if (1) begin : gen
+		integer x;
+		integer z;
+		initial begin
+			for (z = 5; z < 10; z++)
+				if (z == 5)
+					x = 0;
+				else
+					x += 2 ** z;
+			x = x * 2;
+		end
+	end
+	initial x = gen.x;
+endmodule
diff --git a/tests/verilog/for_decl_shadow.ys b/tests/verilog/for_decl_shadow.ys
new file mode 100644
index 000000000..d2dca715e
--- /dev/null
+++ b/tests/verilog/for_decl_shadow.ys
@@ -0,0 +1,6 @@
+read_verilog -sv for_decl_shadow.sv
+hierarchy
+proc
+equiv_make gold gate equiv
+equiv_simple
+equiv_status -assert
diff --git a/tests/verilog/func_typename_ret.sv b/tests/verilog/func_typename_ret.sv
new file mode 100644
index 000000000..423975f97
--- /dev/null
+++ b/tests/verilog/func_typename_ret.sv
@@ -0,0 +1,35 @@
+typedef logic [1:0] T;
+
+package P;
+    typedef logic [3:0] S;
+endpackage
+
+module gate(
+    output wire [31:0] out1, out2
+);
+    function automatic T func1;
+        input reg signed inp;
+        func1 = inp;
+    endfunction
+    assign out1 = func1(1);
+    function automatic P::S func2;
+        input reg signed inp;
+        func2 = inp;
+    endfunction
+    assign out2 = func2(1);
+endmodule
+
+module gold(
+    output wire [31:0] out1, out2
+);
+    function automatic [1:0] func1;
+        input reg signed inp;
+        func1 = inp;
+    endfunction
+    assign out1 = func1(1);
+    function automatic [3:0] func2;
+        input reg signed inp;
+        func2 = inp;
+    endfunction
+    assign out2 = func2(1);
+endmodule
diff --git a/tests/verilog/func_typename_ret.ys b/tests/verilog/func_typename_ret.ys
new file mode 100644
index 000000000..7f6049961
--- /dev/null
+++ b/tests/verilog/func_typename_ret.ys
@@ -0,0 +1,5 @@
+read_verilog -sv func_typename_ret.sv
+proc
+equiv_make gold gate equiv
+equiv_simple
+equiv_status -assert
diff --git a/tests/verilog/gen_block_end_label_only.ys b/tests/verilog/gen_block_end_label_only.ys
new file mode 100644
index 000000000..60dc0476a
--- /dev/null
+++ b/tests/verilog/gen_block_end_label_only.ys
@@ -0,0 +1,9 @@
+logger -expect error "Begin label missing where end label \(incorrect_name\) was given\." 1
+read_verilog -sv <<EOF
+module top;
+if (1)
+    begin
+        initial $display("HI");
+    end : incorrect_name
+endmodule
+EOF
diff --git a/tests/verilog/gen_block_end_label_wrong.ys b/tests/verilog/gen_block_end_label_wrong.ys
new file mode 100644
index 000000000..43cfc8773
--- /dev/null
+++ b/tests/verilog/gen_block_end_label_wrong.ys
@@ -0,0 +1,9 @@
+logger -expect error "Begin label \(correct_name\) and end label \(incorrect_name\) don't match\." 1
+read_verilog -sv <<EOF
+module top;
+if (1)
+    begin : correct_name
+        initial $display("HI");
+    end : incorrect_name
+endmodule
+EOF
diff --git a/tests/verilog/genfor_decl_no_init.ys b/tests/verilog/genfor_decl_no_init.ys
new file mode 100644
index 000000000..348899195
--- /dev/null
+++ b/tests/verilog/genfor_decl_no_init.ys
@@ -0,0 +1,7 @@
+logger -expect error "Generate for loop variable declaration is missing initialization!" 1
+read_verilog -sv <<EOT
+module top;
+    for (genvar i; i < 10; i = i + 1)
+        wire x;
+endmodule
+EOT
diff --git a/tests/verilog/genfor_decl_no_sv.ys b/tests/verilog/genfor_decl_no_sv.ys
new file mode 100644
index 000000000..124a27c28
--- /dev/null
+++ b/tests/verilog/genfor_decl_no_sv.ys
@@ -0,0 +1,7 @@
+logger -expect error "Generate for loop inline variable declaration is only supported in SystemVerilog mode!" 1
+read_verilog <<EOT
+module top;
+    for (genvar i = 1; i < 10; i = i + 1)
+        wire x;
+endmodule
+EOT
diff --git a/tests/verilog/genvar_loop_decl_1.sv b/tests/verilog/genvar_loop_decl_1.sv
new file mode 100644
index 000000000..b503f75da
--- /dev/null
+++ b/tests/verilog/genvar_loop_decl_1.sv
@@ -0,0 +1,18 @@
+`default_nettype none
+
+module gate(a);
+	for (genvar i = 0; i < 2; i++)
+		wire [i:0] x = '1;
+
+	output wire [32:0] a;
+	assign a = {1'b0, genblk1[0].x, 1'b0, genblk1[1].x, 1'b0};
+endmodule
+
+module gold(a);
+	genvar i;
+	for (i = 0; i < 2; i++)
+		wire [i:0] x = '1;
+
+	output wire [32:0] a;
+	assign a = {1'b0, genblk1[0].x, 1'b0, genblk1[1].x, 1'b0};
+endmodule
diff --git a/tests/verilog/genvar_loop_decl_1.ys b/tests/verilog/genvar_loop_decl_1.ys
new file mode 100644
index 000000000..ded486248
--- /dev/null
+++ b/tests/verilog/genvar_loop_decl_1.ys
@@ -0,0 +1,14 @@
+read_verilog -sv genvar_loop_decl_1.sv
+
+select -assert-count 1 gate/genblk1[0].x
+select -assert-count 1 gate/genblk1[1].x
+select -assert-count 0 gate/genblk1[2].x
+
+select -assert-count 1 gold/genblk1[0].x
+select -assert-count 1 gold/genblk1[1].x
+select -assert-count 0 gold/genblk1[2].x
+
+proc
+equiv_make gold gate equiv
+equiv_simple
+equiv_status -assert
diff --git a/tests/verilog/genvar_loop_decl_2.sv b/tests/verilog/genvar_loop_decl_2.sv
new file mode 100644
index 000000000..c5a85ef11
--- /dev/null
+++ b/tests/verilog/genvar_loop_decl_2.sv
@@ -0,0 +1,30 @@
+`default_nettype none
+
+module gate(out);
+    wire [3:0] x;
+    for (genvar x = 0; x < 2; x++) begin : blk
+        localparam w = x;
+        if (x == 0) begin : sub
+            wire [w:0] x;
+        end
+    end
+    assign x = 2;
+    assign blk[0].sub.x = '1;
+    output wire [9:0] out;
+    assign out = {1'bx, x, blk[0].sub.x};
+endmodule
+
+module gold(out);
+    wire [3:0] x;
+    genvar z;
+    for (z = 0; z < 2; z++) begin : blk
+        localparam w = z;
+        if (z == 0) begin : sub
+            wire [w:0] x;
+        end
+    end
+    assign x = 2;
+    assign blk[0].sub.x = '1;
+    output wire [9:0] out;
+    assign out = {1'bx, x, blk[0].sub.x};
+endmodule
diff --git a/tests/verilog/genvar_loop_decl_2.ys b/tests/verilog/genvar_loop_decl_2.ys
new file mode 100644
index 000000000..52fdeb49c
--- /dev/null
+++ b/tests/verilog/genvar_loop_decl_2.ys
@@ -0,0 +1,5 @@
+read_verilog -sv genvar_loop_decl_2.sv
+proc
+equiv_make gold gate equiv
+equiv_simple
+equiv_status -assert
diff --git a/tests/verilog/genvar_loop_decl_3.sv b/tests/verilog/genvar_loop_decl_3.sv
new file mode 100644
index 000000000..4d6d2366d
--- /dev/null
+++ b/tests/verilog/genvar_loop_decl_3.sv
@@ -0,0 +1,28 @@
+`default_nettype none
+
+module gate(x, y);
+    output reg [15:0] x, y;
+    if (1) begin : gen
+        integer x, y;
+        for (genvar x = 0; x < 2; x++)
+            if (x == 0)
+                initial gen.x = 10;
+        assign y = x + 1;
+    end
+    initial x = gen.x;
+    assign y = gen.y;
+endmodule
+
+module gold(x, y);
+    output reg [15:0] x, y;
+    if (1) begin : gen
+        integer x, y;
+        genvar z;
+        for (z = 0; z < 2; z++)
+            if (z == 0)
+                initial x = 10;
+        assign y = x + 1;
+    end
+    initial x = gen.x;
+    assign y = gen.y;
+endmodule
diff --git a/tests/verilog/genvar_loop_decl_3.ys b/tests/verilog/genvar_loop_decl_3.ys
new file mode 100644
index 000000000..19f754124
--- /dev/null
+++ b/tests/verilog/genvar_loop_decl_3.ys
@@ -0,0 +1,5 @@
+read_verilog -sv genvar_loop_decl_3.sv
+proc
+equiv_make gold gate equiv
+equiv_simple
+equiv_status -assert
diff --git a/tests/verilog/global_parameter.ys b/tests/verilog/global_parameter.ys
new file mode 100644
index 000000000..a7a3cddc7
--- /dev/null
+++ b/tests/verilog/global_parameter.ys
@@ -0,0 +1,16 @@
+read_verilog -sv <<EOF
+parameter P = 1;
+module example(
+    output integer out
+);
+    assign out = P;
+endmodule
+module top(
+    output integer out
+);
+    example #(2) e1(out);
+endmodule
+EOF
+
+logger -expect error "Can't find object for defparam" 1
+hierarchy
diff --git a/tests/verilog/ifdef_nest.ys b/tests/verilog/ifdef_nest.ys
new file mode 100644
index 000000000..2202109aa
--- /dev/null
+++ b/tests/verilog/ifdef_nest.ys
@@ -0,0 +1,7 @@
+read_verilog <<EOF
+`ifndef a
+`ifdef b
+`endif
+`else
+`endif
+EOF
diff --git a/tests/verilog/ifdef_unterminated.ys b/tests/verilog/ifdef_unterminated.ys
new file mode 100644
index 000000000..ce511fa8f
--- /dev/null
+++ b/tests/verilog/ifdef_unterminated.ys
@@ -0,0 +1,4 @@
+logger -expect error "Unterminated preprocessor conditional!" 1
+read_verilog <<EOF
+`ifndef a
+EOF
diff --git a/tests/verilog/localparam_no_default_1.ys b/tests/verilog/localparam_no_default_1.ys
new file mode 100644
index 000000000..426a48a1c
--- /dev/null
+++ b/tests/verilog/localparam_no_default_1.ys
@@ -0,0 +1,17 @@
+logger -expect-no-warnings
+read_verilog -sv <<EOF
+module Module #(
+    localparam X = 1
+);
+endmodule
+EOF
+
+design -reset
+
+logger -expect error "localparam initialization is missing!" 1
+read_verilog <<EOF
+module Module #(
+    localparam X
+);
+endmodule
+EOF
diff --git a/tests/verilog/localparam_no_default_2.ys b/tests/verilog/localparam_no_default_2.ys
new file mode 100644
index 000000000..b7b2622ad
--- /dev/null
+++ b/tests/verilog/localparam_no_default_2.ys
@@ -0,0 +1,15 @@
+logger -expect-no-warnings
+read_verilog -sv <<EOF
+module Module;
+    localparam X = 1;
+endmodule
+EOF
+
+design -reset
+
+logger -expect error "localparam initialization is missing!" 1
+read_verilog <<EOF
+module Module;
+    localparam X;
+endmodule
+EOF
diff --git a/tests/verilog/macro_arg_tromp.sv b/tests/verilog/macro_arg_tromp.sv
new file mode 100644
index 000000000..a9c68a417
--- /dev/null
+++ b/tests/verilog/macro_arg_tromp.sv
@@ -0,0 +1,21 @@
+// Taken from: https://github.com/YosysHQ/yosys/issues/2867
+
+`define MIN(x, y) ((x) < (y) ? (x) : (y))
+`define CEIL_DIV(x, y) (((x) / (y)) + `MIN((x) % (y), 1))
+
+module pad_msg1 (input logic [`MIN(512*`CEIL_DIV(64, 512), 64)-1:0] x,
+                output logic [`MIN(512*`CEIL_DIV(64, 512), 64)-1:0] y);
+   assign y[63:0] = x;
+endmodule
+
+module pad_msg2 (input logic [((512*`CEIL_DIV(64, 512)) < (64) ? (512*`CEIL_DIV(64,512)) : (64))-1:0] x,
+                output logic [((512*`CEIL_DIV(64, 512)) < (64) ? (512*`CEIL_DIV(64,512)) : (64))-1:0] y);
+   assign y[63:0] = x;
+endmodule
+
+module top(...);
+`define add(x) x +
+input [3:0] A;
+output [3:0] B;
+assign B = `add(`add(3)A)A;
+endmodule
diff --git a/tests/verilog/macro_arg_tromp.ys b/tests/verilog/macro_arg_tromp.ys
new file mode 100644
index 000000000..e8bd58e9b
--- /dev/null
+++ b/tests/verilog/macro_arg_tromp.ys
@@ -0,0 +1,2 @@
+logger -expect-no-warnings
+read_verilog -sv macro_arg_tromp.sv
diff --git a/tests/verilog/mem_bounds.sv b/tests/verilog/mem_bounds.sv
new file mode 100644
index 000000000..7fb2fb042
--- /dev/null
+++ b/tests/verilog/mem_bounds.sv
@@ -0,0 +1,27 @@
+module top;
+    reg [0:7] mem [0:2];
+
+    initial mem[1] = '1;
+    wire [31:0] a, b, c, d;
+    assign a = mem[1];
+    assign b = mem[-1];
+    assign c = mem[-1][0];
+    assign d = mem[-1][0:1];
+
+    always @* begin
+
+    	assert ($countbits(a, '0) == 24);
+    	assert ($countbits(a, '1) == 8);
+    	assert ($countbits(a, 'x) == 0);
+
+    	assert ($countbits(b, '0) == 24);
+    	assert ($countbits(b, 'x) == 8);
+
+    	assert ($countbits(c, '0) == 31);
+    	assert ($countbits(c, 'x) == 1);
+
+    	assert ($countbits(d, '0) == 30);
+    	assert ($countbits(d, 'x) == 2);
+
+    end
+endmodule
diff --git a/tests/verilog/mem_bounds.ys b/tests/verilog/mem_bounds.ys
new file mode 100644
index 000000000..42623ad09
--- /dev/null
+++ b/tests/verilog/mem_bounds.ys
@@ -0,0 +1,6 @@
+read_verilog -sv -mem2reg mem_bounds.sv
+proc
+flatten
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all -enable_undef
diff --git a/tests/verilog/module_end_label.ys b/tests/verilog/module_end_label.ys
new file mode 100644
index 000000000..c9e5a13a2
--- /dev/null
+++ b/tests/verilog/module_end_label.ys
@@ -0,0 +1,15 @@
+logger -expect-no-warnings
+read_verilog -sv <<EOF
+module correct_name;
+localparam X = 1;
+endmodule : correct_name
+EOF
+
+design -reset
+
+logger -expect error "Module name \(correct_name\) and end label \(incorrect_name\) don't match\." 1
+read_verilog -sv <<EOF
+module correct_name;
+localparam X = 1;
+endmodule : incorrect_name
+EOF
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/package_end_label.ys b/tests/verilog/package_end_label.ys
new file mode 100644
index 000000000..ccc5c96e9
--- /dev/null
+++ b/tests/verilog/package_end_label.ys
@@ -0,0 +1,15 @@
+logger -expect-no-warnings
+read_verilog -sv <<EOF
+package correct_name;
+localparam X = 1;
+endpackage : correct_name
+EOF
+
+design -reset
+
+logger -expect error "Package name \(correct_name\) and end label \(incorrect_name\) don't match\." 1
+read_verilog -sv <<EOF
+package correct_name;
+localparam X = 1;
+endpackage : incorrect_name
+EOF
diff --git a/tests/verilog/package_task_func.sv b/tests/verilog/package_task_func.sv
new file mode 100644
index 000000000..2df7a5205
--- /dev/null
+++ b/tests/verilog/package_task_func.sv
@@ -0,0 +1,30 @@
+package P;
+    localparam Y = 2;
+    localparam X = Y + 1;
+    task t;
+        output integer x;
+        x = Y;
+    endtask
+    function automatic integer f;
+        input integer i;
+        f = i * X;
+    endfunction
+    function automatic integer g;
+        input integer i;
+        g = i == 0 ? 1 : Y * g(i - 1);
+    endfunction
+    localparam Z = g(4);
+endpackage
+
+module top;
+    integer a;
+    initial P::t(a);
+    integer b = P::f(3);
+    integer c = P::g(3);
+    integer d = P::Z;
+
+    assert property (a == 2);
+    assert property (b == 9);
+    assert property (c == 8);
+    assert property (d == 16);
+endmodule
diff --git a/tests/verilog/package_task_func.ys b/tests/verilog/package_task_func.ys
new file mode 100644
index 000000000..c94cc2acb
--- /dev/null
+++ b/tests/verilog/package_task_func.ys
@@ -0,0 +1,4 @@
+read_verilog -sv package_task_func.sv
+proc
+opt -full
+sat -verify -seq 1 -prove-asserts -show-all
diff --git a/tests/verilog/param_no_default.sv b/tests/verilog/param_no_default.sv
new file mode 100644
index 000000000..cc35bd2ea
--- /dev/null
+++ b/tests/verilog/param_no_default.sv
@@ -0,0 +1,52 @@
+module example #(
+    parameter w,
+    parameter x = 1,
+    parameter byte y,
+    parameter byte z = 3
+) (
+    output a, b,
+    output byte c, d
+);
+    assign a = w;
+    assign b = x;
+    assign c = y;
+    assign d = z;
+endmodule
+
+module top;
+    wire a1, b1;
+    wire a2, b2;
+    wire a3, b3;
+    wire a4, b4;
+    byte c1, d1;
+    byte c2, d2;
+    byte c3, d3;
+    byte c4, d4;
+
+    example #(0, 1, 2) e1(a1, b1, c1, d1);
+    example #(.w(1), .y(4)) e2(a2, b2, c2, d2);
+    example #(.x(0), .w(1), .y(5)) e3(a3, b3, c3, d3);
+    example #(1, 0, 9, 10) e4(a4, b4, c4, d4);
+
+    always @* begin
+        assert (a1 == 0);
+        assert (b1 == 1);
+        assert (c1 == 2);
+        assert (d1 == 3);
+
+        assert (a2 == 1);
+        assert (b2 == 1);
+        assert (c2 == 4);
+        assert (d3 == 3);
+
+        assert (a3 == 1);
+        assert (b3 == 0);
+        assert (c3 == 5);
+        assert (d3 == 3);
+
+        assert (a4 == 1);
+        assert (b4 == 0);
+        assert (c4 == 9);
+        assert (d4 == 10);
+    end
+endmodule
diff --git a/tests/verilog/param_no_default.ys b/tests/verilog/param_no_default.ys
new file mode 100644
index 000000000..7f161a909
--- /dev/null
+++ b/tests/verilog/param_no_default.ys
@@ -0,0 +1,7 @@
+read_verilog -sv param_no_default.sv
+hierarchy
+proc
+flatten
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all
diff --git a/tests/verilog/param_no_default_not_svmode.ys b/tests/verilog/param_no_default_not_svmode.ys
new file mode 100644
index 000000000..1ded84e9c
--- /dev/null
+++ b/tests/verilog/param_no_default_not_svmode.ys
@@ -0,0 +1,26 @@
+logger -expect-no-warnings
+read_verilog -sv <<EOF
+module Module;
+    parameter X;
+endmodule
+EOF
+
+design -reset
+
+logger -expect-no-warnings
+read_verilog -sv <<EOF
+module Module #(
+    parameter X
+);
+endmodule
+EOF
+
+design -reset
+
+logger -expect error "Parameter defaults can only be omitted in SystemVerilog mode!" 1
+read_verilog <<EOF
+module Module #(
+    parameter X
+);
+endmodule
+EOF
diff --git a/tests/verilog/param_no_default_unbound_1.ys b/tests/verilog/param_no_default_unbound_1.ys
new file mode 100644
index 000000000..4aab85ab5
--- /dev/null
+++ b/tests/verilog/param_no_default_unbound_1.ys
@@ -0,0 +1,12 @@
+read_verilog -sv <<EOF
+module Example #(
+    parameter X
+);
+endmodule
+module top;
+    Example e();
+endmodule
+EOF
+
+logger -expect error "Parameter `\\X' has no default value and has not been overridden!" 1
+hierarchy -top top
diff --git a/tests/verilog/param_no_default_unbound_2.ys b/tests/verilog/param_no_default_unbound_2.ys
new file mode 100644
index 000000000..4b7f3b028
--- /dev/null
+++ b/tests/verilog/param_no_default_unbound_2.ys
@@ -0,0 +1,12 @@
+read_verilog -sv <<EOF
+module Example #(
+    parameter X, Y
+);
+endmodule
+module top;
+    Example e();
+endmodule
+EOF
+
+logger -expect error "Parameter `\\X' has no default value and has not been overridden!" 1
+hierarchy -top top
diff --git a/tests/verilog/param_no_default_unbound_3.ys b/tests/verilog/param_no_default_unbound_3.ys
new file mode 100644
index 000000000..f32b879a5
--- /dev/null
+++ b/tests/verilog/param_no_default_unbound_3.ys
@@ -0,0 +1,12 @@
+read_verilog -sv <<EOF
+module Example #(
+    parameter X, Y
+);
+endmodule
+module top;
+    Example #(1) e();
+endmodule
+EOF
+
+logger -expect error "Parameter `\\Y' has no default value and has not been overridden!" 1
+hierarchy -top top
diff --git a/tests/verilog/param_no_default_unbound_4.ys b/tests/verilog/param_no_default_unbound_4.ys
new file mode 100644
index 000000000..3a8d69d78
--- /dev/null
+++ b/tests/verilog/param_no_default_unbound_4.ys
@@ -0,0 +1,12 @@
+read_verilog -sv <<EOF
+module Example #(
+    parameter X, Y
+);
+endmodule
+module top;
+    Example #(.Y(1)) e();
+endmodule
+EOF
+
+logger -expect error "Parameter `\\X' has no default value and has not been overridden!" 1
+hierarchy -top top
diff --git a/tests/verilog/param_no_default_unbound_5.ys b/tests/verilog/param_no_default_unbound_5.ys
new file mode 100644
index 000000000..30282eba7
--- /dev/null
+++ b/tests/verilog/param_no_default_unbound_5.ys
@@ -0,0 +1,12 @@
+read_verilog -sv <<EOF
+module Example #(
+    parameter X, Y = 2
+);
+endmodule
+module top;
+    Example #(.Y(1)) e();
+endmodule
+EOF
+
+logger -expect error "Parameter `\\X' has no default value and has not been overridden!" 1
+hierarchy -top top
diff --git a/tests/verilog/parameters_across_files.ys b/tests/verilog/parameters_across_files.ys
new file mode 100644
index 000000000..c53e40179
--- /dev/null
+++ b/tests/verilog/parameters_across_files.ys
@@ -0,0 +1,20 @@
+read_verilog -sv <<EOF
+parameter Q = 1;
+EOF
+read_verilog -sv <<EOF
+parameter P = Q;
+module top(
+    output integer out
+);
+    assign out = P;
+    always @*
+        assert (out == 1);
+endmodule
+EOF
+
+hierarchy
+proc
+flatten
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -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
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
diff --git a/tests/verilog/struct_access.sv b/tests/verilog/struct_access.sv
new file mode 100644
index 000000000..f13b8dd51
--- /dev/null
+++ b/tests/verilog/struct_access.sv
@@ -0,0 +1,88 @@
+module top;
+
+    typedef struct packed {
+        logic a;
+        logic signed b;
+        byte c;
+        byte unsigned d;
+        reg [3:0] e;
+        reg signed [3:0] f;
+        struct packed {
+            logic a;
+            logic signed b;
+        } x;
+        struct packed signed {
+            logic a;
+            logic signed b;
+        } y;
+    } S;
+    S s;
+
+    initial begin
+        // test codegen for LHS
+        s.a = '1;
+        s.b = '1;
+        s.c = '1;
+        s.d = '1;
+        s.e = '1;
+        s.f = '1;
+        s.x.a = '1;
+        s.x.b = '1;
+        s.y.a = '1;
+        s.y.b = '1;
+    end
+
+`define CHECK(expr, width, signedness) \
+    case (expr) \
+        1'sb1: \
+            case (expr) \
+                2'sb11: if (!(signedness)) fail = 1; \
+                default: if (signedness) fail = 1; \
+            endcase \
+        default: if (signedness) fail = 1; \
+    endcase \
+    case (expr) \
+        1'b1: if ((width) != 1) fail = 1; \
+        2'b11: if ((width) != 2) fail = 1; \
+        3'b111: if ((width) != 3) fail = 1; \
+        4'b1111: if ((width) != 4) fail = 1; \
+        5'b1111_1: if ((width) != 5) fail = 1; \
+        6'b1111_11: if ((width) != 6) fail = 1; \
+        7'b1111_11: if ((width) != 7) fail = 1; \
+        8'b1111_1111: if ((width) != 8) fail = 1; \
+        9'b1111_1111_1: if ((width) != 9) fail = 1; \
+        default: fail = 1; \
+    endcase \
+    begin \
+        reg [9:0] indirect; \
+        indirect = (expr); \
+        if ((indirect != (expr)) != (signedness)) fail = 1; \
+        indirect = $unsigned(expr); \
+        if ($countones(indirect) != (width)) fail = 1; \
+    end
+
+    initial begin
+        reg fail;
+        fail = 0;
+
+        `CHECK(s.a, 1, 0)
+        `CHECK(s.b, 1, 1)
+        `CHECK(s.c, 8, 1)
+        `CHECK(s.d, 8, 0)
+        `CHECK(s.e, 4, 0)
+        `CHECK(s.f, 4, 1)
+
+        `CHECK(s.x.a, 1, 0)
+        `CHECK(s.x.b, 1, 1)
+        `CHECK(s.y.a, 1, 0)
+        `CHECK(s.y.b, 1, 1)
+
+        // TODO(zachjs): support access to whole sub-structs and unions
+        // `CHECK(s.x, 2, 0)
+        // `CHECK(s.y, 2, 1)
+
+        assert (fail === 0);
+    end
+
+
+endmodule
diff --git a/tests/verilog/struct_access.ys b/tests/verilog/struct_access.ys
new file mode 100644
index 000000000..29d569c01
--- /dev/null
+++ b/tests/verilog/struct_access.ys
@@ -0,0 +1,4 @@
+read_verilog -formal -sv struct_access.sv
+proc
+opt -full
+sat -verify -seq 1 -prove-asserts -show-all
diff --git a/tests/verilog/typedef_across_files.ys b/tests/verilog/typedef_across_files.ys
new file mode 100644
index 000000000..ca9bba736
--- /dev/null
+++ b/tests/verilog/typedef_across_files.ys
@@ -0,0 +1,23 @@
+read_verilog -sv <<EOF
+typedef logic T;
+EOF
+
+read_verilog -sv <<EOF
+typedef T [3:0] S;
+EOF
+
+read_verilog -sv <<EOF
+module top;
+    T t;
+    S s;
+    always @* begin
+        assert ($bits(t) == 1);
+        assert ($bits(s) == 4);
+    end
+endmodule
+EOF
+
+proc
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all
diff --git a/tests/verilog/typedef_legacy_conflict.ys b/tests/verilog/typedef_legacy_conflict.ys
new file mode 100644
index 000000000..8dff4ec5f
--- /dev/null
+++ b/tests/verilog/typedef_legacy_conflict.ys
@@ -0,0 +1,37 @@
+read_verilog -sv <<EOF
+typedef logic T;
+typedef T [3:0] S;
+EOF
+
+read_verilog -sv <<EOF
+module example;
+    // S and T refer to the definitions from the first file
+    T t;
+    S s;
+    always @* begin
+        assert ($bits(t) == 1);
+        assert ($bits(s) == 4);
+    end
+endmodule
+
+typedef byte T;
+typedef T S;
+
+module top;
+    // S and T refer to the most recent overrides
+    T t;
+    S s;
+    always @* begin
+        assert ($bits(t) == 8);
+        assert ($bits(s) == 8);
+    end
+    example e();
+endmodule
+EOF
+
+hierarchy
+proc
+flatten
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all
diff --git a/tests/verilog/unbased_unsized.sv b/tests/verilog/unbased_unsized.sv
new file mode 100644
index 000000000..1d0c5a72c
--- /dev/null
+++ b/tests/verilog/unbased_unsized.sv
@@ -0,0 +1,40 @@
+module pass_through(
+    input [63:0] inp,
+    output [63:0] out
+);
+    assign out = inp;
+endmodule
+
+module top;
+    logic [63:0]
+        o01, o02, o03, o04,
+        o05, o06, o07, o08,
+        o09, o10, o11, o12,
+        o13, o14, o15, o16;
+    assign o01 = '0;
+    assign o02 = '1;
+    assign o03 = 'x;
+    assign o04 = 'z;
+    assign o05 = 3'('0);
+    assign o06 = 3'('1);
+    assign o07 = 3'('x);
+    assign o08 = 3'('z);
+    pass_through pt09('0, o09);
+    pass_through pt10('1, o10);
+    pass_through pt11('x, o11);
+    pass_through pt12('z, o12);
+    always @* begin
+        assert (o01 === {64 {1'b0}});
+        assert (o02 === {64 {1'b1}});
+        assert (o03 === {64 {1'bx}});
+        assert (o04 === {64 {1'bz}});
+        assert (o05 === {61'b0, 3'b000});
+        assert (o06 === {61'b0, 3'b111});
+        assert (o07 === {61'b0, 3'bxxx});
+        assert (o08 === {61'b0, 3'bzzz});
+        assert (o09 === {64 {1'b0}});
+        assert (o10 === {64 {1'b1}});
+        assert (o11 === {64 {1'bx}});
+        assert (o12 === {64 {1'bz}});
+    end
+endmodule
diff --git a/tests/verilog/unbased_unsized.ys b/tests/verilog/unbased_unsized.ys
new file mode 100644
index 000000000..e1bc99c64
--- /dev/null
+++ b/tests/verilog/unbased_unsized.ys
@@ -0,0 +1,7 @@
+read_verilog -sv unbased_unsized.sv
+hierarchy
+proc
+flatten
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all
diff --git a/tests/verilog/unbased_unsized_tern.sv b/tests/verilog/unbased_unsized_tern.sv
new file mode 100644
index 000000000..ad8493394
--- /dev/null
+++ b/tests/verilog/unbased_unsized_tern.sv
@@ -0,0 +1,31 @@
+module pass_through #(
+	parameter WIDTH = 1
+) (
+	input logic [WIDTH-1:0] inp,
+	output logic [WIDTH-1:0] out
+);
+	assign out = inp;
+endmodule
+
+module gate (
+	input logic inp,
+	output logic [63:0]
+		out1, out2, out3, out4
+);
+	pass_through #(40) pt1('1, out1);
+	pass_through #(40) pt2(inp ? '1 : '0, out2);
+	pass_through #(40) pt3(inp ? '1 : 2'b10, out3);
+	pass_through #(40) pt4(inp ? '1 : inp, out4);
+endmodule
+
+module gold (
+	input logic inp,
+	output logic [63:0]
+		out1, out2, out3, out4
+);
+	localparam ONES = 40'hFF_FFFF_FFFF;
+	pass_through #(40) pt1(ONES, out1);
+	pass_through #(40) pt2(inp ? ONES : 0, out2);
+	pass_through #(40) pt3(inp ? ONES : 2'sb10, out3);
+	pass_through #(40) pt4(inp ? ONES : inp, out4);
+endmodule
diff --git a/tests/verilog/unbased_unsized_tern.ys b/tests/verilog/unbased_unsized_tern.ys
new file mode 100644
index 000000000..5ef63c559
--- /dev/null
+++ b/tests/verilog/unbased_unsized_tern.ys
@@ -0,0 +1,6 @@
+read_verilog -sv unbased_unsized_tern.sv
+hierarchy
+proc
+equiv_make gold gate equiv
+equiv_simple
+equiv_status -assert
diff --git a/tests/verilog/unmatched_endif_2.ys b/tests/verilog/unmatched_endif_2.ys
new file mode 100644
index 000000000..2ee084170
--- /dev/null
+++ b/tests/verilog/unmatched_endif_2.ys
@@ -0,0 +1,7 @@
+logger -expect error "Found `endif outside of macro conditional branch!" 1
+read_verilog <<EOF
+`ifndef a
+`else
+`endif
+`endif
+EOF