Scalable Model Checking Beyond Safety - A Communication Fabric Perspective

In this research, we have developed symbolic algorithms and their open-source implemen-tations that effectively solve liveness verification problem for industrially relevant hardwaresystems. In principle, our tool-suite works on any sequential hardware circuit and for thewhole family of ω-regular properties. Practicality and effectiveness of our tool-suite havebeen demonstrated in the context of proving response properties (a very common and impor-tant liveness property) of on-chip communication fabrics