{"id":32,"date":"2026-04-06T17:31:08","date_gmt":"2026-04-06T17:31:08","guid":{"rendered":"https:\/\/llama.gs\/blog\/?p=32"},"modified":"2026-04-06T17:31:08","modified_gmt":"2026-04-06T17:31:08","slug":"diagnosing-circuits-into-existence","status":"publish","type":"post","link":"https:\/\/llama.gs\/blog\/index.php\/2026\/04\/06\/diagnosing-circuits-into-existence\/","title":{"rendered":"Diagnosing Circuits into Existence"},"content":{"rendered":"

Cadence recently unveiled ChipStack AI, which El Reg memorably described as “vibe coding for chips<\/a>.” The idea is that an LLM agent will design your next processor for you, provided you don’t mind the occasional hallucinated transistor. One Reg commenter recalled Jensen Huang’s declaration that nobody needs to learn programming anymore, and suggested he try designing his next GPU with it. Quite. Meanwhile, a water desalination company spent $200,000 on AI-generated engineering advice<\/a> that turned out to be \u2014 and I use the technical term \u2014 wrong. They then built a second AI to filter out the nonsense from the first one, which is the silicon valley equivalent of hiring a second drunk to drive the first one home. One does wonder what the industry will achieve once it sobers up. In the meantime, I have been doing something unfashionable: using mathematics to design circuits that are provably correct.<\/p>\n

Today I am releasing qbf-designer<\/a>, a tool for exact digital circuit synthesis from arbitrary component libraries via Quantified Boolean Formula solving. It is the top of a dependency stack that has also been modernised and released: llogic<\/a> for logic representation, transformation, and solving; lcfgen<\/a> for generating circuit primitives used both in the QBF encoding itself and as benchmark specifications; and a collection of solver bindings \u2014 pydepqbf<\/a>, pylgl<\/a>, pyllq<\/a>, and pycudd<\/a> \u2014 that connect the Python layer to the C\/C++ solvers doing the actual heavy lifting. The software works. It synthesises provably minimal circuits from specifications. It found a five-gate full-subtractor that improves on the seven-gate textbook design. It does not hallucinate.<\/p>\n

Now, explaining what “provably minimal circuit design” actually means turns out to require rather more than a single blog post \u2014 so this is the first in a series. The short version: given a functional specification (“I want a circuit that adds two numbers”) and a bag of components (“here are some AND, OR, and XOR gates”), find the smallest circuit that does the job. The practical application is technology mapping for FPGAs, where you need to cover a circuit with k-input Look-Up Tables using as few LUTs as possible. The silicon is already on the chip and you have already paid for it \u2014 every LUT you save is space freed for more logic, letting you fit a larger design onto the same device. Current industry tools \u2014 Vivado, Yosys \u2014 use heuristics for this. qbf-designer gives you the exact answer, at least for sub-circuits small enough to chew on. Early results are promising: on a 2-bit comparator mapped to 3-LUTs, the solver finds a 5-LUT implementation where heuristic methods produce 6. One does not need to be a venture capitalist to notice that 5 is fewer than 6.<\/p>\n

There is a fundamental difference between this work and the “AI for chip design” circus currently touring Silicon Valley. Circuit synthesis \u2014 the problem of finding a minimum-size circuit equivalent to a specification \u2014 sits at the second level of the polynomial hierarchy (\u03a3\u2082\u1d56-complete, for those keeping score). This is not a problem you can solve by autocompleting Verilog. It has a precise computational complexity classification, a formal proof of correctness, and a guarantee of optimality. In other words, it is science, the kind that involves theorems rather than pitch decks, and where “it works” means something more rigorous than “the demo didn’t crash during the investor meeting.”<\/p>\n

My interest in circuit synthesis comes from an unexpected direction: breaking things. I spent years working on Model-Based Diagnosis of digital circuits \u2014 the problem of figuring out which component in a circuit has failed, given observed misbehaviour. My colleague Johan de Kleer<\/a>, who has been thinking about this sort of thing since before most AI entrepreneurs were born, used to describe synthesis as “diagnosing a circuit into existence.” The idea is beautifully perverse: start with an empty circuit, treat the absence of every gate as a “fault,” and ask the diagnostic engine what collection of fixes would make the circuit behave like, say, a 32-bit ALU. It turns out that the mathematical machinery for diagnosis and synthesis is nearly identical \u2014 the same \u2203\u2200 quantifier structure, the same miter-based equivalence checking, the same PSPACE-hard satisfaction problems. The only difference is whether you are looking for what went wrong or what should be there in the first place.<\/p>\n

The theoretical foundations and experimental results have been written up and submitted to Constraints<\/a>, a journal that publishes work reviewed by people who can tell the difference between a proof and a press release. The paper covers the QBF encoding, the universal component cell, the configurable interconnection fabric, symmetry breaking, and extensive benchmarks on arithmetic circuits, 74XXX integrated circuits, and exact synthesis function sets. I mention this not to boast but to draw a gentle contrast with the prevailing approach to AI research in the Valley, where the peer review process consists of checking whether the blog post got enough likes on Twitter<\/del> X and the replication methodology is “we lost the weights.” Should the reviewers find fault with the work, they will at least be able to point to a specific equation rather than gesturing vaguely at a loss curve and muttering about emergence.<\/p>\n

In the next instalment, I will demonstrate qbf-designer doing FPGA technology mapping \u2014 taking a circuit, mapping it to k-input Look-Up Tables, and producing a result that uses fewer LUTs than Xilinx Vivado. Not by a little. Not by accident. By mathematics.<\/p>\n","protected":false},"excerpt":{"rendered":"

Cadence recently unveiled ChipStack AI, which El Reg memorably described as “vibe coding for chips.” The idea is that an LLM agent will design your next processor for you, provided you don’t mind the occasional hallucinated transistor. One Reg commenter recalled Jensen Huang’s declaration that nobody needs to learn programming anymore, and suggested he try […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[4,17],"tags":[28,31,26,14,9,29,27,30],"class_list":["post-32","post","type-post","status-publish","format-standard","hentry","category-computer-science-and-philosophy","category-projects","tag-applied-science","tag-combinatorics","tag-digital-circuits","tag-formal-methods","tag-fpga","tag-game-theory","tag-hardware-design","tag-optimization"],"_links":{"self":[{"href":"https:\/\/llama.gs\/blog\/index.php\/wp-json\/wp\/v2\/posts\/32","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/llama.gs\/blog\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/llama.gs\/blog\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/llama.gs\/blog\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/llama.gs\/blog\/index.php\/wp-json\/wp\/v2\/comments?post=32"}],"version-history":[{"count":1,"href":"https:\/\/llama.gs\/blog\/index.php\/wp-json\/wp\/v2\/posts\/32\/revisions"}],"predecessor-version":[{"id":33,"href":"https:\/\/llama.gs\/blog\/index.php\/wp-json\/wp\/v2\/posts\/32\/revisions\/33"}],"wp:attachment":[{"href":"https:\/\/llama.gs\/blog\/index.php\/wp-json\/wp\/v2\/media?parent=32"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/llama.gs\/blog\/index.php\/wp-json\/wp\/v2\/categories?post=32"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/llama.gs\/blog\/index.php\/wp-json\/wp\/v2\/tags?post=32"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}