aboutsummaryrefslogtreecommitdiffstats
path: root/tests/verilog
diff options
context:
space:
mode:
Diffstat (limited to 'tests/verilog')
-rw-r--r--tests/verilog/always_comb_nolatch_5.ys15
-rw-r--r--tests/verilog/always_comb_nolatch_6.ys15
-rw-r--r--tests/verilog/delay_time_scale.ys25
-rwxr-xr-xtests/verilog/dynamic_range_lhs.sh32
-rw-r--r--tests/verilog/dynamic_range_lhs.v76
-rw-r--r--tests/verilog/func_tern_hint.sv42
-rw-r--r--tests/verilog/func_tern_hint.ys4
-rw-r--r--tests/verilog/func_upto.sv77
-rw-r--r--tests/verilog/func_upto.ys7
-rw-r--r--tests/verilog/past_signedness.ys35
-rw-r--r--tests/verilog/sign_array_query.ys52
-rw-r--r--tests/verilog/struct_access.sv5
-rw-r--r--tests/verilog/unreachable_case_sign.ys33
13 files changed, 415 insertions, 3 deletions
diff --git a/tests/verilog/always_comb_nolatch_5.ys b/tests/verilog/always_comb_nolatch_5.ys
new file mode 100644
index 000000000..132878626
--- /dev/null
+++ b/tests/verilog/always_comb_nolatch_5.ys
@@ -0,0 +1,15 @@
+read_verilog -sv <<EOF
+module top;
+logic [4:0] x;
+logic z;
+assign z = 1'b1;
+always_comb begin : foo
+ x = '0;
+ if (z) begin : bar
+ for (int i = 0; i < 5; i++)
+ x[i] = 1'b1;
+ end
+end
+endmodule
+EOF
+proc
diff --git a/tests/verilog/always_comb_nolatch_6.ys b/tests/verilog/always_comb_nolatch_6.ys
new file mode 100644
index 000000000..90ee78a68
--- /dev/null
+++ b/tests/verilog/always_comb_nolatch_6.ys
@@ -0,0 +1,15 @@
+read_verilog -sv <<EOF
+module top(input wire x, y, output reg z);
+function automatic f;
+ input inp;
+ for (int i = 0; i < 1; i++)
+ f = inp + 0;
+endfunction
+always_comb
+ if (y)
+ z = f(x);
+ else
+ z = 0;
+endmodule
+EOF
+proc
diff --git a/tests/verilog/delay_time_scale.ys b/tests/verilog/delay_time_scale.ys
new file mode 100644
index 000000000..f45ba7b26
--- /dev/null
+++ b/tests/verilog/delay_time_scale.ys
@@ -0,0 +1,25 @@
+logger -expect-no-warnings
+read_verilog -sv <<EOT
+module top;
+wand x;
+`define TEST(time_scale) if (1) assign #time_scale x = 1;
+
+`TEST(1s)
+`TEST(1ms)
+`TEST(1us)
+`TEST(1ns)
+`TEST(1ps)
+`TEST(1fs)
+
+`TEST((1s))
+`TEST(( 1s))
+`TEST((1s ))
+`TEST(( 1s ))
+
+`TEST(1.0s)
+`TEST(1.1s)
+`TEST(1.0e-1s)
+`TEST(1e-1s)
+
+endmodule
+EOT
diff --git a/tests/verilog/dynamic_range_lhs.sh b/tests/verilog/dynamic_range_lhs.sh
new file mode 100755
index 000000000..618204aed
--- /dev/null
+++ b/tests/verilog/dynamic_range_lhs.sh
@@ -0,0 +1,32 @@
+#!/bin/bash
+
+run() {
+ alt=$1
+ span=$2
+ left=$3
+ right=$4
+ echo "a=$alt s=$span l=$left r=$right"
+
+ ../../yosys -q \
+ -DALT=$alt \
+ -DSPAN=$span \
+ -DLEFT=$left \
+ -DRIGHT=$right \
+ -p "read_verilog dynamic_range_lhs.v" \
+ -p "proc" \
+ -p "equiv_make gold gate equiv" \
+ -p "equiv_simple" \
+ -p "equiv_status -assert"
+}
+
+trap 'echo "ERROR in dynamic_range_lhs.sh span=$span left=$left right=$right" >&2; exit 1' ERR
+
+for alt in `seq 0 1`; do
+for span in `seq 1 4`; do
+for left in `seq -4 4`; do
+for right in `seq $(expr $left + -3) $(expr $left + 3)`; do
+ run $alt $span $left $right
+done
+done
+done
+done
diff --git a/tests/verilog/dynamic_range_lhs.v b/tests/verilog/dynamic_range_lhs.v
new file mode 100644
index 000000000..ae291374d
--- /dev/null
+++ b/tests/verilog/dynamic_range_lhs.v
@@ -0,0 +1,76 @@
+module gate(
+ output reg [`LEFT:`RIGHT] out_u, out_s,
+ (* nowrshmsk = `ALT *)
+ input wire data,
+ input wire [1:0] sel1, sel2
+);
+always @* begin
+ out_u = 0;
+ out_s = 0;
+ case (`SPAN)
+ 1: begin
+ out_u[sel1*sel2] = data;
+ out_s[$signed(sel1*sel2)] = data;
+ end
+ 2: begin
+ out_u[sel1*sel2+:2] = {data, data};
+ out_s[$signed(sel1*sel2)+:2] = {data, data};
+ end
+ 3: begin
+ out_u[sel1*sel2+:3] = {data, data, data};
+ out_s[$signed(sel1*sel2)+:3] = {data, data, data};
+ end
+ 4: begin
+ out_u[sel1*sel2+:4] = {data, data, data, data};
+ out_s[$signed(sel1*sel2)+:4] = {data, data, data, data};
+ end
+ endcase
+end
+endmodule
+
+module gold(
+ output reg [`LEFT:`RIGHT] out_u, out_s,
+ input wire data,
+ input wire [1:0] sel1, sel2
+);
+task set;
+ input integer a, b;
+ localparam LOW = `LEFT > `RIGHT ? `RIGHT : `LEFT;
+ localparam HIGH = `LEFT > `RIGHT ? `LEFT : `RIGHT;
+ if (LOW <= a && a <= HIGH)
+ out_u[a] = data;
+ if (LOW <= b && b <= HIGH)
+ out_s[b] = data;
+endtask
+always @* begin
+ out_u = 0;
+ out_s = 0;
+ case (sel1*sel2)
+ 2'b00: set(0, 0);
+ 2'b01: set(1, 1);
+ 2'b10: set(2, -2);
+ 2'b11: set(3, -1);
+ endcase
+ if (`SPAN >= 2)
+ case (sel1*sel2)
+ 2'b00: set(1, 1);
+ 2'b01: set(2, 2);
+ 2'b10: set(3, -1);
+ 2'b11: set(4, 0);
+ endcase
+ if (`SPAN >= 3)
+ case (sel1*sel2)
+ 2'b00: set(2, 2);
+ 2'b01: set(3, 3);
+ 2'b10: set(4, 0);
+ 2'b11: set(5, 1);
+ endcase
+ if (`SPAN >= 4)
+ case (sel1*sel2)
+ 2'b00: set(3, 3);
+ 2'b01: set(4, 4);
+ 2'b10: set(5, 1);
+ 2'b11: set(6, 2);
+ endcase
+end
+endmodule
diff --git a/tests/verilog/func_tern_hint.sv b/tests/verilog/func_tern_hint.sv
new file mode 100644
index 000000000..3c58c9913
--- /dev/null
+++ b/tests/verilog/func_tern_hint.sv
@@ -0,0 +1,42 @@
+module top;
+ function automatic [30:0] func;
+ input integer inp;
+ func = { // self-determined context
+ (
+ inp == 0
+ ? -1 // causes whole ternary to be 32 bits
+ : func(inp - 1) // 31 bits, unsigned
+ ) >> 2};
+ endfunction
+ function automatic signed [3:0] dunk;
+ input integer inp;
+ dunk = (
+ inp == 0
+ ? 4'hF
+ // shouldn't make the ternary signed
+ : dunk(inp - 1)
+ ) == -1;
+ endfunction
+ localparam A = func(0);
+ localparam B = func(1);
+ localparam C = func(2);
+ localparam D = func(3);
+ localparam X = dunk(0);
+ localparam Y = dunk(1);
+ initial begin
+ assert(A == 31'h3F_FFFFFF);
+ assert(B == 31'h0F_FFFFFF);
+ assert(C == 31'h03_FFFFFF);
+ assert(D == 31'h00_FFFFFF);
+ assert(X == 0);
+ assert(Y == 0);
+ end
+ initial begin
+ logic x;
+ case (1'b1)
+ dunk(0): x = 0;
+ default: x = 1;
+ endcase
+ assert(x);
+ end
+endmodule
diff --git a/tests/verilog/func_tern_hint.ys b/tests/verilog/func_tern_hint.ys
new file mode 100644
index 000000000..ab8a1e032
--- /dev/null
+++ b/tests/verilog/func_tern_hint.ys
@@ -0,0 +1,4 @@
+read_verilog -sv func_tern_hint.sv
+proc
+opt
+sat -verify -seq 1 -prove-asserts -show-all
diff --git a/tests/verilog/func_upto.sv b/tests/verilog/func_upto.sv
new file mode 100644
index 000000000..547e5d325
--- /dev/null
+++ b/tests/verilog/func_upto.sv
@@ -0,0 +1,77 @@
+`default_nettype none
+
+module evil;
+ parameter HI = 3;
+ parameter LO = 0;
+ parameter SPAN = 1;
+ parameter [HI:LO] A_VAL = 4'b0110;
+ parameter [HI:LO] B_VAL = 4'b1100;
+ parameter [2:0] SWAPS = 0;
+
+ localparam D_LEFT = !(SWAPS[0]) ? HI : LO;
+ localparam D_RIGHT = (SWAPS[0]) ? HI : LO;
+ localparam E_LEFT = !(SWAPS[1]) ? HI : LO;
+ localparam E_RIGHT = (SWAPS[1]) ? HI : LO;
+ localparam F_LEFT = !(SWAPS[2]) ? HI : LO;
+ localparam F_RIGHT = (SWAPS[2]) ? HI : LO;
+
+ localparam [HI:LO] A_CONST = A_VAL;
+ localparam [HI:LO] B_CONST = B_VAL;
+ localparam [HI:LO] C_CONST = F(A_CONST, B_CONST);
+
+ reg [HI:LO] C_WIRE, C_FUNC;
+ always @* begin
+ assert (C_CONST == C_WIRE);
+ assert (C_CONST == C_FUNC);
+ end
+
+ initial begin : blk
+ reg [HI:LO] A_WIRE;
+ reg [HI:LO] B_WIRE;
+ reg [D_LEFT:D_RIGHT] D;
+ reg [E_LEFT:E_RIGHT] E;
+ reg [F_LEFT:F_RIGHT] F_WIRE;
+ reg [31:0] i;
+ A_WIRE = A_VAL;
+ B_WIRE = B_VAL;
+ D = A_WIRE;
+ E = B_WIRE;
+ F_WIRE = 0;
+ for (i = LO; i + SPAN < HI; i = i + SPAN)
+ if (SPAN == 1)
+ F_WIRE[i] = D[i] && E[i];
+ else
+ F_WIRE[i+:SPAN] = D[i+:SPAN] && E[i+:SPAN];
+ C_WIRE = F_WIRE;
+ C_FUNC = F(A_WIRE, B_WIRE);
+ end
+
+ function automatic [F_LEFT:F_RIGHT] F(
+ input [D_LEFT:D_RIGHT] D,
+ input [E_LEFT:E_RIGHT] E);
+ reg [31:0] i;
+ F = 0;
+ for (i = LO; i + SPAN < HI; i = i + SPAN)
+ if (SPAN == 1)
+ F[i] = D[i] && E[i];
+ else
+ F[i+:SPAN] = D[i+:SPAN] && E[i+:SPAN];
+ endfunction
+endmodule
+
+module top;
+ for (genvar hi = 0; hi < 3; hi++)
+ for (genvar lo = 0; lo <= hi; lo++)
+ for (genvar span = 1; span <= hi - lo + 1; span++)
+ for (genvar a_val = 0; a_val < 2 ** (hi - lo + 1); a_val++)
+ for (genvar b_val = 0; b_val < 2 ** (hi - lo + 1); b_val++)
+ for (genvar swaps = 0; swaps < 2 ** 3; swaps++)
+ evil #(
+ .HI(hi),
+ .LO(lo),
+ .SPAN(span),
+ .A_VAL(a_val),
+ .B_VAL(b_val),
+ .SWAPS(swaps)
+ ) e();
+endmodule
diff --git a/tests/verilog/func_upto.ys b/tests/verilog/func_upto.ys
new file mode 100644
index 000000000..7a8c53506
--- /dev/null
+++ b/tests/verilog/func_upto.ys
@@ -0,0 +1,7 @@
+read_verilog -sv func_upto.sv
+hierarchy -top top
+proc
+flatten
+opt -full
+select -module top
+sat -verify -seq 1 -prove-asserts -enable_undef
diff --git a/tests/verilog/past_signedness.ys b/tests/verilog/past_signedness.ys
new file mode 100644
index 000000000..91f32328b
--- /dev/null
+++ b/tests/verilog/past_signedness.ys
@@ -0,0 +1,35 @@
+logger -expect-no-warnings
+
+read_verilog -formal <<EOT
+module top(input clk);
+ reg signed [3:0] value = -1;
+ reg ready = 0;
+
+ always @(posedge clk) begin
+ if (ready)
+ assert ($past(value) == -1);
+ ready <= 1;
+ end
+endmodule
+EOT
+
+prep -top top
+sim -n 3 -clock clk
+
+design -reset
+
+read_verilog -formal <<EOT
+module top(input clk);
+ reg signed [3:0] value = -1;
+ reg ready = 0;
+
+ always @(posedge clk) begin
+ if (ready)
+ assert ($past(value + 4'b0000) == 15);
+ ready <= 1;
+ end
+endmodule
+EOT
+
+prep -top top
+sim -n 3 -clock clk
diff --git a/tests/verilog/sign_array_query.ys b/tests/verilog/sign_array_query.ys
new file mode 100644
index 000000000..f955450b7
--- /dev/null
+++ b/tests/verilog/sign_array_query.ys
@@ -0,0 +1,52 @@
+logger -expect-no-warnings
+
+read_verilog -formal <<EOT
+module top(input clk);
+ reg [-1:-1] x;
+ reg good = 0;
+ reg signed [31:0] zero = 0;
+
+ always @(posedge clk) begin
+ case ($left(x) + zero) 36'shfffffffff: good = 1; endcase
+ assert (good);
+ end
+endmodule
+EOT
+
+prep -top top
+sim -n 3 -clock clk
+
+design -reset
+
+read_verilog -formal <<EOT
+module top(input clk);
+ reg [-1:-1] x;
+ reg good = 0;
+
+ always @(posedge clk) begin
+ case ($left(x)) 36'sh0ffffffff: good = 1; (32'h0 + $left(good)): ; endcase
+ assert (good);
+ end
+
+endmodule
+EOT
+
+prep -top top
+sim -n 3 -clock clk
+
+design -reset
+
+read_verilog -formal <<EOT
+module top(input clk);
+ reg [-1:-1] x;
+ reg good = 1;
+
+ always @(posedge clk) begin
+ case (36'sh100000000 + $left(x)) -1: good = 0; endcase
+ assert (good);
+ end
+endmodule
+EOT
+
+prep -top top
+sim -n 3 -clock clk
diff --git a/tests/verilog/struct_access.sv b/tests/verilog/struct_access.sv
index f13b8dd51..bc91e3f01 100644
--- a/tests/verilog/struct_access.sv
+++ b/tests/verilog/struct_access.sv
@@ -77,9 +77,8 @@ module top;
`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)
+ `CHECK(s.x, 2, 0)
+ `CHECK(s.y, 2, 1)
assert (fail === 0);
end
diff --git a/tests/verilog/unreachable_case_sign.ys b/tests/verilog/unreachable_case_sign.ys
new file mode 100644
index 000000000..25bc0c6f0
--- /dev/null
+++ b/tests/verilog/unreachable_case_sign.ys
@@ -0,0 +1,33 @@
+logger -expect-no-warnings
+
+read_verilog -formal <<EOT
+module top(input clk);
+ reg good = 0;
+
+ always @(posedge clk) begin
+ case (4'sb1111) 15: good = 1; 4'b0000: ; endcase
+ assert (good);
+ end
+endmodule
+EOT
+
+prep -top top
+sim -n 3 -clock clk
+
+design -reset
+
+read_verilog -formal <<EOT
+module top(input clk);
+ reg good = 1;
+ reg signed [1:0] case_value = -1;
+
+ always @(posedge clk) begin
+ case (4'sb1111) 4'b0000: ; case_value: good = 0; endcase
+ assert (good);
+ end
+endmodule
+EOT
+
+prep -top top
+sim -n 3 -clock clk
+
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-06 00:26:48 +0000