Verification Techniques for xMAS

Computers and related hardware are essential in the modern world. It is crucial that new hardware functions correctly. Conventionally, validation of new hardware designs is done using simulation and testing. The latter has a drawback as full coverage of all possible behaviors is impossible for complex hardware designs. On the other hand, Formal Verification covers all possible behaviors as it proves the correctness of new hardware designs using the formal methods of mathematics. However, Formal Verification is not a panacea as it is a challenge to scale it to the system level. In this thesis, among other things, we scaled Formal Verification to the system level.

xMAS is a language designed for convenient modeling and scalable formal verification of hardware. This thesis contains work on formal verification techniques in xMAS and related topics.

Although there exist xMAS verification techniques that rely on a state-based representation of xMAS, a state-based semantics is not described in the literature. In Chapter 2, we formulated the semantics of the xMAS language in terms of Kripke Structures and proved its correctness. It serves as a theoretical basis for the subsequent work and fills the gap in the existing literature.

In Chapter 3, we demonstrated that the liveness verification technique for the xMAS Finite State Machine extension introduced by Verbeek et al. is unsound by providing a counter-example. In the same chapter, we provided our own liveness verification approach for xMAS with FSMs and proved that it is sound. In addition, we showed that using xMAS with FSMs in combination with our verification technique can allow liveness verification at the system level.

The state-of-the-art liveness verification technique for xMAS is prone to reporting spurious deadlocks. In Chapter 4, we introduced two approaches to solve the spurious deadlock issue. One approach is based on an SMT-encoding of $k$-step backward reachability of an initial state from the deadlock state. Another approach uses interpolation to tackle the reachability problem mentioned above. In the same chapter, we prove the correctness of both approaches and evaluate their performance.

Hardware is implemented based on high-level designs. An important question is whether the implementation conforms to the high-level design, which is usually called the specification.
In Chapter 5, we introduced a novel method that, given an abstract xMAS specification, automatically checks the correctness of RTL implementations made according to the xMAS specification. The method takes an xMAS specification and the respective RTL implementation as input. It then turns the specification into an RTL Finite State Machine and checks that all the traces produced by the implementation are included in the traces of the specification.