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
Conference paper
Electronic Resource
English
SpaceWire Remote Memory Access Protocol
British Library Conference Proceedings | 2005
|SpaceWire Remote Memory Access Protocol
British Library Conference Proceedings | 2005
|