aboutsummaryrefslogtreecommitdiffstats
path: root/tests/xprop/test.py
diff options
context:
space:
mode:
Diffstat (limited to 'tests/xprop/test.py')
-rw-r--r--tests/xprop/test.py516
1 files changed, 516 insertions, 0 deletions
diff --git a/tests/xprop/test.py b/tests/xprop/test.py
new file mode 100644
index 000000000..84ad0a1f4
--- /dev/null
+++ b/tests/xprop/test.py
@@ -0,0 +1,516 @@
+import os
+import re
+import subprocess
+import itertools
+import random
+import argparse
+from pathlib import Path
+
+parser = argparse.ArgumentParser(formatter_class=argparse.ArgumentDefaultsHelpFormatter)
+parser.add_argument('-S', '--seed', type=int, help='seed for PRNG')
+parser.add_argument('-c', '--count', type=int, default=32, help='number of random patterns to test')
+parser.add_argument('-s', '--seq', action='store_true', help='run a sequential test')
+parser.add_argument('steps', nargs='*', help='steps to run')
+args = parser.parse_args()
+
+if args.seed is None:
+ args.seed = random.randrange(1 << 32)
+
+print(f"PRNG seed: {args.seed}")
+random.seed(args.seed)
+
+steps = args.steps
+
+all_outputs = [
+ "sim",
+ "sim_xprop",
+ "vsim_expr",
+ "vsim_expr_xprop",
+ "vsim_noexpr",
+ "vsim_noexpr_xprop",
+ "sat",
+ "sat_xprop",
+]
+
+if not args.seq:
+ all_outputs += ["opt_expr", "opt_expr_xprop"]
+
+if not steps:
+ steps = ["clean", "prepare", "verify", *all_outputs, "compare"]
+
+if "clean" in steps:
+ for output in all_outputs:
+ try:
+ os.unlink(f"{output}.out")
+ except FileNotFoundError:
+ pass
+
+
+def yosys(command):
+ subprocess.check_call(["yosys", "-Qp", command])
+
+def remove(file):
+ try:
+ os.unlink(file)
+ except FileNotFoundError:
+ pass
+
+
+def vcdextract(signals, on_change, file, output, limit=None):
+ scope = []
+ ids = {}
+ prefix = []
+
+ for line in file:
+ line = prefix + line.split()
+ if line[-1] != "$end":
+ prefix = line
+ continue
+ prefix = []
+
+ if not line:
+ continue
+ if line[0] == "$scope":
+ scope.append(line[2].lstrip("\\"))
+ elif line[0] == "$upscope":
+ scope.pop()
+ elif line[0] == "$var":
+ ids[".".join(scope + [line[4].lstrip("\\")])] = line[3]
+ elif line[0] == "$enddefinitions":
+ break
+ elif line[0] in ["$version", "$date", "$comment"]:
+ continue
+ else:
+ raise RuntimeError(f"unexpected input in vcd {line}")
+
+ dump_pos = {}
+
+ for i, sig in enumerate(signals + on_change):
+ dump_pos[ids[sig]] = i
+
+ values = [None] * len(signals + on_change)
+
+ last_values = []
+
+ counter = 0
+
+ for line in file:
+ if line.startswith("#"):
+ if None in values:
+ continue
+
+ if values != last_values:
+ last_values = list(values)
+ if limit is None or counter < limit:
+ print(*values[:len(signals)], file=output)
+ counter += 1
+ continue
+
+ if line.startswith("b"):
+ value, id = line[1:].split()
+ else:
+ value, id = line[:1], line[1:]
+
+ pos = dump_pos.get(id)
+ if pos is None:
+ continue
+
+ values[pos] = value
+
+ if values != last_values:
+ if limit is None or counter < limit:
+ print(*values[:len(signals)], file=output)
+
+
+share = Path(__file__).parent / ".." / ".." / "share"
+
+simlibs = [str(share / "simlib.v"), str(share / "simcells.v")]
+
+if "prepare" in steps:
+ yosys(
+ """
+ read_verilog -icells uut.v
+ hierarchy -top uut; proc -noopt
+ write_rtlil uut.il
+ dump -o ports.list uut/x:*
+ """
+ )
+
+inputs = []
+outputs = []
+
+with open("ports.list") as ports_file:
+ for line in ports_file:
+ line = line.split()
+ if not line or line[0] != "wire":
+ continue
+ line = line[1:]
+ width = 1
+ if line[0] == "width":
+ width = int(line[1])
+ line = line[2:]
+ direction, seq, name = line
+ assert name.startswith("\\")
+ name = name[1:]
+ seq = int(seq)
+
+ if direction == "input":
+ inputs.append((seq, name, width))
+ else:
+ outputs.append((seq, name, width))
+
+inputs.sort()
+outputs.sort()
+
+input_width = sum(width for seq, name, width in inputs)
+output_width = sum(width for seq, name, width in outputs)
+
+if "prepare" in steps:
+ if args.seq:
+ patterns = [''.join(random.choices('01x', k=input_width)) for i in range(args.count)]
+ else:
+ if 3**input_width <= args.count * 2:
+ patterns = ["".join(bits) for bits in itertools.product(*["01x"] * input_width)]
+ else:
+ patterns = set()
+
+ for bit in '01x':
+ patterns.add(bit * input_width)
+
+ for bits in itertools.combinations('01x', 2):
+ for bit1, bit2 in itertools.permutations(bits):
+ for i in range(input_width):
+ pattern = [bit1] * input_width
+ pattern[i] = bit2
+ patterns.add(''.join(pattern))
+
+ for i, j in itertools.combinations(range(input_width), 2):
+ pattern = [bit1] * input_width
+ pattern[i] = bit2
+ pattern[j] = bit2
+ patterns.add(''.join(pattern))
+
+ for bit1, bit2, bit3 in itertools.permutations('01x'):
+ for i, j in itertools.combinations(range(input_width), 2):
+ pattern = [bit1] * input_width
+ pattern[i] = bit2
+ pattern[j] = bit3
+ patterns.add(''.join(pattern))
+
+ if len(patterns) > args.count // 2:
+ patterns = sorted(patterns)
+ random.shuffle(patterns)
+ patterns = set(patterns[:args.count // 2])
+
+ while len(patterns) < args.count:
+ pattern = ''.join(random.choices('01x', k=input_width))
+ patterns.add(pattern)
+
+ patterns = sorted(patterns)
+ with open("patterns.list", "w") as f:
+ for pattern in patterns:
+ print(pattern, file=f)
+else:
+ with open("patterns.list") as f:
+ patterns = [pattern.strip() for pattern in f]
+
+
+if "prepare" in steps:
+ with open("wrapper.v", "w") as wrapper_file:
+ print(
+ "module wrapper("
+ f"input [{input_width-1}:0] A, "
+ f"output [{output_width-1}:0] Y);",
+ file=wrapper_file,
+ )
+
+ connections = []
+ pos = 0
+ for seq, name, width in inputs:
+ connections.append(f".{name}(A[{pos+width-1}:{pos}])")
+ pos += width
+ pos = 0
+ for seq, name, width in outputs:
+ connections.append(f".{name}(Y[{pos+width-1}:{pos}])")
+ pos += width
+
+ print(f"uut uut({', '.join(connections)});", file=wrapper_file)
+ print("endmodule", file=wrapper_file)
+
+ yosys(
+ """
+ read_rtlil uut.il
+ read_verilog wrapper.v
+ hierarchy -top wrapper; proc -noopt
+ flatten; clean;
+ rename wrapper uut
+ write_rtlil wrapped.il
+ """
+ )
+
+ try:
+ yosys(
+ """
+ read_rtlil wrapped.il
+ dffunmap
+ xprop -required
+ check -assert
+ write_rtlil wrapped_xprop.il
+ """
+ )
+ except subprocess.CalledProcessError:
+ remove("wrapped_xprop.il")
+
+ with open("verilog_sim_tb.v", "w") as tb_file:
+ print("module top();", file=tb_file)
+ print(f"reg gclk;", file=tb_file)
+ print(f"reg [{input_width-1}:0] A;", file=tb_file)
+ print(f"wire [{output_width-1}:0] Y;", file=tb_file)
+ print(f"uut uut(.A(A), .Y(Y));", file=tb_file)
+ print("initial begin", file=tb_file)
+
+ for pattern in patterns:
+ print(
+ f' gclk = 1; #0; A[0] = 1\'b{pattern[-1]}; #0; A = {input_width}\'b{pattern}; #5; gclk = 0; $display("%b %b", A, Y); #5',
+ file=tb_file,
+ )
+
+ print(" $finish;", file=tb_file)
+ print("end", file=tb_file)
+ print("endmodule", file=tb_file)
+
+ with open("synth_tb.v", "w") as tb_file:
+ print("module top(input clk);", file=tb_file)
+ print(f"reg [{len(patterns).bit_length() - 1}:0] counter = 0;", file=tb_file)
+ print(f"reg [{input_width-1}:0] A;", file=tb_file)
+ print(f"(* gclk *) reg gclk;", file=tb_file)
+ print(f"wire [{output_width-1}:0] Y;", file=tb_file)
+ print(f"uut uut(.A(A), .Y(Y));", file=tb_file)
+ print(f"always @(posedge gclk) counter <= counter + 1;", file=tb_file)
+ print(f"always @* case (counter)", file=tb_file)
+ for i, pattern in enumerate(patterns):
+ print(f" {i:7} : A = {input_width}'b{pattern};", file=tb_file)
+ print(f" default : A = {input_width}'b{'x' * input_width};", file=tb_file)
+ print(f"endcase", file=tb_file)
+ print("endmodule", file=tb_file)
+
+ with open("const_tb.v", "w") as tb_file:
+ print("module top();", file=tb_file)
+ for i, pattern in enumerate(patterns):
+ print(
+ f"(* keep *) wire [{output_width-1}:0] Y_{i}; "
+ f"uut uut_{i}(.A({input_width}'b{pattern}), .Y(Y_{i}));",
+ file=tb_file,
+ )
+ print("endmodule", file=tb_file)
+
+if "verify" in steps:
+ try:
+ seq_args = " -tempinduct -set-init-undef" if args.seq else ""
+ yosys(
+ f"""
+ read_rtlil wrapped.il
+ copy uut gold
+ rename uut gate
+ design -push-copy
+ dffunmap
+ xprop -formal -split-inputs -required -debug-asserts gate
+ clk2fflogic
+ sat{seq_args} -enable_undef -set-def-inputs -prove-asserts -verify -show-all gate
+ design -pop
+
+ dffunmap
+ xprop -required -assume-encoding gate
+ miter -equiv -make_assert -flatten gold gate miter
+ clk2fflogic
+ sat{seq_args} -enable_undef -set-assumes -prove-asserts -verify -show-all miter
+ """
+ )
+ with open("verified", "w") as f:
+ pass
+ except subprocess.CalledProcessError:
+ remove("verified")
+
+
+for mode in ["", "_xprop"]:
+ if not Path(f"wrapped{mode}.il").is_file():
+ for expr in [f"expr{mode}", f"noexpr{mode}"]:
+ remove(f"vsim_{expr}.out")
+ continue
+
+ if "prepare" in steps:
+ yosys(
+ f"""
+ read_rtlil wrapped{mode}.il
+ chformal -remove
+ dffunmap
+ write_verilog -noparallelcase vsim_expr{mode}.v
+ write_verilog -noexpr vsim_noexpr{mode}.v
+ """
+ )
+
+ for expr in [f"expr{mode}", f"noexpr{mode}"]:
+ if f"vsim_{expr}" in steps:
+ subprocess.check_call(
+ [
+ "iverilog",
+ "-DSIMLIB_FF",
+ "-DSIMLIB_GLOBAL_CLOCK=top.gclk",
+ f"-DDUMPFILE=\"vsim_{expr}.vcd\"",
+ "verilog_sim_tb.v",
+ f"vsim_{expr}.v",
+ *simlibs,
+ "-o",
+ f"vsim_{expr}",
+ ]
+ )
+ with open(f"vsim_{expr}.out", "w") as f:
+ subprocess.check_call([f"./vsim_{expr}"], stdout=f)
+
+for mode in ["", "_xprop"]:
+ if f"sim{mode}" not in steps:
+ continue
+ if not Path(f"wrapped{mode}.il").is_file():
+ remove(f"sim{mode}.out")
+ continue
+ yosys(
+ f"""
+ read_verilog synth_tb.v
+ read_rtlil wrapped{mode}.il
+ hierarchy -top top; proc -noopt
+ dffunmap
+ sim -clock clk -n {len(patterns) // 2} -vcd sim{mode}.vcd top
+ """
+ )
+
+ with open(f"sim{mode}.vcd") as fin, open(f"sim{mode}.out", "w") as fout:
+ vcdextract(["top.A", "top.Y"], ["top.counter"], fin, fout, len(patterns))
+
+for mode in ["", "_xprop"]:
+ if f"sat{mode}" not in steps:
+ continue
+ if not Path(f"wrapped{mode}.il").is_file():
+ remove(f"sat{mode}.out")
+ continue
+ chunk_size = len(patterns) if args.seq else 32
+ last_progress = 0
+ with open(f"sat{mode}.ys", "w") as ys:
+ for chunk_start in range(0, len(patterns), chunk_size):
+ chunk = patterns[chunk_start : chunk_start + chunk_size]
+ progress = (10 * chunk_start) // len(patterns)
+ if progress > last_progress:
+ print(f"log sat {progress}0%", file=ys)
+ last_progress = progress
+
+ append = "-a" if chunk_start else "-o"
+ print(
+ end=f"tee -q {append} sat{mode}.log sat -set-init-undef -seq {len(chunk)}"
+ " -show A -show Y -dump_vcd sat.vcd -enable_undef",
+ file=ys,
+ )
+ for i, pattern in enumerate(chunk, 1):
+ ad = pattern.replace("x", "0")
+ ax = pattern.replace("1", "0").replace("x", "1")
+ print(end=f" -set-at {i} A {input_width}'b{pattern}", file=ys)
+ print(file=ys)
+ print(f"log sat 100%", file=ys)
+
+ try:
+ yosys(
+ f"""
+ read_rtlil wrapped{mode}.il
+ clk2fflogic
+ script sat{mode}.ys
+ """
+ )
+ except subprocess.CalledProcessError:
+ remove(f"sat{mode}.out")
+ else:
+ sig_re = re.compile(
+ r" *[0-9]+ +\\([AY]) +(?:--|[0-9]+) +(?:--|[0-9a-f]+) +([01x]+)"
+ )
+ current_input = None
+ with open(f"sat{mode}.log") as logfile, open(f"sat{mode}.out", "w") as outfile:
+ for line in logfile:
+ match = sig_re.match(line)
+ if match:
+ if match[1] == "A":
+ current_input = match[2]
+ else:
+ print(current_input, match[2], file=outfile)
+
+for mode in ["", "_xprop"]:
+ if f"opt_expr{mode}" not in steps:
+ continue
+ if not Path(f"wrapped{mode}.il").is_file():
+ remove(f"opt_expr{mode}.out")
+ continue
+ yosys(
+ f"""
+ read_verilog const_tb.v
+ read_rtlil wrapped{mode}.il
+ hierarchy -top top; proc -noopt
+ flatten
+ opt_expr -keepdc; clean
+ dump -o opt_expr{mode}.list */\Y_*
+ """
+ )
+
+ values = []
+
+ connect_re = re.compile(r" *connect +\\Y_([0-9]+) +[0-9]+'([01x]+)$")
+ with open(f"opt_expr{mode}.list") as connections:
+ for line in connections:
+ match = connect_re.match(line)
+ if match:
+ seq = int(match[1])
+ data = match[2]
+ if len(data) < output_width:
+ data = data * output_width
+ values.append((seq, data))
+
+ values.sort()
+
+ with open(f"opt_expr{mode}.out", "w") as outfile:
+ for seq, data in values:
+ print(patterns[seq], data, file=outfile)
+
+
+if "compare" in steps:
+ groups = {}
+ missing = []
+
+ for output in all_outputs:
+ try:
+ with open(f"{output}.out") as f:
+ groups.setdefault(f.read(), []).append(output)
+ except FileNotFoundError:
+ missing.append(output)
+
+ verified = Path(f"verified").is_file()
+
+ with open("status", "w") as status:
+ name = Path('.').absolute().name
+
+ status_list = []
+
+ if len(groups) > 1:
+ status_list.append("mismatch")
+ if not verified:
+ status_list.append("failed-verify")
+ if missing:
+ status_list.append("missing")
+ if not status_list:
+ status_list.append("ok")
+ print(f"{name}: {', '.join(status_list)}", file=status)
+
+ if len(groups) > 1:
+ print("output differences:", file=status)
+ for group in groups.values():
+ print(" -", *group, file=status)
+ if missing:
+ print("missing:", file=status)
+ print(" -", *missing, file=status)
+
+ with open("status") as status:
+ print(end=status.read())
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-22 15:17:55 +0000