A method for generation of GSTE assertion graphs

Generalized symbolic trajectory evaluation (GSTE) is a formal verification technique developed by Intel and used on next-generation microprocessor designs. One of its current drawbacks is that each property must be supplied in the form of a state-transition diagram known as an assertion graph. Assertion graphs are difficult to construct, to read and to reason about because they describe properties at a low level. In this paper, we propose a higher-level property language for GSTE in which we can specify properties as what we call assertion programs. We describe a way of applying weakest precondition calculations to these programs to generate assertion graphs. These can then be supplied to existing GSTE tools for verification.