#!/usr/bin/env bash
set -eu

source ../gen-tests-makefile.sh

ops="sqrt add sub mul div muladd"
for op in $ops; do
    rm -f ${op}_edges.*
done

prove_op() {
    op=$1
    defs=$2
    ys_file=${op}_edges.ys
    echo """\
symfpu -op $op
sat -prove-asserts -verify
chformal -remove
opt

read_verilog -sv -formal $defs edges.sv
chformal -lower
prep -top edges -flatten
sat -prove-asserts -verify
""" > $ys_file
}

prove_op sqrt "-DSQRT"
prove_op add "-DADD -DADDSUB -DADDS"
prove_op sub "-DSUB -DADDSUB -DADDS"
prove_op mul "-DMUL -DMULS"
prove_op div "-DDIV"
prove_op muladd "-DMULADD -DMULS -DADDS"

generate_mk --yosys-scripts