[dv/formal]: With Yosys and rIC3 fails for python conductor.py prove.

[Eulerianial]

Observed Behavior

I tried to re-run the dv/formal flow using the Opensource tools using the following instructions:
Build instructions:

• nix develop .#oss-dev
• make build/aig-manip builds the Rust aig-manip tool used by conductor.py
• make build/all.aig builds the core Aiger file
• python3 conductor.py prove

but the run crashed with Error code 127. I attached the log file also for the crash.

Expected Behavior

In the link here https://semiiphub.com/industryexpertblogs/open-source-correctness-proof-for-ibex it was mentioned that dv/formal is part of the latest CI. Thus I was hoping it must pass.

Steps to reproduce the issue

Commands I ran:

• git clone https://github.com/lowRISC/ibex.git
• cd dv/formal
• nix develop .#oss-dev
• make build/aig-manip builds the Rust aig-manip tool used by conductor.py
• make build/all.aig builds the core Aiger file
• python3 conductor.py

At pyhon3 conductor.py prove got lot of errors with Error code 127,

My Environment

log_file.txt

Operating system:
Distributor ID: Ubuntu
Description: Ubuntu 24.04.4 LTS
Release: 24.04

Version of the Ibex source code:
branch: master

[hcallahan-lowrisc]

Hello, thanks for checking out the OSS formal flow!

You can see an example of the flow running on a recent CI job here : https://github.com/lowRISC/ibex/actions/runs/22105317587/job/63886235294. The "Run OSS Env" step is the most relevant one, coming from the definition here :

ibex/.github/workflows/ci-formal.yml

Lines 40 to 47 in 8d171a1

	- name: Run OSS Env
	run: |
	source <(nix print-dev-env .#oss-dev)
	cd dv/formal
	make build/aig-manip
	make build/all.aig SHELL=bash
	python3 conductor.py prove --check-complete --max-mem $MAX_MEM_GB

This would seem to match the commands you have given in the issue description.

Can you look at your logfiles and compare them against the CI job? From the extract provided, I cannot see any particular error. However, the line Unknown Exit Code 127: Failed to prove 2 properties in step 15 (0.002s with 0.000GB) (and others similar) would suggest that something is wrong with your environment and the tool has exited immediately / failed to run at all.

[Eulerianial]

Thank you for the tips and references above.
Using the same, I could find the root cause of the crash at my side.
Indeed the problem was in my environment.

ROOT-CAUSE:
I was in the base anaconda environment and on top of that installed Nix.
Due to which the rIC3 binary path was not accessible via the conductor.py

I resolved it by making the following edits in the conductor.py:

`import shutil
async def prove(engine_config: str, step: int, props: list[str], timeout=None, expected_memory=10.0) -> ProcessResult:
specialised = await prepare_aiger(step, props)

# --- ADD THIS LOGIC TO FIX CODE 127 ---
parts = engine_config.split()
abs_binary = shutil.which(parts[0])
if abs_binary:
    parts[0] = abs_binary
    full_cmd = " ".join(parts)
else:
    full_cmd = engine_config
# --------------------------------------

res = await shell(f"{engine_config} {specialised}", timeout=timeout, expected_memory=expected_memory)
proof_done(engine_config, specialised, step, props, res)
return res

[hcallahan-lowrisc]

Thanks for following up, and I'm glad to hear you have got the flow to run.

I'm not an anaconda user, but it sounds like something about the anaconda environment was preventing the rIC3 binary from being located on you path? Would you mind briefly explaining why that was, and I might be able to add a mitigation to the build scripts.

In general, Nix brings all the dependencies you need, so in general it's not recommended to run nix develop inside any other environment. But running it after already entering an anaconda environment should be fine in-theory as the nix programs should all be located at the head of your PATH. I guess there could be problems depending on what shell hooks are executed by your .rc file upon entering the nix shell.