Convert gen-tests shell script to python

tests/aiger/generate_mk.py

@@ -0,0 +1,68 @@
+#!/usr/bin/env python3
+
+import glob
+import os
+
+yosys = "../../yosys"
+default_abc = "../../yosys-abc"
+
+aags = sorted(glob.glob("*.aag"))
+yss = sorted(glob.glob("*.ys"))
+
+print("ABC ?= " + default_abc)
+print("YOSYS ?= " + yosys)
+print()
+
+def base(fn):
+    return os.path.splitext(fn)[0]
+
+# NB: *.aag and *.aig must contain a symbol table naming the primary
+#     inputs and outputs, otherwise ABC and Yosys will name them
+#     arbitrarily (and inconsistently with each other).
+
+# Since ABC cannot read *.aag, read the *.aig instead
+# (which would have been created by the reference aig2aig utility,
+#  available from http://fmv.jku.at/aiger/)
+
+for aag in aags:
+    b = base(aag)
+
+    print(f"all: {aag}")
+    print(f".PHONY: {aag}")
+    print(f"{aag}:")
+    print(f"\t@echo Checking {aag}.")
+    print(f"\t@$(ABC) -q \"read -c {b}.aig; write {b}_ref.v\" >/dev/null 2>&1")
+    print("\t@$(YOSYS) -qp \"\\")
+    print(f"\tread_verilog {b}_ref.v; \\")
+    print("\tprep; \\")
+    print("\tdesign -stash gold; \\")
+    print(f"\tread_aiger -clk_name clock {aag}; \\")
+    print("\tprep; \\")
+    print("\tdesign -stash gate; \\")
+    print("\tdesign -import gold -as gold; \\")
+    print("\tdesign -import gate -as gate; \\")
+    print("\tmiter -equiv -flatten -make_assert -make_outputs gold gate miter; \\")
+    print("\tsat -verify -prove-asserts -show-ports -seq 16 miter; \\")
+    print(f"\t\" -l {aag}.log >/dev/null 2>&1")
+    print()
+
+# ---- Yosys script tests ----
+for ys in yss:
+    b = base(ys)
+    print(f"all: {ys}")
+    print(f".PHONY: {ys}")
+    print(f"{ys}: ")
+    print(f"\t@echo Running {ys}.")
+    print(f"\t@$(YOSYS) -ql {b}.log {ys} >/dev/null 2>&1")
+    print()
+
+# ---- aigmap test ----
+print(f"all: aigmap")
+print(f".PHONY: aigmap")
+print("aigmap:")
+print("\t@echo Running aigmap.")
+print("\t@rm -rf gate; mkdir gate")
+print('\t@$(YOSYS) --no-version -p "test_cell -aigmap -w gate/ -n 1 -s 1 all" >/dev/null 2>&1')
+print("\t@set -o pipefail; diff --brief gold gate | tee aigmap.err")
+print("\t@rm -f aigmap.err")
+print()