Scalable Model Checking Beyond Safety - A Communication Fabric Perspective

Sayak Ray

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2013-181
November 4, 2013

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2013/EECS-2013-181.pdf

In this research, we have developed symbolic algorithms and their open-source implementations 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 important liveness property) of on-chip communication fabrics.

Advisor: Robert K. Brayton


BibTeX citation:

@phdthesis{Ray:EECS-2013-181,
    Author = {Ray, Sayak},
    Title = {Scalable Model Checking Beyond Safety - A Communication Fabric Perspective},
    School = {EECS Department, University of California, Berkeley},
    Year = {2013},
    Month = {Nov},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2013/EECS-2013-181.html},
    Number = {UCB/EECS-2013-181},
    Abstract = {In this research, we have developed symbolic algorithms and their open-source implementations 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 important liveness property) of on-chip communication fabrics.}
}

EndNote citation:

%0 Thesis
%A Ray, Sayak
%T Scalable Model Checking Beyond Safety - A Communication Fabric Perspective
%I EECS Department, University of California, Berkeley
%D 2013
%8 November 4
%@ UCB/EECS-2013-181
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2013/EECS-2013-181.html
%F Ray:EECS-2013-181