ReWire Hardware circuits from functional specifications

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.

The four P's: Productivity, Performance, Portability, and Provability

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:

ReWire programs, however, may all be translated directly to synthesizable hardware—Verilog or VHDL—using the ReWire compiler:

The ReWire compilation flow: ReWire, a subset of Haskell, compiles to synthesizable HDL

What’s New?

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