Verifying deadlock-freedom of communication fabrics

DOI10.1007/978-3-642-18275-4_16zbMATH Open1317.68115OpenAlexW3139271637MaRDI QIDQ3075484FDOQ3075484

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

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

zbMATH Keywords

formal verificationlivenesscommunication fabricshigh-level modelsmicroarchitecturenetworks-on-chipdeadlocks

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (9)

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

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)