Verification of a combinational loop based arbitration scheme in a system-on-chip integration architecture

We tackle the problem of verifying correctness properties on an HDL implementation of a system-on-chip bus-based integration architecture. The bus architecture is characterized by a 2-level arbitration scheme and the absence of a centralized controller. Checking correctness properties on an implementation can be hard because it is common for an implementation to contain constructs which are difficult to capture using a synchronous FSM model. The hard part in our case is that for performance reasons the second-level arbitration is based on a token-ring protocol implemented as a novel combinational loop. While the combinational loop is non-inverting, there is no acyclic implementation which can mimic its functionality. Our contribution has been to show how the combinational loop, and hence the arbitration scheme, can be modeled by means of mechanical transformations of the implementation model. We model check a 4-client base case implementation followed by an inductive argument for the correctness of an n-client implementation. Our approach including the combinational loop modeling and the inductive proof technique has general application to other similar protocols. Our verification methodology involved checking a Verilog implementation for desired properties using symbolic model checking in the VIS system from UC Berkeley. Checking properties on the base case required negligible amount of CPU resources. While there have been a number of formal verification case studies, we do not believe that any previous work has proposed a general purpose technique for modeling combinational loops