Description
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.