Update tests and test infrastructure

.github/workflows/test-verific.yml

@@ -78,7 +78,7 @@ jobs:
       - name: Run Verific specific Yosys tests
         run: |
           make -C tests/sva
-          cd tests/svtypes && bash run-test.sh
+          make -C tests/svtypes
 
       - name: Run SBY tests
         if: ${{ github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' }}

Makefile

@@ -918,111 +918,15 @@ else
 ABCOPT=""
 endif
 
-# Tests that generate .mk with tests/gen-tests-makefile.sh
-MK_TEST_DIRS =
-MK_TEST_DIRS += tests/arch/analogdevices
-MK_TEST_DIRS += tests/arch/anlogic
-MK_TEST_DIRS += tests/arch/ecp5
-MK_TEST_DIRS += tests/arch/efinix
-MK_TEST_DIRS += tests/arch/gatemate
-MK_TEST_DIRS += tests/arch/gowin
-MK_TEST_DIRS += tests/arch/ice40
-MK_TEST_DIRS += tests/arch/intel_alm
-MK_TEST_DIRS += tests/arch/machxo2
-MK_TEST_DIRS += tests/arch/microchip
-MK_TEST_DIRS += tests/arch/nanoxplore
-MK_TEST_DIRS += tests/arch/nexus
-MK_TEST_DIRS += tests/arch/quicklogic/pp3
-MK_TEST_DIRS += tests/arch/quicklogic/qlf_k6n10f
-MK_TEST_DIRS += tests/arch/xilinx
-MK_TEST_DIRS += tests/bugpoint
-MK_TEST_DIRS += tests/opt
-MK_TEST_DIRS += tests/sat
-MK_TEST_DIRS += tests/sdc
-MK_TEST_DIRS += tests/sim
-MK_TEST_DIRS += tests/svtypes
-MK_TEST_DIRS += tests/techmap
-MK_TEST_DIRS += tests/various
-MK_TEST_DIRS += tests/rtlil
-ifeq ($(ENABLE_VERIFIC),1)
-ifneq ($(YOSYS_NOVERIFIC),1)
-MK_TEST_DIRS += tests/verific
-endif
-endif
-MK_TEST_DIRS += tests/verilog
-
-# Tests that don't generate .mk
-SH_TEST_DIRS =
-SH_TEST_DIRS += tests/arith_tree
-SH_TEST_DIRS += tests/simple
-SH_TEST_DIRS += tests/simple_abc9
-SH_TEST_DIRS += tests/hana
-SH_TEST_DIRS += tests/asicworld
-# SH_TEST_DIRS += tests/realmath
-SH_TEST_DIRS += tests/share
-SH_TEST_DIRS += tests/opt_share
-SH_TEST_DIRS += tests/fsm
-SH_TEST_DIRS += tests/memlib
-SH_TEST_DIRS += tests/bram
-SH_TEST_DIRS += tests/svinterfaces
-SH_TEST_DIRS += tests/xprop
-SH_TEST_DIRS += tests/select
-SH_TEST_DIRS += tests/peepopt
-SH_TEST_DIRS += tests/proc
-SH_TEST_DIRS += tests/blif
-SH_TEST_DIRS += tests/arch
-SH_TEST_DIRS += tests/rpc
-SH_TEST_DIRS += tests/memfile
-SH_TEST_DIRS += tests/fmt
-SH_TEST_DIRS += tests/cxxrtl
-SH_TEST_DIRS += tests/liberty
-ifeq ($(ENABLE_FUNCTIONAL_TESTS),1)
-SH_TEST_DIRS += tests/functional
-endif
-
-# Tests that don't generate .mk and need special args
-SH_ABC_TEST_DIRS =
-SH_ABC_TEST_DIRS += tests/memories
-SH_ABC_TEST_DIRS += tests/aiger
-SH_ABC_TEST_DIRS += tests/alumacc
-
-# seed-tests/ is a dummy string, not a directory
-.PHONY: seed-tests
-seed-tests: $(SH_TEST_DIRS:%=seed-tests/%)
-.PHONY: seed-tests/%
-seed-tests/%: %/run-test.sh $(TARGETS) $(EXTRA_TARGETS)
-	+cd $* && bash run-test.sh $(SEEDOPT)
-	+@echo "...passed tests in $*"
-
-# abcopt-tests/ is a dummy string, not a directory
-.PHONY: abcopt-tests
-abcopt-tests: $(SH_ABC_TEST_DIRS:%=abcopt-tests/%)
-abcopt-tests/%: %/run-test.sh $(TARGETS) $(EXTRA_TARGETS)
-	+cd $* && bash run-test.sh $(ABCOPT) $(SEEDOPT)
-	+@echo "...passed tests in $*"
-
-# makefile-tests/ is a dummy string, not a directory
-.PHONY: makefile-tests
-makefile-tests: $(MK_TEST_DIRS:%=makefile-tests/%)
-# this target actually emits .mk files
-%.mk:
-	+cd $(dir $*) && bash run-test.sh
-# this one spawns submake on each
-makefile-tests/%: %/run-test.mk $(TARGETS) $(EXTRA_TARGETS)
-	$(MAKE) -C $* -f run-test.mk
-	+@echo "...passed tests in $*"
-
 test: vanilla-test unit-test
 
-vanilla-test: makefile-tests abcopt-tests seed-tests
-	@echo ""
-	@echo "  Passed \"make vanilla-test\"."
-ifeq ($(ENABLE_VERIFIC),1)
-ifeq ($(YOSYS_NOVERIFIC),1)
-	@echo "  Ran tests without verific support due to YOSYS_NOVERIFIC=1."
-endif
-endif
-	@echo ""
+.PHONY: vanilla-test
+
+vanilla-test: $(TARGETS) $(EXTRA_TARGETS)
+	@$(MAKE) -C tests vanilla-test \
+	$(if $(ENABLE_VERIFIC),ENABLE_VERIFIC=$(ENABLE_VERIFIC)) \
+	$(if $(YOSYS_NOVERIFIC),YOSYS_NOVERIFIC=$(YOSYS_NOVERIFIC)) \
+	SEEDOPT=$(SEEDOPT) ABCOPT=$(ABCOPT)
 
 VALGRIND ?= valgrind --error-exitcode=1 --leak-check=full --show-reachable=yes --errors-for-leak-kinds=all
 
@@ -1188,16 +1092,8 @@ clean: clean-py clean-unit-test
 	rm -f $(OBJS) $(GENFILES) $(TARGETS) $(EXTRA_TARGETS) $(EXTRA_OBJS)
 	rm -f kernel/version_*.o kernel/version_*.cc
 	rm -f libs/*/*.d frontends/*/*.d passes/*/*.d backends/*/*.d kernel/*.d techlibs/*/*.d
-	rm -rf tests/asicworld/*.out tests/asicworld/*.log
-	rm -rf tests/hana/*.out tests/hana/*.log
-	rm -rf tests/simple/*.out tests/simple/*.log
-	rm -rf tests/memories/*.out tests/memories/*.log tests/memories/*.dmp
-	rm -rf tests/sat/*.log tests/techmap/*.log tests/various/*.log
-	rm -rf tests/bram/temp tests/fsm/temp tests/realmath/temp tests/share/temp tests/smv/temp tests/various/temp
 	rm -rf vloghtb/Makefile vloghtb/refdat vloghtb/rtl vloghtb/scripts vloghtb/spec vloghtb/check_yosys vloghtb/vloghammer_tb.tar.bz2 vloghtb/temp vloghtb/log_test_*
-	rm -f tests/svinterfaces/*.log_stdout tests/svinterfaces/*.log_stderr tests/svinterfaces/dut_result.txt tests/svinterfaces/reference_result.txt tests/svinterfaces/a.out tests/svinterfaces/*_syn.v tests/svinterfaces/*.diff
-	rm -f  tests/tools/cmp_tbdata
-	rm -f $(addsuffix /run-test.mk,$(MK_TEST_DIRS))
+	-$(MAKE) -C $(YOSYS_SRC)/tests clean
 	-$(MAKE) -C $(YOSYS_SRC)/docs clean
 	rm -rf docs/util/__pycache__
 	rm -f libyosys.so

tests/.gitignore

@@ -2,3 +2,5 @@
 *.out
 *.err
 run-test.mk
+**/Makefile
+*.result

tests/Makefile

@@ -0,0 +1,127 @@
+ifneq ($(wildcard ../Makefile.conf),)
+include ../Makefile.conf
+endif
+
+OVERRIDE_MAIN=1
+include ./common.mk
+
+# Directories with tests not run:
+#  errors
+#  lut
+#  pyosys
+#  smv
+#  sva
+#  tools
+#  unit
+#  vloghtb
+
+# Tests that generate Makefile with gen_tests_makefile.py
+MK_TEST_DIRS =
+MK_TEST_DIRS += ./arch/analogdevices
+MK_TEST_DIRS += ./arch/anlogic
+MK_TEST_DIRS += ./arch/ecp5
+MK_TEST_DIRS += ./arch/efinix
+MK_TEST_DIRS += ./arch/fabulous
+MK_TEST_DIRS += ./arch/gatemate
+MK_TEST_DIRS += ./arch/gowin
+MK_TEST_DIRS += ./arch/ice40
+MK_TEST_DIRS += ./arch/intel_alm
+MK_TEST_DIRS += ./arch/machxo2
+MK_TEST_DIRS += ./arch/microchip
+MK_TEST_DIRS += ./arch/nanoxplore
+MK_TEST_DIRS += ./arch/nexus
+MK_TEST_DIRS += ./arch/quicklogic/pp3
+MK_TEST_DIRS += ./arch/quicklogic/qlf_k6n10f
+MK_TEST_DIRS += ./arch/xilinx
+MK_TEST_DIRS += ./bind
+MK_TEST_DIRS += ./bugpoint
+MK_TEST_DIRS += ./opt
+MK_TEST_DIRS += ./sat
+MK_TEST_DIRS += ./sdc
+MK_TEST_DIRS += ./sim
+MK_TEST_DIRS += ./svtypes
+MK_TEST_DIRS += ./techmap
+MK_TEST_DIRS += ./various
+MK_TEST_DIRS += ./rtlil
+ifeq ($(ENABLE_VERIFIC),1)
+ifneq ($(YOSYS_NOVERIFIC),1)
+MK_TEST_DIRS += ./verific
+endif
+endif
+MK_TEST_DIRS += ./verilog
+MK_TEST_DIRS += ./arith_tree
+MK_TEST_DIRS += ./simple
+MK_TEST_DIRS += ./simple_abc9
+MK_TEST_DIRS += ./hana
+MK_TEST_DIRS += ./asicworld
+MK_TEST_DIRS += ./realmath
+MK_TEST_DIRS += ./share
+MK_TEST_DIRS += ./opt_share
+MK_TEST_DIRS += ./fsm
+MK_TEST_DIRS += ./memlib
+MK_TEST_DIRS += ./bram
+MK_TEST_DIRS += ./svinterfaces
+MK_TEST_DIRS += ./xprop
+MK_TEST_DIRS += ./select
+MK_TEST_DIRS += ./peepopt
+MK_TEST_DIRS += ./proc
+MK_TEST_DIRS += ./blif
+MK_TEST_DIRS += ./arch
+MK_TEST_DIRS += ./rpc
+MK_TEST_DIRS += ./memfile
+MK_TEST_DIRS += ./fmt
+MK_TEST_DIRS += ./cxxrtl
+MK_TEST_DIRS += ./liberty
+#ifeq ($(ENABLE_FUNCTIONAL_TESTS),1)
+#MK_TEST_DIRS += ./functional
+#endif
+MK_TEST_DIRS += ./memories
+MK_TEST_DIRS += ./aiger
+MK_TEST_DIRS += ./alumacc
+
+all: vanilla-test
+
+# makefile-./ is a dummy string, not a directory
+.PHONY: makefile-tests
+.SILENT: $(MK_TEST_DIRS:%=%/Makefile)
+makefile-tests: $(MK_TEST_DIRS:%=makefile-./%)
+prep: $(MK_TEST_DIRS:%=%/Makefile)
+	@echo "All Makefiles generated."
+
+.PHONY: force-create
+# this target actually emits Makefile files
+%/Makefile: force-create
+	+@cd $* && python3 generate_mk.py
+
+makefile-./%: %/Makefile
+	@$(MAKE) -C $*
+	@echo "...passed tests in $*"
+
+.PHONY: functional
+functional:
+ifeq ($(ENABLE_FUNCTIONAL_TESTS),1)
+	@cd functional && ./run-test.sh
+endif
+
+vanilla-test: prep makefile-tests functional
+	@echo ""
+	@echo "  Passed \"make vanilla-test\"."
+ifeq ($(ENABLE_VERIFIC),1)
+ifeq ($(YOSYS_NOVERIFIC),1)
+	@echo "  Ran tests without verific support due to YOSYS_NOVERIFIC=1."
+endif
+endif
+	@echo ""
+	@$(MAKE) --no-print-directory summary
+
+clean:
+	@rm -rf ./asicworld/*.out ./asicworld/*.log
+	@rm -rf ./hana/*.out ./hana/*.log
+	@rm -rf ./simple/*.out ./simple/*.log
+	@rm -rf ./memories/*.out ./memories/*.log ./memories/*.dmp
+	@rm -rf ./sat/*.log ./techmap/*.log ./various/*.log
+	@rm -rf ./bram/temp ./fsm/temp ./realmath/temp ./share/temp ./smv/temp ./various/temp
+	@rm -f ./svinterfaces/*.log_stdout ./svinterfaces/*.log_stderr ./svinterfaces/dut_result.txt ./svinterfaces/reference_result.txt ./svinterfaces/a.out ./svinterfaces/*_syn.v ./svinterfaces/*.diff
+	@rm -f  ./tools/cmp_tbdata
+	@rm -f $(addsuffix /Makefile,$(MK_TEST_DIRS))
+	@find . -name '*.result' -type f -exec rm -f {} +

tests/aiger/generate_mk.py

@@ -0,0 +1,59 @@
+#!/usr/bin/env python3
+
+import sys
+sys.path.append("..")
+
+import gen_tests_makefile
+
+import glob
+import os
+
+def base(fn):
+    return os.path.splitext(fn)[0]
+
+def cmd(lines):
+    return " \\\n".join(lines)
+
+# 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/)
+def create_tests():
+    aags = sorted(glob.glob("*.aag"))
+    yss = sorted(glob.glob("*.ys"))
+    for aag in aags:
+        b = base(aag)
+
+        gen_tests_makefile.generate_target(aag, cmd([
+            f"$(ABC) -q \"read -c {b}.aig; write {b}_ref.v\";",
+            "$(YOSYS) -qp \"",
+            f"read_verilog {b}_ref.v;",
+            "prep;",
+            "design -stash gold;",
+            f"read_aiger -clk_name clock {aag};",
+            "prep;",
+            "design -stash gate;",
+            "design -import gold -as gold;",
+            "design -import gate -as gate;",
+            "miter -equiv -flatten -make_assert -make_outputs gold gate miter;",
+            "sat -verify -prove-asserts -show-ports -seq 16 miter;",
+            f"\" -l {aag}.log"
+        ]))
+
+    # ---- Yosys script tests ----
+    for ys in yss:
+        gen_tests_makefile.generate_ys_test(ys)
+
+    gen_tests_makefile.generate_target("aigmap", cmd([
+        "rm -rf gate; mkdir gate;",
+        "$(YOSYS) --no-version -p \"test_cell -aigmap -w gate/ -n 1 -s 1 all\";",
+        "set -o pipefail; diff --brief gold gate | tee aigmap.err;",
+        "rm -f aigmap.err"
+    ]))
+
+extra = [ f"ABC ?= {gen_tests_makefile.yosys_basedir}/yosys-abc", "SHELL := /bin/bash" ]
+
+gen_tests_makefile.generate_custom(create_tests, extra)