Iterative Circuit Repair Against Formal Specifications
Authors: Matthias Cosler
Frederik Schmitt
Christopher Hahn
Bernd Finkbeiner
Venue: ICLR 2023 poster (2023)
Keywords: sequential circuits
repair
synthesis
transformer

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.

Published as a conference paper at ICLR 2023
ITERATIVE CIRCUIT REPAIR AGAINST FORMAL SPEC- IFICATIONS
Matthias Cosler
Frederik Schmitt
CISPA Helmholtz Center for Information Security matthi cosler r spa.
CISPA Helmholtz Center for Information Security frederik schmi t spa de
Christopher Hahn
Bernd Finkbeiner
Stanford University
CISPA Helmholiz Center for Information Security finkbeiner&ciss spa.dde
hahn@cs. stanford.edt
ABSTRACT
We present a deep learning approach for repairing sequential circuits against for- mal specifications given in linear-time temporal logic (LTL). Given 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 generaliza- tion to more complex specifications and iittt--distribttion datasets. In addition, our proposed repair mechanism significantly improves the automated synthesis circuits from LTL specifications with Transformers. It improves the state-of of the art by 6.8 percentage points on held-out instances and 11.8 percentage points on distiiibitttoonnnnnnn dataset from the annual reactive synthesis competition.
INTRODUCTION
Sequential circuit repair (Katz & Manna 1975) refers to the task of given a formal specification and defective circuit implementation automatically computing implementation that satisfies the formal specification. Circuit repair finds application especially in formal verification. Examples automated circuit debugging after model checking (Clarke) 1997) correcting faulty circuit implementations predicted by heuristics such as neural networks (Schmitt et al.) (0211). In this paper, we design and study a deep learning approach circuit repair for linear-ting temporal logic (LTL.) specifications (Pnueli 1977) that also improves the state-of-the- of synthesizing sequential circuits with neural networks.
We consider sequential circuit implementations that continuously interact with their environments. For example, an arbiter that manages access to a shared resource interacts with processes by giving out mutually exclusive grants to the shared resource. Linear-time temporal logic (LTL) and its dialects (c.g., STL Maler& & Nickovic (2004) or CTL Clarke & Emerson (1981) are widely used in academia and industry to specify the behavior of sequential circuits (c.g., Godhal al. (2013); IEEB (2005); Horak et al. (202I)). A typical example the response property O O g). stating that always ( holds that request is eventually (+) answered by grant g. We specify arbiter that manages the access to a shared resource for four processes by combining response patterns for requests To, 13 and grants go, .......... 93 with mutual exclusion property as follows:
D + 90) A (m: + Og.) (r2 + 92) A (r's + 033) [((-9 A -1 A (-92 V (gs)) v ((-90 V -91) A -2 A -g))
response properties
mutual exclusion property
A possible implementation of this specification is circuit that gives grants based on round-robin scheduler. However, running neural reactive synthesis (Schmitt et al. 202 on this specification results in a defective circuit shown in Figure After model checking the implementation, observe that the circuit is not keeping track of counting (missing an AND gate) and that the mutual exclusion property is violated (the same variable controls grants go and 91).

---

Published as a conference paper at ICLR 2023
53
92
ga
96
92
91.
16
20
18
16
20
14
12
(a) Faulty circuit, predicted by synthesis model.
(b) Faulty circuit, first iteration of repair model.
aag 12
5
2
input
input (r_2)
input (r_0)
input (r.3)
@2
Q3
go
input (r 1)
latch (10)
14
24
latch (11)
18
10
autput (g.3)
18
output 1 (g.2)
output (g.0)
12
autput (g-1)
0
output 4 (o4)
(c) Correct circuit. Final prediction the repair model in the second iteration (DOT visualization on the left, model's output in AIGER the right).
and-gates
18
15
12
and and-gates
and-gales
22
14
12
and and-gates
and and-gates
Figure I: Circuit representations of 4-process arbiter implementation in DOT visualizations: The triangles represent inputs and outputs, the rectangles represent variables, the diamond-shaped nodes represent latches (flip-flop), ovals represent AND gates, and the black dots represent inverter (NOT gates). The output of our repair model given an AIGER circuit (bottom right).
We present the first deep learning approach to repair such faulty circuits, inspired by the successful application of deep learning to the L.TL trace generation (Hahn al.) (02T) and reactive synthesis problem (Schmitt al. [b. We introduce new Transformer architecture, the separated hi- erarchical Transformer, that accounts for the different characteristics of the problem's input. The separated hierarchical Transformer combines the advantages of the hierarchical Transformer (Li) et al. 2021) with the multimodal representation learning an LTL specification and a faulty circuit. In particular, it utilizes that LTL specifications typically consist of reoccurring patterns. This archi- tecture can successfully be trained on the circuit repair problem. Our model, for example, produces a correct circuit implementation of the round-robin strategy repairing the faulty circuit in Figure in only two iterations. Each iteration predicts a circuit based on the specification and faulty circuit as input. The result of the first iteration is shown in Figure Tb The circuit remains faulty, with two of the four grants still controlled by the same variable. Progress was made, however, towards functioning counter: latch 11 now consists of combination of AND gates and inverters expressive enough to represent a counter. The second iteration finally results in a correct implementation, as shown in Figure Tc
To effectively train and enable further research on repair models, we provide open-source datasets and our open-source implementation for the supervised training of the circuit repair problem!) We demonstrate that the trained separated hierarchical Transformer architecture generalizes to unseen specifications and faulty circuits. Further, we show that our approach can be combined with the existing neural method for synthesizing sequential cireuits (Schmitt et al.) (02Tb) by repairing its mispredictions, improving the overall accuracy substantially. We made a significant improvement of 6.8 percentage points to total of 84% held-out-instancee improvement was made on out-of-diittribution datasets with 11.8 percentage points on samples from the annual reactive synthesis competition SYNTCOMP (Jacobs et al. 2022a).
while even more significant
vi repair
2

---

Published as a conference paper at ICLR 2023
2
RELATED WORK
Circuit repair. The repair problem is an active field of research dating back to Katz & Manna [1975). Jobstmann et al. (2005, 2012) show a game-based approach to repair programs using LTL specifications, |Baumeister et al. 2020) propose an approach for synthesizing reactive systems from LTL specifications iteratively through repair steps. [Ahmad et al. (2022) presented framework for automatically repairing defects in hardware design languages like Verilog. [Staber et al. (2005)
combine fault localization and correction for sequential systems with L.L specifications.
Deep learning for temporal logics and hardware. HHahn et al. (021); |Schmitt et al. (022
initiated the study of deep learning for temporal logies; showing that Transformer can understand the semantics of temporal and propositional logics. |Schmitt et al. (2021b) successfully applied the Transformer to the reactive synthesis problem. Kreber & Hahn (2021) showed that (W)GANs equipped with Transformer encoders can generate sensible and challenging training data for LTL problems. Luo et al. apply deep learning to the LTL, satisfiability problem. Mukherjee et al. (2022) present deep learning approach to learn graph representations for LTL model checking. Vasudevan et al. (2021) applied deep learning to learn semantic abstractions of hardware designs. In Hahn al. (2022). the authors generate formal specifications from unstructured natural language.
Reactive synthesis. The hardware synthesis problem traces back to Alonzo Church in 1957 (Church) (963). Buchi & Landweber (1990) provided solutions, although only theoretically, already in 1969. Since then, significant advances in the field have been made algorithmically. e.g., with a mulsi-polynomial algorithm for parity games (Calude et al., 2020), conceptually with dis- tributed (Pneuli & Rosner 1990) and bounded synthesis (Finkbeiner & Schewe 2013). and on 2006) synthesis. Synthesis algorithms have been developed for hyperproperties (Finkbeiner et al. 2020). Recently, deep learning has been success- fully applied to the hardware synthesis problem (Schmitt et al.) (021b). Compared to classical synthesis, deep learning approach can be more efficient, with the tradcoff' of being inherently in- complete. The field can build on a rich supply of tools (e.g. (Bohy et al. 2012 Faymonville et al. 2017 Meyer et al. 2018a)). A yearly competition (SYNTCOMP) (Jacobs & Pérez) is held at CAV.
efficient Iragments, e.g., GR(I) (Piterman et al.
3 DATASETS
We build on the reactive synthesis dataset from Schmitt et al. (2021b). where each sample consists of two entries: a formal specification in LTL and a target circuit that implements the specification given in the AIGER format. We construct dataset for the circuit repair problem that consists of three entries: a formal specification in I.TI,, a defective circuit, and the corrected target circuit. In Section 3.1 we give details of the domain-specific languages for the circuit repair problem's input. Section 3.2 describes the data generation process and summarizes the dataset that resulted in the best pest-perorming model (see Section O for ablations). We approach the generation of the dataset from two angles: 1) we collect mispredictions, i.e., faulty circuits predicted by neural model, and 2) we introduce semantic errors to correct circuits in way that they mimic human mistakes.
3.1 LINEAR-TIME TEMPORAL LOGIC (LTL) AND AND-INVERTER GRAPHI (AIGER)
LTL specifications. The specification consists of two lists of sub-specifications: assumptions and guarantees. Assumptions pose restrictions on the environment behavior, while guarantees describe how the circuit has to react the environment, They jointly build an LTL specification as follows: spec = (assumplion; A ... A ussumplion, - (guaranlees A ... A ). A speci- fication is called realizabile there exists a circuit implementing the required behavior and called unrealizable if no such circuit exists. For example, an implementation can be unrcalizable if there are contradictions in the required behavior, or if the environment assumptions are not restrictive enough. Formally, an LTI. specification is defined over traces through the circuit. A circuit C' satis- fies an LTL specification yp if all possible traces through the circuit Tracesc satisfy the specification, i.e., if vt E Trucesc. & } sp For example, the LTL formula O( (-99 -9o V -91) from the arbiter example in Section 3.I requires all traces through the circuit to respect mutual exclusive behavior between Go and 91. If a specification is realizable, the target circuit represents the implementation, and if speci- fication is unrealizable, the target circuit represents the counter-stratege of the environment showing that no such implementation exists. The formal semantics of LTL. can be found in Appendix A
3

---

Published as a conference paper at ICLR 2023
Algorithm 1 Algorithm for introducing errors to correct circuit implementations.
circuit C, number of changes standard deviation de, maximum number of changes Mc new variable number standard deviation ov, delete line probability Pdelete
Input:
2: Output: circuit C
3: changes ~ o.",
Sample from discrete truncated Gaussian
4: for i 0 to changes do
5: with probability Paelete do
6: [~ U(1, number of lines in C))
Sample line number uniformly
7:
Remove line of C
8:
else
9:
pos ~ (11, number of positions in C)
> Sample position uniformly
var' t- var +- variable number at position pos in C while var = var' do var' (var, o. .0.61)
11:
b Sample from discrete truncated Gaussian
13:
replace variable number at position pos in C¹ with var'
AIGER format. The defective and target circuits, are in text-based representation of And-Inverter Graphs called AIGER Format (Brummayer et al. (007);; see, for example, bottom-right of Figure [ A line in the AIGER format defines nodes such as latches (flip-flops) and AND-gates by defining the inputs and outputs of the respective node. Connections between nodes are described by the variable numbers used the input and output of nodes. A latch is defined by one input and one output connection, whereas two inputs and one output connection define an AND gate. Inputs and outputs of the whole circuit are defined through lines with single variable number that describes the connection to a node. The parity of the variable number implicitly gives negations. Hence, two consecutive numbers describe the same connection, with odd numbers representing the negated value of the preceding even variable number. The numbers 0 and 1 are the constants False and True. The full definition of AIGER circuits can be found in Appendix
3.2 DATA GENERATION
We replicated the neural circuit synthesis model of Schmitt al. (202lb) and evaluated the model with all specifications from their dataset while keeping the training, validation, and test split sepa- rate. We evaluated with beam size of 3, resulting in dataset Repai rRaw of roughly 580 000 specifications and corresponding (possibly faulty) circuits in the training split and about 72 000 in the validation and test split, respectively. We model-check each predicted circuit against its speci- fication with nuXmv (Cavada et al., 2014) to classify defective implementations into the following classes. A sample violated the predicted circuit defective, i.c., violates the specification (55%). A sample is matching if the prediction of the synthesis model is completely identical to the target circuit in the dataset (16%). Lastly, sample is satisfied when the predicted eircuit satisfies the specification (or represents a correct counter- (ounter-strategy) but is no match (29%). which regularly hap- pens as a specification has multiple correct implementations. For example, consider our round-robin scheduler from the introduction: the specification does not specify the order in which the processes are given access to the resource.
We construct our final dataset from Repa i rRaw in two steps. In the first step, we consider the violating samples, i.c., mispredictions of the neural circuit synthesis network, which are natural candidates for circuit repair dataset. In the second step, introduce mistakes inspired by human errors into correct implementations (see Figure 6 in the appendix for an overview of the dataset generation and its parameters). In the following, we describe these steps in detail.
Mispredictions of neural circuit synthesis. We first consider the violating samples from Repair rRaw. Likewise to specification having multiple correct implementations, defective circuit has multiple possible fixes, leading to correct yet different implementations. For a given de- fective circuit, fix can thus either be small and straightforward or lengthy and complicated. In supervised learning setting, this leads us to the issue of misleading target circuits. This concerns samples where only lengthy and complicated fix of the faulty circuit leads the target circuit,
4

---

Published as a conference paper at ICLR 2023
global layer parameters
specilication parameters
circuit parameters
assumption
guarantee
circuit
Figure 2: The structure of global and local layers the separated hierarchical Transformer. For simplicity, shown for single assumption, single guarantee and only two tokens each.
although a minor fix would also lead a correct but different implementation. We identify mislead- ing targets by searching for alternative solutions with the synthesis model (up to a beam size of 4). If the model finds a correct alternative circuit with a smaller Levenshtein distance (see Appendix C for definition) to the faulty circuit, a fix leading to the alternative circuit is smaller than fix to the original target. The target circuit will replaced accordingly with the alternative circuit. We select all samples with Levenshtein distance to the target circuit 50 for the final dataset.
Introducing errors. We propose Algorithm [ which probabilistically introduces human-like mis- takes into correct circuits. Such mistakes include missing latches, AND gates, or inverters and mis- wired connections between the components. First, we determine the number of mistakes or changes will introduce to the circuit. For that, sample from a discrete truncated normal distribu- tion around zero, with a standard deviation of 7.5 and bounds from to 50. For each change, we flip coin with the probability of Pdelete 0.2 for deleting a line from the AIGER cireuit and 1- Pdelete = 0.8 for changing a variable number. For deleting, we uniformly choose line from the AIGER circuit remove. We do remove inputs outputs stay consistent with the dataset. For changing a variable number, we uniformly choose position a variable number. The position can be an input, output, inbound edge(s), outbound edge of latch or AND gate. We replace the variable number at this position with new variable number that is determined by sampling discrete truncated normal distribution around the old variable number, a standard deviation of and bounds given by the minimal and maximal possible variable number in the dataset (0 to 61). The new variable number cannot be the mean itself to ensure a definite change. For visualization of the discrete truncated normal distributions, see Figure 7 in the appendix. Lastly, spot-check altered circuits by model-checking to determine whether introduced changes create faulty circuit. Only in less than 2% of the cases the cireuit still satisfies the specification.
Final Dataset. In the final dataset Repair, 61% of the samples contain circuits with errors intro- duced by Algorithm [ while the others are based mispredicted circuits. In 38% of cases, the samples have a Levenshtein distance of less than 10 between the repair circuit and the target circuit. In total, the Levenshtein distance in the dataset has mean of 15.7 with standard deviation of 12.77, and the median is at 13 (see Figure X Appendix for its composition).
ARCHITECTURE
In this section, we introduce the separated hierarchical Transformer architecture, a variation of the hierarchical Transformer Li et al. (2021), and provide further details our architectural setup. The hierarchical Transformer has been shown to be superior to a vanilla Transformer in many appli- cations including logical and mathematical problems Li al. 20 Schmitt al. (2021b). The hierarchical Transformer, as well as the novel separated hierarchical Transformer, is invariant against the order of the assumptions and guarantees in the specification.
5

---

Published as a conference paper at ICLR 2023
4.1 SEPARATED HIERARCHICAL TRANSFORMER
The encoder of a hierarchical Transformer contains two types of hierarchically structured layers. Local layers only see parts of the input, while global layers handle the combined output of all lo- cal layers. Contrary to the original Transformer, the input is partitioned before being fed into the local layers. A positional encoding applied separately to each partition of the input. Model pa- rameters are shared between the local layers, but no attention can be calculated between tokens in different partitions. The hierarchical Transformer has been beneficial to understanding repetitive structures in mathematics (Li et al. 2021) and has shown to be superior for processing LTL specifi- cations (Shhmitt et al. 2021b).
We extend the hierarchical Transformer to separated hierarchical Transformer, which has two types of local layers: Each separated local layer an independent encoder; therefore, separated local layers do not share any model parameters. Attention calculations local layer. A visualization of the proposed Architecture is shown in Figure 2 Shared local layers are identical to local layers in the hierarchical Transformer. A separated local layer contains or more shared local layers. The results of the separated and shared local layers are concatenated and fed into the global layer. While the number of shared local layers does not change the model size, multiple separated local layers introduce slightly more model parameters. The separated hierarchical Transformer handles multiple independent inputs that differ in structure, type, length better.
done independently for each
4.2 ARCHITECTURAL SETUP
We separate the specification and the faulty circuit with a separate local layer. The specification partitioned into its guarantees and assumptions, which we feed into shared local layers. Let Attention be the attention function of Vaswani et al. (2017) (see Appendix K]. When identifying the assumptions assumplion, ... ,ssumppiinn, and guarantees guaranlee). guaranleem with specification properties Pl......PP*.. the following computations are performed in shared local layer:
Attention H,,, W Hl, W W5) where pj {Pi,.... (Pit...,,PPt.))) Pn+m3
where Hp. denotes the stacked representations of all positions of specification property P:- There- fore, the attention computation is limited between tokens in each guarantee and between tokens in each assumption while the learned parameters W.. W WV are shared between all guarantees and assumptions. The separated local layer that processes the circuit performs the attention computation:
Attention(HHoWe HoW H)W
where He denotes the stacked representations of positions of the circuit. Therefore, the com- putation is performed over all tokens the circuit but the parameters W W.K, wy are different from the parameters for the specification (see Figure 2
For embedding and tokenization, we specialize in the Domain Specific Language (DSL) of LTL formulas and AIGER circuits with only a few symbols. For every symbol in the DSL, we introduce a token. Variables in properties (i.e., assumptions and guarantees) are limited to five inputs ig -.... i i4 and five outputs Ou 04. for each of which we introduce token. In the AIGER format (used for the faulty circuit and the target circuit), we fix the variable numbers to the range 0 to 61, thereby indirectly limiting the size of the circuit, while allowing for reasonable expressiveness. We set a special token as a prefix to the circuit embedding to encode the presumed realizability of the specification. This determines whether the circuit represents satisfying circuit a counter strategy- We embed the tokens by applying one-hot encoding which we multiply with a learned embedding matrix. Properties have tree positional encoding (Shiv & Quirk 2019) used for LTL formulas by (Hahn et al.) 202T). This encoding incorporates the tree structure of the LTL formula into the positional encoding and allows easy calculations between tree relations. For eircuits, we use the standard linear positional encoding from Vaswani et al. (2017).
5 EXPERIMENTS
In this section, we report on experimental results. We first describe our training setup in Section 5.1 before evaluating the model with two different methods. The model evaluation shows the evaluation

---

Published as a conference paper at ICLR 2023
100
samples (%)
50
10
20
30
40
50
60
70
Levenshtein distance
Semantic Accuracy (smoothed) violated (copy) satisfied
violated match
Figure 3: Accuracy broken down by the Levenshtein distance between faulty and target circuit.
of the repair model the Repai dataset distributiion(Sction 5.2 In the synthesis pipeline eval- uation, the repair model is evaluated on the predictions of the synthesis model and then repeatedly evaluated on its predictions (Section 5.3). We differentiate between syntactie and semantic accuracy, following Hahn et al. (2021). A sample is considered semantically correct if the prediction satisfies the specification. We consider the prediction syntactically correct if it is identical to the target.
5.1 TRAINING SETUP
We trained a separated hierarchical Transformer with 4 heads in all attention layers, 4 stacked local layers both separated local layers, and stacked layers in the global layer. The decoder stack contains 8 stacked decoders. The embedding size in the decoder and encoder is 256 and all feed- forward networks have size of 1024 and use the Rectified Linear Unit (ReLU) activation function. We use the Adam optimizer (Kingma & Ba 2017) with 31 = 0.9, 3g = 0.98 and 4000 warmup steps with an increased learning rate, as proposed in Vaswani et al. (017). . We trained on single GPU of a NVIDIA DGX A A100 system with batch size of 256 for 20000 steps. We restricted the specification input to 5 inputs and 5 outputs, no more than 12 properties (assumptions guarantees) and no properties of size of its abstract syntax tree (AST) greater than 25.
10-3 and
5.2 MODEL EVALUATION
We evaluated the model up to a beam size of 16. The key results of the model evaluation can be found the top of Table With a beam size of 16, the model outputs a correct implementation in 84% of the cases on single try. When analyzing the beams, we found that the model shows enormous variety when fixing the circuits. Almost half of the beams result correct implementations. To investigate if the model performs repair operation, we identify samples where the model copied the defective circuit ( (Violated (Copy)). The model only copied 31 of 1024 samples. We, additionally, track if the predicted circuit contains syntax errors, which rarely happens (a total of 8 errors out of every beam). We provide insight into the model's performance by analyzing a) what exactly makes sample challenging solve for the model and b) if the model makes significant improvements towards the target circuit even when the prediction violates the specification.
Difficulty measures. We consider three parameters measure the difficulty of solving a specific repair problem: the size of the specification (the LTL formula's AST), the size of the target circuit (AND gates + latches), and the Levenshtein distance between the defective circuit and the target circuit. The Levenshtein distance is the dominant indicator of a sample's 's difficulty (see Figure 3). However, the specification and circuit size is, perhaps surprisingly, less of factor (see Figure II and Figure 10 in the appendix). This indicates that our approach has the potential to scale up to larger circuits when inereasing the model size.
Improvement measures. We semantically and syntactically approximate whether violating pre- diction still an improvement over the faulty input circuit. For syntactic improvement, we cal- culate the difference between the distance of the faulty input and target circuit lev(C;, C.) and the distance between prediction and target circuit leo(Cp. C.). If the difference below zero: (ev(Cp. C.) Leu(C), C,) 0, the model syntactically improved the faulty circuit towards the target circuit. On our test set, violated circuits improved by 99.98 edits on average. For seman- tic improvement, obtained set of sub-specifications by creating new specification with each
7

---

Published as a conference paper at ICLR 2023
100
samples (%)
50
11
11.
20
80
120
140
160
specification size
Semantic Accuracy (new, smoothed) Match Satisfied (unchanged)
Violated Error (remaining) Satisfied (new)
Match (new)
Figure 4: Improvements on the reactive synthesis held-out test set (see test in Table D broken down by the size of the specifications AST. We aggregate the best result from all iterations over 16 beams. The annotations new and unchanged indicate whether the status improved from the evaluation of the synthesis model to the evaluation of the repair model.
guarantee from the original specification: Let 01 to an be the original assumptions and 91 to Jm the original guarantees, the set of sub-speciffiattios is defined {(a) A... A an.) - 9i S S m)- We approximate that, the more sub-specifications circuit satisfies, the closer semantically to correct circuit. On our test set, in 75.9%, the prediction satisfied more sub-specifications, and in 2.4%, the prediction satisfied fewer sub-specifications. For more detailed insight, we supported violin plots for syntactic (Figure T2) and semantic (Figure [3) improvement in the Appendix. Since in both approximations, even violating predictions are an improvement over the faulty input, this poses the natural question if the model's performance can be increased by iteratively querying the model on its predictions. In the next section, we investigate this more in-depth by applying our repair model iteratively the prediction of neural circuit synthesis model including real-world examples.
5.3 SYNTHESIS PIPELINE EVALUATION
We demonstrate how our approach can be used improve the current state-of-the-art for neural reactive synthesis (see Figure We first evaluate the synthesis model we replicated from |Schmitt al. (2021b). the predicted eircuit violates the specification, we feed the specification together with the violating circuit into repair model. If the prediction still violates the specification after applying the repair model once, we re-feed the specification with the new violating circuit into the repair model until it is solved. Using the presented pipeline, we improve the results of Schmitt et al. (2021)) significantly, as shown the bottom half of Table [ We evaluate held- samples from the synthesis dataset and of-distribution benchmarks and filtered out samples that exceed our input restrictions (see Section 5.T.. The datasets test contain randomly sam- pled held-out instances from the repair and neural synthesis dataset, respectively. Figure shows an in-depth analysis of the status changes of the samples when applying the synthesis pipeline.
Table 1: Syntactic and semantic accuracy the model (top) and pipeline (bottom) evaluation.
Beam Size
16
semantic accuracy
58.3%
84.8%
syntactic accuracy
29.4%
53.2%
correct beams per sample
0.58
6.57
synthesis model
after first iteration
after up to n iterations
test (repair dataset))
84.2%
87.5% (+3.3)
test (synthesis dataset)
77.1%
82.6%
(+5.5)
83.9%
(+6.8)
5
timeouts
26.1%
32.5%
(+7.4)
34.2%
(+8.1)
5
syntcomp
64.1%
71.7%
(+7.6)
75.9%
(+11.8)
smart home
42.9%
61.9% (+19)
66.7%
(+23.8)
8

---

Published as a conference paper at ICLR 2023
Light and dark green represent the instances that were additionally solved with our repair approach; gray represent the instances that were already initially solved by the synthesis network. The prob- lem becomes increasingly more challenging with a larger target cir- cuit size. In total, achieve an improvement of 6.8 percentage points. To show that our improvement over the state-of-the-ar is due to scaling but rather a combination new training data, ar- chitecture and iterative evaluation, we additionally scaled the model from |Schmitt et al. (2021b) match or exceed the number of pa- rameters of our model. The parameter-matched models only lead to insignificant improvements over the base model (see Table in the Appendix). We further identified a set of held-out samples were our approach performs significantly better than the classical state- of-the-art synthesizer tool Strix (Meyer et al. 2018b); Samples in t cimeouts could not been solved by Strix in 1h, of which we still achieve 34.2% with an improvement of 8.1 percentage points. Even more significant improvement can be observed in real-world sam- ples from the annual synthesis competitions and out-of-distribution benchmarks: The dataset smart home are benchmarks for syn- thesizing properties over smart home applications (Geier et al. 2022), where we improve by 11.8 percentage points. The dataset synt.omp contains benchmarks from the annual reactive synthe- sis competition (Jacobs et al.) 2022a b), where the model pipeline improves the state-of-the-art by 23.8 percentage points and even by 19 percentage points by applying it once.
Specification
LTT.)
Neural Ciranit Synihesis
Hierarchicnl
Transformer
Circuit (Prodiction)
Model Chocking
(Faulty) AIGER ciecuig
Specification (in LTL)
lterative Circuit Repuir
Separated Hierarchical Transformer
Circuir (Prediction)
Madel Checking
Figure 5: Pipeline structure
6 ABLATIONS
We performed various ablation studies that the interested reader can find in the appendix. In partic- ular, we parameterized our data generation for constructing the circuit repair dataset (see Figure Appendix D). An extensive collection of over 100 generated datasets at GitHut We trained various models based on these datasets and different byperparameters, also available at GitHub. A hyperparameter study can be found in Figure 3 in Appendix [] An in-depth analysis of the results of different models tested in the synthesis pipeline can be found in Appendix[]
available through code
7 CONCLUSION
In this paper, we studied the first application of neural networks to the circuit repair problem. We introduced the separated hierarchical Transformer account for the multimodal input of the prob- lem. We provided a data generation method with a novel algorithm for introducing errors to circuit implementations. A separated hierarchical Transformer model was successfully trained repair defective sequential circuits. The resulting model was used to significantly improve the state-of-the art in neural circuit synthesis. Additionally, our experiments indicate that the separated hierarchical Transformer has the potential to scale up to even larger circuits.
Our approach can find applications the broader hardware verification community. Possible appli- cations include the automated debugging of defective hardware after model checking or testing. Due to its efficiency, a well-performing neural repair method reduces the necessary human interaction in the hardware design process. The benefit of a deep learning approach to the circuit repair problem is the scalability and generalization capabilities deep neural networks: this allows for an efficient re-feeding of faulty circuits into the network when classical approaches suffer from the problem's 's high computational complexity. Moreover, neural networks generalize beyond classical repair op- erations, whereas classical approaches are limited in their transformations, such the limitation of replacing boolean fuucciions. Future work includes, for example, the extension of our approach to hardware description languages, such as VHDL Verilog, and the extension other specification languages that express security policies, such as noninterference or observational determinism.
httts://gi httpr/etttteeeetteeeeeeeeerriiie

---

Published as a conference paper at ICLR 2023
REPRODUCIBILITY STATEMENT
All models, datasets, code, and guides are available in the corresponding code repository. All our datasets and models mentioned in the paper, the code of the data generation method, and the code for training new models as well as evaluating existing models are licensed under the open-source MIT License. Multiple Jupyter notebooks guide the interested reader through the use of the code to allow low-effort reproducibility of all our results and encourage fellow researchers to use, extend and build on our work.
ACKNOWLEDGMENTS
This work was partially supported by the European Research Council (ERC) Grant HYPER (No. 101055412).
REFERENCES
Hammad Ahmad, Yu Huang, and Westley Weimer. Cirfix: automatically repairing defects hard- ware design code. In Proceedings of the 27th ACM International Conference Architectural Support for Programming Languages and Operating Systems, pp. 990-1003, 2022.
Tom Baumeister, Bernd Finkbeiner, and Hazem Torfah. Explainable reactive synthesis. In Interna- tional Symposium on Automated Technology for Verification and Analysis, pp. 413-428. Springer, 2020.
Aaron Bohy, Véronique Bruyere, Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. Aca- cia+, tool for LTL synthesis. In International Conference on Computer Aided Verification, pp. 652-657. Springer, 2012.
Robert Brummayer, Alessandro Cimatti, Koen Claessen, Niklas Een, Marc Herbstritt, Hyondeuk Kim, Toni Jussila, Ken McMillan, Alan Mishchenko, and Fabio Somenzi. The AIGER And- Inverter Graph (AIG) Format Version 20070427. 2007.
J Richard Buchi and Lawrence Landweber. Solving sequential conditions by finite-state strategies. In The Collected Works of J. Richard Büichi, pp. 525-541. Spriner, 1990.
Cristian S Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasi-polynomin time. SIAM Journal on Computing, (0):STOCI7-152, 2020.
Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. The nuxmv symbolic model checker. In Armin Biere and Roderick Bloem (eds.), Computer Aided Verification 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL. 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Com- puter Science, pp. 334 332-342. Springer, 2014. doi: 10.1097/778-333 3-7788--33199 3-319-088667-9
URL
org.i.oorg//e 10. 0ttp//.0..1177999
319 08867-9 22
Alonzo Church. Application of recursive arithmetic to the problem of circuit synthesis. 1963.
Edmund M Clarke, Model checking. In International Conference on Foundations of Software Technology and Theoretical Computer Science, pp. 54-56. Springer, 1997.
Edmund M Clarke and E Allen Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on logic of programs, pp. 52-71. Springer, 1981.
Peter Faymonville, Bernd Finkbeiner, and Leander Tentrup. BoSy: An experimentation framework for bounded synthesis. In International Conference on Computer Aided Verification, pp. 325-332. Springer, 2017.
Bernd Finkbeiner and Sven Schewe. Bounded synthesis. International Journal on Software Tools for Technology Transfer, 15(5):519-539) 2013.
10

---

Published as a conference paper at ICLR 2023
Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. Synthesis from hyperproperties. Acta informatica, 57(1):137-163, 2020.
Gideon Geier, Philippe Heim, Felix Klein, and Marvin Stenger. J.I.R. TSL/TLSF benchmark suite, 2022. URL https:://ttttttaet com/ SYNTCOMP http:o//////eccaaakk....e
Yashdeep Godhal, Krishnendu Chatterjee, and Thomas A. Henzinger. Synthesis of AMBA AHB from formal specification: case study. Int. J. Sofiw. Tools Technol. Transf., 15(5-6); 585-601, 2013. doi: 10. (007///10009001-00007--0 URL 120009-011-02017
wrg./o.......... 1007/
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner. Teach- ing temporal logics to neural networks. In International Conference on Learning Representations, 2021. /tppatt///eeeeeessww.eeeert www.:eeeeeooommmmdd.ede...eo
f4byz
Christopher Hahn, Frederik Schmitt, Julia J Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner. Formal specifications from natural language. arXiv preprint 2206.022000019666 2022.
Tom Horak, Norine Coenen, Niklas Metzger, Christopher Hahn, Tamara Flemisch, Julián Méndez, Dennis Dimov, Bernd Finkbeiner, and Raimund Dachselt. Visual analysis of hyperproperties for understanding model checking results. IEEE Transactions on Visualization and Computer Graphics, (8(1):3573367, 2021.
IEEE. Ieee standard for property specification language (psl). IEEE Std 1850-2005, pp- 1-143, 2005. doi: 10. 10.100/IEEESTT22205.77777
Sven Jacobs and Guillermo A. Pérez. The 7th reactive synthesis competition: SYNTCOMP 2020.
http:// wwww htt.:w/sstcoom..cm wrt.or///sy.... httpg////ttcooppooo 2twpiiccoomm200-eeeeeee0e0- 20200resu1000ere results/
Swen Jacobs, Guillermo A. Perez, Remco Abraham, Veronique Bruyere, Michael Cadilhac, Max- imilien Colange, Charly Delfosse, Tom Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissied Mouhammad Sakr, Salomon Sickert, Gaetan Staquet, Clement Tamines, Leander Tentrup, and Adam Walker. SYNT- COMP 2020 Results The Reactive Synthesis Competition, June 2022a. URL http:///// synt wwt.orgg./....... synt www.ooomoo-c---- results/
Swen Jacobs, Guillermo A. Perez, Remco Abraham, Veronique Bruyere, Michael Cadilhac, Maxim- ilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Shnlchuber-Caissiee Mouhammad Sakr, Salomon Sickert, Gaetan Staquet, Clement Tamines, Leander Tentrup, and Adam Walker. The Reactive Synthesis Competition (SYNTCOMP): 2022-20,, June 2022b. URL htth:httt///artt org// Number: arXiv:2206.0022 00251 arXiv:2206.0025 [cs].
abs/2206. 00251
Barbara Jobstmann, Andreas Griesmayer, and Roderick Bloem. Program repair as game. In International conference on computer aided verification, pp. 226-238. Springer, 2005.
Barbara Jobstmann, Stefan Staber, Andreas Griesmayer, and Roderick Bloem. Finding and fixing faults. Journal of Computer and System Sciences, 78(2):441-400, 2012. Publisher: Elsevier.
Shmuel Katz and Zohar Manna. Towards automatic debugging of programs. ACM SIGPLAN No- fices, 10(6):143-155 1975.
Diederik P. Kingma and Jimmy Ba. Adam: Method for Stochastic Optimization, January 2017. [cs].
URL http:://ttxpii..tttp// org. abs/ /tt.s////..... 6980
Jens U Kreber and Christopher Hahn. Generating symbolic reasoning problems with transformer gans. arXiv preprint arXiv:2 10. 10054, 2021.
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. IsarStep: Benchmark for High-level Mathematical Reasoning. Technical Report S.Xiv:2006.002663 arXiv, March 2021. URLhttr 09265 arXiv:2006.09265 [cs, stat] type: article.
//arx

---

Published as a conference paper at ICLR 2023
Weilin Luo, Hai Wan, Jianfeng Du, Xiaoda Li. Yuze Fu, Rongzhen Ye, and Delong Zhang. Teaching Itlf satisfiability checking to neural networks.
Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pp. 152-166. Springer, 2004.
Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit reactive synthesis strikes back! Computer Aided Verification 33thh International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 Lecture Notes in Computer Science, pp. 578-586. Springer, 201 1a. doi: 10. 3-17798--3999911555
Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit Reactive Syn- thesis Strikes Back! In Hana Chockler and Georg Weissenbacher (eds.), Computer Aided Verification, Lecture Notes in Computer Science, pp. 578-586, Cham, 2018b. Springer Inter- national Publishing. ISBN
doi: 10.
URL
https: /tts:://stix..o mow.l...o.d..................... in. tum. de/
Prasita Mukherjee, Haoteng Yin, Susheel Suresh, and Tiark Rompf. Octal: Graph representation learning for Itl model checking, arXiv preprint arXiv:2207. 16649, 2022.
Nir Piterman, Amir Pnueli, and Yaniv Sa' ar. Synthesis of reactive(1) designs. In E. Allen Emerson and Kedar S. Namjoshi (eds.), Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, volume 3855 of Lecture Notes in Computer Science, pp. 364-380. Springer, 2006. doi: 10. 11609773).24. URL
1111111.1001111 1tt.o/..o00001111011010077701000
24
Amir Pneuli and Roni Rosner. Distributed reactive systems are hard to synthesize. In Proceedings [1990] 31 Annual Symposium on Foundations of Computer Science, pp. 746-757. IEEE, 1990.
A. Pnueli. The temporal logic of programs. In 18th Annual Symposium Foundations of Computer Science (sfcs 1977). pp. 46-57, October 1977. doi: 10.1109/SFCS.1977.3
Frederik Schmitt, Christopher Hahn, Jens U Kreber, Markus N Rabe, and Bernd Finkbeiner. Deep learning for temporal logics. 6th Conference on Artificial Intelligence and Theorem Proving (AITP), 2021a.
Frederik Schmitt, Christopher Hahn, Markus N. Rabe, and Bernd Finkbeiner. Neural circuit synthe- sis from specification patterns. In Advances Neural Information Processing Systems 34 Pre- proceedings, 2021b. URL 8230bea7d5 22230baa77544ccdc99ccee33333
neurips.......pp..p............. cc http:ppss.cpppppp/eepeeee/ Saaper22221/hss2 7313d5 Abst.sctstt........ html
Vighnesh Shiv and Chris Quirk. Novel positional encodings to enable tree-based transform- In Advances in Neural Information Processing Systems, volume 32. Curran Asso- ciates, Inc., 2019. URL (tt.:///66644dddddbcedceco wttpreootteeee-tttttttt......... html
Abstract
Stefan Staber, Barbara Jobstmann, and Roderick Bloem. Finding and fixing faults. In Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pp. 35- 49. Springer, 2005.
Shobha Vasudevan, Wenjie Joe Jiang, David Bieber, Rishabh Singh, C Richard Ho, Charles Sut- ton, et al. Learning semantic representations to verify hardware designs. Advances in Neural Information Processing Systems, 34:23491-23504, 2021.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention All you Need. In Ad- vances in Neural Information Processing Systems, volume 30. Curran Associates, wew.eeiiiinnnnnnenisseeee httppppee//22//ast// Inc., 2017. URL http::ts/ppoooceeeeiiieee html
12

---

Published as a conference paper at ICLR 2023
A LINEAR-TIME TEMPORAL LOGIC (LTL)
The syntax of linear-time temporal logic (LTL) Pnueli 1977) is given as follows.
+ = p 9 1
up Op ppl p
where p is an atomic proposition AP. In this context, we assume that the set of atomic propo- sitions AP be partitioned into inputs and outputs O: AP 130.
The semantics of LTL is defined over a set of traces: TR := (24P)). Let E TR be trace, "[o] the starting element of trace and for k N and be TT|] be the kth element of the trace л. With [[] denote the infinite suffix of starting at k. We write F + for the trace satisfies the formula 4p
For trace E TR, p E AP and formulas yp the semanties of LTL is defined as follows:
x iff 4
p TTo i b -p iff E [[0]
x F 9 12 iff क + ppandd - 922
x O iff || F
x = 인 u 62
iff 31 N: (TT()))) F P2 A Vm E [0,[-1] [(m,oo) } (1))
We use further temporal and boolean operators that can be derived from the ones defined above.
That includes V, -, boolean operators and the following temporal operators:
ii S2 (release) is defined -(-9) U xp2)
D (globally) is defined as false R yp
p (eventually) is defined as true 21 y
REACTIVE SYNTHESIS
Reactive synthesis is the task to find circuit C that satisfies given formal specification ço, i.e., Vt E Tracese. t = i0, or determine that no such circuit exists. We consider formal specifications that are formulas behavior of a system based on a set of input and output variables. As the system, we consider circuits, more precisely
set of atomic propositions (AP) in LTL. The specification defines the desired
representation And-Inverter Graphs, called AIGER circuits. And-Inverter Graphs connect input and output edges using AND gates, NOT gates (inverter), and memory cells (latches).
B AND-INVERTER GRAPHS
Graphs are graphs that describe hardware circuits. The graph connects input edges with output edges through AND gates, latches, and implicit NOT gates. We usually represent this graph by a text version called the AIGER Format (ermaat/rummaye et al. (2007). The AIGER format uses variable numbers that define variables. Variables be interpreted wired connections in circuit or as edges in graph, where gates and latches are nodes.
A negation is implicitly encoded by distinguishing between even and odd variable numbers. Two successive variable numbers represent the same variable, the even variable number represents the non-negated variable, and the odd variable number represents the negated variable. The variable numbers 0 and 1 have the constant values FALSE and TRUE.
Each input and output edge is defined by a single variable number, respectively.
An AND gate is defined by three variable numbers. The first variable number defines the outbound edge of the AND gate, and the following variable numbers are inbound edges. The value of the outbound variable is determined by the conjunction of the values of both inbound variables.
13

---

Published as a conference paper at ICLR 2023
A latch is defined by two variable numbers: outbound edge and inbound edge. The value of the outbound variable the value of the inbound variable at the previous time step. In the first time step, the outbound variable is initialized as FALSE.
The AIGER format starts with a header, beginning with the letters aag and following five non- negative integers M, I, L, o, A with the following meaning:
MEmaximum variable index 1=number of inputs 1.=numerr of latches O=number of outputs A=number of AND gates
After the header, each line represents a definition of either input, latch, output, or AND gate in this order. The numbers in the header define the number of lines associated with each type. After the definition of the circuit, an optional symbol table might follow, where we can define names for inputs, outputs, latches, and AND gates. In this context, the circuit either describe satisfying system or counter strategy to the specification.
C LEVENSHTEN DISTANCE
The Levenshtein distance is an edit distance metric, measuring the degree of distinction between two strings. Let $1 and $2 two given strings, then the Levenshtein distance lev 81, $2) is a the number of actions necessary transform string 81 into string 82 vice versa. Possible actions are deletions, insertions, and substitutions.
D DATA GENERATION
In Figure 6 we sketch the data generation process. The base of the process is the evaluation of model for neural circuit synthesis. This is parameterized as multiple beam size are possible. For mispredicted samples,
replace misleading targets (see Section 3.2 This is optional but our experiments showed that the training benefits from this step. Up to a given Levenshtein distance, we collect samples for the final dataset. All other samples (greater Levenshtein distances and correct predictions) are processed in Section 3.2 and Algorithm This process is optional, can be applied only some samples and also parameterized. The results can used for the final dataset are, depending on various parameters, discarded.
parameterized optional
evaluation of neural circuit sythesis
mispredicted samples
correct samples
replace misleading
Introduce artificial mistakes
targets
distance 50
distance
50
FINAL DATASET
Figure 6: Overview over the data generation process.
Figure shows the probability mass function for the used truncated normal distributions used in Algorithm I Figure g shows the composition the final dataset. Samples are sorted into bins depending the Levenshtein distance between its faulty circuit and its target circuit. While yellow shows all samples in the final dataset, blue only shows samples in the final dataset that are based on Section 3.2 and red only shows samples that are based Section 3.2
14

---

Published as a conference paper at ICLR 2023
0.08
0.04
probability
0.06
0.03
0.02
10
20
30
40
20
40
60
number of changes per sample
new variable number
Figure 7: Probability mass function for the truncated normal distributions. Left: distribution for sampling the number of changes. Right: distribution for sampling variable number with exem- plary old variable number 12.
60k
40k
count
20k
10
50
Levenshtein distance between repair circuit and target circuit
depicted samples
samples with mispredicted faulty circuits samples with altered faulty circuits
final dataset
Figure Composition of the final dataset. Outliers >> 55 not shown.
In Figure 9 show the composition three alternative datasets. Samples sorted into bins depending on Levenshtein distance between its faulty circuit and its target circuit. The dataset scpa scpa-
(blue) shows dataset that is solely based on Section 3.2 Datasets scpa-repair-gen-1000 and scpa-repa Sempairrgen--- 96 (red and yellow) are the two best per- and and Section 3.2
forming datasets from all datasets we trained and based on a mixture Section 3.22
Dataset scpa-repair-gen- 9 (yellow) is the dataset presented in this paper.
E DIFFICULTY MEASURES
Figure 10 and Figure (together with Figure 3) show predictions of the presented model, sorted into bin by specification and target size as well as Levenshtein distance between faulty input circuit and target circuit. We use beam search (beam size 16) and only display the result of the best beam. Different colors depict the different classes, a sample is sorted into, i.c. violated for prediction that violates the specification and violated (copy) for prediction that additionally is identical to the faulty input. satisfied for correct predictions and match for predictions that additionally are identical to the target circuit. The line shows the semantic accuracy smoothed over several bins.
15

---

Published as a conference paper at ICLR 2023
60k
40k
count
20k
20
40
60
80
100
Levenshtein distance hetween repair circuit and target circuit scpa-repair-attes (9trai))
dataset
scpa-repair-gen -enpparr-ge--OO((rain))
scpa-repair-gen--66trann)))
Figure 9: Comparison of the two best performing datasets and dataset that solely based on altered circuit data. Range 0 to 100
100
samples (56
50
20
40
60
80
100
120
140
160
specification size
Semantic Accuracy (smoothed) violated (copy)
error
violated
satisfied
match
Figure 10: Accuracies and sample status broken down by the size of the specification AST.
100
samples (%)
50
0
5
target size
Semantic Accuracy (smoothed) violated (copy) satisfied
violated
match
Figure 11: Accuracies and sample status broken down by the size the target circuit (ands latches).
16

---

Published as a conference paper at ICLR 2023
F IMPROVEMENT MEASURES
Figure 12 shows the Levenshtein distance difference (lev(Cpp C+) lev(Cr. C+)) between faulty input circuit and prediction. A value below zero implies syntactic improvement towards the target circuit. Figure 13 shows the number of satisfied sub-specifications. The more sub-specifications circuit satisfies, the closer semantically is correct circuit.
Violated
Satisfied
-60
-40
-20
20
40
Levenshtein distance improvement unrealizable
realizable
Figure 12: Violin plot of the improvement the Levenshtein distance from the repair circuit and prediction the target. The dashed line shows the mean of the displayed distribution.
Violated
Satisfied
0
10
Figure 13: Violin plot of the difference between the number of sub-specs that satisfied by the faulty input circuit vs. the predicted circuit. The larger the number the larger the improvement. In- side the violin plot is box plot with the dashed line showing the mean of the displayed distribution. Only realizable samples.
17

---

Published as a conference paper at ICLR 2023
G ARBITER
Here, we repeat the arbiter from Figure | graph representation.
with the AIGER format for all circuits on the left of each
aag
10
input
4
imput (r_2)
input (r_0)
8
imput (r.3)
93
9o
91
92
10
input 4 1)
12
18
latch
14
16
latch 1 (11)
output (g.3)
16
20
18
18
output 1 (g.2)
output 2 (g_0)
20
output 3
0
output 4 (o4)
14
12
16
15
13
and-gates
18
14
13
and-gates
and-gates
(a) Faulty circuit. Predicted in the base model (iteration 0).
aag
2
input 0 (i0)
input (r_2)
input 2 (r_0)
8
imput (r.3)
10
input (r_l)
12
13
latch 0 (10)
22
go
22
16
output 0 (g. 3)
18
output (g.2)
18
output 2
20
outpul 3 (g.1)
16
18
20
10
0
output 4 (o4)
16
15
13
and-gates
and-gates
20
14
13
and-gates
14
12
19
17
and-gates
(b) Faulty circuit. Predicted in iteration of the repair model.
aag
input (10)
11
input
6
input 2 (r_0)
input
10
imput 4 (t_1)
latch (10)
21
14
24
latch I (11)
16
output 0 (g.3)
18
output
20
output 2 (g-0)
output (g-1)
18
16
22
20
0
output 4 (o4)
16
and-gates
18
15
12
and-gates
20
14
13
and-gates
22
12
and-gates
24
23
17
and-gates
(c) Correct circuit. Predicted iteration of repair model.
Figure 14: Failed attempt of synthesizing arbiter and successful repair.
18

---

Published as a conference paper at ICLR 2023
H SCALING PARAMETERS
In this experiment, we scaled the synthesis model (Schmitt et al., 2021b) to match or exceed the number of parameters of our model. This shows that the increased number of parameters of the separated hierarchical Transformer is not the reason for the overall increase in performance. The detailed results are shown in Table
Table 2: Comparison of model size and semantic accuracy between different configurations of the synthesis model and model.
model
parameter
sem acc. with beam size 16
synthesis model
14786372
77.1%
(baseline)
synthesis model:
17945412 (+21.4%)
46.3% (-30.8)
8 local layers
synthesis model:
17945412 (+21.4%)
46.5% 30.66)
8 global layers
synthesis model:
17945412 (+21.4%)
58.2% (- (-18.9)
6 encoder layers pagtee
synthesis model:
16887620 (+14.2%)
77.4% (+0.3)
network size of 2048 (local layers) wow.eaaangggna....
synthesis model:
16887620 (+14.2%)
77.2% (+0.1)
network size of 2048 (global layers) synthesis model:
18988868 (+28.4%)
77.3% (+0.2)
network size of 2048 (encoder) repair model (ours)
17962820
(+21.5%)
83.9% (+6.8)
I HYPERPARAMETER STUDY
We trained several versions of model the presented dataset hyperparameter study shown in Table
96)
J ABLATIONS
Figure 15 shows the semantic accuracy of an evaluation of the pipeline with a beam size of 16. If sample has been solved correctly will counted as correct for all further iterations. We show the results of the model presented in this paper repp-rrepirgger 96-0 (blue) and two further mod- els. The model exp-repa a-aater-- 9--0 (green) shows a model trained on dataset that solely based on Section 3.2 Model exp-repa -erepparrreenn0---- and
(red and blue) are the two best performing models and trained on mixture of Section 3.2 and For insights into the datasets, see Figure
Section 3.2
19

---

Published as a conference paper at ICLR 2023
Table Hyperparameter study. Each column represents a model. The first column shows the final hyperparameters. Grey values of hyperparameters do not differ from the first column. Bold values of results show the best value in this row.
parameters
embedding size
256
256
256
256
256
256
128
256
256
network sizes
1024
1024
1024
1024
256
512
1024
1024
256
encoder
heads global
4
4
4
heads spec
4
4
4
4
4
4
4
heads circuit
4
4
4
4
4
layers global
4
4
4
4
4
4
8
layers spec
4
4
layers circuit
4
6
4
4
4
4
8
8
decoder
heads
4
4
4
4
4
4
4
layers
8
6
10
8
8
results
training split loss
0.03
0.05
0.03
0.04
0.04
0.04
0.04
0.06
0.08
accuracy
0.97
0.95
0.97
0.97
0.96
0.96
0.96
0.94
0.92
(per sequence)
0.47
0.40
0.44
0.43
0.39
0.42
0.42
0.32
0.24
validation split
loss
0.06
0.13
0.07
0.06
0.07
0.06
0.07
0.14
0.14
accuracy
0.95
0.91
0.95
0.95
0.95
0.95
0.95
0.89
0.88
(per sequence)
0.32
0.27
0.30
0.30
0.29
0.30
0.30
0.22
0.19
beam size
0.59
0.54
0.58
0.58
0.53
0.57
0.53
0.47
0.42
beam size
0.82
0.77
0.81
0.82
0.80
0.82
0.81
0.73
0.69
test split
beam size
0.58
0.52
0.59
0.57
0.56
0.58
0.59
0.44
0.41
beam size 16
0.85
0.77
0.85
0.82
0.83
0.82
0.81
0.72
0.70
20

---

Published as a conference paper at ICLR 2023
0.84
0.838
0.838
0,839
0.835
0.836
0.836
0.837
0.833
0.82
9224
accuracy
0.811
0.812
0.807
0.8
4297
0.78
0.721
model
repuir model
repair model
repair model
repair model
repair
iterations
exp-repair-gen gen-96-0
exp-repair geapairr-gee--ae 108-0 - exp-repair-atee- 19-0
Figure 15: Accuracy after each iterative step of the pipeline (aggregated).
In Figure T6 we display all models that were trained on different datasets. For all training, we used the same hyperparameters. We plot the accuracy improvement in the pipeline, hence the perfor- mance on the reactive synthesis task on the y-axis. On the x-axis, we depict the validation accuracy, hence the performance on the circuit repair problem. Further, the pipeline accuracy improvement based on the same distribution for all models, while the validation accuracy is based on the respec- tive datasets used for training the model. We can see that models having a higher pipeline accuracy trained with dataset that included evaluation results (Section (.2) instead of altered circuits (Section 3.2). This is not surprising, as these datasets are closer to the distribution, on which the pipeline accuracy is based. We can identify several clusters of models, of which one cluster (yellow) has relatively good validation accuracy and very good pipeline accuracy improvement. All models in this cluster improve the synthesis accuracy by more than percentage points, with the highest gain of 6.8 percentage points by the model exp-repair-gen-966.
Zen 96
gem: 108
pipeline accuracy improvement
pen- 37-0
gen 90.0
Reb-55 52-0
pon-18-0
gon-
ges-2.0
46-0
gen-45-0
ge0-15-0
77-077-0
gon-5-0
pmm-98-0
gen- 102-0
gen 35-0 0
gon-75-0
pen-84-0
gen-76-D
alter 1-0
gen 79 0
gen 32-0
0.02
alter-21-0
0.65
0.7
0.75
0.8
validation accuracy
Figure 16: Pipeline accuracy improvement (percentage points) compared validation accuracy of all trained models. Colors are based on k-means clustering with 4 clusters.
21

---

Published as a conference paper at ICLR 2023
In Figure 17 plot the mean and median of the Levenshtein distance between the faulty circuit and the target circuit for all models we trained. In the Figure 17a the plot is dependent on the validation accuracy (the accuracy of the repair problem) and in Figure 17b the plot is dependent on the pipeline accuracy improvement (performance on the synthesis task).
1.5
Or Ci www.ettt-aoaaaoooooo dio
F1 poat speda dape
O'EE www.-nmbeeeee..oo....ooooo thdba
Disprtatt www.aaoooaaaa.....oooo thoaaahh
0.5
0.65
0.7
0.75
0.8
0.85
0.9
validation accuracy
mean
trendline mean
median
trendline median
Validation accuracy (bs 16)
1.5
exp rppop abar
Coe Careeraae yonn 33.00
csp-a1ppen 19-0
Ord soot uedd doa
Fyg--ood spodo tha
0-911 wodk-unn www.-nnnooo-aaa
O-30 0od sopddd -di
On alte-
0.5
06
0.02
0.03
0.04
0.05
0.06
0.07
pipeline accuracy improvement
trendline mean
median
trendline median
(b) Pipeline accuracy improvement
Figure 17: Validation accuracy and pipeline accuracy improvement of all trained models compared to the Levenshtein distance between faulty circuit and target circuit. Mean and median are scaled from smallest and largest values to 0 and 1. Only the labels of selected models are shown.
K SCALED DOT PRODUCT ATTENTION
For set of queries, keys and values packed into the matrices Q (queries), (keys) and V (values), the scaled dot product attention Vasswan et al. 2017) is defined as:
QKT
Attention( Q2, K, V) softmax
V
Van
22

---

Published as a conference paper at ICLR 2023
L REPAIRING CIRCUITS FROM PARTIAL SPECIFICATIONS
To show the widespread applicability of our approach, we conduct another experiment. With classical synthesis tool, we generated where we removed the last one or two guarantees compared to the original spec. This method ensures that only 7.8% of these circuits still satisfy the original specification. We evaluated (not trained) our model on these out-of-din of-distribuution circuits and achieved 71.4% semantic accuracy after up iterations (see Table
set of potentially faulty circuits from specifications
We further looked into the status of the samples broken down by (original) specification size and target size (see Figures [8 and 19). While overall results demonstrate successful application of our model to this problem, it is noticeable that the model produces more syntax errors, most notably larger circuits and specifications. Especially compared to Figures [0 and IT], where the model did not produce any circuits with syntax errors. This is most likely because the defective circuits in this test are out-of out-of- -istibtiibuti.n.
100
samples (%)
50
20
40
80
100
120
140
160
Semantic Accuracy (smoothed)
error
violated (copy)
violated match
satisfied
Figure 18: Accuracies and sample status broken down by the size of the specification AST. Evalua- tion on faulty circuits from partial specifications.
100
Samples (%)
50
5
10
1.5
20
25
Semantic Accuracy (smoothed)
violated (copy)
violated
satisfied
match
Accuracies and sample status broken down by the size of the target circuit. Evaluation Figure 19:
on faulty circuits from partial specifications.
Table 4: Results on repairing faulty circuits generated with partial specifications. Table
(Extension to
synthesis model
after first iteration
after up to v iterations
partial
64.2%
71.4% (+7.2)
5
23


Reviews:
[{"review_id": "xiRw8nfxeN", "reviewer": "Reviewer_NdwS", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "This paper proposes using a neural network to iteratively repair sequential circuits represented as And Inverter Graphs (AIGs) against temporal logic specifications. The architecture is a variation of a transformed that separately takes as input the circuit and the specification. The specification is also separated into its assumptions and its guarantees. The network is then trained by (i) sampling circuits and specifications from well established benchmarks (ii) randomly introducing errors by changing the textual representation of the AIG.\n\nEmpirical results suggest that this technique is indeed able to correct incorrectly synthesized specifications and that repeated applications further improve performance. Importantly this can be used in combination with neural network based synthesis of the initial circuit.", "summary_of_the_review": "Overall, I believe the future potential of the propose method out weight the clear limitations on scale and questionable motivation for the error insertion. Circuit repair (and circuit synthesis) are computationally difficult problems in general and the field largely relies on hand tuned heuristics. Supporting data-driven techniques is a natural means to accelerate synthesis in specific target domains.", "strength_and_weaknesses": "# Strengths\n1. The problem considered is a very important and difficult problem with a wide range of applications. Further, neural approaches make sense since in practice scalable synthesis in electronic design automation involves specializing the synthesis software by hand.\n\n2. The technique empirically improves synthesis on established benchmarks. This is measured as Levenshtein distance in the AIGER format which intuitively captures a degree of close-ness.\n\n# Weakness\n\n1. The technique seems to be limited to incredibly small circuits.\n    - To give context, the upper limit on 61 symbols is easily exceed by small adders (a naive adder using the popular py-aiger tool uses 65 symbols.)\n\n2. Unconvinced by human generated error argument.\n   - Having worked with AIGER a fair amount, most large circuits I create are done using tools (e.g., py-aiger) and not by hand. Thus, the argument that the introduced errors are natural seems odd.\n   - A more common setting is that the specification (or unit tests) used when designing the circuit were slightly wrong, either because:\n     1) It was missing assumptions.\n     2) It was missing guarantees.\n     3) Used bounded time horizon reasoning.\n   - I would be much more interested in a neural repair that could fix this more common class of errors.\n\n3. Perhaps I missed something, but there seems to be a missing comparison with non-neural techniques. As the authors point out, this is a very mature field, so it would be have been nice to see a detailed comparison.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "txJbBcecY30", "reviewer": "Reviewer_Y3T4", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "Given a formal specification in LTL, this paper introduces a transformer architecture that aims to transform a defective circuit into a repaired one, in accordance to the spec.   The primary contribution is in the transformer neural architecture, which they call the separated hierarchical transformer since it has separate local layers that do not share model parameters. \n\nIn addition, they introduce a data generation procedure that models human errors to encourage generalization to more complex specifications.", "summary_of_the_review": "- Well written paper with comprehensive experimental analysis\n- Limited novelty\n- Would like to see much more evidence that claimed contributions are responsible for improved performance", "strength_and_weaknesses": "### Main strengths:\n\n- Well motivated problem\n- Mostly well written and easy to follow\n- Comprehensive experimental analysis (with some caveats)\n\n### Main weaknesses:\n\n- Most of the value of this contribution rests upon whether the following causal claims are true and well-justified: the new architecture and/or the data-augmentation procedure caused the improvements in performance of state of the art.  Despite a number of different experimental analyses in the paper, determining this is not straightforward.  In particular, I cannot see where if anywhere the number of parameters are controlled for.  The paper does say that using separated heads leads to an increase in the number of parameters, but I do not see any evidence in this paper to suggest that performance increases over previous methods is not attributed simply to this network being larger.  Also, the experimental results do not allow us to distinguish whether improvements are from the model changes or from the data changes.\n- I have some reservations about the use of Levenshtein distance as a metric for the quality of a synthesized circuit.  Obviously there is no “right” metric, and Levenshtein may be used in prior work, but a more semantic property could be used in addition to convey improvement.  For instance, one could try to look at (some approximation of) the increase or decrease in the number of satisfying traces", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "n7IFgPumQD", "reviewer": "Reviewer_LxSj", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "The paper investigates the application of transformer models to repairing circuits given formal specifications. The transformer takes a faulty circuit represented in AIGER format and a specification in LTL, and outputs a circuit that hopefully satisfies the specification. The paper also comes with a detailed description of the generation process of datasets.", "summary_of_the_review": "The framework is well-designed and the performance looks good. I lean toward accepting the paper.", "strength_and_weaknesses": "Strength:\n\n+ The approach is technically sound. While there have been a variety of work on generating logical formulas, formal specifications, or formal proofs with language models these days, the problem this paper is targeting (with language models) looks novel to me.\n\n+ The empirical evaluation is extensive, and validates the proposed framework. The difficulty measures and Levenshtein distance help better understand the capability of language models on the task.\n\nWeakness:\n\n- The specifications are restricted to 5 inputs and 5 outputs, no more than 12 properties. Did you observe a degradation in performance as the size of specifications increases?\n\n- What are the advantages of hierarchical transformers over vanilla ones? Although the experiments are extensive, I can't seem to find this particular dimension of evaluation. Also, would fine-tuning a pre-trained language model be as good as training a hierarchical transformer from scratch?", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "4B8y5lO9Vyk", "reviewer": "Reviewer_ocom", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "The paper extends hierarchical transformers (neural network models for\nsynthesising circuits from linear time specifications)  to build models  for\nthe repair of circuits so that they satisfy a certain linear time property. The\nmodels, which are also used in an iterative procedure to do reactive synthesis,\nare trained on a novel algorithm for introducing faults to a dataset.", "summary_of_the_review": "The paper introduces neural models for circuit synthesis which exhibit gains\nover the state-of-the-art, albeit being highly incremental to previous work.", "strength_and_weaknesses": "+ Good empirical analysis that shows the efficacy of the proposed method in\ncircuit repair and its superior performance in reactive synthesis when compared\nwith the state-of-the-art.\n\n- Highly incremental to previous work (the model proposed is a variation of the\n  work from Li et al. (2021) and the data generation algorithm is a standard\n  fault injection algorithm).\n\n- Some comparisons with related work are shallow. For instance, the\n  advantages/disadvantages of the present method to symbolic synthesis are not\n  discussed.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}]

Author rebuttal:

Decision: Accept: poster