Computer Science ETDs

Publication Date

7-8-1974

Abstract

While there are well-known techniques for proving the correctness of software (programs), hardware designs have apparently not been proven correct previously. A method for designing and proving the correctness of a particular kind of hardware, combinational cellular logic arrays, is developed. Algorithms are specified in a cellular logic Hardware design language that is suitable for the associated correctness proof to be given. Programs written in the language are then translated directly into an array design whose correctness is implied by the correctness of the program. The practical problem of choosing particular array dimensions that will be necessary and sufficient for the correct implementation of a given class of computations is also considered.

The cellular logic produced is strictly combinational, with no clocking or memory required. Restrictions on the elements of the hardware design language (e.g. limiting multiplication to powers of the base) can lead to the design of algorithms that result in more efficient array designs, usually at the expense of more complicated programming. A beneficial side effect of this approach to array synthesis is that the resulting array designs are documented in a unified, high-level reference language, as well as the usual cell-design-plus-interconnections logical description. In the conclusion are some suggestions for further research, as well as some observations on why hardware correctness proofs have apparently not been achieved previously.

The Appendix gives an example of the complete design procedure, from an algorithm specified in the cellular logic design language, with the associated correctness proof, to the resulting array design.

Language

English

Document Type

Dissertation

Degree Name

Computer Science

Level of Degree

Doctoral

Department Name

Department of Computer Science

First Committee Member (Chair)

Ronald Clifford DeVries

Second Committee Member

Harold Knud Knudsen

Third Committee Member

Edgar John Gilbert

Fourth Committee Member

Dale Sparks

Download

Share

COinS