Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results

Adwait Godbole, Yatin Manerkar, and Sanjit A. Seshia. Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2022.

Download

[pdf] 

Abstract

A system may be modelled as an operational model (which has explicit notions of state and transitions between states) or an axiomatic model (which is specified entirely as a set of invariants). Most formal methods techniques (e.g., IC3, invariant synthesis, etc) are designed for operational models and are largely inaccessible to axiomatic models. Furthermore, no prior method exists to automatically convert axiomatic models to operational ones, so operational equivalents to axiomatic models had to be manually created and proven equivalent.In this paper, we advance the state-of-the-art in axiomatic to operational model conversion. We show that general axioms in the muspec axiomatic modelling framework cannot be translated to equivalent finite-state operational models. We also derive restrictions on the space of muspec axioms that enable the feasible generation of equivalent finite-state operational models for them. As for practical results, we develop a methodology for automatically translating muspec axioms to finite-state automata-based operational models. We demonstrate the efficacy of our method by using operational models generated by our procedure to prove the correctness of properties on three RTL designs.

BibTeX

@InProceedings{adwait-fmcad22,
  Author = {Adwait Godbole and Yatin Manerkar and Sanjit A. Seshia},
  Title = {Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results},
  booktitle = {Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD)},
  month = "October",
  year = {2022},
  abstract = {A system may be modelled as an operational model (which has explicit notions of state and transitions between states) or an axiomatic model (which is specified entirely as a set of invariants). Most formal methods techniques (e.g., IC3, invariant synthesis, etc) are designed for operational models and are largely inaccessible to axiomatic models. Furthermore, no prior method exists to automatically convert axiomatic models to operational ones, so operational equivalents to axiomatic models had to be manually created and proven equivalent.
In this paper, we advance the state-of-the-art in axiomatic to operational model conversion. We show that general axioms in the muspec axiomatic modelling framework cannot be translated to equivalent finite-state operational models. We also derive restrictions on the space of muspec axioms that enable the feasible generation of equivalent finite-state operational models for them. As for practical results, we develop a methodology for automatically translating muspec axioms to finite-state automata-based operational models. We demonstrate the efficacy of our method by using operational models generated by our procedure to prove the correctness of properties on three RTL designs.},
}