Circuit Transformer: A Transformer That Preserves Logical Equivalence

TL;DR

The paper tackles the challenge of generating circuits that are strictly equivalent to a given Boolean function, addressing the risk of incorrect predictions by standard generative models. It introduces the Circuit Transformer, aTransformer-based model that uses a masking-based decoding process and a top-down sequential circuit representation to enforce equivalence throughout generation, aided by a three-valued logic to allow short-circuit evaluation. It also casts equivalence-preserving optimization as a Markov decision process and demonstrates an 88-million-parameter Circuit Transformer trained on Resyn2 signals to produce strictly equivalent yet more compact circuits, achieving zero equivalence violations on unseen data and often smaller results than ground truth. The work provides a practical pathway for exact, constraint-satisfying generation in hardware design and opens avenues for applying similar constrained-generation strategies to other domains requiring formal feasibility guarantees.

Abstract

Implementing Boolean functions with circuits consisting of logic gates is fundamental in digital computer design. However, the implemented circuit must be exactly equivalent, which hinders generative neural approaches on this task due to their occasionally wrong predictions. In this study, we introduce a generative neural model, the "Circuit Transformer", which eliminates such wrong predictions and produces logic circuits strictly equivalent to given Boolean functions. The main idea is a carefully designed decoding mechanism that builds a circuit step-by-step by generating tokens, which has beneficial "cutoff properties" that block a candidate token once it invalidate equivalence. In such a way, the proposed model works similar to typical LLMs while logical equivalence is strictly preserved. A Markov decision process formulation is also proposed for optimizing certain objectives of circuits. Experimentally, we trained an 88-million-parameter Circuit Transformer to generate equivalent yet more compact forms of input circuits, outperforming existing neural approaches on both synthetic and real world benchmarks, without any violation of equivalence constraints.

Figures (8)

• Figure 1: An example showing how a Boolean function can be implemented by circuits, i.e., cascade connections of logic gates. and are the AND gate and NOT gate respectively, and is the NAND gate, an AND gate followed by a NOT gate. The circuits shown in \ref{['fig:circuit_1']} and \ref{['fig:circuit_2']} are both valid implementations of $f$, while the latter is more compact in size. The circuit shown in \ref{['fig:circuit_3']} is invalid, even if the difference is as small as one bit.
• Figure 2: A valid solution of the eight-queen puzzle, sequentially encoded as "dbhegacf".
• Figure 3: An example showing how a strictly feasible circuit can be built with our proposed sequential representation with cutoff properties. $f(x_2, x_1, x_0)$ is a Boolean function with $f(0, 0, 1) = f(1, 1, 1) = 1$ and $f(x_2, x_1, x_0) = 0$ otherwise. $D = \{x_0, \overline{x_0}, x_1, \overline{x_1}, x_2, \overline{x_2}, \land, \overline{\land}\}$, $U$ denotes the wildcard node. The next wildcard node to be replaced is marked in red. $S_t = \{s \in D \mid F(s_1, \dots, s_{t-1}, s; f) \text{ holds}\}$. The selection of $s_t$ from $S_t$ is based on a masked probability distribution estimated via a trained Circuit Transformer, which will be elaborated in \ref{['sec:neural_encoding']}.
• Figure 4: Transition between a DAG and one or more trees.
• Figure 5: The training and the inference stage of the Circuit Transformer. In the inference stage, the positional encoding $e_t$ at step $t$ is computed on-the-fly based on the position of the current token $s_t$ in the partially defined circuit. The mask $S_{t+1}$ for predicting the next token $s_{t+1}$ is computed based on \ref{['eq:s_t']} given the previous tokens $s_1, \dots, s_t$ and the cutoff property $F(s_1, \dots, s_t ; f)$. "S" and "E" denote the [START] and [END] tokens in Transformer model.