Research

Robert Jones
My research is in the application of formal mathematics to the specification, design, and verification of high-performance, robust computer systems.

The specification and verification aspect of this work is commonly called formal verification, and is essentially the process of mathematically analyzing a design to detect functional errors before it is fabricated (in the case of hardware) or shipped (in the case of software). In many settings, the difficulty of functional verification is increasing at a higher rate than the difficulty of other design activities. Formal verification attempts to address the functional verification problem by providing a way to exhaustively verify a design's functionality under all possible inputs and operating modes. This actually works on relatively small designs, but in the worst case, the complexity of the problem scales exponentially with design size and formal verification cannot be applied. Formal verification capacity issues result in many of the current research questions.

Reasoning mathematically about designs requires mathematical models of the design itself (often called an implementation) and the design requirements (the specification). It also requires a mathematical system for reasoning about the implementation and specification. Much research is taking place in implementation and specification representations, efficiency of the underlying algorithms, and approaches to automation. Not surprisingly, there is significant interplay between the different issues.

The application of formal methods in the design process is not limited to verification. While design verification typically occurs concurrent with design, it is usually considered a separate task. A design revision is created, it is verified (often by a different team than the team creating the design), and problems found in verification are communicated back to the design team for integration into the next revision. A developing area of research considers the application of formal methods during the design process itself. Ideally, this so-called design for correctness would prevent a broad class of functional errors from being introduced into the design in the first place. Less-obvious benefits include cleaner hierarchy definitions and design decomposition which would result in improved modularity and better potential for design re-use.

My research spans much of formal methods, although it has almost exclusively been concerned with and applied to hardware. In particular, much of my research has concerned the functional verification of microprocessors. I'm fascinated by microprocessors, probably because they are the most complex systems I've encountered. In addition to functional verification, I'm interested in other aspects of the design problem including architecture, performance, and the design process itself. Intel is an ideal place for me to pursue my research: there is no shortage of complex designs that need to be verified.

My work in formal verification can be roughly partitioned into the following areas:

Each is discussed briefly below, along with pointers to some relevant papers.

Large-Scale Formal Verification: Methodology and Applications

Applying formal verification in practice can be difficult. The scale of the verification problems encountered in practice can be several orders of magnitude more complex than that encountered in academic problems--which are often designed for the sole purpose of verification. This should not be interpreted to impinge academic verification research, as it is the source of many new and innovative ideas. However, applying new ideas to large-scale circuits is in and of itself an interesting problem.

This issue is not unique to verification. Most CAD (computer-aided design) concepts require methodology development to be successfully applied to general problems. A good methodology provides problem-solving structure that can be applied to more than a single problem instance. When defining a methodology, there is a delicate balance between over-specifying what should be done (handicapping expert users) and not providing enough structure (a disadvantage for new users and a problem for re-using results for different problems).

A recent book, an extended and updated version of my dissertation, discusses applications and methodologies for using symbolic simluation in industrial verification.

Two papers discuss the benefits of applying symbolic trajectory evaluation (STE) to the verification of very large datapath circuits.

A more recent paper provides an improved interface to symbolic indexing, a data abstraction technique that exploits the partially-ordered state space of STE.

Beyond the methodology question, we have also considered a problem class that often arises in micro-processor verification: iterative circuits.

Other application areas, notably arithmetic circuits, have been researched extensively by my colleagues.

High-Level Modeling in Formal Verification

The functional complexity of hardware is increasing at a similar rate to transistor density. Applying formal verification to these increasingly-complex circuits is difficult, as it is often difficult (if not impossible) to decompose the problem by identifying clean partitions within a design. Even if the design can be partitioned, there is almost always a problem with lack of specifications. When specifications are available, they are usually out-of-date.

Over the years, many attempts have been made to address this problem. One of them is the use of high-level models (HLMs), functional models that are created at a higher level of abstraction than RTL. One of the persistent difficulties with HLMs is connecting them to the RTL. Often, an HLM is developed and serves as an initial "sketch pad" of a design, but then serves no further purpose and is abandoned as the low-level RTL implementation model is created.

My research in this area considers the creation and use of HLMs that are expressed in a language that can automatically be translated to a formal representation. This representation can be used for verification, and since it is executable, provides an early model of design functionality. Our goal is to establish an HLM representation that can continue to "live" as the design progresses.

Applications of Symbolic Simulation

Much of the early use of formal verification in commercial design involved the use of CTL model checkers, largely based on Ken McMillan's SMV system. Symbolic simulation, another approach, has not been applied as extensively. One of the reasons is likely that there is not a robust system (like SMV) that is publically available. Randy Bryant's COSMOS system is a notable exception, but is intended for switch-level verification.

Much of my research has addressed ways to effectively apply symbolic simulation in design verification. Symbolic simulation is an attractive platform for hardware verification. At it's simplest (without any symbolic data) it looks just like a logic simulator. And this is the environment that hardware designers are used to. However, effectively using symbolic simulation is non-trivial. Two primary difficulties are specifying desired behavior and controlling the complexity of the symbolic representation.

Specification. Self consistency is a way to automatically derive a useful specification from the hardware being verified. It is based on the observation that much of the complexity in modern hardware designs arises from performance-enhancing techniques like pipelining, superscalar execution, other forms of parallelism, and speculation. Functionally, the effects of these performance "carbunkles" should be transparent. Thus, if a design without performance enhancements is available, it can serve as a specification for a design with extensive performance enhancements. Further, it is often the case that the performance-enhanced design itself can yield a base implementation without performance enhancements. Other applications of self consistency are based on the observation that certain transactions or operations should be similar in some way--and then proving that the similarity is maintained for all combinations of inputs and state.

Complexity. All symbolic techniques encounter complexity problems because of their fundamental nature--simultaneous representation of many distinct values. Different representations scale for different problems in different ways. An important observation is that we often only care about design behavior for a certain class of inputs. And, while symbolically representing all possible behaviors may not be not be feasible, representing only the class of behaviors in the care set may be. The parametric representation is a way of implicitly encoding "care" conditions on the inputs to a symbolic simulator. It has facilitated symbolic simulation-based verification of many circuits that would otherwise have not been possible to verify.

These ideas are also detailed in the first two sections of my Ph.D. thesis, which contains a more thorough treatment of both subjects.

Pipelined Processor Verification

Processors we identified early-on as an ideal target for formal verification. Unfortunately, modern processors are far too complex to verify with even the most advanced formal techniques. Much research has been addressed at scaling the capabilities of formal techniques to apply to full processor descriptions.

To this date, this class of work has been limited to simple processors that are either special-purpose or academic. Steady progress continues to expand the application domain for these techniques.

Our research in this area extends work by Burch and Dill that discovered a way to automate a tedious aspect of pipeline verification: the generation of abstraction functions to relate pipeline state to specification state. Their flushing approach achieves success on relatively simple pipelines. Their unmodified approach fails more more complicated pipelines, like those found in out-of-order micro-architectures. Our work, based on the approach of Burch and Dill, provides a way to automate a portion of out-of-order pipeline verification.

Several different approaches for microprocessor verification are presented in the literature. Relating the different approaches has been difficult, particularly because they use different models, specifications, and even correctness criteria. Our work considers the relationships between the correctness criteria of the different approaches in the literature. The first paper presents a framework for classifying microprocessor correctness statements and includes a fairly thorough survey of the existing literature and how it fits in the framework. The second paper extends the framework to superscalar microprocessors and uses an improved notation.

Combined Model Checking and Theorem Proving

The combination of model checking and theorem proving is one of the most interesting problems in formal verification today, particularly in industrial applications of formal verification. Model checking is usually viewed as automatic but with limited capacity. On the other hand, theorem proving has essentially unlimited capacity but is very labor intensive.

Several research efforts have considered the combination of model checking and theorem proving. Most of these have been theorem-proving centric, in that the theorem prover is viewed as the central capability, with model checkers built "on top" as decision procedures. Our approach is to view the model checker as the central capability, and extend the model checker with integrated, lightweight theorem-proving support.

This approach allows model checking to be the initial and primary focus of user activities. Theorem proving is used to stitch together individual model checking runs into larger results. The first paper considers certain technical aspects encountered when implementing theorem proving and model checking in the same system. The second paper is at a higher-level and presents the overall philosophy of our approach and details a large case study.

Automated Deduction

One area of research in automated deduction considers algorithms that can be used to deduce the truth (or falsity) of logical formulas. If these algorithms are efficient, they can be encoded in computer programs and can prove theorems (deduce facts) about formulas of remarkable complexity. Many different logics and deduction systems for those logics have been proposed and are detailed in the literature.

This work involves the quantifier-free logic of uninterpreted functions with equality, a logic that is well-suited for modeling microprocessor pipelines at a fairly abstract level. We extend the base logic with certain "partially-interpreted" functions, for example, read and write support the modeling of memory structures. Later extensions by my colleagues include bit-vectors and linear arithmetic. The system described in the paper has evolved into the Stanford Validity Checker (SVC).

Simulation-Based Verification

Simulation is the predominant technique for functional verification. It's primary advantages are scalability and speed. It's primary disadvantage is limited coverage of design behavior--it is simply infeasible to exhaustively test every possible combination of inputs and state.

Several techniques are used to enhance the effectiveness of limited simulation cycles. One is the specification of event patterns at the micro-architectural level. These event patterns serve as specifications, and can be used to generate tests that will (hopefully) cover the behavior specified. Because test generation is not always feasible, they can also serve as simulation coverage monitors.

The PROTO system described in this paper has been widely deployed at Intel as a major part of simulation-based functional verification.

Robert Jones,  rjones @ ichips.intel.com
Last Modified: 10 January 2004