Verification of Register Transfer Level (RTL) designs is still a challenging task. Even today, simulation is often considered the only viable option for verifying designs before implementation. Thereby, Formal Property Verification (FPV) provides an additional verification approach. Capable of addressing simulation-specific problems like incompleteness and frequently able to be more efficient concerning complexity and consumed time. This paper shows how FPV is applied to prove the major functionality of a SpaceWire router which covers packet arbitration and data integrity properties. On one hand, the paper includes basic approaches to allow property definitions for packet-based designs. On the other hand, typical FPV problems like system complexity issues are discussed and possible solutions are outlined.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal Arbitration and Data Integrity Checking of a SpaceWire Router IP-Core


    Beteiligte:
    Borchers, Kai (Autor:in)


    Erscheinungsdatum :

    04.03.2023


    Format / Umfang :

    458882 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    SpaceWire Router

    Parkes, Steve / McClements, Chris / Kempf, Gerald et al. | BASE | 2003

    Freier Zugriff


    SpaceWire Router Boards

    Saunders, S. / Gross, D. | Springer Verlag | 2022


    GR740 SpaceWire router validation methodology and results: SpaceWire components, long paper

    Hjorth, Magnus / Jalle, Javier / Siegle, Felix et al. | IEEE | 2016


    SpaceWire standard and improved wormhole router design

    Yi, Dalu / Yu, Lixin / Fei, Haidong et al. | IEEE | 2012