GSTE: an Illustrative and comparative introduction

GSTE (Generalized Symbolic Trajectory Evaluation) is an industrially proven high capacity model checking technology for hardware verification. It combines the efficiency and flexibility of the original STE with the expressiveness of classical model checking. This paper explains the three key aspects of GSTE through a simple example and show how they work together to make GSTE more powerful than the classical approach based on language containment. Real life verification results are provided to demonstrate the strength of GSTE.