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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

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


    Contributors:


    Publication date :

    2023-03-04


    Size :

    458882 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    SpaceWire Router

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

    Free access


    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