Formal methods are becoming an indispensable part of the design process in software and hardware industry. It takes robust tools and proofs to make formal validation of large scale projects reliable. In this paper, we will describe the current status of formal verification at Centaur Technology. We will explain our challenges and our methodology—how various proofs and verification artifacts are interconnected and how we keep them consistent over the duration of a project. We also describe our main engine—a powerful symbolic simulator with rewriting capabilities that is integrated in a theorem prover and proven correct.

A common technique for checking properties of complex state machines is to build a finite abstraction then check the property on the abstract system -- where a passing check on the abstract system is only transferred to the original system if the abstraction is proven to be representative. This approach does require the derivation or definition of the finite abstraction, but can avoid the need for complex invariant definition. For our work in checking progress of memory transactions in microprocessors, we need to prove that transactions in complex state machines always make progress to completion. As a part of this effort, we developed a process for computing a finite abstract graph of the target state machine along with annotations on whether certain measures decrease or not on arcs in the abstract graph. We then iteratively divide the abstract graph by splitting into strongly connected components and then building a measure for every node in the abstract graph which is ensured to be reducing on every transition of the original system guaranteeing progress. For finite state target systems (e.g. hardware designs), we present approaches for extracting the abstract graph efficiently using incremental SAT through GL and then the application of our process to check for progress. We present an implementation of the Bakery algorithm as an example application.

Verification of modern microprocessors is a complex task that requires a substantial allocation of resources. Despite significant progress in formal verification, the goal of complete verification of an industrial design has not been achieved. In this paper, we describe a current contribution of formal methods to the validation of modern x86 microprocessors at Centaur Technology. We focus on proving correctness of instruction implementations, which includes the decoding of an instruction, its translation into a sequence of microoperations, any subsequent execution of traps to microcode ROM, and the implementation of these micro-operations in execution units. All these tasks are performed within one verification framework, which includes a theorem prover, a verified symbolic simulator, and SAT solvers. We describe the work of defining the needed formal models for both the architecture and micro-architecture in this framework, as well as tools for decomposing the requisite properties into smaller lemmas which can be automatically checked. We additionally cover the advantages and limitations of our approach. To our knowledge, there are no similar results in the verification of implementations of an x86 microprocessor.

We present a tool that primarily supports the ability to check bounded properties starting from a sequence of states in a run. The target design is compiled into an AIGNET which is then selectively and iteratively translated into an incremental SAT instance in which clauses are added for new terms and simplified by the assignment of existing literals. Additional applications of the tool can be derived by the user providing alternative attachments of constrained functions which guide the iterations and SAT checks performed. Some Verilog RTL examples are included for reference.

We present a series of definitions and theorems demonstrating how to reduce the requirements for proving system refinements ensuring containment of fair stuttering runs. A primary result of the work is the ability to reduce the requisite proofs on runs of a system of interacting state machines to a set of definitions and checks on single steps of a small number of state machines corresponding to the intuitive notions of freedom from starvation and deadlock. We further refine the definitions to afford an efficient explicit-state checking procedure in certain finite state cases. We demonstrate the proof reduction on versions of the Bakery Algorithm.

We present a framework for the specification and verification of reactive concurrent programs using general-purpose mechanical theorem proving. We define specifications for concurrent programs by formalizing a notion of refinements analogous to stuttering trace containment. The formalization supports the definition of intuitive specifications of the intended behavior of a program. We present a collection of proof rules that can be effectively orchestrated by a theorem prover to reason about complex programs using refinements. The proof rules systematically reduce the correctness proof for a concurrent program to the definition and proof of an invariant. We include automated support for discharging this invariant proof with a predicate abstraction tool that leverages the existing theorems proven about the components of the concurrent programs. The framework is integrated with the ACL2 theorem prover and we demonstrate its use in the verification of several concurrent programs in ACL2.

We present an efficient term simplifier written in ACL2 and interfaced with ACL2 as an untrusted clause processor. We also demonstrate how an advanced user can extend this simplifier in a sound manner by proving rewrite rules with special annotations and programmed constraints on their application. For problems requiring extensive case analysis, the simplifier is more efficient than ACL2 built-in simplification and we demonstrate this on some relevant examples. In addition, we discuss the issue of user control over predictable simplification and conclude the paper with the proposed implementation of invariant discovery using the simplifier.

We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while allowing sound and efficient execution. In particular, the features supporting this method allow the user to install, in a logically sound way, alternative executable counterparts for logically defined functions. These alternatives are often much more efficient than the logically equivalent terms they replace. These features have been implemented in the ACL2 theorem prover, and we discuss several applications of the features in ACL2.

Using theorem-based approaches to prove the invariants of infinite-state reactive systems often demands significant manual involvement. This article presents a new approach in which model checking complements theorem proving, reducing the manual effort involved by transferring user attention from defining inductive invariants to proving rewrite rules. The authors use this approach with ACL2 to verify cache coherence protocols.

We present a proof of an efficient, in-place Quicksort implementation [1] using single-threaded objects (stobjs) in ACL2 [3, 4]. We demonstrate that the Quicksort implementation is equivalent to a simple insertion-sort function that is shown to produce an ordered permutation of its input. For ease of reasoning, the demonstration is carried out by verifying a series of ”intermediate” sorting functions. The intermediate functions are equivalent to the efficient Quicksort implementation, but written in a more applicative style, and hence easier to reason about. We then decompose the proof into a verification of the equivalence of the efficient implementation with an intermediate implementation, and a proof of correctness of the intermediate implementation. We show how this decomposition allows us to simplify our reasoning about stobjs and obtain a cleaner proof of the implementation.

We present a deductive method for proving invariants of reactive systems. Our approach uses term rewriting to reduce invariant proofs to reachability analysis on a finite graph. This substantially automates invariant proofs by obviating the need to define inductive invariants while still benefitting from the expressiveness of deductive methods. We implement a procedure supporting this approach which interfaces with the ACL2 theorem prover. The interface affords sound extension of our procedure with rewrite rules based on proven theorems. We demonstrate the method in the verification of cache coherence protocols.

We present a tool-supported methodology for proving predicates invariant over all time on the behavior of systems by exploring a finite graph generated from the definition of the predicate using rewrite rules from proven ACL2 theorems. The methodology provides a means for proving invariants which avoids the complexity and cost of defining an inductive invariant while still allowing the proof of invariants for infinite-state systems. We present two examples of the application of the methodology: a simple critical section example, and a slightly more complex MESI cache coherence system.

We present a procedure for checking a suitably-bounded ACL2 theorem using a SAT checker. The check is carried out by first translating the ACL2 theorem into an equivalent theorem defined with functions which only use the primitives if, cons, car, cdr, and nil. The translated theorem on simple cons-trees is then translated to a propositional formula by a form of evaluation lifted to a certain representations of functions on these simple cons-trees. The resulting propositional formula can be checked using a SAT checker. We present one such SAT checker also written in ACL2, but presumably any SAT checker could be used. In the case when the propositional formula fails, the propositional witness can easily be translated back to a witness of the failure for the original theorem.

We give a useful set of unconditional rewrite rules for reasoning about record structures,which are essentially finite functions. The problem, then, is to define functions for whichthese rules are true and then prove the rules. We begin with a series of definitions thatattempt to satisfy these rules but fall short for various reasons. Then we give two solutions,one of which generalizes to other finite structures. The definitions of our access and updatefunctions are somewhat subtle,...

Abstract: Formal Verification HistoryWe have emphasized automated theorem proving.1995--96: Division and square root algorithmsfor AMD-K5 microcode[3, 5]1997--present: Proofs of floating-point algorithmsand actual RTL that use ACL2 on theAMD Athlonprocessor and its derivatives [6,7, 8]\Gamma We have a translator from our proprietary RTL toACL2 [7] that enables RTL proofs.2001: Completed some protocol-level proofs5A natural target for theorem provers [10, 4]Concise formal...

We present a compositional proof of correctness for a binary decision diagram (BDD) manager used in the context of a propositional satissability checker implemented using Single-Threaded Objects (stobjs) in ACL2. The use of stobjs aaords the deenition of an eecient BDD manager which ensures unique construction, allows constant-time comparison, and caches previously computed results. The use of ACL2 means we can prove that the BDD manager implements the prescribed task of building a normal-form representation of a boolean formula. We divide the proof requirements into (1) showing that a simpler set of BDD functions is correct, and (2) showing that the stobj-based BDD functions return values consistent with these simpler functions. We conclude the paper with a discussion of future extensions and reenements to the BDD manager presented.