Recent years have seen significant advances in using formal verification to check hardware security properties. Of particular practical interest are checking confidentiality and integrity of secrets, by checking that there is no information flow between the secrets and observable outputs. A standard method for checking information flow is to translate the corresponding non-interference hyperproperty into a safety property on a self-composition of the design, which has two copies of the design composed together. Although prior efforts have aimed to reduce the size of the self-composed design, there are no state-of-the-art model checkers that exploit their special structure for hardware security verification. In this paper, we propose SecIC3, a hardware model checking algorithm based on IC3 that is customized to exploit this self-composition structure. SecIC3 utilizes this structure in two complementary techniques: symmetric state exploration and adding equivalence predicates. We implement SecIC3 on top of two open-source IC3 implementations and evaluate it on a non-interference checking benchmark consisting of 10 designs. The experiment results show that SecIC3 significantly reduces the time for finding security proofs, with up to 49.3x proof speedup compared to baseline implementations.

Reasoning about the correctness of distributed systems is a significant challenge, with precise correctness specifications serving as an essential prerequisite to verification. However, identifying and formulating specifications remains a major hurdle for developers in practice. Specy addresses this challenge by automatically learning specifications from observable event traces generated by message exchanges in distributed systems. The system employs a specialized grammar tailored for event-based specifications, incorporating support for quantifiers over events - a capability essential for capturing the complex behavioral patterns inherent in distributed protocols. Specy utilizes a novel learning procedure that combines grammar-based enumerative search with dynamic learning from event traces, providing effective control over the specification search. We evaluated Specy on established distributed protocols and industrial case studies, demonstrating its ability to successfully learn important protocol specifications. Specy can discover previously unidentified specifications overlooked by developers, automatically derive inductive invariants that were previously constructed manually for verification purposes, and, through run-time monitoring in production systems, reveal gaps in testing coverage - highlighting opportunities to leverage specifications in practice.

Scaling hardware formal verification (FV) has been an ongoing challenge due to the state space explosion problem. In this article, we introduce a bottom-up verification methodology that leverages design hierarchy by using sound abstractions at each level in the hierarchy to decompose the overall FV problem into a set of smaller, more manageable FV tasks.We use the recently proposed instruction-level abstraction (ILA) as a complete specification at each level of the design hierarchy. We then utilize ILA-based verification methods to check correctness of modules composed at that level. The ILA specification includes an interface specification for each module and interface checks for verifying correct intermodule communication. This approach enables compositional verification with the following guarantee: if each hardware component refines its ILA specification and passes the interface checks, then the register-transfer level composition refines the ILA composition. We then show how this compositional verification methodology facilitates a bottom-up hierarchical verification approach, where the specification at one level serves as the implementation at the next higher level. We demonstrate the increased scalability of our methodology through several case studies, including complex modules in two deep learning accelerators (FlexASR and NVDLA), where verification fails to complete on the flat designs.

Specialized hardware accelerators are increasingly utilized to provide performance/power efficiency for Deep Neural Network (DNN) applications. However their benefits are limited by expensive off-chip data movement between host memory and the accelerator’s on-chip scratchpad, which can consume significantly more energy than accelerator computation [13]. While application-level DNN operators can have arbitrary sizes, accelerators typically support fixed-sized operations due to constrained on-chip memory and micro-architectures. Consequently, mapping an application-level operator to an accelerator involves decomposing it into loops of smaller tiles. Different choices of tile sizes, loop orders and memory partition across tensors result in a vast design space with huge differences in off-chip data movement volume. To address this challenge, we introduce Shoehorn, a schedule optimization framework that jointly optimizes loop tiling, loop ordering, and memory partitioning for mapping application-level DNN operators to hardware accelerators. Shoehorn can generate optimal schedules in subseconds and outperforms state-of-the-art approaches, reducing up to 51% total off-chip memory traffic relative to competing schedulers for several widely-used DNN applications on three distinct hardware accelerator targets.

Despite recent advances in using formal methods for analyzing network performance, modeling network functionality for performance analysis remains challenging. Existing tools expect users to directly create the logical formulas corresponding to the network functionality of interest. This is often unintuitive, difficult to get right, and tightly coupled with the specific encoding and reasoning engine one chooses to use. Instead, we propose language abstractions that enable users to model network functionality and analysis tasks in an imperative solver-agnostic program, and a framework to transform them into a representation that can be analyzed by the appropriate solver. We outline our progress so far, demonstrating the potential of our approach through preliminary case studies and directions for future work.

Simulation is widely used during different stages of hardware development. This paper focuses on one specific type of simulation - cycle-accurate timing simulation, which measures the number of cycles for a given computation. We propose a pioneering approach for automatically generating cycle-accurate timing models of hardware accelerators from their RTL designs based on dependency analysis and constraint solving, making this the first technique of its kind in this domain. We demonstrate the applicability of our approach for six non-trivial designs. We show that our method achieves a 1.5x-6.9x speedup for cycle-accurate simulation over RTL models for computation-intensive accelerators, demonstrating its effectiveness. Our approach provides a cost-effective way to quickly determine the execution time of accelerators.

Fine-grained monitoring is crucial for multiple data-driven tasks such as debugging, provisioning, and securing networks. Yet, practical constraints in collecting, extracting, and storing data often force operators to use coarse-grained sampled monitoring, degrading the performance of the various tasks. In this work, we explore the feasibility of leveraging the correlations among coarse-grained time series to impute their fine-grained counterparts in software. We present Zoom2Net, a transformer-based model for network imputation that incorporates domain knowledge through operational and measurement constraints, ensuring that the imputed network telemetry time series are not only realistic but align with existing measurements. This approach enhances the capabilities of current monitoring infrastructures, allowing operators to gain more insights into system behaviors without the need for hardware upgrades. We evaluate Zoom2Net on four diverse datasets (e.g., cloud telemetry and Internet data transfer) and use cases (e.g., bursts analysis and traffic classification). We demonstrate that Zoom2Net consistently achieves high imputation accuracy with a zoom-in factor of up to 100 and performs better on downstream tasks compared to baselines by an average of 38%.

Ideally, accelerator development should be as easy as software development. Several recent design languages/tools are working toward this goal, but actually testing early designs on real applications end-to-end remains prohibitively difficult due to the costs of building specialized compiler and simulator support. We propose a new first-in-class, mostly automated methodology termed “3LA” to enable end-to-end testing of prototype accelerator designs on unmodified source applications. A key contribution of 3LA is the use of a formal software/hardware interface that specifies an accelerator’s operations and their semantics. Specifically, we leverage the Instruction-level Abstraction (ILA) formal specification for accelerators that has been successfully used thus far for accelerator implementation verification. We show how the ILA for accelerators serves as a software/hardware interface, similar to the Instruction Set Architecture for processors, that can be used for automated development of compilers and instruction-level simulators. Another key contribution of this work is to show how ILA-based accelerator semantics enables extending recent work on equality saturation to auto-generate basic compiler support for prototype accelerators in a technique we term “flexible matching.” By combining flexible matching with simulators auto-generated from ILA specifications, our approach enables end-to-end evaluation with modest engineering effort. We detail several case studies of 3LA, which uncovered an unknown flaw in a recently published accelerator and facilitated its fix.

Satisfiability Modulo Theories (SMT)-based analysis allows exhaustive reasoning over complex distributed control plane routing behaviors, enabling verification of converged routing states under arbitrary conditions. To improve scalability of SMT solving, we introduce a modular verification approach to network control plane verification, where we cut a network into smaller fragments. Users specify an annotated cut which describes how to generate these fragments from the monolithic network, and we verify each fragment independently, using these annotations to define assumptions and guarantees over fragments akin to assume-guarantee reasoning. We prove that any converged states of the fragments are converged states of the monolithic network, and there exists an annotated cut that can generate fragments corresponding to any converged state of the monolithic network. We implement this procedure as, an extension of the network verification language and tool, and evaluate it on industrial topologies with synthesized policies. We observe a 10x improvement in end-to-end verification time, with SMT solve time improving by up to 6 orders of magnitude.

Compiling high-level programs to high-speed packet-processing pipelines is a challenging combinatorial optimization problem. The compiler must configure the pipeline’s resources to match the semantics of the program’s high-level specification, while packing all of the program’s computation into the pipeline’s limited resources. State of the art approaches tackle individual aspects of this problem. Yet, they miss opportunities to produce globally high-quality outcomes within reasonable compilation times. We develop a framework to decompose the compilation problem for such pipelines into three phases—making extensive use of solver engines (e.g., ILP, SMT, and program synthesis) to simplify the development of these phases. Transformation rewrites programs to use more abundant pipeline resources, avoiding scarce ones. Synthesis breaks complex transactional code into configurations of pipelined compute units. Allocation maps the program’s compute and memory to the pipeline’s hardware resources. We prototype these ideas in a compiler, CaT, which targets (1) the Tofino programmable switch pipeline and (2) Menshen, a cycle-accurate simulator of a Verilog description of the RMT pipeline. CaT can handle programs that existing compilers cannot currently run on pipelines and generates code faster than existing compilers, where the generated code uses fewer pipeline resources.

This paper presents the Instruction-Level Abstraction (ILA) as a formal software/hardware interface for accelerator-rich platforms. The ILA provides a common framework for formal functional specification of processors and accelerator behavior, verifying their implementations, and reasoning about software-hardware interactions of programs with accelerators. The ILA-MCM specification extends the ILA to enable reasoning about interactions of accelerators with other compute engines through shared memory. The 3LA compilation flow for accelerators uses the ILA model to bridge the gap between fine-grain compiler intrinsics and coarse-grain accelerator operations.

Owing to its adaptability and scalability, Machine Learning (ML) has gained significant momentum in the networking community. Yet, ML models can still produce outputs that contradict knowledge, i.e., established networking rules and principles. On the other hand, Formal Methods (FM) use rigorous mathematical reasoning based on knowledge, but suffer from the lack of scalability. To capitalize on the complementary strengths of both approaches, we advocate for the integration of knowledge-based FM into ML-based systems for networking problems. Through a case study, we demonstrate the benefits and limitations of using ML models or FM alone. We find that incorporating FM in the training and inference of an ML model yields not only more reliable results but also better performance in various downstream tasks. We hope that our paper inspires a tighter integration of FM-based and ML-based approaches in networking, facilitating the development of more robust and dependable systems.

Verification of distributed systems using systematic exploration is daunting because of the many possible interleavings of messages and failures. When faced with this scalability challenge, existing approaches have traditionally mitigated state space explosion by avoiding exploration of redundant states (e.g., via state hashing) and redundant interleavings of transitions (e.g., via partial-order reductions). In this paper, we present an efficient symbolic exploration method that not only avoids redundancies in states and interleavings, but additionally avoids redundant computations that are performed during updates to states on transitions. Our symbolic explorer leverages a novel, fine-grained, canonical representation of distributed system configurations (states) to identify opportunities for avoiding such redundancies on-the-fly. The explorer also includes an interface that is compatible with abstractions for state-space reduction and with partial-order and other reductions for avoiding redundant interleavings. We implement our approach in the tool Psym and empirically demonstrate that it outperforms a state-of-the-art exploration tool, can successfully verify many common distributed protocols, and can scale to multiple real-world industrial case studies across

Monolithic control plane verification cannot scale to hyperscale network architectures with tens of thousands of nodes, heterogeneous network policies and thousands of network changes a day. Instead, modular verification offers improved scalability, reasoning over diverse behaviors, and robustness following policy updates. We introduce Timepiece, a new modular control plane verification system. While one class of verifiers, starting with Minesweeper, were based on analysis of stable paths, we show that such models, when deployed naïvely for modular verification, are unsound. To rectify the situation, we adopt a routing model based around a logical notion of time and develop a sound, expressive, and scalable verification engine. Our system requires that a user specifies interfaces between module components. We develop methods for defining these interfaces using predicates inspired by temporal logic, and show how to use those interfaces to verify a range of network-wide properties such as reachability or access control. Verifying a prefix-filtering policy using a non-modular verification engine times out on an 80-node fattree network after 2 hours. However, Timepiece verifies a 2,000-node fattree in 2.37 minutes on a 96-core virtual machine. Modular verification of individual routers is embarrassingly parallel and completes in seconds, which allows verification to scale beyond non-modular engines, while still allowing the full power of SMT-based symbolic reasoning.

While mixed integer linear programming (MILP) solvers are routinely used to solve a wide range of important science and engineering problems, it remains a challenging task for end users to write correct and efficient MILP constraints, especially for problems specified using the inherently non-linear Boolean logic operations. To overcome this challenge, we propose a syntax guided synthesis (SyGuS) method capable of generating high-quality MILP constraints from the specifications expressed using arbitrary combinations of Boolean logic operations. At the center of our method is an extensible domain specification language (DSL) whose expressiveness may be improved by adding new integer variables as decision variables, together with an iterative procedure for synthesizing linear constraints from non-linear Boolean logic operations using these integer variables. To make the synthesis method efficient, we also propose an over-approximation technique for soundly proving the correctness of the synthesized linear constraints, and an under-approximation technique for safely pruning away the incorrect constraints. We have implemented and evaluated the method on a wide range of benchmark specifications from statistics, machine learning, and data science applications. The experimental results show that the method is efficient in handling these benchmarks, and the quality of the synthesized MILP constraints is close to, or higher than, that of manually-written constraints in terms of both compactness and solving time.

In modern systems-on-chips, several hardware protocols are used for communication and interaction among different modules. These protocols are complex and need to be implemented correctly for correct operation of the system-on-chip. Therefore, protocol verification has received significant attention. However, this verification is often limited to checking high-level properties on a protocol specification or an implementation. Verifying these properties directly on an implementation faces scalability challenges due to its size and design complexity. Further, even after some high-level properties are verified, there is no guarantee that an implementation fully complies with a given specification, even if the same properties have also been checked on the specification. We address these challenges and gaps by adding a layer of component specifications, one for each component in the protocol implementation, and specifying and verifying the interactions at the interfaces between each pair of communicating components. We use the recently proposed formal model termed Instruction-Level Abstraction (ILA) as a component specification, which includes an interface specification for the interactions in composing different components. The use of ILA models as component specifications allows us to decompose the complete verification task into two sub-tasks: checking that the composition of ILAs is sequentially equivalent to a verified formal protocol specification, and checking that the protocol implementation is a refinement of the ILA composition. This check requires that each component implementation is a refinement of its ILA specification and includes interface checks guaranteeing that components interact with each other as specified. We have applied the proposed ILA-based methodology for protocol verification to several third-party design case studies. These include an AXI on-chip communication protocol, an off-chip communication protocol, and a cache coherence protocol. For each system, we successfully detected bugs in the implementation, and show that the full formal verification can be completed in reasonable time and effort.

Simulation-based testing has been the workhorse of hardware implementation validation. For processors, tandem simulation improves test and debug efficiency by cross-level simulating the Instruction Set Architecture (ISA) and RTL models, and comparing architectural-state variables at the end of each instruction rather than at the end of the whole trace. Further, the simulation may start with the ISA model and switch to the RTL model at some point by transferring the values of the architectural variables, thus speeding up the “warm-up” phase. However, thus far tandem simulation has been limited to processor designs as other SoC components lack high-level ISA models and thus the notion of instructions. Even for processors, significant manual effort is required in connecting the two models and constructing the necessary controller to synchronize/check/swap between them. This paper leverages the recently proposed Instruction-level Abstractions (ILAs) for generalizing tandem simulation to accelerators. Further, we use the refinement-map that is part of the ILA verification methodology to automate the connection between the ILA and the RTL simulation models for both processors and accelerators. We provide seven case studies to demonstrate the practical applicability of our methodology.

Hardware platforms comprise general-purpose processors and application-specific accelerators. Unlike processors, application-specific accelerators often do not have clearly specified architecture-level models/specifications (the instruction set architecture or ISA). This poses challenges to the development and verification/validation of firmware/software for these accelerators. Manually writing architecture-level models takes great effort and is error-prone. When Register-Transfer Level (RTL) designs are available, they can be a source from which to automatically derive the architecture-level models. In this work, we propose an approach for automatically generating architecture-level models for processors as well as accelerators from their RTL designs. In previous work we showed how to automatically extract the architectural state variables (ASVs) from RTL designs. (These are the state variables that are persistent across instructions.) In this work we present an algorithm for generating the update functions of the model: how the ASVs and outputs are updated by each instruction. Experiments on several processors and accelerators demonstrate that our approach can cover a wide range of hardware features and generate high-quality architecture-level models within reasonable time.

Error-correction codes (ECCs) are becoming a de rigueur feature in modern memory subsystems, as it becomes increasingly important to safeguard data against random bit corruption.ECC architecture constantly evolves towards designs that leverage complex mathematics to minimize check-bits and maximize the number of data bits protected, as a result of which subtle bugs may be introduced into the design.These algorithms traverse a vast data space and are subject to corner case bugs which are hard to catch through constraint-based randomized testing.This necessitates formal verification of ECC designs to assure correctness of the algorithm and its hardware implementation.In this paper we present a technique of representing various ECC algorithm outputs as Boolean equations in the form of Boolean Decision Diagrams (BDDs) to facilitate reasoning about the algorithms.We also discuss the counting and generation of examples from the BDD representations and how it aids in tuning ECC algorithms for performance and security.Additionally, we display the use of Symbolic Trajectory Evaluation (STE) to prove the correctness of register transfer level (RTL) implementations of these algorithms.We discuss the scaling up of this verification methodology, using different complexity and convergence techniques.We apply these techniques to a number of complex ECC designs at Intel and showcase their efficacy on several categories of bugs.

Recent years have witnessed increasing use of domain-specific accelerators in computing platforms to provide power-performance efficiency for emerging applications. To increase their applicability within the domain, these accelerators tend to support a large set of functions, e.g. Nvidia's open-source Deep Learning Accelerator, NVDLA, supports five distinct groups of functions [17]. However, an individual use case of an accelerator may utilize only a subset of these functions. The unused functions lead to unnecessary overhead of silicon area, power, and hardware verification/hardware-software co-verification complexity. This motivates our research question: Given an RTL design for an accelerator and a subset of functions of interest, can we automatically extract a subset of the RTL that is sufficient for these functions and sequentially equivalent to the original RTL? We call this the Usage-based RTL Subsetting problem, referred to as the RTL subsetting problem in short. We first formally define this problem and show that it can be formulated as a program synthesis problem, which can be solved by performing expensive hyperproperty checks. To overcome the high cost, we propose multiple levels of sound over-approximations to construct an effective algorithm based on relatively less expensive temporal property checking and taint analysis for information flow checking. We demonstrate the acceptable computation cost and the quality of the results of our algorithm through several case studies of accelerators from different domains. The applicability of our proposed algorithm can be seen in its ability to subset the large NVDLA accelerator (with over 50,000 registers and 1,600,000 gates) for the group of convolution functions, where the subset reduces the total number of registers by 18.6% and the total number of gates by 37.1%.

Property-based specification s uch a s SystemVerilog Assertions (SVA) uses mathematical logic to specify the temporal behavior of RTL designs which can then be formally verified using model checking algorithms. These properties are specified for a single component (which may contain other components in the design hierarchy). Composing design components that have already been verified requires additional verification since incorrect communication at their interface may invalidate the properties that have been checked for the individual components. This paper focuses on a specification for their interface which can be checked individually for each component, and which guarantees that refinement-based properties checked for each component continue to hold after their composition. We do this in the setting of the Instruction-level Abstraction (ILA) specification and verification methodology. The ILA methodology provides a uniform specification for processors, accelerators and general modules at the instruction-level, and the automatic generation of a complete set of correctness properties for checking that the RTL model is a refinement of the ILA specification. We add an interface specification to model the inter-ILA communication. Further, we use our interface specification to generate a set of interface checking properties that check that the communication between the RTL components is correct. This provides the following guarantee: if each RTL component is a refinement of its ILA specification and the interface checks pass, then the RTL composition is a refinement of the ILA composition. We have applied the proposed methodology to six case studies including parts of large-scale designs such as parts of the FlexASR and NVDLA machine learning accelerators, demonstrating the practical applicability of our method.

Satisfiability Modulo Theories (SMT)-based analysis allows exhaustive reasoning over complex distributed control plane routing behaviors, enabling verification of routing under arbitrary conditions. To improve scalability of SMT solving, we introduce a modular verification approach to network control plane verification, where we cut a network into smaller fragments. Users specify an annotated cut which describes how to generate these fragments from the monolithic network, and we verify each fragment independently, using these annotations to define assumptions and guarantees over fragments akin to assume-guarantee reasoning. We prove this modular network verification procedure is sound and complete with respect to verification over the monolithic network. We implement this procedure as Kirigami, an extension of NV [25] - a network verification language and tool - and evaluate it on industrial topologies with synthesized policies. We observe a 10x improvement in end-to-end NV verification time, with SMT solve time improving by up to 6 orders of magnitude.

Abstract Symbolic model checking is an important tool for finding bugs (or proving the absence of bugs) in modern system designs. Because of this, improving the ease of use, scalability, and performance of model checking tools and algorithms continues to be an important research direction. In service of this goal, we present , an open-source SMT-based model checker. is designed to be both a research platform for developing and improving model checking algorithms, as well as a performance-competitive tool that can be used for academic and industry verification applications. In addition to performance, prioritizes transparency (developed as an open-source project on GitHub), flexibility ( can be adapted to a variety of tasks by exploiting its general SMT-based interface), and extensibility (it is easy to add new algorithms and new back-end solvers). In this paper, we describe the design of the tool with a focus on the flexible and extensible architecture, cover its current capabilities, and demonstrate that is competitive with state-of-the-art tools.

For processors, an instruction-set-architecture (ISA) provides a complete functional specification that can be used to formally verify an implementation. There has been recent work in specifying accelerators using formal instruction sets, referred to as Instruction-Level Abstractions (ILAs), and using them to formally verify their implementations by leveraging processor verification techniques. In this paper, we generalize ILAs for specification of general hardware modules and formal verification of their RTL implementations. This includes automated generation of a complete set of functional (not including timing) specification properties using the ILA instructions. We address the challenges posed by this generalization and provide several case studies to demonstrate the applicability of this technique, including all the modules in an open-source 8051 micro-controller. This verification identified three bugs and completed in reasonable time.

Today's Systems-on-Chips (SoCs) comprise general/special purpose programmable processors and specialized hardware modules referred to as accelerators. These accelerators serve as co-processors and are invoked through software or firmware. Thus, verifying SoCs requires co-verification of hardware with software/firmware. Co-verification using cycle-accurate hardware models is often not scalable, and requires hardware abstractions. Among various abstractions, architecture-level abstractions are very effective as they retain only the software visible state. An Instruction-Set Architecture (ISA) serves this role for processors and such ISA-like abstractions are also desirable for accelerators. Manually creating such abstractions for accelerators is tedious and error-prone, and there is a growing need for automation in deriving them from existing Register-Transfer Level (RTL) implementations. An important part of this automation is determining which state variables to retain in the abstract model. For processors and accelerators, this set of variables is naturally the Architectural State Variables (ASVs) - variables that are persistent across instructions. This paper presents the first work to automatically determine ASVs of processors and accelerators from their RTL implementations. We propose three novel algorithms based on different characteristics of ASVs. Each algorithm provides a sound abstraction, i.e., an over-approximate set of ASVs. The quality of the abstraction is measured by the size of the set of ASVs computed. Experiments on several processors and accelerators demonstrate that these algorithms perform best in different cases, and by combining them a high quality set of ASVs can be found in reasonable time.

Recurrent Neural Networks (RNNs) are one of the most successful neural network architectures that deal with temporal sequences, e.g., speech and text recognition. Recently, RNNs have been shown to be useful in cognitive neuroscience as a model of decision-making. RNNs can be trained to solve the same behavioral tasks performed by humans and other animals in decision-making experiments, allowing for a direct comparison between networks and experimental subjects. Analysis of RNNs is expected to be a simpler problem than the analysis of neural activity. However, in practice, reasoning about an RNN's behaviour is a challenging problem. In this work, we take an approach based on formal verification for the analysis of RNNs. We make two main contributions. First, we consider the cognitive domain and formally define a set of useful properties to analyse for a popular experimental task. Second, we employ and adapt wellknown verification techniques for reachability analysis to our focus domain, i.e., polytope propagation, invariant detection, and counter-example-guided abstraction refinement. Our experiments show that our techniques can effectively solve classes of benchmark problems that are challenging for state-of-the-art verification tools.

Verifying secure information flow by reducing it to safety verification is a popular approach, based on constructing product programs or self-compositions of given programs.However, most such existing efforts are non-modular, i.e., they do not infer relational specifications for procedures in interprocedural programs.Such relational specifications can help to verify security properties in a modular fashion, e.g., for verifying clients of library APIs.They also provide security contracts at procedure boundaries to aid code understanding and maintenance.There has been recent interest in constructing modular product programs, but where users are required to provide procedure summaries and related annotations.In this work, we propose to automatically infer relational specifications for procedures in modular product programs.Our approach uses syntax-guided synthesis techniques and grammar templates that target verification of secure information flow properties.This enables automation of modular verification for such properties, thereby reducing the annotation burden.We have implemented our techniques on top of a solver for constrained Horn clauses (CHC).Our evaluation demonstrates that our tool is capable of inferring adequate relational specifications for procedures without requiring annotations.Furthermore, it outperforms an existing state-of-the-art hyperproperty verifier and a modular CHC-based verifier on benchmarks with loops or recursion.

Writing packet-processing programs for programmable switch pipelines is challenging because of their all-or-nothing nature: a program either runs at line rate if it can fit within pipeline resources, or does not run at all. It is the compiler's responsibility to fit programs into pipeline resources. However, switch compilers, which use rewrite rules to generate switch machine code, often reject programs because the rules fail to transform programs into a form that can be mapped to a pipeline's limited resources---even if a mapping actually exists.

Abstract Fixpoint logics have recently been drawing attention as common foundations for automated program verification. We formalize fold/unfold transformations for fixpoint logic formulas and show how they can be used to enhance a recent fixpoint-logic approach to automated program verification, including automated verification of relational and temporal properties. We have implemented the transformations in a tool and confirmed its effectiveness through experiments.

The control plane of most computer networks runs distributed routing protocols that determine if and how traffic is forwarded. Errors in the configuration of network control planes frequently knock down critical online services, leading to economic damage for service providers and significant hardship for users. Validation via ahead-of-time simulation can help find configuration errors but such techniques are expensive or even intractable for large industrial networks. We explore the use of abstract interpretation to address this fundamental scaling challenge and find that the right abstractions can reduce the asymptotic complexity of network simulation. Based on this observation, we build a tool called ShapeShifter for reachability analysis. On a suite of 127 production networks from a large cloud provider, ShapeShifter provides an asymptotic improvement in runtime and memory over the state-of-the-art simulator. These gains come with a minimal loss in precision. Our abstract analysis accurately predicts reachability for all destinations for 95% of the networks and for most destinations for the remaining 5%. We also find that abstract interpretation of network control planes not only speeds up existing analyses but also facilitates new kinds of analyses. We illustrate this advantage through a new destination "hijacking" analysis for the border gateway protocol (BGP), the globally-deployed routing protocol.

Programs with arrays are ubiquitous. Automated reasoning about arrays necessitates discovering properties about ranges of elements at certain program points. Such properties are formally specified by universally quantified formulas, which are difficult to find, and difficult to prove inductive. In this paper, we propose an algorithm based on an enumerative search that discovers quantified invariants in stages. First, by exploiting the program syntax, it identifies ranges of elements accessed in each loop. Second, it identifies potentially useful facts about individual elements and generalizes them to hypotheses about entire ranges. Finally, by applying recent advances of SMT solving, the algorithm filters out wrong hypotheses. The combination of properties is often enough to prove that the program meets a safety specification. The algorithm has been implemented in a solver for Constrained Horn Clauses, Freq-Horn, and extended to deal with multiple (possibly nested) loops. We show that FreqHorn advances state-of-the-art on a wide range of public array-handling programs.

We present a fast and scalable testing approach for datacenter/cloud systems such as Cassandra, Hadoop, Spark, and ZooKeeper. The uniqueness of our approach is in its ability to overcome the path/state-space explosion problem in testing workloads with complex interleavings of messages and faults. We introduce three powerful algorithms: state symmetry, event independence, and parallel flips, which collectively makes our approach on average 16x (up to 78x) faster than other state-of-the-art solutions. We have integrated our techniques with 8 popular datacenter systems, successfully reproduced 12 old bugs, and found 10 new bugs --- all were done without random walks or manual checkpoints.

We present ILAng, a platform for modeling and verification of systems-on-chip (SoCs) using Instruction-Level Abstractions (ILA). The ILA formal model targeting the hardware-software interface enables a clean separation of concerns between software and hardware through a unified model for heterogeneous processors and accelerators. Top-down it provides a specification for functional verification of hardware, and bottom-up it provides an abstraction for software/hardware co-verification. ILAng provides a programming interface for (i) constructing ILA models (ii) synthesizing ILA models from templates using program synthesis techniques (iii) verifying properties on ILA models (iv) behavioral equivalence checking between different ILA models, and between an ILA specification and an implementation. It also provides for translating models and properties into various languages (e.g., Verilog and SMT LIB2) for different verification settings and use of third-party verification tools. This paper demonstrates selected capabilities of the platform through case studies. Data or code related to this paper is available at: [ 9 ].

Modern Systems-on-Chip (SoC) designs are increasingly heterogeneous and contain specialized semi-programmable accelerators in addition to programmable processors. In contrast to the pre-accelerator era, when the ISA played an important role in verification by enabling a clean separation of concerns between software and hardware, verification of these “accelerator-rich” SoCs presents new challenges. From the perspective of hardware designers, there is a lack of a common framework for formal functional specification of accelerator behavior. From the perspective of software developers, there exists no unified framework for reasoning about software/hardware interactions of programs that interact with accelerators. This article addresses these challenges by providing a formal specification and high-level abstraction for accelerator functional behavior. It formalizes the concept of an Instruction Level Abstraction (ILA), developed informally in our previous work, and shows its application in modeling and verification of accelerators. This formal ILA extends the familiar notion of instructions to accelerators and provides a uniform, modular, and hierarchical abstraction for modeling software-visible behavior of both accelerators and programmable processors. We demonstrate the applicability of the ILA through several case studies of accelerators (for image processing, machine learning, and cryptography), and a general-purpose processor (RISC-V). We show how the ILA model facilitates equivalence checking between two ILAs, and between an ILA and its hardware finite-state machine (FSM) implementation. Further, this equivalence checking supports accelerator upgrades using the notion of ILA compatibility, similar to processor upgrades using ISA compatibility.

We present new algorithms for proving program termination and non-termination using syntax-guided synthesis. They exploit the symbolic encoding of programs and automatically construct a formal grammar for symbolic constraints that are used to synthesize either a termination argument or a non-terminating program refinement. The constraints are then added back to the program encoding, and an off-the-shelf constraint solver decides on their fitness and on the progress of the algorithms. The evaluation of our implementation, called Freq-Term , shows that although the formal grammar is limited to the syntax of the program, in the majority of cases our algorithms are effective and fast. Importantly, FreqTerm is competitive with state-of-the-art on a wide range of terminating and non-terminating benchmarks, and it significantly outperforms state-of-the-art on proving non-termination of a class of programs arising from large-scale Event-Condition-Action systems. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Relational safety specifications describe multiple runs of the same program or relate the behaviors of multiple programs. Approaches to automatic relational verification often compose the programs and analyze the result for safety, but a naively composed program can lead to difficult verification problems. We propose to exploit relational specifications for simplifying the generated verification subtasks. First, we maximize opportunities for synchronizing code fragments. Second, we compute symmetries in the specifications to reveal and avoid redundant subtasks. We have implemented these enhancements in a prototype for verifying k -safety properties on Java programs. Our evaluation confirms that our approach leads to a consistent performance speedup on a range of benchmarks. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

The secure information flow problem, which checks whether low-security outputs of a program are influenced by high-security inputs, has many applications in verifying security properties in programs. In this paper we present lazy self-composition, an approach for verifying secure information flow. It is based on self-composition, where two copies of a program are created on which a safety property is checked. However, rather than an eager duplication of the given program, it uses duplication lazily to reduce the cost of verification. This lazy self-composition is guided by an interplay between symbolic taint analysis on an abstract (single copy) model and safety verification on a refined (two copy) model. We propose two verification methods based on lazy self-composition. The first is a CEGAR-style procedure, where the abstract model associated with taint analysis is refined, on demand, by using a model generated by lazy self-composition. The second is a method based on bounded model checking, where taint queries are generated dynamically during program unrolling to guide lazy self-composition and to conclude an adequate bound for correctness. We have implemented these methods on top of the SeaHorn verification platform and our evaluations show the effectiveness of lazy self-composition.

Formal security verification of firmware interacting with hardware in modern Systems-on-Chip (SoCs) is a critical research problem. This faces the following challenges: (1) design complexity and heterogeneity, (2) semantics gaps between software and hardware, (3) concurrency between firmware/hardware and between Intellectual Property Blocks (IPs), and (4) expensive bit-precise reasoning. In this paper, we present a co-verification methodology to address these challenges. We model hardware using the Instruction-Level Abstraction (ILA), capturing firmware-visible behavior at the architecture level. This enables integrating hardware behavior with firmware in each IP into a single thread. The co-verification with multiple firmware across IPs is formulated as a multi-threaded program verification problem, for which we leverage software verification techniques. We also propose an optimization using abstraction to prevent expensive bit-precise reasoning. The evaluation of our methodology on an industry SoC Secure Boot design demonstrates its applicability in SoC security verification.

A Constrained Horn Clause (CHC) is a logical implication involving unknown predicates. Systems of CHCs are widely used to verify programs with arbitrary loop structures: interpretations of unknown predicates, which make every CHC in the system true, represent the program's inductive invariants. In order to find such solutions, we propose an algorithm based on Syntax-Guided Synthesis. For each unknown predicate, it generates a formal grammar from all relevant parts of the CHC system (i.e., using syntax). Grammars are further enriched by predicates and constants guessed from models of various unrollings of the CHC system (i.e., using data). We propose an iterative approach to guess and check candidates for multiple unknown predicates. At each iteration, only a candidate for one unknown predicate is sampled from its grammar, but then it gets propagated to candidates of the remaining unknowns through implications in the CHC system. Finally, an SMT solver is used to decide if the system of candidates contributes towards a solution or not. We present an evaluation of the algorithm on a range of benchmarks originating from program verification tasks and show that it is competitive with state-of-the-art in CHC solving.

Modern Systems-on-Chip (SoCs) integrate heterogeneous compute elements ranging from non-programmable specialized accelerators to programmable CPUs and GPUs. To ensure correct system behavior, SoC verification techniques must account for inter-component interactions through shared memory, which necessitates reasoning about memory consistency models (MCMs) This paper presents ILA-MCM, a symbolic reasoning framework for automated SoC verification, where MCMs are integrated with Instruction-Level Abstractions (ILAs) that have been recently proposed to model architecture-level program-visible states and state updates in heterogeneous SoC components. ILA-MCM enables reasoning about system-wide properties that depend on functional state updates as well as ordering relations between them. Central to our approach is a novel facet abstraction, where a single program-visible variable is associated with potentially multiple facets that act as auxiliary state variables. Facets are updated by ILA "instructions," and the required orderings between these updates are captured by MCM axioms. Thus, facets provide a symbolic constraint-based integration between operational ILA models and axiomatic MCM specifications. We have implemented a prototype ILA-MCM framework and use it to demonstrate two verification applications in this paper: (a) finding a known bug in an accelerator-based SoC, plus a new potential bug under a weaker MCM, and (b) checking that a recently proposed low-level GPU hardware implementation is correct with respect to a high-level ILA-MCM specification.

GPUs have been widely used to accelerate big-data inference applications and scientific computing through their parallelized hardware resources and programming model. Their extreme parallelism increases the possibility of bugs such as data races and un-coalesced memory accesses, and thus verifying program correctness is critical. State-of-the-art GPU program verification efforts mainly focus on analyzing application-level programs, e.g., in C, and suffer from the following limitations: (1) high false-positive rate due to coarse-grained abstraction of synchronization primitives, (2) high complexity of reasoning about pointer arithmetic, and (3) keeping up with an evolving API for developing application-level programs. In this paper, we address these limitations by modeling GPUs and reasoning about programs at the instruction level. We formally model the Nvidia GPU at the parallel execution thread (PTX) level using the recently proposed Instruction-Level Abstraction (ILA) model for accelerators. PTX is analogous to the Instruction-Set Architecture (ISA) of a general-purpose processor. Our formal ILA model of the GPU includes non-synchronization instructions as well as all synchronization primitives, enabling us to verify multithreaded programs. We demonstrate the applicability of our ILA model in scalable GPU program verification of data-race checking. The evaluation shows that our checker outperforms state-of-the-art GPU data race checkers with fewer false-positives and improved scalability.

Memory consistency models (MCMs) specify rules which constrain the values that can be returned by load instructions in parallel programs. To ensure that parallel programs run correctly, verification of hardware MCM implementations would ideally be complete; i.e. verified as being correct across all possible executions of all possible programs. However, no existing automated approach is capable of such complete verification. To help fill this verification gap, we present PipeProof, a methodology and tool for complete MCM verification of an axiomatic microarchitectural (hardware-level) ordering specification against an axiomatic ISA-level MCM specification. PipeProof can automatically prove a microarchitecture correct in all cases, or return an indication (often a counterexample) that the microarchitecture could not be verified. To accomplish unbounded verification, PipeProof introduces the novel Transitive Chain Abstraction to represent microarchitectural executions of an arbitrary number of instructions using only a small, finite number of instructions. With the help of this abstraction, PipeProof proves microarchitectural correctness using an automatic abstraction refinement approach. PipeProof's implementation also includes algorithmic optimizations which improve runtime by greatly reducing the number of cases considered. As a proof-of-concept study, we present results for modelling and proving correct simple microarchitectures implementing the SC and TSO MCMs. PipeProof verifies both case studies in under an hour, showing that it is indeed possible to automate microarchitectural MCM correctness proofs.

We develop an algorithm capable of compressing large networks into smaller ones with similar control plane behavior: For every stable routing solution in the large, original network, there exists a corresponding solution in the compressed network, and vice versa. Our compression algorithm preserves a wide variety of network properties including reachability, loop freedom, and path length. Consequently, operators may speed up network analysis, based on simulation, emulation, or verification, by analyzing only the compressed network. Our approach is based on a new theory of control plane equivalence. We implement these ideas in a tool called Bonsai and apply it to real and synthetic networks. Bonsai can shrink real networks by over a factor of 5 and speed up analysis by several orders of magnitude.

Modern system-on-chip (SoC) designs comprise programmable cores, application-specific accelerators, and I/O devices. Accelerators are controlled by software/firmware and functionality is implemented by this combination of programmable cores, firmware, and accelerators. Verification of such SoCs is challenging, especially for system-level properties maintained by a combination of firmware and hardware. Attempting to formally verify the full SoC design with both firmware and hardware is not scalable, while separate verification can miss bugs. A general technique for scalable system-level verification is to construct an abstraction of SoC hardware and verify firmware/software using it. There are two challenges in applying this technique in practice. Constructing the abstraction to capture required details and interactions is error-prone and time-consuming. The second is ensuring abstraction correctness so that properties proven with it are valid. This paper introduces a methodology for SoC design and verification based on the synthesis of instruction-level abstractions (ILAs). The ILA is an abstraction of SoC hardware which models updates to firmware-visible state at the granularity of instructions. For hardware accelerators, the ILA is analogous to the instruction-set architecture definition for programmable processors and enables scalable verification of firmware interacting with hardware accelerators. To alleviate the disadvantages of manual construction of abstractions, we introduce two algorithms for synthesis of ILAs from partial description called templates. We then show how the ILA can be verified to be correct. We evaluate the methodology using a small SoC design consisting of the 8051 microcontroller and two cryptographic accelerators. The methodology uncovered 15 bugs.

We present Minesweeper, a tool to verify that a network satisfies a wide range of intended properties such as reachability or isolation among nodes, waypointing, black holes, bounded path length, load-balancing, functional equivalence of two routers, and fault-tolerance. Minesweeper translates network configuration files into a logical formula that captures the stable states to which the network forwarding will converge as a result of interactions between routing protocols such as OSPF, BGP and static routes. It then combines the formula with constraints that describe the intended property. If the combined formula is satisfiable, there exists a stable state of the network in which the property does not hold. Otherwise, no stable state (if any) violates the property. We used Minesweeper to check four properties of 152 real networks from a large cloud provider. We found 120 violations, some of which are potentially serious security vulnerabilities. We also evaluated Minesweeper on synthetic benchmarks, and found that it can verify rich properties for networks with hundreds of routers in under five minutes. This performance is due to a suite of model-slicing and hoisting optimizations that we developed, which reduce runtime by over 460x for large networks.

Programming with tasks is a promising approach to write performance portable parallel code. In this model, the programmer explicitly specifies tasks and the task parallel runtime employs work stealing to distribute tasks among threads. Similar to multithreaded programs, task parallel programs can also exhibit data races. Unfortunately, prior data race detectors for task parallel programs either run the program serially or do not handle locks, and/or detect races only in the schedule observed by the analysis. This paper proposes PTRacer, a parallel on-the-fly data race detector for task parallel programs that use locks. PTRacer detects data races not only in the observed schedule but also those that can happen in other schedules (which are permutations of the memory operations in the observed schedule) for a given input. It accomplishes the above goal by leveraging the dynamic execution graph of a task parallel execution to determine whether two accesses can happen in parallel and by maintaining constant amount of access history metadata with each distinct set of locks held for each shared memory location. To detect data races (beyond the observed schedule) in programs with branches sensitive to scheduling decisions, we propose static compiler instrumentation that records memory accesses that will be executed in the other path with simple branches. PTRacer has performance overheads similar to the state-of-the-art race detector for task parallel programs, SPD3, while detecting more races in programs with locks.

Symbolic execution is a powerful technique for systematic testing of sequential and multithreaded programs. However, its application is limited by the high cost of covering all feasible intra-thread paths and inter-thread interleavings. We propose a new assertion guided pruning framework that identifies executions guaranteed not to lead to an error and removes them during symbolic execution. By summarizing the reasons why previously explored executions cannot reach an error and using the information to prune redundant executions in the future, we can soundly reduce the search space. We also use static concurrent program slicing and heuristic minimization of symbolic constraints to further reduce the computational overhead. We have implemented our method in the Cloud9 symbolic execution tool and evaluated it on a large set of multithreaded C/C++ programs. Our experiments show that the new method can reduce the overall computational cost significantly.

Cloud systems have become ubiquitous today -- they are used to store and process the tremendous amounts of data being generated by Internet users. These systems run on hundreds of commodity machines, and have a huge amount of non-determinism (thousands of threads and hundreds of processes) in their execution. Therefore, bugs that occur in cloud systems are hard to understand, reproduce, and fix. The state-of-the-art of debugging in the industry is to log messages during execution, and refer to those messages later in case of errors. In ReproLite, we augment the already widespread process of debugging using logs by enabling testers to quickly and easily specify the conjectures that they form regarding the cause of an error (or bug) from execution logs, and to also automatically validate those conjectures.

There is a strong trend in networking to move towards Software-Defined Networks (SDN). SDNs enable easier network configuration through a separation between a centralized controller and a distributed data plane comprising a network of switches. The controller implements network policies through installing rules on switches. Recently the "Big Switch" abstraction [1] was proposed as a specification mechanism for high-level network behavior, i.e., the network policies. The network operating system or compiler can use his specification for placing rules on individual switches. However, this is constrained by the limited capacity of the Ternary Content Addressable Memories (TCAMs) used for rules in each switch. We propose an Integer Linear Programming (ILP) based solution for placing rules on switches for a given firewall policy while optimizing for the total number of rules and meeting the switch capacity constraints. Experimental results demonstrate that our approach is scalable to practical sized networks.

The ever-increasing reliance of today's society on software requires scalable and precise techniques for checking the correctness, reliability, and robustness of software. Object-oriented languages have been used extensively to build large-scale systems, including Java and C++. While many scalable static analysis approaches for C and Java have been proposed, there has been comparatively little work on the static analysis of C++ programs. In this paper, we provide an abstract representation to model C++ objects, containers, references, raw pointers, and smart pointers. Further, we present a new analysis called lifetime dependency analysis, which allows us to precisely track the complex lifetime semantics of temporary objects in C++. Finally, we propose an implementation of our techniques and present promising %experimental results on a large variety of open-source software.

In industry, software testing and coverage-based metrics are the predominant techniques to check correctness of software. This paper addresses automatic unit test generation for programs written in C/C++. The main idea is to improve the coverage obtained by feedback-directed random test generation methods, by utilizing concolic execution on the generated test drivers. Furthermore, for programs with numeric computations, we employ non-linear solvers in a lazy manner to generate new test inputs. These techniques significantly improve the coverage provided by a feedback-directed random unit testing framework, while retaining the benefits of full automation. We have implemented these techniques in a prototype platform, and describe promising experimental results on a number of C/C++ open source benchmarks.

We present a Monte-Carlo optimization technique for finding system behaviors that falsify a metric temporal logic (MTL) property. Our approach performs a random walk over the space of system inputs guided by a robustness metric defined by the MTL property. Robustness is guiding the search for a falsifying behavior by exploring trajectories with smaller robustness values. The resulting testing framework can be applied to a wide class of cyber-physical systems (CPS). We show through experiments on complex system models that using our framework can help automatically falsify properties with more consistency as compared to other means, such as uniform sampling.

Testing and debugging multi-threaded programs are notoriously difficult due to non-determinism not only in inputs but also in OS schedules. In practice, dynamic analysis and failure replay systems instrument the program to record events of interest in the test execution, e.g., program inputs, accesses to shared objects, synchronization operations, context switches, etc. To reduce the overhead of logging during runtime, these testing and debugging efforts have proposed tradeoffs for sampling or selective logging, at the cost of reducing coverage or performing more expensive search offline.

introduction Share on Introduction to special section on verification challenges in the concurrent world Authors: Sandip Ray University of Texas at Austin, TX University of Texas at Austin, TXView Profile , Jayanta Bhadra Freescale Semiconductor Inc., Austin, TX Freescale Semiconductor Inc., Austin, TXView Profile , Magdy S. Abadir Freescale Semiconductor Inc., Austin, TX Freescale Semiconductor Inc., Austin, TXView Profile , Li-C. Wang University of California at Santa Barbara, CA University of California at Santa Barbara, CAView Profile , Aarti Gupta NEC Laboratories America, Inc., Princeton, NJ NEC Laboratories America, Inc., Princeton, NJView Profile Authors Info & Claims ACM Transactions on Design Automation of Electronic SystemsVolume 17Issue 3June 2012 Article No.: 19pp 1–3https://doi.org/10.1145/2209291.2209292Published:05 July 2012Publication History 0citation172DownloadsMetricsTotal Citations0Total Downloads172Last 12 Months1Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

Shared-memory multi-threaded programs are notoriously difficult to test, and because of the often astronomically large number of thread schedules, testing all possible interleavings is practically infeasible. In this paper we propose a coverage-guided systematic testing framework, where we use dynamically learned ordering constraints over shared object accesses to select only high-risk interleavings for test execution. An interleaving is of high-risk if it has not been covered by the ordering constraints, meaning that it has concurrency scenarios that have not been tested. Our method consists of two components. First, we utilize dynamic information collected from good test runs to learn ordering constraints over the memory-accessing and synchronization statements. These ordering constraints are treated as likely invariants since they are respected by all the tested runs. Second, during the process of systematic testing, we use the learned ordering constraints to guide the selection of interleavings for future test execution. Our experiments on public domain multithreaded C/C++ programs show that, by focusing on only the high-risk interleavings rather than enumerating all possible interleavings, our method can increase the coverage of important concurrency scenarios with a reasonable cost and detect most of the concurrency bugs in practice.

We present a tool BEST (Binary instrumentation-based Error-directed Symbolic Testing) for predicting concurrency violations.1We automatically infer potential concurrency violations such as atomicity violations from an observed run of a multi-threaded program, and use precise modeling and constraint-based symbolic (non-enumerative) search to find feasible violating schedules in a generalization of the observed run. We specifically focus on tool scalability by devising POR-based simplification steps to reduce the formula and the search space by several orders-of-magnitude. We have successfully applied the tool to several publicly available C/C++/Java programs and found several previously known/unknown concurrency related bugs. The tool also has extensive visual support for debugging.

Software model checking and static analysis have matured over the last decade, enabling their use in automated software verification. However, lack of scalability makes these tools hard to apply. Furthermore, approximations in the models of program and environment lead to a profusion of false alarms. This paper proposes DC2, a verification framework using scope-bounding to bridge these gaps. DC2 splits the analysis problem into manageable parts, relying on a combination of three automated techniques: (a) techniques to infer useful specifications for functions in the form of pre- and post-conditions; (b) stub inference techniques that infer abstractions to replace function calls beyond the verification scope; and (c) automatic refinement of pre- and post-conditions from false alarms identified by a user. DC2 enables iterative reasoning over the calling environment, to help in finding non-trivial bugs and fewer false alarms. We present an experimental evaluation that demonstrates the effectiveness of DC2 on several open-source and industrial software projects.

We address the problem of detecting serializability violations in a concurrent program using predictive analysis, where a violation is detected either in an observed trace or in an alternate interleaving of events in that trace. Under the widely used notion of conflict-serializability, checking whether a given execution is serializable can be done in polynomial time. However, when all possible interleavings are considered, the problem becomes intractable. We address this in practice through a graph-based method, which for a given atomic block and trace, derives a smaller segment of the trace, referred to as the Trace Atomicity Segment (TAS), for further systematic exploration. We use the observed write-read pairs of events in the given trace to consider a set of events that guarantee feasibility, i.e., each interleaving of these events corresponds to some real execution of the program. We call this set of interleavings the almost view-preserving (AVP) interleavings. We show that the TAS is sufficient for finding serializability violations among all AVP interleavings. Further, the TAS enables a simple static check that can prove the absence of a violation. This check often succeeds in practice. If it fails, we perform a systematic exploration over events in the TAS, where we use dynamic partial order reduction with additional pruning to reduce the number of interleavings considered. Unlike previous efforts that are less precise, when our method reports a serializability violation, the reported interleaving is guaranteed to correspond to an actual execution of the program. We report experimental results that demonstrate the effectiveness of our method in detecting serializability violations for Java and C/C++ benchmark programs.

Abstract Predictive analysis aims at detecting concurrency errors during runtime by monitoring a concrete execution trace of a concurrent program. In recent years, various models based on the happens-before causality relations have been proposed for predictive analysis. However, these models often rely on only the observed runtime events and typically do not utilize the program source code. Furthermore, the enumerative algorithms they use for verifying safety properties in the predicted traces often suffer from the interleaving explosion problem. In this paper, we introduce a precise predictive model based on both the program source code and the observed execution events, and propose a symbolic algorithm to check whether a safety property holds in all feasible permutations of events of the given trace. Rather than explicitly enumerating and checking the interleavings, our method conducts the search using a novel encoding and symbolic reasoning with a satisfiability modulo theory solver. We also propose a technique to bound the number of context switches allowed in the interleavings during the symbolic search, to further improve the scalability of the algorithm.

We present a Monte-Carlo optimization technique for finding inputs to a system that falsify a given Metric Temporal Logic (MTL) property. Our approach performs a random walk over the space of inputs guided by a robustness metric defined by the MTL property. Robustness can be used to guide our search for a falsifying trajectory by exploring trajectories with smaller robustness values. We show that the notion of robustness can be generalized to consider hybrid system trajectories. The resulting testing framework can be applied to non-linear hybrid systems with external inputs. We show through numerous experiments on complex systems that using our framework can help automatically falsify properties with more consistency as compared to other means such as uniform sampling.

Software model checking has recently been successful in discovering bugs in production software. Most tools have targeted heap related programming mistakes and control-heavy programs. However, real-time and embedded controllers implemented in software are susceptible to computational numeric instabilities. We target verification of numerical programs that use floating-point types, to detect loss of numerical precision incurred in such programs. Techniques based on abstract interpretation have been used in the past for such analysis. We use bounded model checking (BMC) based on Satisfiability Modulo Theory (SMT) solvers, which work on a mixed integer-real model that we generate for programs with floating points. We have implemented these techniques in our software verification platform. We report experimental results on benchmark examples to study the effectiveness of model checking on such problems, and the effect of various model simplifications on the performance of model checking.

Path-sensitivity is often a crucial requirement for verifying safety properties of programs. As it is infeasible to enumerate and analyze each path individually, analyses compromise by soundly merging information about executions along multiple paths. However, this frequently results in a loss of precision. We present a program analysis technique that we call Satisfiability Modulo Path Programs (SMPP), based on a path-based decomposition of a program. It is inspired by insights that have driven the development of modern SMT(Satisfiability Modulo Theory) solvers. SMPP symbolically enumerates path programs using a SAT formula over control edges in the program. Each enumerated path program is verified using an oracle, such as abstract interpretation or symbolic execution, to either find a proof of correctness or report a potential violation. If a proof is found, then SMPP extracts a sufficient set of control edges and corresponding interference edges, as a form of proof-based learning. Blocking clauses derived from these edges are added back to the SAT formula to avoid enumeration of other path programs guaranteed to be correct, thereby improving performance and scalability. We have applied SMPP in the F-Soft program verification framework, to verify properties of real-world C programs that require path-sensitive reasoning. Our results indicate that the precision from analyzing individual path programs, combined with their efficient enumeration by SMPP, can prove properties as well as indicate potential violations in the large.

We present a simple yet useful technique for refining the control structure of loops that occur in imperative programs. Loops containing complex control flow are common in synchronous embedded controllers derived from modeling languages such as Lustre, Esterel, and Simulink/Stateflow. Our approach uses a set of labels to distinguish different control paths inside a given loop. The iterations of the loop are abstracted as a finite state automaton over these labels. Subsequently, we use static analysis techniques to identify infeasible iteration sequences and subtract such forbidden sequences from the initial language to obtain a refinement. In practice, the refinement of control flow sequences often simplifies the control flow patterns in the loop. We have applied the refinement technique to improve the precision of abstract interpretation in the presence of widening. Our experiments on a set of complex reactive loop benchmarks clearly show the utility of our refinement techniques. Abstraction interpretation with our refinement technique was able to verify all the properties for 10 out of the 13 benchmarks, while abstraction interpretation without refinement was able to verify only four. Other potentially useful applications include termination analysis and reverse engineering models from source code.

This paper proposes a framework for determining the correctness and robustness of simulations of hybrid systems. The focus is on simulations generated from model-based design environments and, in particular, Simulink. The correctness and robustness of the simulation is guaranteed against floating-point rounding errors and system modeling uncertainties. Toward that goal, self-validated arithmetics, such as interval and affine arithmetic, are employed for guaranteed simulation of discrete-time hybrid systems. In the case of continuous-time hybrid systems, self-validated arithmetics are utilized for over-approximations of reachability computations.

We propose a new algorithm for verifying concurrent programs, which uses concrete executions to partition the program into a set of lean partitions called concurrent trace programs (CTPs), and symbolically verifies each CTP using a satisfiability solver. A CTP, derived from a concrete execution trace, implicitly captures all permutations of the trace that also respect the control flow of the program. We show that a CTP, viewed as a coarser equivalence class than the popular (Mazurkiewicz) trace equivalence in partial order reduction (POR) literature, leads to more effective pruning of the search space during model checking. While classic POR can prune away redundant interleavings within each trace equivalence class, the pruning in POR is not property driven. We use symbolic methods to achieve property-driven pruning. The effort of exploration is distributed between a symbolic component (verification of a particular CTP) and an enumerative component (exploration of the space of CTPs). We show that the proposed method facilitates more powerful pruning of the search space during the enumerative exploration.

With the growth of multi-core processing and concurrent programming in modern computing systems, there is a great need to develop effective verification techniques for concurrent programs. Static analysis techniques have been shown effective for finding data races, but suffer from a general problem of too many false alarms. Dynamic techniques like testing have also shown promise, but provide limited coverage over the state space including all possible thread interleavings. Model checking alone cannot scale. However, it works better in combination with these techniques, with the potential of finding real error traces on one hand and better coverage on the other. In this talk, I will describe our recent advances in concurrent dataflow analysis, symbolic model checking with partial order reduction, and dynamic techniques for verifying concurrent programs. These techniques have been implemented in a unified verification platform, currently targeted at multi-threaded C programs. I will also report on our experiences on some challenging examples from the public domain and the industry.

We present an efficient symbolic search algorithm for software model checking. Our algorithms perform word-level reasoning by using a combination of decision procedures in Boolean and integer and real domains, and use novel symbolic search strategies optimized specifically for sequential programs to improve scalability. Experiments on real-world C programs show that the new symbolic search algorithms can achieve several orders-of-magnitude improvements over existing methods based on bit-level (Boolean) reasoning.

Bounded Model Checking (BMC) provides complete design coverage with respect to a correctness property up to a bounded depth. However, with successive unrolling of the design, each BMC instance at depth k becomes bigger in size and harder to solve. We propose a novel scalable approach to decompose disjunctively a BMC instance, into simpler and independent subproblems, based on tunnels i.e., a set of control paths. We simplify each subproblem using slicing, data path simplification and tunnel specific control flow constraints, and solve them independently. We implemented such a tunneling and slicing-based reduction (TSR) approach in Satisfiability-Modulo-Theory (SMT)-based BMC framework. Such a TSR-based approach improves the overall performance of BMC when applied to verification of lowlevel embedded industry programs.

Bounded Model Checking (BMC) is incomplete without a completeness threshold (CT) bound. Previous methods, using recurrence diameter for obtaining CT, check for existence of a longest loop-free path at every depth k. For terminating software programs, we propose an efficient method for obtaining CT that requires solving a formula of size O(k) at some depths only, as compared to previous methods that require solving a formula of O(k2) (or O(klogk)) size at every depth. We augment previous methods for BMC simplifications using model transformation and control flow information, with context-sensitive analysis. This results in more BMC simplifications and further reduction in the number of CT checks. We have implemented our techniques in a Satisfiability Modulo Theory (SMT)-based BMC framework. Our controlled experiments on real-world software programs show that our proposed formulation provides significant improvements over previous approaches.

Software libraries organize useful functionalities in order to promote modularity and code reuse. A typical library is used by client programs through an application programming interface (API) that hides its internals from the client. Typically, the rules governing the correct usage of the API are documented informally. In many cases, libraries may have complex API usage rules and unclear documentation. As a result, the behaviour of the library under some corner cases may not be well understood by the programmer. Formal specifications provide a precise understanding of the API behaviour.

We present a technique to infer likely data preconditions forprocedures written in an imperative programming language. Given a procedure and a set of predicates over its inputs, our technique enumerates different truth assignments to the predicates, deriving test cases from each feasible truth assignment. The predicates themselves are derived automatically using simple heuristics. The enumeration of truth assignments is performed using a propositional SAT solver along with a theory satisfiability checker capable of generating unsatisfiable cores.

We propose a novel method for modular verification of web service compositions. We first use symbolic fixpoint computations to derive conditions on the incoming messages and relations among the incoming and outgoing messages of individual BPEL web services. These pre- and post-conditions are accumulated and serve as a repository of summarizations of individual web services. We then compose the summaries of the invoked BPEL services to model external invocations, resulting in a scalable verification approach for web service compositions. Our technical contributions include (1) an efficient symbolic encoding for modeling the concurrency semantics of systems having both multi-threading and message passing, and (2) a scalable method for summarizing concurrent processes that interact with each other using synchronous message passing, along with a modular framework that utilizes these summaries for scalable verification.

This paper presents a lightweight interval analysis technique for determining the lower and upper bounds for program variables and its application in improving software model checking techniques. The experiments demonstrate that it is an effective approach to alleviate the state explosion problem in software model checking.

Current industry trends in system design - multiple clocks, clocks with arbitrary frequency ratios, multi-phased clocks, gated clocks, and level-sensitive latches, combined with clocked - pose additional challenges to verification efforts. We propose an integrated solution that improves SAT-based bounded model checking (BMC) by orders of magnitude, for verification of synchronous multi-clock systems with clocked LTL properties. Our main contributions are: a) efficient clock modeling schemes to handle clock related challenges uniformly; b) generation of automatic schedules and clock constraints to avoid unnecessary unrolling and loop-checks in BMC; c) dynamic simplification of BMC problem instances with clock constraints; and d) customized BMC translations - with incremental formulations and learning - to directly handle PSL-style clocked specifications. We demonstrate the effectiveness of our approach on some OpenCores multi-clock system benchmarks.

Induction has been studied in model checking for proving the validity of safety properties, i.e., showing the absence of counterexamples. To our knowledge, induction has not been used to refute safety properties. Existing algorithms including bounded model checking, predicate abstraction, and interpolation are not efficient in detecting long counterexamples. In this paper, we propose the use of induction inside the counterexample guided abstraction and refinement (CEGAR) loop to prove the existence of counterexamples. We target bugs whose counterexamples are long and yet can be captured by regular patterns. We identify the pattern algorithmically by analyzing the sequence of spurious counterexamples generated in the CEGAR loop, and perform the induction proof automatically. The new method has little additional overhead to CEGAR and this overhead is insensitive to the actual length of the concrete counterexample.

Variable hiding and predicate abstraction are two popular abstraction methods to obtain simplified models for model checking. Although both methods have been used successfully in practice, no attempt has been made to combine them in counterexample guided abstraction refinement (CEGAR). In this paper, we propose a hybrid abstraction method that allows both visible variables and predicates to take advantages of their relative strengths. We use refinement based on weakest preconditions to add new predicates, and under certain conditions trade in the predicates for visible variables in the abstract model. We also present heuristics for improving the overall performance, based on static analysis to identify useful candidates for visible variables, and use of lazy constraints to find more effective unsatisfiable cores for refinement. We have implemented the proposed hybrid CEGAR procedure. Our experiments on public benchmarks show that the new abstraction method frequently outperforms the better of the two existing abstraction methods.

Existing BDD-based symbolic algorithms designed for hardware designs do not perform well on software programs. We propose novel techniques based on unique characteristics of software programs. Our algorithm divides an image computation step into a disjunctive set of easier ones that can be performed in isolation. We use hypergraph partitioning to minimize the number of live variables in each disjunctive component, and variable scopes to simplify transition relations and reachable state subsets. Our experiments on nontrivial C programs show that BDD-based symbolic algorithms can directly handle software models with a much larger number of state variables than for hardware designs.

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.

Finite state models generated from software programs have unique characteristics that are not exploited by existing model checking algorithms. In this paper, we propose a novel disjunctive image computation algorithm and other simplifications based on these characteristics. Our algorithm divides an image computation into a disjunctive set of easier ones that can be performed in isolation. Hypergraph partitioning is used to minimize the number of live variables in each disjunctive component. We use the live variables to simplify transition relations and reachable state subsets. Our experiments on a set of real-world C programs show that the new algorithm achieves orders-of-magnitude performance improvement over the best known conjunctive image computation algorithm

SAT-based Bounded Model Checking (BMC) has been found promising in finding deep bugs in industry designs and scaling well with design sizes. However, it has limitations due to requirement of finite data paths, inefficient translations and loss of high-level design information during the BMC problem formulation. These shortcomings inherent in Boolean-level BMC can be avoided by using high-level BMC. We propose a novel framework for high-level BMC, which includes several techniques that extract high-level design information from EFSM models to make the verification model "BMC friendly", and use it on-the-fly to simplify the BMC problem instances. Such techniques overcome the inherent limitations of Boolean-level BMC, while allowing integration of state-of-the-art techniques for BMC. In our controlled experiments we found signficant performance improvements achievable by the proposed techniques.

In this paper, we propose a new technique for the verification of concurrent multi-threaded programs. In general, the problem is known to be undecidable even for programs with just two threads. However, we exploit the observation that, in practice, a large fraction of concurrent programs can either be modeled as pushdown systems communicating solely using locks or can be reduced to such systems by applying standard abstract interpretation techniques or by exploiting separation of data from control. Moreover, standard programming practice guidelines typically recommend that programs use locks in a nested fashion. In fact, in languages like Java and C#, locks are guaranteed to be nested. For such a framework, we show, by using the new concept of Lock Constrained Multi-Automata Pair (LMAP), that pre*-closures of regular sets of states can be computed efficiently. This is accomplished by reducing the pre*-closure computation for a regular set of states of a concurrent program with nested locks to those for its individual threads. Leveraging this new technique then allows us to formulate a fully automatic, efficient and exact (sound and complete) decision procedure for model checking threads communicating via nested locks for indexed linear-time temporal logic formulae

We present an efficient symbolic search algorithm for software model checking. The algorithm combines multiple symbolic representations to efficiently represent the transition relation and reachable states and uses a combination of decision procedures for Boolean and integer representations. Our main contributions include: (1) mixed symbolic representations to model C programs with rich data types and complex expressions; and (2) new symbolic search strategies and optimization techniques specific to sequential programs that can significantly improve the scalability of model checking algorithms. Our controlled experiments on real-world software programs show that the new symbolic search algorithm can achieve several orders-of-magnitude improvements over existing methods. The proposed techniques are extremely competitive in handling sequential models of non-trivial sizes, and also compare favorably to popular Boolean-level model checking algorithms based on BDDs and SAT

Model checking of safety properties has taken a significant lead over non-safety 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 non-safety 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.

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.

With the success of formal verification techniques like equivalence checking and model checking for hardware designs, there has been growing interest in applying such techniques for formal analysis and automatic verification of software programs. This paper provides a brief tutorial on model checking of C programs. The essential approach is to model the semantics of C programs in the form of finite state systems by using suitable abstractions. The use of abstractions is key, both for modeling programs as finite state systems and for reducing the model sizes in order to manage verification complexity. We provide illustrative details of a verification platform called F-Soft, which provides a range of abstractions for modeling software, and uses customized SAT-based and BDD-based model checking techniques targeted for software.

We describe an efficient approach for SAT-based quantifier elimination that significantly improves the performance of pre-image and fixed-point computation in SAT-based unbounded symbolic model checking (UMC). The proposed method captures a larger set of new states per SAT-based enumeration step during quantifier elimination, in comparison to previous approaches. The novelty of our approach is in the use of circuit-based cofactoring to capture a large set of states, and in the use of a functional hashing based simplified circuit graph to represent the captured states. We also propose a number of heuristics to further enlarge the state set represented per enumeration, thereby reducing the number of enumeration steps. We have implemented our techniques in a SAT-based UMC framework where we show the effectiveness of SAT-based existential quantification on public benchmarks, and on a number of large industry designs that were hard to model check using purely BDD-based techniques. We show several orders of improvement in time and space using our approach over previous CNF-based approaches. We also present controlled experiments to demonstrate the role of several heuristics proposed in the paper. Importantly, we were able to prove using our method the correctness of a safety property in an industry design that could not be proved using other known approaches.

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.

Resolution-based proof analysis techniques have been proposed recently to identify a sufficient set of reasons for unsatisfiability derived by a CNF-based SAT solver. We have adapted these techniques to work with a hybrid SAT solver. We use the proof analysis technique with SAT-based BMC, in order to, generate useful abstract models. Our abstraction procedure is used iteratively in a top-down framework, starting from the concrete design, where we apply BMC on increasingly more abstract models. We apply various SAT-based and BDD-based verification methods on these abstract models, in order to obtain proofs of correctness, or to perform deeper searches for counterexamples. We demonstrate the effectiveness of our prototype implementation on several large industry designs.

We propose Satisfiability Checking (SAT) techniques that lead to a consistent performance improvement of up to 3x over state-of-the-art SAT solvers like Chaff on important problem domains in VLSI CAD. We observe that in circuit oriented applications like ATPG and verification, different software engineering techniques are required for the portions of the formula corresponding to learnt clauses compared to the original formula. We demonstrate that by employing the same innovations as in advanced CNF-based SAT solvers, but in a hybrid approach where these two portions of the formula are represented differently and processed separately, it is possible to obtain the consistently highest performing SAT solver for circuit oriented problem domains. We also present controlled experiments to highlight where these gains come from. Once it is established that the hybrid approach is faster, it becomes possible to apply low overhead circuit-based heuristics that would be unavailable in the CNF domain for greater speedup.

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.

A practical solution to the complexity of design validation is semi-formal verification, where the specification of correctness criteria is done formally, as in model checking, but checking is done using simulation, which is guided by directed vector sequences derived from knowledge of the design and/or the property being checked. Simulation vectors must be effective in targeting the types of bugs designers expect to find rather than some generic coverage metrics. The focus of our work is to generate property-specific testbenches for guided simulation, that are targeted either at proving the correctness of a full CTL property or at finding a bug. This is facilitated by generation of a property-specific model, called a "witness graph", which captures interesting paths in the design. Starting from an initial abstract model of the design, symbolic model checking, pruning, and refinement steps are applied in an iterative manner, until either a conclusive result is obtained or computing resources are exhausted. The witness graph is annotated with, e.g., state or transition priorities before testbench generation. The overall testbench generation flow, and the iterative flow for witness graph generation are shown.

Methods based on Boolean satisfiability (SAT) typically use a conjunctive normal form (CNF) representation of the Boolean formula, and exploit the structure of the given problem through use of various decision heuristics and implication methods. We propose a new decision heuristic based on separator-set induced partitioning of the underlying CNF graph. It targets those variables whose choice generates clause partitions with disjoint variable supports. This can potentially improve performance of SAT applications by decomposing the problem dynamically within the search. In the context of a recently proposed image computation method combining SAT and BDDs, this results in simpler BDD subproblems. We provide algorithms for CNF partitioning - one based on a clause-variable dependency matrix, and another based on standard hypergraph partitioning techniques, and also for the use of partitioning information in decision heuristics for SAT. The effectiveness of the proposed partition-based heuristic is shown with practical results for reachability analysis of benchmark sequential circuits.

This article introduces the notion of a Complete-1-Distinguishability (C-1-D) property for simplifying equivalence checking of finite state machines (FSMs). When a specification machine has the C-1-D property, the traversal of the product machine can be eliminated. Instead, a much simpler check suffices. The check consists of first obtaining a 1-equivalence mapping between the individually reachable states of the specification and the implementation machines, and then checking that it is a bisimulation relation. The C-1-D property can be used directly for specification machines on which it naturally holds---a condition that has not been exploited thus far in FSM verification. We also show how this property can be enforced on an arbitrary FSM by exposing some of its latch outputs as pseudo-primary outputs during synthesis and verification. In this sense, our synthesis/verification methodology provides another point in the trade-off curve between constraints-on-synthesis versus complexity-of-verification. Practical experiences with this methodology have resulted in success with several examples for which it is not possible to complete verification using existing implicit state space traversal techniques.

We propose a novel procedure based on uninterpreted symbolic simulation for checking the scheduling step in high-level synthesis. The primary task in scheduling is the assignment of time steps or, equivalently, states to operations. Various transformations like operation reordering and loop unrolling may be performed in the process to meet the optimization criteria. The contribution of our proposal lied in its ability to efficiently handle loops and a wide range of loop transformations performed during scheduling. Our algorithm is based on loop invariant extraction using a combination of uninterpreted symbolic simulation and induction techniques. In spite of its wide scope, our procedure is relatively complete and practical. This work is a part of our effort to provide a suite of techniques for verifying the various steps involved in the high-level synthesis process. It is being implemented in an in-house verification system for checking equivalence of designs generated from high-level specifications through successive refinements. We present case studies to demonstrate the applicability of our approach. These case studies consist of examples where equivalence cannot be established using conventional FSM-based methods. By providing a viable automated equivalence checking technique for such examples, we improve on the state of the art.

The biggest obstacle in the formal verification of large designs istheir very large state spaces, which cannot be handled even bytechniques such as implicit state space traversal. The only viablesolution in most cases is validation by functional simulation. Unfortunately, this has the drawbacksof high computationalrequirementsdue to the large number of test vectors needed, and the lack of adequate coverage measures to characterize the quality of a given testset. To overcome these limitations, there has been recent interest inhybrid techniques which combine the strengths of formal verification and simulation. Formal verification-based techniques are usedon a test model (usually much smaller than the design) to derive a setof functional test vectors, which are then used for design validationthrough simulation. The test set generated typically satisfies somecoverage measure on the test model. Recent research has proposedthe use of state or transition coverage. However, no effort has beenmade to relate these measures to the coverage of design errors. Furthermore, the derivation of the test model remains largely ad-hoc,with few formal guidelines.We demonstrate that under a given set of assumptions, transitiontours on test models can be used for complete validation of an implementation against a specification, for a large and important classof designs that includes many programmable/hardwired, general-purpose processors/DSPs. A by-product of this study is specificguidelines for deriving the test model, motivated by the requirement of providing complete coverage of all errors. We illustrate theapplication of our methodology on a pipelined implementation of the DLX processor.

This paper introduces the use of the Complete-1-Distinguishability (C-1-D) property for simplifying FSM verification. This property eliminates the need for a traversal of the product machine for the implementation and the specification. Instead, a much simpler check suffices. This check consists of first obtaining a 1-equivalence mapping between states of the two machines, and then checking that it is a bisimulation relation. The C-1-D property can be used directly on specifications for which it naturally holds a condition that has not been exploited thus far in FSM verification. We also show how this property can be enforced on arbitrary FSMs by exposing some of the latch outputs as pseudo-primary outputs during synthesis and verification. In this sense, our synthesis/verification methodology provides another point in the tradeoff curve between constraints-on-synthesis versus complexity-of-verification. Practical experiences with using this methodology have resulted in success with several examples for which it is not possible to complete verification using existing implicit state space traversal techniques.

State space exploration is of prime importance in the study of finite state sequential systems, with several efforts aimed at compact representation of the state space in order to tackle the state explosion problem. In the work presented on formal verification of inductively-defined hardware, we have identified a useful class of Boolean functions called linearly inductive functions (LIFs). We explore the relationship between our LIF representation and the classic DFA (deterministic finite state automaton) representation of a sequential function, and examine the associated tradeoffs. We show that our LIF representation corresponds to a minimal reverse DFA, i.e. a minimal DFA which accepts the language consisting of the reverse input strings, where our implicit method for obtaining an LIF representation does not require explicit construction of a forward DFA. Its practical usefulness arises from our demonstration that reverse DFAs for several datapath circuits are exponentially more compact than the classic forward DFAs. Furthermore, in comparison to the traditional representation of DFAs as state transition diagrams, our LIF representations allow for state-sharing while maintaining decomposition, resulting in memory savings in practice.>

We consider a class of practically useful Boolean functions, called linearly inductive functions (LIFs), and present a canonical representation as well as algorithms for their automatic symbolic manipulation. LIFs can be used to capture structural induction in parameterized circuit descriptions, whereby our LIF representation provides a fixed-sized representation for all size instances of a circuit. Furthermore, since LIFs can naturally capture the temporal induction inherent in sequential system descriptions, our representation also provides a canonical form for sequential functions. This allows for a wide range of applications of symbolic LIF manipulation in the verification and synthesis of digital systems. We also present practical results from a preliminary implementation of a general purpose LIF package.