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

This publication is archived. It is kept only for reference purposes, so it is no longer being updated and may not meet accessibility standards. If you need this content in a different format, please email webteam@eecs.berkeley.edu.

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2013/Archive/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.

Advisors: 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