Iterative Circuit Repair Against Formal Specifications

TL;DR

This paper introduces a deep learning method using hierarchical Transformers to repair defective sequential circuits based on formal LTL specifications, significantly improving synthesis accuracy and generalization.

Contribution

The paper proposes a novel hierarchical Transformer architecture and a data generation algorithm for effective circuit repair against formal specifications.

Findings

Improves state-of-the-art repair accuracy by 6.8 percentage points.

Enhances out-of-distribution generalization by 11.8 percentage points.

Demonstrates effectiveness on reactive synthesis competition datasets.

Abstract

We present a deep learning approach for repairing sequential circuits against formal specifications given in linear-time temporal logic (LTL). Given a defective circuit and its formal specification, we train Transformer models to output circuits that satisfy the corresponding specification. We propose a separated hierarchical Transformer for multimodal representation learning of the formal specification and the circuit. We introduce a data generation algorithm that enables generalization to more complex specifications and out-of-distribution datasets. In addition, our proposed repair mechanism significantly improves the automated synthesis of circuits from LTL specifications with Transformers. It improves the state-of-the-art by $6.8$ percentage points on held-out instances and $11.8$ percentage points on an out-of-distribution dataset from the annual reactive synthesis competition.