Abstraction plays a central role in formal verification. Term-level abstraction is a technique for abstracting word-level designs in a formal logic, wherein data is modeled with abstract terms, functional blocks with uninterpreted functions, and memories with a suitable theory of memories. A major challenge for any abstraction technique is to determine what components can be safely abstracted. We present an automatic technique for term-level abstraction of hardware designs, in the context of equivalence and refinement checking problems. Our approach is hybrid, involving a combination of random simulation and static analysis. We use random simulation to identify functional blocks that are suitable for abstraction with uninterpreted functions. Static analysis is then used to compute conditions under which such function abstraction is performed. The generated term-level abstractions are verified using techniques based on Boolean satisfiability (SAT) and satisfiability modulo theories (SMT). We demonstrate our approach for verifying processor designs, interface logic, and low-power designs. We present experimental evidence that our approach is efficient and that the resulting term-level models are easier to verify even when the abstracted designs generate larger SAT problems.

We prove the parameterized correctness of one of the largest cache coherence protocols being used in modern multi-core processors today. Our approach is a generalization of a method we described last year that uses data type reduction and compositional reasoning to iteratively abstract and refine the protocol and uses invariants derived from protocol ¿flows¿ to make the abstraction-refinement loop converge. Our prior work demonstrated the value of sequencing information that appeared within the linear flows describing a protocol in design documents. This paper extends the notion of flows to capture intricate scenarios seen in real industrial protocols and demonstrates that there is also valuable information in the interaction among flows. We further show that judicious use of flows is required to make the method converge and identify which flows are most suitable.

We used the Spin model checker to show that Intel's implementation of software transactional memory is correct. Transactional memory makes it possible to write properly-synchronized multi-threaded programs without the explicit use of locks. We describe our model of Intel's implementation, our experience with Spin, what we have shown, and what obstacles remain to showing more.

We cannot apply PODC methodologies to industrial designs without formal models of the designs. Formal models are usually hard to find. We have built a tool that extracts formal models directly from design documents.

We used the Spin model checker to show that Intel's implementation of software transactional memory is correct, and built a preprocessor to accelerate the performance of Spin on parameterized models of shared-memory protocols.

We show how to verify the correctness of transactional memory implementations with a model checker. We show how to specify transactional memory in terms of the admissible interchange of transaction operations, and give proof rules for showing that an implementation satisfies this specification. This notion of an admissible interchange is a key to our ability to use a model checker, and lets us capture the various notions of transaction conflict as characterized by Scott. We demonstrate our work using the TLC model checker to verify several well-known implementations described abstractly in the TLA+ specification language.

This paper introduces reFLect, a functional programming language with reflection features intended for applications in hardware design and verification. The reFLect language is strongly typed and similar to ML, but has quotation and antiquotation constructs. These may be used to construct and decompose expressions in the reFLect language itself. The paper motivates and presents the syntax and type system of this language, which brings together a new combination of pattern-matching and reflection features targeted specifically at our application domain. It also gives an operational semantics based on a novel use of contexts as expression constructors, and it presents a scheme for compiling reFLect programs using the same context mechanism.

The Forte formal verification environment for datapath-dominated hardware is described. Forte has proven to be effective in large-scale industrial trials and combines an efficient linear-time logic model-checking algorithm, namely the symbolic trajectory evaluation (STE), with lightweight theorem proving in higher-order logic. These are tightly integrated in a general-purpose functional programming language, which both allows the system to be easily customized and at the same time serves as a specification language. The design philosophy behind Forte is presented and the elements of the verification methodology that make it effective in practice are also described.

Many modern microprocessors implement floating point square root hardware using subtractive algorithms. Such processors include the HP PA7200, the MIPS R4400, and the Intel Pentium. The Intel Pentium division bug highlights the importance of verifying such implementations. In this paper we discuss the verification of a radix-2 square root unit similar to that used in the MIPS R4400. The verification is done by theorem proving to bridge the gap between the algorithm and the implementation. At the top level, we verify that a subtractive, non-restoring algorithm correctly calculates the square root function. We then show a series of optimizing transformations that refine the top level algorithm into the hardware implementation. Each transformation can be verified. We show the transformation of the top level proof to a level that is closer to the hardware implementation. The implementation is at the RTL level, and consists of a structural description of the hardware including an adder/subtracter, simple combinational hardware and some registers.