878886
Verification of embedded memory systems using efficient memory modeling
We describe verification techniques for embedded memory systems using efficient memory modeling (EMM), without explicitly modeling each memory bit. We extend our previously proposed approach of EMM in bounded model checking (BMC) for a single read/write port single memory system, to more commonly occurring systems with multiple memories, having multiple read and write ports. More importantly, we augment such EMM to providing correctness proofs, in addition to finding real bugs as before. The novelties of our verification approach are in (a) combining EMM with a proof-based abstraction that preserves the correctness of a property up to a certain analysis depth of SAT-based BMC, and (b) modeling arbitrary initial memory state precisely and thereby providing inductive proofs using SAT-based BMC for embedded memory systems. Similar to the previous approach, we construct a verification model by eliminating memory arrays, but retaining the memory interface signals with their control logic and adding constraints on those signals at every analysis depth to preserve the data forwarding semantics. The size of these EMM constraints depends quadratically on the number of memory accesses and the number of read and write ports; and linearly on the address and data widths and the number of memories. We show the effectiveness of our approach on several industry designs and software programs.
600527
Learning from BDDs in SAT-based bounded model checking
Bounded Model Checking (BMC) based on Boolean Satisfiability (SAT) procedures has recently gained popularity as an alternative to BDD-based model checking techniques for finding bugs in large designs. In this paper, we explore the use of learning from BDDs, where learned clauses generated by BDD-based analysis are added to the SAT solver, to supplement its other learning mechanisms. We propose several heuristics for guiding this process, aimed at increasing the usefulness of the learned clauses, while reducing the overheads. We demonstrate the effectiveness of our approach on several industrial designs, where BMC performance is improved and the design can be searched up to a greater depth by use of BDD-based learning.
11387042
Predicate learning and selective theory deduction for a difference logic solver
Design and verification of systems at the register-transfer (RT) or behavioral level require the ability to reason at higher levels of abstraction. Difference logic consists of an arbitrary Boolean combination of propositional variables and difference predicates and therefore provides an appropriate abstraction. In this paper, we present several new optimization techniques for efficiently deciding difference logic formulas. We use the lazy approach by combining a DPLL Boolean SAT procedure with a dedicated graph-based theory solver, which adds transitivity constraints among difference predicates on a "need-to" basis. Our new optimization techniques include flexible theory constraint propagation, selective theory deduction, and dynamic predicate learning. We have implemented these techniques in our lazy solver. We demonstrate the effectiveness of the proposed techniques on public benchmarks through a set of controlled experiments
8665183
Dynamic detection and removal of inactive clauses in SAT with application in image computation
In this paper, we present a new technique for the efficient dynamic detection and removal of inactive clauses, i.e. clauses that do not affect the solutions of interest of a Boolean satisfiability (SAT) problem. The algorithm is based on the extraction of gate connectivity information during generation of the Boolean formula from the circuit, and its use in the inner loop of a branch-and-bound SAT algorithm. The motivation for this optimization is to exploit the circuit structure information, which can be used to find unobservable gates at circuit outputs under dynamic conditions. It has the potential to speed up all applications of SAT in which the SAT formula is derived from a logic circuit. In particular, we find that it has considerable impact on an image computation algorithm based on SAT. We present practical results for benchmark circuits which show that the use of this optimization consistently improves the performance for reachability analysis, in some cases enabling the prototype tool to reach more states than otherwise possible.
15353920
Beyond safety: customized SAT-based model checking
Model checking of safety properties has taken a significant lead over nonsafety properties in recent years. To bridge the gap, we propose dedicated SAT-based model checking algorithms for properties beyond safety. Previous bounded model checking (BMC) approaches have relied on either converting such properties to safety checking, or finding proofs by deriving termination criteria using loop-free path analysis. Instead, our approach uses a customized SAT-based formulation for bounded model checking of nonsafety properties, and determines the completeness bounds for liveness using unbounded SAT-based analysis. Our main contributions are: 1) Customized property translations for LTL formulas for BMC, with novel features that utilize partitioning, learning, and incremental formulation. Customized translations not only improve the BMC performance significantly in comparison to standard monolithic LTL translations, but also allow efficient derivation and use of completeness bounds. Though we discuss the translation schemas for liveness, they can be easily extended to handle other LTL properties as well. 2) Customized formulations for determining completeness bounds for liveness using SAT-based unbounded model checking (UMC) rather than using loop-free path analysis. These formulations comprise greatest fixed-point and least fixed-point computations to efficiently handle nested properties using SAT-based quantification approaches. We show the effectiveness of our overall approach for checking liveness on public benchmarks and several industry designs.
10395010
Abstraction and BDDs Complement SAT-Based BMC in DiVer
Bounded Model Checking (BMC) based on Boolean Satisfiability (SAT) procedures has recently gained popularity for finding bugs in large designs. However, due to its incompleteness, there is a need to perform deeper searches for counterexamples, or a proof by induction where possible. The DiVer verification platform uses abstraction and BDDs to complement BMC in the quest for completeness. We demonstrate the effectiveness of our approach in practice on industrial designs.
2840997
A survey of recent advances in SAT-based formal verification
Dramatic improvements in SAT solver technology over the last decade and the growing need for more efficient and scalable verification solutions have fueled research in verification methods based on SAT solvers. This paper presents a survey of the latest developments in SAT-based formal verification, including incomplete methods such as bounded model checking and complete methods for model checking. We focus on how the surveyed techniques formulate the verification problem as a SAT problem and how they exploit crucial aspects of a SAT solver, such as application-specific heuristics and conflict-driven learning. Finally, we summarize the noteworthy achievements in this area so far and note the major challenges in making this technology more pervasive in industrial design verification flows.
1221956
Knowledge-based integration of neuroscience data sources
The need for information integration is paramount in many biological disciplines, because of the large heterogeneity in both the types of data involved and in the diversity of approaches (physiological, anatomical, biochemical, etc.) taken by biologists to study the same or correlated phenomena. However, the very heterogeneity makes the task of information integration very difficult since two approaches studying different aspects of the same phenomena may not even share common attributes in their schema description. The paper develops a wrapper-mediator architecture which extends the conventional data- and view-oriented information mediation approach by incorporating additional knowledge modules that bridge the gap between the heterogeneous data sources. The semantic integration of the disparate local data sources employs F-logic as a data and knowledge representation and reasoning formalism. We show that the rich object oriented modeling features of F-logic together with its declarative rule language and the uniform treatment of data and metadata (schema information) make it an ideal candidate for complex integration tasks. We substantiate this claim by elaborating on our integration architecture and illustrating the approach using real world examples from the neuroscience domain. The complete integration framework is currently under development; a first prototype establishing the viability of the approach is operational.
27335258
Adaptive Connected Dominating Set - An Exercise in Distributed Output Switching
Switching between protocols based on environment is an elegant idea of enabling adaptation in distributed systems. In this paper, we give one approach of switching between two connected dominating set (CDS) construction protocols, one suitable for low load and the other suitable for higher load. In this method, the two connected dominating sets are computed in advance and switching is done between the two precomputed outputs. In addition, some CDS of the network is always maintained when switching is in progress.
3086074
An Exercise in Fault-Containment: Self-Stabilizing Leader Election
Self-stabilizing algorithms are designed to guarantee convergence to some desired stable state from arbitrary initial states arising out of an arbitrarily large number of faults. However, in a well-designed system, the simultaneous occurrence of a large number of faults is rare. It is therefore desirable to design algorithms that are not only self-stabilizing, but also have the ability to recover very fast from a bounded number of faults. As an illustration, we present a simple self-stabilizing leader election protocol that recovers in O(1) time from a state with a single transient fault on oriented rings. Only the faulty node and its two neighbors change their state during convergence to a stable state. Thus, the effect of a single fault is tightly contained around the fault. The technique for transforming a self-stabilizing algorithm into its fault-contained version is simple and general, and can be applied to other problems as well that satisfy certain properties.
8323337
Modeling Functional Data Sources as Relations
In this paper we present a model of functional access to data that, we argue, is suitable for modeling a class of data repositories characterized by functional access, such as web sites. We discuss the problem of modeling such data sources as a set of relations, of determining whether a given query expressed on these relations can be translated into a combination of functions defined by the data sources, and of finding an optimal plan to do so.