diff options
Diffstat (limited to 'tests')
-rw-r--r-- | tests/simple/mem2reg_bounds_tern.v | 19 | ||||
-rw-r--r-- | tests/verilog/mem_bounds.sv | 27 | ||||
-rw-r--r-- | tests/verilog/mem_bounds.ys | 6 |
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 |