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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal Property Verification of a Remote Memory Access Protocol IP-Core


    Contributors:


    Publication date :

    2022-03-05


    Size :

    766121 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    SpaceWire Remote Memory Access Protocol

    Parkes, S. / McClements, C. / Eurospace | British Library Conference Proceedings | 2005


    SpaceWire Remote Memory Access Protocol

    Cook, B. M. / Walker, C. H. P. / Eurospace | British Library Conference Proceedings | 2005



    Formal Verification of the LDACS MAKE Protocol

    Mäurer, Nils / Grundner-Culemann, Sophia | German Aerospace Center (DLR) | 2022

    Free access