diff options
Diffstat (limited to 'tests/various')
56 files changed, 1239 insertions, 262 deletions
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/abc9.ys b/tests/various/abc9.ys index a9880c722..e0add714b 100644 --- a/tests/various/abc9.ys +++ b/tests/various/abc9.ys @@ -90,7 +90,7 @@ $_DFF_N_ ff4(.C(clk), .D(1'b1), .Q(z)); endmodule EOT simplemap -equiv_opt abc9 -lut 4 -dff +equiv_opt -assert abc9 -lut 4 -dff design -load postopt cd abc9_test038 select -assert-count 3 t:$_DFF_N_ @@ -99,3 +99,58 @@ clean select -assert-count 2 a:init select -assert-count 1 w:w a:init %i select -assert-count 1 c:ff4 %co c:ff4 %d %a a:init %i + + +# Check that non-dangling ABC9 black-boxes are preserved +design -reset +read_verilog -specify <<EOT +(* abc9_box, blackbox *) +module mux_with_param(input I0, I1, S, output O); +parameter P = 0; +specify + (I0 => O) = P; + (I1 => O) = P; + (S => O) = P; +endspecify +endmodule + +module abc9_test039(output O); + mux_with_param #(.P(1)) m ( + .I0(1'b1), + .I1(1'b1), + .O(O), + .S(1'b0) + ); +endmodule +EOT +abc9 -lut 4 +cd abc9_test039 +select -assert-count 1 t:mux_with_param + + +# Check that dangling ABC9 black-boxes are swept away +design -reset +read_verilog -specify <<EOT +(* abc9_box, blackbox *) +module mux_with_param(input I0, I1, S, output O); +parameter P = 0; +specify + (I0 => O) = P; + (I1 => O) = P; + (S => O) = P; +endspecify +endmodule + +module abc9_test040(output O); + wire w; + mux_with_param #(.P(1)) m ( + .I0(1'b1), + .I1(1'b1), + .O(w), + .S(1'b0) + ); +endmodule +EOT +abc9 -lut 4 +cd abc9_test040 +select -assert-count 0 t:mux_with_param diff --git a/tests/various/async.sh b/tests/various/async.sh index 7c41d6d94..e83935d02 100644 --- a/tests/various/async.sh +++ b/tests/various/async.sh @@ -1,9 +1,9 @@ #!/bin/bash set -ex -../../yosys -q -o async_syn.v -p 'synth; rename uut syn' async.v -../../yosys -q -o async_prp.v -p 'prep; rename uut prp' async.v -../../yosys -q -o async_a2s.v -p 'prep; async2sync; rename uut a2s' async.v -../../yosys -q -o async_ffl.v -p 'prep; clk2fflogic; rename uut ffl' async.v +../../yosys -q -o async_syn.v -r uut -p 'synth; rename uut syn' async.v +../../yosys -q -o async_prp.v -r uut -p 'prep; rename uut prp' async.v +../../yosys -q -o async_a2s.v -r uut -p 'prep; async2sync; rename uut a2s' async.v +../../yosys -q -o async_ffl.v -r uut -p 'prep; clk2fflogic; rename uut ffl' async.v iverilog -o async_sim -DTESTBENCH async.v async_???.v vvp -N async_sim > async.out tail async.out diff --git a/tests/various/blackbox_wb.ys b/tests/various/blackbox_wb.ys new file mode 100644 index 000000000..f9c9bec06 --- /dev/null +++ b/tests/various/blackbox_wb.ys @@ -0,0 +1,14 @@ +read_verilog <<EOT +(* whitebox *) +module box(input a, output q); +assign q = ~a; +endmodule + +module top(input a, output q); +box box_i(.a(a), .q(q)); +endmodule +EOT +select -assert-count 1 =box/t:$not +blackbox =box +select -assert-count 0 =A:whitebox +select -assert-count 0 =box/t:$not diff --git a/tests/various/const_arg_loop.sv b/tests/various/const_arg_loop.sv new file mode 100644 index 000000000..f28d06e68 --- /dev/null +++ b/tests/various/const_arg_loop.sv @@ -0,0 +1,92 @@ +module top; + function automatic [31:0] operation1; + input [4:0] rounds; + input integer num; + integer i; + begin + begin : shadow + integer rounds; + rounds = 0; + end + for (i = 0; i < rounds; i = i + 1) + num = num * 2; + operation1 = num; + end + endfunction + + function automatic [31:0] pass_through; + input [31:0] inp; + pass_through = inp; + endfunction + + function automatic [31:0] operation2; + input [4:0] inp; + input integer num; + begin + inp[0] = inp[0] ^ 1; + operation2 = num * inp; + end + endfunction + + function automatic [31:0] operation3; + input [4:0] rounds; + input integer num; + reg [4:0] rounds; + integer i; + begin + begin : shadow + integer rounds; + rounds = 0; + end + for (i = 0; i < rounds; i = i + 1) + num = num * 2; + operation3 = num; + 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; + + parameter A = 3; + + 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); + + always_comb begin + assert(a == 2); + assert(A == 3); + assert(x1 == 16); + assert(x1b == 16); + assert(x2 == 4); + assert(x3 == 16); + assert(x4 == a << 1); + assert(x5 == 64); + end +endmodule diff --git a/tests/various/const_arg_loop.ys b/tests/various/const_arg_loop.ys new file mode 100644 index 000000000..392532213 --- /dev/null +++ b/tests/various/const_arg_loop.ys @@ -0,0 +1,6 @@ +read_verilog -sv const_arg_loop.sv +hierarchy +proc +opt -full +select -module top +sat -verify -seq 1 -tempinduct -prove-asserts -show-all diff --git a/tests/various/const_func.v b/tests/various/const_func.sv index 76cdc385d..af65f5c73 100644 --- a/tests/various/const_func.v +++ b/tests/various/const_func.sv @@ -53,23 +53,34 @@ module top(out); c1, c2, c3, c4, d1, d2, d3, d4}; -// `define VERIFY -`ifdef VERIFY - assert property (a1 == 0); - assert property (a2 == 0); - assert property (a3 == "BAR"); - assert property (a4 == 0); - assert property (b1 == "FOO"); - assert property (b2 == "FOO"); - assert property (b3 == 0); - assert property (b4 == "HI"); - assert property (c1 == 1); - assert property (c2 == 1); - assert property (c3 == 0); - assert property (c4 == 0); - assert property (d1 == 0); - assert property (d2 == 0); - assert property (d3 == 1); - assert property (d4 == 1); -`endif + function signed [31:0] negate; + input integer inp; + negate = ~inp; + endfunction + parameter W = 10; + parameter X = 3; + localparam signed Y = $floor(W / X); + localparam signed Z = negate($floor(W / X)); + + always_comb begin + assert(a1 == 0); + assert(a2 == 0); + assert(a3 == "BAR"); + assert(a4 == 0); + assert(b1 == "FOO"); + assert(b2 == "FOO"); + assert(b3 == 0); + assert(b4 == "HI"); + assert(c1 == 1); + assert(c2 == 1); + assert(c3 == 0); + assert(c4 == 0); + assert(d1 == 0); + assert(d2 == 0); + assert(d3 == 1); + assert(d4 == 1); + + assert(Y == 3); + assert(Z == ~3); + end endmodule diff --git a/tests/various/const_func.ys b/tests/various/const_func.ys index 5e3c04105..2f60acfe6 100644 --- a/tests/various/const_func.ys +++ b/tests/various/const_func.ys @@ -1 +1,7 @@ -read_verilog const_func.v +read_verilog -sv const_func.sv +hierarchy +proc +flatten +opt -full +select -module top +sat -verify -seq 1 -tempinduct -prove-asserts -show-all diff --git a/tests/various/const_func_block_var.v b/tests/various/const_func_block_var.v new file mode 100644 index 000000000..cb60844ab --- /dev/null +++ b/tests/various/const_func_block_var.v @@ -0,0 +1,26 @@ +module top(out); + function integer operation; + input integer num; + localparam incr = 1; + localparam mult = 1; + begin + operation = 0; + begin : op_i + integer i; + for (i = 0; i * mult < 2; i = i + incr) + begin : op_j + integer j; + localparam other_mult = 2; + for (j = i; j < i * other_mult; j = j + incr) + num = num + incr; + end + num = num * 2; + end + operation = num; + end + endfunction + + localparam res = operation(4); + output wire [31:0] out; + assign out = res; +endmodule diff --git a/tests/various/const_func_block_var.ys b/tests/various/const_func_block_var.ys new file mode 100644 index 000000000..7c2e85c64 --- /dev/null +++ b/tests/various/const_func_block_var.ys @@ -0,0 +1 @@ +read_verilog const_func_block_var.v diff --git a/tests/various/countbits.sv b/tests/various/countbits.sv new file mode 100644 index 000000000..5762217bb --- /dev/null +++ b/tests/various/countbits.sv @@ -0,0 +1,69 @@ +module top; + + assert property ($countbits(15'b011xxxxzzzzzzzz, '0 ) == 1); + assert property ($countbits(15'b011xxxxzzzzzzzz, '1 ) == 2); + assert property ($countbits(15'b011xxxxzzzzzzzz, 'x ) == 4); + assert property ($countbits(15'b011xxxxzzzzzzzz, 'z ) == 8); + assert property ($countbits(15'b011xxxxzzzzzzzz, '0, '1 ) == 3); + assert property ($countbits(15'b011xxxxzzzzzzzz, '1, '1, '0 ) == 3); + assert property ($countbits(15'b011xxxxzzzzzzzz, '0, 'x ) == 5); + assert property ($countbits(15'b011xxxxzzzzzzzz, '0, 'z ) == 9); + assert property ($countbits(15'bz1x10xzxzzxzzzz, '0, 'z ) == 9); + assert property ($countbits(15'b011xxxxzzzzzzzz, 'x, 'z ) == 12); + assert property ($countbits(15'b011xxxxzzzzzzzz, '1, 'z ) == 10); + assert property ($countbits(15'b011xxxxzzzzzzzz, '1, 'x, 'z ) == 14); + assert property ($countbits(15'b011xxxxzzzzzzzz, '1, 'x, 'z, '0) == 15); + + assert property ($countbits(0, '0) == 32); // test integers + assert property ($countbits(0, '1) == 0); + assert property ($countbits(80'b0, '0) == 80); // test something bigger than integer + assert property ($countbits(80'bx0, 'x) == 79); + + always_comb begin + logic one; + logic [1:0] two; + logic [3:0] four; + + // Make sure that the width of the whole expression doesn't affect the width of the shift + // operations inside the function. + one = $countbits(3'b100, '1) & 1'b1; + two = $countbits(3'b111, '1) & 2'b11; + four = $countbits(3'b111, '1) & 4'b1111; + + assert (one == 1); + assert (two == 3); + assert (four == 3); + end + + assert property ($countones(8'h00) == 0); + assert property ($countones(8'hff) == 8); + assert property ($countones(8'ha5) == 4); + assert property ($countones(8'h13) == 3); + + logic test1 = 1'b1; + logic [4:0] test5 = 5'b10101; + + assert property ($countones(test1) == 1); + assert property ($countones(test5) == 3); + + assert property ($isunknown(8'h00) == 0); + assert property ($isunknown(8'hff) == 0); + assert property ($isunknown(8'hx0) == 1); + assert property ($isunknown(8'h1z) == 1); + assert property ($isunknown(8'hxz) == 1); + + assert property ($onehot(8'h00) == 0); + assert property ($onehot(8'hff) == 0); + assert property ($onehot(8'h01) == 1); + assert property ($onehot(8'h80) == 1); + assert property ($onehot(8'h81) == 0); + assert property ($onehot(8'h20) == 1); + + assert property ($onehot0(8'h00) == 1); + assert property ($onehot0(8'hff) == 0); + assert property ($onehot0(8'h01) == 1); + assert property ($onehot0(8'h80) == 1); + assert property ($onehot0(8'h81) == 0); + assert property ($onehot0(8'h20) == 1); + +endmodule diff --git a/tests/various/countbits.ys b/tests/various/countbits.ys new file mode 100644 index 000000000..a556f7c5d --- /dev/null +++ b/tests/various/countbits.ys @@ -0,0 +1,7 @@ +read_verilog -sv countbits.sv +hierarchy +proc +flatten +opt -full +select -module top +sat -verify -seq 1 -tempinduct -prove-asserts -show-all diff --git a/tests/various/dynamic_part_select.ys b/tests/various/dynamic_part_select.ys index abc1daad6..2dc061e89 100644 --- a/tests/various/dynamic_part_select.ys +++ b/tests/various/dynamic_part_select.ys @@ -21,18 +21,18 @@ read_verilog ./dynamic_part_select/multiple_blocking.v proc rename -top gold design -stash gold - + read_verilog ./dynamic_part_select/multiple_blocking_gate.v proc rename -top gate design -stash gate - + design -copy-from gold -as gold gold design -copy-from gate -as gate gate miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv - + ### Non-blocking to the same output register ### design -reset read_verilog ./dynamic_part_select/nonblocking.v @@ -44,13 +44,13 @@ read_verilog ./dynamic_part_select/nonblocking_gate.v proc rename -top gate design -stash gate - + design -copy-from gold -as gold gold design -copy-from gate -as gate gate miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv - + ### For-loop select, one dynamic input design -reset read_verilog ./dynamic_part_select/forloop_select.v @@ -62,13 +62,13 @@ read_verilog ./dynamic_part_select/forloop_select_gate.v proc rename -top gate design -stash gate - + design -copy-from gold -as gold gold design -copy-from gate -as gate gate miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv - + #### Double loop (part-select, reset) ### design -reset read_verilog ./dynamic_part_select/reset_test.v @@ -83,10 +83,10 @@ design -stash gate design -copy-from gold -as gold gold design -copy-from gate -as gate gate - + miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv - + ### Reversed part-select case ### design -reset read_verilog ./dynamic_part_select/reversed.v @@ -101,6 +101,62 @@ design -stash gate design -copy-from gold -as gold gold design -copy-from gate -as gate gate - + +miter -equiv -make_assert -make_outcmp -flatten gold gate equiv +sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv + +### Latches +## Issue 1990 +design -reset +read_verilog ./dynamic_part_select/latch_1990.v +hierarchy -top latch_1990; prep; async2sync +rename -top gold +design -stash gold + +read_verilog ./dynamic_part_select/latch_1990_gate.v +hierarchy -top latch_1990_gate; prep +rename -top gate +design -stash gate + +design -copy-from gold -as gold gold +design -copy-from gate -as gate gate + +miter -equiv -make_assert -make_outcmp -flatten gold gate equiv +sat -prove-asserts -show-public -verify -set-init-zero equiv + +### +## Part select with obvious latch, expected to fail due comparison with old shift&mask AST transformation +design -reset +read_verilog ./dynamic_part_select/latch_002.v +hierarchy -top latch_002; prep; async2sync +rename -top gold +design -stash gold + +read_verilog ./dynamic_part_select/latch_002_gate.v +hierarchy -top latch_002_gate; prep; async2sync +rename -top gate +design -stash gate + +design -copy-from gold -as gold gold +design -copy-from gate -as gate gate + +miter -equiv -make_assert -make_outcmp -flatten gold gate equiv +sat -prove-asserts -seq 10 -show-public -falsify -set-init-zero equiv + +## Part select + latch, with no shift&mask +design -reset +read_verilog ./dynamic_part_select/latch_002.v +hierarchy -top latch_002; prep; async2sync +rename -top gold +design -stash gold + +read_verilog ./dynamic_part_select/latch_002_gate_good.v +hierarchy -top latch_002_gate; prep; async2sync +rename -top gate +design -stash gate + +design -copy-from gold -as gold gold +design -copy-from gate -as gate gate + miter -equiv -make_assert -make_outcmp -flatten gold gate equiv sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv diff --git a/tests/various/dynamic_part_select/forloop_select.v b/tests/various/dynamic_part_select/forloop_select.v index 8260f3186..926fb3133 100644 --- a/tests/various/dynamic_part_select/forloop_select.v +++ b/tests/various/dynamic_part_select/forloop_select.v @@ -1,13 +1,14 @@ +`default_nettype none module forloop_select #(parameter WIDTH=16, SELW=4, CTRLW=$clog2(WIDTH), DINW=2**SELW) - (input clk, - input [CTRLW-1:0] ctrl, - input [DINW-1:0] din, - input en, + (input wire clk, + input wire [CTRLW-1:0] ctrl, + input wire [DINW-1:0] din, + input wire en, output reg [WIDTH-1:0] dout); - - reg [SELW:0] sel; + + reg [SELW:0] sel; localparam SLICE = WIDTH/(SELW**2); - + always @(posedge clk) begin if (en) begin @@ -16,4 +17,3 @@ module forloop_select #(parameter WIDTH=16, SELW=4, CTRLW=$clog2(WIDTH), DINW=2* end end endmodule - diff --git a/tests/various/dynamic_part_select/forloop_select_gate.v b/tests/various/dynamic_part_select/forloop_select_gate.v index 71ae88537..1a5fffdc7 100644 --- a/tests/various/dynamic_part_select/forloop_select_gate.v +++ b/tests/various/dynamic_part_select/forloop_select_gate.v @@ -1,8 +1,9 @@ +`default_nettype none module forloop_select_gate (clk, ctrl, din, en, dout); - input clk; - input [3:0] ctrl; - input [15:0] din; - input en; + input wire clk; + input wire [3:0] ctrl; + input wire [15:0] din; + input wire en; output reg [15:0] dout; reg [4:0] sel; always @(posedge clk) diff --git a/tests/various/dynamic_part_select/latch_002.v b/tests/various/dynamic_part_select/latch_002.v new file mode 100644 index 000000000..7617d6a72 --- /dev/null +++ b/tests/various/dynamic_part_select/latch_002.v @@ -0,0 +1,13 @@ +`default_nettype none +module latch_002 + (dword, sel, st, vect); + output reg [63:0] dword; + input wire [7:0] vect; + input wire [7:0] sel; + input wire st; + + always @(*) begin + if (st) + dword[8*sel +:8] <= vect[7:0]; + end +endmodule // latch_002 diff --git a/tests/various/dynamic_part_select/latch_002_gate.v b/tests/various/dynamic_part_select/latch_002_gate.v new file mode 100644 index 000000000..4acf129c6 --- /dev/null +++ b/tests/various/dynamic_part_select/latch_002_gate.v @@ -0,0 +1,18 @@ +`default_nettype none +module latch_002_gate(dword, vect, sel, st); + output reg [63:0] dword; + input wire [7:0] vect; + input wire [7:0] sel; + input wire st; + reg [63:0] mask; + reg [63:0] data; + always @* + case (|(st)) + 1'b 1: + begin + mask = (8'b 11111111)<<((((8)*(sel)))+(0)); + data = ((8'b 11111111)&(vect[7:0]))<<((((8)*(sel)))+(0)); + dword <= ((dword)&(~(mask)))|(data); + end + endcase +endmodule diff --git a/tests/various/dynamic_part_select/latch_002_gate_good.v b/tests/various/dynamic_part_select/latch_002_gate_good.v new file mode 100644 index 000000000..809c74fc9 --- /dev/null +++ b/tests/various/dynamic_part_select/latch_002_gate_good.v @@ -0,0 +1,141 @@ +`default_nettype none +module latch_002_gate (dword, vect, sel, st); + output reg [63:0] dword; + input wire [7:0] vect; + input wire [7:0] sel; + input st; + always @* + case (|(st)) + 1'b 1: + case ((((8)*(sel)))+(0)) + 0: + dword[7:0] <= vect[7:0]; + 1: + dword[8:1] <= vect[7:0]; + 2: + dword[9:2] <= vect[7:0]; + 3: + dword[10:3] <= vect[7:0]; + 4: + dword[11:4] <= vect[7:0]; + 5: + dword[12:5] <= vect[7:0]; + 6: + dword[13:6] <= vect[7:0]; + 7: + dword[14:7] <= vect[7:0]; + 8: + dword[15:8] <= vect[7:0]; + 9: + dword[16:9] <= vect[7:0]; + 10: + dword[17:10] <= vect[7:0]; + 11: + dword[18:11] <= vect[7:0]; + 12: + dword[19:12] <= vect[7:0]; + 13: + dword[20:13] <= vect[7:0]; + 14: + dword[21:14] <= vect[7:0]; + 15: + dword[22:15] <= vect[7:0]; + 16: + dword[23:16] <= vect[7:0]; + 17: + dword[24:17] <= vect[7:0]; + 18: + dword[25:18] <= vect[7:0]; + 19: + dword[26:19] <= vect[7:0]; + 20: + dword[27:20] <= vect[7:0]; + 21: + dword[28:21] <= vect[7:0]; + 22: + dword[29:22] <= vect[7:0]; + 23: + dword[30:23] <= vect[7:0]; + 24: + dword[31:24] <= vect[7:0]; + 25: + dword[32:25] <= vect[7:0]; + 26: + dword[33:26] <= vect[7:0]; + 27: + dword[34:27] <= vect[7:0]; + 28: + dword[35:28] <= vect[7:0]; + 29: + dword[36:29] <= vect[7:0]; + 30: + dword[37:30] <= vect[7:0]; + 31: + dword[38:31] <= vect[7:0]; + 32: + dword[39:32] <= vect[7:0]; + 33: + dword[40:33] <= vect[7:0]; + 34: + dword[41:34] <= vect[7:0]; + 35: + dword[42:35] <= vect[7:0]; + 36: + dword[43:36] <= vect[7:0]; + 37: + dword[44:37] <= vect[7:0]; + 38: + dword[45:38] <= vect[7:0]; + 39: + dword[46:39] <= vect[7:0]; + 40: + dword[47:40] <= vect[7:0]; + 41: + dword[48:41] <= vect[7:0]; + 42: + dword[49:42] <= vect[7:0]; + 43: + dword[50:43] <= vect[7:0]; + 44: + dword[51:44] <= vect[7:0]; + 45: + dword[52:45] <= vect[7:0]; + 46: + dword[53:46] <= vect[7:0]; + 47: + dword[54:47] <= vect[7:0]; + 48: + dword[55:48] <= vect[7:0]; + 49: + dword[56:49] <= vect[7:0]; + 50: + dword[57:50] <= vect[7:0]; + 51: + dword[58:51] <= vect[7:0]; + 52: + dword[59:52] <= vect[7:0]; + 53: + dword[60:53] <= vect[7:0]; + 54: + dword[61:54] <= vect[7:0]; + 55: + dword[62:55] <= vect[7:0]; + 56: + dword[63:56] <= vect[7:0]; + 57: + dword[63:57] <= vect[7:0]; + 58: + dword[63:58] <= vect[7:0]; + 59: + dword[63:59] <= vect[7:0]; + 60: + dword[63:60] <= vect[7:0]; + 61: + dword[63:61] <= vect[7:0]; + 62: + dword[63:62] <= vect[7:0]; + 63: + dword[63:63] <= vect[7:0]; + endcase + endcase +endmodule diff --git a/tests/various/dynamic_part_select/latch_1990.v b/tests/various/dynamic_part_select/latch_1990.v new file mode 100644 index 000000000..864c05244 --- /dev/null +++ b/tests/various/dynamic_part_select/latch_1990.v @@ -0,0 +1,12 @@ +module latch_1990 #( + parameter BUG = 1 +) ( + (* nowrshmsk = !BUG *) + output reg [1:0] x +); + wire z = 0; + integer i; + always @* + for (i = 0; i < 2; i=i+1) + x[z^i] = z^i; +endmodule diff --git a/tests/various/dynamic_part_select/latch_1990_gate.v b/tests/various/dynamic_part_select/latch_1990_gate.v new file mode 100644 index 000000000..a46183f23 --- /dev/null +++ b/tests/various/dynamic_part_select/latch_1990_gate.v @@ -0,0 +1,6 @@ +`default_nettype none +module latch_1990_gate + (output wire [1:0] x); + assign x = 2'b10; +endmodule // latch_1990_gate + diff --git a/tests/various/dynamic_part_select/multiple_blocking.v b/tests/various/dynamic_part_select/multiple_blocking.v index 2858f7741..3bb249a76 100644 --- a/tests/various/dynamic_part_select/multiple_blocking.v +++ b/tests/various/dynamic_part_select/multiple_blocking.v @@ -1,8 +1,9 @@ +`default_nettype none module multiple_blocking #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SELW) - (input clk, - input [CTRLW-1:0] ctrl, - input [DINW-1:0] din, - input [SELW-1:0] sel, + (input wire clk, + input wire [CTRLW-1:0] ctrl, + input wire [DINW-1:0] din, + input wire [SELW-1:0] sel, output reg [WIDTH-1:0] dout); localparam SLICE = WIDTH/(SELW**2); diff --git a/tests/various/dynamic_part_select/multiple_blocking_gate.v b/tests/various/dynamic_part_select/multiple_blocking_gate.v index 073b559dc..840918876 100644 --- a/tests/various/dynamic_part_select/multiple_blocking_gate.v +++ b/tests/various/dynamic_part_select/multiple_blocking_gate.v @@ -1,8 +1,9 @@ +`default_nettype none module multiple_blocking_gate (clk, ctrl, din, sel, dout); - input clk; - input [4:0] ctrl; - input [1:0] din; - input [0:0] sel; + input wire clk; + input wire [4:0] ctrl; + input wire [1:0] din; + input wire [0:0] sel; output reg [31:0] dout; reg [5:0] a; reg [0:0] b; diff --git a/tests/various/dynamic_part_select/nonblocking.v b/tests/various/dynamic_part_select/nonblocking.v index 0949b31a9..20f857cf9 100644 --- a/tests/various/dynamic_part_select/nonblocking.v +++ b/tests/various/dynamic_part_select/nonblocking.v @@ -1,8 +1,9 @@ +`default_nettype none module nonblocking #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SELW) - (input clk, - input [CTRLW-1:0] ctrl, - input [DINW-1:0] din, - input [SELW-1:0] sel, + (input wire clk, + input wire [CTRLW-1:0] ctrl, + input wire [DINW-1:0] din, + input wire [SELW-1:0] sel, output reg [WIDTH-1:0] dout); localparam SLICE = WIDTH/(SELW**2); diff --git a/tests/various/dynamic_part_select/nonblocking_gate.v b/tests/various/dynamic_part_select/nonblocking_gate.v index ed1ee2776..212d44609 100644 --- a/tests/various/dynamic_part_select/nonblocking_gate.v +++ b/tests/various/dynamic_part_select/nonblocking_gate.v @@ -1,8 +1,9 @@ +`default_nettype none module nonblocking_gate (clk, ctrl, din, sel, dout); - input clk; - input [4:0] ctrl; - input [1:0] din; - input [0:0] sel; + input wire clk; + input wire [4:0] ctrl; + input wire [1:0] din; + input wire [0:0] sel; output reg [31:0] dout; always @(posedge clk) begin diff --git a/tests/various/dynamic_part_select/original.v b/tests/various/dynamic_part_select/original.v index f7dfed1a1..41310a215 100644 --- a/tests/various/dynamic_part_select/original.v +++ b/tests/various/dynamic_part_select/original.v @@ -1,8 +1,9 @@ +`default_nettype none module original #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SELW) - (input clk, - input [CTRLW-1:0] ctrl, - input [DINW-1:0] din, - input [SELW-1:0] sel, + (input wire clk, + input wire [CTRLW-1:0] ctrl, + input wire [DINW-1:0] din, + input wire [SELW-1:0] sel, output reg [WIDTH-1:0] dout); localparam SLICE = WIDTH/(SELW**2); always @(posedge clk) diff --git a/tests/various/dynamic_part_select/original_gate.v b/tests/various/dynamic_part_select/original_gate.v index 22093bf63..963b4228c 100644 --- a/tests/various/dynamic_part_select/original_gate.v +++ b/tests/various/dynamic_part_select/original_gate.v @@ -1,8 +1,9 @@ +`default_nettype none module original_gate (clk, ctrl, din, sel, dout); - input clk; - input [4:0] ctrl; - input [1:0] din; - input [0:0] sel; + input wire clk; + input wire [4:0] ctrl; + input wire [1:0] din; + input wire [0:0] sel; output reg [31:0] dout; always @(posedge clk) case (({(ctrl)*(sel)})+(0)) diff --git a/tests/various/dynamic_part_select/reset_test.v b/tests/various/dynamic_part_select/reset_test.v index 29355aafb..1bb9379f2 100644 --- a/tests/various/dynamic_part_select/reset_test.v +++ b/tests/various/dynamic_part_select/reset_test.v @@ -1,8 +1,10 @@ +`default_nettype none module reset_test #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SELW) - (input clk, - input [CTRLW-1:0] ctrl, - input [DINW-1:0] din, - input [SELW-1:0] sel, + (input wire clk, + input wire reset, + input wire [CTRLW-1:0] ctrl, + input wire [DINW-1:0] din, + input wire [SELW-1:0] sel, output reg [WIDTH-1:0] dout); reg [SELW:0] i; @@ -16,8 +18,6 @@ module reset_test #(parameter WIDTH=32, SELW=1, CTRLW=$clog2(WIDTH), DINW=2**SE dout[i*rval+:SLICE] <= 32'hDEAD; end end - //else begin dout[ctrl*sel+:SLICE] <= din; - //end end endmodule diff --git a/tests/various/dynamic_part_select/reset_test_gate.v b/tests/various/dynamic_part_select/reset_test_gate.v index 96dff4135..4ae76c4f7 100644 --- a/tests/various/dynamic_part_select/reset_test_gate.v +++ b/tests/various/dynamic_part_select/reset_test_gate.v @@ -1,8 +1,10 @@ -module reset_test_gate (clk, ctrl, din, sel, dout); - input clk; - input [4:0] ctrl; - input [1:0] din; - input [0:0] sel; +`default_nettype none +module reset_test_gate (clk, reset, ctrl, din, sel, dout); + input wire clk; + input wire reset; + input wire [4:0] ctrl; + input wire [1:0] din; + input wire [0:0] sel; output reg [31:0] dout; reg [1:0] i; wire [0:0] rval; diff --git a/tests/various/dynamic_part_select/reversed.v b/tests/various/dynamic_part_select/reversed.v index 8b114ac77..0268fa6bb 100644 --- a/tests/various/dynamic_part_select/reversed.v +++ b/tests/various/dynamic_part_select/reversed.v @@ -1,8 +1,9 @@ +`default_nettype none module reversed #(parameter WIDTH=32, SELW=4, CTRLW=$clog2(WIDTH), DINW=2**SELW) - (input clk, - input [CTRLW-1:0] ctrl, - input [DINW-1:0] din, - input [SELW-1:0] sel, + (input wire clk, + input wire [CTRLW-1:0] ctrl, + input wire [DINW-1:0] din, + input wire [SELW-1:0] sel, output reg [WIDTH-1:0] dout); localparam SLICE = WIDTH/(SELW**2); diff --git a/tests/various/dynamic_part_select/reversed_gate.v b/tests/various/dynamic_part_select/reversed_gate.v index 9349d45ee..5ffdcb4d7 100644 --- a/tests/various/dynamic_part_select/reversed_gate.v +++ b/tests/various/dynamic_part_select/reversed_gate.v @@ -1,8 +1,9 @@ +`default_nettype none module reversed_gate (clk, ctrl, din, sel, dout); - input clk; - input [4:0] ctrl; - input [15:0] din; - input [3:0] sel; + input wire clk; + input wire [4:0] ctrl; + input wire [15:0] din; + input wire [3:0] sel; output reg [31:0] dout; always @(posedge clk) case ((({(32)-((ctrl)*(sel))})+(1))-(2)) diff --git a/tests/various/equiv_opt_undef.ys b/tests/various/equiv_opt_undef.ys new file mode 100644 index 000000000..5d2c60d0a --- /dev/null +++ b/tests/various/equiv_opt_undef.ys @@ -0,0 +1,35 @@ +read_ilang << EOT + +module \top + wire $a + wire $b + wire input 1 \D + wire input 2 \EN + wire output 3 \Q + cell $mux $x + parameter \WIDTH 1 + connect \A \Q + connect \B \D + connect \S \EN + connect \Y $a + end + cell $ff $y + parameter \WIDTH 1 + connect \D $a + connect \Q $b + end + cell $and $z + parameter \A_SIGNED 0 + parameter \A_WIDTH 1 + parameter \B_SIGNED 0 + parameter \B_WIDTH 1 + parameter \Y_WIDTH 1 + connect \A $b + connect \B 1'x + connect \Y \Q + end +end + +EOT + +equiv_opt -assert -undef ls 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/fib_tern.v b/tests/various/fib_tern.v new file mode 100644 index 000000000..fefde74ce --- /dev/null +++ b/tests/various/fib_tern.v @@ -0,0 +1,70 @@ +module gate( + off, fib0, fib1, fib2, fib3, fib4, fib5, fib6, fib7, fib8, fib9 +); + input wire signed [31:0] off; + + function automatic blah( + input x + ); + blah = x; + endfunction + + function automatic integer fib( + input integer k + ); + fib = k == 0 + ? 0 + : k == 1 + ? 1 + : 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_tern.ys b/tests/various/fib_tern.ys new file mode 100644 index 000000000..e5bf186e1 --- /dev/null +++ b/tests/various/fib_tern.ys @@ -0,0 +1,6 @@ +read_verilog fib_tern.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/integer_range_bad_syntax.ys b/tests/various/integer_range_bad_syntax.ys new file mode 100644 index 000000000..4f427211f --- /dev/null +++ b/tests/various/integer_range_bad_syntax.ys @@ -0,0 +1,6 @@ +logger -expect error "syntax error, unexpected" 1 +read_verilog -sv <<EOT +module test_integer_range(); +parameter integer [31:0] a = 0; +endmodule +EOT diff --git a/tests/various/integer_real_bad_syntax.ys b/tests/various/integer_real_bad_syntax.ys new file mode 100644 index 000000000..942d8de77 --- /dev/null +++ b/tests/various/integer_real_bad_syntax.ys @@ -0,0 +1,6 @@ +logger -expect error "syntax error, unexpected TOK_REAL" 1 +read_verilog -sv <<EOT +module test_integer_real(); +parameter integer real a = 0; +endmodule +EOT diff --git a/tests/various/logger_fail.sh b/tests/various/logger_fail.sh new file mode 100755 index 000000000..19b650007 --- /dev/null +++ b/tests/various/logger_fail.sh @@ -0,0 +1,42 @@ +#!/bin/bash + +fail() { + echo "$1" >&2 + exit 1 +} + +runTest() { + desc="$1" + want="$2" + shift 2 + echo "running '$desc' with args $@" + output=`../../yosys -q "$@" 2>&1` + if [ $? -ne 1 ]; then + fail "exit code for '$desc' was not 1" + fi + if [ "$output" != "$want" ]; then + fail "output for '$desc' did not match" + fi +} + +unmet() { + kind=$1 + runTest "unmet $kind" \ + "ERROR: Expected $kind pattern 'foobar' not found !" \ + -p "logger -expect $kind \"foobar\" 1" +} + +unmet log +unmet warning +unmet error + +runTest "too many logs" \ + "ERROR: Expected log pattern 'statistics' found 2 time(s), instead of 1 time(s) !" \ + -p "logger -expect log \"statistics\" 1" -p stat -p stat + +runTest "too many warnings" \ + "Warning: Found log message matching -W regex: +Printing statistics. +ERROR: Expected warning pattern 'statistics' found 2 time(s), instead of 1 time(s) !" \ + -p "logger -warn \"Printing statistics\"" \ + -p "logger -expect warning \"statistics\" 1" -p stat -p stat diff --git a/tests/various/logic_param_simple.ys b/tests/various/logic_param_simple.ys new file mode 100644 index 000000000..968564080 --- /dev/null +++ b/tests/various/logic_param_simple.ys @@ -0,0 +1,9 @@ +read_verilog -sv <<EOT +module test_logic_param(); +parameter logic a = 0; +parameter logic [31:0] e = 0; +parameter logic signed b = 0; +parameter logic unsigned c = 0; +parameter logic unsigned [31:0] d = 0; +endmodule +EOT 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/muxpack.v b/tests/various/muxpack.v index 33ece1f16..752f9ba48 100644 --- a/tests/various/muxpack.v +++ b/tests/various/muxpack.v @@ -154,7 +154,7 @@ always @* o <= i[4*W+:W]; endmodule -module cliffordwolf_nonexclusive_select ( +module clairexen_nonexclusive_select ( input wire x, y, z, input wire a, b, c, d, output reg o @@ -167,7 +167,7 @@ module cliffordwolf_nonexclusive_select ( end endmodule -module cliffordwolf_freduce ( +module clairexen_freduce ( input wire [1:0] s, input wire a, b, c, d, output reg [3:0] o diff --git a/tests/various/muxpack.ys b/tests/various/muxpack.ys index 3e90419af..d73fc44b4 100644 --- a/tests/various/muxpack.ys +++ b/tests/various/muxpack.ys @@ -167,7 +167,7 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -show-ports miter design -load read -hierarchy -top cliffordwolf_nonexclusive_select +hierarchy -top clairexen_nonexclusive_select prep design -save gold muxpack @@ -182,7 +182,7 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -show-ports miter #design -load read -#hierarchy -top cliffordwolf_freduce +#hierarchy -top clairexen_freduce #prep #design -save gold #proc; opt; freduce; opt diff --git a/tests/various/param_struct.ys b/tests/various/param_struct.ys new file mode 100644 index 000000000..6d7a7c6ad --- /dev/null +++ b/tests/various/param_struct.ys @@ -0,0 +1,51 @@ +read_verilog -sv << EOF +package p; +typedef struct packed { + logic a; + logic b; +} struct_t; + +typedef struct packed { + struct_t g; + logic [2:0] h; +} nested_struct_t; + +typedef union packed { + logic [4:0] x; +} nested_union_t; + +parameter struct_t c = {1'b1, 1'b0}; +parameter nested_struct_t x = {{1'b1, 1'b0}, 1'b1, 1'b1, 1'b1}; +endpackage + +module dut (); +parameter p::struct_t d = p::c; +parameter p::nested_struct_t i = p::x; + +parameter p::nested_union_t u = {5'b11001}; + +localparam e = d.a; +localparam f = d.b; + +localparam j = i.g.a; +localparam k = i.g.b; +localparam l = i.h; +localparam m = i.g; + +localparam o = u.x; + +always_comb begin + assert(d == 2'b10); + assert(e == 1'b1); + assert(f == 1'b0); + assert(j == 1'b1); + assert(k == 1'b0); + assert(l == 3'b111); +// TODO: support access to whole sub-structs and unions +// assert(m == 2'b10); + assert(u == 5'b11001); +end +endmodule +EOF +hierarchy; proc; opt +sat -verify -seq 1 -tempinduct -prove-asserts -show-all diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index ee5ad8a1a..45e936a21 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -68,146 +68,3 @@ equiv_opt -assert peepopt design -load postopt clean select -assert-count 0 t:* - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o); - always @(posedge clk) if (ce) o <= i; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -clean -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 1 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o); - always @(posedge clk) if (ce) o <= i; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -clean -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 1 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o); - always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 1 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o); - always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -select -assert-count 1 t:$dff r:WIDTH=4 %i -select -assert-count 1 t:$mux r:WIDTH=4 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o); - always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i; -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -wreduce -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 2 t:$mux -select -assert-count 2 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$dff t:$mux %% t:* %D - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); - always @(posedge clk) begin - if (ce) o <= i; - if (!rstn) o <= 4'b1111; - end -endmodule -EOT - -proc -equiv_opt -assert peepopt -design -load postopt -wreduce -select -assert-count 1 t:$dff r:WIDTH=2 %i -select -assert-count 2 t:$mux -select -assert-count 2 t:$mux r:WIDTH=2 %i -select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D - -#################### - -design -reset -read_verilog <<EOT -module peepopt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); - initial o <= 4'b0010; - always @(posedge clk) begin - if (ce) o <= i; - if (!rstn) o <= 4'b1111; - end -endmodule -EOT - -proc -# NB: equiv_opt uses equiv_induct which covers -# only the induction half of temporal induction -# --- missing the base-case half -# This makes it akin to `sat -tempinduct-inductonly` -# instead of `sat -tempinduct-baseonly` or -# `sat -tempinduct` which is necessary for this -# testcase -#equiv_opt -assert peepopt - -design -save gold -peepopt -wreduce -design -stash gate -design -import gold -as gold -design -import gate -as gate -miter -equiv -flatten -make_assert -make_outputs gold gate miter -sat -tempinduct -verify -prove-asserts -show-ports miter - -design -load gate -select -assert-count 1 t:$dff r:WIDTH=4 %i -select -assert-count 2 t:$mux -select -assert-count 2 t:$mux r:WIDTH=4 %i -select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D 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/various/run-test.sh b/tests/various/run-test.sh index ea56b70f0..2f91cf0fd 100755 --- a/tests/various/run-test.sh +++ b/tests/various/run-test.sh @@ -1,20 +1,4 @@ #!/usr/bin/env bash -set -e -{ -echo "all::" -for x in *.ys; do - echo "all:: run-$x" - echo "run-$x:" - echo " @echo 'Running $x..'" - echo " @../../yosys -ql ${x%.ys}.log $x" -done -for s in *.sh; do - if [ "$s" != "run-test.sh" ]; then - echo "all:: run-$s" - echo "run-$s:" - echo " @echo 'Running $s..'" - echo " @bash $s" - fi -done -} > run-test.mk -exec ${MAKE:-make} -f run-test.mk +set -eu +source ../gen-tests-makefile.sh +run_tests --yosys-scripts --bash diff --git a/tests/various/sta.ys b/tests/various/sta.ys new file mode 100644 index 000000000..156c31c47 --- /dev/null +++ b/tests/various/sta.ys @@ -0,0 +1,81 @@ +read_verilog -specify <<EOT +module buffer(input i, output o); +specify +(i => o) = 10; +endspecify +endmodule + +module top(input i); +wire w; +buffer b(.i(i), .o(w)); +endmodule +EOT + +logger -expect warning "Critical-path does not terminate in a recognised endpoint\." 1 +sta + + +design -reset +read_verilog -specify <<EOT +module top(input i, output o, p); +assign o = i; +endmodule +EOT + +logger -expect log "No timing paths found\." 1 +sta + + +design -reset +read_verilog -specify <<EOT +module buffer(input i, output o); +specify +(i => o) = 10; +endspecify +endmodule + +module top(input i, output o, p); +buffer b(.i(i), .o(o)); +endmodule +EOT + +sta + + +design -reset +read_verilog -specify <<EOT +module buffer(input i, output o); +specify +(i => o) = 10; +endspecify +endmodule + +module top(input i, output o, p); +buffer b(.i(i), .o(o)); +const0 c(.o(p)); +endmodule +EOT + +logger -expect warning "Cell type 'const0' not recognised! Ignoring\." 1 +sta + + +design -reset +read_verilog -specify <<EOT +module buffer(input i, output o); +specify +(i => o) = 10; +endspecify +endmodule +module const0(output o); +endmodule + +module top(input i, output o, p); +buffer b(.i(i), .o(o)); +const0 c(.o(p)); +endmodule +EOT + +sta + +logger -expect-no-warnings |