diff options
Diffstat (limited to 'tests')
52 files changed, 1246 insertions, 14 deletions
diff --git a/tests/arch/xilinx/mux.ys b/tests/arch/xilinx/mux.ys index 1b2788448..c2a23de6d 100644 --- a/tests/arch/xilinx/mux.ys +++ b/tests/arch/xilinx/mux.ys @@ -40,10 +40,11 @@ proc equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd mux16 # Constrain all select calls below inside the top module +select -assert-max 2 t:LUT3 select -assert-max 2 t:LUT4 select -assert-min 4 t:LUT6 select -assert-max 7 t:LUT6 select -assert-max 2 t:MUXF7 dump -select -assert-none t:LUT6 t:LUT4 t:MUXF7 %% t:* %D +select -assert-none t:LUT6 t:LUT4 t:LUT3 t:MUXF7 %% t:* %D diff --git a/tests/arch/xilinx/xilinx_dffopt.ys b/tests/arch/xilinx/xilinx_dffopt.ys index 2c729832e..c09699411 100644 --- a/tests/arch/xilinx/xilinx_dffopt.ys +++ b/tests/arch/xilinx/xilinx_dffopt.ys @@ -223,3 +223,49 @@ select -assert-count 1 t:LUT2 select -assert-none t:FDRSE t:LUT4 t:LUT2 %% t:* %D design -reset + + +read_verilog << EOT + +// FDSE_1, mergeable CE and S, but CE only not worth it. + +module t0 (...); +input wire clk; +input wire [7:0] i; +output wire [7:0] o; + +wire [7:0] tmp ; + +LUT2 #(.INIT(4'h6)) lut0 (.I0(i[0]), .I1(i[1]), .O(tmp[0])); +LUT2 #(.INIT(4'h6)) lut1 (.I0(i[1]), .I1(i[2]), .O(tmp[1])); + +FDSE_1 ff (.D(tmp[0]), .CE(i[7]), .S(tmp[1]), .Q(o[0])); + +endmodule + +EOT + +read_verilog -lib +/xilinx/cells_sim.v +design -save t0 + +equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt +design -load postopt +clean + +cd t0 +select -assert-count 1 t:FDSE_1 +select -assert-count 1 t:LUT5 +select -assert-none t:FDSE_1 t:LUT5 %% t:* %D + +design -load t0 + +equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt -lut4 +design -load postopt +clean + +cd t0 +select -assert-count 1 t:FDSE_1 +select -assert-count 2 t:LUT2 +select -assert-none t:FDSE_1 t:LUT2 %% t:* %D + +design -reset diff --git a/tests/opt/opt_share_bug2538.ys b/tests/opt/opt_share_bug2538.ys new file mode 100644 index 000000000..7261c6695 --- /dev/null +++ b/tests/opt/opt_share_bug2538.ys @@ -0,0 +1,20 @@ +read_verilog <<EOT + +module top(...); + +input [3:0] A; +input S; +output [1:0] Y; + +wire [3:0] A1 = A + 1; +wire [3:0] A2 = A + 2; +assign Y = S ? A1[3:2] : A2[3:2]; + +endmodule + +EOT + +proc +alumacc +equiv_opt -assert opt_share + diff --git a/tests/simple/const_branch_finish.v b/tests/simple/const_branch_finish.v index 8166688e6..f585be87a 100644 --- a/tests/simple/const_branch_finish.v +++ b/tests/simple/const_branch_finish.v @@ -21,9 +21,6 @@ module top; end end generate - begin : unconditional_block - initial `CONSTANT_CHECK - end if (WIDTH == 32) begin : conditional_block initial `CONSTANT_CHECK end diff --git a/tests/simple/const_fold_func.v b/tests/simple/const_fold_func.v new file mode 100644 index 000000000..ee2f12e06 --- /dev/null +++ b/tests/simple/const_fold_func.v @@ -0,0 +1,61 @@ +module top( + input wire [3:0] inp, + output wire [3:0] out1, out2, out3, out4, out5, + output reg [3:0] out6 +); + function automatic [3:0] flip; + input [3:0] inp; + flip = ~inp; + endfunction + + function automatic [3:0] help; + input [3:0] inp; + help = flip(inp); + endfunction + + // while loops are const-eval-only + function automatic [3:0] loop; + input [3:0] inp; + reg [3:0] val; + begin + val = inp; + loop = 1; + while (val != inp) begin + loop = loop * 2; + val = val + 1; + end + end + endfunction + + // not const-eval-only, despite calling a const-eval-only function + function automatic [3:0] help_mul; + input [3:0] inp; + help_mul = inp * loop(2); + endfunction + + // can be elaborated so long as exp is a constant + function automatic [3:0] pow_flip_a; + input [3:0] base, exp; + begin + pow_flip_a = 1; + if (exp > 0) + pow_flip_a = base * pow_flip_a(flip(base), exp - 1); + end + endfunction + + function automatic [3:0] pow_flip_b; + input [3:0] base, exp; + begin + out6[exp] = base & 1; + pow_flip_b = 1; + if (exp > 0) + pow_flip_b = base * pow_flip_b(flip(base), exp - 1); + end + endfunction + + assign out1 = flip(flip(inp)); + assign out2 = help(flip(inp)); + assign out3 = help_mul(inp); + assign out4 = pow_flip_a(flip(inp), 3); + assign out5 = pow_flip_b(2, 2); +endmodule diff --git a/tests/simple/const_func_shadow.v b/tests/simple/const_func_shadow.v new file mode 100644 index 000000000..ca63606d9 --- /dev/null +++ b/tests/simple/const_func_shadow.v @@ -0,0 +1,33 @@ +module top(w, x, y, z); + function [11:0] func; + input reg [2:0] x; + input reg [2:0] y; + begin + x = x * (y + 1); + begin : foo + reg [2:0] y; + y = x + 1; + begin : bar + reg [2:0] x; + x = y + 1; + begin : blah + reg [2:0] y; + y = x + 1; + func[2:0] = y; + end + func[5:3] = x; + end + func[8:6] = y; + end + func[11:9] = x; + end + endfunction + output wire [func(2, 3) - 1:0] w; + output wire [func(1, 3) - 1:0] x; + output wire [func(3, 1) - 1:0] y; + output wire [func(5, 2) - 1:0] z; + assign w = 1'sb1; + assign x = 1'sb1; + assign y = 1'sb1; + assign z = 1'sb1; +endmodule diff --git a/tests/simple/func_block.v b/tests/simple/func_block.v new file mode 100644 index 000000000..be759d1a9 --- /dev/null +++ b/tests/simple/func_block.v @@ -0,0 +1,33 @@ +`default_nettype none + +module top(inp, out1, out2, out3); + input wire [31:0] inp; + + function automatic [31:0] func1; + input [31:0] inp; + reg [31:0] idx; + for (idx = 0; idx < 32; idx = idx + 1) begin : blk + func1[idx] = (idx & 1'b1) ^ inp[idx]; + end + endfunction + + function automatic [31:0] func2; + input [31:0] inp; + reg [31:0] idx; + for (idx = 0; idx < 32; idx = idx + 1) begin : blk + func2[idx] = (idx & 1'b1) ^ inp[idx]; + end + endfunction + + function automatic [31:0] func3; + localparam A = 32 - 1; + parameter B = 1 - 0; + input [31:0] inp; + func3[A:B] = inp[A:B]; + endfunction + + output wire [31:0] out1, out2, out3; + assign out1 = func1(inp); + assign out2 = func2(inp); + assign out3 = func3(inp); +endmodule diff --git a/tests/simple/func_recurse.v b/tests/simple/func_recurse.v new file mode 100644 index 000000000..d61c8cc06 --- /dev/null +++ b/tests/simple/func_recurse.v @@ -0,0 +1,25 @@ +module top( + input wire [3:0] inp, + output wire [3:0] out1, out2 +); + function automatic [3:0] pow_a; + input [3:0] base, exp; + begin + pow_a = 1; + if (exp > 0) + pow_a = base * pow_a(base, exp - 1); + end + endfunction + + function automatic [3:0] pow_b; + input [3:0] base, exp; + begin + pow_b = 1; + if (exp > 0) + pow_b = base * pow_b(base, exp - 1); + end + endfunction + + assign out1 = pow_a(inp, 3); + assign out2 = pow_b(2, 2); +endmodule diff --git a/tests/simple/func_width_scope.v b/tests/simple/func_width_scope.v new file mode 100644 index 000000000..ce81e894e --- /dev/null +++ b/tests/simple/func_width_scope.v @@ -0,0 +1,41 @@ +module top(inp, out1, out2); + input wire signed inp; + + localparam WIDTH_A = 5; + function automatic [WIDTH_A-1:0] func1; + input reg [WIDTH_A-1:0] inp; + func1 = ~inp; + endfunction + wire [func1(0)-1:0] xc; + assign xc = 1'sb1; + wire [WIDTH_A-1:0] xn; + assign xn = func1(inp); + + generate + if (1) begin : blk + localparam WIDTH_A = 6; + function automatic [WIDTH_A-1:0] func2; + input reg [WIDTH_A-1:0] inp; + func2 = ~inp; + endfunction + wire [func2(0)-1:0] yc; + assign yc = 1'sb1; + wire [WIDTH_A-1:0] yn; + assign yn = func2(inp); + + localparam WIDTH_B = 7; + function automatic [WIDTH_B-1:0] func3; + input reg [WIDTH_B-1:0] inp; + func3 = ~inp; + endfunction + wire [func3(0)-1:0] zc; + assign zc = 1'sb1; + wire [WIDTH_B-1:0] zn; + assign zn = func3(inp); + end + endgenerate + + output wire [1023:0] out1, out2; + assign out1 = {xc, 1'b0, blk.yc, 1'b0, blk.zc}; + assign out2 = {xn, 1'b0, blk.yn, 1'b0, blk.zn}; +endmodule diff --git a/tests/simple/genblk_collide.v b/tests/simple/genblk_collide.v new file mode 100644 index 000000000..f42dd2cfc --- /dev/null +++ b/tests/simple/genblk_collide.v @@ -0,0 +1,27 @@ +`default_nettype none + +module top1; + generate + if (1) begin : foo + if (1) begin : bar + wire x; + end + assign bar.x = 1; + wire y; + end + endgenerate +endmodule + +module top2; + genvar i; + generate + if (1) begin : foo + wire x; + for (i = 0; i < 1; i = i + 1) begin : foo + if (1) begin : foo + assign x = 1; + end + end + end + endgenerate +endmodule diff --git a/tests/simple/genblk_dive.v b/tests/simple/genblk_dive.v new file mode 100644 index 000000000..98d0e1f4b --- /dev/null +++ b/tests/simple/genblk_dive.v @@ -0,0 +1,21 @@ +`default_nettype none +module top(output wire x); + generate + if (1) begin : Z + if (1) begin : A + wire x; + if (1) begin : B + wire x; + if (1) begin : C + wire x; + assign B.x = 0; + wire z = A.B.C.x; + end + assign A.x = A.B.C.x; + end + assign B.C.x = B.x; + end + end + endgenerate + assign x = Z.A.x; +endmodule diff --git a/tests/simple/genblk_order.v b/tests/simple/genblk_order.v new file mode 100644 index 000000000..7c3a7a756 --- /dev/null +++ b/tests/simple/genblk_order.v @@ -0,0 +1,18 @@ +`default_nettype none +module top( + output wire out1, + output wire out2 +); + generate + if (1) begin : outer + if (1) begin : foo + wire x = 0; + if (1) begin : foo + wire x = 1; + assign out1 = foo.x; + end + assign out2 = foo.x; + end + end + endgenerate +endmodule diff --git a/tests/simple/genblk_port_shadow.v b/tests/simple/genblk_port_shadow.v new file mode 100644 index 000000000..a04631a20 --- /dev/null +++ b/tests/simple/genblk_port_shadow.v @@ -0,0 +1,10 @@ +module top(x); + generate + if (1) begin : blk + wire x; + assign x = 0; + end + endgenerate + output wire x; + assign x = blk.x; +endmodule diff --git a/tests/simple/generate.v b/tests/simple/generate.v index 12327b36e..445c88ba8 100644 --- a/tests/simple/generate.v +++ b/tests/simple/generate.v @@ -167,7 +167,7 @@ module gen_test7; reg [2:0] out2; wire [2:0] out3; generate - begin : cond + if (1) begin : cond reg [2:0] sub_out1; reg [2:0] sub_out2; wire [2:0] sub_out3; @@ -215,9 +215,9 @@ module gen_test8; wire [1:0] x = 2'b11; generate - begin : A + if (1) begin : A wire [1:0] x; - begin : B + if (1) begin : B wire [1:0] x = 2'b00; `ASSERT(x == 0) `ASSERT(A.x == 2) @@ -228,7 +228,7 @@ module gen_test8; `ASSERT(gen_test8.A.C.x == 1) `ASSERT(gen_test8.A.B.x == 0) end - begin : C + if (1) begin : C wire [1:0] x = 2'b01; `ASSERT(x == 1) `ASSERT(A.x == 2) @@ -260,3 +260,66 @@ module gen_test8; `ASSERT(gen_test8.A.C.x == 1) `ASSERT(gen_test8.A.B.x == 0) endmodule + +// ------------------------------------------ + +module gen_test9; + +// `define VERIFY +`ifdef VERIFY + `define ASSERT(expr) assert property (expr); +`else + `define ASSERT(expr) +`endif + + wire [1:0] w = 2'b11; + generate + begin : A + wire [1:0] x; + begin : B + wire [1:0] y = 2'b00; + `ASSERT(w == 3) + `ASSERT(x == 2) + `ASSERT(y == 0) + `ASSERT(A.x == 2) + `ASSERT(A.C.z == 1) + `ASSERT(A.B.y == 0) + `ASSERT(gen_test9.w == 3) + `ASSERT(gen_test9.A.x == 2) + `ASSERT(gen_test9.A.C.z == 1) + `ASSERT(gen_test9.A.B.y == 0) + end + begin : C + wire [1:0] z = 2'b01; + `ASSERT(w == 3) + `ASSERT(x == 2) + `ASSERT(z == 1) + `ASSERT(A.x == 2) + `ASSERT(A.C.z == 1) + `ASSERT(A.B.y == 0) + `ASSERT(gen_test9.w == 3) + `ASSERT(gen_test9.A.x == 2) + `ASSERT(gen_test9.A.C.z == 1) + `ASSERT(gen_test9.A.B.y == 0) + end + assign x = B.y ^ 2'b11 ^ C.z; + `ASSERT(x == 2) + `ASSERT(A.x == 2) + `ASSERT(A.C.z == 1) + `ASSERT(A.B.y == 0) + `ASSERT(gen_test9.w == 3) + `ASSERT(gen_test9.A.x == 2) + `ASSERT(gen_test9.A.C.z == 1) + `ASSERT(gen_test9.A.B.y == 0) + end + endgenerate + + `ASSERT(w == 3) + `ASSERT(A.x == 2) + `ASSERT(A.C.z == 1) + `ASSERT(A.B.y == 0) + `ASSERT(gen_test9.w == 3) + `ASSERT(gen_test9.A.x == 2) + `ASSERT(gen_test9.A.C.z == 1) + `ASSERT(gen_test9.A.B.y == 0) +endmodule diff --git a/tests/simple/local_loop_var.sv b/tests/simple/local_loop_var.sv new file mode 100644 index 000000000..46b4e5c22 --- /dev/null +++ b/tests/simple/local_loop_var.sv @@ -0,0 +1,11 @@ +module top(out); + output integer out; + initial begin + integer i; + for (i = 0; i < 5; i = i + 1) + if (i == 0) + out = 1; + else + out += 2 ** i; + end +endmodule diff --git a/tests/simple/loop_var_shadow.v b/tests/simple/loop_var_shadow.v new file mode 100644 index 000000000..0222a4493 --- /dev/null +++ b/tests/simple/loop_var_shadow.v @@ -0,0 +1,15 @@ +module top(out); + genvar i; + generate + for (i = 0; i < 2; i = i + 1) begin : loop + localparam j = i + 1; + if (1) begin : blk + localparam i = j + 1; + wire [i:0] x; + assign x = 1'sb1; + end + end + endgenerate + output wire [63:0] out; + assign out = {loop[0].blk.x, loop[1].blk.x}; +endmodule diff --git a/tests/simple/macro_arg_spaces.sv b/tests/simple/macro_arg_spaces.sv new file mode 100644 index 000000000..75c4cd136 --- /dev/null +++ b/tests/simple/macro_arg_spaces.sv @@ -0,0 +1,28 @@ +module top( + input wire [31:0] i, + output wire [31:0] x, y, z +); + +`define BAR(a) a +`define FOO(a = function automatic [31:0] f) a + +`BAR(function automatic [31:0] a); + input [31:0] i; + a = i * 2; +endfunction + +`FOO(); + input [31:0] i; + f = i * 3; +endfunction + +`FOO(function automatic [31:0] b); + input [31:0] i; + b = i * 5; +endfunction + +assign x = a(i); +assign y = f(i); +assign z = b(i); + +endmodule diff --git a/tests/simple/macro_arg_surrounding_spaces.v b/tests/simple/macro_arg_surrounding_spaces.v new file mode 100644 index 000000000..3dbb5ea01 --- /dev/null +++ b/tests/simple/macro_arg_surrounding_spaces.v @@ -0,0 +1,20 @@ +module top( + IDENT_V_, + IDENT_W_, + IDENT_X_, + IDENT_Y_, + IDENT_Z_, + IDENT_A_, + IDENT_B_, + IDENT_C_ +); + `define MACRO(dummy, x) IDENT_``x``_ + output wire IDENT_V_; + output wire `MACRO(_,W); + output wire `MACRO(_, X); + output wire `MACRO(_,Y ); + output wire `MACRO(_, Z ); + output wire `MACRO(_, A); + output wire `MACRO(_,B ); + output wire `MACRO(_, C ); +endmodule diff --git a/tests/simple/named_genblk.v b/tests/simple/named_genblk.v new file mode 100644 index 000000000..b8300fc4d --- /dev/null +++ b/tests/simple/named_genblk.v @@ -0,0 +1,27 @@ +`default_nettype none +module top; + generate + if (1) begin + wire t; + begin : foo + wire x; + end + wire u; + end + begin : bar + wire x; + wire y; + begin : baz + wire x; + wire z; + end + end + endgenerate + assign genblk1.t = 1; + assign genblk1.foo.x = 1; + assign genblk1.u = 1; + assign bar.x = 1; + assign bar.y = 1; + assign bar.baz.x = 1; + assign bar.baz.z = 1; +endmodule diff --git a/tests/simple/nested_genblk_resolve.v b/tests/simple/nested_genblk_resolve.v new file mode 100644 index 000000000..da5593f8a --- /dev/null +++ b/tests/simple/nested_genblk_resolve.v @@ -0,0 +1,14 @@ +`default_nettype none +module top; + generate + if (1) begin + wire x; + genvar i; + for (i = 0; i < 1; i = i + 1) begin + if (1) begin + assign x = 1; + end + end + end + endgenerate +endmodule diff --git a/tests/simple/unnamed_block_decl.sv b/tests/simple/unnamed_block_decl.sv new file mode 100644 index 000000000..e81b457a8 --- /dev/null +++ b/tests/simple/unnamed_block_decl.sv @@ -0,0 +1,17 @@ +module top(z); + output integer z; + initial begin + integer x; + x = 1; + begin + integer y; + y = x + 1; + begin + integer z; + z = y + 1; + y = z + 1; + end + z = y + 1; + end + end +endmodule diff --git a/tests/svtypes/typedef_struct_port.sv b/tests/svtypes/typedef_struct_port.sv new file mode 100644 index 000000000..ecc03bee8 --- /dev/null +++ b/tests/svtypes/typedef_struct_port.sv @@ -0,0 +1,111 @@ +package p; + +typedef struct packed { + byte a; + byte b; +} p_t; + +typedef logic [31:0] l_t; + +endpackage + +module foo1( + input p::p_t p, + output p::p_t o +); + assign o = p; +endmodule + +module foo2(p, o); + input p::p_t p; + output p::p_t o; + assign o = p; +endmodule + +module foo3(input p::l_t p, input p::l_t o); + assign o = p; +endmodule + +module foo4(input logic [15:0] p, input logic [15:0] o); + assign o = p; +endmodule + +module test_parser(a,b,c,d,e,f,g,h,i); +input [7:0] a; // no explicit net declaration - net is unsigned +input [7:0] b; +input signed [7:0] c; +input signed [7:0] d; // no explicit net declaration - net is signed +output [7:0] e; // no explicit net declaration - net is unsigned +output [7:0] f; +output signed [7:0] g; +output signed [7:0] h; // no explicit net declaration - net is signed +output unsigned [7:0] i; +wire signed [7:0] b; // port b inherits signed attribute from net decl. +wire [7:0] c; // net c inherits signed attribute from port +logic signed [7:0] f;// port f inherits signed attribute from logic decl. +logic [7:0] g; // logic g inherits signed attribute from port + + assign a = 8'b10001111; + assign b = 8'b10001111; + assign c = 8'b10001111; + assign d = 8'b10001111; + assign e = 8'b10001111; + assign f = 8'b10001111; + assign g = 8'b10001111; + assign h = 8'b10001111; + assign i = 8'b10001111; + always_comb begin + assert($unsigned(143) == a); + assert($signed(-113) == b); + assert($signed(-113) == c); + assert($signed(-113) == d); + assert($unsigned(143) == e); + assert($unsigned(143) == f); + assert($signed(-113) == g); + assert($signed(-113) == h); + assert($unsigned(143) == i); + end +endmodule + +module top; + p::p_t ps; + assign ps.a = 8'hAA; + assign ps.b = 8'h55; + foo1 foo(.p(ps)); + + p::p_t body; + assign body.a = 8'hBB; + assign body.b = 8'h66; + foo2 foo_b(.p(body)); + + typedef p::l_t local_alias; + + local_alias l_s; + assign l_s = 32'hAAAAAAAA; + foo3 foo_l(.p(l_s)); + + typedef logic [15:0] sl_t; + + sl_t sl_s; + assign sl_s = 16'hBBBB; + foo4 foo_sl(.p(sl_s)); + + typedef sl_t local_alias_st; + + local_alias_st lsl_s; + assign lsl_s = 16'hCCCC; + foo4 foo_lsl(.p(lsl_s)); + + const logic j = 1'b1; + + always_comb begin + assert(8'hAA == ps.a); + assert(8'h55 == ps.b); + assert(8'hBB == body.a); + assert(8'h66 == body.b); + assert(32'hAAAAAAAA == l_s); + assert(16'hBBBB == sl_s); + assert(16'hCCCC == lsl_s); + assert(1'b1 == j); + end +endmodule diff --git a/tests/svtypes/typedef_struct_port.ys b/tests/svtypes/typedef_struct_port.ys new file mode 100644 index 000000000..5b75c3105 --- /dev/null +++ b/tests/svtypes/typedef_struct_port.ys @@ -0,0 +1,6 @@ +read_verilog -sv typedef_struct_port.sv +hierarchy; proc; opt +select -module top +sat -verify -seq 1 -tempinduct -prove-asserts -show-all +select -module test_parser +sat -verify -seq 1 -tempinduct -prove-asserts -show-all diff --git a/tests/various/.gitignore b/tests/various/.gitignore index 12d4e5048..2bb6c7179 100644 --- a/tests/various/.gitignore +++ b/tests/various/.gitignore @@ -4,3 +4,4 @@ /write_gzip.v.gz /run-test.mk /plugin.so +/plugin.so.dSYM diff --git a/tests/various/const_arg_loop.v b/tests/various/const_arg_loop.v index 3bfff4acd..358fb439a 100644 --- a/tests/various/const_arg_loop.v +++ b/tests/various/const_arg_loop.v @@ -14,6 +14,11 @@ module top; end endfunction + function automatic [31:0] pass_through; + input [31:0] inp; + pass_through = inp; + endfunction + function automatic [31:0] operation2; input [4:0] var; input integer num; @@ -39,6 +44,18 @@ module top; end endfunction + function automatic [16:0] operation4; + input [15:0] a; + input b; + operation4 = {a, b}; + endfunction + + function automatic integer operation5; + input x; + integer x; + operation5 = x; + endfunction + wire [31:0] a; assign a = 2; @@ -47,18 +64,30 @@ module top; wire [31:0] x1; assign x1 = operation1(A, a); + wire [31:0] x1b; + assign x1b = operation1(pass_through(A), a); + wire [31:0] x2; assign x2 = operation2(A, a); wire [31:0] x3; assign x3 = operation3(A, a); + wire [16:0] x4; + assign x4 = operation4(a[15:0], 0); + + wire [31:0] x5; + assign x5 = operation5(64); + // `define VERIFY `ifdef VERIFY assert property (a == 2); assert property (A == 3); assert property (x1 == 16); + assert property (x1b == 16); assert property (x2 == 4); assert property (x3 == 16); + assert property (x4 == a << 1); + assert property (x5 == 64); `endif endmodule diff --git a/tests/various/fib.v b/tests/various/fib.v new file mode 100644 index 000000000..986749626 --- /dev/null +++ b/tests/various/fib.v @@ -0,0 +1,65 @@ +module gate( + off, fib0, fib1, fib2, fib3, fib4, fib5, fib6, fib7, fib8, fib9 +); + input wire signed [31:0] off; + + function automatic integer fib( + input integer k + ); + if (k == 0) + fib = 0; + else if (k == 1) + fib = 1; + else + fib = fib(k - 1) + fib(k - 2); + endfunction + + function automatic integer fib_wrap( + input integer k, + output integer o + ); + o = off + fib(k); + endfunction + + output integer fib0; + output integer fib1; + output integer fib2; + output integer fib3; + output integer fib4; + output integer fib5; + output integer fib6; + output integer fib7; + output integer fib8; + output integer fib9; + + initial begin : blk + integer unused; + unused = fib_wrap(0, fib0); + unused = fib_wrap(1, fib1); + unused = fib_wrap(2, fib2); + unused = fib_wrap(3, fib3); + unused = fib_wrap(4, fib4); + unused = fib_wrap(5, fib5); + unused = fib_wrap(6, fib6); + unused = fib_wrap(7, fib7); + unused = fib_wrap(8, fib8); + unused = fib_wrap(9, fib9); + end +endmodule + +module gold( + off, fib0, fib1, fib2, fib3, fib4, fib5, fib6, fib7, fib8, fib9 +); + input wire signed [31:0] off; + + output integer fib0 = off + 0; + output integer fib1 = off + 1; + output integer fib2 = off + 1; + output integer fib3 = off + 2; + output integer fib4 = off + 3; + output integer fib5 = off + 5; + output integer fib6 = off + 8; + output integer fib7 = off + 13; + output integer fib8 = off + 21; + output integer fib9 = off + 34; +endmodule diff --git a/tests/various/fib.ys b/tests/various/fib.ys new file mode 100644 index 000000000..946e0738a --- /dev/null +++ b/tests/various/fib.ys @@ -0,0 +1,6 @@ +read_verilog fib.v +hierarchy +proc +equiv_make gold gate equiv +equiv_simple +equiv_status -assert diff --git a/tests/various/func_port_implied_dir.sv b/tests/various/func_port_implied_dir.sv new file mode 100644 index 000000000..0424f1b46 --- /dev/null +++ b/tests/various/func_port_implied_dir.sv @@ -0,0 +1,23 @@ +module gate(w, x, y, z); + function automatic integer bar( + integer a + ); + bar = 2 ** a; + endfunction + output integer w = bar(4); + + function automatic integer foo( + input integer a, /* implicitly input */ integer b, + output integer c, /* implicitly output */ integer d + ); + c = 42; + d = 51; + foo = a + b + 1; + endfunction + output integer x, y, z; + initial x = foo(1, 2, y, z); +endmodule + +module gold(w, x, y, z); + output integer w = 16, x = 4, y = 42, z = 51; +endmodule diff --git a/tests/various/func_port_implied_dir.ys b/tests/various/func_port_implied_dir.ys new file mode 100644 index 000000000..b5c22a05b --- /dev/null +++ b/tests/various/func_port_implied_dir.ys @@ -0,0 +1,6 @@ +read_verilog -sv func_port_implied_dir.sv +hierarchy +proc +equiv_make gold gate equiv +equiv_simple +equiv_status -assert diff --git a/tests/various/gen_if_null.v b/tests/various/gen_if_null.v index a12ac6288..992bc68b3 100644 --- a/tests/various/gen_if_null.v +++ b/tests/various/gen_if_null.v @@ -1,13 +1,17 @@ -module test(x, y, z); +`default_nettype none +module test; localparam OFF = 0; generate if (OFF) ; - else input x; - if (!OFF) input y; + else wire x; + if (!OFF) wire y; else ; if (OFF) ; else ; if (OFF) ; - input z; + wire z; endgenerate + assign genblk1.x = 0; + assign genblk2.y = 0; + assign z = 0; endmodule diff --git a/tests/various/gen_if_null.ys b/tests/various/gen_if_null.ys index 31dfc444b..0733e3a94 100644 --- a/tests/various/gen_if_null.ys +++ b/tests/various/gen_if_null.ys @@ -1,4 +1,4 @@ read_verilog gen_if_null.v -select -assert-count 1 test/x -select -assert-count 1 test/y +select -assert-count 1 test/genblk1.x +select -assert-count 1 test/genblk2.y select -assert-count 1 test/z diff --git a/tests/various/memory_word_as_index.data b/tests/various/memory_word_as_index.data new file mode 100644 index 000000000..d525c18ee --- /dev/null +++ b/tests/various/memory_word_as_index.data @@ -0,0 +1,4 @@ +00 04 08 0c +10 14 18 1c +20 24 28 2c +30 34 38 3c diff --git a/tests/various/memory_word_as_index.v b/tests/various/memory_word_as_index.v new file mode 100644 index 000000000..a99ea9566 --- /dev/null +++ b/tests/various/memory_word_as_index.v @@ -0,0 +1,21 @@ +`define DATA 64'h492e5c4d7747e032 + +`define GATE(n, expr) \ +module gate``n(sel, out); \ + input wire [3:0] sel; \ + output wire out; \ + reg [63:0] bits; \ + reg [5:0] ptrs[15:0]; \ + initial bits = `DATA; \ + initial $readmemh("memory_word_as_index.data", ptrs); \ + assign out = expr; \ +endmodule + +`GATE(1, bits[ptrs[sel]]) +`GATE(2, bits[ptrs[sel][5:0]]) +`GATE(3, bits[ptrs[sel]+:1]) + +module gold(sel, out); + input wire [3:0] sel; + output wire out = `DATA >> (sel * 4); +endmodule diff --git a/tests/various/memory_word_as_index.ys b/tests/various/memory_word_as_index.ys new file mode 100644 index 000000000..9a2dea40e --- /dev/null +++ b/tests/various/memory_word_as_index.ys @@ -0,0 +1,23 @@ +read_verilog memory_word_as_index.v + +hierarchy +proc +memory +flatten +opt -full + +equiv_make gold gate1 equiv +equiv_simple +equiv_status -assert + +delete equiv + +equiv_make gold gate2 equiv +equiv_simple +equiv_status -assert + +delete equiv + +equiv_make gold gate3 equiv +equiv_simple +equiv_status -assert diff --git a/tests/various/port_sign_extend.v b/tests/various/port_sign_extend.v new file mode 100644 index 000000000..813ceb503 --- /dev/null +++ b/tests/various/port_sign_extend.v @@ -0,0 +1,95 @@ +module GeneratorSigned1(out); + output wire signed out; + assign out = 1; +endmodule + +module GeneratorUnsigned1(out); + output wire out; + assign out = 1; +endmodule + +module GeneratorSigned2(out); + output wire signed [1:0] out; + assign out = 2; +endmodule + +module GeneratorUnsigned2(out); + output wire [1:0] out; + assign out = 2; +endmodule + +module PassThrough(a, b); + input wire [3:0] a; + output wire [3:0] b; + assign b = a; +endmodule + +module act(o1, o2, o3, o4, o5, o6, o7, o8, o9, yay1, nay1, yay2, nay2); + output wire [3:0] o1, o2, o3, o4, o5, o6, o7, o8, o9; + + // unsigned constant + PassThrough pt1(1'b1, o1); + + // unsigned wire + wire tmp2; + assign tmp2 = 1'sb1; + PassThrough pt2(tmp2, o2); + + // signed constant + PassThrough pt3(1'sb1, o3); + + // signed wire + wire signed tmp4; + assign tmp4 = 1'sb1; + PassThrough pt4(tmp4, o4); + + // signed expressions + wire signed [1:0] tmp5a = 2'b11; + wire signed [1:0] tmp5b = 2'b01; + PassThrough pt5(tmp5a ^ tmp5b, o5); + + wire signed [2:0] tmp6a = 3'b100; + wire signed [2:0] tmp6b = 3'b001; + PassThrough pt6(tmp6a ? tmp6a : tmp6b, o6); + + wire signed [2:0] tmp7 = 3'b011; + PassThrough pt7(~tmp7, o7); + + reg signed [2:0] tmp8 [0:0]; + initial tmp8[0] = 3'b101; + PassThrough pt8(tmp8[0], o8); + + wire signed [2:0] tmp9a = 3'b100; + wire signed [1:0] tmp9b = 2'b11; + PassThrough pt9(0 ? tmp9a : tmp9b, o9); + + output wire [2:0] yay1, nay1; + GeneratorSigned1 os1(yay1); + GeneratorUnsigned1 ou1(nay1); + + output wire [2:0] yay2, nay2; + GeneratorSigned2 os2(yay2); + GeneratorUnsigned2 ou2(nay2); +endmodule + +module ref(o1, o2, o3, o4, o5, o6, o7, o8, o9, yay1, nay1, yay2, nay2); + output wire [3:0] o1, o2, o3, o4, o5, o6, o7, o8, o9; + + assign o1 = 4'b0001; + assign o2 = 4'b0001; + assign o3 = 4'b1111; + assign o4 = 4'b1111; + assign o5 = 4'b1110; + assign o6 = 4'b1100; + assign o7 = 4'b1100; + assign o8 = 4'b1101; + assign o9 = 4'b1111; + + output wire [2:0] yay1, nay1; + assign yay1 = 3'b111; + assign nay1 = 3'b001; + + output wire [2:0] yay2, nay2; + assign yay2 = 3'b110; + assign nay2 = 3'b010; +endmodule diff --git a/tests/various/port_sign_extend.ys b/tests/various/port_sign_extend.ys new file mode 100644 index 000000000..6d1adf7f3 --- /dev/null +++ b/tests/various/port_sign_extend.ys @@ -0,0 +1,29 @@ +read_verilog -nomem2reg port_sign_extend.v +hierarchy +flatten +proc +memory +equiv_make ref act equiv +equiv_simple +equiv_status -assert + +delete + +read_verilog -nomem2reg port_sign_extend.v +flatten +proc +memory +equiv_make ref act equiv +equiv_simple +equiv_status -assert + +delete + +read_verilog -nomem2reg port_sign_extend.v +hierarchy +proc +memory +equiv_make ref act equiv +prep -flatten -top equiv +equiv_induct +equiv_status -assert diff --git a/tests/various/rand_const.sv b/tests/various/rand_const.sv new file mode 100644 index 000000000..be00812c0 --- /dev/null +++ b/tests/various/rand_const.sv @@ -0,0 +1,8 @@ +module top; + rand const reg rx; + const reg ry; + rand reg rz; + rand const integer ix; + const integer iy; + rand integer iz; +endmodule diff --git a/tests/various/rand_const.ys b/tests/various/rand_const.ys new file mode 100644 index 000000000..74e43c7cc --- /dev/null +++ b/tests/various/rand_const.ys @@ -0,0 +1 @@ +read_verilog -sv rand_const.sv diff --git a/tests/verilog/atom_type_signedness.ys b/tests/verilog/atom_type_signedness.ys new file mode 100644 index 000000000..22bbe6efc --- /dev/null +++ b/tests/verilog/atom_type_signedness.ys @@ -0,0 +1,19 @@ +read_verilog -dump_ast1 -dump_ast2 -sv <<EOT +module dut(); + +enum integer { uInteger = -10 } a; +enum int { uInt = -11 } b; +enum shortint { uShortInt = -12 } c; +enum byte { uByte = -13 } d; + +always_comb begin + assert(-10 == uInteger); + assert(-11 == uInt); + assert(-12 == uShortInt); + assert(-13 == uByte); +end +endmodule +EOT +hierarchy; proc; opt +select -module dut +sat -verify -seq 1 -tempinduct -prove-asserts -show-all diff --git a/tests/verilog/block_labels.ys b/tests/verilog/block_labels.ys new file mode 100644 index 000000000..e76bcf771 --- /dev/null +++ b/tests/verilog/block_labels.ys @@ -0,0 +1,26 @@ +read_verilog <<EOT +module foo; + + genvar a = 0; + for (a = 0; a < 10; a++) begin : a + end : a +endmodule +EOT +read_verilog <<EOT +module foo2; + + genvar a = 0; + for (a = 0; a < 10; a++) begin : a + end +endmodule +EOT + +logger -expect error "Begin label \(a\) and end label \(b\) don't match\." 1 +read_verilog <<EOT +module foo3; + + genvar a = 0; + for (a = 0; a < 10; a++) begin : a + end : b +endmodule +EOT diff --git a/tests/verilog/bug2493.ys b/tests/verilog/bug2493.ys new file mode 100644 index 000000000..380d2a823 --- /dev/null +++ b/tests/verilog/bug2493.ys @@ -0,0 +1,12 @@ +logger -expect error "Failed to detect width for identifier \\genblk1\.y!" 1 +read_verilog <<EOT +module top1; + wire x; + generate + if (1) begin + mod y(); + assign x = y; + end + endgenerate +endmodule +EOT diff --git a/tests/verilog/bug656.v b/tests/verilog/bug656.v new file mode 100644 index 000000000..068d045fd --- /dev/null +++ b/tests/verilog/bug656.v @@ -0,0 +1,21 @@ +module top #( + parameter WIDTH = 6 +) ( + input [WIDTH-1:0] a_i, + input [WIDTH-1:0] b_i, + output [WIDTH-1:0] z_o +); + genvar g; + generate + for (g = 0; g < WIDTH; g = g + 1) begin + if (g > 2) begin + wire tmp; + assign tmp = a_i[g] || b_i[g]; + assign z_o[g] = tmp; + end + else begin + assign z_o[g] = a_i[g] && b_i[g]; + end + end + endgenerate +endmodule diff --git a/tests/verilog/bug656.ys b/tests/verilog/bug656.ys new file mode 100644 index 000000000..7f367341a --- /dev/null +++ b/tests/verilog/bug656.ys @@ -0,0 +1,13 @@ +read_verilog bug656.v + +select -assert-count 1 top/a_i +select -assert-count 1 top/b_i +select -assert-count 1 top/z_o + +select -assert-none top/genblk1[0].genblk1.tmp +select -assert-none top/genblk1[1].genblk1.tmp +select -assert-none top/genblk1[2].genblk1.tmp + +select -assert-count 1 top/genblk1[3].genblk1.tmp +select -assert-count 1 top/genblk1[4].genblk1.tmp +select -assert-count 1 top/genblk1[5].genblk1.tmp diff --git a/tests/verilog/genblk_case.v b/tests/verilog/genblk_case.v new file mode 100644 index 000000000..081fb09d3 --- /dev/null +++ b/tests/verilog/genblk_case.v @@ -0,0 +1,26 @@ +module top; + parameter YES = 1; + generate + if (YES) wire y; + else wire n; + + if (!YES) wire n; + else wire y; + + case (YES) + 1: wire y; + 0: wire n; + endcase + + case (!YES) + 0: wire y; + 1: wire n; + endcase + + if (YES) wire y; + else wire n; + + if (!YES) wire n; + else wire y; + endgenerate +endmodule diff --git a/tests/verilog/genblk_case.ys b/tests/verilog/genblk_case.ys new file mode 100644 index 000000000..3c1bb51f9 --- /dev/null +++ b/tests/verilog/genblk_case.ys @@ -0,0 +1,15 @@ +read_verilog genblk_case.v + +select -assert-count 0 top/genblk1.n +select -assert-count 0 top/genblk2.n +select -assert-count 0 top/genblk3.n +select -assert-count 0 top/genblk4.n +select -assert-count 0 top/genblk5.n +select -assert-count 0 top/genblk6.n + +select -assert-count 1 top/genblk1.y +select -assert-count 1 top/genblk2.y +select -assert-count 1 top/genblk3.y +select -assert-count 1 top/genblk4.y +select -assert-count 1 top/genblk5.y +select -assert-count 1 top/genblk6.y diff --git a/tests/verilog/genblk_port_decl.ys b/tests/verilog/genblk_port_decl.ys new file mode 100644 index 000000000..589d3d2e1 --- /dev/null +++ b/tests/verilog/genblk_port_decl.ys @@ -0,0 +1,12 @@ +logger -expect error "Cannot declare module port `\\x' within a generate block\." 1 +read_verilog <<EOT +module top(x); + generate + if (1) begin : blk + output wire x; + assign x = 1; + end + endgenerate + output wire x; +endmodule +EOT diff --git a/tests/verilog/hidden_decl.ys b/tests/verilog/hidden_decl.ys new file mode 100644 index 000000000..aed7847dc --- /dev/null +++ b/tests/verilog/hidden_decl.ys @@ -0,0 +1,11 @@ +logger -expect error "Identifier `\\y' is implicitly declared and `default_nettype is set to none" 1 +read_verilog <<EOT +`default_nettype none +module top1; + wire x; + generate + if (1) wire y; + endgenerate + assign x = y; +endmodule +EOT diff --git a/tests/verilog/unnamed_block.ys b/tests/verilog/unnamed_block.ys new file mode 100644 index 000000000..0f209a089 --- /dev/null +++ b/tests/verilog/unnamed_block.ys @@ -0,0 +1,28 @@ +read_verilog <<EOT +module top; + initial begin : blk + integer x; + end +endmodule +EOT + +delete + +read_verilog -sv <<EOT +module top; + initial begin + integer x; + end +endmodule +EOT + +delete + +logger -expect error "Local declaration in unnamed block is only supported in SystemVerilog mode!" 1 +read_verilog <<EOT +module top; + initial begin + integer x; + end +endmodule +EOT diff --git a/tests/verilog/unnamed_genblk.sv b/tests/verilog/unnamed_genblk.sv new file mode 100644 index 000000000..41828b1b0 --- /dev/null +++ b/tests/verilog/unnamed_genblk.sv @@ -0,0 +1,39 @@ +// This test is taken directly from Section 27.6 of IEEE 1800-2017 + +module top; + parameter genblk2 = 0; + genvar i; + + // The following generate block is implicitly named genblk1 + + if (genblk2) logic a; // top.genblk1.a + else logic b; // top.genblk1.b + + // The following generate block is implicitly named genblk02 + // as genblk2 is already a declared identifier + + if (genblk2) logic a; // top.genblk02.a + else logic b; // top.genblk02.b + + // The following generate block would have been named genblk3 + // but is explicitly named g1 + + for (i = 0; i < 1; i = i + 1) begin : g1 // block name + // The following generate block is implicitly named genblk1 + // as the first nested scope inside g1 + if (1) logic a; // top.g1[0].genblk1.a + end + + // The following generate block is implicitly named genblk4 since + // it belongs to the fourth generate construct in scope "top". + // The previous generate block would have been + // named genblk3 if it had not been explicitly named g1 + + for (i = 0; i < 1; i = i + 1) + // The following generate block is implicitly named genblk1 + // as the first nested generate block in genblk4 + if (1) logic a; // top.genblk4[0].genblk1.a + + // The following generate block is implicitly named genblk5 + if (1) logic a; // top.genblk5.a +endmodule diff --git a/tests/verilog/unnamed_genblk.ys b/tests/verilog/unnamed_genblk.ys new file mode 100644 index 000000000..2b9aa9d69 --- /dev/null +++ b/tests/verilog/unnamed_genblk.ys @@ -0,0 +1,8 @@ +read_verilog -sv unnamed_genblk.sv +select -assert-count 0 top/genblk1.a +select -assert-count 1 top/genblk02.b +select -assert-count 0 top/genblk1.a +select -assert-count 1 top/genblk02.b +select -assert-count 1 top/g1[0].genblk1.a +select -assert-count 1 top/genblk4[0].genblk1.a +select -assert-count 1 top/genblk5.a diff --git a/tests/verilog/wire_and_var.sv b/tests/verilog/wire_and_var.sv new file mode 100644 index 000000000..79c7c04c6 --- /dev/null +++ b/tests/verilog/wire_and_var.sv @@ -0,0 +1,33 @@ +`define TEST(kwd) \ + kwd kwd``_1; \ + kwd kwd``_2; \ + initial kwd``_1 = 1; \ + assign kwd``_2 = 1; + +`define TEST_VAR(kwd) \ + var kwd var_``kwd``_1; \ + var kwd var_``kwd``_2; \ + initial var_``kwd``_1 = 1; \ + assign var_``kwd``_2 = 1; + +`define TEST_WIRE(kwd) \ + wire kwd wire_``kwd``_1; \ + wire kwd wire_``kwd``_2; \ + initial wire_``kwd``_1 = 1; \ + assign wire_``kwd``_2 = 1; + +module top; + +`TEST(wire) // wire assigned in a block +`TEST(reg) // reg assigned in a continuous assignment +`TEST(logic) +`TEST(integer) + +`TEST_VAR(reg) // reg assigned in a continuous assignment +`TEST_VAR(logic) +`TEST_VAR(integer) + +`TEST_WIRE(logic) // wire assigned in a block +`TEST_WIRE(integer) // wire assigned in a block + +endmodule diff --git a/tests/verilog/wire_and_var.ys b/tests/verilog/wire_and_var.ys new file mode 100644 index 000000000..9359a9d55 --- /dev/null +++ b/tests/verilog/wire_and_var.ys @@ -0,0 +1,9 @@ +logger -expect warning "wire '\\wire_1' is assigned in a block" 1 +logger -expect warning "reg '\\reg_2' is assigned in a continuous assignment" 1 + +logger -expect warning "reg '\\var_reg_2' is assigned in a continuous assignment" 1 + +logger -expect warning "wire '\\wire_logic_1' is assigned in a block" 1 +logger -expect warning "wire '\\wire_integer_1' is assigned in a block" 1 + +read_verilog -sv wire_and_var.sv |