n every department of physical science, there is as much science, properly so called, as there is mathematics."

My research centers on the mathematical modeling and analysis of computer hardware and software, i.e., computing as applied mathematics. "Computer science" might be an apt description of this endeavor—unfortunately, that term has been irretrievably abused.

Practical modeling of real computer systems often requires greater attention to detail than is typical of traditional mathematical domains. A variety of so-called "formal methods", based on special-purpose notations and mechanical reasoning tools, have been developed to ease this burden. These methods have been applied successfully across the computer industry, but their potential benefits remain largely unexplored. The emphasis has been on automatic tools that are easy to use but lack the versatility of interactive theorem proving. It is unfortunate that the value of a formal method is measured more often by its accessibility to the untrained user than by its ultimate utility as an aid to mathematical reasoning.

The effective systematic use of formal methods will require a broader view of the role of mathematics in the science of computing, which I envision as patterned after the classical physical sciences. Thus, I try to use formal methods where appropriate to support, rather than to replace, mathematical rigor.

Most of the papers listed below describe the formal analysis and ultimate proof of correctness of (hardware and software) designs that were created by other people. In some cases, this analysis exposed fatal flaws in the original designs. Some day, I hope to do something creative, but for now, this is the thing that I enjoy most and do best: finding fault in the efforts of others. (Hey, I am certainly not the first to build a career around a personality disorder. Mike Tyson and Mel Tillis come to mind. And what was the name of that French nightclub performer whose act was based on a profound case of chronic flatulence?)

"Nature is written in that great book which ever lies before our eyes -- I mean the universe -- but we cannot understand it if we do not first learn the language and grasp the symbols in which it is written. The book is written in the mathematical language, and the symbols are triangles, circles and other geometrical figures, without whose help it is impossible to comprehend a single word of it; without which one wanders in vain through a dark labyrinth." -- Galileo

A Mechanical Proof of Quadratic Reciprocity.

The primary significance of this last result, of course, was that it finally put to rest any suspicion that the 269 previously published proofs of this theorem were all flawed. By the way, it also put me in some good company.

More recently, I have repeated these proofs with the ACL2 prover. Generally, it is difficult to attach any practical significance to work of this sort. However, Piergiorgio Bertoli showed me a real application for

A Mechanical Proof of the Chinese Remainder Theorem.

From UT, I went to the Artificial Intelligence Program of Microelectronics and Computer Technology Corp. (MCC), where I developed

Proteus: A Frame-based Nonmonotonic Inference System.

This was largely a waste of time, although it did introduce me to logic programming and eventually led to

A Verified Prolog Compiler for the Warren Abstract Machine.

I later joined MCC's Formal Methods Project, where I got back to proving theorems and did some work on concurrent program verification:

A Verification System for Concurrent Programs Based on the Boyer-Moore Prover

A Mechanically Verified Incremental Garbage Collector.

In 1991, I went to Computational Logic, Inc. (CLI) to work on fault-tolerant hardware verification. This led to an analysis of the semantics of VHDL:

A Formalization of a Subset of VHDL

The application of interest was an asynchronous system of communicating processors:

Verification of Gate-Level VHDL Models of Synchronous and Asynchronous Circuits .

When CLI folded in 1995, I went to Advanced Micro Devices, Inc. (AMD), where I worked primarily on floating-point design verification. Here are some papers on our register-transfer logic (RTL) verification methodology:

Mechanical Verification of RTL: A Simple Floating-Point Multiplier

Verification of Pipeline Circuits

Formal Verification of Floating-Point RTL at AMD Using the ACL2 Theorem Prover

One aspect of this methodology is the translation of RTL to ACL2, which led me to an investigation of the semantics of Verilog and, in particular, an analysis of IEEE Standard 1362-2001:

A Note on the IEEE Verilog Simulation Cycle

Here are some applications:

Proof of IEEE Compliance of the AMD-K5 Floating Point Square Root Microcode

Proof of IEEE Compliance of the AMD-K7 Floating Point Multiplication, Division, and Square Root RTL

Mechanical Verification of RTL: The Athlon Floating-Point Adder

A Mechanically Verified Commercial SRT Divider

Computation and Formal Verification of SRT Quotient and Square Root Digit Selection Tables

Here is my rant on the accepted standard of correctness for floating-point designs:

Remarks on the IEEE Standard for Floating-Point Arithmetic

An outgrowth of my work is an evolving ACL2 library of floating-point arithmetic, which has been made publicly available through the ACL2 Web site in the hope that it will be useful to others who are interested in floating-point verification.

At CAV 2007, I gave an invited talk describing my experience at AMD:

A Mathematical Approach to RTL Verification

I also worked at AMD on a formal model of the x86 instruction set architecture. Here is a note on

Modeling the x87 Transcendental Instructions with Elementary Polynomial Approximations

In 2012, I joined Intel, where I continued my work on floating-point verification. John O'Leary and I defined a functional programming language for the purpose of modeling arithmetic algorithms to be implemented in RTL. The language was essentially a primitive subset of C augmented by the register class templates of SystemC and was called MASC (Modeling Algorithms in SystemC). In order to verify correctness of MASC programs, I implemented a translator to the ACL2 logic:

Modeling Algorithms in SystemC and ACL2

One application of MASC was a formal proof of correctness of a hardware implementation of the Diffie-Hellman key exchange algorithm known as Curve25519:

A Computationally Surveyable Proof of the Curve25519 Group Axioms

Two by-products of this project: a formalization of

Pratt Certification and the Primality of   2²⁵⁵ – 19

and an analysis of

Polynomial Terms and Sparse Horner Normal Form

In 2016, I moved to Arm. When I discovered the simpler register classes of Algorithmic C, MASC evolved into RAC (Restricted Algorithmic C) and along with ACL2 has become the basis of most formal floating-point verification at Arm. Here is a paper intended for ACL2 users that explains how I formally prove correctness of RAC models:

Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2

This one, which I presented at ARITH-2022, is intended for floating-point designers:

Formal Verification of a Chained Multiply-Add Design: Combining Theorem Proving and Equivalence Checking

I have published a book on my approach to arithmetic RTL verification and the underlying mathematical theory:

Formal Verification of Floating-Point Hardware Design: A Mathematical Approach

In my spare time, I sometimes engage in recreational theorem proving. I wrote a formal model of the Hebrew calendar and proved some theorems about it.

I've also developed an ACL2 formalization of group theory, which is described in a series of papers:

A Formalization of Finite Group Theory

A Formalization of Finite Group Theory: Part II

A Formalization of Finite Group Theory: Part III