Rohit's Blog

Following “Lava: Hardware Design in Haskell” by Bjesse, Claessen, Sheeran and Singh (ICFP 1998). Parts 1 and 2 built a capability hierarchy and a combinator vocabulary, and ran circuits under the identity monad.

This is the post the design was for. We’re going to run the same half adder we wrote in part 1 — no changes, no annotations — and get out a logical formula that a solver can prove things about.

🔗Run a circuit on variables

The idea is one sentence: evaluate the circuit symbolically by feeding it abstract variables instead of concrete values. What comes back isn’t an answer; it’s a description of how the answer would be computed. That description is what you hand to external tools.

For that, a bit has to be able to be either a value or a variable:

type Var = String

enum BitExpr:
  case Lit(b: Boolean)
  case Ref(v: Var)

Note what part 1 bought us here. In the paper, Bit is a single datatype carrying both concrete and symbolic constructors, and the constructors must be kept abstract so the simulator can’t be handed a variable it cannot evaluate. With type Bit as a member, Std’s bit is Boolean and Sym’s bit is BitExpr, and the simulator has no case to get wrong.

Now, the monad. Each time a gate is applied to symbolic inputs we mint a fresh variable and record how it relates to its inputs. So we need somewhere to keep a counter and an accumulated list of assertions — a state monad, which is what the paper uses (state over fresh names, writer over assertions):

enum Gate:
  case And(a: BitExpr, b: BitExpr)
  case Or (a: BitExpr, b: BitExpr)
  case Xor(a: BitExpr, b: BitExpr)
  case Inv(a: BitExpr)

final case class Assertion(name: Var, gate: Gate)
final case class Netlist(next: Int, assertions: Vector[Assertion])

type SymM[A] = State[Netlist, A]

And the interpretation itself. Every gate does the same three things: allocate a name, record the assertion, return a reference.

object Sym extends Symbolic[SymM]:
  type Bit = BitExpr

  def low  = BitExpr.Lit(false)
  def high = BitExpr.Lit(true)

  private def emit(g: Gate): SymM[BitExpr] = State { n =>
    val v = s"b${n.next}"
    (Netlist(n.next + 1, n.assertions :+ Assertion(v, g)), BitExpr.Ref(v))
  }

  def and2(a: BitExpr, b: BitExpr) = emit(Gate.And(a, b))
  def or2 (a: BitExpr, b: BitExpr) = emit(Gate.Or(a, b))
  def xor2(a: BitExpr, b: BitExpr) = emit(Gate.Xor(a, b))
  def inv (a: BitExpr)             = emit(Gate.Inv(a))

  def newBitVar: SymM[BitExpr] = State { n =>
    val v = s"b${n.next}"
    (Netlist(n.next + 1, n.assertions), BitExpr.Ref(v))
  }

  // Monad[SymM] delegated to cats' State monad
  export cats.data.State.catsDataMonadForState[Netlist].{pure, flatMap, tailRecM}

Run the half adder from part 1 on two fresh variables and you get two assertions: one naming the AND of the inputs, one naming the XOR of them. Inputs b1 and b2, outputs b3 and b4. That’s a netlist, and it’s the whole circuit.

The half adder source never changed.

Here’s the thing I did not expect, and it closes a loop from an earlier series.

That series ended on an open problem. In Composing Contracts, an American option is built from a sub-contract used twice:

val opt = Anytime(perhaps(t2, u))
Get(Truncate(t1, opt)) thereafter opt

opt is obviously one thing in the source and invisibly two things to the evaluator, which values it twice. The sharing is apparent to the reader and unavailable to the program.

Now look at what the monad does here. In Lava, applying a gate is an effect — it allocates a name and appends to the netlist. So:

for
  x <- c.and2(a, b)      // one AND gate, named x
  p <- c.or2(x, a)       // reuses x
  q <- c.or2(x, b)       // reuses x — still one AND gate
yield (p, q)

versus

for
  p <- c.and2(a, b).flatMap(c.or2(_, a))   // one AND gate
  q <- c.and2(a, b).flatMap(c.or2(_, b))   // a second AND gate
yield (p, q)

Binding with <- shares. Re-invoking duplicates. Both are visible in the source, and they mean different circuits — which is correct, because two AND gates and one AND gate are genuinely different hardware.

Contracts had this problem because contracts are pure values: val opt = ... and Anytime(...) written twice are indistinguishable to the evaluator. Making construction monadic makes naming observable, because a name is exactly what the monad allocates.

I’d stop short of calling that a solution to the general problem — it’s a design choice with a real cost, which is that every gate is a bind and your descriptions get for-comprehension noise throughout. The paper concedes exactly this when discussing O’Donnell’s Hydra, which has no monads: circuit descriptions there are more direct, and the authors say plainly that must be an advantage. It’s their use of monads that makes Lava extensible, and they took the trade knowingly.

And it’s worth knowing that Claessen went on to write the paper about the general case — Observable Sharing for Functional Circuit Description (1999) — which came directly out of this work. The problem I flagged as open two series ago is a problem this paper’s author spent the following year on.

🔗The netlist is already Tseitin-encoded

Second thing I didn’t expect.

To hand a Boolean formula to a SAT solver you need conjunctive normal form. Converting a formula to CNF naively is exponential, so everyone uses the Tseitin transformation: introduce a fresh variable for each subformula, and add clauses asserting that the variable is equivalent to its subformula. The result is linear in the size of the input and equisatisfiable.

Now re-read what emit does. It introduces a fresh variable per gate and records that the variable is defined by that gate.

That is the Tseitin transformation. Lava’s symbolic interpretation isn’t producing a formula that then needs encoding — it produces the encoded form directly, because naming every intermediate result is what both procedures do. Turning the netlist into DIMACS is then mechanical, three or four clauses per gate.

I don’t think the paper says this anywhere, and I suspect it was simply obvious to the authors. It’s a nice illustration of a general pattern: the structure a domain wants and the structure a solver wants sometimes coincide, and when they do you get the bridge for free.

🔗Asking a question

So how do you state a property? Lava’s answer is the elegant part: the property is itself a circuit.

You build a description containing both the circuits you care about and the claim relating them, and the claim is expressed with the same gates as everything else. The paper defines the type of a formula to be the same as the type of a bit, precisely so that the ordinary logical operators work on both.

To check that a full adder with its carry-in tied low behaves like a half adder:

def question[F[_]](using c: Symbolic[F]): F[c.Bit] =
  for
    a  <- c.newBitVar
    b  <- c.newBitVar
    o1 <- halfAdd(a, b)
    o2 <- fullAdd(c.low, a, b)
    eq <- equalPairs(o1, o2)
  yield eq

Two fresh variables feed both circuits; the result is a bit that is true exactly when the two agree. equalPairs is built from xor2 and inv and and2 like anything else — no separate property language, no separate proof syntax.

I like this more the longer I look at it. A specification language that is the implementation language means there’s nothing to keep in sync, and every combinator from part 2 is available for writing properties.

🔗Handing it to a solver

The paper connects to a propositional tautology checker and to the first-order provers Otter and Gandalf, generating a file containing variable definitions and the question separated by an implication arrow.

The 2026 equivalent is SMT-LIB and Z3, and the emitter is a fold over the netlist:

def toSmt(n: Netlist, goal: Var): String =
  val decls = freeVars(n).map(v => s"(declare-const $v Bool)")
  val defs  = n.assertions.map { case Assertion(v, g) =>
    s"(define-fun $v () Bool ${gateToSmt(g)})"
  }
  // assert the negation: unsat means the goal always holds
  (decls ++ defs :+ s"(assert (not $goal))" :+ "(check-sat)").mkString("\n")

def gateToSmt(g: Gate): String = g match
  case Gate.And(a, b) => s"(and ${ref(a)} ${ref(b)})"
  case Gate.Or (a, b) => s"(or ${ref(a)} ${ref(b)})"
  case Gate.Xor(a, b) => s"(xor ${ref(a)} ${ref(b)})"
  case Gate.Inv(a)    => s"(not ${ref(a)})"

Assert the negation of the goal and ask for satisfiability. unsat means no counterexample exists, so the circuits are equivalent. sat means the solver found inputs where they differ, and it will hand you those inputs — which the paper models as a proof result that carries a countermodel when one exists.

I’ve written this emitter but not run it — there’s no JVM on the machine I drafted this on, so I can’t honestly report a unsat I haven’t seen. The shape is standard SMT-LIB and the netlist is already in definitional form, so I expect it to work with little fuss; when I’ve run it I’ll say so here rather than leave you to find out.

🔗VHDL is the same netlist, printed differently

The payoff of having got this far. The paper’s VHDL interpretation produces structural VHDL for the half adder — an entity with the inputs and outputs as ports, and an architecture with one component instance per gate, wired by name.

Look at what that needs: a list of gates, each with a name and its inputs. Which is the netlist. Verification and VHDL generation are the same interpretation with different printers:

def toVhdl(name: String, n: Netlist, ins: List[Var], outs: List[Var]): String
def toSmt (n: Netlist, goal: Var): String
def toDimacs(n: Netlist, goal: Var): String

Part 1 said four interpretations turned out to be two monads and three back-ends, and this is why. “Produce a description of the circuit” is one capability; everything downstream is printing. Adding a fourth output format — EDIF, Verilog, a JSON netlist for a viewer — is a new function over Netlist and nothing else. The paper makes exactly this point about being able to add interpretations with little disturbance to the existing system.

🔗Where we are

One description; simulation under Id; symbolic evaluation under State; and from the symbolic netlist, a formula for a solver and structural VHDL for a fab.

What we haven’t done is anything that would impress a hardware engineer. A half adder is four gates. The paper’s own demonstration is considerably more serious: two Fast Fourier Transform algorithms — different butterfly networks, different twiddle-factor placement, extra multiplication stages in one and not the other, circuits that look nothing alike — proved equivalent automatically.

That needs one thing we don’t have yet, and it’s not more gates. It’s an algebra: the equivalence isn’t provable by Boolean reasoning alone, because it depends on laws about complex roots of unity.

Next: Part 4 — Two FFTs, proved equivalent.

🔗Sources

Bjesse, Per, Koen Claessen, Mary Sheeran & Satnam Singh. Lava: Hardware Design in Haskell. ICFP 1998. Symbolic evaluation with fresh variables, the state-plus-writer monad, the assertion list, the trick of expressing a property as a circuit whose formula type is the bit type, the proof-result type carrying a countermodel, and the VHDL interpretation are all theirs.
Claessen, Koen & David Sands. Observable Sharing for Functional Circuit Description. ASIAN 1999 — the follow-up on the sharing problem, out of this work.
Tseitin, G. S. On the complexity of derivation in propositional calculus. 1968 — the encoding the netlist turns out to be in.
O’Donnell, John. Hydra — the monad-free design whose directness the paper concedes.

The Scala 3 translation, the SMT-LIB emitter, the observation that binding-versus-reinvoking makes sharing explicit, and the identification of the netlist as Tseitin form are mine.