Circuit Transformer: A Transformer That Preserves Logical Equivalence

TL;DR

The paper introduces the Circuit Transformer, a neural model that generates logic circuits strictly equivalent to Boolean functions, ensuring correctness and outperforming existing methods in producing compact, accurate circuits.

Contribution

A novel generative neural model with a decoding mechanism that guarantees logical equivalence, advancing neural approaches in circuit synthesis.

Findings

Outperforms existing neural methods on benchmarks

Generates more compact and accurate circuits

Strictly preserves logical equivalence during generation

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.