My primary technical contributions concern the formalization and verification of a litany of microprocessor designs. These efforts involved specifying several microprocessor designs at the ISA level. To represent the designs of these microprocessor, I formalized several hardware descriptions languages (HDLs); these HDLs were formalized using the logic of the theorem-proving systems. Derivatives of my tools, developed on top of the ACL2 system, are now used by AMD, Centuar Technology, and IBM to help assure that their microprocessor designs are correct.
In the fifteen years I have been with UT Austin, I have supervised ten PhD students. I am presently (Fall, 2019) supervising two PhD students.
In 1985, I was the first to mechanically verify the correctness of the FM8501 microprocessor design using a theorem-proving program.
In 1990, Bishop Brock and I published a formal specification of the DUAL-EVAL HDL, which was used to specify the gate-level design of the FM9001 microprocessor. We mechanically verified the FM9001 DUAL-EVAL-based design; this design was translated into LSI Logic's Network Description Language (NDL). LSI Logic manufactured the FM9001 design; we extensively tested the resulting FM9001 microprocessor and never found an error. As far as I know, this is the only formally verified microprocessor design that has been manufactured.
While working at IBM, I (along with Will Adams and Damir Jamsek) developed the Verisym array verification tool. This tool provided for a proof-based approach for assuring the correctness of arrays (e.g., caches, TLBs, register files, etc.) In modern microprocessor design, arrays account for more transistors than all other components combined.
Also while at IBM, I (along with Mootaz Elnozahy) created and co-supervised (until I left for UT Austin) the IBM PERCS project. This 10-year-long project involved nearly 100 scientists and engineers, both from IBM and several universities.
While working at UT Austin, I (along with Robert Boyer) the Hash-CONS extension for the ACL2 theorem-proving system. In addition, we extended the ACL2 system to include function memoization and "fast" (constant-time) association lists. We also developed symbolic simulation for ACL2 language.
I (along with Robert Boyer and Serita Nelesen) developed a greatly improved consensus algorithm for phylogenetics computations; this algorithm greatly reduced the size of data sets that for which a consensus can be calculated.
With Shilpi Goel and Matt Kaufmann, I have developed a partial model of the x86 instruction-set architecture.
Since 2006, I have had a collaboration with Centaur Technology, a company that designs X86-compatible microprocessors that are sold by VIA. This effort involves a direct connection between my UT group, that includes another professor, three scientists, a group of PhD students, and a highly-skilled group I helped to attract to work at Centaur. We now have a very tight research and development relationship, where there is a bi-directional exchange of techniques being developed at both places. The Centaur management has allowed improvements in our core tool conceived at Centaur to flow back to UT for inclusion in our analysis tool, ACL2, which is now used by approximately 20 design engineers at Centaur. This approach has resulted in a huge advance in the scale of the problems we can address as well as the type of problems we are pursuing. This made it possible for us to provide Centaur with analysis tools much more advanced than can be leased or purchased at any price.
I have served as chairman of the FMCAD Conference steering committee from 2000 to 2019. I am president of FMCAD, Inc., a company dedicated to supporting the FMCAD Conference series.
Presently, I am working with Ivan Sutherland on the design, analysis, verification, testing, and implementation of RSFQ-based circuits.
To return to Hunt's homepage.