# SBY: liveness check (deadlock / livelock)
**URL:** https://yosyshq.discourse.group/t/sby-liveness-check-deadlock-livelock/110
**Category:** Users
**Created:** [December 16, 2025, 11:06am UTC](https://yosyshq.discourse.group/t/sby-liveness-check-deadlock-livelock/110 "2025-12-16T11:06:02Z")
**Posts on this page:** 3
**Page:** 1
### Author:  [@MysticExplorer](https://yosyshq.discourse.group/u/MysticExplorer)
#### Post date: [December 16, 2025, 11:06am UTC](https://yosyshq.discourse.group/t/sby-liveness-check-deadlock-livelock/110/1 "2025-12-16T11:06:02Z")
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?)
---
### Author:  [@KrystalDelusion](https://yosyshq.discourse.group/u/KrystalDelusion)
#### Post date: [December 16, 2025, 9:17pm UTC](https://yosyshq.discourse.group/t/sby-liveness-check-deadlock-livelock/110/2 "2025-12-16T21:17:22Z")
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](https://github.com/YosysHQ/sby/issues/new) with a minimized reproducer for this?
---
### Author:  [@MysticExplorer](https://yosyshq.discourse.group/u/MysticExplorer)
#### Post date: [December 17, 2025, 9:30am UTC](https://yosyshq.discourse.group/t/sby-liveness-check-deadlock-livelock/110/3 "2025-12-17T09:30:18Z")
Issue raised, thanks!