diff --git a/synth.sh b/synth.sh index a093203..05e20c0 100755 --- a/synth.sh +++ b/synth.sh @@ -1,162 +1,177 @@ #!/bin/bash BBDD_SCRIPT="yosys/bbdd_synth_muxxor.ys" BDD_SCRIPT="yosys/bdd_synth.ys" MUXIG_SCRIPT="yosys/muxig_synth.ys" TEMP_DIR="temp" LIBERTY_FILE="liberty/nem_thesis.lib" TIMEOUT="2m" #1 minute timeout for now TECHMAP_BBDD="yosys/techmap_bbdd.v" +TABLE_SIZE="300000" +MAX_INPUTS=0 # 0 disables partitioning, i.e. one diagram over all inputs print_options(){ echo "(1) Synthesis Verilog file with bbdd optimization" echo "(2) Synthesis Verilog file with bdd optimization" echo "(3) Synthesis Verilog file with muxig optimization" echo "(e) Exit" } safe_path() { local unsafe_path="$1" echo "$(printf '%s\n' "$unsafe_path" | sed 's/[&/\]/\\&/g')" } process_input() { file_name=$(basename "$file_path") # with extension file_base="${file_name%.*}" # without # get top module name read -p "top module [default=${file_base}] " top_module top_module=${top_module:-${file_base}} #safe_file_path=$(printf '%s\n' "$file_path" | sed 's/[&/\]/\\&/g') safe_file_path=$(safe_path "$file_path") #safe_techmap_path=$(printf '%s\n' "$TECHMAP_BBDD" | sed 's/[&/\]/\\&/g') } run_yosys() { # Run yosys if $nosat; then sat_replacement="#" # comment out {{SAT}} else sat_replacement="" # replace {{SAT}} with nothing fi + # options handed to the converter; the bbdd template picks them up through + # {{CONV_FLAGS}}. convert_bdd takes no options, and its template has no + # placeholder, so the substitution is a no-op there. + conv_flags="-t $TABLE_SIZE" + if [ "$MAX_INPUTS" -gt 0 ] 2>/dev/null; then + conv_flags="$conv_flags -n $MAX_INPUTS" + fi echo "Synthesising $file_base" sed -e "s/{{VERILOG_FILE}}/$safe_file_path/g" \ -e "s/{{TEMP_DIR}}/$TEMP_DIR/g" \ -e "s/{{TOP_MODULE}}/$top_module/g" \ -e "s/{{BASE_NAME}}/$file_base/g" \ -e "s/{{TECHMAP_BBDD}}/$safe_techmap_path/g" \ -e "s/{{LIBERTY_FILE}}/$safe_liberty_path/g" \ -e "s/{{OUT_DIR}}/$safe_out_path/g" \ -e "s/{{TIMEOUT}}/$TIMEOUT/g" \ -e "s/{{SAT}}/$sat_replacement/g" \ + -e "s/{{CONV_FLAGS}}/$(safe_path "$conv_flags")/g" \ "$yosys_script" > "$TEMP_DIR/${file_base}_synth.ys" mkdir -p ${out_dir}/${file_base}/ /usr/bin/time -f "Time: %E\nCPU: %P\nMemory: %M KB" -o ${out_dir}/${file_base}/yosys_${opt_name}_time.txt yosys${yosys_flags} ${TEMP_DIR}/${file_base}_synth.ys if [ -e ${out_dir}/${file_base} ]; then python ./yosys/print_summary.py ${out_dir}/${file_base} else echo "${file_base} did not finish in time" fi } synth_verilog() { local yosys_script="$1" local opt_name="$2" if ! $verbose; then yosys_flags=" -q" # is quite mode else yosys_flags="" fi safe_techmap_path=$(safe_path "$TECHMAP_BBDD") safe_liberty_path=$(safe_path "$LIBERTY_FILE") echo "Using script: $yosys_script" read -e -p 'Input file path: ' file_path # Get Output Dir read -e -p 'Output directory: ' out_dir safe_out_path=$(safe_path "$out_dir") out_dir="${out_dir%/}/" if [ -f "$file_path" ]; then process_input run_yosys if ! $nocleanup; then rm ${TEMP_DIR}/${file_base}_synth.ys rm ${TEMP_DIR}/${file_base}.blif rm -f ${TEMP_DIR}/${file_base}_bbdd.blif rm -f ${TEMP_DIR}/${file_base}_bdd.blif fi exit elif [ -d "$file_path" ]; then # extend / if not present file_path="${file_path%/}/" for file in "$file_path"*.v; do if [ -e "$file" ]; then safe_file_path=$(safe_path "$file") file_name=$(basename "$file") # with extension file_base="${file_name%.*}" # without top_module="$file_base" yosys_flags=" -q" run_yosys if ! $nocleanup; then rm ${TEMP_DIR}/${file_base}_synth.ys rm ${TEMP_DIR}/${file_base}.blif rm -f ${TEMP_DIR}/${file_base}_bbdd.blif rm -f ${TEMP_DIR}/${file_base}_bdd.blif fi fi done exit else echo "[ERROR] File ${file_path} does not exist" fi } handle_selection() { case "$1" in 1) synth_verilog $BBDD_SCRIPT "bbdd";; 2) synth_verilog $BDD_SCRIPT "bdd";; 3) synth_verilog $MUXIG_SCRIPT "muxig";; e) echo "Exiting..."; exit 0 ;; *) echo "Invalid option. Please try again." ;; esac } # Initialize booleans as false nocleanup=false nosat=false verbose=false # Parse flags while [[ $# -gt 0 ]]; do case "$1" in -nocleanup) nocleanup=true shift ;; -nosat) nosat=true shift ;; -v) verbose=true shift ;; + -n) + MAX_INPUTS="$2" + shift 2 + ;; *) echo "Unknown option: $1" + echo "Usage: $0 [-nocleanup] [-nosat] [-v] [-n MAX_INPUTS]" exit 1 ;; esac done # get input file mkdir -p $TEMP_DIR while true; do if [ "$nosat" = false ]; then echo "Satisfiability check is enabled" fi print_options read -p "Enter your choice [1-3]: " choice handle_selection "$choice" echo "" done diff --git a/test/run_iscas85.sh b/test/run_iscas85.sh index 0ebf0a2..3c7e0f7 100755 --- a/test/run_iscas85.sh +++ b/test/run_iscas85.sh @@ -1,191 +1,198 @@ #!/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" - # forward -n to the converter invocation inside the rendered script - sed -i "s#\(convert_bbdd\|convert_bdd\) -t 300000#\1 $conv_flags#" "$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 diff --git a/yosys/bbdd_synth_muxxor.ys b/yosys/bbdd_synth_muxxor.ys index b52f11f..ef5cbf0 100644 --- a/yosys/bbdd_synth_muxxor.ys +++ b/yosys/bbdd_synth_muxxor.ys @@ -1,71 +1,71 @@ ######################### preprocessing ########################################################################### read_verilog {{VERILOG_FILE}} hierarchy -top {{TOP_MODULE}} proc;; opt;;; flatten -noscopeinfo;; opt;;; techmap;; opt;;; splitnets -ports;; opt;;; ########################## write design to a blif file and delete empty line because mockturtle cannot handle that # write_blif {{TEMP_DIR}}/{{BASE_NAME}}.blif rename {{TOP_MODULE}} {{TOP_MODULE}}_golden exec -- sed -i '/^$/d' {{TEMP_DIR}}/{{BASE_NAME}}.blif ########################## execute bbdd pass map the result back to yosys names and rename the module ############# -exec -- timeout {{TIMEOUT}} time -f "\nTime: %E\nCPU: %P\nMemory: %M KB" -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd_time.txt ./build/src/convert_bbdd -t 300000 {{TEMP_DIR}}/{{BASE_NAME}}.blif +exec -- timeout {{TIMEOUT}} time -f "\nTime: %E\nCPU: %P\nMemory: %M KB" -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd_time.txt ./build/src/convert_bbdd {{CONV_FLAGS}} {{TEMP_DIR}}/{{BASE_NAME}}.blif read_blif {{TEMP_DIR}}/{{BASE_NAME}}_bbdd.blif rename {{TOP_MODULE}} {{TOP_MODULE}}_bbdd stat {{TOP_MODULE}}_bbdd techmap -map {{TECHMAP_BBDD}} copy {{TOP_MODULE}}_bbdd {{TOP_MODULE}}_sat techmap -map yosys/muxxor_inv_map.v {{TOP_MODULE}}_bbdd techmap -map yosys/muxxor_inv_sat.v {{TOP_MODULE}}_sat opt -full {{TOP_MODULE}}_bbdd opt -full {{TOP_MODULE}}_golden ########################### check equality of the optimization ###################################################### {{SAT}}miter -equiv -make_assert {{TOP_MODULE}}_golden {{TOP_MODULE}}_sat equal {{SAT}}flatten equal {{SAT}}clean equal {{SAT}}opt -full equal;; {{SAT}}techmap equal {{SAT}}sat -prove-asserts -set-init-zero -tempinduct -verify -show-regs -show-inputs -show-outputs -dump_vcd trace.vcd equal ########################### write data without abc pass ############################################################# tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd.json stat -json {{TOP_MODULE}}_bbdd tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden.json stat -json {{TOP_MODULE}}_golden tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd_ltp.txt ltp {{TOP_MODULE}}_sat tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_ltp.txt ltp {{TOP_MODULE}}_golden ########################### abc pass for the golden solution ######################################################## copy {{TOP_MODULE}}_golden {{TOP_MODULE}}_golden_abc abc -liberty {{LIBERTY_FILE}} {{TOP_MODULE}}_golden_abc ########################### abc pass for the optimization solution ################################################# copy {{TOP_MODULE}}_bbdd {{TOP_MODULE}}_bbdd_abc abc -D 100 -liberty {{LIBERTY_FILE}} {{TOP_MODULE}}_bbdd_abc #print stats to file tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd.json stat -json {{TOP_MODULE}}_bbdd tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd_abc.json stat -json {{TOP_MODULE}}_bbdd_abc tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden.json stat -json {{TOP_MODULE}}_golden tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_abc.json stat -json {{TOP_MODULE}}_golden_abc ########################### write abc blif and verilog ############################################################# write_blif -top {{TOP_MODULE}}_bbdd_abc {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd_abc.blif write_blif -top {{TOP_MODULE}}_bbdd {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd.blif write_blif -top {{TOP_MODULE}}_golden_abc {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_abc.blif write_blif -top {{TOP_MODULE}}_golden {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden.blif select {{TOP_MODULE}}_bbdd_abc write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd_abc.v select {{TOP_MODULE}}_bbdd write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd.v select {{TOP_MODULE}}_golden_abc write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_abc.v select {{TOP_MODULE}}_golden write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden.v