New xprop pass to encode 3-valued x-propagation using 2-valued logic

4 files changed, 801 insertions, 0 deletions

diff --git a/tests/xprop/.gitignore b/tests/xprop/.gitignore
new file mode 100644
index 000000000..ff0b65b54
--- /dev/null
+++ b/tests/xprop/.gitignore
@@ -0,0 +1,2 @@
+/xprop_*
+/run-test.mk
diff --git a/tests/xprop/generate.py b/tests/xprop/generate.py
new file mode 100644
index 000000000..eef8dc36e
--- /dev/null
+++ b/tests/xprop/generate.py
@@ -0,0 +1,278 @@
+import os
+import re
+import sys
+import random
+import argparse
+
+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('-f', '--filter', default='', help='regular expression to filter tests to generate')
+args = parser.parse_args()
+
+if args.seed is None:
+    args.seed = random.randrange(1 << 32)
+
+print(f"xprop PRNG seed: {args.seed}")
+
+makefile = open("run-test.mk", "w")
+
+def add_test(name, src, seq=False):
+    if not re.search(args.filter, name):
+        return
+    workdir = f"xprop_{name}"
+
+    os.makedirs(workdir, exist_ok=True)
+    with open(f"{workdir}/uut.v", "w") as uut:
+        print(src, file=uut)
+    print(f"all: {workdir}", file=makefile)
+    print(f".PHONY: {workdir}", file=makefile)
+    print(f"{workdir}:", file=makefile)
+    seq_arg = " -s" if seq else ""
+    print(
+        f"\t@cd {workdir} && python3 -u ../test.py -S {args.seed} -c {args.count}{seq_arg} > test.log 2>&1 || echo {workdir}: failed > status\n"
+        f"\t@cat {workdir}/status\n"
+        # f"\t@grep '^.*: ok' {workdir}/status\n"
+        ,
+        file=makefile,
+    )
+
+def cell_test(name, cell, inputs, outputs, params, initial={}, defclock=False, seq=False):
+    ports = []
+    port_conns = []
+    for inport, width in inputs.items():
+        ports.append(f"input [{width-1}:0] {inport}")
+        if defclock and inport in ["C", "CLK"]:
+            port_conns.append(f".{inport}({inport} !== 0)")
+        else:
+            port_conns.append(f".{inport}({inport})")
+    for outport, width in outputs.items():
+        reg = " reg" if outport in initial else ""
+        ports.append(f"output{reg} [{width-1}:0] {outport}")
+        port_conns.append(f".{outport}({outport})")
+    param_defs = []
+    for param, value in params.items():
+        param_defs.append(f".{param}({value})")
+    initials = []
+    # for port, value in initial.items():
+    #     initials.append(f"initial {port} = {value};\n")
+    add_test(name,
+        f"module uut({', '.join(ports)});\n"
+        f"\\${cell} #({', '.join(param_defs)}) cell ({', '.join(port_conns)});\n"
+        f"{''.join(initials)}"
+        "endmodule",
+        seq=seq,
+    )
+
+def unary_test(cell, width, signed, out_width):
+    add_test(
+        f"{cell}_{width}{'us'[signed]}_{out_width}",
+        f"module uut(input [{width-1}:0] A, output [{out_width}-1:0] Y);\n"
+        f"\\${cell} #(.A_WIDTH({width}), .A_SIGNED({int(signed)}), .Y_WIDTH({out_width}))"
+        " cell (.A(A), .Y(Y));\n"
+        "endmodule",
+    )
+
+def binary_test(cell, a_width, b_width, signed, out_width):
+    add_test(
+        f"{cell}_{a_width}{'us'[signed]}{b_width}_{out_width}",
+        f"module uut(input [{a_width-1}:0] A, input [{b_width-1}:0] B, output [{out_width}-1:0] Y);\n"
+        f"\\${cell} #(.A_WIDTH({a_width}), .A_SIGNED({int(signed)}), .B_WIDTH({b_width}), .B_SIGNED({int(signed)}), .Y_WIDTH({out_width}))"
+        " cell (.A(A), .B(B), .Y(Y));\n"
+        "endmodule",
+    )
+
+def shift_test(cell, a_width, b_width, a_signed, b_signed, out_width):
+    add_test(
+        f"{cell}_{a_width}{'us'[a_signed]}{b_width}{'us'[b_signed]}_{out_width}",
+        f"module uut(input [{a_width-1}:0] A, input [{b_width-1}:0] B, output [{out_width}-1:0] Y);\n"
+        f"\\${cell} #(.A_WIDTH({a_width}), .A_SIGNED({int(a_signed)}), .B_WIDTH({b_width}), .B_SIGNED({int(b_signed)}), .Y_WIDTH({out_width}))"
+        " cell (.A(A), .B(B), .Y(Y));\n"
+        "endmodule",
+    )
+
+def mux_test(width):
+    cell_test(f"mux_{width}", 'mux', {"A": width, "B": width, "S": 1}, {"Y": width}, {"WIDTH": width})
+
+def bmux_test(width, s_width):
+    cell_test(f"bmux_{width}_{s_width}", 'bmux', {"A": width << s_width, "S": s_width}, {"Y": width}, {"WIDTH": width, "S_WIDTH": s_width})
+
+def demux_test(width, s_width):
+    cell_test(f"demux_{width}_{s_width}", 'demux', {"A": width, "S": s_width}, {"Y": width << s_width}, {"WIDTH": width, "S_WIDTH": s_width})
+
+def pmux_test(width, s_width):
+    cell_test(f"pmux_{width}_{s_width}", 'pmux', {"A": width, "B": width * s_width, "S": s_width}, {"Y": width}, {"WIDTH": width, "S_WIDTH": s_width})
+
+def bwmux_test(width):
+    cell_test(f"bwmux_{width}", 'bwmux', {"A": width, "B": width, "S": width}, {"Y": width}, {"WIDTH": width})
+
+def bweqx_test(width):
+    cell_test(f"bweqx_{width}", 'bweqx', {"A": width, "B": width}, {"Y": width}, {"WIDTH": width})
+
+def ff_test(width):
+    cell_test(f"ff_{width}", 'ff', {"D": width}, {"Q": width}, {"WIDTH": width}, seq=True)
+
+def dff_test(width, pol, defclock):
+    cell_test(f"dff_{width}{'np'[pol]}{'xd'[defclock]}", 'dff', {"CLK": 1, "D": width}, {"Q": width}, {"WIDTH": width, "CLK_POLARITY": int(pol)}, defclock=defclock, seq=True)
+
+def dffe_test(width, pol, enpol, defclock):
+    cell_test(f"dffe_{width}{'np'[pol]}{'np'[enpol]}{'xd'[defclock]}", 'dffe', {"CLK": 1, "EN": 1, "D": width}, {"Q": width}, {"WIDTH": width, "CLK_POLARITY": int(pol), "EN_POLARITY": int(enpol)}, defclock=defclock, seq=True)
+
+
+print(".PHONY: all", file=makefile)
+print("all:\n\t@echo done\n", file=makefile)
+
+for cell in ["not", "pos", "neg"]:
+    unary_test(cell, 1, False, 1)
+    unary_test(cell, 3, False, 3)
+    unary_test(cell, 3, True, 3)
+    unary_test(cell, 3, True, 1)
+    unary_test(cell, 3, False, 5)
+    unary_test(cell, 3, True, 5)
+
+for cell in ["and", "or", "xor", "xnor"]:
+    binary_test(cell, 1, 1, False, 1)
+    binary_test(cell, 1, 1, True, 2)
+    binary_test(cell, 2, 2, False, 2)
+    binary_test(cell, 2, 2, False, 1)
+    binary_test(cell, 2, 1, False, 2)
+    binary_test(cell, 2, 1, False, 1)
+
+# [, "pow"] are not implemented yet
+for cell in ["add", "sub", "mul", "div", "mod", "divfloor", "modfloor"]:
+    binary_test(cell, 1, 1, False, 1)
+    binary_test(cell, 1, 1, False, 2)
+    binary_test(cell, 3, 3, False, 1)
+    binary_test(cell, 3, 3, False, 3)
+    binary_test(cell, 3, 3, False, 6)
+    binary_test(cell, 3, 3, True, 1)
+    binary_test(cell, 3, 3, True, 3)
+    binary_test(cell, 3, 3, True, 6)
+    binary_test(cell, 5, 3, False, 3)
+    binary_test(cell, 5, 3, True, 3)
+
+for cell in ["lt", "le", "eq", "ne", "eqx", "nex", "ge", "gt"]:
+    binary_test(cell, 1, 1, False, 1)
+    binary_test(cell, 1, 1, False, 2)
+    binary_test(cell, 3, 3, False, 1)
+    binary_test(cell, 3, 3, False, 2)
+    binary_test(cell, 3, 3, True, 1)
+    binary_test(cell, 3, 3, True, 2)
+    binary_test(cell, 5, 3, False, 1)
+    binary_test(cell, 5, 3, True, 1)
+    binary_test(cell, 5, 3, False, 2)
+    binary_test(cell, 5, 3, True, 2)
+
+for cell in ["reduce_and", "reduce_or", "reduce_xor", "reduce_xnor"]:
+    unary_test(cell, 1, False, 1)
+    unary_test(cell, 3, False, 1)
+    unary_test(cell, 3, True, 1)
+    unary_test(cell, 3, False, 3)
+    unary_test(cell, 3, True, 3)
+
+for cell in ["reduce_bool", "logic_not"]:
+    unary_test(cell, 1, False, 1)
+    unary_test(cell, 3, False, 3)
+    unary_test(cell, 3, True, 3)
+    unary_test(cell, 3, True, 1)
+
+for cell in ["logic_and", "logic_or"]:
+    binary_test(cell, 1, 1, False, 1)
+    binary_test(cell, 3, 3, False, 3)
+    binary_test(cell, 3, 3, True, 3)
+    binary_test(cell, 3, 3, True, 1)
+
+for cell in ["shl", "shr", "sshl", "sshr", "shift"]:
+    shift_test(cell, 2, 1, False, False, 2)
+    shift_test(cell, 2, 1, True, False, 2)
+    shift_test(cell, 2, 1, False, False, 4)
+    shift_test(cell, 2, 1, True, False, 4)
+    shift_test(cell, 4, 2, False, False, 4)
+    shift_test(cell, 4, 2, True, False, 4)
+    shift_test(cell, 4, 2, False, False, 8)
+    shift_test(cell, 4, 2, True, False, 8)
+    shift_test(cell, 4, 3, False, False, 3)
+    shift_test(cell, 4, 3, True, False, 3)
+
+for cell in ["shift"]:
+    shift_test(cell, 2, 1, False, True, 2)
+    shift_test(cell, 2, 1, True, True, 2)
+    shift_test(cell, 2, 1, False, True, 4)
+    shift_test(cell, 2, 1, True, True, 4)
+    shift_test(cell, 4, 2, False, True, 4)
+    shift_test(cell, 4, 2, True, True, 4)
+    shift_test(cell, 4, 2, False, True, 8)
+    shift_test(cell, 4, 2, True, True, 8)
+    shift_test(cell, 4, 3, False, True, 3)
+    shift_test(cell, 4, 3, True, True, 3)
+
+for cell in ["shiftx"]:
+    shift_test(cell, 2, 1, False, True, 2)
+    shift_test(cell, 2, 1, False, True, 4)
+    shift_test(cell, 4, 2, False, True, 4)
+    shift_test(cell, 4, 2, False, True, 8)
+    shift_test(cell, 4, 3, False, True, 3)
+
+mux_test(1)
+mux_test(3)
+
+bmux_test(1, 2)
+bmux_test(2, 2)
+bmux_test(3, 1)
+
+demux_test(1, 2)
+demux_test(2, 2)
+demux_test(3, 1)
+
+pmux_test(1, 4)
+pmux_test(2, 2)
+pmux_test(3, 1)
+pmux_test(4, 4)
+
+bwmux_test(1)
+bwmux_test(3)
+
+bweqx_test(1)
+bweqx_test(3)
+
+ff_test(1)
+ff_test(3)
+
+dff_test(1, True, True)
+dff_test(1, False, True)
+dff_test(3, True, True)
+dff_test(3, False, True)
+
+# dff_test(1, True, False)  # TODO support x clocks
+# dff_test(1, False, False)  # TODO support x clocks
+# dff_test(3, True, False)  # TODO support x clocks
+# dff_test(3, False, False)  # TODO support x clocks
+
+dffe_test(1, True, False, True)
+dffe_test(1, False, False, True)
+dffe_test(3, True, False, True)
+dffe_test(3, False, False, True)
+dffe_test(1, True, True, True)
+dffe_test(1, False, True, True)
+dffe_test(3, True, True, True)
+dffe_test(3, False, True, True)
+
+
+
+# TODO "shift", "shiftx"
+
+# TODO "fa", "lcu", "alu", "macc", "lut", "sop"
+
+# TODO "slice", "concat"
+
+# TODO "tribuf", "specify2", "specify3", "specrule"
+
+# TODO "assert", "assume", "live", "fair", "cover", "initstate", "anyconst", "anyseq", "anyinit", "allconst", "allseq", "equiv",
+
+# TODO "bweqx", "bwmux"
+
+# TODO "sr", "ff", "dff", "dffe", "dffsr", "sffsre", "adff", "aldff", "sdff", "adffe", "aldffe", "sdffe", "sdffce", "dlatch", "adlatch", "dlatchsr"
+
+# TODO "fsm"
+
+# TODO "memrd", "memrd_v2", "memwr", "memwr_v2", "meminit", "meminit_v2", "mem", "mem_v2"
diff --git a/tests/xprop/run-test.sh b/tests/xprop/run-test.sh
new file mode 100755
index 000000000..1fc7e10b6
--- /dev/null
+++ b/tests/xprop/run-test.sh
@@ -0,0 +1,5 @@
+#!/bin/bash
+set -e
+
+python3 generate.py $@
+make -f run-test.mk
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())