ReWire: Functional Hardware Description

ReWire is an open source programming language for designing, implementing, and formally verifying hardware artifacts. ReWire is a language for high-level synthesis based in the functional language Haskell. Functional languages are a commonly proposed approach to alleviating the well-known FPGA programmability problem—a.k.a., the three P’s (Productivity, Performance and Portability). But the ReWire approach takes this one step further with Provability.

Screenshot

ReWire programs are Haskell programs. That means, every ReWire program is a Haskell program as well. And so, ReWire inherits many of Haskell’s fine qualities, including:

  • Pure functions and types, monads, equational reasoning, etc.
  • Formal semantics supporting formal reasoning.

ReWire programs, however, may all be translated directly to VHDL using the ReWire compiler:

Screenshot

Why does all this distinguish us from other research efforts? Read on!

What’s New?

  • ReWire, Version 2.0, released on July 21, 2021! This included a number of improvements to the VHDL backend and a swathe of bug fixes.
  • The ReWire language and compiler is currently under intense and active development and is, therefore, something of a moving target. E.g., we have added a Verilog backend, among other things.
  • Our development of the language and compiler has outstripped our now quite dusty website; writing documentation is like eating broccoli. If you have any questions, please send us an email.

Just Say No! to Semantic Archaeology

Say you have a hardware design written in a production hardware description language (HDL) like VHDL or Verilog and you need to formally verify some properties of the design and implementation. Where do you start?

Well, you can’t reason directly about the HDL code. Why not? Because the HDL possesses no formal semantics! Using traditional formal methods for hardware (e.g., Kropf 1999), one must laboriously formulate a formal model in the logic of a theorem prover. We call this process semantic archaeology and it is expensive, time-consuming and error-prone (i.e., how do you know that your formal specification is related to the concrete HDL design?). Semantic archaeology is the bane of formal methods.

Because ReWire has a formal semantics, one can reason about hardware designs in ReWire directly on the ReWire code itself just as one would about a normal pure functional program. One can also apply tools and techniques from software verification to hardware verification (e.g., as we have with Coq and language-based methods in security). For more information, please consult the reading below or send an email.

Further Reading

  • A Mechanized Semantic Metalanguage for High Level Synthesis., Bill Harrison, Chris Hathhorn, and Gerard Allwein. Proceedings of PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming. pdf
  • Strongly Bounded Termination with Applications to Security and Hardware Synthesis., Tom Reynolds, Rohit Chadha, Bill Harrison, and Gerard Allwein. Proceedings of TyDe 2020: ACM Workshop on Type Driven Development. pdf
  • Verifiable Security Templates for Hardware., Bill Harrison and Gerard Allwein. Proceedings of 2020 Design, Automation, and Test Europe (DATE). pdf
  • Language Abstractions for Hardware-based Control-Flow Integrity Monitoring. Bill Harrison and Gerard Allwein. Proceedings of the 2018 International Conference on Reconfigurable Computing and FPGAs. pdf
  • The Mechanized Marriage of Effects and Monads with Applications to High Assurance Hardware. Tom Reynolds, Bill Harrison, Adam Procter, and Gerard Allwein. To appear in ACM Transactions on Embedded Computing Systems. pdf
  • Semantics-directed Prototyping of Hardware Runtime Monitors. Bill Harrison and Gerard Allwein. To appear in Proceedings of the 29th International Symposium on Rapid System Prototyping (RSP). pdf
  • A Core Calculus for Secure Hardware: Its Formal Semantics and Proof System. Tom Reynolds, Adam Procter, Bill Harrison, and Gerard Allwein. 15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE17). pdf
  • A Programming Model for Reconfigurable Computing Based in Functional Concurrency, William L. Harrison, Adam Procter, Ian Graves, Michela Becchi, and Gerard Allwein. ReCoSoC 2016 pdf slides.
  • Provably Correct Development of Reconfigurable Hardware Designs via Equational Reasoning, Ian Graves, Adam Procter, William L. Harrison, and Gerard Allwein. FPT 2015 pdf slides.
  • A Principled Approach to Secure Multi-Core Processor Design with ReWire, Adam Procter, William Harrison, Ian Graves, Michela Becchi, and Gerard Allwein. ACM Transactions on Embedded Computing Systems (to appear) pdf.
  • Semantics Driven Hardware Design, Implementation, and Verification with ReWire, Adam Procter, William Harrison, Ian Graves, Michela Becchi, and Gerard Allwein. LCTES 2015 pdf.
  • Hardware Synthesis from Functional Embedded Domain-Specific Languages: A Case Study in Regular Expression Compilation, Ian Graves, Adam Procter, William Harrison, Michela Becchi, and Gerard Allwein. ARC 2015 pdf.