Formal verification methodology for real‐time Field Programmable Gate Array
| Autor: | Shaista Jabeen, Sana Shuja, Sudarshan K. Srinivasan |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Correctness
Computer science Liveness 020207 software engineering 02 engineering and technology Programmable logic array 020202 computer hardware & architecture Programmable Array Logic Computer engineering Hardware and Architecture Gate array Scalability 0202 electrical engineering electronic engineering information engineering Electrical and Electronic Engineering Field-programmable gate array Formal verification Software |
| Zdroj: | IET Computers & Digital Techniques. 11:197-203 |
| ISSN: | 1751-861X 1751-8601 |
| DOI: | 10.1049/iet-cdt.2016.0189 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Plný text