Document Open Access Logo

Wiring Circuits Is Easy as {0,1,ω}, or Is It...

Authors Jan de Muijnck-Hughes , Wim Vanderbauwhede

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.8.pdf
  • Filesize: 1.09 MB
  • 28 pages

Document Identifiers

Author Details

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

Funding

The work is funded by EPSRC grants: Border Patrol (EP/N028201/1) and AppControl (EP/V000462/1).

Cite AsGet BibTex

Jan de Muijnck-Hughes and Wim Vanderbauwhede. Wiring Circuits Is Easy as {0,1,ω}, or Is It.... In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 8:1-8:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.8

Abstract

Quantitative Type-Systems support fine-grained reasoning about term usage in our programming languages. Hardware Design Languages are another style of language in which quantitative typing would be beneficial. When wiring components together we must ensure that there are no unused ports, dangling wires, or accidental fan-ins and fan-outs. Although many wire usage checks are detectable using static analysis tools, such as Verilator, quantitative typing supports making these extrinsic checks an intrinsic aspect of the type-system. With quantitative typing of bound terms, we can provide design-time checks that all wires and ports have been used, and ensure that all wiring decisions are explicitly made, and are neither implicit nor accidental. We showcase the use of quantitative types in hardware design languages by detailing how we can retrofit quantitative types onto SystemVerilog netlists, and the impact that such a quantitative type-system has when creating designs. Netlists are gate-level descriptions of hardware that are produced as the result of synthesis, and it is from these netlists that hardware is generated (fabless or fabbed). First, we present a simple structural type-system for a featherweight version of SystemVerilog netlists that demonstrates how we can type netlists using standard structural techniques, and what it means for netlists to be type-safe but still lead to ill-wired designs. We then detail how to retrofit the language with quantitative types, make the type-system sub-structural, and detail how our new type-safety result ensures that wires and ports are used once. Our ideas have been proven both practically and formally by realising our work in Idris2, through which we can construct a verified language implementation that can type-check existing designs. From this work we can look to promote quantitative typing back up the synthesis chain to a more comprehensive hardware description language; and to help develop new and better hardware description languages with quantitative typing.

Subject Classification

ACM Subject Classification
  • Software and its engineering → General programming languages
  • Software and its engineering → Language features
  • Software and its engineering → Domain specific languages
  • Software and its engineering → System modeling languages
Keywords
  • Hardware Design
  • Linear Types
  • Dependent Types
  • DSLs
  • Idris
  • SystemVerilog
  • Netlists

Metrics

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

Supplementary Materials

References

  1. Guillaume Allais. Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. In 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, pages 1:1-1:22, 2017. URL: https://doi.org/10.4230/LIPIcs.TYPES.2017.1.
  2. 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: https://doi.org/10.1145/3236785.
  3. Nada Amin and Tiark Rompf. Type soundness proofs with definitional interpreters. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 666-679. ACM, 2017. URL: http://dl.acm.org/citation.cfm?id=3009866, URL: https://doi.org/10.1145/3009837.3009866.
  4. Robert Atkey. Syntax and Semantics of Quantitative Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 56-65, 2018. URL: https://doi.org/10.1145/3209108.3209189.
  5. Robert Atkey. Data Types with Negation. Extended Abstract (Talk Only) at Ninth Workshop on Mathematically Structured Functional Programming, Munich, Germany, 2nd April 2022, 2022. URL: https://youtu.be/mZZjOKWCF4A.
  6. Jonathan Bachrach, Huy Vo, Brian C. Richards, Yunsup Lee, Andrew Waterman, Rimas Avizienis, John Wawrzynek, and Krste Asanovic. Chisel: constructing hardware in a Scala embedded language. In Patrick Groeneveld, Donatella Sciuto, and Soha Hassoun, editors, The 49th Annual Design Automation Conference 2012, DAC '12, San Francisco, CA, USA, June 3-7, 2012, pages 1216-1225. ACM, 2012. URL: https://doi.org/10.1145/2228360.2228584.
  7. Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158093.
  8. Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, and Arvind. The essence of Bluespec: a core language for rule-based hardware design. In Alastair F. Donaldson and Emina Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 243-257. ACM, 2020. URL: https://doi.org/10.1145/3385412.3385965.
  9. Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program., 23(5):552-593, 2013. URL: https://doi.org/10.1017/S095679681300018X.
  10. Edwin C. Brady. Idris 2: Quantitative Type Theory in Practice. In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference), volume 194 of LIPIcs, pages 9:1-9:26. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2021.9.
  11. Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind. Kami: a platform for high-level parametric hardware specification and its modular verification. Proc. ACM Program. Lang., 1(ICFP):24:1-24:30, 2017. URL: https://doi.org/10.1145/3110268.
  12. Michael Christensen, Timothy Sherwood, Jonathan Balkind, and Ben Hardekopf. Wire sorts: a language abstraction for safe hardware composition. In Stephen N. Freund and Eran Yahav, editors, PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 20211, pages 175-189. ACM, 2021. URL: https://doi.org/10.1145/3453483.3454037.
  13. Deeksha Dangwal, Georgios Tzimpragos, and Timothy Sherwood. Agile Hardware Development and Instrumentation With PyRTL. IEEE Micro, 40(4):76-84, 2020. URL: https://doi.org/10.1109/MM.2020.2997704.
  14. Peter Flake, Phil Moorby, Steve Golson, Arturo Salz, and Simon Davidmann. Verilog HDL and Its Ancestors and Descendants. Proc. ACM Program. Lang., 4(HOPL), June 2020. URL: https://doi.org/10.1145/3386337.
  15. Dan R. Ghica. Geometry of synthesis: a structured approach to VLSI design. In Martin Hofmann and Matthias Felleisen, editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 363-375. ACM, 2007. URL: https://doi.org/10.1145/1190216.1190269.
  16. Dan R. Ghica. The Geometry of Synthesis - How to Make Hardware Out of Software. In Mathematics of Program Construction - 11th International Conference, MPC 2012, Madrid, Spain, June 25-27, 2012. Proceedings, pages 23-24, 2012. URL: https://doi.org/10.1007/978-3-642-31113-0_3.
  17. Dan R. Ghica and Alex I. Smith. Geometry of Synthesis II: From Games to Delay-Insensitive Circuits. In Michael W. Mislove and Peter Selinger, editors, Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2010, Ottawa, Ontario, Canada, May 6-10, 2010, volume 265 of Electronic Notes in Theoretical Computer Science, pages 301-324. Elsevier, 2010. URL: https://doi.org/10.1016/j.entcs.2010.08.018.
  18. Dan R. Ghica and Alex I. Smith. Geometry of synthesis III: resource management through type inference. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 345-356. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926425.
  19. Dan R. Ghica, Alex I. Smith, and Satnam Singh. Geometry of synthesis IV: compiling affine recursion into static hardware. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 221-233, 2011. URL: https://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: https://doi.org/10.1007/978-3-642-16478-1_2.
  21. Robert Griesemer, Raymond Hu, Wen Kokke, Julien Lange, Ian Lance Taylor, Bernardo Toninho, Philip Wadler, and Nobuko Yoshida. Featherweight Go. Proc. ACM Program. Lang., 4(OOPSLA):149:1-149:29, 2020. URL: https://doi.org/10.1145/3428217.
  22. Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal verification of high-level synthesis. Proc. ACM Program. Lang., 5(OOPSLA):1-30, 2021. URL: https://doi.org/10.1145/3485494.
  23. IEEE. IEEE Standard for SystemVerilog-Unified Hardware Design, Specification, and Verification Language, IEEE Std 1800-2017 edition, February 2018. URL: https://doi.org/10.1109/IEEESTD.2018.8299595.
  24. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst., 23(3):396-450, 2001. URL: https://doi.org/10.1145/503502.503505.
  25. Simon L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall, 1987. Google Scholar
  26. Wilayat Khan, Alwen Tiu, and David Sanán. VeriFormal: An Executable Formal Model of a Hardware Description Language. In Abhik Roychoudhury and Yang Liu, editors, A Systems Approach to Cyber Security - Proceedings of the 2nd Singapore Cyber-Security R&D Conference (SG-CRC 2017), Singapore, February 21-22, 2017, volume 15 of Cryptology and Information Security Series, pages 19-36. IOS Press, 2017. URL: https://doi.org/10.3233/978-1-61499-744-3-19.
  27. Wen Kokke, Jeremy G. Siek, and Philip Wadler. Programming language foundations in Agda. Sci. Comput. Program., 194:102440, 2020. URL: https://doi.org/10.1016/j.scico.2020.102440.
  28. Andreas Lööw. Lutsig: a verified Verilog compiler for verified circuit development. In Cătălin Hricommabelowtcu and Andrei Popescu, editors, CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 46-60. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439916.
  29. Conor McBride. Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In Bruno C. d. S. Oliveira and Marcin Zalewski, editors, Proceedings of the ACM SIGPLAN Workshop on Generic Programming, WGP 2010, Baltimore, MD, USA, September 27-29, 2010, pages 1-12. ACM, 2010. URL: https://doi.org/10.1145/1863495.1863497.
  30. 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: https://doi.org/10.1007/978-3-319-30936-1_12.
  31. Patrick O'Neil Meredith, Michael Katelman, José Meseguer, and Grigore Rosu. A formal executable semantics of Verilog. In 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), Grenoble, France, 26-28 July 2010, pages 179-188. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/MEMCOD.2010.5558634.
  32. Rishiyur S. Nikhil. Bluespec System Verilog: efficient, correct RTL from high level specifications. In 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 23-25 June 2004, San Diego, California, USA, Proceedings, pages 69-70. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/MEMCOD.2004.1459818.
  33. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. Quantitative program reasoning with graded modal types. PACMPL, 3(ICFP):110:1-110:30, 2019. URL: https://doi.org/10.1145/3341714.
  34. Jens Palsberg. Featherweight X10: a core calculus for async-finish parallelism. In Wei-Ngan Chin and Aquinas Hobor, editors, Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs, FTfJP 2012, Beijing, China, June 12, 2012, page 1. ACM, 2012. URL: https://doi.org/10.1145/2318202.2318203.
  35. Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser. Intrinsically-typed definitional interpreters for imperative languages. Proc. ACM Program. Lang., 2(POPL):16:1-16:34, 2018. URL: https://doi.org/10.1145/3158104.
  36. Dimitri Racordon and Didier Buchs. Featherweight Swift: a Core calculus for Swift’s type system. In Ralf Lämmel, Laurence Tratt, and Juan de Lara, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, Virtual Event, USA, November 16-17, 2020, pages 140-154. ACM, 2020. URL: https://doi.org/10.1145/3426425.3426939.
  37. John C. Reynolds. Definitional Interpreters for Higher-Order Programming Languages. High. Order Symb. Comput., 11(4):363-397, 1998. URL: https://doi.org/10.1023/A:1010027404223.
  38. John C. Reynolds. Definitional Interpreters Revisited. High. Order Symb. Comput., 11(4):355-361, 1998. URL: https://doi.org/10.1023/A:1010075320153.
  39. Thomas N. Reynolds, Adam M. Procter, William L. Harrison, and Gerard Allwein. A core calculus for secure hardware: its formal semantics and proof system. In Jean-Pierre Talpin, Patricia Derler, and Klaus Schneider, editors, Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, Vienna, Austria, September 29 - October 02, 2017, pages 122-131. ACM, 2017. URL: https://doi.org/10.1145/3127041.3127048.
  40. Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser. Intrinsically-typed definitional interpreters for linear, session-typed languages. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 284-298. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373818.
  41. Jeremy Siek. Type Safety in Three Easy Lemmas. Online, May 2013. URL: https://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html.
  42. 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: https://doi.org/10.4230/DagSemProc.10281.3.
  43. Arvind K. Sujeeth, Kevin J. Brown, HyoukJoong Lee, Tiark Rompf, Hassan Chafi, Martin Odersky, and Kunle Olukotun. Delite: A Compiler Architecture for Performance-Oriented Embedded Domain-Specific Languages. ACM Trans. Embedded Comput. Syst., 13(4s):134:1-134:25, 2014. URL: https://doi.org/10.1145/2584665.
  44. Philip Wadler. Linear Types can Change the World! In Manfred Broy and Cliff B. Jones, editors, Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990, page 561. North-Holland, 1990. Google Scholar
  45. David Walker. Advanced Topic in Types and Programming Languages, chapter Substructural Type Systems, pages 3-43. The MIT Press, 2004. Google Scholar
  46. James Wood and Robert Atkey. A Linear Algebra Approach to Linear Metatheory. In Ugo Dal Lago and Valeria de Paiva, editors, Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity & TLLA @ IJCAR-FSCD 2020, Online, 29-30 June 2020, volume 353 of EPTCS, pages 195-212, 2020. URL: https://doi.org/10.4204/EPTCS.353.10.
  47. Andrew K. Wright and Matthias Felleisen. A Syntactic Approach to Type Soundness. Inf. Comput., 115(1):38-94, 1994. URL: https://doi.org/10.1006/inco.1994.1093.
  48. Danfeng Zhang, Yao Wang, G. Edward Suh, and Andrew C. Myers. A Hardware Design Language for Timing-Sensitive Information-Flow Security. In Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '15, pages 503-516, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2694344.2694372.
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