Tag: logic

Bitcoin miners are liquidating their holdings to pivot into AI hosting. The machines that wasted electricity producing imaginary money will now waste it producing imaginary intelligence. Anthropic has secured 3.5 gigawatts of compute — the consumption of three and a half million households — to serve language models.

GCC compiles the entire Linux kernel in fifteen minutes on a single machine drawing 200 watts. Fifty watt-hours. A light bulb left on for an afternoon. It manages this because it is not guessing. It has a grammar, a type system, and an optimisation pipeline where every transformation preserves semantics. There is no temperature parameter. There is no “try again and hope.”

A compiler’s cost is \(O(n \log n)\) in the size of the input. A language model’s cost is \(O(n \cdot d)\) where \(d\) is the dimensionality of a model that cannot tell you whether the answer is correct. When the task has a formal specification, you do not need gigawatts. You need a parser.

I have been writing parsers for twenty years. Today I started improving the one that matters most: the circuit description language at the heart of llogic, qbf-designer, and the formal methods toolchain I am building at Llama Logic.

My first encounter with a compiler was at Zend Technologies in Ramat Gan in 2000. I was twenty-two, fresh off the plane from Bulgaria, and I did not know what a parser was. Zend built the PHP language engine. I watched a small team turn a grammar into a working language that ran half the web. I did not understand how.

A few years later, at Delft, I read the Dragon Book and took the compiler construction course of Koen Langendoen. We became friends over my many years at the university. That course turned out to be one of the most useful things I have ever learned. It is the skill that lets me write software that works — not approximately, not statistically, not when the vibes are right, but deterministically, on all inputs, by construction.

It is also how I got into diagnosis. At the end of my master’s I went to Koen and asked for a Ph.D. position in compiler construction. He told me “compilers are passé” — but I could go work with Arjan J.C. van Gemund doing diagnostics. Arjan has since retired north to compose music, which is a better use of a fine mind than supervising Ph.D. students, though he was good at both. They needed a compiler for LyDiA, the diagnostic modelling language. So I built one. Then I built many more. Every research system I have worked on since — LyDiA, the DXC framework at NASA Ames, the synthesis tools at PARC, and now llogic — has a parser at its core. The compiler is never the point. The compiler is always the point.

A domain-specific language is a small language built for one job. SQL is a DSL for databases. Regular expressions are a DSL for pattern matching. Makefiles are a DSL for build dependencies. You do not write an operating system in SQL. You do not query a database with a Makefile. The language fits the problem, and because it fits, it can enforce constraints that a general-purpose language cannot.

This is the point that the vibe-coding movement misses entirely. A grammar is not a convenience. It is a contract. When I write a parser for a circuit description language, the grammar specifies exactly what constitutes a valid circuit. If you misspell a gate type, the parser rejects your input. If you connect an output to a nonexistent signal, the parser tells you. If you instantiate a module that does not exist, you get an error message with a line number — not a plausible-looking circuit that silently computes the wrong function.

This is what determinism means in practice. The parser either accepts or rejects. There is no 95% confidence. There is no temperature. The same input produces the same result every time, on every machine, for every user. A QBF solver receiving a malformed netlist will produce garbage. A diagnosis engine receiving an inconsistent model will compute meaningless results. The parser is the gate that keeps garbage out. It costs milliwatts. It works.

There is a second reason, less often discussed. Humans need to read these things. An engineer debugging a faulty adder needs to look at the circuit description and understand it. A reviewer verifying a synthesis result needs to confirm that the specification matches the intent. This is not a machine-to-machine format. It is a language — with the same design obligations as any language: clarity, consistency, and the ability to say exactly what you mean and nothing else.

The circuit DSL in llogic had outgrown its grammar. The new format adds modules, arrays, imports, and arbitrary nesting. A full adder, from primitives to a 4-bit module with array slicing:

# 4-bit ripple carry adder

import "std_logic.circ"

module half_adder(input a, b; output s, c):
    x: s = xor(a, b)
    a: c = and(a, b)
end

module full_adder(input a, b, ci; output s, co):
    wire f, p, q

    inst half_adder ha1(a=a, b=b, s=f, c=p)
    inst half_adder ha2(a=ci, b=f, s=s, c=q)
    o: co = or(p, q)
end

module adder2(input a[2], b[2], ci; output s[2], co):
    wire c0

    inst full_adder bit0(a=a[0], b=b[0], ci=ci, s=s[0], co=c0)
    inst full_adder bit1(a=a[1], b=b[1], ci=c0, s=s[1], co=co)
end

module adder4(input a[4], b[4], ci; output s[4], co):
    wire cm

    inst adder2 lo(a=a[0:1], b=b[0:1], ci=ci, s=s[0:1], co=cm)
    inst adder2 hi(a=a[2:3], b=b[2:3], ci=cm, s=s[2:3], co=co)
end

Four levels of nesting. Modules, arrays, slices, named connections. The flattener — a recursive tree walk, the same algorithm I used in LyDiA for system descriptions — traverses the instantiation tree and emits the flat netlist the solver has always consumed. The hierarchy is for the engineer. The solver does not know it exists.

Sequential circuits work the same way. A 4-bit serial adder with synchronous reset:

# 4-bit serial adder with synchronous reset

module shift4(input d, rst; output q):
    wire d1, d2, d3

    f1: d1 = dff(d, rst)
    f2: d2 = dff(d1, rst)
    f3: d3 = dff(d2, rst)
    f4: q = dff(d3, rst)
end

module seq_adder4(input a, b, rst; output s, co):
    wire i1, i2, ci

    inst shift4 sa(d=a, rst=rst, q=i1)
    inst shift4 sb(d=b, rst=rst, q=i2)
    inst full_adder fa(a=i1, b=i2, ci=ci, s=s, co=co)
    c: ci = dff(co, rst)
end

A dff with one argument is a plain register. Two arguments: synchronous reset. This maps directly to the standard Verilog template always @(posedge clk) if (rst) q <= 0; else q <= d; — making translation between the two languages mechanical.

So why not just use Verilog?

Because Verilog is a simulation language that has been coerced into serving as a synthesis input. A synthesis tool reads an always block, pattern-matches the sensitivity list, and infers what is a register and what is combinational logic. The engineer writes behaviour and hopes the tool’s heuristics match their intent. In llogic, a dff is a dff. An and is an and. There is no inference. The circuit says what it is.

This matters for formal methods. Diagnosis requires knowing exactly what components exist. Synthesis requires a precise specification of the design space. Neither tolerates a language that hides structure behind inference rules. Verilog is the right language for RTL designers who want to describe behaviour and let tools figure out the structure. Llogic is the right language when the structure is the point.

The parser, AST, and flattener should take a few days. When they are done I will update the llogic repository on the feature/hierarchical-dsl branch.

Three and a half million households’ worth of electricity to serve a model that cannot tell whether it is thinking deeply or not. Fifty watt-hours to compile a kernel. Considerably less to parse a circuit. The tools that work have always been quiet, small, and correct. The software will continue to not hallucinate.

Ceterum censeo slopem esse delendam.

(Cato the Elder ended every speech in the Roman Senate with “Carthage must be destroyed” — regardless of the topic. This is that, but for AI slop.)

Repository: llogic