GSTE through a case study [digital IC verification]

Generalized symbolic trajectory evaluation (GSTE) 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. 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.