Title :
Formal Verification of System Level Designs: A GSM Vocoder Case Study
Author :
Sammane, Ghiath Al ; Mohamed, Otmane Ait
Author_Institution :
Concordia Univ., Montreal
Abstract :
System-level design of embedded systems is essential to enhance designer productivity. Several design methodologies has been emerged using languages such as SystemC or SpecC that addresses the industry´s need for a fast time-to-market. The higher abstraction level offered by these new methodologies is a challenge to rigorous, formal verification. This paper describes the formal verification of designs written in SpecC at the specification level. The method is illustrated on a high level description of the GSM Vocoder: a voice encoder decoder based on the European GSM standard. We define a set of properties P that the GSM Vocoder should satisfy. Essentially, P describes the temporal specification of the Vocoder, including properties about: timing, concurrency, states transitions and communication.
Keywords :
cellular radio; embedded systems; formal verification; systems analysis; vocoders; European GSM standard; GSM Vocoder; SpecC specification language; embedded systems; formal verification; system level design; voice encoder decoder; Decoding; Design methodology; Embedded system; Formal verification; GSM; Productivity; System-level design; Time to market; Timing; Vocoders;
Conference_Titel :
Electrical and Computer Engineering, 2007. CCECE 2007. Canadian Conference on
Conference_Location :
Vancouver, BC
Print_ISBN :
1-4244-1020-7
Electronic_ISBN :
0840-7789
DOI :
10.1109/CCECE.2007.355