A compiler that emits a proof alongside the circuit

Datacenter.Dev Supercompiler is a compile to silicon pipeline for spatial dataflow architectures. It places computation onto a routing fabric and produces a machine checkable argument that the placement preserves the semantics of the reference.

Lowering

Specifications to Compute Fabric

One specification, lowered through four levels to the chipAn inverted pyramid, apex down, cut into four layers. The LOGOS source is the wide base at the top. Below it the interpreter, then the register virtual machine, each layer narrower by exactly the ratio its height is lower, because every cross-section of a pyramid is similar to the base. The dataflow tiles are the tip, and from the tip a beam lands on a chip drawn as an eight by eight grid of tiles, the spatial compute fabric. Each transition between layers carries a discharged proof obligation that semantics are preserved.01020304

  1. Source

    LOGOS, the executable specification

    Proof obligation dischargedsemantics preserved

  2. Interpreter

    Reference semantics, software

    Proof obligation dischargedsemantics preserved

  3. Register VM

    Sequential execution model

    Proof obligation dischargedsemantics preserved

  4. Dataflow tiles

    Spatial placement, physical fabric

    The tip lands on the chip.

ProvenZero counterexamples

Every lowering discharges its proof obligation in our proof kernel, and the 8x8 run of the int8 matmul primitive matches an independent reference oracle, checksum 510,720. The kernel behind that proof finishes families Z3 and Kissat do not.

The specification is lowered through four levels, from the LOGOS source to the dataflow tiles, and the tip of that lowering lands on the spatial compute fabric. Each lowering carries a discharged proof obligation that semantics are preserved, which is what makes the bottom level something to rely on rather than something to test.

The same proof, at both ends of the pipeline

The toolchain addresses one problem that appears twice. Lowering a model onto a fabric and lowering RTL onto a mask set are both compilation, and both already use formal methods where a tool exists for the step. Logic equivalence checking proves a netlist implements the RTL it came from, over every input. What neither end has is a tool that proves the lowered form agrees with the description it came from, and that step is closed by testing.

Model bring-up

Silicon you have bought

Weeks to months before a new fleet carries production traffic, most of it verification.

The full bring-up case

Design signoff

Silicon you are designing

The most expensive phase of a tapeout, bounded by what simulation can establish.

The full signoff case

Placement instead of sequencing

A conventional core fetches, decodes, and sequences. The compiler places computation onto routing tiles instead, so the datapath settles rather than stepping through instructions. The consequence is that correctness becomes a property of the placement, which is something a compiler can be made to prove.

One frontend, every backend

A program is written once and lowered many times. English meets one parser, the parser produces an imperative tree and a logical tree, and below the assert bridge the program continues as a single register bytecode. Every instruction target hangs off that one description of the program, which is what makes a new target something the toolchain gains rather than something the compiler gets rebuilt around.

Each target earns its place the same way. The virtual machine runs the program as the reference, the backend runs the same program, and the two are compared byte for byte. Where an operation has no lowering, the backend refuses to emit rather than emitting something close, and the list of refusals only shrinks, so coverage cannot regress quietly.

The frontend is the part that stays singular. LOGOS is the one surface language, and a Lean 4 frontend is specified and measured against a 248 case conformance corpus.

One program, one bytecode, and the targets it lowers toEnglish source enters one parser, which produces an imperative tree and a logical tree joined by the assert bridge. Below the bridge the program continues as one register bytecode. C, RISC-V, WebAssembly, CUDA and Tenstorrent each lower from that bytecode. Rust source lowers from the tree instead, drawn beside the bytecode. A spatial dataflow IR leaves the same bytecode and lowers onto a reconfigurable fabric and into synthesizable Verilog.English sourceOne parserImperative ASTStmt, ExprLogical ASTLogicExprAssert bridgeRustsourceRegister bytecodeCsourceRISC-VassemblyWebAssemblybinaryCUDAsourceTenstorrentbundleSpatial dataflow IRReconfigurablefabricSynthesizableVerilog

  1. From the tree

    Rust source, the reference path, handed to cargo rather than lowered through the bytecode.

  2. From the bytecode

    C, RISC-V, WebAssembly, CUDA and the Tenstorrent target all lower from the one register bytecode.

  3. From the spatial IR

    Stages, bounded buffers and typed handshakes placed on a described mesh, for a fabric or for Verilog.

  4. Every lane runs the same program, and the table below says where each target stands.

One parser produces two trees, the assert bridge joins them, and the program continues as a single register bytecode. C, RISC-V, WebAssembly, CUDA and Tenstorrent lower from that bytecode, Rust source lowers from the tree beside it, and a separate spatial dataflow IR lowers onto a reconfigurable fabric and into synthesizable Verilog.
Compiler targets, what each one emits, and where each one stands
TargetWhere it stands
RustRust source, handed to cargoThe reference path, lowered from the tree rather than from the bytecode.
CC source with a self contained runtimeA scoped subset that doubles as the oracle the GPU and Tensix paths are checked against.
RISC-VRV64GC assembly, assembled by riscv gcc115 operations lower with an empty gap list, and the programs run under qemu.
WebAssemblyA finished wasm binary from our own encoderNo rustc and no wasm-bindgen anywhere in the path.
CUDACUDA source and a host launcherThe most developed target after Rust, with tensor core lowering measured on A100 and H100.
TenstorrentA TT-Metalium host and kernel bundleBuilds today; host and kernel bundle emitted, validated in simulation.
Reconfigurable fabricPlacement onto a described meshPlaces onto a described mesh, validated in simulation.
VerilogSynthesizable modulesChecked against the running virtual machine under iverilog and by our own certified SAT, on one Sky130 signoff clean layout.

Two of those targets never fetch an instruction at all. A separate spatial dataflow IR carries the program as stages, bounded buffers and typed handshakes placed on a described mesh, and lowers from there onto a fabric or into synthesizable Verilog. A choreography certificate travels with that lowering, because a datapath that settles has to be argued for differently than a sequence of instructions.

RISC-V lowers 115 operations with an empty gap list. The Verilog path is checked bit for bit against the running virtual machine under iverilog and by our own certified SAT. Tenstorrent emits a TT-Metalium host and kernel bundle, and the fabric target places onto a described mesh, both validated in simulation.

Validated on physical hardware

Executed on a physical substrate: a Nexys A7-100T, Artix-7, flashed over JTAG. Manufacturing signoff comes back with zero DRC, LVS, antenna and routing violations under Sky130 signoff parameters, and 15,725+ regression tests re-run the obligation inside existing build pipelines.

The front end

The pipeline starts at English, which is where a hardware specification starts. The parser produces first order logic rather than a guess at intent, and the lowering that follows is the same one the rest of the toolchain runs on.

Two examples, both real output from the LOGOS compiler:

  1. Specification, in LOGOS

    SystemVerilog assertion

    Bounded response

    assert property (@(posedge clk) low_spi_cs_ |-> ##[0:1] valid_spi_miso_);

  2. Specification, in LOGOS

    SystemVerilog assertion

    Conjunction in the antecedent

    assert property (@(posedge clk) (low_dco_enable_ && high_cpu_en_) |-> Assert_dco_wkup_);

Emitted at a posedge clk clock. The full hardware corpus and the synthesizer that produced these are in the repository. Every pair here can be regenerated in your browser: press Compile and the compiler produces the assertion again, locally. Edit the sentence to compile something the corpus does not contain.

The language, pointed at hardware

How is any of that actually established?

The method