Generation of inductive invariants from register transfer level designs of communication fabrics

Communication fabrics constitute a key component of multicore processors and systems-on-chip. To ensure correctness of communication fabrics, formal methods such as model checking are essential. Due to the large number of buffers and the distributed character of control, applying these methods is challenging. Recent advancements in the verification of communication fabrics have demonstrated that the use of inductive invariants provides promising results towards scalable verification of Register Transfer Level (RTL) designs. In particular, these invariants are key in the verification of progress properties. Such invariants are difficult to infer. So far, they were either manually or automatically derived from a high-level description of the design. Important limitations of these approaches are the need for the high-level model and the necessary match between the model and the RTL design. We propose an algorithm to automatically derive these invariants directly from the RTL design. We consider communication fabrics to be a set of message storing elements (e.g, buffers) and some routing logic in-between. The only input required by our method is a definition of when messages enter or leave a buffer. We then exploit this well-defined buffer interface to automatically derive invariants about the number of packets stored in buffers. For several previously published examples, we automatically generate the exact same invariants that were either manually or automatically derived from a high-level model. Experimental results show that the time needed to generate invariants is a few seconds even for large examples.