About Kookamara

I'm Jared Davis — Kookamara is my company for freelance consulting. I specialize in formal hardware and software verification, usually with ACL2.

Kookamara is Not Operating

In 2016 I started working full-time with the great formal verification group at Apple. As part of this, Kookamara is not currently operating and cannot accept new clients.

Qualifications at a Glance

I can't discuss my current work at Apple.

For many years I worked to formally verify the X86 processors designed at Centaur Technology. This work gave 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 involved frequent and productive collaboration with microcoders, logic designers, circuit designers, pre- and post-silicon verification engineers, external vendors, and univerity researchers.

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
• Web development (HTML, JavaScript, CSS, JSON, XML, etc.)
• 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 the (open source) VL Verilog Toolkit. This 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 was also responsible for maintaining VL in production use and for integrating it into a continuous integration flow.

X86 Instruction Specification. To formally specify the desired behavior of X86 instructions, I developed and maintained the Centaur X86 (“C86”) Specification, which covered over 500 integer, media, and floating-point operations. These ACL2 specifications were 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 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. Using a Lisp foreign function interface to directly invoke C/Assembly routines, it could achieve throughputs in the millions of tests per second. XVAL served double duty as a post-silicon validation suite and was run continually against newly fabricated chips. It was also used as a cross-check of Centaur's traditional golden model for simulation.

Execution Unit Verification. I 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 were automatically rerun as changes were made to the design. Since their initial completion, they revealed numerous bugs, including bugs related to: power management, operation decoding, a new variable shifter design, mixing of pipeline signals, and other problems. I was also involved in maintaining similar proofs for floating point execution units.

Microcode Verification. I was heavily involved in developing a microcode verification framework, particularly in creating a processor state representation that provides highly efficient execution and reasoning, developing believable instruction semantics that were connected to proven execution-unit specifications, extending the microcode assembler to automate modeling, and creating supporting proof automation.

Proof Engine Development. I contributed to the development of automated symbolic simulation and reasoning engines to support the above work. In particular, I 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 made significant improvements to the hons and memoization capabilities in ACL2. I 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 were all documented in this single framework and easily accessible by everyone throughout the company. I also led the effort to use this tool as the basis for ACL2's documentation.

Side Tools

Aside from the Formal Verification activities above, I was involved in many ad-hoc projects and 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 developed a linter for Verilog and SystemVerilog. The tool supported both standalone and differential linting (to compare warnings across two revisions of the design). This linter was integrated into Centaur's continuous integration flow, automatically reportings new bugs to logic designers via email and also via a web interface. It constantly found new bugs as logic designers made changes.

Equivalence Checking. I was involved in developing a standalone, push-button equivalence checking tool, and in reverse engineering the output from Synopsys Design Compiler in order to map the synthesized gate-level design back to the RTL. This work 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.