Circuits That Mean What They Say

Abstract

A chip is designed in software, yet the software we design chips in cannot say what a design means. Register-transfer text is written, transformed by optimizers on trust, and only afterward checked by simulating a sample of inputs; the meaning of the circuit is never an object the tools hold. The alternatives are few and each concedes something: the open physical flow is mature but has no notion of a design's meaning, and the verified hardware languages establish meaning only by asking you to trust a source description and its compiler. This paper opens a different program—designing chips in mathematics, where the trusted artifact is the circuit's meaning and the description is a disposable rendering—and reports its first release. Two ideas carry it. First, unknown is a number: a hardware bit ranges over four values {0, 1, X, Z} ordered by information, and in this order two-valued synthesis provably refines four-valued simulation—it never resolves an unknown the silicon leaves undetermined, closing the classical simulation–synthesis gap as a theorem rather than a lint rule. Second, faithfulness is a fixed point: a clean, single-pass denotational semantics is proved equal to a genuinely order-independent, event-driven reference—the semantics a real simulator implements—exactly on the well-formed (topologically ordered) circuits, and proved to diverge off them; the boundary of agreement is itself a sharp object. On this foundation we build a four-valued production surface: clock-domain-crossing safety proved for every schedule rather than a sampled one, a small RISC-V core whose behavioral receipt is made load-bearing by a mutation test, optimization passes that compose as behavior-preserving translations, and the circuit's receipt carried through the open flow to a Sky130 layout. We are explicit about the distance still to travel to rival an industrial hardware description language—a full model of concurrent time, a maximal synthesizable subset, technology mapping inside the trusted boundary, scale—and we lay that distance out as a concrete map. This is a first iteration and an invitation: the mathematics of a chip's meaning is now real enough to build on, and the work of making it a competitor is work we want to share. Published by The Institute for Applied Ontological Mathematics.