Alexander Fedotov: Fixing block and idle equations for FSMs in MaDL (work in progress)

Event Details

The xMAS language introduced a convenient way of high-level modeling and verification of communication fabrics. For micro-architectural models expressed in xMAS, it was shown that the problem of proving liveness could be transformed into a SAT-problem, which is advantageous in terms of scalability. Later on, Verbeek et al. proposed an approach to combine basic xMAS primitives with Finite State Machines. The idea itself resulted in a more expressive, yet scalable technique for modeling and verification of microarchitectures. However, we found a mistake in it. In the current work, we show that the technique introduced by Verbeek et al. is not sound, i.e., it fails to prove deadlock freedom. We propose a new method which addresses  the problems of the previous approach.