tests/symfpu: Switch to generate_mk.py

tests/symfpu/generate_mk.py

@@ -0,0 +1,50 @@
+#!/usr/bin/env python3
+
+import sys
+sys.path.append("..")
+import gen_tests_makefile
+
+from pathlib import Path
+from textwrap import dedent
+
+cwd = Path.cwd()
+for path in cwd.glob("*_edges.*"):
+    path.unlink()
+
+for op, defs in {
+    # standard ops
+    "sqrt": "-DSQRT -DSQRTS",
+    "add": "-DADD -DADDSUB -DADDS",
+    "sub": "-DSUB -DADDSUB -DADDS",
+    "mul": "-DMUL -DMULS",
+    "div": "-DDIV -DDIVS",
+    "muladd": "-DMULADD -DMULS -DADDS",
+    # altops
+    "altdiv": "-DALTDIV -DDIVS",
+    "altsqrt": "-DALTSQRT -DSQRTS",
+    # unrounded
+    "min": "-DMIN -DCOMPARES",
+    "max": "-DMAX -DCOMPARES",
+}.items():
+    rms = ["DYN"]
+    dyn_only = op in ["min", "max"]
+    if not dyn_only:
+        rms.extend(["RNE", "RNA", "RTP", "RTN", "RTZ"])
+    for rm in rms:
+        with open(f"{op}_{rm}_edges.ys", "w") as ys:
+            print(f"symfpu -op {op} -rm {rm}", file=ys)
+            if rm != "DYN" or dyn_only:
+                print("sat -prove-asserts -verify", file=ys)
+            print(
+                dedent(f"""\
+                    chformal -remove
+                    opt
+
+                    read_verilog -sv -formal {defs} -D{rm} edges.sv
+                    chformal -remove -cover
+                    chformal -lower
+                    prep -top edges -flatten
+                    sat -set-assumes -prove-asserts -verify"""
+                ), file=ys)
+
+gen_tests_makefile.generate(["--yosys-scripts"])

tests/symfpu/run-test.sh

@@ -1,59 +0,0 @@
-#!/usr/bin/env bash
-set -eu
-
-source ../gen-tests-makefile.sh
-
-rm -f *_edges.*
-
-prove_rm() {
-    op=$1
-    rm=$2
-    defs=$3
-    ys_file=${op}_${rm}_edges.ys
-    echo "symfpu -op $op -rm $rm" > $ys_file
-    if [[ $rm != "DYN" ]] then
-        echo "sat -prove-asserts -verify" >> $ys_file
-    fi
-    echo """\
-chformal -remove
-opt
-
-read_verilog -sv -formal $defs -D${rm} edges.sv
-chformal -remove -cover
-chformal -lower
-prep -top edges -flatten
-sat -set-assumes -prove-asserts -verify
-""" >> $ys_file
-}
-
-prove_op() {
-    op=$1
-    defs=$2
-    rms="RNE RNA RTP RTN RTZ DYN"
-    for rm in $rms; do
-        prove_rm $op $rm "$defs"
-    done
-}
-
-prove_op_unrounded() {
-    # DYN is default rounding mode, so this is (currently) equivalent to no rounding mode
-    # but this does skip verifying the built in asserts
-    op=$1
-    defs=$2
-    prove_rm $op "DYN" "$defs"
-}
-
-prove_op sqrt "-DSQRT -DSQRTS"
-prove_op add "-DADD -DADDSUB -DADDS"
-prove_op sub "-DSUB -DADDSUB -DADDS"
-prove_op mul "-DMUL -DMULS"
-prove_op div "-DDIV -DDIVS"
-prove_op muladd "-DMULADD -DMULS -DADDS"
-
-prove_op altdiv "-DALTDIV -DDIVS"
-prove_op altsqrt "-DALTSQRT -DSQRTS"
-
-prove_op_unrounded min "-DMIN -DCOMPARES"
-prove_op_unrounded max "-DMAX -DCOMPARES"
-
-generate_mk --yosys-scripts