Bounded Model Checking (BMC) for software is a precise bug-finding technique that builds upon the efficiency of modern SAT and SMT solvers. BMC currently does not scale to large programs because the size of the generated formulae exceeds the capacity of existing solvers. We present a new, compositional and property-sensitive algorithm that enables BMC to automatically find bugs in large programs. A novel feature of our technique is to decompose the behaviour of a program into a sequence of BMC instances and use a combination of satisfying assignments and unsatisfiability proofs to propagate information across instances. A second novelty is to use the control- and data-flow of the program as well as information from proofs to prune the set of variables and procedures considered and hence, generate smaller instances. Our tool BLITZ outperforms existing tools and scales to programs with over 100,000 lines of code. BLITZ automatically and efficiently discovers bugs in widely deployed software including new vulnerabilities in Internet infrastructure software.

Hardware module reuse is a standard solution to the problems of increasing complexity of chip architectures and pressure to reduce time to market. In the absence of a single module interface standard, predesigned modules for “plug-and-play” usually require a converter between incompatible interface protocols. Current approaches to automatic synthesis of protocol converters mostly lack formal foundations and either employ abstractions far removed from the HDL implementation level or grossly simplify the structure of the protocols considered. This work presents a state-machine-based formalism for modeling bus-based communication protocols and a notion of protocol compatibility and of correct conversion between incompatible protocols. This formalism is used to derive algorithms for checking protocol compatibility and for provably correct, automatic converter synthesis. Experiments with automatic converter synthesis between different configurations of widely used commercial bus protocols, such as AMBA AHB, ASB APB, and the Open Core Protocol (OCP) are discussed. The work here is unique in its combination of a completely formal approach and the use of a low abstraction level that enables precise modeling of protocol characteristics that is also close to HDL.

In the absence of a single module interface standard, integration of pre-designed modules in System-on-Chip design often requires the use of protocol converters. Existing approaches to automatic synthesis of protocol converters mostly lack formal foundations and either employ abstractions that ignore crucial low level behaviors, or grossly simplify the structure of the protocols considered. We present a state-machine based formal model for bus based communication protocols, and precisely define protocol compatibility, and correct protocol conversion. Our model is expressive enough to capture features of commercial protocols such as bursts, pipelined transfers, wait state insertion, and data persistence, in cycle accurate detail. We show that the most general, correct converter for a pair of protocols, can be described as the greatest fixed point of a function for updating buffer states. This characterization yields a natural algorithm for automatic synthesis of a provably correct converter by iterative computation of the fixed point. We report our experience with automatic converter synthesis between widely used commercial bus protocols, such as AMBA AHB, ASB, APB, and OCP, considering features which are beyond the scope of current techniques.

Synchronous languages are well suited to implementation and verification of reactive systems. Large reactive systems tend to be distributed to cope with scalability and application specific demands. We propose abstractions for distributed reactive systems modelled as a set of synchronous nodes with asynchronous communication between them. The special features of synchronous programs allow us to obtain abstractions that are also valid synchronous programs only by syntactic transformations. For a given program, the set of all such abstractions forms a semi-lattice with the original program as the bottom and the most abstract program as the top element. The transformation we define is a natural basis for constructing an abstraction-refinement framework for verification. Given a program and a safety property, the abstraction-refinement process is a search in a lattice of programs obtained via syntactic transformations. We have implemented this abstraction refinement framework in a prototype tool and report our case studies.

Plug-n-Play style Intellectual Property (IP) reuse in System on Chip (SoC) design is facilitated by the use of an on-chip bus architecture. We present a synchronous, Finite State Machine based framework for modelling communication aspects of such architectures. This formalism has been developed via interaction with designers and the industry and is intuitive and lightweight. We have developed cycle accurate methods to formally specify protocol compatibility and component composition and show how our model can be used for compatibility verification, interface synthesis and model checking with automated specification. We demonstrate the utility of our framework by modelling the AMBA bus architecture including details such as pipelined operation, burst and split transfers, the AHB-APB bridge and arbitration features.