Verified compilation of communicating processes into clocked circuits

DOI10.1007/BF01211459MaRDI QIDQ1267038zbMATH OpenFDO

Authors K. Appert, John O'Leary, Geoffrey L. Brown, Wayne Luk

Publication date 11 January 1999

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

Full work available at URL https://doi.org/10.1007/BF01211459

zbMATH Keywords

clocked implementationprotocol conversion

Mathematics Subject Classification ID

Computer system organization (68M99) Theory of compilers and interpreters (68N20)

Recommendations

• Retargeting a hardware compiler using protocol converters
• Compiling communicating processes into delay-insensitive VLSI circuits
• An approach to the specification and verification of a hardware compilation scheme
• scientific article; zbMATH DE number 868112
• Geometry of synthesis. II: From games to delay-insensitive circuits

Cites work

• Handshake Circuits
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 43800 (Why is no real title available?)
• scientific article; zbMATH DE number 559729 (Why is no real title available?)
• Process simulation and refinement
• Retargeting a hardware compiler using protocol converters

Cited in

(7)

• Verified timing transformations in synchronous circuits with \(\lambda\pi\)-Ware
• Retargeting a hardware compiler using protocol converters
• scientific article; zbMATH DE number 1670834 (Why is no real title available?)
• Mechanised wire-wise verification of Handel-C synthesis
• scientific article; zbMATH DE number 1418462 (Why is no real title available?)
• Mechanised wire-wise verification of Handel-C synthesis
• An approach to the specification and verification of a hardware compilation scheme

This page was built for publication: Verified compilation of communicating processes into clocked circuits

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