Suprove求解器崩溃求助：SymbiYosys形式化验证故障排查

Let's start with the most obvious clue from your logs: the suprove process exited with return code 127. In Unix-like systems, this exit code almost always means the shell couldn't locate the executable you're trying to run. Here's a step-by-step breakdown of how to diagnose and fix this:

1. Verify Suprove is Installed and in Your PATH #

First, check if suprove is actually present on your system and accessible from your shell:

which suprove

If this command returns nothing, that's your core problem—Suprove isn't installed, or it's not in your PATH:

• If it's missing, install Suprove (it's typically distributed as part of the AIGER tool collection; you can build it from source or check your package manager for pre-built binaries).
• If it exists but which doesn't find it, add its installation directory to your PATH (e.g., export PATH="/path/to/suprove/dir:$PATH"), then re-run your SBY script.

2. Manually Run the Suprove Command to Get Detailed Errors #

SBY's logs don't show full error output from suprove when it crashes. Try running the exact command SBY uses directly in your terminal to see explicit issues:

cd assert_seq_proof
suprove model/design_aiger.aig

This will print any missing dependency errors, invalid AIG format warnings, or other crash details that SBY swallows.

3. Validate the AIG File for Suprove Compatibility #

Even though the AIG file works with ABC, Suprove might have stricter format requirements. Use the AIGER validation tool to check for issues:

aigcheck model/design_aiger.aig

If aigcheck reports problems, adjust your Yosys synthesis script in the SBY file to produce a standard AIG. For example, ensure you're using write_aiger -ascii instead of non-standard variants that might break Suprove's parsing.

4. Check Version Compatibility Between SymbiYosys and Suprove #

Mismatched versions of tools often cause compatibility bugs. Verify your tool versions:

sby --version
suprove --version

If you're running an older SymbiYosys release, upgrade to the latest version. Similarly, ensure your Suprove build is up-to-date—newer releases often fix edge-case crashes with AIG files.

5. Explicitly Specify Suprove Path in Your SBY Script #

If suprove is installed in a non-standard location, bypass PATH issues by hardcoding its path in your SBY file's engine section:

[engines]
aiger suprove -cmd /full/path/to/suprove

This ensures SBY uses the exact executable you intend.

6. Rule Out Resource or Environment Issues #

In rare cases, resource limits (like insufficient memory) or misconfigured environment variables can cause suprove to crash:

• Try running the command with elevated resources (if your system allows it) to rule out memory constraints.
• Check if LD_LIBRARY_PATH is missing dependencies required by suprove (e.g., shared libraries it needs to run).

内容的提问来源于stack exchange，提问作者turbo_fingers