Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Cirbo: A New Tool for Boolean Circuit Analysis and Synthesis

Daniil Averkov, Tatiana Belova, Gregory Emdin, Mikhail Goncharov, Viktoriia Krivogornitsyna, Alexander S. Kulikov, Fedor Kurmazov, Daniil Levtsov, Georgie Levtsov, Vsevolod Vaskin, Aleksey Vorobiev

TL;DR

Cirbo addresses the practical needs of circuit analysis, synthesis, and minimization by introducing an open-source Python tool that supports XAIG and AIG representations. It combines manual, SAT-based, and hybrid synthesis with both low- and high-effort minimization, and maintains a database of small, near-optimal circuits to accelerate design. Experimental results on IWLS 2024 benchmarks show substantial circuit-size reductions (average around $12\%$, up to $83\%$ on some cases) and contest-winning performance, underscoring the practical impact for symmetric and arithmetic functions. The work provides a modular framework, combining building-block approaches with SAT-based optimization, and demonstrates scalable improvements across SUM, MAJ, SORT, and arithmetic circuits, offering a valuable toolchain for circuit designers and researchers.

Abstract

We present an open-source tool for manipulating Boolean circuits. It implements efficient algorithms, both existing and novel, for a rich variety of frequently used circuit tasks such as satisfiability, synthesis, and minimization. We tested the tool on a wide range of practically relevant circuits (computing, in particular, symmetric and arithmetic functions) that have been optimized intensively by the community for the last three years. The tool helped us to win the IWLS 2024 Programming Contest. In 2023, it was Google DeepMind who took the first place in the competition. We were able to reduce the size of the best circuits from 2023 by 12\% on average, whereas for some individual circuits, our size reduction was as large as 83\%.

Cirbo: A New Tool for Boolean Circuit Analysis and Synthesis

TL;DR

Cirbo addresses the practical needs of circuit analysis, synthesis, and minimization by introducing an open-source Python tool that supports XAIG and AIG representations. It combines manual, SAT-based, and hybrid synthesis with both low- and high-effort minimization, and maintains a database of small, near-optimal circuits to accelerate design. Experimental results on IWLS 2024 benchmarks show substantial circuit-size reductions (average around , up to on some cases) and contest-winning performance, underscoring the practical impact for symmetric and arithmetic functions. The work provides a modular framework, combining building-block approaches with SAT-based optimization, and demonstrates scalable improvements across SUM, MAJ, SORT, and arithmetic circuits, offering a valuable toolchain for circuit designers and researchers.

Abstract

We present an open-source tool for manipulating Boolean circuits. It implements efficient algorithms, both existing and novel, for a rich variety of frequently used circuit tasks such as satisfiability, synthesis, and minimization. We tested the tool on a wide range of practically relevant circuits (computing, in particular, symmetric and arithmetic functions) that have been optimized intensively by the community for the last three years. The tool helped us to win the IWLS 2024 Programming Contest. In 2023, it was Google DeepMind who took the first place in the competition. We were able to reduce the size of the best circuits from 2023 by 12\% on average, whereas for some individual circuits, our size reduction was as large as 83\%.

Paper Structure

This paper contains 25 sections, 7 equations, 4 figures, 16 tables.

Table of Contents

  1. Introduction
  2. New Tool
  3. Related Work
  4. General Setting
  5. Boolean Functions
  6. Boolean Circuits
  7. Tool Features
  8. Analysis
  9. Function Analysis
  10. Circuit Analysis
  11. Synthesis
  12. Manual Synthesis out of Presynthesized Blocks
  13. Automated SAT-based Synthesis
  14. Hybrid Synthesis
  15. Minimization
  16. ...and 10 more sections

Figures (4)

  • Figure 1: A circuit (known as Full Adder) and the corresponding straight line program (in Python) for $\operatorname{SUM}_3$. The output gates are shown in bold.
  • Figure 2: A circuit over the basis $B_2 \setminus \{\oplus, \equiv\}$ computing $\operatorname{SUM}_3$ (left) and its AIG representation (right). The output gates are shown in bold, whereas the negated wires are shown dashed. The binary Boolean operation $>$ is defined in a natural way: $a>b=a \land \overline{b}$.
  • Figure 3: A miter composed out of circuits from Figures \ref{['fig:fulladder']} and \ref{['fig:fulladderaig']}. Since these two circuits compute the same function, the miter is unsatisfiable.
  • Figure 4: A visualization of the miter circuit produced by Listing \ref{['lst:verification']}.