GSTE through a case study
Jin Seok Yang, Amit Kumar Goel · Digest of technical papers/Digest of technical papers - IEEE/ACM International Conference on Computer-Aided Design · 2002
Generalized Symbolic Trajectory Evaluation (GSTE) [17, 18, 19] is a very significant extension of STE that has the power to verify all ω-regular properties but at the same time preserves the benefits of the original STE [16]. It also extends the symbolic quaternary model used by STE to support seamless model refinement for efficiency and accuracy trade-off in GSTE model checking. In this paper, we present a case study on FIFO verification to illustrate the strength of GSTE and demonstrate its methodology in specifying and verifying large scale designs.