SBY: liveness check (deadlock / livelock)

Users
1

I’m evaluating SBY’s liveness checking. I created a simple FSM (module deadlock_test) with an intentional deadlock: the ‘locked’ state should violate a deadlock check, and (at least) the initial idle state should violate a livelock check. My .sby file includes a task prove_deadlock with mode live and engine aiger suprove.

When I run this, I get:

SBY ... [deadlock_test_prove_deadlock] engine_0: Error: engine_0/trace.aiw: unexpected data in AIGER witness file

Is my setup correct for checking deadlock/livelock? What does this error mean, and how should I interpret it? (Since this file is generated by the tool, I suppose the user is not supposed to see such a message?)

2

That suggests there is a problem in SBY with reading the output of suprove for liveness counter examples. Could you raise an issue on the SBY repository with a minimized reproducer for this?

3

Issue raised, thanks!