xMAS is a graphical specification language that allows to describe hardware components such as communication fabrics by composing microarchitectural primitives such as queues. Hardware components described using xMAS are sufficiently precise to allow formal verification, however, the explicit state space of such components suffers from the state space explosion problem. Therefore, other verification techniques have been described in the literature. In particular, sound (but not complete) approaches have been devised that translate the lack of liveness (sometimes referred to as the presence of a local deadlock) to SAT or SMT. In this talk I will discuss the main aspects of the semantics of xMAS networks, and I will discuss my understanding of some of the existing verification approaches.