|
|
|---|
|
|
|
|---|
B. Brock and W. A. Hunt, Jr., “Formal
Analysis of the Motorola CAP DSP”, in M. Hinchey and J. Bowen,
editors, Industrial-Strength Formal Methods, Springer-Verlag,
pp. 81-115, 1999.
Relevance: first industrial application of
operational semantics with ACL2 and the first complete formal specification
of a commercially designed microprocessor
Abstract
We describe our formal specification of Motorola's Complex Arithmetic Processor (CAP) Digital Signal Processor (DSP) and our subsequent use of this specification in formal analyses of the CAP hardware and software. The CAP was designed by Motorola Government Systems and Technology Group (Scottsdale, Arizona), which, as a part of their business, builds and sells purpose-built products. The CAP is an ASIC that was designed to efficiently implement a number of signal processing algorithms required in digital communications. Motorola's CAP is a super-scalar, pipelined DSP with seven memories and more than 20 functional units. Motorola's specification for the CAP was captured using the Cadence Signal Processing (SPW) (Cadence, 1994) toolsuite; the design is represented as a series of drawings that specify register files, data manipulation units, and interconnecting busses. We have completely specified the CAP (Gilfeather et al, 1994) using the formal logic ACL2 (Kaufmann and Moore, 1996). Our specification is executable and can be used as a simulator as well as a basis for proving the correctness of the CAP hardware design and CAP programs. We believe our specification is bit-for-bit exact with respect to the SPW specification produced by Motorola, and was created by hand translating Motorola's SPW drawings for the CAP. We have used our CAP specification to analyse the CAP instruction pipeline and various CAP algorithms. We believe that the specification developed is the largest of its kind, as this is the only formal specification of which we are aware for a complete commercial design. We believe that the use of mathematical logic for modeling and reasoning about hardware designs such as we have demonstrated here can provide assurance of circuit design correctness well beyond what is available from current CAD techniques.
See the discussion of the CAP DSP project in operational-semantics-2__other-examples.