Sound idle and block equations for finite state machines in xMAS
Alexander Fedotov, Jeroen J. A. Keiren, Julien Schmaltz · TU/e Research Portal · 2019
The xMAS language allows the high-level modeling of communication fabrics.For microarchitectural models expressed in xMAS, it was shown that liveness can be proven effectively using a reduction to SAT.Verbeek et al. extended xMAS with finite state machines (FSMs) to model and verify liveness of the combination of cache coherence protocols and interconnects.To support state machines, they extended the existing reductions to SAT to incorporate FSMs.We present counterexamples showing that this technique is unsound and fails to detect certain deadlocks.We propose an alternative reduction of liveness for xMAS networks with FSMs to SAT.We prove the correctness of our approach and evaluate its performance.