c2v

#!/bin/bash
#
# Cryptol to acirc optimized by ABC
#

set -e

scriptdir=$(dirname $(realpath "${BASH_SOURCE[0]}"))
liberty_file=$scriptdir/../liberties/gc_cells.lib
opt_binary=""
ty="acirc"

usage () {
    echo "C2V: Cryptol to acirc through Verilog"
    echo "Usage: $0 [options] <cryptol-file> <function>"
    echo "  -b              output binary netlist instead of acirc"
    echo "  -l LIBERTY      use liberty file LIBERTY"
    echo "  -t TYPE         type of circuit to produce from cxs [default=$ty]"
    echo "  -Y              skip yosys step"
    exit $1
}

POSITIONAL=()
while [[ $# -gt 0 ]]; do
    key="$1"
    case $key in
        -b)
            opt_binary=1
            shift
            ;;
        -l)
            liberty_file="$scriptdir/../$2"
            shift
            shift
            ;;
        -h)
            usage 0
            ;;
        -t)
            ty=$2
            shift
            shift
            ;;
        -Y)
            skip_yosys=1
            shift
            ;;
        *)
            POSITIONAL+=("$1")
            shift
    esac
done
set -- "${POSITIONAL[@]}"

if [[ x$1 = x ]] || ([[ x$2 = x ]] && [[ ${1##*.} != 'aig' ]]); then
    usage 1
fi

if ! [ -f cxs ]; then
    echo "[c2a] ERROR: cxs not present! maybe you should run ./build_cxs.sh" >/dev/stderr
    exit 1
fi
cxs=$(realpath cxs)

filename=$(realpath $1)
echo "filename = $filename"
if [[ ${1##*.} == 'aig' ]]; then
    file=$(basename $1)
    func=${file%.*}
else
    func=$2
fi

dir=$(pwd)
tmp=$(mktemp -d)
cd $tmp
echo "temp dir: $tmp"

cat > sawcmds.saw <<- EOM
m <- cryptol_load "$filename";
f <- cryptol_extract m "$func";
write_aig "${func}.aig" f;
EOM

if [[ "$skip_yosys" ]]; then
cat > abccmds.abc <<- EOM
read "${func}.aig"
write "${func}.bench"
EOM
else
cat > abccmds.abc <<- EOM
read "${func}.aig"
write_verilog "${func}.in.v"
EOM
fi

cat > yosys.ys <<- EOM
read_verilog "${func}.in.v"
synth -run fine
techmap; opt -fast
dfflibmap -liberty ${liberty_file}
abc -liberty ${liberty_file}
write_verilog ${func}.out.v
EOM

extension="${filename##*.}"
if [[ $extension == 'cry' ]]; then 

    sizes=($(egrep "^$func\\s*:\\s*" $filename | perl -ne \
        'if (/: \(\[(\d+)],\s*\[(\d+)\]\) ->/) { print "$1 $2"; } elsif (/: \[(\d+)\] ->/) { print "$1 0"; }' \
    ))
    inputsize=${sizes[0]}
    keysize=${sizes[1]}

    fixed_input=""
    for i in $(seq $inputsize $((inputsize + keysize - 1))); do
        fixed_input+=" $i:0"
    done

    echo "running saw..."
    saw sawcmds.saw
elif [[ $extension == 'aig' ]]; then
    cp $filename .
fi

echo "running abc..."
abc -f abccmds.abc
if [[ ! "$skip_yosys" ]]; then
    echo "running yosys..."
    yosys yosys.ys
fi

if [ "$opt_binary" ]; then
    cat $func.out.v > $dir/$func.c2v.netlist
else
    if [[ ! "$skip_yosys" ]]; then
        $scriptdir/resolve-netlist-aliases.pl $func.out.v > $func.netlist
        echo "running cxs..."
        $cxs read $func.netlist -i -o $dir/$func.c2v.$ty -k "$fixed_input"
    else
        $cxs read $func.bench -i -o $dir/$func.c2v.$ty -k "$fixed_input"
    fi
fi