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.
Formal Property Verification of a Remote Memory Access Protocol IP-Core
2022-03-05
766121 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch
SpaceWire Remote Memory Access Protocol
British Library Conference Proceedings | 2005
|SpaceWire Remote Memory Access Protocol
British Library Conference Proceedings | 2005
|Formal Verification of the LDACS MAKE Protocol
Deutsches Zentrum für Luft- und Raumfahrt (DLR) | 2022
|