Neural Model Checking
Authors: Mirco Giacobbe
Daniel Kroening
Abhinandan Pal
Michael Tautschnig
Venue: NeurIPS 2024 poster (2024)
Keywords: Formal Verification
SystemVerilog
Temporal Logic
Neuro-symbolic AI
Neural Certificates
Primary area: machine_learning_for_other_sciences_and_fields
TL;DR: Hardware model checking using neural certificates

Abstract: We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every execution of a given system satisfies a desired temporal logic specification. Unlike testing, model checking provides formal guarantees. Its application is expected standard in silicon design and the EDA industry has invested decades into the development of performant symbolic model checking algorithms. Our new approach combines machine learning and symbolic reasoning by using neural networks as formal proof certificates for linear temporal logic. We train our neural certificates from randomly generated executions of the system and we then symbolically check their validity using satisfiability solving which, upon the affirmative answer, establishes that the system provably satisfies the specification. We leverage the expressive power of neural networks to represent proof certificates as well as the fact that checking a certificate is much simpler than finding one. As a result, our machine learning procedure for model checking is entirely unsupervised, formally sound, and practically effective. We experimentally demonstrate that our method outperforms the state-of-the-art academic and commercial model checkers on a set of standard hardware designs written in SystemVerilog.

Neural Model Checking
Mirco Giacobbe"
Daniel Kroening"
University of Birmingham, UK
Amazon Web Services, USA
Abhinandan Pal" University of Birmingham, UK
Michael Tautschnig"
Amazon Web Services, USA and Queen Mary University of London, UK
Abstract
We introduce machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every execution given system satisfies a desired temporal logic specification. Unlike testing, model checking provides formal guarantees. Its application is expected standard in silicon design and the EDA industry has invested decades into the development of performant symbolic model checking algorithms. Our new approach combines machine learning and symbolic reasoning by using neural networks formal proof certificates for linear temporal logic. We train our neural certificates from randomly generated executions of the system and we then symbolically check their validity using satisfiability solving which, upon the affirmative answer, establishes that the system provably satisfies the specification. We leverage the expressive power of neural networks represent proof certificates as well as the fact that checking certificate is much simpler than finding one. As a result, our machine learning procedure for model checking entirely unsupervised, formally sound, and practically effective. We experimentally demonstrate that our method outperforms the sate-of-theearr academic and commercial model checkers on a set of standard hardware designs written in System Verilog.
Introduction
Electronic design is complex and prone to error. Hardware bugs are permanent after production and as such can irremediably affect the correctness of software- -oftware-which which runs on hardware and can compromise the safety of cyber-physical systems-which embed hardware. Correctness assurance is core to the engineering of digital circuitry, with the median FPGA and IC/ASIC projects spending respectively 40 % and 60 % of time in verification [48). Verification approaches based on directed
or constrained random testing are easy to set up but are inherently non-cxhaustive [89 91]. Testing cannot show the absence of bugs which, for systems the safety of which is critical, can have serious consequences; notably, over 40 % of hardware development projects must satisfy at least one functional safety standard [48] In contrast to testing, model checking design against formal specification correctness answers the question of whether the design satisfies the specification with mathematical certainty, for every possible execution of the system
13 35).
The EDA industry has heavily invested in software tools for symbolic model checking. Early symbolic model checking algorithms utilise fixed-poin computations with binary decision diagrams (BDDs) [7). where each node specifies the Boolean assignment for a circuit's flip-flop or input bit (26 45 BDDs struggle to scale when applied complex arithmetic data paths, prompting a shift towards iterative approximation of fixed points using propositional satisfiability (SAT) solving [16] 17 33), which
'The authors are listed alphabetically.
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

is now the oftte-of-the-arr technique. Both BDD and SAT-based model checking, despite extensive research, remain computationally demanding; even small circuit modules can require days to verify or may not complete at all. Consequently, verification engineers often limit state space exploration to a bounded time horizon through bounded model checking, sacrificing global correctness over the unbounded time domain.
We present machine learning approach hardware model checking that leverages neural networks to represent proof certificates for the compliance of a given hardware design with a given linear temporal logic (LTL) specification 82 Our approach avoids fixed-point algorithms entirely, capitalises on the efficient word-level reasoning of satisfiability solvers, and delivers a formal guarantee over an unbounded time horizon. Given hardware design and an LTL specification Φ, we train word- level neural certificate for the compliance of the design with the specification from test executions, which we then check using a satisfiability solver. We leverage the observation that checking a proof certificate is much simpler than solving the model checking problem directly, and that neural networks are an effective representation of proof certificates for the correctness of systems [2] 50 We ultimately obtain machine learning procedure for hardware model checking that is entirely unsupervised, formally sound and, as our experiments show, very effective in practice.
Our learn-and-check procedure begins by generating a synthetic dataset through random executions of the system alongside Büchi automaton that identifies counterexamples o. We then train a neural ranking function functtonunction designed to strictly decrease whenever the automaton encounters an accepting state and remain stable on non acccppinn states. After training, we formally check that the ranking function generalises to all possible executions. We frame the check as a cost-effective one-step bounded model checking problem involving the system, the automaton, and the quantised neural ranking function, which we delegate to a satisfibbility solver. As the ranking function cannot decrease indefinitely, this confirms that the automaton cannot accept any system execution, effectively proving that such executions are impossible. Hence, if the solver concludes that no counterexample exists, it demonstrates that no execution satisfies - thereby affirming that the system satisfies [37 95].
We have built prototype that integrates PyTorch, the bounded model checker EBMC. the LTL- to-automata translator Spot. the SystemVerilog simulator Verilator, and the satisfiability solver Bitwuzla 44 hardware model checking problems written in SystemVerilog and compared our results with the -fate-of-thh-ar academic hardware model checkers ABC and nuXmv [24 27), and two commercial counterparts. For any given time budget of less than hours, our method completes on average 60 % more tasks than ABC, 34% % more tasks than nuXmv, and 11 % more tasks than the leading commercial model checker. Our method faster than the academic tools on 67 % of the tasks, 10X faster on 34 %. and 100X faster on 4 %; when considering the leading commercial tool, our method is faster on 75 %, 10X faster on 29 %, and 100X faster on % of them. Overall, with a straightforward implementation,
76 80 88]. We have assessed the effectiveness of our method across 194 standard
method outperforms mature academic and commercial model checkers.
Our contribution is threefold. We present for the first time hardware model checking approach based on neural certificates. We extend neural ranking functions, previously introduced for the termination analysis of software, to LTL model checking and the verification of reactive systems. We have built a prototype and experimentally demonstrated that our approach compares favourably with the leading academic and commercial hardware model checkers. Our technology delivers formal guarantees of correctness and positively contributes to the safety assurance of systems.
Automata-theoreti Linear Temporal Logic Model Checking
An LTL model checking problem consists of a model M that describes a system design and an LTL formula & that describes the desired temporal behaviour of the system [52 82 The problem is to decide whether all traces of M satisfy 2.
Our formal model M of a hardware design consists of a finite set of bit-vector-typed variables XM with fixed bit-width and domain of assignments S, partitioned into input variables inp XMM S XM and state-holding register variables reg XM S X.M we interpret primed variables X'M M as the value of X M after one clock cycle. Then, a sequential update relation Updatem relates XMM and reg X'M and computes the next-state valuation of the registers from the current-state valuation of all variables; we interpret Updatem as first-order logic formula encoding this relation. state 8 E is a valuation for the variables XM. We denote as reg 8, inp 8, ... the restriction of to the respective
2

---

first con- reg XM
M
imp XM
clk
obs XM
0q
A_
(9
time
q
Figure 1: Automata-theoretic neural model checking via fair termination
class of variables. For two states s and s', the state s' is a successor of 8, which we write as 8 - s', if Update (s, reg s') evaluates to true. We call +M the transition relation of M and say that an infinite sequence of states 8o, 81, ...... is an execution of M if 8; - 8,41 for all 2 0; we say that an execution is initialised in so E S when 8g- 50-
We specify the intended behaviour of systems in LTL, which is the foundation of System Verilog Assertions. LTL extends propositional logic with temporal modalities X, G, F, and U. The modality p indicates that 1 holds immediately after one step in the future, G o indicates that d1 holds at all times in the future, F 4, indicates that 4, holds some time in the future, and $ U Φ2 indicates that i holds at all times until 4 holds at some time in the future. We refer the reader to the literature for the formal syntax and semantics of LTL 32 The atomic propositions of the LTL formulae we consider are Boolean variables of M, which we call the observables obs XM S XM of M. We note that any first-order predicate over X M can be bound to Boolean observable using combinational logic (cf. Figure 4 where observable ful corresponds to predicate cnt == 7).
We call trace of M sequence obs $p. obs $1, obs $ ... where So $1, $2.... is an execution of M. We define the language LM of .M as the maximal set of traces of M. Every LTL formula is interpreted over traces and such defines the language Lg of traces that satisfy b. The model checking problem corresponds to deciding the language inclusion question LM C L..
As is standard in automata-theoretic model checking, we rely on the result that every LTL. formula admits a -eneeeermiiiiti Büchi automaton that recognises the same language [95] 96). non- deterministic Büchi automaton A consists of finite set of states Q, an initial start state go E Q, an input domain Σ (also called alphabet), a transition relation 8 C Q Σ x Q, and a set fair states F Q. One can interpret automaton A as hardware design with one register variable reg XA* = {q} having domain Q, input and observable variables inp X = obs XA having domain E, and sequential update relation ( 9. q') (q. a. ,4)) E governing the automaton state transitions. We say that an execution A fair (also said to be an accepting execution) if it visits fair states infinitely often. We define the fair language L of A as the maximal set of traces corresponding to fair executions initialised in go- Given any I.TI. formula + there are translation algorithms and tools to construct non-deterministic Büchi automata As such that Ae L.
44
The standard approach to answer the language inclusion question LM S Lip is to answer the 13 35). For this purpose,
dual language emptiness question LM n L-P struct a non-deterministic Büchi automaton A_ for the complement specification -Q where inp X obs XMM then we reason over the synchronous composition (over a shared clock) of M and A-a as illustrated in Figure T.. We direct the reader to the relevant literature for general definitions of system composition [10]. In this context, the synchronous composition re- sults in the system M A with input variables inp XMIIA_ = inp XM- register variables reg XMIIA = reg XM U {q}. observable variables obs X = obs XMM and sequential up- date relation Update MIlA- (s, g. (') = Update,y r') Update (obs s, q, d'). We extend the fair states of A. to M .., i.e., we define them as ((s, E S.q E F), and result we have that LMMJA LM n -i LL LunLo This reduces our language emptiness question to the equivalent fair emptiness problem M = 0.
3

---

D
M A
Learn
V,0
Check
v.0 valid!
D + DU [cex]
Figure 2: Learn-and-check workflow for provably sound neural ranking function learning
The fair emptiness problem amounts to showing that all executions of M A-a are unfair, and we do so by presenting ranking function that witnesses fair termination [5] 67 A ranking function for fair termination is map V: reg S x Q - R where (R, -) defines well-founded relation and, for all system and automaton states 8, 8' E S. q. q' E Q, the following two conditions hold true:
(8, 9) MIIA (8', 9) = V(reg 8, q) 2 (regs',.4
(s, - MIILA-S (8', A = V(reg 8, q) > ((regs''g"
A ranking function V strictly decreases every time transition from fair state is taken, and never increases in any other case. Since every strictly decreasing sequence must be bounded from below (well-foundedness)) every fair state can be visited at most finitely many times; the intuition is presented in Figure J. where [q) denotes the indicator function of F, returning if q E F and otherwise. The existence of valid ranking function represented in some form establishes that every execution of M || A is necessarily unfair [95]. In this work, we represent ranking functions as neural networks, the parameters of which train from generated sample executions.
3 Neural Ranking Functions for Fair Termination
We approach the problem of computing ranking function for fair termination by training a neural network V: R" θ + R. with n input neurons where n rreg XM is the number of register variables of the system, one output neuron, and with a space of learnable parameters θ for its weights and biases. We associate distinct trainable parameter 0g O to each state q E Q of the Büchi automaton. We train these parameters on sampled executions of M A- to ultimately represent a ranking function as neural network (rr, 9) = V (r; 0g), which we call a neural ranking function. This scheme is illustrated in Figure | where we denote the set of all parameters by the unindexed 0.
We define training objective fulfilling conditions
and (2) on our synthetic dataset of sampled executions which, by analogy with reinforcement learning, can be viewed as a special case of episodes [53] (55. Subsequently, we verify the conditions symbolically over the full state space x Q using satisfiability solving modulo theories (SMT) [4 60). to confirm the validity of our neural ranking function obtain counterexample for re-training. Overall, our approach combines learning and SMT-based checking for both efficacy and formal soundness, as illustrated in Figure 2
For system M and specification 4 train the parameters 0 of neural network V from a sample dataset C reg S X'Q Q x reg S SxQ of subsequent transition pairs, which we construct from random ex- ecutions of the synchronous composition M || A-... Each execution (So, Qo), (81, 4 Qi)..... (8x, @s) initiates from a random system and automaton state pair and is then simulated over finite number of steps; the inputs to M and the -enddmteriiiistic choices in A- dataset is constructed as the set all quadruples (reg &,, q,, reg 8;+1, q++1) for i = O,..., k 1 from all sampled executions, capturing consecutive state pairs along each exccution; notably, the order in which quadruples are stored D is immaterial for our purpose, as our method reasons and trains locally each transition pair regardless of their order of appearance along any execution.
resolved randomly. Our
We train the parameters of our neural network to satisfy the ranking function conditions ① and (2) over D. For each quadruple (r, q, r' g') E D, this amounts to minimising the following loss function:
LRank(r: (r,, q,r,, 0):0) (VL'(V(r':
V(: 0g) + lg()))
where e > 0 is a hyper- that denotes the margin for the decrease condition. When CRank takes its minimum value-which is zero then the following two cases are satisfied: if q & F, then V does not increase along the given transition, i.e., V(r; 0g) 2 V(r': ) which corresponds to satisfy condition (T); if otherwise q E F, then V decreases by at least the margin > along the given transition, i.c., ((r: 0g) 2 V(r: 0gr) which corresponds to satisfy condition 2

---

Clamp
Clamp
Clamp
V
Norm.
Trainable parameters 0g
Figure 3: Neural ranking function architecture
Overall, our learning phase ensures that the total loss function C();0) below takes value zero:
(D) ('r.a.r'.'"' DD q, r 4):
Unlike many other machine learning applications, for our purpose is essential attain the global minimum; if this fails, there are counterexamples to V being ranking function in the dataset D itself. To facilitate the optimisation process, we train the parameters associated to each automaton state independently, one after the other, as opposed to training all parameters at once. Iteratively, we select one automaton state q E Q and optimise only 0g E for a number of steps, while keeping all other parameters fy ( fixed to their current value, for all # q. We repeat the process over each automaton state, possibly iterating over the entire set of automaton states Q multiple times, until the total loss L(D; 8) takes value zero.
Our neural network V follows werdard architecture as depicted in Figure for given automaton state Q and associated parameter 4g. it takes an n-dimensional input IR" where each input neuron corresponds to the value of a register variable reg X M. and produces one output for the corresponding ranking value (r; 02). Our architecture consists of normalisation layer, followed by an element-wis wise multiplication layer, turn followed by multi-layer perceptron with clamped ReLU activation functions. The first layer applies scaling factor to each input neuron independently to ensure consistent value ranges across inputs, implemented via element-wiss multiplication with constant vector of scaling coefficients derived from the dataset D before training; this integrates data normalisation into the network, enables V to use raw data from M and simplifies the symbolic encoding of the normalisation operation during the verification phase. The second layer applies a trainable scaling factor to each individual neuron and is implemented via element- wise multiplication with n--dimensional vector with trainable coefficients. Finally, this is followed by fully connected multi-layer perceptron with trainable weights and biases, with the activation function defined as the element-wise application of Clamp( u) max (0, min(x, u)); the upper bound w and the depth and width of the hidden layers of the multi-layer perceptron component are hyper-parameters chosen optimise training and verification performance.
Attaining zero total loss L(D;0) guarantees that our neural ranking function candidate V satisfies the ranking criteria for fair termination over the dataset D but not necessarily over the entire transition relation - M as required to fulfil conditions IT] and ( and consequently to answer our model checking question (cf. Section 2). To formally check whether the ranking criteria satisfied over the entire transition relation, we couple our learning procedure with a sound decision procedure that verifies their validity, illustrated in Figure 2
We check the validity of our candidate ranking neural network using satisfiability modulo the theory of bit-vectors. While the sequential update relation Update Am.. is natively expressed over the
theory of bit-vectors, the formal semantics of the neural network V is defined on the reals. Hence, encoding V and Update, AI within the same query would result in a combination of real and bit-vector theories, which is supported in modern SMT solvers but often leads to sub-optimal performance [60]. Therefore, to leverage the efficacy of specialised solvers for the theory of bit- vectors 80 we quantise our neural network using standard approach for this purpose [57]] this converts all arithmetic operations within the neural networks into fixed-point arithmetic, which are implemented using integer arithmetic only. We quantise our parameters to their respective integer representation 0 ~ 2 0, where is hyper-parameter for the number of fractional digits in fixed-point representation, and we replace línear layers and activation functions by their quantised counterpart; readers may consult the relevant literature for more detailed information neural
5

---

modula BufferOtr (input clk, output reg ful, emp, rw); reg [2:0] cat;
dul
8 + Clamp( 14n 2cnt; 16]+
reg m;
true
tul
Clamp(cnt; 15) Clamp(11n; 15)
assign ful (ent == 7);
aasign eup
0);
assign
(n 111 !ful);
14 90
alvaya a(posedge c1x) begin
(n
emp)
eep
Clampp(14 2ent; 15)+ Clamp(ent; 15)
10
if (n -- 1 ful) n <- 0; (rv) cat cat 1; else cnt < cnt
12
13
end endmodule
14
Figure 4: Illustrative hardware design, Büchi automaton, and respective ranking function
network quantisation 49 57
This results in a quantised neural network V 2" x θ that approximates our trained network V 2/ V. where é denotes the space of integer parameters.
fractional digits introduced by the linear layers 49 57 candidate proof certificate for fair termination.
We consider the quantised network V as our
We reduce the validity query whether our quantised neural network V satisfies the ranking criteria for fair termination ( and over the entire transition relation of .M || A the dual satisfi- ability query for the existence of a counterexample to the criteria. Specifically, we delegate to an fff-the-shelf SMT solver the task of computing satisfying assignment S, reg S for which the following quantifier-fre first-order logie formula satisfied:
V
Update (s, q,r', .') Viee s; 0,) 11(()) (():
(5)
9-0'E0 EQ
where θ is the (constant) parameter resulting from training and quantisation. We encode the quantised neural network using a standard translation into first-order logic over the theory of bit-vectors 44), supplementing with specialised rewriting rules enhance the solver's performance, as detailed in Appendix A We additionally note that V guaranteed to bounded from below as is finite, albeit potentially very large, i.e., exponential in the combined bit-width of XM-
If the solver finds satisfying assignment, then the assignment represents a transition of M that refutes the validity of V; in this case, extend it to respective transition in M A add it to our dataset D and repeat training and verification in a loop. Conversely, if the solver determines that formula (5) is unsatisfiable, then our procedure concludes that V is formally a valid neural ranking function and, consequently, system M satisfies specification 4
note that LTL model checking of hardware designs decidable and PSPACE-complete 13 While it is theoretically possible for approach achieve completeness when ranking function exists by enumerating all transitions and employing a sufficiently large neural network as a lookup table over the entire state space, this is impractical for all but toy cases. In this work, employ tiny neural networks and incomplete but practically effective gradient descent algorithms to train neural ranking funetions. We experimentally demonstrate large set of formal hardware verification benchmarks that this solution is very effective practice.
Illustrative Example
Modern hardware designs frequently incorporate word-level arithmetic operations, the simplest of which being counter increments/dderrmeents which are a staple in hardware engineering [71 (8]. One such example is illustrated as part of the SystemVerilgy module in Figure This represents a simplified buffer controller that counts the number of packets stored in the buffer and indicates when the buffer is full or empty with the ful and emp signals, respectively. This specific controller internally coordinates read-and-write operations through the rw signal: iteratively, the system signals r== until the buffer is full and then O until the buffer is empty.
The design satisfies the property that both our observables ful and emp are true infinitely often, captured by the LTL formula & fFlul/ A GF emp. Dually, this specification says that the system

---

does not eventually go into a state from where -ful holds indefinitely nor emp holds indefinitely. that is, - FG -ful v FG emmp. Equivalently, this amounts proving that no system trace is in the fair language of the automaton A given in Figure 4
A neural ranking function V for the fair termination of this system and automaton has input neurons for the register variables cnt, m, ful, emp, and rw, and one hidden layer with three neurons in the multi-layer perceptron component. As illustrated in Figure each automaton state is associated with a ranking function defined in terms of this architecture and their respective parameters. The sequence below gives an execution of model states alongside the respective ranking function values:
emp
ful
emp
ful
cnt
0
2
3
4
5
6
5
4
3
2
0
2
3
4
5
0
0
0
0
rw
1
1
1
1
1
0
0
0
0
0
0
0
1
1
1
1
14
14
14
14
14
14
14
14
14
14
14
8
7
6
5
4
3
2
14
13
12
11
10
9
8
7
6
5
4
3
(()
14
13
12
11
10
9
3
2
1
14
13
10
One can observe that all transitions throughout this execution satisfy conditions 11) and 2 This assessment is based on the (not explicitly presented) synchronous composition with the automaton. First, note that every transition originating from qo has non-increasing ranking value, as (=. = 14 an upper bound to all other values. Furthermore, every transition leaving Q q--that is, every transition whose source state satisfies -ful-xhibbits a strictly decreasing value V(;00,) Similarly, the same observation applies to q2 and the condition -mmp. We note that the transitions that exhibit increasing values from 1 to 14 this execution are impossible over the synchronous composition; this is because they originating from states that satisfy both ful and q1, and similarly states that satisfy both emp and Q2. and which do not have corresponding transitions in the automaton.
This neural ranking function admits no increasing transition originating from go and no non-decreasing transitions originating from qi or 92 on the synchronous composition of the system and the automaton. Therefore, it is a valid proof certificate for every system trace to satisfy specification tb
5
Experimental Evaluation
We examine 194 verification tasks derived from ten parameterised hardware designs, detailed in Appendix B By adjusting parameter values, we create tasks of varying complexity, resulting in different logic gate counts and state space sizes, thus offering a broad spectrum of verification complexity for tool comparison. The parameter ranges for each design given as "all tasks" in Figure 5 These tasks serve as benchmarks to evaluate the scalability of our method relative to conventional model checking.
Implementation We have developed a prototype tool for neural model checking utilising Spot 2.11.6 [44] to generate the automaton A-4 from LTL specification 4. As depicted in Figure] [ the circuit model M and the automaton A- synchronise over a shared clock to form a product machine. Using Verilator version 5.022 88 we generate dataset D from finite trajectories of this machine. This dataset trains a neural network using PyTorch 2.2.2, as outlined in Section 3 To ensure formal guarantees, the network is quantised and subsequently translated SMT, following the process outlined in Appendix A The System Verilog model is converted to SMT using EBMC 5.2 (76). We check the satisfiability problem using the Bitwuzla 0.6.0 SMT solver 88
State of the Art We benchmarked our neural model checking approach against two leading model checkers, nuXmv (27 and ABC 24 25). ABC and nuXmv the top performers in the liveness category of the hardware model checking competition (HWMCC) [55 19]. Our comparison employed the latest versions: nuXmv 2.0.0 and ABC's Super Prove tool suite (25), which were also used in the
most recent HWMCC'20 15). We further consider two widely used industrial formal verification tools for System Verilog, anonymised industry tool X and industry tool Tool Y fails complete any of the 194 tasks and is therefore not referenced further in this section.

---

Table 1: Number of verification task completed by academic and industrial tool, per design
LS
LCD
Tmep
i2cS
7-Seg
PWM
VGA
UARTI
Delay
Gray
Total
Tasks
16
14
17
20
30
12
10
10
32
33
194
ABC
3
2
10
13
57
nuXmv
9
12
10
10
7
10
24
24
117
our
15
14
17
18
30
11
10
32
33
180
Ind. X
16
14
17
18
18
12
10
10
19
22
156
Ind.
0
0
0
0
0
ABC
ABC
10th
101".
lill
State Spase Stoe
Logic Count
Inll Lill
Inl
Lill
Intl
13
ltd
hid
324
Lall
LCO
Troop
1265
Fiee
VGA
Delay Giay
10b
Trop
1255
Plan
Delas
Grey
Figure 5: Solved tasks in terms of state space size and logic gate count (log scale)
Experimental Setup Evaluations were conducted on an Intel Xeon 2.5 GHz processor with eight threads and GB of RAM running Ubuntu 20.04. Bitwuzla and nuXmv utilise one core each, ABC used three cores, and PyTorch leveraged all available cores. Each tool was allotted a maximum of five hours for each verification task, as detailed in Appendix C
Hlyper-parameters We instantiate the architecture described in Section illustrated in Figure 3 employing two hidden layers containing and neurons. The normalisation layer scales the input values to the range [0, 100]. We train with the AdamW optimiser [70), typically setting the learning rate to 0.1 or selecting from 0.2, 0.05, 0.03, 0.01 if adjusted, with fixed weight decay of 0.01, demonstrating minimal hyperparameter tuning for training.
Dataset Generation In hardware design, engineers utilise test benches to verify safety properties through directed testing or Constraint Random Verification (CRV), aiming for high coverage and capturing edge cases [48 18). We apply CRV to the System Verilog file, generating random trajectories. start these trajectories by selecting the internal states of model M (e.g.. module BufferCtr and automaton A o: in Figure 4 assign random inputs to model M and handle the non-determinism in automaton A- by making choices from uniform or skewed distributions. We skew the distribution when particular event is predominant or rare. In our experiments, such skewing is rare and limited the reset and enable signals in M, as well as the non-determinism in the automaton A....
As outlined in Section
using a uniform distribution. At each step,
Solved Tasks Table presents the number of completed tasks for each tool across the ten hard- ware designs, while Figure shows the range of state-space sizes and logic gate counts each tool successfully handled. Overall, our tool performs favourably in comparison others, with the notable exception of the VGA design, where training a ranking function failed due to local minima, preventing convergence zero loss known limitation of gradient descent- based methods.
Aggregate Runtime Comparison Figure 6p displays a cactus plot with h limit, we consider our configuration with 8 and hidden neurons detailed in the section, along with the aggregate of the best time on individual tasks obtained from our ablation study, as detailed in Appendix D While the default architecture performs the best across all tasks, on some tasks smaller network is sufficient, and leads to lower verification time. At the same time, larger networks often succeed on tasks that otherwise fail, making the "our best" line strictly better than "our (5, 8)". This shows that improvement can be obtained by tuning the width of the hidden layers; note that this analysis considers three additional configurations (i.e, (3, 2), (5, 3). (15, 8)) that adhere to the architecture introduced in Section 3 For the rest of our experiments, continue using the default architecture

---

26
5t-
54
1h:
15m
Satt Space size
15m
Ohu time
time
Time
12:
3m
Lm
2m
15c
nukmm
ind
50
our (5.8)
our best
1X
10X
100X
Learning time
bhy
20%
40%
60%
80% 60%
Tacks complesed
muXani/ACCtin
Tasks completed
(a)
(b)
(c)
Figure 6: Runtime comparison with the state of the art (all times are in log scale)
The plot further shows that our tool completes 93 % of tasks, outperforming ABC, nuXmv, and industry tool X, which completes 29 %, 60 %, and 80 %, respectively. At any point in the time axis, we compute the difference between the percentage of tasks completed by our tool with each of the others in the figure. Then, taking the average of these differences across the time axis, showing that our method is successful in 60 % more tasks than ABC, 34 % more than nuXmy, and 11 % more than the leading commercial model checker any given time. Furthermore, the number of tasks completed by nuxmy in 5 h are finished by our tool in less than 8 min, and those completed by ABC in 5 h take just under 3 min with our method.
Individual Runtime Comparison Figure presents a scatter plot where each point represents verification task, with size and brightness indicating the state-space size. Points are plotted horizontally by the lesser of time taken by nuXmv or ABC and vertically by our method's time. The plot reveals that academic tools time out on 39 % of tasks, while our method times out on 7 %. Moreover, we are faster than the academic tools on 67 % of tasks, 10 times faster on 34 %, and 100 times faster 4 %. These results demonstrate that we generally outperform the state of the art on this benchmark set (see Appendix 3 for individual runtimes). However, we perform relatively worse on the UARTt design. This design involves an --bit register for data storage and a counter for transmitted bits, enabling sequential outputs. Since there is no word-level arithmetic over the N-bit register, increasing its size minimally affects the complexity of symbolic model checking. Consequently, ABC, nuXmv, and industry tool X complete all UARTt tasks in under a second, while our tool takes a few minutes due to overhead from the sampling, learning, and SMMT-heeck steps, making us slower on trivial model-checking problems.
Learning vs. Checking Time Figure 6 illustrates the time split between learning the neural network-which involves dataset generation and training-and verifying it as a valid ranking function. The lower line indicates learning time; the upper line represents total time, with the gap showing the time spent on SMT checking. Extensive sampling across broad range of trajectories covering most edge cases led our method to learn the network directly without needing retraining due to counterexamples in the SMT-check phase, except in four tasks. The plot shows that 93 % of tasks were trained successfully, generally within five minutes, and remarkably, the 70 % were completed in under a minute. For tasks that did not train to zero loss, the h time limit was not fully utilised; the loss function stabilised local minima in just few minutes. Moreover, training was faster than verification 97 % tasks- 10 times faster on 46 % and 100 times faster on 6 %.
Limitations The primary limitation of our approach arises from the extended SMT-check times and the risk of getting trapped in local minima. Despite these challenges, our method consistently outperforms traditional symbolic model checkers while relying on off-the-shelf SMT solvers and machine learning optimisers. Additionally, our neural architecture requires numerical inputs at the word level, which limits its application to bit-level netlists. This limitation is not high-impact, as modern formal verification tools predominantly utilise Verilog RTL rather than netlist representations.
Threats to Validity The experimental results may not generalise other workloads. As any work that relies on benchmarks, our benchmarks may not be representative for other workloads. We mitigate this threat by selecting extremely common hardware design patterns from the standard literature. We remark that our data sets we use to train the neural nets do not suffer from the common threat of training data bias, and the common duitt--disttibutionn problem: we train our neural net from scratch for each benchmark using randomly generated trajectories, and do not any pretraining.

---

6
Related Work
Formal verification, temporal logic and model checking have been developed for more than fifty years; key contributors have been recognised with the 1996, 2007 and 2013 ACM Turing Awards. Here, we restrict our discussion to algorithms that are the basis of the model checkers for System that available to hardware engineers today as well as on the techniques that underpin this work.
Temporal logic describes the intended behaviour of systems and System Assertions whhshh is
based on LTL-is a widely adopted language for this purpose [8] 82]. Any temporal specifications
are compositions of safety and liveness properties, where the former indicate the dangerous conditions
to be avoided and the latter indicate the desirable conditions to be attained [8] 65] Safety properties
are a fragment of LTL., and can be checked using BDDs by forward fixed- point iterations [12 [4 [2]
Bounded model checking uses SAT and scales much better than BDDs [16), but it is only complete when the bound reaches an often unrealistically large completeness threshold [59]. SAT-based
unbounded safety checking uses sophisticated Craig Interpolation and IC3 algorithms (20 73 87
Our work uses one-step bounded model checking query to check the ranking function (see Eq. ( and goes beyond safety. Liveness checking for branching- timee CTL is straightforward to implement using BDD-based fixed points [35] 45 Our method does not support CTL: this is considered acceptable given the prevailing use of LTL-based property languages in industry. LTL model checking is commonly reduced to the fair emptiness problem and, for this purpose, bounded model checking has been generalised to k-liveness [3 [56] IC3 has been augmented with strongly connected components [23], and BDD-based algorithms with the Emerson-Lei fixed-poin computation [23] [66. Iterative symbolic computation is the bottleneck systems with word-level arithmetic. This is
usually addressed by either computing succinet explicit-state abstractions of the system 66 32 or by
computing proof certificates based on inductive invariants and ranking functions.
Ranking functions were introduced for termination analysis of software [47), and subsequently generalised to liveness verification [5]
39 (7] (95). Software and hardware model checking
share common questions 42 76 77. Early symbolic approaches for software analysis based on
constraint solving are limited to linear ranking functions [21 (84. As we illustrate in Figure 4
even simple examples often require non-linear ranking functions. These include piecewise-defined
functions 663 93 94], word-level arithmetic functions 29
40). lexicographic ranking functions [22]
68 and disjoint well-founded relations
[36
38, 61
and similar proof certificates based on
liveesss-tossffet translation to reason about the transitive closure of the system [8
78 85
Our method follows a much more lightweight approach than the symbolic approaches above, by
training ranking functions from synthetic executions [81). Deep learning has been successfully applied to generate software and hardware designs, but without delivering any formal guarantees (30 69 74)
In our work, we use neural networks to represent formal proof certificates, rather than to generate proofs or designs. This goes along the lines of recent work on neural certificates, previously applied to control [
41 66 77 86 102), formal verification of software and probabilistic programs 3 and this work applies them for the first time to hardware model checking.
7 Conclusion
We have introduced a method that leverages (quantised) neural networks as representations of ranking functions for fair termination, which we train from synthetic executions of the system without using any external information other than the design at hand and its specification. We have applied our new method to model checking System Verilog Assertions and compared its performance with the state of the art on a range of DesteeVerrllg designs. We employed off-the-shelf SMT solving (Bitwuzla) and bounded model checking (EBMC) to formally verify neural ranking functions [76] 80]; although this phase takes the majority of our compute time, with a straightforward implementation and using tiny feed-forward neural networks, we obtained scalability superior to traditional symbolic model checking. Whether alternative neural architectures as well as specialised solvers for quantised neural networks can further improve approach is topic of future work [I] 64 72 75).
This is the first successful application of neural certificates to model checking temporal logic, and introduces hardware model checking a new application domain for this technology. Neural networks could be used in many other ways to improve model checking. Our work creates baseline for further development in this field and positively contributes to the safety assurance of systems.
10

---

Acknowledgements
We thank Matthew Leeke, Sonia Marin, and Mark Ryan for their feedback and the anonymous reviewers for their comments and suggestions on this manuscript. This work was supported in part by the Advanced Research Invention Agency (ARIA) under the Safeguarded Al programme.
References
[1] A. Abate, D. Ahmed, A. Edwards, M. Giacobbe, and A. Peruffo. FOSSIL: software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks, In HSCC, pages 24:1-24:11. ACM, 2021.
[2] A. Abate, D. Ahmed, M. Giacobbe, and A. Peruffo. Formal synthesis of Lyapunov neural networks. IEEE Control. Syst. Lett., 5(3):773-778, 2021.
[3] A. Abate, M. Giacobbe, and D. Roy. Learning probabilistic termination proofs. In CAV (2), volume 12760 of Lecture Notes in Computer Science, pages 3-26. Springer, 2021.
[4] A. Abate, A. Edwards, M. Giacobbe, H. Punchihewa, and D. Roy. Quantitative verification with neural networks. In CONCUR, volume 279 of LIPles, pages 22:1-22:18 18. Schloss Dagstuhl Leibniz-Zentrum für Informatik, 2023.
[5] A. Abate, M. Giacobbe, and D. Roy. Stochastic omega-regular verification and control with supernartingales. In CAV (3), volume 14683 of Lecture Notes in Computer Science, pages 395 499. Springer, 2024.
[6] Abate, M. Giacobbe, and Y. Schnitzer. Bisimulation learning. In CAV (3), volume 14683 of Lecture Notes in Computer Science, pages 161-183. Springer, 2024.
[7] S. B. Akers. Binary decision diagrams. IEEE Trans. Computers, 27(6):509-516, 1978.
[8] B. Alper and B. Schneider. Recognizing safety and liveness. Distributed Comput., 2(3):
1 117-126, 1987.
[9] R. Alur. Principles of Cyber-Physical Systems, MIT Press, 2015.
[10] R. Alur and T. A. Henzinger. Reactive modules. In LICS, pages 207-218. IEEE, 1996.
[11] G. Amir, H. Wu, C. W. Barrett, and G. Katz. An SMT-based approach for verifying binarized neural networks. In TACAS (2), volume 12652 Lecture Notes in Computer Science, pages 203-222. Springer, 2021.
[12] Z. S. Andraus, M. H. Liffiton, and K. A. Sakallah. Reveal: A formal verification tool for Verilog designs. In LPAR, volume 5330 of Lecture Notes in Computer Science, pages 343-352. Springer, 2008
[13] C. Baier and J. Katoen. Principles of Model Checking. MIT Press, 2008
[14] W. Barrett, Sehastiani, A. Seshia, and C. Tinelli. Satisfiability modulo theories. In Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 825 885. IOS Press, 2009.
[15] Biere, N. Froleyks, and M. Preiner. Hardware model checking competition (HWMCC) 2020.
10/2020/
[16] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS, volume 1579 of LNCS, pages 193-207. Springer, 1999.
[17] A. Biere, E. M. Clarke, R. Raimi, and Y. Zhu. Verifiying safety properties of Power PC microprocessor using symbolic model checking without BDDs. In CAV, volume 1633 of LNCS, pages 60-71. Springer, 1999.
[18] A. Biere, C. Artho, and V. Schuppan. Liveness checking safety checking. In FMICS, volume 66 of Electronic Notes in Theoretical Computer Science, pages 160-177. Elsevier, 2002.

---

[19] A. Biere, T. Van Dijk, and K. Heljanko. Hardware model checking competition 2017. In Formal Methods in Computer Aided Design (FMCAD), pages 9-9. IEEE. 2017.
[20] A. R. Bradley, SAT-based model checking without unrolling. In VMCAI, volume 6538 of Lecture Notes in Computer Science, pages 70-87. Springer, 2011.
[21] A. R. Bradley, Z. Manna, and H. B. Sipma. Linear ranking with reachability, In CAV, volume 3576 of Lecture Notes in Computer Science, pages 491-504. Springer, 2005.
[22] A. Bradley, Z. Manna, and
Sipma. The polyranking principle. ICALP, volume 3580 of Lecture Notes in Computer Science, pages 1349-1361 Springer, 2005.
[23] A. R. Bradley, Somenzi, Z. Hassan, and Zhang. An incremental approach to model checking progress properties. In FMCAD, pages 144-153. FMCAD Inc., 2011.
[24] R. K. Brayton and A. Mishchenko, ABC: academic industrial-street -trengthh verification tool. In CAV, volume 6174 of LNCS, pages 24 40. Springer, 2010.
[25] R. K. Brayton, B. Sterin, N. Een, S. Ray, J. Long, and A. Mishchenko. Model checking system URL https::/t////ttttt cow./stariineupeer-prrreee
"super_prove"
[26] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Inf. Comput., 14--17,, 1992.
[27] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta. The nuXmv symbolic model checker. In CAV, volume 8559 of LNCS, pages 334-342. Springer, 2014.
[28] Y. Chang, N. Roohi, and S. Gao. Neural Lyapunov Control. In NeurlPS, pages 3240-3249, 2019.
[29] H. Chen, C. David, D. Kroening, P. Schrammel, and B. Wachter. Bit-precise procelure-modular termination analysis. ACM Trans. Program. Lang. Syst. 40(1):1:1-1:38, 2018.
[30] M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. de Oliveira Pinto, J. Kaplan, H. Edwards, Y. Burda,
N. Joseph, G. Brockman, A. Ray, R. Puri, G. Krueger, M. Petrov, H. Khlaaf, G. Sastry,
P. Mishkin, B. Chan, S. Gray, N. Ryder, M. Pavlov, A. Power, L. Kaiser, M. Bavarian, C. Winter,
P. Tillet, F. Such, D. Cummings, M. Plappert, F. Chantzis, E. Barnes, A. Herbert- Voss, W. H. Guss, A. Nichol, A. Paino, N. Tezak, J. Tang, I. Babuschkin, S. Balaji, S. Jain, W. Saunders, C. Hesse, A. N. Carr, J. Leike, Achiam, V. Misra, E. Morikawa, A. Radford, M. Knight, M. Brundage, M. Murati, K. Mayer, P. Welinder, B. McGrew, D. Amodei, S. McCandlish, I. Sutskever, and W. Zaremba. Evaluating large language models trained on code. CoRR, abs/2107.03374, 2021.
[31] K. Claessen and N. Sörensson. A liveness checking algorithm that counts. In FMCAD, pages 52-59. IEEE, 2012.
[32] E. M. Clarke, O. Grumberg. S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV, volume 1855 of Lecture Notes in Computer Science, pages 154-169. Springer, 2000.
[33] E. M. Clarke, D. Kroening, and F. Lerda. tool for checking ANSI-C programs. TACAS, volume 2988 of LNCS, pages 168-176. Springer, 2004.
[34] E. M. Clarke, R. Kurshan, and H. Veith. The localization reduction and counterexample- guided abstraction refinement. In Essays in Memory of Amir Pnueli, volume 6200 of Lecture Notes in Computer Science, pages 61-71. Springer, 2010.
[35] E. M. Clarke, O. Grumberg, D. Kroening, D. A. Peled, and H. Veith. Model checking, 2nd Edition. MIT Press, 2018.
[36] Cook, A. Podelski, and Rybalchenko. Termination proofs for systems code. PLDI, pages 415-426. ACM, 2006.
12

---

[37] B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M. Y. Vardi. Proving that programs eventually do something good. In POPL, pages 265-276. ACM, 2007.
[38] Cook, A. See, and Zuleger. Ramsey vs, lexicographic termination proving. In TACAS, volume 7795 of Lecture Notes in Computer Science, pages 47-61. Springer, 2013.
[39] B. Cook, H. Khlaaf, and N. Piterman. Fairness for infinite-state systems. In TACAS, volume 9035 of Lecture Notes Computer Science, pages 384-398. Springer, 2015.
[40] C. David, D. Kroening, and M. Lewis. Unrestricted termination and temminmmintion arguments for bit-vector programs. In ESOP, volume 9032 of Lecture Notes in Computer Science, pages 183-204. Springer, 2015.
[41] C. Dawson, Z. Qin, S. Gao, and C. Fan. Safe nonlinear control using robust neural Lyapunov- barrier functions. In CoRL, volume 164 of Proceedings of Machine Learning Research, pages 1724-1735. PMLR, 2021.
[42] Dietsch, M. Heizmann, V. Langenfeld, and Podelski. Fairness modulo theory: A new approach to LTL software model checking. In CAV (I), volume 9206 of Lecture Notes in Computer Science, pages 49-66. Springer, 2015.
[43] Dimitrova, M. F. Fioriti, H. Hermanns, and R. Majumdar. Probabilistic CTL * The deductive way. In TACAS, volume 9636 of Lecture Notes in Computer Science, pages 280-296. Springer, 2016.
[44] A. Luret-Lutz, Renault, M. Colange, F. Renkin, A. G. Aisse, P. Schlehuber Caissieer T. Medioni, A. Martin, J. Dubois, C. Gillard, and H. Lauko. From Spot 2.0 to Spot 2.10: What's new? In CAV (2), volume 13372 of LNCS, pages 174-187. Springer, 2022.
[45] A. Emerson and E. M. Clarke. Characterizing correctness properties of parallel programs using fixpoints. In /CALP, volume 85 of LNCS, pages 169-181. Springer, 1980.
[46] E. A. Emerson and C. Lei. Modalities for model checking: Branching time strikes back. In POPL., pages 84-96. ACM Press, 1985.
[47] W. Floyd. Assigning meanings to programs. Proceedings of Symposium in Applied Ilathematic,, volume 19, pages 19-32, 1967.
[48] H. Foster.
The 2022 Wilson research group functional verification study, 2022. sw. http://www...s.oooooooooooooetts
URL
[49] M. Giacobbe, T. A. Henzinger, and M. Lechner. How many bits does it take to quantize your neural network? TACAS (2), volume 12079 of LNCS, pages 79-97. Springer, 2020.
[50] M. Giacobbe, D. Kroening, and J. Parsert. Neural termination analysis. ESEC/SIGSOFT FSE, pages 633-645. ACM, 2022.
[51] O. Grumberg, N. Francez, J. A. Makowsky, and W. P. de Roever. A proof rule for fair termination of guarded commands. Inf. Control., 66(1/2):83-102, 1985.
[52] Harel and Pnueli. On the development of reactive systems. Logics and Models of Concurrent Systems, volume 13 of NATO ASI Series, pages 477-498. Springer, 1984.
[53] H. Hasanbeig, D. Kroening, and A. Abate. Certified reinforcement learning with logic guidance. Artif. Intell., 022:103940 2023.
[54] D. G. Holmes and A. Lipo. Pulse width modulation for power converters: principles and practice, volume 18. John Wiley & Sons, 2003.
[55] R. T. Icarte, T. Q. Klassen, R. A. Valenzano, and S. A. Mcllraith. Reward machines: Exploiting reward function structure in reinforcement learning. J. Artif. Intell. Res., 73:173-208, 2022.
[56] Ivrii, Z. Nevo, and J. Baumgartner. k-FAIR K-LIVENESS + FAIR- revisiivv SAT-based liveness algorithms. In FMCAD, pages 1-5. IEEE, 2018.
13

---

[57] B. Jacob, S. Kligys, B. Chen, M. Zhu, M. Tang, A. G. Howard. H. Adam, and D. Kalenichenko. Quantization and training neural networks for efficient pnnger-arithmetic-nnl, inference. In CVPR, pages 2704-2713 13. Computer Vision Foundation IEEE Computer Society, 2018.
[58] J. Kretínsky, T. Meggendorfer, and S. Sickert. Owl: A library for w-words, automata, and LTL. ATVA, volume 11138 of Lecture Notes in Computer Science, pages 543-550, Springer, 2018.
[59] D. Kroening and O. Strichman. Efficient computation of recurrence diameters. In VMCAI, volume 2575 of Lecture Notes in Computer Science, pages 298-309. Springer, 2003.
[60] D. Kroening and O. Strichman. Decision Procedures-Ae An Algorithmic Point of View, Second Edition. Texts in Theoretical Computer Science. Springer, 2016.
[61] Kroening, N. Sharygina, A. Tsitovich, and C. M. Wintersteiger. Termination analysis with compositional transition invariants. In CAV, volume 6174 of Lecture Notes in Computer Science, pages 89-103. Springer, 2010.
[62] O. Kupferman and M. Y. Vardi. Model checking of safety properties. In CAV, volume 1633 of Lecture Notes in Computer Science, pages 172-183. Springer, 1999.
[63] S. Kura, H. Unno, and I. Hasuo. Decision tree learning in CEGIS-based termination analysis. In CAV (2), volume 12760 of Lecture Notes in Computer Science, pages 75-98. Springer, 2021.
[64] L. C. Lamb, A. S. d' Avila Garcez, M. Gori, M. O. R. Prates, P. H. C. Avelar, and M. Y. Vardi. Graph neural networks meet neural-symbolic computing: A survey and perspective. In IJCAI, pages 4877-4884. ojcai.org. 2020.
[65] L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Eng., 3 22:125-143, 1977.
[66] M. Lechner, D. Žikelić, K. Chatterjee, and T. A. Henzinger. Stability verification in stochastic control systems via neural network supermartingaless. AAAI, pages 7326-7336. AAAI Press, 2022.
[67] Lehmann, A. Pnueli, and J. Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. In ICALP, volume 115 of LNCS, pages 264 264-277.00 Springer 1981.
[68] J. Leike and M. Heizmann. Ranking templates for linear loops. Log. Methods Comput. Sci., 1 (1)), 2015.
[69] M. Liu, N. R. Pinckney, B. Khailany, and H. Ren. VerilogEval: Evaluating large language models for Verilog code generation. In ICCAD, pages 1-8. IEEE, 2023.
[70] I. Loshchilov and F, Hutter. Decoupled weight decay regularization. In ICLR (Poster). OpenReview.net, 2019.
[71] A. K. Maini. Digital electronics: principles, devices and applications, Chapter Hl: Counters and Registers. John Wiley & Sons, 2007.
[72] J. B. P. Matos. Jr., E. B. de Lima Filho, I. Bessa, E. Manino, X. Song, and L. C. Cordeiro. Counterexample guided neural network quantization refinement. IEEE Trans. Comput, Aided Des. Integr. Circuits Syst., 43(4): 121-1134, 2024.
[73] K. L. McMillan. Applying SAT methods in unbounded symbolic model checking. In CAV, volume 2404 of Lecture Notes in Computer Science, pages 250-264. Springer, 2002.
[74] A. Mirhoseini, A. Goldie, M. Yazgan, et al. A graph placement methodology for fast chip design. Nature, (594):207-212, 2021.
[75] S. Mistry, I. Saha, and S. Biswas. MILP encoding for efficient verification of quantized deep neural networks. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 41(11):4445 4456, 2022.
14

---

[76] R. Mukherjee, D. Kroening, and T. Melham. Hardware verification using software analyzers. In ISVLSI, pages 7-12. IEEE Computer Society, 2015.
[77] R. Mukherjee, P. Schrammel, D. Kroening, and T. Melham. Unbounded safety verification for hardware using software analyzers. In DATE, pages 1152-1155. IEEE, 2016.
[78] V. Murali, A. Trivedi, and M. Zamani. Closure certificates. In HSCC, pages 10:1-10:11. ACM, 2024.
[79] A. Nadali, V. Murali, A. Trivedi, and M. Zamani. Neural closure certificates. In AAAI, pages
21 21446-21453 AAAT Press, 2024.
[80] A. Niemetz and M. Preiner. Bitwuzla. In CAV (2), volume 13965 of LNCS, pages 3-17. Springer, 2023.
[81] A. V. Nori and R. Sharma. Termination proofs from tests. In ESEC/SIGSOFT FSE, pages 246 256..56.440 ACM, 2013.
[82] A. Pnueli. The temporal logic of programs. In FOCS, pages 46-57. IEEE, 1977.
[83] A. Podelski and A. Rybalchenko. Transition invariants. In LICS, pages 32-41 IEEE Computer Society, 2004.
[84] A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI, volume 2937 of Lecture Notes in Computer Science, pages 239-251. Springer, 2004.
[85] Podelski and A. Rybalchenko. Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst., 29(3):15, 2007.
[86] Z. Qin, K. Zhang, Y. Chen, J. Chen, and C. Fan. Learning safe multi-agent control with decentralized neural barrier certificates. ICLR. OpenReview.net, 2021.
[87] T. Seufert, F. Winterer, C. Scholl, K. Scheibler; T. Paxian, and B. Becker. Everything you always wanted know about generalization of proof obligations in PDR. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 13(4):3351-1366 2023.
[88] W. Snyder. Verilator and SystemPerl. In North American SystemC Users' Group. Design Automation Conference, 2004.
[89] C. Spear and G. Tumbush. System for verification-a guide to learning the testbench language features. 2012.
[90] A. Subero and A. Subero. USART, SPI, and I2C: serial communication protocols. Program- ming PIC Microcontrollers with XC8, pages 209-276, 2018.
[91] T. Trippel, K. G. Shin, A. Chemyakhovskky G. Kelly, D. Rizzo, and M. Hicks. Fuzzing hard- ware like software. In USENIX Security Symposium, pages 3237-3254. USENIX Association, 2022.
[92] UM10204. I2C-bus specification and user manual, 2021. URL https://www. nxp com/ docs/ cics/ennuser--e www.d//uu0020/
[93] C. Urban. The abstract domain of segmented ranking functions. In SAS, volume 7935 of Lecture Notes in Computer Science, pages 43-62. Springer, 2013.
[94] C. Urban. FuncTion: An abstract domain functor for termination (competition contribution). In TACAS, volume 9035 of Lecture Notes in Computer Science, pages 464-466. Springer, 2015.
[95] M. Y. Vardi. Verification of concurrent programs: The automata-theoretie framework. Ann. Pure Appl. Log., 51((12):7795)) 1991.
[96] M. Y. Vardi and P. Wolper. An aatomata--theored approach to automatic program verification (preliminary report). In L/CS, pages 332-344. IEEE, 1986.
15

---

[97] E. W. Weisstein. Gray code. http::/maativorddwoffra...omm 2003.
[98] X. Zhang, S. Dwarkadas, G. Folkmanis, and K. Shen. Processor hardware counter statistics as a first-class system resource. In HotOS. USENIX Association, 2007.
[99] Zhao, X. Zeng. T. Chen, and Z. Liu. Synthesizig barrier certificates using neural networks. In HSCC, pages 25:1-25:11 ACM, 2020.
[100] D. Zhi, P. Wang, S. Liu, I. Ong, and M. Zhang. Unifying qualitative and quantitative safety verification of DNN-controlled systems. In CAV, Lecture Notes in Computer Science. Springer, 2024.
[101] Zikelic, M. Lechner, Henzinger, and K. Chatterjee. Learning control policies for stochastic systems with reach-avoid guarantees. In AAAI, pages 11926-11935. AAAI Press, 2023.
[102] Zikelic, M. Lechner, A. Verma, K. Chatterjee, and A. Henzinger. Compositional policy learning in stochastic control systems with formal guarantees. In NeurIPS, 2023.
16

---

To prevent overflow in the SMT query, we set bit-vector sizes appropriately. Let B be such that (R) A Details of the SMT Encoding of Quantised Neural Networks
The hth hidden layer in our network comprises fully connected layer followed by clamp operation that restricts outputs to the range [0, u/. This layer has hs neurons, and the previous layer contains hg-1 neurons. Each neuron in the ba layer is defined by:
hx-11
2 = Clamp(y, (2) uu),
(R)
(
w
1) (k-1) 2j
(6)
To facilitate SMT-checking modulo Bit- Vector theory, we quantise the floating-poit weights way and biases b, by multiplying them by 2 and truncating decimals, where f determines the precision. We define:
(k) trunc(w!) (A) 2²), bi = trunc (*) .2)
This transformation converts weights from floating-pott point values in [0. u] to integers in [0. 2f u). To ensure consistency between bit-vector and floating-point arithmetic, the output of each bit-vector encoded component should be equivalent to multiplying the floating-point output by 2/ and truncating the decimals. To achieve this, the SMT constraints on the bit-vectors formulated follows:
hg
hk-1
(k) = Clamp(y, ;2 (h = b(hh) + (fs
11)1)) =)(((1))))))
(7)
(k-1) and 2/(-11 are integers in [0. 2 u/. thus their product remains within (0,22 20) The Here, Wi
sum =(k) aggregates he such products, resulting in [0, uPha). An arithmetic right shift by / bits scales 2/4h to j0, 2 h²h to align with b, in [0, 2 u] (in floating-pon point arithmetic, the addition would involve values in [0, hx) and [0, u)). The clamp operation then restricts ji(*) [0, 2 u), ensuring consistency with the Hlatingg-poin arithmetic, where the value would lie within [0, u].
2 2 2 u. Each product w 3j requires up 2B bits, and summing hg terms necessitates additional log hg bits.
This encoding is standard in post-training quantisation fully connected layers 449 For element- wise multiplication layers, where each input is multiplied by corresponding weight, we quantise w; 2, as ashr( (0;- Te f): Again, W,C; lies within [0, u²). and the right shift scales it back to [0, 2 u²). ensuring consistency with the floating point encoding.
To address the significant slowdown caused by negative numbers in the Bitwuzla SMT-solver during our experiments, we restructured the dot product computation equation 7 By decomposing the weight vector Vig into two non-negative components-ur containing positive weights and wij containing the absolute values of negative weights we expressed the linear layers as
Wig
Σ G J=1
This transformation simplified multiplications to involve only non-negative numbers and consolidated negative operations into a single subtraction, speeding up the SMT-check our experiments.
We further rewrite the SMT encoding originally involving several à È multiplications, where ă is neuron value and ă is quantised integer weight- by replacing these multiplications with additions and left shifts. By factorising ă as sum of powers of two, >d G: 22, where G E {0, 1}. the multiplication can be rewritten
d
à T
C shi(
where ih) represents left-shifting by bits, effectively multiplying by 2
17

---

B Details of the Case Studies
We consider ten hardware designs in our study. These serve as benchmarks to demonstrate the scalability of our method compared to conventional symbolic model checkers. They are designed to be parameterizable.
The DELAY models generates positive signal sig after a fixed delay determined by the counter ent, includes a reset imput event that sets cnt to O, and aims to ensure that sig occurs infinitely often under the assumption that the reset event rst received finitely many times, resulting in the specification FG !rst + GF sig. We further verify FG !rst - GF (sig A X !sig), to ensure sig doesn't 't remain triggered forever.
The LCD Controller (LCD) performs a display initialisation setup, then awaits the ced_ee signal transition from ready to send for data transmission, and returns to ready after fixed interval, ensuring FG lcd__eeeee enable + GF ready.
Similarly, Thermocouple (Tmcp. >) transitions through stages, start, get_data and pause with suitable delay in between, processing SPI transactions and managing transitions based on bus activity, adhering to the specification FG ! - GF pata..
The The S-Semment (7-Seg) model alternates between two displays, ensuring each is activated regularly unless reset, as specified by FG ! + (GF disp = O A GF disp 1), we also verify simpler specification FG !sst + GF disp 1.
The i2c Stretch (i2cS) generates timing signals scl_clk and data_ clk based on the ratio of input and bus clock frequencies 92]. It monitors rst and detects the ena signal to manage clock stretching, ensuring FG (!rst & ena) + GF stretch.
The Pulse Width Modulation (PWM) system utilises an N-bit counter to adjust pulse widths dynamically based on input, verifying the low setting of pulse infinitely often as GF !pulse [54].
The VGA Controller (VGA) manages display interface using horizontal and vertical counters for pixel coordinates, ensuring smooth rendering by adjusting syne pulses and the display enable signal disp_ena, here we confirm FG !rst + GF disp_ena.
The UART Transmitter (UARTt) toggles between wait for preparing data and transmit for sending data, based on tx_ema requests and clk signals, validated by FG !rst + GF wait [90]
The Load-Store (LS) toggles between load and store with delay implemented by counter which counts from 0 up to N when load then switch to store counting back down to 0, before switching back to load, sig signals a switch from load to store, and we verify FG ! GF sig.
Lastly, the Gray Counter (Gray) counts in Gray codes to minimise transition errors by ensuring single bit changes between consecutive counts, with FG !rst - GF sig, indicating regular signalling of complete cycles [97]. Similar to the Delay module, we aim to ensure that the signal sig does not remain triggered indefinitely. We establish this with two distinct specifications FG!rst -> GF(sig A X !sig) and FG!rst > (GFsig/ A GF !sig).
C Details of the Experimental Results
3 the runtimes for each tool on the 194 verification tasks considered in Section These tasks involve verifying each hardware design across an increasing state space, labelled numerically. The "Train Time" column indicates the training duration for the neural network in seconds, while the other columns represent the total runtime for each tool, with the fastest tool time in bold and the rest in grey. In this table, our method uses the configuration described in Section [ with two hidden layers containing 8 and 5 neurons, respectively. Some of our runtimes are marked with an asterisk (*), indicating that in those cases we obtained counterexamples using the SMT solver; these were used for retraining and then validating the trained network. The reported time includes all SMT checks and training. Table
these results by showing the number of tasks successfully completed by each tool for each design. Tasks not marked as oul of time (oot.) or did not train (dnt.) are considered successful. Table 3 as the basis for computing all statistical observations discussed in Section and Section except those related to the "our best" line in Figure 64. All other
18

---

Model
LTI. Specification
Key Table 3
FG !rst GF sig
Da
DELAY
FG Irst GF (sig X !sig)
Db
LCD Controller
FG @cd_eenable + GF ready
L
Thermocouple
FG rrst + GF get_data
T
FG !sst -> GF disp
7a
7-Segment
FG !rst
(GF disp
GF disp 1)
7b
12c Stretch
FG (Irst & ena) - GF stretch
Pulse Width Modulation
GF !pulse
P
VGA Controller
FG !rrst + GF disp_ena
V
UART Transmitter
FG !rst - GF wait
U
Load-Store
FG !rst + GF sig
Ls
FG Irst - GF sig
Ga
Gray Counter
FG!rst - GF A X !sig)
Gb
FG!rst + (GFsig GF !sig)
Ge
Table Model Name and LTL Specification in our Benchmark
components of F derived from this table. By aggregating the duration of each experiment in the table, including OOT instances counted as 5 hours per experiment, the total time amounts 104 days and hours.
D Ablation Study
The network architecture deseribed in Section includes element-wise multiplication layer and separate trainable parameters associated with each state of the automaton A- For most of experiments in Section and all experiments in Appendix [ employ fully connected multilayer perceptron component with two hidden layers containing 8 and 5 neurons, respectively. perform ablation study and report the runtimes
To experimentally justify our architecture, for different configurations in Table[4 We consider three configurations for the two hidden layers: containing (3, 2) neurons, (5, 3) neurons, and (15, 8) neurons, respectively. We further replace the element-wist multiplication layer with fully connected layer of the same size, denoted as 'ExtL' for the extra layer. Additionally, we explore providing the global trainable parameters 0 to all automaton states of the automaton A-q. leading to a monolithic neural ranking function V (r. = V (r.:q:0) where the automaton state given as an additional input, which we denote as 'Mono'.
Given the large number of possible combinations of these modifications, we restrict our ablation study to switching only single configuration at time. In Table 4 the column labelled "Default' contains the results for our original configuration-the runtimes in this column are the same as those under 'Our (8, 5)' in Table Following that, have column for each of the three hidden layer configurations, followed by columns for the extra layer ('ExtL.'), and the monolithic neural ranking function ('Mono'). The 'our best" line Figure 6a is obtained by selecting the minimum runtime from the 'Default" and the three hidden layer configuration columns for each of the 194 tasks.
From Table 4 observe that default configuration succeeds in more cases than the alternative configurations, justifying our choices experimentally. Specifically, the default confi oonfiuuration completes 93 % of the tasks, while the three configurations with hidden layers containing (3. 2), (5. 3), and (15, 8) neurons complete 25 %, 63 %, and 74 of the tasks, respectively. The extra-layer configuration and the monolithic neural ranking function complete 24 %. and 39 %. of the tasks, respectively.
Generally-but not always-wwa when smaller network succeeds, runtime lower than that of the default network. Specifically, among the tasks completed by the (3, 2) neuron configuration,
19

---

was faster than the default configuration in 57 %of cases; for the (5, 3) neuron configuration, this statistic rises to 94%. Interestingly. this trend does not hold when comparing the (3, 2) and (5. 3) configurations: despite having more neurons, the (5, 3) configuration was faster than the (3, 2) configuration in 56 % of tasks. The default configuration not only completes more tasks than the (15, 8) configuration but is also faster on 97 % of the tasks successfully completed by the (15, 8) configuration. Notably, among the hidden layer configurations only the (15, 8) configuration succeeds on any of the tasks for the VGA design, labelled as "V" in the table. In 67 % of the tasks that the 'Ext. L' configuration completes, it is faster than the default configuration; this figure rises to 86 % for the "Mono' configuration. While the monolithic neural ranking function ('Mono') ) fails 61% of tasks, surprisingly succeeds on nine out of the ten tasks for the VGA design. Overall, only 5 of the 194 tasks fail under all configurations in the ablation study.
NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: The primary claims of our paper are outlined in the abstract and further detailed in Section I Here, we briefly discuss the theoretical aspects of our claims and provide brief summary of experiments that quantify the scalability of our method.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification: Our paper includes subsection 'Limitations' in Section where clearly outline our assumptions and justify their reasonableness alongside our theoretical limitations. In the same section, the 'Threats Validity' subsection validates the scope of our claims by justifying the benchmarks used to compare our method against tools developed with alternative verification methods. Section ( alao presents two studies, VGA and UART, to discuss the performance limitations of our approach, in comparison to others.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof?
Answer: [Yes]
Justification: We provide references for all theoretical results we rely on, i.e., automata- theoretical LTL model checking and fair termination, in Sec.
4. Experimental Result Reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
Justification: Subsections 'Implementation' 'Dataset Generation', and 'Network Hyper- parameters' in Section detail the workflow and specify the versions of our dependencies. These subsections clearly outline the hyperparameters and neural network architecture used. Specifically, Section 3 addresses theoretical aspects of the loss function, dataset generation, training procedures. neural network architecture, and the SMT-check problem. In contrast, the aforementioned subsections of Section 5 focus on practical implementation details, together providing sufficient information for implementing neural model checking. Additionally, 'Standard Model Checkers' and 'Industrial Verification Tools' discuss the tool versions we compare against. For additional specific implementation details, our code and benchmarks will be made available.
5. Open access to data and code
20

---

Question: Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Alongside the paper, we include a zip file in accordance with NeurIPS guidelines. This file contains benchmarks, scripts for running our experiments, and README. file that offers detailed instructions on how to reproduce our experiments.
Justification:
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (c.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary understand the results?
Answer: [Yes]
subsection, outlines training details and along with other subsections in the section provides essential information for interpreting the results. Appendix Cincludes table with the data used to generate the figures and tables in the main body of the paper.
Justification: Section 5 particularly the 'Network
7. Experiment Statistical Significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer:[Yes)
Justification: While error bars and confidence intervals are typically not applicable to our experiments that compare formal verification tools-which must be formally correct-we still present statistical data about our benchmarks. This data includes the range of logic gate counts and state space sizes considered for each design. Such metrics are definable for each SystemVerilogg file and inherently free from errors. These details are presented in Figure [S] We further discuss potential biases of the benchmark set in the subsection 'Threats Validity' in Section [
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: The computational resources allocated for experiments are outlined in Section The Appendix C details the computational time required for each experiment and the cumulative time to all experiments sequentially. We included all experiments in the experimental evaluation Section 5] and we discuss the experiments where our tool performs worse than the alternatives in the discussion of its limitations.
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics
Answer: [Yes]
Justification: We hereby affirm that all information presented in our research is disclosed with utmost academic integrity. Original works are duly cited and we ensure the repro- ducibility of our methodology through a detailed description of throughout the paper, we also provide our implementation of the methodology with all our experiments in the supplementary materials accompanying this paper. Notably, our experiments utilize solely synthetic data, with no human subjects involved, thereby aligning with ethical research standards. Our method aims to enhance the reliability and safety of computer systems. The benchmarks employed are derived from standard algorithms extensively documented in academic textbooks, which are referenced appropriately. Furthermore, we have thoroughly reviewed the NeurlPS Code of Ethics and confirm strict adherence to it.
10. Broader Impacts
21

---

Question:
Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: As discussed in the introduction, it is conceivable that improving the correct- ness of hardware designs prior to production delivers safer and more reliable devices; not manufacturing buggy silicon reduces waste. We are not aware of direct path negative application.
Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, scraped datasets)?
Question:
Answer: [NA].
Justification: Our work contributes to the safety of hardware systems. The designs used in our benchmarks are standard designs, from well-known literature, which are public domain and pose no risks for misuse.
12. Licenses for existing assets
Question: Are the creators or original owners of assets (e.g.. code, data, models), used in the paper, properly credited and the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification: We include the licences of the academic tools ABC and nuXmv. Appropriate references are used.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification: We include the source code of our prototype and our benchmarks as supplementary material of this paper with MIT licence.
14. Crowdsourcing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification: The paper does not involve crowdsoureing nor research with human subjects. 15. Institutional Review Board (IRB) Approvals Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: Neither crowdsourcing nor human subjects are involved.
22

---

Table 3: Runtime comparison with the state of the art on individual tasks.
Tasks
Train Time
18ST
Total Time
REARY
APR
Tool (in
Tosks
Time
D8.ST
BIXMIV
ABC
D6
181
78r
185
Dag
Digg
Dhy
D57
D2u
157
102
197
200
1009
occ
OCL
000
111
785
101
00L
000
000
005
7aa
70B
1310
2155
113
50
11005
000
100
000
006
000
000
000
o00
815
816
1010
120
1055
815
802
30304
813
0.56
1.3
520
oc0
2363
1006
Dw0
oct
70%
E1G
326
389
9691
705
000
100k
15129
000
000
oct
791
0.3
1.9
1000
000
601
cs0l
25
26
781
000
4448
20.10
000
100
47335
ool.
360
181
71333
oot
oct
oct
817
105
130
datt
onl
841
805
0.14
0.06
0.25
0.24
1018
0.00
1001
oot
514
0.14
0.1
1.40
0.40
oce
110
0.12
0.79
Cbn
106
358
1350
Clig
102
110
000
19164
585
o00
Clg
202
000
000
615
600
100
Gby
862
100
3341
824
Gbe
2055
14515
000
19
100
817
O8g
J547
000
1g
Ghi
o00
0.3
55
Gng
233
784
oct
1.25
110
GRa
6190
105
05%
100
3339
OBi
8211
3688
Clng
055
105
000
GB7
2003
oct
OcB
3535
Gai
12935
13b
231
1015
oc0
160
Dhb
300
6968
161
1.5
0ct.
30
2000
100
7bp
5352
130
500
000
7be
112088
181
Dba
2077
000
15
746
4.35
000
D611
555
7b
2386
7b
4.30
100
000
oct
000
313
000
100
000
5714
000
000
000
2121
000
1015
2187
000
16
700
310
oct
Exp
31
10773
339
0c0
100
100
000
136
000
000
155
185
000
105
000.
1420
044
750
1x0
100
11330
000
000
791
137
000
109
000
831
155
873
23

---

Table 4: Ablation Study Runtime.
Tusks
Ticks
Decabi
15
1000 TImee PET ScRup NOUT
15.31
115.87
EXLL
Momo
D51
D02
1.0
D20
703
254
160
Eail
785
35
575
130t
189
157
78
761
Faat
199
Dau
162
90
52
410
145
210
Eait
Tall
D57
137
119
Tar
85
Teil
329
Dieg
109
10%
700
100
2155
151
701
242
574
858
2018
750
133t
133
195
05:
1109
De1
1500
686
618
S463
1014
505
41.37
Tail
1515
3305
12:9
0525
7
2077
1579
7811
10
45226
1ea
101
13
Tea
235
96
Tei
364
1014
2017
114
601
Gril
1088
516
1382
9353
29992
$190
933
1896
013
Tail
X205
325
1043
Teal
291
360
Tioes
335
1329
355
1308
470
360
629
Fail
Tacl
Gri
Guil
33447
1322
1005
7537
Feal
Tail
7135
3011
Tult
Tail
Tiil
Trrl
Eril
Firl
Tail
109
101
69
Tail
593
420
102
11
760
155
161
251
1797
178
Tail
Fall
789
Eril
Firl
501
Tail
414
Tail
Tuil
Im
Ctby
21
Teal
118
Tall
Tiil
07
268
C10gg
312
2017
Eill
661
555
149
RTS
Enil
90%
3201
119
Tail
Clho
2011
6981
100
Ob
1876
1300
17855
Tail
Gan
30
135
1:56
700
255
GBn
381
Clng
2501
Gar
7.66
1793
1091
201
7864
1566
1014
849
2027
1305
0B11
57900
2207
2318
10005
1130
Tail
Db
189
9555
6255
Tmil
30
121
Euil
1066
160
100
104
-17
110
DBc
471
1889
DEC
711
532
Enil
Tmil
096
Dbb
862
Gail
2017
Dh1o
75g
1005
885
255
18:99
7654
210
1999
6356
16
3700
1615
12007
2187
701
130
Gall
24


Reviews:
[{"review_id": "VSYQm2eaWn", "reviewer": "Reviewer_ST48", "summary": "This work incorporates neural networks into the model checking process. Specifically, it learns a neural ranking function on random trajectories of the formal model. The ranking function first achieves zero loss on the training set and then is verified for soundness symbolically using SMT solvers. Evaluated on nine different hardware designs, the proposed approach shows significant improvement over prior works.", "questions": "Please consider addressing the points raised in the “Weakness” section.", "limitations": "The paper has sufficiently addressed the points concerning limitations and societal impact.", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The paper is easy-to-follow with illustrative examples and well motivated. The domain of hardware verification is very important. Moreover, the approach not only provides significant benefits as demonstrated in the experiments but also maintains the soundness guarantee.", "weaknesses": "My main concerns are the following.\n\n### 1. Choice of neural architecture\nThe architecture and some of the layers in Figure 2 seem carefully designed. What are the reasons for choosing these layers? Did you incorporate knowledge of the evaluated tasks into the design of the neural network?\n\n### 2. Size of evaluated tasks\nHow do the chosen tasks reflect real-world usages? As the paper suggests, increasing the network size would slow SMT check (Do other approaches have the same limitation?). If the size of the evaluated tasks is too small compared to real-world usages, the practical effectiveness of the proposed approach would be rather limited.\n\n### 3. Comparison\nThe evaluation compares the neural model checker with other checkers as a whole. While this comparison is valuable, there are many differing factors that can influence the results. I suggest adding ablation studies where different algorithms for constructing the ranking functions while keeping the overall system consistent. This would provide a clearer understanding of the algorithmic contribution of the paper.\n\n### 4. Other smaller issues\n- At Line 130, the signature of the network contains the parameters of the network. However, at Line 160, the signature does not. I suggest keeping this consistent.\n- The tool Industry Y failed on all tasks. What is the reason for this?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "1. Our architecture comprises three main components. The first component is a non-trainable element-wise multiplication layer, designed to normalize the input.  The second component is a trainable element-wise multiplication layer, whose purpose is to automatically focus attention on those inputs that contribute to the ranking. The third component is a trainable, fully connected network that represents the ranking. We employ the clamp activation function, which is standard for quantized neural networks. Overall, our architecture is tailored to address the problem domain effectively. Rather than tuning the architecture for each individual problem instance, we have developed a general architecture that is suitable for all our problems. Details of our architecture are further elaborated in lines 159-173 of the paper.\n\n2. We utilize a neural network with a consistent number of neurons across all our verification tasks. Consequently, in our experiments, the performance of the SMT check is influenced by the complexity of the overall verification task rather than the number of neurons. Our chosen tasks are based on established design patterns from standard literature, reflecting real-world hardware designs, and we have demonstrated favourable comparisons with both academic and industrial model checkers. Addressing scalability for large hardware designs is a significant challenge for the entire formal verification community, and our results represent a notable step forward in the field.\n\n3. We appreciate the reviewer's suggestion to conduct an ablation study. In the final version, we will include ablation studies in the appendix to justify our architectural choices. We will measure the performance of our method without the normalisation layer and without the element-wise multiplication layer, as well as different values for the clamp upper bound. We performed a preliminary ablation study on a subset of examples which confirms, as expected, that our normalisation layer and our choice of clamp upper bound are essential for the efficacy of our method. A systematic ablation will indeed make our evaluation even more solid.\n\n4. As per the reviewer’s suggestion, we will ensure the consistency of the signature of V throughout the paper. Finally, we remark that the internals of industry tool Y are proprietary and not disclosed to us. Although the tool accepts our specifications, we conjecture that its algorithm has not been optimized for full LTL verification. We consider industry tool X to be the leading tool for this purpose.", "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": "", "extra_scores": {}}, {"review_id": "1qVQq9JlOf", "reviewer": "Reviewer_2gkW", "summary": "The paper presents a novel application of machine learning to hardware model checking. The model checking problem is given as a design written in SystemVerilog and a temporal logic property in linear-time temporal logic (LTL). Similar to many classical model checking approaches the authors first construct the synchronous composition of the system model and the negation of the LTL property. The model checking problem then corresponds to checking whether the composition is empty (under some fairness condition). This emptiness can be witnessed by a ranking function on the states of the synchronous composition. The authors propose to learn this ranking function by representing it as a neural network and training the neural network with trajectories sampled from the composition. After training, a symbolic ranking function is extracted from the neural network using post-training quantization and checked with an SMT solver to be valid. On a set of benchmarks from the literature the authors impressively demonstrate that their approach often outperforms state-of-the-art academic model checkers and is competitive with industrial-grade model checkers.", "questions": "- In theory, the LTL model checking is decidable and has been extensively studied with respect to its computational complexity. Do you expect that any completeness or computational complexity results can be established for the presented approach?\n- I am confused about industry tool Y. It is reported even though it does not solve a single instance. Has industry tool Y been developed for these kinds of verification problems?\n- Do all benchmarks in the experimental evaluation include a fairness condition?\n- I do not understand the relationship that is drawn to reinforcement learning. How is the presented approach related? For example, what would be the MDP?", "limitations": "- The paper is transparent about the SMT checks being a bottleneck of the approach.\n- The tuning of the approach to individual benchmarks could be discussed in more detail in the limitations section.\n- I agree with the authors that no negative societal impacts are expected.", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 4, "strengths": "- The model checking problem is a fundamental problem in formal verification and is of great importance in industry. The paper contributes a novel neuro-symbolic approach to this fundamental problem. To the best of my knowledge, it is the first successful application of neural networks to the LTL model checking problem.\n- With designs being expressed in a hardware description language and properties being expressed in LTL, the approach is evaluated similarly to a real-world workflow.\n- The prototype implementation is already competitive with established tools. The authors compare with nuXmv and ABC which are state-of-the-art solvers in academia and the result of many years of engineering and research. The prototype outperforms those tools on 7 out of 9 benchmarks. Impressively, the authors show that their prototype is also competitive with industrial-grade solvers.\n- The results are also interesting for its use of ranking functions in the hardware model checking problem.", "weaknesses": "- When being familiar with the LTL model checking problem, Section 2 of the paper gives a helpful description of the problem. However, I expect it to be hard to follow for someone less familiar with the problem.\n- The approach requires some tuning when being applied to a specific problem instance (with respect to trajectory sampling and the neural network architecture). I assume that in the evaluation the academic and industrial tools didn’t need to be tuned to the instances.\n- The presented approach can only be used to establish that a system satisfies a formal guarantee but not a violation. Model checkers such as ABC and nuXmv establish both. This limitation is not immediately clear from the paper.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "* LTL model checking of hardware designs is indeed decidable and PSPACE-complete. While it is theoretically possible to achieve completeness by enumerating all transitions and employing a sufficiently large neural network as a look-up table for the entire state space, this approach is impractical for all but toy examples. We will note this in the final version of our paper.\n\n* Tool Y, a widely used industry tool for formal hardware verification, accepts specifications in SystemVerilog Assertions and thus supports our specifications out of the box. As the tool is proprietary, its internal workings are not disclosed to us, and neither are the reasons for its failure across all instances. We hypothesize that its algorithm may not be optimised for liveness and fairness checking. Consequently, we consider Tool X to be the state-of-the-art for LTL model checking.\n\n* We confirm that all benchmarks include fairness conditions, with further details provided in the appendix.\n\n* Our models are non-deterministic transition systems without probabilities and are hence not MDPs. While our approach shares similarities with reinforcement learning—primarily due to its training on traces or episodes rather than an external dataset—we acknowledge that this similarity may be confusing. We will clarify this in the final version.\n\n* Our method requires some parameter tuning, which is standard for stochastic gradient descent algorithms. Specifically, only two training parameters—the learning rate and clamp upper-bound—need tuning, both optimized across three predefined values. Additionally, our sampling parameter to determine the skewed distribution is chosen among four values (see lines 250-253). It is worth noting that symbolic algorithms also use parameters, such as BDD ordering heuristics, though these are often automated in established tools. Our parameters are certainly suitable for automated tuning methods.\n\n* Finally, we highlight that the presented approach is specialized to establish whether a property is satisfied, as is standard for verification methods based on proof rules (e.g., Hoare logic). The computation of counterexamples is done by combining the method with a bounded model checker, which is the best-known approach to falsification. Our prototype builds on top of the bounded model checker EBMC and hence already includes this capability.", "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": "", "extra_scores": {}}, {"review_id": "EvpYgoUpHS", "reviewer": "Reviewer_U2Dq", "summary": "This paper addresses the problem of hardware model checking with respect to LTL specifications. Although this a well-studied problem, hardware model checking can still suffer from scalability issues. A general automata-theoretic approach to model checking is to check if intersection of the formal languages corresponding to the system and to the complement of the specification is empty. One strategy for conducting this emptiness check is to construct a ranking function that can serve as an emptiness certificate. The main idea of the paper is to use neural networks to represent and learn these ranking functions. The functions are learned using traces of the system composed with the complement of the specification. It is then checked (using an SMT solver) if the learned function satisfies the required constraints of a ranking function. If not, the counterexamples are used to further train the function but if yes, then we have a proof that the system satisfies its spec. The proposed approach is evaluated on 9 hardware designs and with respect to 123 verification tasks. The presented approach outperforms state-of-the-art baselines on these verification tasks.", "questions": "In addition to the questions above, I have the following questions and comments:\n\n1. What if system does not meet its specification? In that case, no ranking function would exist. Is the proposed approach able to handle such scenarios and generate counterexamples when the system violates it spec?\n2. The paper frequently refers to word-level but it is never clarified what this means.\n3. Fig 1 needs more description. It is a little mysterious at present.\n4. Line 101: Is the language L_M defined over sequences of observed states of M or over sequences of atomic propositions about observed states of M. If it is the former, then the language inclusion does not make sense.\n5. Line 106: \"inputs and observables being equal to obs X\" --> this is a little hard to follow\n6. Line 161: \"normalizes these inputs through element-wise multiplication ...\" --> please expand a bit on this\n7. Equation 4: The indicator function seems to be incorrectly used. Should the term \"- 1_F(q)\" instead be \"- \\epsilon. \\neg 1_F(q)\"\n8. Line 226: Since there are only 9 designs and 123 verification tasks, are there multiple specs per design?\n9. Line 238: \"network is quantized and translated into SystemVerilog\" --> please provide some more details about this\n10. Figure 4: I am confused by the figure. How is the state space size and logic gate count different across the same design?\n11. Line 288: \"Of the 11 tasks that were not trained to zero loss, ...\" --> Are these tasks considered as timed out? Are they plotted in Fig 5b?\n12. Fig 5b: What are the tasks where x is almost 0 but y has large values?\n13. Line 306: Why is different hardware used for experiments with the industrial tools? This makes the head-to-head comparison unfair.", "limitations": "Yes, the paper includes a discussion about limitations. I do not see any potential negative societal impact of this work..", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "The paper is largely well-written and, for the chosen benchmarks, the results are quite impressive. The use of neural networks to represent ranking functions has been proposed before (citation [44] in the paper), but the setting in the prior work in slightly different  (termination analysis of programs in [44] vs model checking of hardware ciruits with respect to LTL specifications here). It is interesting to see that neural ranking functions can be effective in the setting of hardware model checking as well. It is particularly striking that the learned ranking function is frequently correct in the first attempt and does not need any further training.", "weaknesses": "I have a number of concerns with the paper.\n1. Given the prior work on neural termination analysis, I find the technical contribution to be quite incremental. The core of the technical approach is almost the same as in [44].\n\n2. While the empirical results are quite impressive, I wonder how the benchmarks were chosen. Why not choose the benchmarks from HWMCC'20? Also, why not compare against the best performing tool from HWMCC'20, i.e., AVR? Why set the time limit to 5 hours in particular? All these points make me a little concerned about the results. When is this approach not applicable? Can it be applied to all hardware model checking problems? Can it be applied to software model checking problems?\n\n4. The paper may not be easily accessible to readers not familiar with formal methods. In particular, there are a number of approaches for model checking with respect to LTL functions and using ranking functions for the purpose is not that common. I could only find two citations [A,B]. The paper should at least include these citations if not more for the ranking function based LTL model checking approach.\n\n[A] Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., & Vardi, M. Y. (2007). Proving that programs eventually do something good. ACM SIGPLAN Notices, 42(1), 265-276.\n\n[B] Dietsch, D., Heizmann, M., Langenfeld, V., & Podelski, A. (2015). Fairness modulo theory: A new approach to LTL software model checking. In Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I 27 (pp. 49-66). Springer International Publishing.\n\n5. I find the title to overclaim a bit. The paper focuses on hardware model checking but the title suggests that any model checking problem is within scope. Moreover, there might be other ways in which neural networks could be used to aid model checking. Is it a claim of the paper that the only way in which neural networks can aid model checking is as ranking functions? I also think that a formal methods conference might be a better fit for the paper.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "1 Our work is inspired by neural certificates [25,44,2,58,87], including neural termination analysis. Previous results on neural certificates focus on reachability/termination and avoidance/safety and temporal logic is largely unexplored. We applied neural certificates to LTL model checking and compared them with state-of-the-art model checkers. This is a substantial step forward in the area of verifying properties using neural certificates and introduces hardware model checking as a new application domain for this technology. \n\n2 Our benchmarks are derived from extremely common hardware design patterns from standard literature. The HWMCC benchmarks are exclusively bit-level designs and largely focus on safety verification; our work targets word-level designs and general LTL liveness/fairness. We compared with nuXmv and ABC as they are the best-performing tools in the liveness category, whereas AVR is restricted to safety analysis. Our 5-hour limit is significantly beyond the 1-hour limit used in the competition. We applied our approach to hardware model checking, where LTL is a natural specification language. Our approach applies to every LTL verification question and can in principle be extended to the verification of concurrent software, which is subject to future work. \n\n3 We leverage the fair-termination proof rule applied to Buechi acceptance, introduced in seminal work [45, 59, 83]. We refer to \"Proving that programs eventually do something good\", which influenced our work [A,33], and give an overview of ranking function synthesis (lines 359-362). The paper \"Fairness modulo theory: A new approach to LTL software model checking\" is an alternative and important related work in software verification, which we will cite in the final version.\n\n5 We agree that neural networks could be used in many other ways to improve model checking, and will discuss options for this in our conclusion. We have demonstrated that neural ranking functions are extremely effective for LTL model checking, and we instantiated this technology to circuits and SystemVerilog Assertions. Work on neural certificates is being regularly published at machine learning conferences [25,87,69]. This is a novel and emerging application for neural networks and, for this reason, we believe our result is best suited for NeurIPS. Our work offers a formal guarantee of correctness, a feature which is in strong demand in all AI communities.\n\nQ1 As is standard for methods based on proof rules, the presented approach solves the verification question in one direction. To make an analogy, this is similar to methods based on Hoare logic in software verification, where ranking functions and loop invariants prove correctness but do not directly provide counterexamples. To construct counterexamples, it is standard to couple verifiers with falsifiers such as bounded model checkers. Our prototype is built on top of EBMC and, as such, it includes this capability. \n\nQ2 By word-level we mean hardware descriptions based on arithmetic operations over fixed-width integers, as opposed to Boolean operations over bits. This is an important class of designs and a challenging problem for existing tools. We will clarify this important distinction in the final version. \n\nQ3 We will elaborate on Fig. 1 and clarify the meaning of the outputs \"fair\" and \"rnk\".\n\nQ4 The languages L_M and L_Phi are defined over sequences of valuations for the observables of M - the first option suggested by the reviewer. The reader familiar with alphabets defined over atomic propositions can assume the observables to be Boolean, and this will cover the second option. \n\nQ5 Line 106 indicates that an automaton can be expressed symbolically, with variables Y where inp Y = obs Y = obs = X, which is then in parallel composition with the system under analysis. We will elaborate and connect this to Fig. 1.\n\nQ6 Data normalization is a standard practice, typically, datasets are normalized before training. In our approach, we calculate the required normalization factors and incorporate them as the initial non-trainable layer. This enables the neural ranking function to process inputs directly without the need for separate normalization.\n\nQ7 Indeed, the signs of V(r,q;\\theta) and V(r',q';\\theta) in Eq. (3) should be switched. We will fix this in the final version.\n\nQ8 Each of the 9 designs has one spec, and the 123 tasks are generated by adjusting various parameters of the model, as we elaborate in lines 228-231. \n\nQ9 Quantisation converts a standard neural network over floats into a neural network over fixed-width integers. These are easily mappable to circuits in SystemVerilog. We will give an example in the appendix.\n\nQ10 The designs we use as benchmarks are parameterizable, which is a common feature when designing hardware using Verilog RTL. Our benchmark set includes multiple instances of each design, for a range of typical parameter values.\n\nQ11 Yes, indeed, the tasks that are not trained to zero loss are considered timeouts. These are visible in the top timeout line of Fig 5b.\n\nQ12 The tasks were nuXmv/ABS are fast but our method is slow are problems associated with VGA and UART, and are discussed as limitations (cf. Sec 5) \n\nQ13 We used different hardware because our license for the commercial tools is tied to a specific machine with restricted software. We highlight that we ran our prototype and nuXmv and ABC on the same machine, thus all measurements in Fig. 5 are consistent. We agree on the need for a head-to-head comparison between the industrial and academic tools. We are rerunning all the experiments on a machine with hardware identical to the one used for tools X and Y. We will include these results in the final version. Our preliminary results confirm (unsurprisingly) that our relative runtime w.r.t nuXmv and ABC are consistent with previous results, as we are also running them on the same machine. The results in comparison to X have changed by a small margin (+5%/-5%).", "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": "", "extra_scores": {}}, {"review_id": "Y9ZSH0PxZX", "reviewer": "Reviewer_GhN5", "summary": "The paper introduces a novel approach to hardware model checking using neural networks as proof certificates for linear temporal logic (LTL) specifications. Traditional model checking in electronic design automation (EDA) relies on symbolic techniques like SAT solvers, which are computationally intensive. In contrast, the proposed method leverages machine learning to generate neural certificates from random system executions, which are then verified symbolically for validity. The neural network acts as a ranking function ensuring compliance with the LTL specification, trained on synthetic data. Experimental results demonstrate the method's scalability and efficiency, outperforming academic tools in completion time across diverse hardware designs in SystemVerilog, and performing competitively with leading commercial tools.", "questions": "Can the proposed method provide any formal guarantee over the evaluated program?", "limitations": "The author discussed the limitation of this work about the heavy reliance on the SMT solver and the extensibility of application to Computational Tree Logic.", "rating": 5, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- This approach enhance verification in complex hardware designs efficiently through unsupervised machine learning techniques integrated with symbolic reasoning.\n- The paper is well organized and well written.", "weaknesses": "- The classic algorithm has a guarantee for the verification. I do not know how the use of deep neural network can still have such guarantee. \n- If we transform the problem to the SMT solver with same difficulty, it seems the SMT solver will still take a huge amount of time for verification.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "* Our method is as formally sound as traditional algorithms. We ensure this soundness through an SMT check, which validates that our neural ranking function is valid across the entire state space. Specifically, the SMT query in Eq. (4) represents the negation of the proof rules outlined in Eqs. (1) and (2). If this formula is unsatisfiable, it confirms that our neural ranking function is formally correct. This methodology aligns with established practices in neural certificate-based approaches, including Neural Lyapunov Control, Neural Termination Analysis, and Neural Supermartingales [25,44,2,58,87].\n\n* It is important to note that the complexity of verifying a ranking function via SMT solving, which is co-NP, is notably less than the complexity of LTL model checking, which is PSPACE-hard. Our machine learning approach heuristically fills this gap by training a proof certificate—a ranking function for fair termination—that we formally validate with an SMT solver. Our experimental results demonstrate that training and verifying a ranking function with SMT is more efficient than applying existing standard model-checking algorithms.\n\n* In summary, our method does provide formal guarantees while demonstrating scalability superior to standard model-checking algorithms.", "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": "", "extra_scores": {}}]

Author rebuttal:
We thank the reviewers for their comments, suggestions and questions, which we will address in the final version as we discuss in this rebuttal. We stress the novelty of our contribution, which introduces a new approach to model-checking temporal logic based on neural certificates. We demonstrated the superior efficacy of our approach compared to the state of the art in hardware model checking on standard hardware designs by means of a direct comparison with both academic and industrial tools. Our procedure guarantees the formal soundness of the result thanks to the combination of neural networks with symbolic reasoning (SMT).

Meta-review: The reviewers were overall positive about the importance of the problem considered, the closeness of the setting to practice, the quality of the presentation, and the improvements in relation to experimental results in the literature.  At the same time, they had some reservations about the choices in the evaluations, the sensitivity of the proposed approach to tuning, and in particular that the limitation to positive instances (as opposed to finding bugs or counterexamples) should be clarified and emphasized.  All four reviews are recommending acceptance, however three of them only at the borderline.
Decision: Accept (poster)