Abstract :
The formal hardware verification technique of Generalized Symbolic Trajectory Evaluation (GSTE) traditionally uses diagrams called assertion graphs to express properties. Although the graphical nature of assertion graphs can be useful for understanding simple properties, it places limitations on formal reasoning. Clean reasoning is important for high-level verification steps, such as property decomposition. In GSTE, formal reasoning is also required to justify abstraction refinement steps, which are achieved via property transformation. This paper proposes a linear temporal logic, generalized trajectory logic, to provide a basis for reasoning about GSTE properties. The logic is textual and algebraic in nature, so it induces clean reasoning rules. We describe model checking for the logic, and look at rules for semantic equality, property decomposition and abstraction refinement.
