Scaling up livelock verification for network-on-chip routing algorithms

DOI10.1007/978-3-030-94583-1_19zbMath1498.68173OpenAlexW4205102018MaRDI QIDQ2152663

Zhen Zhang, Landon Taylor

Publication date: 8 July 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-94583-1_19

zbMATH Keywords

model checkingnetwork-on-chipfault-tolerant routingproperty-directed reachability

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07) Reliability, testing and fault tolerance of networks and computer systems (68M15)

Uses Software

• ACL2
• IF-2.0
• SPIN
• z3
• CADP
• ABC
• LNT2LOTOS
• ABS
• GitHub
• Ivy

Cites Work

• Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks
• CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
• Unnamed Item

This page was built for publication: Scaling up livelock verification for network-on-chip routing algorithms