Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics

Abstract microarchitectural models of communication fabrics present a challenge for verification. Due to the presence of deep pipelining, a large number of queues and distributed control, the state space of such models is usually too large for enumeration by protocol verification tools such as Murphi. On the other hand, we find that state-of-the-art rtl model checkers such as abc have poor performance on these models since there is very little opportunity for localization and most of the recent capacity advances in rtl model checking have come from better ways of discarding the irrelevant parts of the model. In this work we explore a new approach for verifying these models where we capture a model at a high level of abstraction by requiring that it be described using a small set of well-defined microarchitectural primitives. We exploit the high level structure present in this description, to automatically strengthen some classes of properties, in order to make them 1-step inductive, and then use an rtl model checker to prove them. In some cases, even if we cannot make the property inductive, we can dramatically reduce the number and complexity of lemmas that are needed to make the property inductive.

1. Our queues are always fifo i.e. first-in-first-out.

2. Henceforth we only mention the value parameters of a component and leave the type parameters implicit.

3. When o.irdy is false, o.data is a don’t care. But for brevity in the equations, we always assign to o.data rather than only when o.irdy is asserted.

4. By “v↦(v=0)” we mean the function that is 1 iff the input is equal to 0, i.e. the function λv.(v=0) using λ notation.

5. Even with general joins there is an easy case. If p is a property such that p′=p∘h depends on only one variable, then it suffices to propagate p′ along the corresponding input.

6. Assuming that the (local) assertions G(num ≤ k) for each queue have already been added.

7. A typical example of such a system would be when separate virtual channels are used for req and rsp in Fig. 3 to avoid deadlock.

8. To check for adequate buffering to avoid deadlocks.

Authors and Affiliations

1. Two Sigma Investments LLC, New York, NY, 10012, USA

   Satrajit Chatterjee

2. Intel Corporation, Hillsboro, OR, 97124, USA

   Michael Kishinevsky

Corresponding author

Correspondence to Satrajit Chatterjee.

Reprints and permissions