Home

Functional Netlists

Functional Netlists, Sungwoo Park, Jinha Kim, Hyeonseung Im. ICFP 2008.

In efforts to overcome the complexity of the syntax and the lack of formal semantics of conventional hardware description languages, a number of functional hardware description languages have been developed. Like conventional hardware description languages, however, functional hardware description languages eventually convert all source programs into netlists, which describe wire connections in hardware circuits at the lowest level and conceal all high-level descriptions written into source programs.

We develop a variant of the lambda calculus, called l-lambda (linear lambda), which may serve as a high-level substitute for netlists. In order to support higher-order functions, l-lambda uses a linear type system which enforces the linear use of variables of function type. The translation of l-lambda into structural descriptions of hardware circuits is sound and complete in the sense that it maps expressions only to realizable hardware circuits and that every realizable hardware circuit has a corresponding expression in l-lambda. To illustrate the use of l-lambda as a high-level substitute for netlists, we design a simple hardware description language that extends l with polymorphism, and use it to implement a Fast Fourier Transform circuit.

Given the recent discussion about hardware synthesis languages, the appearance of this paper seems timely. The use of linear types is perhaps unsurprising from a technical point of view, but it's surprising when you consider how frequently and in how many different contexts they appear.

Also, one thing I don't understand: there's apparently a difference between a "hardware description language" and a "hardware synthesis language". If anyone could explain what the difference means, I'd appreciate it. :)

By neelk at 2008-07-09 21:53 | DSL | Functional | other blogs | 11899 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

"hardware description" versus "hardware synthesis"

A hardware description language is used to describe the actual behavior of electronic circuits so that you can simulate them. (This is part of the standard design process for electronic circuits; especially if you're building an integrated circuit, you want a design that's going to work the first time, since the edit-compile-debug cycle is very long and very expensive.)

A hardware synthesis language describes the desired behavior of electronic circuits; a synthesizer compiles this description into a netlist that is used to build the circuit.

A hardware description language may be more detailed than a synthesis language; for instance, it may give detailed timing information, saying that a particular AND gate produces its output between 3 and 4 nanoseconds after the inputs change. A simulator will then keep track of all the times involved, and will propagate a 1-nanosecond-long pulse of "invalid" through the rest of the system, and report a potential error if any of the outputs of the system depend on the value of this signal during its invalid time.

A synthesis language, on the other hand, would probably just describe the AND gate without any timing information; the timing requirements would be specified elsewhere, by saying that the input of any register must be stable at the rising edge of the clock.

On the other hand, the hardware description language may be less detailed. For a multiplier, for instance, it might just say that it is a multiplier, without giving details of the internals of the circuit. If you're describing an entire circuit board, then entire chips may be given simulation models that are wholly inadequate for synthesis (for example, a microcontroller might be described by giving a reference to a C library that simulates the microcontroller).

It's common to use a single language for both purposes. For example, Verilog and VHDL are both hardware description languages; but both have a (somewhat informally specified) "synthesizable subset" that is accepted by synthesizers (different synthesizers may accept different subsets).

By Carl Witty at Wed, 2008-07-09 23:49 | login or register to post comments

Somewhat disappointing discussion

Since there has been a discussion of the relationship between proof nets for linear logic and circuits ever since (at least) Abramsky's Proofs as processes, I'd have like to see at least some mention of the suitability or not of work from this train of research. In particular, I'd have liked to have seen a mention of Yves Lafont's Towards an algebraic theory of Boolean circuits (mentioned briefly in the discussion for Ralf Hinze: An algebra of scans, also relevant to this paper). In particular, this related literature is relevant to the question "Have we got a good abstract representation of circuits?".

By Charles Stewart at Thu, 2008-07-10 10:22 | login or register to post comments

Geometry of Synthesis

The author's do, however, cite, Dan Ghica's very interesting looking Geometry of Synthesis, from last year's POPL. The calculus of the paper is based on Peter O'Hearn's syntatcic control of interference for typing Idealised Algol, and he claims that the geometry of interaction (GoI) guides the design of the calculus, although I have not found an attempt to give a GoI for the calculus.

By Charles Stewart at Thu, 2008-07-10 10:40 | login or register to post comments

*delete*

*comment from possible Drupal bug*

By Charles Stewart at Thu, 2008-07-10 10:22 | login or register to post comments