Industrial scale formal verification using concurrent GSTE

Author

Yang, Jin ; Ghughal, Rajnish ; Tiemeyer, Andreas

Author_Institution

Intel Corp., Santa Clara, CA

Volume

2

fYear

2005

fDate

24-0 Oct. 2005

Firstpage

930

Lastpage

933

Abstract

We give a detailed description of the formal specification and verification of a complex Intel(R) Pentium(R) 4 resource scheduler with over one thousand state elements using concurrent GSTE (CGSTE) l. CGSTE is a powerful extension of GSTE (generalized symbolic trajectory evaluation) for succinctly specifying and efficiently verifying the concurrent behavior of a complex circuit. We show how an operational high level specification (HLS) for the hardware was developed and cleanly captured in an algebraic-style specification language in CGSTE. The correctness of the hardware implementation was automatically verified against the HLS using the CGSTE model checker in the matter of two minutes

Keywords

formal specification; formal verification; microprocessor chips; specification languages; algebraic-style specification language; complex circuit; formal specification; generalized symbolic trajectory evaluation; high level specification; industrial scale formal verification; model checker; resource scheduler; Circuit simulation; Concurrent computing; Costs; Formal specifications; Formal verification; Hardware; High level synthesis; Job shop scheduling; Processor scheduling; Specification languages;

fLanguage

English

Publisher

ieee

Conference_Titel

ASIC, 2005. ASICON 2005. 6th International Conference On

Conference_Location

Shanghai

Print_ISBN

0-7803-9210-8

Type

conf

DOI

10.1109/ICASIC.2005.1611464

Filename

1611464