Verifying deadlock-freedom of communication fabrics

DOI10.1007/978-3-642-18275-4_16MaRDI QIDQ3075484zbMATHOpenAlexFDO

Authors Alexander Gotmanov, Satrajit Chatterjee, Michael Kishinevsky

Publication date 15 February 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-18275-4_16

zbMATH Keywords

formal verificationlivenesscommunication fabricshigh-level modelsmicroarchitecturenetworks-on-chipdeadlocks

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics
• Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks
• Scaling up livelock verification for network-on-chip routing algorithms
• The pursuit of deadlock freedom
• Deadlock-free channels and locks

Cites work

• Correct Hardware Design and Verification Methods
• Proving that non-blocking algorithms don't block
• Reachability problems in piecewise FIFO systems

Cited in

(9)

• An Expressive Framework for Verifying Deadlock Freedom
• Verification, Model Checking, and Abstract Interpretation
• Scaling up livelock verification for network-on-chip routing algorithms
• Construction of Deadlock-free Designs of Communication Protocols from Observations
• Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics
• scientific article; zbMATH DE number 7314999 (Why is no real title available?)
• Formal verification of a deadlock detection algorithm
• A formalisation of \textsc{xMAS}
• Verification of building blocks for asynchronous circuits

Describes a project that uses

Uses Software

• ABC

This page was built for publication: Verifying deadlock-freedom of communication fabrics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3075484)