  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 $\mu$spec axiomatic
modelling framework cannot be translated to equivalent finite-state operational
models. We also derive restrictions on the space of $\mu$spec 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 $\mu$spec axioms to equivalent finite-state automata-based
operational models. We demonstrate the efficacy of our method by using the
models generated by our procedure to prove the correctness of ordering
properties on three RTL designs.
