The partially-ordered state spaces of symbolic trajectory evaluation (STE and GSTE) provide a built-in data abstraction mechanism that can be very effective in reducing verification complexity. The mechanism works through clever encodings of individual verification formulas, which make them easier to prove but which may also make it impossible to compose them together to derive more comprehensive properties. This talk presents a practical algorithm for transforming directly-stated formulas into this encoded form, together with a characterisation of its soundness conditions. These results allow properties to be both efficiently verified in abstracted form and still composed to derive larger properties.

The talk places this work in the context of reasoning about microarchitectural algorithms in processor designs, one of its main motivations. We are particularly interested in high-level models that express algorithms involving embedded memories, because the abstraction transformation is especially well suited to verifying operations on these.