Property Directed Reachability (aka PDR/IC3) is the strongest engine presently used in formal verification tools. Localization abstraction is a way to reduce the complexity of a verification problem by cutting away irrelevant logic. Both methods are effective when used independently or when an abstracted model is passed to PDR. This paper proposes a new method of combining them by minimally changing the PDR engine. The method differs from previous work, which requires a larger implementation effort. Experiments show that the integrated engine is, on average, stronger than the baseline and produces inductive invariants that are smaller and depend on fewer variables, making them more useful in design analysis and debugging.

We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.

Reachability games are a useful formalism for the synthesis of reactive systems. Solving a reachability game involves (1) determining the winning player and (2) computing a winning strategy that determines the winning player's action in each state of the game. Recently, a new family of game solvers has been proposed, which rely on counterexample- guided search to compute winning sequences of actions represented as an abstract game tree. While these solvers have demonstrated promising performance in solving the winning determination problem, they currently do not support strategy extraction. We present the first strategy extraction algorithm for abstract game tree- based game solvers. Our algorithm performs SAT encoding of the game abstraction produced by the winner determination algorithm and uses interpolation to compute the strategy. Our experimental results show that our approach performs well on a number of software synthesis benchmarks.

Game tree Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification Abstract Game tree verificationGame tree verification

Verification benefits from removing logic that is not relevant for a proof. Techniques for doing this are known as localization abstraction. Abstraction is often performed by selecting a subset of gates to be included in the abstracted model; the signals feeding into this subset become unconstrained cut-points. In this paper, we propose several improvements to substantially increase the scalability of automated abstraction. In particular, we show how a better integration between the BMC engine and the SAT solver is achieved, resulting in a new hybrid abstraction engine, that is faster and uses less memory. This engine speeds up computation by constant propagation and circuit-based structural hashing while collecting UNSAT cores for the intermediate proofs in terms of a subset of the original variables. Experimental results show improvements in the abstraction depth and size.

This paper presents a method for translating formulas written in assertion languages such as LTL into a monitor circuit suitable for model checking. Unlike the conventional approach, no automata is generated for the property, but instead the monitor is built directly from the property formula through a recursive traversal. This method was first introduced by Pnueli et. al. under the name of Temporal Testers. In this paper, we show the practicality of temporal testers through experimental evaluation, as well as offer a self-contained exposition for how to construct them in manner that meets the requirements of industrial model checking tools. These tools tend to operate on logic circuits with sequential elements, rather than transition relations, which means we only need to consider so called positive testers with no future references. This restriction both simplifies the presentation and allows for more efficient monitors to be generated. In the final part of the paper, we suggest several possible optimizations that can improve the quality of the monitors, and conclude with experimental data.

ion Phase Design ∣ ∣ #And #PI #FF ∣ ∣ Depth 6s102 ∣ ∣ 6,594 72 1,121 → 56 ∣ ∣ 23 6s121 ∣ ∣ 1,636 99 419 → 110 ∣ ∣ 19 6s132 ∣ ∣ 1,216 94 139 → 113 ∣ ∣ 7 6s144 ∣ ∣ 41,862 480 3,337 → 236 ∣ ∣ 18 6s150 ∣ ∣ 5,448 146 1,044 → 323 ∣

In numerous EDA flows, time-consuming computations are repeatedly applied to sequential circuits. This motivates developing methods to determine what circuits have been processed already by a tool. This paper proposes an algorithm for semi-canonical labeling of nodes in a sequential AIG, allowing problems or sub-problems solved by an EDA tool to be cached with their computed results. This can speed up the tool when applied to designs with isomorphic components or design suites exhibiting substantial structural similarity.

Counter-examples are produced by formal verification engines to witness failures of safety properties. A counterexample is a sequence of input assignments bringing the design from the initial state into a state where some property fails. In practice, these input assignments contain redundancies. This paper focuses on methods for analyzing counter-examples to detect don’t-care, optional, and essential input assignments. The proposed analysis of counter-examples helps design debugging. Additionally, it is useful to reduce the length of counter-examples derived by random simulation and for efficient refinement in localization abstraction.

A Boolean network with unknown components can be modeled as an AIG with black boxes (bb-AIG). The delay of an AIG is measured in terms of its maximum level after it is balanced. We propose a delay model for a black box which is consistent in that if a bb-AIG is refined by replacing an internal black box with another bb-AIG, its delay cannot decrease. It is also tight in that there exists an AIG which can replace a black box resulting in a delay equal to the estimated one. We prove that the proposed black box delay estimation is consistent and tight.

An improved method for speculative reduction is proposed and applied to (suspected) hard verification problems. Several variations of the algorithm were tested: (a) applying speculation initially to the original problem; (b) applying speculation after simplification, before our regular model checker, super_prove is applied, as well as (c) using different filters to reduce the number of speculated equivalences tried. On the benchmarks coming from sequential equivalence checking, the speculationfirst strategy with filtering proved to be faster than super_prove. On other benchmarks that may have come from property checking, super_prove is found superior.

Mapping into K-input lookup tables (K-LUTs) is an important step in synthesis for Field-Programmable Gate Arrays (FPGAs). The traditional FPGA architecture assumes all interconnects between individual LUTs are “routable”. This paper proposes a modified FPGA architecture which allows for direct (non-routable) connections between adjacent LUTs. As a result, delay can be reduced but area may increase. This paper investigates two types of LUT structures and the associated tradeoffs. A new mapping algorithm is developed to handle such structures. Experimental results indicate that even when regular LUT structures are used, area and delay can be improved 7.4% and 11.3%, respectively, compared to the high-effort technology mapping with structural choices. When the dedicated architecture is used, the delay can be improved up to 40% at the cost of some area increase.

ion phase. The next phase employs abstractions. Usually, the CB/PB localization abstractions [8] are done first followed by refinement using a verify phase. Then speculation [3] is done, again followed by refinement using a verify phase. 1 In some rare cases, the forward diameter of the design is know, in which case BMC can be considered a complete method. 2 In theory, if the synthesis algorithms were powerful enough and the property holds, this would be all that is needed since the circuit can be reduced to a constant. Sometimes this happens. Speculation is the process where equivalences between signals in the circcuit are postulated based on extensive random or semi-formal simulation. By simplifying the circuit using the speculated equivalences, a “speculatively reduced model” is produced with additional outputs representing proof-obligations for the speculations. These obligations can be dispatched all at once or individually. Each of these sub-problems can be attacked as a separate MC problem using any of the sequence of MC engines in the arsenal. As can be imagined, the orchestration of the use of these engines and their variations becomes quite complex requiring intricate code or use of expert systems [30] [Ziv]. 4 Concurrent verify phase If there are initially many properties to be proved for the same design, the obvious way to exploit multi-cores is just to solve each property separately. However, as soon as all easy properties have been solved, we are left with the hard ones, and we claim that CPU power is better used by a welltuned concurrent engine. In the following, we describe our efforts along these lines and some experimental results. The scripting layer of our model checker 3 was modified to use a concurrent verify phase, which can fork off a subset of basic MC engines. These run concurrently as separate processes. 4 At the time of the fork, the global state of the Python interpreter and the current AIG for the problem are copied for each process. The list of basic engines that we use are: 1. Four different versions of BDD reachability, reachx, reachm, reachn, reachp 2. Four different versions of property directed reachability 5 , pdr, pdrs, pdrm, pdrmm 3. Two different implementations of bounded model checking, bmc, bmc3 4. Interpolation, interpolate 5. Repeated random simulation, simulate Each engine is given the same timeout. The fork terminates when any algorithm returns a definitive result, SAT or UNSAT, or when all engines have timed out. Only the winning result (which may include a counter-example (CEX), used for refinement) is kept. In the verify phase, the AIG is not changed, but the transformation engines used in the next section may also return a new AIG. The Python function call is “verify(list, time)”, where list is a list of engines to be run concurrently, and time is the timeout in seconds for each engine. In contrast to a sequential verify phase, the code for this is markedly simpler. 5 Deployment of a concurrent verify A rough outline of our hybrid concurrent MC algorithm called c_prove, which uses the concurrent verify is shown in Figure 1. 3 The ABC model checker is scripted in Python with the capability of orchestrating ABC or ZZ/BIP commands which are written in C or C++. 4 In our experiments we used an 8-core server running Ubuntu Linux. 5 PDR is based on Bradley’s method and program, which he called IC3.

Last spring, in March 2010, Aaron Bradley published the first truly new bit-level symbolic model checking algorithm since Ken McMillan's interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley's procedure, and discuss our successful and unsuccessful attempts to improve it.

This paper presents an efficient, combined formulation of two widely used abstraction methods for bit-level verification: counterexample-based abstraction (CBA) and proof-based abstraction (PBA). Unlike previous work, this new method is formulated as a single, incremental SAT-problem, interleaving CBA and PBA to develop the abstraction in a bottom-up fashion. It is argued that the new method is simpler conceptually and implementation-wise than previous approaches. As an added bonus, proof-logging is not required for the PBA part, which allows for a wider set of SAT-solvers to be used.

This paper presents an industrial-strength CAD system for logic optimization, technology mapping, and formal verification of synchronous designs. The new system, Magic, is based on the code of ABC that has been improved by adding industrial requirements. Distinctive features include: global-view optimizations for area and delay, scalable sequential synthesis, the use of white-boxes for instances that should not be mapped, and a built-in formal verification framework to run combinational and sequential equivalence checking. Comparison against a reference industrial flow shows that Magic is capable of reducing both area and delay. Experiments on a suite of industrial FPGA designs show that LUT count is reduced by 12.7%, flip-flop (FF) count is reduced by 9.4%, FF-to-FF level is reduced by 22.3%, and fMAX is improved by 11.8%. A remarkable consequence of these reductions is that, although Magic itself takes time to run, the total runtime of the design flow is reduced.

A well-known example is the 2001 paper by the group of Sharad Malik at Princeton, appropriately titled “Chaff: Engineering an Efficient SAT Solver” [7]. This has become one of the most cited papers on formal verification and represents a major break-through, even though the contribution of this paper is not a new theoretical formulation. The contribution was in the exploitation of the synergy between algorithms and data-structures, most of which were known before. Yet this was a break-through in SAT solver technology, and was responsible for stimulating research that led to the majority of the recent successes of formal verification.

Satisfiability solving, the problem of deciding whether the variables of a propositional formula can be assigned in such a way that the formula evaluates to true, is one of the classic problems in computer science. It is of theoretical interest because it is the canonical NP-complete problem. It is of practical interest because modern SAT-solvers can be used to solve many important and practical problems. In this tutorial paper, we show briefly how such SAT-solvers are implemented, and point to some typical applications of them. Our aim is to provide sufficient information (much of it through the reference list) to kick-start researchers from new fields wishing to apply SAT-solvers to their problems. Supervisory control theory originated within the control community and is a framework for reasoning about a plant to be controlled and a specification that the closed-loop system must fulfil. This paper aims to bridge the gap between the computer science community and the control community by illustrating how SAT-based techniques can be used to solve some supervisory control related problems.