Borchers, Kai and Firchau, Thomas (2022) Formal Property Verification of a Remote Memory Access Protocol IP-Core. In: 2022 IEEE Aerospace Conference, AERO 2022. IEEE Aerospace Conference 2022, 2022-05-03 - 2022-12-03, Big Sky MT, United States. doi: 10.1109/AERO53065.2022.9843263. ISBN 978-166543760-8. ISSN 1095-323X.
PDF
- Only accessible within DLR
770kB |
Abstract
Formal Property Verification (FPV) of Register-Transfer Level (RTL) designs have been adopted in many industry domains. It provides the ability to evaluate full state spaces rather than selecting a subset as it is done for functional simulation. This, in turn, drastically decreases the appearance of bug escapes. This paper demonstrates how FPV is applied to a packet-based Field Programmable Gate Array (FPGA) design. It shows how additional code alongside property definitions can help to capture and compare packet data fields. Additionally, encountered FPV specific problems and possible solutions are discussed.
Item URL in elib: | https://elib.dlr.de/188180/ | ||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Document Type: | Conference or Workshop Item (Speech) | ||||||||||||
Title: | Formal Property Verification of a Remote Memory Access Protocol IP-Core | ||||||||||||
Authors: |
| ||||||||||||
Date: | 2022 | ||||||||||||
Journal or Publication Title: | 2022 IEEE Aerospace Conference, AERO 2022 | ||||||||||||
Refereed publication: | Yes | ||||||||||||
Open Access: | No | ||||||||||||
Gold Open Access: | No | ||||||||||||
In SCOPUS: | Yes | ||||||||||||
In ISI Web of Science: | Yes | ||||||||||||
DOI: | 10.1109/AERO53065.2022.9843263 | ||||||||||||
ISSN: | 1095-323X | ||||||||||||
ISBN: | 978-166543760-8 | ||||||||||||
Status: | Published | ||||||||||||
Keywords: | FPGA, Formal, SVA, Model checking | ||||||||||||
Event Title: | IEEE Aerospace Conference 2022 | ||||||||||||
Event Location: | Big Sky MT, United States | ||||||||||||
Event Type: | international Conference | ||||||||||||
Event Start Date: | 3 May 2022 | ||||||||||||
Event End Date: | 3 December 2022 | ||||||||||||
HGF - Research field: | Aeronautics, Space and Transport | ||||||||||||
HGF - Program: | Space | ||||||||||||
HGF - Program Themes: | Space System Technology | ||||||||||||
DLR - Research area: | Raumfahrt | ||||||||||||
DLR - Program: | R SY - Space System Technology | ||||||||||||
DLR - Research theme (Project): | R - ScOSA Flight Experiment | ||||||||||||
Location: | Bremen | ||||||||||||
Institutes and Institutions: | Institute of Space Systems > Avionics Systems | ||||||||||||
Deposited By: | Borchers, Kai | ||||||||||||
Deposited On: | 07 Sep 2022 11:15 | ||||||||||||
Last Modified: | 24 Apr 2024 20:49 |
Repository Staff Only: item control page