test: add non-interactive ISCAS85 regression runner
synth.sh cannot drive a regression sweep: it prompts via read -e -p, and
its directory mode globs "$file_path"*.v, which misses the nested
benchmarks/ISCAS85/<name>/<name>.v layout.
test/run_iscas85.sh renders a yosys template with the same substitutions
synth.sh uses, runs it with the SAT equivalence check enabled, classifies
the outcome (PASS/FAIL/TIMEOUT/ERROR) and prints a markdown table.
Two environment details it has to handle:
- yosys 0.33 predates flatten -noscopeinfo (added in 0.40), so the flag is detected and stripped from the rendered script when unsupported. Plain flatten is equivalent there since no $scopeinfo cells are produced.
- with -tempinduct the SAT pass reports "Induction step proven: SUCCESS!" rather than "no model found: SUCCESS!"; both are accepted.
PARTITIONING.md is the living design/progress document for the upcoming
support-bounded partitioning work. It lives at the repo root because docs/
is the Doxygen output directory and is gitignored.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012nXGcHc3GSLAqg1AL53LKM