UC Berkeley

In this research, we have developed symbolic algorithms and their open-source implemen-

tations that effectively solve liveness verification problem for industrially relevant hardware

systems. In principle, our tool-suite works on any sequential hardware circuit and for the

whole family of ω-regular properties. Practicality and effectiveness of our tool-suite have

been demonstrated in the context of proving response properties (a very common and impor-

tant liveness property) of on-chip communication fabrics.