Merge pull request #5903 from YosysHQ/krys/verific_memsize

verific: Fix non-contiguous memory flattening producing out of bounds accesses in some cases

tests/Makefile

@@ -74,6 +74,7 @@ MK_TEST_DIRS += ./liberty
 MK_TEST_DIRS += ./memories
 MK_TEST_DIRS += ./aiger
 MK_TEST_DIRS += ./alumacc
+MK_TEST_DIRS += ./check_mem
 
 all: vanilla-test
 

tests/check_mem/bad_il.ys

@@ -0,0 +1,47 @@
+read_rtlil << EOF
+module \top
+  wire input 1 \clk
+  wire output 1 \o
+  memory size 2 offset 1 \my_array
+  cell $meminit \bad_init
+    parameter \WORDS 1
+    parameter \MEMID "\\my_array"
+    parameter \ABITS 32
+    parameter \WIDTH 1
+    parameter \PRIORITY 1
+    connect \ADDR 0
+    connect \DATA 1'0
+  end
+  cell $memwr \bad_wr
+    parameter \MEMID "\\my_array"
+    parameter \CLK_ENABLE 1
+    parameter \CLK_POLARITY 1
+    parameter \PRIORITY 1
+    parameter \ABITS 2
+    parameter \WIDTH 1
+    connect \EN 1'1
+    connect \CLK \clk
+    connect \ADDR 2'00
+    connect \DATA 1'0
+  end
+  cell $memrd \bad_rd
+    parameter \MEMID "\\my_array"
+    parameter \CLK_ENABLE 0
+    parameter \CLK_POLARITY 1
+    parameter \TRANSPARENT 0
+    parameter \ABITS 2
+    parameter \WIDTH 1
+    connect \CLK 1'x
+    connect \EN 1'x
+    connect \ADDR 2'11
+    connect \DATA \o
+  end
+end
+EOF
+
+logger -expect warning "initializes address 0" 1
+logger -expect warning "writes address 0" 1
+logger -expect warning "reads address 3" 1
+check_mem
+logger -check-expected
+design -reset

tests/check_mem/generate_mk.py

@@ -0,0 +1,8 @@
+#!/usr/bin/env python3
+
+import sys
+sys.path.append("..")
+
+import gen_tests_makefile
+
+gen_tests_makefile.generate(["--check-sv", "--yosys-scripts"], yosys_cmds="hierarchy; proc; check_mem -assert")

tests/check_mem/init.sv

@@ -0,0 +1,15 @@
+module top (
+  input logic clk,
+  input logic idx,
+  output logic [2:0] out_data
+);
+  (* nomem2reg *)
+  logic my_array [3:2][2:0] = '{'{0, 1, 1}, '{1, 0, 1}};
+
+  always_comb begin
+    for (int i=0; i < 3; i++) begin
+        out_data[i] = my_array[{1'b1, idx}][i];
+    end
+  end
+
+endmodule

tests/check_mem/init_correct.ys

@@ -0,0 +1,44 @@
+read -sv << EOT
+module top;
+  (* nomem2reg *)
+  logic a1 [2:3][3:1] = '{'{0, 1, 1}, '{1, 0, 1}};
+
+  always_comb begin
+    assert(a1[2][3] == 0);
+    assert(a1[2][2] == 1);
+    assert(a1[2][1] == 1);
+    assert(a1[3][3] == 1);
+    assert(a1[3][2] == 0);
+    assert(a1[3][1] == 1);
+  end
+
+  (* nomem2reg *)
+  logic [1:0] a2 [6:5][2:4] = '{'{0, 1, 2}, '{1, 0, 3}};
+
+  always_comb begin
+    assert(a2[6][2] == 0);
+    assert(a2[6][3] == 1);
+    assert(a2[6][4] == 2);
+    assert(a2[5][2] == 1);
+    assert(a2[5][3] == 0);
+    assert(a2[5][4] == 3);
+  end
+
+  (* nomem2reg *)
+  logic [1:0] a3 [-2:-1][-1:1] = '{'{0, 1, 2}, '{1, 0, 3}};
+
+  always_comb begin
+    assert(a3[-2][-1] == 0);
+    assert(a3[-2][0] == 1);
+    assert(a3[-2][1] == 2);
+    assert(a3[-1][-1] == 1);
+    assert(a3[-1][0] == 0);
+    assert(a3[-1][1] == 3);
+  end
+endmodule
+EOT
+hierarchy
+proc
+memory
+async2sync
+sat -enable_undef -verify -prove-asserts

tests/check_mem/negative_idx.sv

@@ -0,0 +1,13 @@
+module top;
+  (* nomem2reg *)
+  logic [1:0] a3 [-2:-1][-1:1] = '{'{0, 1, 2}, '{1, 0, 3}};
+
+  always_comb begin
+    assert(a3[-2][-1] == 0);
+    assert(a3[-2][0] == 1);
+    assert(a3[-2][1] == 2);
+    assert(a3[-1][-1] == 1);
+    assert(a3[-1][0] == 0);
+    assert(a3[-1][1] == 3);
+  end
+endmodule

tests/check_mem/non_zero.sv

@@ -0,0 +1,21 @@
+module top (
+  input logic clk,
+  input logic [3:1][2:0] in_data,
+  output logic [3:1][2:0] out_data
+);
+  (* nomem2reg *)
+  logic [2:0] my_array [3:1];
+
+  always_ff @(posedge clk) begin
+    for (int i = 1; i <= 3; i++) begin
+      my_array[i] <= in_data[i];
+    end
+  end
+
+  always_comb begin
+    for (int i = 1; i <= 3; i++) begin
+      out_data[i] = my_array[i];
+    end
+  end
+
+endmodule

tests/check_mem/power_of_two.sv

@@ -0,0 +1,24 @@
+module top (
+  input logic clk,
+  input logic [1:0][5:0] in_data,
+  output logic [1:0][5:0] out_data
+);
+  (* nomem2reg *)
+  logic my_array [1:0][5:0];
+
+  always_ff @(posedge clk) begin
+    for (int i = 0; i < 2; i++) begin
+      for (int j = 0; j <= 5; j++) begin
+        my_array[i][j] <= in_data[i][j];
+      end
+    end
+  end
+
+  always_comb begin
+    for (int i = 0; i < 2; i++) begin
+      for (int j = 0; j <= 5; j++) begin
+        out_data[i][j] = my_array[i][j];
+      end
+    end
+  end
+endmodule

tests/check_mem/sub_addr.sv

@@ -0,0 +1,18 @@
+module memtest05(clk, addr, wdata, rdata, wen);
+
+input clk;
+input [1:0] addr;
+input [7:0] wdata;
+output reg [7:0] rdata;
+input [3:0] wen;
+
+reg [7:0] mem [0:3];
+
+integer i;
+always @(posedge clk) begin
+	for (i = 0; i < 4; i = i+1)
+		if (wen[i]) mem[addr][i*2 +: 2] <= wdata[i*2 +: 2];
+	rdata <= mem[addr];
+end
+
+endmodule

tests/check_mem/variable.ys

@@ -0,0 +1,65 @@
+
+
+read_rtlil << EOF
+module \top
+  wire input 1 \clk
+  wire input 2 width 2 \addr
+  wire output 1 \o
+  memory size 3 offset 0 \my_array
+  # potentially dangerous - requires external control to avoid illegal access
+  cell $memrd \bad_rd
+    parameter \MEMID "\\my_array"
+    parameter \CLK_ENABLE 0
+    parameter \CLK_POLARITY 1
+    parameter \TRANSPARENT 0
+    parameter \ABITS 2
+    parameter \WIDTH 1
+    connect \CLK 1'x
+    connect \EN 1'x
+    connect \ADDR \addr
+    connect \DATA \o
+  end
+  wire width 2 \n_addr
+  cell $not \not_addr
+    parameter \A_SIGNED 0
+    parameter \A_WIDTH 2
+    parameter \Y_WIDTH 2
+    connect \A \addr
+    connect \Y \n_addr
+  end
+  # address is partially const, making the illegal access of 2'11 impossible
+  cell $memrd \partial_const_rd
+    parameter \MEMID "\\my_array"
+    parameter \CLK_ENABLE 0
+    parameter \CLK_POLARITY 1
+    parameter \TRANSPARENT 0
+    parameter \ABITS 2
+    parameter \WIDTH 1
+    connect \CLK 1'x
+    connect \EN 1'x
+    connect \ADDR { 1'0 \addr [0] }
+    connect \DATA \o
+  end
+  # address is non-const but limited to 2'10 and 2'01 - both of which are valid
+  cell $memrd \limited_rd
+    parameter \MEMID "\\my_array"
+    parameter \CLK_ENABLE 0
+    parameter \CLK_POLARITY 1
+    parameter \TRANSPARENT 0
+    parameter \ABITS 2
+    parameter \WIDTH 1
+    connect \CLK 1'x
+    connect \EN 1'x
+    connect \ADDR { \n_addr [0] \addr [0] }
+    connect \DATA \o
+  end
+end
+EOF
+
+logger -expect warning "potentially dangerous non-const input \\addr" 1
+# unhandled false-positives
+# logger -werror "potentially dangerous non-const input \{ 1'0"
+# logger -werror "potentially dangerous non-const input \{ \\n_addr"
+check_mem -non-const
+logger -check-expected
+design -reset

tests/gen_tests_makefile.py

@@ -37,6 +37,11 @@ def generate_tcl_test(tcl_file, yosys_args="", commands=""):
         cmd += f"; \\\n{commands}"
     generate_target(tcl_file, cmd)
 
+def generate_sv_check(sv_file, yosys_args="", yosys_cmds=""):
+    yosys_cmd = f'read -sv {sv_file}; {yosys_cmds}'
+    cmd = f'$(YOSYS) -ql {sv_file}.err -p "{yosys_cmd}" {yosys_args} && mv {sv_file}.err {sv_file}.log'
+    generate_target(sv_file, cmd)
+
 def generate_sv_test(sv_file, yosys_args="", commands=""):
     base = os.path.splitext(sv_file)[0]
     if not os.path.exists(base + ".ys"):
@@ -62,19 +67,23 @@ def unpack_cmd(cmd):
 def generate_cmd_test(test_name, cmd, yosys_args="", deps = None):
     generate_target(test_name, unpack_cmd(cmd), deps)
 
-def generate_tests(argv, cmds):
+def generate_tests(argv, cmds, yosys_cmds=""):
     parser = argparse.ArgumentParser(add_help=False)
     parser.add_argument("-y", "--yosys-scripts", action="store_true")
     parser.add_argument("-t", "--tcl-scripts", action="store_true")
+    parser.add_argument("-c", "--check-sv", action="store_true")
     parser.add_argument("-s", "--prove-sv", action="store_true")
     parser.add_argument("-b", "--bash", action="store_true")
     parser.add_argument("-a", "--yosys-args", default="")
 
     args = parser.parse_args(argv)
 
-    if not (args.yosys_scripts or args.tcl_scripts or args.prove_sv or args.bash):
+    if not (args.yosys_scripts or args.tcl_scripts or args.check_sv or args.prove_sv or args.bash):
         raise RuntimeError("No file types selected")
 
+    if args.check_sv and args.prove_sv:
+        raise RuntimeError("Unable to use --check-sv and --prove-sv together")
+
     if args.yosys_scripts:
         for f in sorted(glob.glob("*.ys")):
             generate_ys_test(f, args.yosys_args, cmds)
@@ -83,6 +92,10 @@ def generate_tests(argv, cmds):
         for f in sorted(glob.glob("*.tcl")):
             generate_tcl_test(f, args.yosys_args, cmds)
 
+    if args.check_sv:
+        for f in sorted(glob.glob("*.sv")):
+            generate_sv_check(f, args.yosys_args, yosys_cmds)
+
     if args.prove_sv:
         for f in sorted(glob.glob("*.sv")):
             generate_sv_test(f, args.yosys_args, cmds)
@@ -109,11 +122,11 @@ def redirect_stdout(new_target):
     finally:
         sys.stdout = old_target
 
-def generate(argv, extra=None, cmds=""):
+def generate(argv, extra=None, cmds="", yosys_cmds=""):
     with open("Makefile", "w") as f:
         with redirect_stdout(f):
             print_header(extra)
-            generate_tests(argv, cmds)
+            generate_tests(argv, cmds, yosys_cmds)
 
 def generate_custom(callback, extra=None):
     with open("Makefile", "w") as f: