Skip to main content
eScholarship
Open Access Publications from the University of California

UC Berkeley

UC Berkeley Electronic Theses and Dissertations bannerUC Berkeley

Scalable Model Checking Beyond Safety - A Communication Fabric Perspective

Abstract

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.

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View