Ranking structure in communication fabrics
Sayak Ray, Robert K. Brayton · Formal Methods · 2013
We present our experience and case studies for proving liveness of communication fabrics. A methodology is developed that reveals ranking structure underlying the state spaces of such fabrics. This enables an efficient proof of liveness using the k-LIVENESS algorithm leveraging this ranking structure. An open-source infrastructure for the k-LIVENESS algorithm has been implemented that has a provision for specifying and leveraging ranking structures in the form of stabilizing constraints. A significant speed-up was achieved with this modified k-LIVENESS framework when proving response property of communication fabrics.