Scalable Liveness Verification for Communication Fabrics

by S.J.C. Joosten and J. Schmaltz

Abstract

In the realm of multi-core processors and systems-on-chip, communication fabrics constitute a key element. A large number of queues and distributed control are two important aspects of this class of designs. These aspects make decomposition and abstraction techniques difficult to apply. For this class of designs, the application of formal methods is a real challenge. In particular, the verification of liveness properties is often intractable. Communication fabrics can be seen as a set of queues and flops interconnected by combinatorial logic. Based on this simple but powerful observation, we propose a novel method for liveness verification. Our method directly applies to Register Transfer Level designs. The essential aspects of our approach are (1) to abstract away from the details of queue implementations and (2) an efficient encoding of liveness properties in an SMT instance. Experimental results are promising. Designs with hundreds of queues can be analysed for liveness within minutes.

Files

All software is licensed under the Apache 2.0 license.

To get our implementation of the method described in our paper, we recommend installing the Haskell platform. You should be able to compile from the command line by typing: ghc --make eMOD. To run it, pipe an .emod file to the eMOD executable. We have used Haskell version 7.6.3, anything newer should be good. In addition, you will need the source files:

For the designs in the paper, you may download the following zip files: