Lifting Hardware Models from Implementations for Verification

Jonathan Shi

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2022-149
May 19, 2022

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2022/EECS-2022-149.pdf

We introduce rtl2model, a compositional Python framework for modeling hardware designs. rtl2model models can be generated from RTL with various degrees of micro-architectural granularity, and can be composed with other models that are either manually constructed or algorithmically produced. We combine cone-of-influence algorithms with syntax-guided synthesis techniques to produce simpler models than those that are translated directly from RTL, thus reducing the model-to-implementation gap and facilitating more efficient verification.

Advisor: Sanjit A. Seshia


BibTeX citation:

@mastersthesis{Shi:EECS-2022-149,
    Author = {Shi, Jonathan},
    Title = {Lifting Hardware Models from Implementations for Verification},
    School = {EECS Department, University of California, Berkeley},
    Year = {2022},
    Month = {May},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2022/EECS-2022-149.html},
    Number = {UCB/EECS-2022-149},
    Abstract = {We introduce rtl2model, a compositional Python framework for modeling hardware designs. rtl2model models can be generated from RTL with various degrees of micro-architectural granularity, and can be composed with other models that are either manually constructed or algorithmically produced. We combine cone-of-influence algorithms with syntax-guided synthesis techniques to produce simpler models than those that are translated directly from RTL, thus reducing the model-to-implementation gap and facilitating more efficient verification.}
}

EndNote citation:

%0 Thesis
%A Shi, Jonathan
%T Lifting Hardware Models from Implementations for Verification
%I EECS Department, University of California, Berkeley
%D 2022
%8 May 19
%@ UCB/EECS-2022-149
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2022/EECS-2022-149.html
%F Shi:EECS-2022-149