Document Open Access Logo

A Typing Discipline for Hardware Interfaces

Authors Jan de Muijnck-Hughes , Wim Vanderbauwhede

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2019.6.pdf
  • Filesize: 0.64 MB
  • 27 pages

Document Identifiers

Author Details

Jan de Muijnck-Hughes
  • University of Glasgow, UK
Wim Vanderbauwhede
  • University of Glasgow, UK

Funding

This work is part of Border Patrol: Improving Smart Device Security through Type-Aware Systems Design (http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/N028201/1) and has been sponsored by an EPSRC funding call on Trust, Identity, Privacy and Security in the Digital Economy.

Acknowledgements

The authors would like to thank the anonymous reviewers for commenting on the paper, and also various members of Scottish Programming Language Community (SPLS) for their helpful comments on early versions of the work.

Cite AsGet BibTex

Jan de Muijnck-Hughes and Wim Vanderbauwhede. A Typing Discipline for Hardware Interfaces. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 6:1-6:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ECOOP.2019.6

Abstract

Modern Systems-on-a-Chip (SoC) are constructed by composition of IP (Intellectual Property) Cores with the communication between these IP Cores being governed by well described interaction protocols. However, there is a disconnect between the machine readable specification of these protocols and the verification of their implementation in known hardware description languages. Although tools can be written to address such separation of concerns, the tooling is often hand written and used to check hardware designs a posteriori. We have developed a dependent type-system and proof-of-concept modelling language to reason about the physical structure of hardware interfaces using user provided descriptions. Our type-system provides correct-by-construction guarantees that the interfaces on an IP Core will be well-typed if they adhere to a specified standard.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Hardware → System on a chip
  • Software and its engineering → System description languages
Keywords
  • System-on-a-Chip
  • AXI
  • Dependent Types
  • Substructural Typing

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. A type and scope safe universe of syntaxes with binding: their semantics and proofs. PACMPL, 2(ICFP):90:1-90:30, 2018. URL: http://dx.doi.org/10.1145/3236785.
  2. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical Reconstruction of a Reduction Free Normalization Proof. In David H. Pitt, David E. Rydeheard, and Peter T. Johnstone, editors, Category Theory and Computer Science, 6th International Conference, CTCS '95, Cambridge, UK, August 7-11, 1995, Proceedings, volume 953 of Lecture Notes in Computer Science, pages 182-199. Springer, 1995. URL: http://dx.doi.org/10.1007/3-540-60164-3_27.
  3. ARM Limited. AMBA APB Protocol, ARM IHI 0024C edition, 2010. Google Scholar
  4. ARM Limited. AXI and ACE Protocol Specification, ARM IHI 0022F.b edition, 2017. Google Scholar
  5. Robert Atkey. Parameterised notions of computation. J. Funct. Program., 19(3-4):335-376, 2009. URL: http://dx.doi.org/10.1017/S095679680900728X.
  6. Robert Atkey. Syntax and Semantics of Quantitative Type Theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 56-65. ACM, 2018. URL: http://dx.doi.org/10.1145/3209108.3209189.
  7. Lennart Augustsson and Magnus Carlsson. An Exercise in Dependent Types: A Well-Typed Interpreter. In In Workshop on Dependent Types in Programming, Gothenburg, 1999. Google Scholar
  8. Johannes Borgström, Juan Chen, and Nikhil Swamy. Verifying stateful programs with substructural state and hoare types. In Ranjit Jhala and Wouter Swierstra, editors, Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, Austin, TX, USA, January 29, 2011, pages 15-26. ACM, 2011. URL: http://dx.doi.org/10.1145/1929529.1929532.
  9. Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program., 23(5):552-593, 2013. URL: http://dx.doi.org/10.1017/S095679681300018X.
  10. Edwin Brady. Programming and reasoning with algebraic effects and dependent types. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 133-144. ACM, 2013. URL: http://dx.doi.org/10.1145/2500365.2500581.
  11. Edwin Brady. Resource-Dependent Algebraic Effects. In Jurriaan Hage and Jay McCarthy, editors, Trends in Functional Programming - 15th International Symposium, TFP 2014, Soesterberg, The Netherlands, May 26-28, 2014. Revised Selected Papers, volume 8843 of Lecture Notes in Computer Science, pages 18-33. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-14675-1_2.
  12. Edwin Brady. Type-Driven Development with Idris. Manning, 1st edition, 2016. Google Scholar
  13. James Maitland Chapman. Type checking and normalisation. PhD thesis, School of Computer Science, University of Nottingham, July 2009. URL: http://eprints.nottingham.ac.uk/10824/.
  14. Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay A. McCarthy, and Sam Tobin-Hochstadt. A programmable programming language. Commun. ACM, 61(3):62-71, 2018. URL: http://dx.doi.org/10.1145/3127323.
  15. J Pizani Flor. π-Ware: An Embedded Hardware Description Language using Dependent Types. Masters, Department of Information and Computing Sciences, 2014. URL: https://dspace.library.uu.nl/bitstream/handle/1874/298576/.
  16. João Paulo Pizani Flor, Wouter Swierstra, and Yorick Sijsling. Pi-Ware: Hardware Description and Verification in Agda. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, volume 69 of LIPIcs, pages 9:1-9:27. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.TYPES.2015.9.
  17. Dan R. Ghica. The Geometry of Synthesis - How to Make Hardware Out of Software. In Jeremy Gibbons and Pablo Nogueira, editors, Mathematics of Program Construction - 11th International Conference, MPC 2012, Madrid, Spain, June 25-27, 2012. Proceedings, volume 7342 of Lecture Notes in Computer Science, pages 23-24. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31113-0_3.
  18. Dan R. Ghica, Achim Jung, and Aliaume Lopez. Diagrammatic Semantics for Digital Circuits. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden, volume 82 of LIPIcs, pages 24:1-24:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2017.24.
  19. Dan R. Ghica, Alex I. Smith, and Satnam Singh. Geometry of synthesis iv: compiling affine recursion into static hardware. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 221-233. ACM, 2011. URL: http://dx.doi.org/10.1145/2034773.2034805.
  20. Andy Gill, Tristan Bull, Garrin Kimmell, Erik Perrins, Ed Komp, and Brett Werling. Introducing Kansas Lava. In Marco T. Morazán and Sven-Bodo Scholz, editors, Implementation and Application of Functional Languages - 21st International Symposium, IFL 2009, South Orange, NJ, USA, September 23-25, 2009, Revised Selected Papers, volume 6041 of Lecture Notes in Computer Science, pages 18-35. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-16478-1_2.
  21. John Hatcliff and Olivier Danvy. A Generic Account of Continuation-Passing Styles. In Hans-Juergen Boehm, Bernard Lang, and Daniel M. Yellin, editors, Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994, pages 458-471. ACM Press, 1994. URL: http://dx.doi.org/10.1145/174675.178053.
  22. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 273-284. ACM, 2008. URL: http://dx.doi.org/10.1145/1328438.1328472.
  23. IEEE. IEEE Standard for IP-XACT, Standard Structure for Packaging, Integrating, and Reusing IP within Tool Flows, ieee std 1685-2014 edition, September 2014. URL: http://dx.doi.org/10.1109/IEEESTD.2014.6898803.
  24. Antti Kamppi, Lauri Matilainen, Joni-Matti Määttä, Erno Salminen, Timo D. Hämäläinen, and Marko Hännikäinen. Kactus2: Environment for Embedded Product Development Using IP-XACT and MCAPI. In 14th Euromicro Conference on Digital System Design, Architectures, Methods and Tools, DSD 2011, August 31 - September 2, 2011, Oulu, Finland, pages 262-265. IEEE Computer Society, 2011. URL: http://dx.doi.org/10.1109/DSD.2011.36.
  25. Eddie Kohler, Robert Tappan Morris, Benjie Chen, John Jannotti, and M. Frans Kaashoek. The click modular router. ACM Trans. Comput. Syst., 18(3):263-297, 2000. URL: http://dx.doi.org/10.1145/354871.354874.
  26. Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, and Deepak Garg. Superficially substructural types. In Peter Thiemann and Robby Bruce Findler, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012, pages 41-54. ACM, 2012. URL: http://dx.doi.org/10.1145/2364527.2364536.
  27. Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. A static verification framework for message passing in Go using behavioural types. In Michel Chaudron, Ivica Crnkovic, Marsha Chechik, and Mark Harman, editors, Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018, pages 1137-1148. ACM, 2018. URL: http://dx.doi.org/10.1145/3180155.3180157.
  28. Per Martin-Löf and Giovanni Sambin. Intuitionistic Type Theory. Bibliopolis, 1984. Google Scholar
  29. Conor McBride. I Got Plenty o' Nuttin'. In Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella, editors, A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of Lecture Notes in Computer Science, pages 207-233. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-30936-1_12.
  30. Paul Edward McKechnie. Validation and verification of the interconnection of hardware intellectual property blocks for FPGA-based packet processing systems. PhD thesis, University of Glasgow, 2010. URL: http://theses.gla.ac.uk/1879/.
  31. Filipe Militão, Jonathan Aldrich, and Luís Caires. Substructural typestates. In Nils Anders Danielsson and Bart Jacobs, editors, Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, PLPV 2014, January 21, 2014, San Diego, California, USA, Co-located with POPL '14, pages 15-26. ACM, 2014. URL: http://dx.doi.org/10.1145/2541568.2541574.
  32. Aleksandar Nanevski, J. Gregory Morrisett, and Lars Birkedal. Hoare type theory, polymorphism and separation. J. Funct. Program., 18(5-6):865-911, 2008. URL: http://dx.doi.org/10.1017/S0956796808006953.
  33. Ulf Norell. Dependently typed programming in Agda. In Andrew Kennedy and Amal Ahmed, editors, Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009, pages 1-2. ACM, 2009. URL: http://dx.doi.org/10.1145/1481861.1481862.
  34. John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55-74. IEEE Computer Society, 2002. URL: http://dx.doi.org/10.1109/LICS.2002.1029817.
  35. Gerard J. M. Smit, Jan Kuper, and Christiaan P. R. Baaij. A mathematical approach towards hardware design. In Peter M. Athanas, Jürgen Becker, Jürgen Teich, and Ingrid Verbauwhede, editors, Dynamically Reconfigurable Architectures, 11.07. - 16.07.2010, volume 10281 of Dagstuhl Seminar Proceedings. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2010. URL: http://drops.dagstuhl.de/opus/volltexte/2010/2840/.
  36. Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. Secure distributed programming with value-dependent types. J. Funct. Program., 23(4):402-451, 2013. URL: http://dx.doi.org/10.1017/S0956796813000142.
  37. Wouter Swierstra. A Hoare Logic for the State Monad. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 440-451. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-03359-9_30.
  38. Muralidaran Vijayaraghavan, Adam Chlipala, Arvind, and Nirav Dave. Modular Deductive Verification of Multiprocessor Hardware Designs. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, volume 9207 of Lecture Notes in Computer Science, pages 109-127. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-21668-3_7.
  39. Product page for Vivado IP Integrator by Xilinx. Online, 2019. URL: https://www.xilinx.com/products/design-tools/vivado/integration.html.
  40. David Walker. Advanced Topic in Types and Programming Languages, chapter Substructural Type Systems, pages 3-43. The MIT Press, 2004. Google Scholar
  41. Xilinx. LocalLink Interface Specification, SP006 (v2.0) edition, 2005. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact