11410 Windermere Meadows
Austin, TX 78759 USA
Since 2008, I have worked to formally verify the X86 processors designed at Centaur Technology. This work has given me a broad perspective of the verification effort that spans everything from hardware modeling, specification development, proof engineering, reasoning engines, build integration, systems support, and day-to-day operations. It has involved frequent and productive collaboration with microcoders, logic designers, circuit designers, pre- and post-silicon verification engineers, external vendors, and univerity researchers.
I'd be excited to help with your verification efforts.
Qualifications at a Glance
I have 12 years of ACL2 experience including
- Industrial experience at Centaur Technology and Rockwell Collins
- Ph.D. research completed at UT Austin, developing a verified ACL2-like prover
- Administrator and top contributor to the Community Books project
- Member of the gold-medal ACL2 team in the VSTTE 2012 competition
- Editor of the ACL2 Workshop 2013
- Author of many ACL2-related academic papers
- Author of libraries like std, xdoc, vl, esim, bitops, bridge, aig, ubdd, 4v, and many more
- Author of ACL2(h) extensions such as hons, fast alists, and serialize routines
I have broad experience beyond ACL2, including
- Hardware description languages (Verilog, SystemVerilog)
- Systems programming languages (C, C++, Java, assembly)
- Scripting languages (Ruby, Perl, etc), build systems, and Unix in general
- Lisp, ML, and other functional languages
- Multithreading, networking, IPC, GUIs, GPGPU, databases, parsers, ...
Some Recent Projects
Verilog and SystemVerilog Modeling. To create the formal models of hardware modules to be analyzed, I developed and have maintained the the (open source) VL Verilog Toolkit. This has required a careful study of the language standards and the behavior of commercial simulators. Models created by VL are amenable to symbolic simulation and comprise the basis for all formal verification at Centaur. I have also been responsible for maintaining VL in production use and for integrating it into our continuous integration flow.
X86 Instruction Specification. To formally specify the desired behavior of X86 instructions, I developed and have maintained the Centaur X86 (“C86”) Specification, which now covers over 500 integer, media, and floating-point operations. These ACL2 specifications are designed to achieve high performance and to faciltate effective reasoning, e.g., by carefully controlling case splits and using a style that is amenable to symbolic simulation.
X86 Specification Validation. To validate these C86 specifications against Intel hardware, I developed and have maintained the high-speed XVAL testing framework. It compares C86 specifications against corresponding assembly routines on millions of crafted tests, random tests, and directed semi-random tests. Based on a Lisp foreign function interface to directly invoke C/Assembly routines, it can achieve throughputs in the millions of tests per second. XVAL serves double duty as a post-silicon validation suite and is run continually against new Centaur chips. It is also used as a cross-check of Centaur's traditional golden model for simulation.
Execution Unit Verification. I have constructed and maintained specifications and ACL2 proofs establishing the correctness of every instruction implemented by Centaur's media unit, and for the vast majority of instructions implemented by Centaur's integer units. These proofs are automatically rerun when changes are made to the design. Since their initial completion, they have revealed bugs on 12 occasions, including bugs related to: power management, operation decoding, a new variable shifter design, mixing of pipeline signals, and other problems. I have also maintained similar proofs for floating point execution units.
Microcode Verification. I have been heavily involved in developing a microcode verification framework. I have been particularly involved in creating a processor state representation that provides highly efficient execution and reasoning, developing believable instruction semantics that are connected to proven execution-unit specifications, extending the microcode assembler to automate modeling, and creating supporting proof automation.
Proof Engine Development. I have been involved in the ongoing development of automated symbolic simulation and reasoning engines to support the above work. I have integrated ACL2 with off-the-shelf SAT solvers, developed representations and algorithms for working with four-valued logics, implemented verified AIG and BDD algorithms, and made improvements to the GL symbolic simulation framework. To support these efforts I have made significant improvements to the hons and memoization capabilities in ACL2. I have also developed many of the core ACL2 libraries, e.g., for bit-vector arithmetic, data structures, and so on. Most of these tools are open source.
Documentation. To document our tools and to make our proof results and specifications accessible throughout Centaur, I developed the XDOC documentation system for ACL2. Centaur's full formal verification effort, including C86 specifications, XVAL coverage, unit-level proofs, microcode proofs, and supporting tools like VL are all documented in this single framework and easily accessible by everyone throughout the company. I have also led the effort to use this tool as the basis for the ACL2's documentation.
Aside from the Formal Verification activities above, I have been involved in many ad-hoc projects and have found many opportunities to re-purpose our formal verification work to create useful side tools.
Verilog Linting. Reusing much of the parsing and analysis found in the VL Verilog Toolkit, I have developed a linter for Verilog and SystemVerilog. The tool supports both standalone and differential linting (to compare warnings across two revisions of the design). This linter is integrated into Centaur's continuous integration flow, automatically reportings new bugs to logic designers via email and also via a web interface. It constantly finds new bugs as logic designers make changes.
Equivalence Checking. I have been involved in developing a standalone, push-button equivalence checking tool, and in reverse engineering the output from Synopsys Design Compiler in order to map it back to the RTL. This work had facilitated formal equivalence checking and also had other applications such as timing analysis.
Verilog Refactoring. For a particular design effort, we wanted to safely convert a legacy module (a large block, implemented by circuit designers, with many transistor-level constructs and no corresponding RTL), into a clean, RTL-level design that logic designers could understand, maintain, and use for synthesis. I developed a Verilog refactoring tool to significantly automate lifting the design to RTL, with equivalence checking support at each step. The resulting RTL was drastically simpler, largely synthesizable, and sped up whole-chip simulations by 17% despite only targetting a small portion of the overall processor. The tool would later be valuable when collaborating with another company, and for other internal projects.
Next Up: Your Project?
I am available for consulting and development on a contract basis. If you think you might like to work with me, let's chat:
11410 Windermere Meadows
Austin, TX 78759 USA