Hardware Research History

Hardware Research History

Computational Logic performed a broad range of research in hardware verification using the Nqthm and ACL2 logics as specification and proving tools. Some hardware examples developed by CLI include:
  1. the FM9001 microprocessor whose netlist design was expressed in our DUAL-EVAL hardware description language,
  2. an OBDD-based tautology checker,
  3. a fault analysis tool,
  4. a formalization of a small subset of VHDL, and
  5. a specification for the Motorola DSP 56100 family.
We employed these techniques on various government and commercial projects. The older FM8501 work is part of the Nqthm distribution.

VHDL

We spent some time studying an operational formal semantics for a subset of VHDL. The formal semantics were written in the ACL2 Logic. The purpose of this research was to provide a means to specify VHDL programs and to permit the verification of VHDL programs. The operational-style VHDL specification we developed can be used like a traditional VHDL simulator, but also admits the specification and verification of VHDL designs. VHDL, the VHSIC Hardware Description Language, is an event driven simulation language that permits netlist level and behavioral level descriptions of hardware designs. Its use is mandated by the U. S. Government for ASIC designs.

DSP

We worked with Motorola in Scottsdale, AZ, on the specification of a new, high-performance DSP, known as the Complex Arithmetic Processor (CAP). This 20-bit DSP is expected to be able to perform a 1024-point FFT in 131 microseconds. We formally specified the machine-level interface of the CAP as an aid in the architectural definition of the device, as well as providing a basis for verifying its internal hardware and the software that runs on it.

For a description of the CAP chip, see ``Architecture of a Complex Arithmetic Processor for Communication Signal Processsing'' written by Susan Gilfeather, John Gehman, and Calvin Harrison of Motorola's Government and Systems Technology Group.

For a description of CLI's work on the CAP chip, see ACL2 Theorems about Commercial Microprocessors.

This page is URL http://www.computationallogic.com/hardware/index.html