aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/simple/mem2reg_bounds_tern.v19
-rw-r--r--tests/verilog/mem_bounds.sv27
-rw-r--r--tests/verilog/mem_bounds.ys6
3 files changed, 52 insertions, 0 deletions
diff --git a/tests/simple/mem2reg_bounds_tern.v b/tests/simple/mem2reg_bounds_tern.v
new file mode 100644
index 000000000..89d6dd3e8
--- /dev/null
+++ b/tests/simple/mem2reg_bounds_tern.v
@@ -0,0 +1,19 @@
+module top(
+ input clk,
+ input wire [1:0] sel,
+ input wire [7:0] base,
+ output reg [7:0] line
+);
+ reg [0:7] mem [0:2];
+
+ generate
+ genvar i;
+ for (i = 0; i < 4; i = i + 1) begin : gen
+ always @(posedge clk)
+ mem[i] <= i == 0 ? base : mem[i - 1] + 1;
+ end
+ endgenerate
+
+ always @(posedge clk)
+ line = mem[sel];
+endmodule
diff --git a/tests/verilog/mem_bounds.sv b/tests/verilog/mem_bounds.sv
new file mode 100644
index 000000000..7fb2fb042
--- /dev/null
+++ b/tests/verilog/mem_bounds.sv
@@ -0,0 +1,27 @@
+module top;
+ reg [0:7] mem [0:2];
+
+ initial mem[1] = '1;
+ wire [31:0] a, b, c, d;
+ assign a = mem[1];
+ assign b = mem[-1];
+ assign c = mem[-1][0];
+ assign d = mem[-1][0:1];
+
+ always @* begin
+
+ assert ($countbits(a, '0) == 24);
+ assert ($countbits(a, '1) == 8);
+ assert ($countbits(a, 'x) == 0);
+
+ assert ($countbits(b, '0) == 24);
+ assert ($countbits(b, 'x) == 8);
+
+ assert ($countbits(c, '0) == 31);
+ assert ($countbits(c, 'x) == 1);
+
+ assert ($countbits(d, '0) == 30);
+ assert ($countbits(d, 'x) == 2);
+
+ end
+endmodule
diff --git a/tests/verilog/mem_bounds.ys b/tests/verilog/mem_bounds.ys
new file mode 100644
index 000000000..42623ad09
--- /dev/null
+++ b/tests/verilog/mem_bounds.ys
@@ -0,0 +1,6 @@
+read_verilog -sv -mem2reg mem_bounds.sv
+proc
+flatten
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all -enable_undef