A functional formalization of on chip communications

DOI10.1007/S00165-007-0049-0MaRDI QIDQ931433zbMATH OpenOpenAlexFDO

Authors Julien Schmaltz, Dominique Borrione

Publication date 25 June 2008

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-007-0049-0

zbMATH Keywords

Automated theorem provingCommunication architecturesFormal methodsNetworks on chip

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07) Computer system organization (68M99)

Recommendations

• Formalizing on chip communications in a functional style
• Theorem Proving in Higher Order Logics
• Formal Methods in Computer-Aided Design
• Networks-on-Chips
• The Verification of the On-Chip COMA Cache Coherence Protocol

Cites work

• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• Correct Hardware Design and Verification Methods
• Formal Methods in Computer-Aided Design
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Formalizing on chip communications in a functional style
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• Modeling layered distributed communication systems
• Theorem Proving in Higher Order Logics

Cited in

(5)

• Formalizing on chip communications in a functional style
• Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks
• Theorem Proving in Higher Order Logics
• Formal Methods in Computer-Aided Design
• A formalisation of \textsc{xMAS}

Describes a project that uses

Uses Software

• PVS
• ACL2
• HOL
• NQTHM

This page was built for publication: A functional formalization of on chip communications

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