Neural Model Checking

Authors: mirco  giacobbe
daniel  kroening
abhinandan  pal
michael  tautschnig
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-14 18:41:50

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.

Main paper: 
 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-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-exhaustive [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 a design against a formal specification of correctness answers the question of whether the design satisfies the specification with mathematical certainty, for every possible execution of the system [9, 13, 35] .The EDA industry has heavily invested in software tools for symbolic model checking. Early symbolic model checking algorithms utilise fixed-point 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 to complex arithmetic data paths, prompting a shift towards iterative approximation of fixed points using propositional satisfiability (SAT) solving [16, 17, 33] , which is now the state-of-the-art 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 a machine learning approach to 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 a hardware design and an LTL specification Φ, we train a wordlevel 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 [28, 50] . We ultimately obtain a 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 a Büchi automaton that identifies counterexamples to Φ. We then train a neural ranking function designed to strictly decrease whenever the automaton encounters an accepting state and remain stable on non-accepting 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 satisfiability 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 a prototype that integrates PyTorch, the bounded model checker EBMC, the LTLto-automata translator Spot, the SystemVerilog simulator Verilator, and the satisfiability solver Bitwuzla [44, 76, 80, 88] . We have assessed the effectiveness of our method across 194 standard hardware model checking problems written in SystemVerilog and compared our results with the state-of-the-art academic hardware model checkers ABC and nuXmv [24, 27] , and two commercial counterparts. For any given time budget of less than 5 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 is 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 2 % of them. Overall, with a straightforward implementation, our method outperforms mature academic and commercial model checkers.Our contribution is threefold. We present for the first time a 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.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 1. Here, we briefly discuss the theoretical aspects of our claims and provide a brief summary of experiments that quantify the scalability of our method. 
automata-theoretic 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 Φ.Our formal model M of a hardware design consists of a finite set of bit-vector-typed variables X M with fixed bit-width and domain of assignments S, partitioned into input variables inp X M ⊆ X M and state-holding register variables reg X M ⊆ X M ; we interpret primed variables X ′ M as the value of X M after one clock cycle. Then, a sequential update relation Update M relates X M and reg X ′ M and computes the next-state valuation of the registers from the current-state valuation of all variables; we interpret Update M as a first-order logic formula encoding this relation. A state s ∈ S is a valuation for the variables X M . We denote as reg s, inp s, . . . the restriction of s to the respectiveM A ¬Φ reg X M q obs X M inp X M clk V θ θ q 1 F (q) V time → (a) (b)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 s, which we write as s → M s ′ , if Update M (s, reg s ′ ) evaluates to true. We call → M the transition relation of M and say that an infinite sequence of states s0 , s1 , s2 , . . . is an execution of M if si → M si+1 for all i ≥ 0; we say that an execution is initialised in s 0 ∈ S when s0 = s 0 .We specify the intended behaviour of systems in LTL, which is the foundation of SystemVerilog Assertions. LTL extends propositional logic with temporal modalities X, G, F, and U. The modality X Φ 1 indicates that Φ 1 holds immediately after one step in the future, G Φ 1 indicates that Φ 1 holds at all times in the future, F Φ 1 indicates that Φ 1 holds at some time in the future, and Φ 1 U Φ 2 indicates that Φ 1 holds at all times until Φ 2 holds at some time in the future. We refer the reader to the literature for the formal syntax and semantics of LTL [82] . The atomic propositions of the LTL formulae we consider are Boolean variables of M, which we call the observables obs X M ⊆ X M of M. We note that any first-order predicate over X M can be bound to a Boolean observable using combinational logic (cf. Figure 4 , where observable ful corresponds to predicate cnt == 7).We call a trace of M a sequence obs s0 , obs s1 , obs s2 , . . . where s0 , s1 , s2 , . . . is an execution of M. We define the language L M of M as the maximal set of traces of M. Every LTL formula Φ is interpreted over traces and as such defines the language L Φ of traces that satisfy Φ. The model checking problem corresponds to deciding the language inclusion question L M ⊆ L Φ .As is standard in automata-theoretic model checking, we rely on the result that every LTL formula admits a non-deterministic Büchi automaton that recognises the same language [95, 96] . A nondeterministic Büchi automaton A consists of a finite set of states Q, an initial start state q 0 ∈ Q, an input domain Σ (also called alphabet), a transition relation δ ⊆ Q × Σ × Q, and a set of fair states F ⊆ Q. One can interpret an automaton A as a hardware design with one register variable reg X A = {q} having domain Q, input and observable variables inp X A = obs X A having domain Σ, and sequential update relation Update A (σ, q, q ′ ) ≡ (q, σ, q ′ ) ∈ δ governing the automaton state transitions. We say that an execution of A is fair (also said to be an accepting execution) if it visits fair states infinitely often. We define the fair language L f A of A as the maximal set of traces corresponding to fair executions initialised in q 0 . Given any LTL formula Φ, there are translation algorithms and tools to construct non-deterministic Büchi automata A Φ such that L f AΦ = L Φ [44, 58] . The standard approach to answer the language inclusion question L M ⊆ L Φ is to answer the dual language emptiness question L M ∩ L ¬Φ = ∅ [13, 35] . For this purpose, we first construct a non-deterministic Büchi automaton A ¬Φ for the complement specification ¬Φ where inp X A¬Φ = obs X M , then we reason over the synchronous composition (over a shared clock) of M and A ¬Φ as illustrated in Figure 1a . We direct the reader to the relevant literature for general definitions of system composition [10] . In this context, the synchronous composition results in the system M ∥ A ¬Φ with input variables inp X M∥A¬Φ = inp X M , register variables reg X M∥A¬Φ = reg X M ∪ {q}, observable variables obs X M∥A¬Φ = obs X M , and sequential update relation Update M∥A¬Φ (s, q, r ′ , q ′ ) = Update M (s, r ′ ) ∧ Update A¬Φ (obs s, q, q ′ ). We extend the fair states of A ¬Φ to M ∥ A ¬Φ , i.e., we define them as {(s, q) | s ∈ S, q ∈ F }, and as a result we have thatL f M∥A¬Φ = L M ∩ L f A¬Φ = L M ∩ L ¬Φ .This reduces our language emptiness question to the equivalent fair emptiness problemL f M∥A¬Φ = ∅. Learn Check M ∥ A ¬Φ D V , θ D ← D ∪ {cex} Ṽ , θ valid!Figure 2 : Learn-and-check workflow for provably sound neural ranking function learningThe fair emptiness problem amounts to showing that all executions of M ∥ A ¬Φ are unfair, and we do so by presenting a ranking function that witnesses fair termination [51, 67] . A ranking function for fair termination is a map V : reg S × Q → R where (R, ≺) defines a well-founded relation and, for all system and automaton states s, s ′ ∈ S, q, q ′ ∈ Q, the following two conditions hold true:EQUATIONEQUATIONA ranking function V strictly decreases every time a transition from a 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 1b , where 1 F (q) denotes the indicator function of F , returning 1 if q ∈ F and 0 otherwise. The existence of a 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 we train from generated sample executions.Question: Does the paper discuss the limitations of the work performed by the authors?Answer: [Yes] Justification: Our paper includes a subsection on 'Limitations' in Section 5, where we clearly outline our assumptions and justify their reasonableness alongside our theoretical limitations.In the same section, the 'Threats to 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 5 also presents two case studies, VGA and UART, to discuss the performance limitations of our approach, in comparison to others. 
neural ranking functions for fair termination: 
 We approach the problem of computing a ranking function for fair termination by training a neural network V : R n × Θ → R, with n input neurons where n = | reg X M | 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 a distinct trainable parameter θ q ∈ Θ to each state q ∈ Q of the Büchi automaton. We train these parameters on sampled executions of M ∥ A ¬Φ to ultimately represent a ranking function as a neural network V (r, q) ≡ V (r; θ q ), which we call a neural ranking function. This scheme is illustrated in Figure 1 , where we denote the set of all parameters by the unindexed θ.We define our training objective as fulfilling conditions (1) 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 S × Q using satisfiability solving modulo theories (SMT) [14, 60] , to confirm the validity of our neural ranking function or obtain a 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 a system M and a specification Φ, we train the parameters θ of a neural network V from a sample dataset D ⊂ reg S×Q×reg S×Q of subsequent transition pairs, which we construct from random executions of the synchronous composition M ∥ A ¬Φ . Each execution (s 0 , q0 ), (s 1 , q1 ), . . . , (s k , qk ) initiates from a random system and automaton state pair and is then simulated over a finite number of steps; the inputs to M and the non-deterministic choices in A ¬Φ are resolved randomly. Our dataset D is constructed as the set of all quadruples (reg si , qi , reg si+1 , qi+1 ) for i = 0, . . . , k -1 from all sampled executions, capturing consecutive state pairs along each execution; notably, the order in which quadruples are stored in D is immaterial for our purpose, as our method reasons and trains locally on each transition pair regardless of their order of appearance along any execution.We train the parameters of our neural network V to satisfy the ranking function conditions (1) and (2) over D. For each quadruple (r, q, r ′ , q ′ ) ∈ D, this amounts to minimising the following loss function: L Rank (r, q, r ′ , q ′ ; θ) = ReLU( V (r ′ ; θ q ′ ) -V (r; θ q ) + ϵ • 1 F (q)).(3) where ϵ > 0 is a hyper-parameter that denotes the margin for the decrease condition. When L Rank 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; θ q ) ≥ V (r ′ ; θ q ′ ), which corresponds to satisfy condition (1); if otherwise q ∈ F , then V decreases by at least the margin ϵ > 0 along the given transition, i.e., V (r; θ q ) ≥ V (r ′ ; θ q ′ ) + ϵ, which corresponds to satisfy condition (2). Trainable parameters θ q r V Figure 3 : Neural ranking function architecture Overall, our learning phase ensures that the total loss function L(D; θ) below takes value zero:EQUATIONUnlike many other machine learning applications, for our purpose it is essential to attain the global minimum; if this fails, there are counterexamples to V being a 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 ∈ Q and optimise only θ q ∈ Θ for a number of steps, while keeping all other parameters θ q ′ ∈ Θ fixed to their current value, for all q ′ ̸ = 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; θ) takes value zero.Our neural network V follows a feed-forward architecture as depicted in Figure 3 : for a given automaton state q ∈ Q and associated parameter θ q , it takes an n-dimensional input r ∈ R n where each input neuron corresponds to the value of a register variable in reg X M , and produces one output for the corresponding ranking value V (r; θ q ). Our architecture consists of a normalisation layer, followed by an element-wise multiplication layer, in turn followed by a multi-layer perceptron with clamped ReLU activation functions. The first layer applies a scaling factor to each input neuron independently to ensure consistent value ranges across inputs, implemented via element-wise multiplication with a 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 a n-dimensional vector with trainable coefficients. Finally, this is followed by a fully connected multi-layer perceptron with trainable weights and biases, with the activation function defined as the element-wise application of Clamp(x; u) = max(0, min(x, u)); the upper bound u and the depth and width of the hidden layers of the multi-layer perceptron component are hyper-parameters chosen to optimise training and verification performance.Attaining zero total loss L(D; θ) 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∥A¬Φ , as required to fulfil conditions (1) and (2) and consequently to answer our model checking question (cf. Section 2). To formally check whether the ranking criteria are satisfied over the entire transition relation, we couple our learning procedure with a sound decision procedure that verifies their validity, as 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 M∥A¬Φ 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 M∥A¬Φ 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 bitvectors [80] , we quantise our neural network using a 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 θ ≈ 2 f • θ, where f is a hyper-parameter for the number of fractional digits in fixed-point representation, and we replace linear layers and activation functions by their quantised counterpart; readers may consult the relevant literature for more detailed information on neural [49, 57] . This results in a quantised neural network Ṽ : Z n × Θ → Z that approximates our trained network Ṽ ≈ 2 f • V , where Θ denotes the space of integer parameters. fractional digits introduced by the linear layers [49, 57] . We consider the quantised network Ṽ as our candidate proof certificate for fair termination.We reduce the validity query-whether our quantised neural network Ṽ satisfies the ranking criteria for fair termination ( 1) and ( 2) over the entire transition relation of M ∥ A ¬Φ -to the dual satisfiability query for the existence of a counterexample to the criteria. Specifically, we delegate to an off-the-shelf SMT solver the task of computing a satisfying assignment s ∈ S, r ′ ∈ reg S for which the following quantifier-free first-order logic formula is satisfied:EQUATIONwhere θ 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 [49] , supplementing it with specialised rewriting rules to enhance the solver's performance, as detailed in Appendix A. We additionally note that Ṽ is guaranteed to be bounded from below as S is finite, albeit potentially very large, i.e., exponential in the combined bit-width of X M .If the solver finds a satisfying assignment, then the assignment represents a transition of M that refutes the validity of Ṽ ; in this case, we extend it to a respective transition in M ∥ A ¬Φ , we 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 Ṽ is formally a valid neural ranking function and, consequently, system M satisfies specification Φ.We note that LTL model checking of hardware designs is decidable and PSPACE-complete [9, 13, 35 ]. While it is theoretically possible for our approach to achieve completeness when a 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, we employ tiny neural networks and incomplete but practically effective gradient descent algorithms to train neural ranking functions. We experimentally demonstrate on a large set of formal hardware verification benchmarks that this solution is very effective in practice.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., automatatheoretical LTL model checking and fair termination, in Sec. 2 
illustrative example: 
 Modern hardware designs frequently incorporate word-level arithmetic operations, the simplest of which being counter increments/decrements, which are a staple in hardware engineering [71, 98] .One such example is illustrated as part of the SystemVerilog module in Figure 4 . 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 rw = 1 until the buffer is full and then rw = 0 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 Φ = GF ful ∧ 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 ∨ FG ¬emp. Equivalently, this amounts to 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 5 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 4 , 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: 0 1 2 3 4 5 6 7 6 5 4 3 2 1 0 1 2 3 4 5 6 emp ful emp ful cnt7 m 0 1 1 1 1 1 1 1 0 0 0 0 0 0 0 1 1 1 1 1 1 1 rw 1 1 1 1 1 1 1 0 0 0 0 0 0 0 1 1 1 1 1 1 1 0 V (•;θq 0 ) 14 14 14 14 14 14 14 14 14 14 14 14 14 14 14 14 14 14 14 14 14 14 V (•; θq 1 ) 8 7 6 5 4 3 2 1 14 13 12 11 10 9 8 7 6 5 4 3 2 1 V (•; θq 2 ) 1 14 13 12 11 10 9 8 7 6 5 4 3 2 1 14 13 12 11 10 9 8One can observe that all transitions throughout this execution satisfy conditions (1) and ( 2). This assessment is based on the (not explicitly presented) synchronous composition with the automaton. First, we note that every transition originating from q 0 has a non-increasing ranking value, as V (•; θ q0 ) = 14 is an upper bound to all other values. Furthermore, every transition leaving q 1 -that is, every transition whose source state satisfies ¬ful-exhibits a strictly decreasing value V (•; θ q1 ). Similarly, the same observation applies to q 2 and the condition ¬emp. We note that the transitions that exhibit increasing values from 1 to 14 in this execution are impossible over the synchronous composition; this is because they are originating from states that satisfy both ful and q 1 , and similarly states that satisfy both emp and q 2 , and which do not have corresponding transitions in the automaton. This neural ranking function admits no increasing transition originating from q 0 and no non-decreasing transitions originating from q 1 or q 2 on the synchronous composition of the system and the automaton. Therefore, it is a valid proof certificate for every system trace to satisfy specification Φ.Question: Does the paper fully disclose all the information needed to reproduce the main experimental results of the paper to the extent that it 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 Hyperparameters' in Section 5 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. 
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 are 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 checking2 , utilising Spot 2.11.6 [44] to generate the automaton A ¬Φ from an LTL specification Φ. As depicted in Figure 1 , 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 a 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 to SMT, following the process outlined in Appendix A. The SystemVerilog model is converted to SMT using EBMC 5.2 [76] . We check the satisfiability problem using the Bitwuzla 0.6.0 SMT solver [80] .We benchmarked our neural model checking approach against two leading model checkers, nuXmv [27] and ABC [24, 25] . ABC and nuXmv were the top performers in the liveness category of the hardware model checking competition (HWMCC) [15, 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 SystemVerilog, anonymised as industry tool X and industry tool Y. Tool Y fails to complete any of the 194 tasks and is therefore not referenced further in this section. Hyper-parameters We instantiate the architecture described in Section 3 and illustrated in Figure 3 , employing two hidden layers containing 8 and 5 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 a 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, 89] . We apply CRV to the SystemVerilog file, generating random trajectories. As outlined in Section 3, we start these trajectories by selecting the internal states of model M (e.g., module BufferCtr and automaton A ¬Φ ; in Figure 4 ) using a uniform distribution. At each step, we 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 a particular event is too predominant or too rare. In our experiments, such skewing is rare and limited to the reset and enable signals in M, as well as the non-determinism in the automaton A ¬Φ .Solved Tasks Table 1 presents the number of completed tasks for each tool across the ten hardware designs, while Figure 5 shows the range of state-space sizes and logic gate counts each tool successfully handled. Overall, our tool performs favourably in comparison to others, with the notable exception of the VGA design, where training a ranking function failed due to local minima, preventing convergence to zero loss-a known limitation of gradient descent-based methods.Aggregate Runtime Comparison Figure 6a displays a cactus plot with a 5 h limit, we consider our configuration with 8 and 5 hidden neurons as 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 a 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, we continue using the default architecture. 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 nuXmv, and 11 % more than the leading commercial model checker at any given time. Furthermore, the number of tasks completed by nuXmv 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 6b presents a scatter plot where each point represents a 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 on 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 N -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 SMT-check steps, making us slower on trivial model-checking problems.Learning vs. Checking Time Figure 6c 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 a 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 5 h time limit was not fully utilised; the loss function stabilised at local minima in just a few minutes. Moreover, training was faster than verification on 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.The experimental results may not generalise to 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 out-of-distribution problem: we train our neural net from scratch for each benchmark using randomly generated trajectories, and do not use any pretraining.Question: Does the paper provide open access to the data and code, with sufficient instructions to faithfully reproduce the main experimental results, as described in supplemental material?Answer: [Yes] Justification: Alongside the paper, we include a zip file in accordance with NeurIPS guidelines. This file contains benchmarks, scripts for running our experiments, and a README.md file that offers detailed instructions on how to reproduce our experiments. 
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 SystemVerilog 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 SystemVerilog Assertions-which is based on LTL-is a widely adopted language for this purpose [48, 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, 34, 62] . 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 a one-step bounded model checking query to check the ranking function (see Eq. ( 5)), and goes beyond safety. Liveness checking for branching-time 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 [31, 56] , IC3 has been augmented with strongly connected components [23] , and BDD-based algorithms with the Emerson-Lei fixed-point computation [23, 46] . Iterative symbolic computation is the bottleneck on systems with word-level arithmetic. This is usually addressed by either computing succinct explicit-state abstractions of the system [6, 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, 37, 39, 43, 51, 67, 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 [63, 93, 94] , word-level arithmetic functions [29, 40] , lexicographic ranking functions [22, 68] , and disjoint well-founded relations [36, 38, 61, 83] , and similar proof certificates based on liveness-to-safety translation to reason about the transitive closure of the system [18, 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 [1, 2, 28, 41, 66, 79, 86, 99-102], formal verification of software and probabilistic programs [3, 4, 50] , and this work applies them for the first time to hardware model checking.Question: Does the paper specify all the training and test details (e.g., data splits, hyperparameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?Answer: [Yes]Justification: Section 5, particularly the 'Network Hyper-parameter' subsection, outlines training details and along with other subsections in the section provides essential information for interpreting the results. Appendix C includes a table with the data used to generate the figures and tables in the main body of the paper. 
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 SystemVerilog Assertions and compared its performance with the state of the art on a range of SystemVerilog designs. We employed off-the-shelf SMT solving (Bitwuzla) and bounded model checking (EBMC) to formally verify our 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 our approach is topic of future work [11, 64, 72, 75] . This is the first successful application of neural certificates to model checking temporal logic, and introduces hardware model checking as a new application domain for this technology. Neural networks could be used in many other ways to improve model checking. Our work creates a baseline for further development in this field and positively contributes to the safety assurance of systems.Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?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 SystemVerilog file and inherently free from errors. These details are presented in Figure 5 . We further discuss potential biases of the benchmark set in the subsection 'Threats to Validity' in Section 5. 
experiments compute resources: 
 Question: For each experiment, does the paper provide sufficient information on the computer resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?Answer: [Yes] Justification: The computational resources allocated for our experiments are outlined in Section 5. The Appendix C details the computational time required for each experiment and the cumulative time to run all experiments sequentially. We included all our 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. 
code of ethics: 
 Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics https://neurips.cc/public/EthicsGuidelines? 
 
 Appendix: The k th hidden layer in our network comprises a fully connected layer followed by a clamp operation that restricts outputs to the range [0, u]. This layer has h k neurons, and the previous layer contains h k-1 neurons. Each neuron i in the k th layer is defined by:EQUATIONTo facilitate SMT-checking modulo Bit-Vector theory, we quantise the floating-point weights w ij and biases b i by multiplying them by 2 f and truncating decimals, where f determines the precision. We define:w(k) ij = trunc(w (k) ij • 2 f ), b(k) i = trunc(b (k) i • 2 f )This transformation converts weights from floating-point values in [0, u] to integers in [0, 2 f 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 f and truncating the decimals. To achieve this, the SMT constraints on the bit-vectors are formulated as follows: To prevent overflow in the SMT query, we set bit-vector sizes appropriately. Let B be such thatEQUATION2 B ≥ 2 f u. Each product w(k) ij x(k) jrequires up to 2B bits, and summing h k terms necessitates additional log h k bits. This encoding is standard in post-training quantisation of fully connected layers [49] . For elementwise multiplication layers, where each input is multiplied by a corresponding weight, we quantise w i • x i as ashr( wi • xi ; f ): Again, wi xi lies within [0, 2 2f u 2 ], and the right shift scales it back to [0, 2 f u 2 ], 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 in equation 7. By decomposing the weight vector wij into two non-negative components-w+ ij containing positive weights and wij containing the absolute values of negative weights-we expressed the linear layers asEQUATIONThis transformation simplified multiplications to involve only non-negative numbers and consolidated negative operations into a single subtraction, speeding up the SMT-check in our experiments.We further rewrite the SMT encoding-originally involving several ã • x multiplications, where x is a neuron value and ã is a quantised integer weight-by replacing these multiplications with additions and left shifts. By factorising ã as a sum of powers of two, ã =d i=0 c i • 2 i, where c i ∈ {0, 1}, the multiplication can be rewritten as:ã • x = d i=0 c i • shl(x; i),where shl(x; i) represents left-shifting x by i bits, effectively multiplying x by 2 i .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 a positive signal sig after a fixed delay determined by the counter cnt, includes a reset input event that sets cnt to 0, and aims to ensure that sig occurs infinitely often under the assumption that the reset event rst is received finitely many times, resulting in the specification FG !rst → GF sig. We further verify FG !rst → GF (sig ∧ X !sig), to ensure sig doesn't remain triggered forever.The LCD Controller (LCD) performs a display initialisation setup, then awaits the lcd_enable signal to transition from ready to send for data transmission, and returns to ready after a fixed interval, ensuring FG lcd_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 !rst → GF get_data.The 7-Segment (7-Seg) model alternates between two displays, ensuring each is activated regularly unless reset, as specified by FG !rst → (GF disp = 0 ∧ GF disp = 1), we also verify a simpler specification FG !rst → 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 [90, 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 a display interface using horizontal and vertical counters for pixel coordinates, ensuring smooth rendering by adjusting sync 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_ena requests and clk signals, validated by FG !rst → GF wait [90] .The Load-Store (LS) toggles between load and store with a 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 !rst → 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 ∧ X !sig) and FG!rst → (GFsig ∧ GF !sig).Table 3 provides the runtimes for each tool on the 194 verification tasks considered in Section 5. 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 5, 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 1 summaries these results by showing the number of tasks successfully completed by each tool for each design. Tasks not marked as out of time (oot.) or did not train (dnt.) are considered successful. Table 3 serves as the basis for computing all statistical observations discussed in Section 1 and Section 5, except those related to the "our best" line in Figure 6a . All otherKey Table 3 DELAY FG !rst → GF sig Da FG !rst → GF (sig ∧ X !sig) Db LCD Controller FG lcd_enable → GF ready L Thermocouple FG !rst → GF get_data T 7-Segment FG !rst → GF disp = 1 7a FG !rst → (GF disp = 0 ∧ GF disp = 1) 7b i2c Stretch FG (!rst & ena) → GF stretch I Pulse Width Modulation GF !pulse P VGA Controller FG !rst → GF disp_ena V UART Transmitter FG !rst → GF wait U Load-Store FG !rst → GF sig Ls Gray Counter FG !rst → GF sig Ga FG!rst → GF(sig ∧ X !sig) Gb FG!rst → (GFsig ∧ GF !sig) GcThe network architecture described in Section 3 includes an element-wise multiplication layer and separate trainable parameters associated with each state of the automaton A ¬Φ . For most of our experiments in Section 5 and all experiments in Appendix C, we employ a fully connected multilayer perceptron component with two hidden layers containing 8 and 5 neurons, respectively. To experimentally justify our architecture, we perform an ablation study and report the runtimes 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-wise multiplication layer with a fully connected layer of the same size, denoted as 'ExtL' for the extra layer. Additionally, we explore providing the global trainable parameters θ to all automaton states of the automaton A ¬Φ , leading to a monolithic neural ranking function V (r, q) ≡ V (r, q; θ), where the automaton state q is 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 a single configuration at a 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 3 . Following that, we have one 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 in 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 , we observe that our default configuration succeeds in more cases than the alternative configurations, justifying our choices experimentally. Specifically, the default configuration 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-when a smaller network succeeds, its runtime is lower than that of the default network. Specifically, among the tasks completed by the (3, 2) neuron configuration, it 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 on 61% of tasks, it 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 ChecklistJustification: 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 reproducibility of our methodology through a detailed description of it 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 NeurIPS Code of Ethics and confirm our strict adherence to it.10. Broader Impacts https://github.com/aiverification/neuralmc 


Decision: 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.

Reviews: review: paper_summary: paper_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.
strength_weakness: strength_weakness: My main concerns are the following.

### 1. Choice of neural architecture
The 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?

### 2. Size of evaluated tasks
How 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.

### 3. Comparison
The 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.

### 4. Other smaller issues
- 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.
- The tool Industry Y failed on all tasks. What is the reason for this?
questions: questions: Please consider addressing the points raised in the “Weakness” section.
limitations: limitations: The paper has sufficiently addressed the points concerning limitations and societal impact.
paper_summary: paper_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.
strength_weakness: strength_weakness: - 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.
- 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.
- 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.
questions: 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?
- 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?
- Do all benchmarks in the experimental evaluation include a fairness condition?
- 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: limitations: - The paper is transparent about the SMT checks being a bottleneck of the approach.
- The tuning of the approach to individual benchmarks could be discussed in more detail in the limitations section.
- I agree with the authors that no negative societal impacts are expected.
paper_summary: paper_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.
strength_weakness: strength_weakness: I have a number of concerns with the paper.
1. 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].

2. 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?

4. 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.

[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.

[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.

5. 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.
questions: questions: In addition to the questions above, I have the following questions and comments:

1. 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?
2. The paper frequently refers to word-level but it is never clarified what this means.
3. Fig 1 needs more description. It is a little mysterious at present.
4. 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.
5. Line 106: "inputs and observables being equal to obs X" --> this is a little hard to follow
6. Line 161: "normalizes these inputs through element-wise multiplication ..." --> please expand a bit on this
7. Equation 4: The indicator function seems to be incorrectly used. Should the term "- 1_F(q)" instead be "- \epsilon. \neg 1_F(q)"
8. Line 226: Since there are only 9 designs and 123 verification tasks, are there multiple specs per design?
9. Line 238: "network is quantized and translated into SystemVerilog" --> please provide some more details about this
10. Figure 4: I am confused by the figure. How is the state space size and logic gate count different across the same design?
11. 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?
12. Fig 5b: What are the tasks where x is almost 0 but y has large values?
13. Line 306: Why is different hardware used for experiments with the industrial tools? This makes the head-to-head comparison unfair.
limitations: limitations: Yes, the paper includes a discussion about limitations. I do not see any potential negative societal impact of this work..
paper_summary: paper_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.
strength_weakness: strength_weakness: - 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. 
- 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.
questions: questions: Can the proposed method provide any formal guarantee over the evaluated program?
limitations: 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.

Comments: title: reply
Thanks for the rebuttal
comment: Thanks for the detailed reply. I'm happy to improve my score from 4 to 5.
Thank you for the detailed response! I will keep my score.
I have read the rebuttal and thank the authors for their comments and clarifications.
Thanks for submitting the rebuttal. I have read it and will keep the score. I hope the authors incorporate the reviews and the rebuttal into the next version of the paper.