4 files changed, 54 insertions, 19 deletions
diff --git a/tests/verilog/.gitignore b/tests/verilog/.gitignore
index b48f808a1..34da23437 100644
--- a/tests/verilog/.gitignore
+++ b/tests/verilog/.gitignore
@@ -1,3 +1,5 @@
 /*.log
 /*.out
 /run-test.mk
+/const_arst.v
+/const_sr.v
diff --git a/tests/verilog/const_arst.ys b/tests/verilog/const_arst.ys
new file mode 100644
index 000000000..df720575c
--- /dev/null
+++ b/tests/verilog/const_arst.ys
@@ -0,0 +1,24 @@
+read_verilog <<EOT
+module test (
+	input clk, d,
+	output reg q
+);
+wire nop = 1'h0;
+always @(posedge clk, posedge nop) begin
+	if (nop) q <= 1'b0;
+	else q <= d;
+end
+endmodule
+EOT
+prep -top test
+write_verilog const_arst.v
+design -stash gold
+read_verilog const_arst.v
+prep -top test
+design -stash gate
+design -copy-from gold -as gold A:top
+design -copy-from gate -as gate A:top
+miter -equiv -flatten -make_assert gold gate miter
+prep -top miter
+clk2fflogic
+sat -set-init-zero -tempinduct -prove-asserts -verify
diff --git a/tests/verilog/const_sr.ys b/tests/verilog/const_sr.ys
new file mode 100644
index 000000000..c1406b0a0
--- /dev/null
+++ b/tests/verilog/const_sr.ys
@@ -0,0 +1,25 @@
+read_verilog <<EOT
+module test (
+	input clk, rst, d,
+	output reg q
+);
+wire nop = 1'h0;
+always @(posedge clk, posedge nop, posedge rst) begin
+	if (rst) q <= 1'b0;
+	else if (nop) q <= 1'b1;
+	else q <= d;
+end
+endmodule
+EOT
+prep -top test
+write_verilog const_sr.v
+design -stash gold
+read_verilog const_sr.v
+prep -top test
+design -stash gate
+design -copy-from gold -as gold A:top
+design -copy-from gate -as gate A:top
+miter -equiv -flatten -make_assert gold gate miter
+prep -top miter
+clk2fflogic
+sat -set-init-zero -tempinduct -prove-asserts -verify
diff --git a/tests/verilog/run-test.sh b/tests/verilog/run-test.sh
index ea56b70f0..2f91cf0fd 100755
--- a/tests/verilog/run-test.sh
+++ b/tests/verilog/run-test.sh
@@ -1,20 +1,4 @@
 #!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
-	echo "all:: run-$x"
-	echo "run-$x:"
-	echo "	@echo 'Running $x..'"
-	echo "	@../../yosys -ql ${x%.ys}.log $x"
-done
-for s in *.sh; do
-	if [ "$s" != "run-test.sh" ]; then
-		echo "all:: run-$s"
-		echo "run-$s:"
-		echo "	@echo 'Running $s..'"
-		echo "	@bash $s"
-	fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+set -eu
+source ../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash