Formal verification methodology for real‐time Field Programmable Gate Array. Issue 5 (9th August 2017)

• Record Type: Journal Article
• Authors: Jabeen, Shaista; Srinivasan, Sudarshan; Shuja, Sana
• Is Part Of: IET computers & digital techniques. Volume 11:Issue 5(2017)
• Page Start: 197
• Page End: 203
• Publication Date: 2017-08-09
• Subjects: formal verification -- field programmable gate arrays; formal verification methodology -- real‐time field programmable gate array -- real‐time digital controllers -- timed transition systems -- high‐level specification requirements -- timed well‐founded simulation -- proof obligation templates; Computers -- Periodicals; Digital electronics -- Periodicals; Computer engineering -- Periodicals; Computer architecture -- Periodicals; Computer organization -- Periodicals; 621.39
• DOI: 10.1049/iet-cdt.2016.0189
• Languages: English
• ISSNs: 1751-8601

Abstract

Abstract : A formal verification methodology for checking both functional and timing requirements of real‐time digital controllers targeted at field programmable gate array technology is proposed. Timed transition systems (TTSs) are used to model both the digital controller circuit and the high‐level specification requirements. Timed well‐founded simulation (TWFS) refinement is used as the notion of correctness and defines what it means for an implementation TTS to satisfy a specification TTS. The primary contribution is a set of proof obligation templates (based on TWFS refinement) that account for both functional and timing requirements. The proof obligations generated using the templates can be checked using a decision procedure. One of the key ideas is the overloaded use of rank functions (that are typically used for liveness verification) for timing verification. The efficiency and scalability of the approach is demonstrated using three case studies.