AIGLE: A Tool for Compact, Legible AIGER Circuits from Safety Specifications

Automated logic circuit design enhances chip performance, energy efficiency, and reliability, with applications in model-checking, reactive synthesis, and hyperproperty verification. AIGER circuits are a standard format for these domains, used in hardware model-checking, synthesis competitions such as Syntcomp, symbolic synthesis algorithms, and the verification of security properties in neural networks and safety-critical systems.

Traditionally, AIGER circuits are generated from Linear Temporal Logic (LTL) specifications through complex pipelines, such as translating LTL to SMV or to automata and then to AIGER. These pipelines guarantee functional equivalence but produce large circuits with auto-generated labels that obscure the specification’s meaning. In applications like symbolic reactive synthesis, model-checking, and neural network verification, understanding latches and outputs is critical for debugging and tool improvement.

In this tool paper, we introduce AIGLE, a novel tool that generates compact AIGER circuits directly from LTL[X] or Past-LTL specifications. Our approach uses linear-size translation from LTL[X] to Past-LTL, which produces highly legible circuits. Compared to tools like py-aiger, our tool reduces gate counts-—often by thousands-— improving readability and synthesis speed. Our empirical evaluation demonstrates smaller, more understandable circuits and faster synthesis, offering a scalable, engineer-friendly solution for formal methods applications.