# Types as Interpreters for HDLs to Graphs.

As part of my PhD I was interested in: Types as (Abstract) Interpreters. This approach embeds an interpretation of your model directly in the type of your terms. A previous post details it.

As port of my current work I have been investigating the construction of Hardware Description Languages (HDLs) and reasoning about their structure using denotational semantics. Currently my soundness checks are extrinsic to the intrinsically typed term language I have developed. It only recently occured to me that we can make these soundness checks intrinsic using the Types as (Abstract) Interpreters approach.

In this post I will describe how we can model a simple core HDL for netlist (derived from Verilog’s own syntax and interesting design decisions) and embed a denotation to a multigraph directly in the model’s types. I will also outline more problems that need addressing for this model to be of use. Of note I have solved these problems but cannot seem to get past the reviewers with the solutions :-(

First we will need some helpers:

import Decidable.Equality
import Data.Fin
import Data.List.Elem


## A Simple Graph

Digital circuits are graphs. To help with the abstract interpretation we need to have a graph to construct.

The details of how the graph is construct is not required per se to understand the interpretation. We leave their details for the reader, and note that when adding edges to the graph we ensure that the vertices in the edge are also inserted. What is important is the kind of graph we require: A Multigraph. Multigraphs are graphs in which we have a set of vertices, and a list of edges. We can represent such graphs as:

record Graph where
constructor G
vertices : List Nat
edges    : List (Pair Nat Nat)


Note Although we require a set of vertices reasoning about existential quantification (isElem) of the SortedSet datatype in Idris has not been contributed, and working with Lists is sufficient for our needs. Provided we ensure the List is a setdate: 2022-05-25-Type-Interpreter-HDLs.md —.

We provide the following API for working with graphs.

addVertex : Nat -> Graph -> Graph

fromEdges : List (Nat, Nat) -> Graph

addEdge : (Nat, Nat) -> Graph -> Graph

merge : Graph -> Graph -> Graph


## Types

We now provide the types for our little HDL.

First we give the datatypes that determine the shape of channels and ports. Here the datatypes are just the synthesised subset:

namespace DataType
public export
data DataType = LOGIC | VECT Nat DataType


Next we give the types of our terms.

namespace Ty


For ports we also need to denote the expected signal flow which, for simplicity, is uni-directional.

  namespace Property
public export
data Direction = IN | OUT


The types for terms capture:

  public export
data Ty : Type where


Ports in which ports have a shape and a direction.

    Port : (shape : DataType)
-> (dir   : Direction)
-> Ty


Channels are internal wires, and are simply shaped.

    Chan : (shape : DataType)
-> Ty


Gates are primitive wiring constructs.

    Gate : Ty


Unit helps us ensure that we know when the end of the specification has been reached.

    Unit : Ty


## Typing Contexts

namespace Context


We will be using an intrinsically typed representation. As we will be capturing, at the type-level, the denotation of terms we need to construct a typing context that keeps track of the denotations as well as the types.

First we give the denotation of our types to types in our graph construct.

  public export
Interp : Ty -> Type


Ports map to vertex identifiers.

  Interp (Port d y)
= Nat


Channels to an edge between two vertices.

  Interp (Chan s)
= (Nat, Nat)


Gates are a sub-graph.

  Interp Gate
= Graph


Unit is Unit.

  Interp Unit
= Unit


With this interpretation we can now specify items in our typing context:

  public export
record Item where
constructor I


Items capture the type of a term coupled with the interpretation of the term in terms of a graph.

    type   : Ty
denote : Interp type


Here we have effectively merged the typing and interpretation environments together!

## Terms

namespace Term


Now with the types and graph constructs define we can now describe how to embed the interpretation of the HDL into its definition. This is going to be a hairy definition but it is worth it.

First we detail the data structure that represents terms in our HDL. The type for term takes as ‘input’, really ‘is parameterised by’, a counter and a starting graph. The counter supports unique tagging of vertices, and the starting graph captures the state of the interpretation so far.

  public export
data Term : (c_in   : Nat) -> (g_in   : Graph)


We then provide the judgement form for terms. Terms have a typing context and a type. We also provide the interpretation of the term.

           -> (ctxt   : List Item)
-> (type   : Ty)
-> (denote : Interp type)


We then finish the definition with the ‘result’ of the interpretation. That is the current state of the accumulator and graph.

           -> (c_out  : Nat)
-> (g_out  : Graph)
-> Type
where


More formally we might describe this as:

(c : Nat, g : Graph)[| G |- t : type |] ::= (c' : Nat, g' : Graph, v : [| type |])


Alternatively we might present the interpretation environment explicitly:

(c : Nat, e : E, g : Graph)[| G |- t : type |] ::= (c' : Nat, g' : Graph, v : [| type |])


With this definition we can now intertwin the definition of our HDLs syntax with its denotation.

### Stop

When we have finished the specification we have also finished the interpretation. We simply return the current state of the accumulators.

      Stop : Term c_in g_in ctxt Unit () c_in g_in


### Variables

We use De Bruijn indices (proof that an item is in the context) to capture bindings. Merging the typing context and interpretation environment makes it easier to extra the type and denotation of bound terms.

      Var : Elem (I ty de) ctxt
-> Term c_in g_in ctxt ty de c_in g_in


### Port introductions

To ensure normal forms we have embedded sequencing of terms within the language’s structure, and require that the final expression has type Unit. Only the Stop term introduces the Unit type.

Thus when introducing ports to the design we model it as a let-binding. Introducing ports simply extends the typing context with a new bound port. Ports interpret to just a vertex. Here we must ensure that when diving into the scope (the body of the let-binding) the input accumulator is correctly updated: counter incremented by one; and the vertex embedded in the graph.

      Port : (dtype  : DataType)
-> (dir   : Direction)
-> (scope : Term (S c_in)
(I (Port dtype dir) (S c_in) :: ctxt)
Unit
()
c_out
g_out)
-> Term c_in  g_in  ctxt Unit ()
c_out g_out


### Wires

Wires are similarly formed/typed/interpreted as ports. Instead of ports the wire introduction introduces a channel. Interpretation of wires maps channels to a subgraph that is a directed edge between two vertices that represent the input and output ports of the channel.

      Wire : (dtype : DataType)
-> (scope : Term (S (S c_in))
(merge (fromEdges [(S c_in, S (S c_in))])
g_in)
(I (Chan dtype) (S c_in, S (S c_in)) :: ctxt)
Unit
()
c_out
g_out)
-> Term c_in  g_in  ctxt Unit ()
c_out g_out


### Gates

We now turn our attention to gates. For simplicity we have considered binary gates only. The following description naturally extends to n-ary gates, but is somewhat more hairydate: 2022-05-25-Type-Interpreter-HDLs.md —.

## For our HDL binary gates take two inputs and return a single output. Interpretation of gates are to a sub-graph in which the gate is a single node with two incoming edges and a single outgoing edgedate: 2022-05-25-Type-Interpreter-HDLs.md

      Gate : (outport : Term c_in  g_in ctxt (Port LOGIC OUT) vo
c_a   g_a)
-> (inportA : Term c_a   g_a  ctxt (Port LOGIC IN)  va
c_b   g_b)
-> (inportB : Term c_b   g_b  ctxt (Port LOGIC IN)  vb
c_out g_out)
-> Term c_in  g_in ctxt Gate (fromEdges [(va, S c_out), (vb,S c_out), (S c_out, vo)])
(S c_out) g_out


### Gate Instantiation

To include gates into our design (i.e. wire them in) they need to be instantiated. The GDecl term suppots this. Its design follows that of the introduction of ports and wires.

      GDecl : (gate : Term c_in  g_in  ctxt Gate g
c_mid g_mid)
-> (scope : Term c_mid (merge g_mid g) (I Gate g :: ctxt) Unit ()
c_out g_out)
-> Term c_in g_in ctxt Unit ()
c_out g_out


### Indexing

It is permissible to index vectors on ports. This will return a single port that is in the same direction. The interpretation just returns the vertex representing the original port.

      Index : (port : Term c_in g_in ctxt (Port (VECT size type) dir) v c_out g_out)
-> (idx  : Fin size)
-> Term c_in g_in ctxt (Port            type  dir) v c_out g_out


### Projection

We need to be able to access the endpoints of channels. We do so by projection. For simplicity we have split the terms in twain, but note they can be merged into a single term. Project, in both the term language and interpretation, returns the endpoint of the channel. During interpretation this is the corresponding vertex at the end of the edge.

The direction of projection is counter-intuitive, but is nonetheless intuitive for interpretation. If we are accessing the ‘reading’ end of the channel it needs to connect to the inputting port of the primitive term it is being plugged into. The ‘writing’ end needs to go to the outputting end.

      ProjR : (chan : Term c_in g_in ctxt (Chan type)     (s,t) c_out g_out)
-> Term c_in g_in ctxt (Port type IN)     t  c_out g_out

ProjW : (chan : Term c_in g_in ctxt (Chan type)     (s,t) c_out g_out)
-> Term c_in g_in ctxt (Port type OUT)  s    c_out g_out


With this we have finished the description of the language and its interpretation to a graph.

## Example

We end this tour with simple examples and interactions.

### Example 1

#### Definitions

example : (c : Nat **
g : Graph ** Term Z (G Nil Nil) Nil Unit ()
c g)
example
= (_ ** _ **
Port LOGIC OUT
$Port LOGIC IN$ Port LOGIC IN
$GDecl (Gate (Var (There (There Here))) (Var (There Here)) (Var Here))$ Stop)


#### Interactions

Main> fst (snd example)
G [1, 3, 4, 2]
[(4, 1), (3, 4), (2, 4)]
Main> snd (snd example)
Port LOGIC OUT
(Port LOGIC IN
(Port LOGIC IN
(GDecl (Gate (Var (There (There Here)))
(Var (There Here))
(Var Here))
Stop)))
Main> :t snd (snd example)
snd (snd example) : Term 0 (G [] []) [] Unit ()
4 (G [1, 3, 4, 2]
[(4, 1), (3, 4), (2, 4)])


### Example 2

#### Definitions

example2 : (c : Nat ** g : Graph ** Term Z (G Nil Nil) Nil Unit ()
c g)
example2
= (_ ** _ **
Port LOGIC OUT
$Port LOGIC IN$ Wire LOGIC
$GDecl (Gate (ProjW (Var Here)) (Var (There Here)) (Var (There Here)))$ GDecl (Gate (Var        (There (There (There Here))))
(ProjR (Var               (There Here)))
(ProjR (Var               (There Here))))
\$ Stop)


#### Interactions

Main> fst (snd example2)
G [2, 5, 3, 1, 6, 4]
[(2, 5), (2, 5), (5, 3), (3, 4), (6, 1), (4, 6), (4, 6)]
Main> snd (snd example2)
Port LOGIC OUT
(Port LOGIC IN
(Wire LOGIC
(GDecl (Gate (ProjW (Var Here))
(Var (There Here))
(Var (There Here)))
(GDecl (Gate (Var (There (There (There Here))))
(ProjR (Var (There Here)))
(ProjR (Var (There Here))))
Stop))))
Main> :t snd (snd example2)
snd (snd example2) : Term 0 (G [] []) [] Unit ()
6 (G [2, 5, 3, 1, 6, 4]
[(2, 5),
(2, 5),
(5, 3),
(3, 4),
(6, 1),
(4, 6),
(4, 6)])


## Problems

This is a very simple illustrative example, that does not do everything we need it to do.

1. We have not taken into account bi-directional ports. There are tricks we need to do to ensure that we can plug-in bi-directional ports into gates.

I will explain these tricks in another post.

2. We have not taken into account the correctness of the resulting graph. This will require extending the definition of Stop with a correctness predicate over the graph.

I will explain the approach I take in another post.

3. Going from raw SystemVerilog terms to this core representation. If not dealing with bi-directional ports, this elaboration is not complicated. For bi-directional ports we are going to need some clever elaboration to ensure the correct plugging of wires.

I will explain the approach I take in another post.

4. We have not reasoned about the usage of ports in this setting. Our language provides unrestriced wiring which can lead to accidental fan-outs, or even worse accidental fan-ins.

Even if we provide a multiplexer primitive, we need something special in the type-system to ensure wire usage is linear.

I will explain the approach I take in another post/paper.

## Coda

This post should have demonstrated how dependent types helps us to write more precise software where extrinsic checks (in this case abstract interpretation) can be embedded directly into the ’types’ of our terms. With this approach we can design new HDLs in which the wiring structure is not only correct at compile time but that our approach is provable sound. Before my soundness checks were extrinsic, here they are intrinsic.

What will be interesting will be to write the elaborator/type-checker and see if we can erase the checks for runtime…