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.

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