Title :
GSTE through a case study [digital IC verification]
Author :
Yang, Jin ; Goel, Amit
Abstract :
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.
Keywords :
circuit CAD; circuit simulation; formal verification; integrated circuit design; integrated circuit modelling; logic CAD; logic simulation; FIFO verification; GSTE model checking efficiency/accuracy refinement; STE extensions; STE symbolic quaternary models; assertion graphs; digital IC verification; generalized symbolic trajectory evaluation; quaternary symbolic simulation; Circuit simulation; Computer aided software engineering; Decoding; Design automation; Flexible printed circuits; Floating-point arithmetic; Hardware; Large-scale systems; Latches; Mathematical model;
Conference_Titel :
Computer Aided Design, 2002. ICCAD 2002. IEEE/ACM International Conference on
Print_ISBN :
0-7803-7607-2
DOI :
10.1109/ICCAD.2002.1167584
