diff options
Diffstat (limited to 'tests/verilog')
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 |