Categorical semantics of digital circuits

Isn’t it funny that the world of programming languages is defined by syntax while the world of circuit design is defined by semantics? One can never be sure, but it seems to me that when people design software they imagine the code whereas when people design circuits they imagine the behaviour. This seems also to apply to the design of programming languages, where an endless variety of syntaxes exist, all essentially doing the same thing (crudely speaking) but in weirdly different ways. In hardware design there are only two syntaxes (languages) worth considering, VHDL and Verilog. Unlike programming languages, hardware language don’t even trap you into a particular ecosystem and most tools allow you to happily interoperate the two. These hardware languages may be, from the point of view of a programmer, quite horrible but, since I am typing this post on a working computer and sending it over to a global network of working computers, these horrible hardware languages seem to get the job done.

The hardware-software contrast carries over into the semantics of the two classes of languages. The semantics of programming languages is most commonly specified as syntactic transformation rules called operational semantics. For example in any programming language there is a rule that says that the phrase “1+1″ can be safely replaced with “2″. Of course, these rules can be very complicated, describing how functions are called, exceptions are managed, input-output interactions handled and so on. But the idea is that a program and some additional configuration information can be reduced to a “simpler” program with some (potentially different) configuration information.

On the other hand, the semantics of a circuit is most commonly given as sets of waveforms which describe directly the evolution in time of a measurable parameter at any chosen point in the circuit — a simulation, informally speaking. There are similar behavioural approaches to giving semantics to programming languages (denotational semantics) but they are not as widely used in applications (although they are very interesting things to study!).

What is quite surprising is that there is no equivalent of operational semantics for digital circuits — at least nothing I could find. The closest I can mention is the ground-breaking work by Mary Sheeran in the 1980s on using functional languages to specify circuit designs. As a part of this approach she specifies some equations for simplifying circuits, which can serve as part of an operational semantics — but more axioms are needed for that.

One thing that Sheeran’s work makes implicitly clear is that the conventional syntax of hardware languages is too unstructured to be useful for the formulation of axioms, and consequently for operational syntax-level modelling. Her Haskell-based syntax has the requisite mathematical structure so that axioms can be formulated. But how do we know what axioms are needed?

Circuits in general are diagrams of interconnected components (e.g. logical gates) and the way we like to think of them is up to topological isomorphism. This means that when we design a circuit we prefer not to think about the geometry of the interconnect (the wires lengths and shapes) but only the topology (what connects to what). The geometric details (in particular the presence of very long wires or especially very long parallel wires) is of course important for the physical realisation of the circuit, but at the logical design level we want to abstract away from geometric detail. Specialised place-and-route tools make sure that physical realisation of logical designs does not violate the abstractions we use.

The wonderful thing about diagrams-up-to-topological-isomorphism is that they can be usually described very precisely in the mathematical language of monoidal categories. This gives us a good language, and a good set of equations to work with. Unsurprisingly, the categorical specification language for circuit diagrams looks a lot like Sheeran’s Haskell-based specifications — this similarity has a name, the Curry-Howard-Lambek correspondence. The extra thing that we get though is the equations — all the equations that we need in order to start reasoning syntactically about circuits!

In a paper, jointly authored with my colleague Achim Jung, about t0 be published in the conference Formal Methods in Computer-Aided Design we pursue this observation and produce a categorical semantics of digital circuits. The main idea of the paper is that digital circuits can be shown to belong to a class of monoidal categories called control categories, which are (informally speaking) diagrams equipped with an unfoldable iterator. The rule of the iterator unfolding can be expressed diagrammatically as:

So whenever we have a circuit with feedback we can replicate the circuit, connect the two in a certain way, and get an equivalent circuit. This unfolding of the iterated circuit is the diagrammatic equivalent of the unfolding of a fixpoint combinator: Yf = f(Yf). This equation provides the essential means of syntactic reasoning about feedback.

Note that we prove that circuits satisfy this equation, we don’t simply require it axiomatically. The proof relies on smaller, more obvious, axioms which circuits must satisfy, such as the interaction between constant circuits denoting fixed logical levels and structural circuit components such as splitting and joining wires.

How is this syntactic approach helpful? We were mainly motivated by the filling this gap in syntactic reasoning about circuits, but it turns out interesting applications do exist. One such application are the so-called combinational circuits with feedback, where feedback loops are in some sense fake, i.e. they don’t create conventional feedback effects (latching, oscillation, etc.). Conventionally, digital design tools ban such circuits even though they can be very useful. This is an example of a circuit implementing, informally speaking, a circuit which behaves like if c then F(G(x)) else G(F(x)) efficiently, while using only one instance each of circuits and G:

The main example in our paper is to show how we can easily reason about such circuits without descending into complicated simulations.

The full paper is available from this link [PDF].

About Dan Ghica

Reader in Semantics of Programming Languages // University of Birmingham // https://twitter.com/danghica // https://www.facebook.com/dan.ghica
This entry was posted in Geometry of Synthesis. Bookmark the permalink.

One Response to Categorical semantics of digital circuits

  1. Dan Ghica says:

    Someone on Reddit pointed out the Mary Sheeran wrote a paper on “Categories for the Working Hardware Designer” which I haven’t referenced (even though I reference Mary’s work in general). Fortunately there is almost no overlap between that paper and this work.

Leave a Reply to Dan Ghica Cancel reply

Your email address will not be published. Required fields are marked *

*

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>