Page MenuHomePhorge
Files F27034008

run_iscas85.sh
No OneTemporary
Actions

Authored By
Unknown
Size
6 KB
Referenced Files
None
Subscribers
None

run_iscas85.sh
View Options

#!/bin/bash
# Non-interactive ISCAS85 regression runner for the DD synthesis passes.
#
# Renders one of the yosys script templates for every ISCAS85 circuit, runs it
# with the SAT equivalence check enabled, and reports for each circuit whether
# the optimised netlist was proven equivalent to the golden one.
#
# Usage: test/run_iscas85.sh [-n MAX_INPUTS] [-t TIMEOUT] [-o OUT_DIR]
# [-s SCRIPT] [-k] [circuit ...]
#
# -n max inputs per partition block, forwarded to the converter as -n
# (0 or unset = no partitioning, i.e. the original behaviour)
# -t timeout for the converter call itself (default 2m)
# -T timeout for the whole yosys run (default 10m)
# -o output directory (default out/iscas85)
# -s yosys script template (default yosys/bbdd_synth_muxxor.ys)
# -k keep the rendered .ys and intermediate blif files
#
# With no circuit names all 11 ISCAS85 benchmarks are run.
set -u
BENCH_DIR="benchmarks/ISCAS85"
SCRIPT="yosys/bbdd_synth_muxxor.ys"
OUT_DIR="out/iscas85"
TEMP_DIR="temp"
LIBERTY_FILE="liberty/nem_thesis.lib"
TECHMAP_BBDD="yosys/techmap_bbdd.v"
TIMEOUT="2m"
YOSYS_TIMEOUT="10m"
MAX_INPUTS=0
KEEP=false
while getopts "n:t:T:o:s:k" opt; do
case "$opt" in
n) MAX_INPUTS="$OPTARG" ;;
t) TIMEOUT="$OPTARG" ;;
T) YOSYS_TIMEOUT="$OPTARG" ;;
o) OUT_DIR="$OPTARG" ;;
s) SCRIPT="$OPTARG" ;;
k) KEEP=true ;;
*) sed -n '2,20p' "$0"; exit 1 ;;
esac
done
shift $((OPTIND - 1))
if [ ! -f "$SCRIPT" ]; then
echo "[ERROR] script template not found: $SCRIPT" >&2
exit 1
fi
if [ ! -x ./build/src/convert_bbdd ]; then
echo "[ERROR] ./build/src/convert_bbdd missing - build first:" >&2
echo " mkdir -p build && cd build && cmake .. && make" >&2
exit 1
fi
# Circuits: either those named on the command line, or all of ISCAS85.
if [ $# -gt 0 ]; then
CIRCUITS=("$@")
else
CIRCUITS=()
for d in "$BENCH_DIR"/*/; do
CIRCUITS+=("$(basename "${d%/}")")
done
fi
# yosys 0.40 added `flatten -noscopeinfo`; on older yosys the flag is a hard
# error, and plain `flatten` is equivalent there because no $scopeinfo cells
# are ever produced. Detect once and patch the rendered script if needed.
STRIP_NOSCOPEINFO=false
if ! yosys -qp "help flatten" 2>/dev/null | grep -q -- "-noscopeinfo"; then
STRIP_NOSCOPEINFO=true
echo "[INFO] yosys $(yosys -V 2>/dev/null | awk '{print $2}') has no 'flatten -noscopeinfo'; stripping the flag"
fi
safe_path() { printf '%s\n' "$1" | sed 's/[&/\]/\\&/g'; }
# Converter options are injected through {{CONV_FLAGS}}. Only the bbdd template
# carries that placeholder; convert_bdd still takes no options at all, so -n
# would be dropped without a word here.
if ! grep -q "{{CONV_FLAGS}}" "$SCRIPT" && [ "$MAX_INPUTS" -gt 0 ] 2>/dev/null; then
echo "[ERROR] $SCRIPT has no {{CONV_FLAGS}} placeholder; -n cannot be forwarded" >&2
exit 1
fi
mkdir -p "$TEMP_DIR" "$OUT_DIR"
RESULTS=()
for name in "${CIRCUITS[@]}"; do
src="$BENCH_DIR/$name/$name.v"
if [ ! -f "$src" ]; then
echo "[WARN] no such benchmark: $src" >&2
continue
fi
mkdir -p "$OUT_DIR/$name"
rendered="$TEMP_DIR/${name}_synth.ys"
log="$OUT_DIR/$name/yosys.log"
conv_flags="-t 300000"
if [ "$MAX_INPUTS" -gt 0 ] 2>/dev/null; then
conv_flags="$conv_flags -n $MAX_INPUTS"
fi
sed -e "s/{{VERILOG_FILE}}/$(safe_path "$src")/g" \
-e "s/{{TEMP_DIR}}/$(safe_path "$TEMP_DIR")/g" \
-e "s/{{TOP_MODULE}}/$name/g" \
-e "s/{{BASE_NAME}}/$name/g" \
-e "s/{{TECHMAP_BBDD}}/$(safe_path "$TECHMAP_BBDD")/g" \
-e "s/{{LIBERTY_FILE}}/$(safe_path "$LIBERTY_FILE")/g" \
-e "s/{{OUT_DIR}}/$(safe_path "$OUT_DIR")/g" \
-e "s/{{TIMEOUT}}/$TIMEOUT/g" \
-e "s/{{SAT}}//g" \
-e "s/{{CONV_FLAGS}}/$(safe_path "$conv_flags")/g" \
"$SCRIPT" > "$rendered"
if $STRIP_NOSCOPEINFO; then
sed -i 's/flatten -noscopeinfo/flatten/' "$rendered"
fi
# yosys -l only captures what yosys itself prints; the converter is spawned
# through `exec` and writes to the inherited stderr, so its diagnostics
# (e.g. "Unique Table is full") only show up in the combined stdio stream.
stdio="$OUT_DIR/$name/stdio.log"
printf '%-8s ' "$name"
start=$(date +%s.%N)
timeout "$YOSYS_TIMEOUT" yosys -ql "$log" "$rendered" > "$stdio" 2>&1
rc=$?
end=$(date +%s.%N)
elapsed=$(awk -v a="$start" -v b="$end" 'BEGIN{printf "%.1f", b-a}')
# Classify. The SAT step is `sat -prove-asserts -tempinduct ... equal`.
# With -tempinduct yosys reports "Induction step proven: SUCCESS!"; without
# it, "SAT proof finished - no model found: SUCCESS!". Accept either.
if [ $rc -eq 124 ]; then
verdict="TIMEOUT(yosys)"
elif grep -qE "Induction step failed|model found: FAIL|Assert failed|induction length [0-9]+ failed" "$log" "$stdio" 2>/dev/null; then
verdict="FAIL"
elif grep -qE "Induction step proven: SUCCESS|no model found: SUCCESS" "$log" "$stdio" 2>/dev/null; then
verdict="PASS"
elif grep -q "Unique Table is full" "$log" "$stdio" 2>/dev/null; then
# the converter exhausted its hash table: a capacity problem, not a
# timeout, and it aborts within seconds rather than running long
verdict="TABLE-FULL"
elif grep -qE "Assertion .* failed|Segmentation fault" "$log" "$stdio" 2>/dev/null; then
verdict="ASSERT"
elif grep -qE "did not finish in time|Command failed: timeout|ERROR: Can't open input file" "$log" "$stdio" 2>/dev/null; then
verdict="TIMEOUT(conv)"
elif [ $rc -ne 0 ]; then
verdict="ERROR($rc)"
else
verdict="NO-PROOF"
fi
# Stats straight out of the blif the flow already writes.
blif="$TEMP_DIR/$name.blif"
pi=$(awk '/^\.inputs/{print NF-1; exit}' "$blif" 2>/dev/null)
po=$(awk '/^\.outputs/{print NF-1; exit}' "$blif" 2>/dev/null)
gold=$(python3 -c "
import json,sys
try:
d=json.load(open('$OUT_DIR/$name/${name}_golden.json'))
m=list(d['modules'].values())[0]
print(sum(m['num_cells_by_type'].values()))
except Exception: print('-')" 2>/dev/null)
opt=$(python3 -c "
import json,sys
try:
d=json.load(open('$OUT_DIR/$name/${name}_bbdd.json'))
m=list(d['modules'].values())[0]
print(sum(m['num_cells_by_type'].values()))
except Exception: print('-')" 2>/dev/null)
echo "PI=${pi:--} PO=${po:--} gates:${gold:--}->${opt:--} ${elapsed}s $verdict"
RESULTS+=("$name|${pi:--}|${po:--}|${gold:--}|${opt:--}|${elapsed}|$verdict")
if ! $KEEP; then
rm -f "$rendered" "$TEMP_DIR/${name}_bbdd.blif" "$TEMP_DIR/${name}_bdd.blif"
fi
done
n_label=$([ "$MAX_INPUTS" -gt 0 ] 2>/dev/null && echo "$MAX_INPUTS" || echo "off")
echo
echo "| Circuit | PIs | POs | n | Gates (golden) | Gates (bbdd) | Runtime | SAT equivalence |"
echo "|---|---|---|---|---|---|---|---|"
for r in "${RESULTS[@]}"; do
IFS='|' read -r c pi po g o t v <<< "$r"
echo "| $c | $pi | $po | $n_label | $g | $o | ${t}s | $v |"
done
# exit non-zero if anything actually miscompiled (timeouts are not failures here)
for r in "${RESULTS[@]}"; do
case "$r" in *"|FAIL") exit 1 ;; esac
done
exit 0

File Metadata

Mime Type
text/x-shellscript
Expires
Tue, Oct 27, 5:15 PM (15 m, 12 s)
Storage Engine
blob
Storage Format
Raw Data
Storage Handle
406011
Default Alt Text
run_iscas85.sh (6 KB)

Event Timeline