Proceedings of the Second Great Lakes Symposium on VLSI (1992)

Kalamazoo, MI, USA

Feb. 28, 1992 to Feb. 29, 1992

ISBN: 0-8186-2610-0

pp: 183-190

Xin Hua , Dept. of Comput. Sci., Iowa Univ., Iowa City, IA, USA

Hantao Zhang , Dept. of Comput. Sci., Iowa Univ., Iowa City, IA, USA

ABSTRACT

Formal hardware design verification is to examine whether a structural specification of a circuit meets its behavioral specification. Despite the progress in formal verification, there is a big gap between hardware designers and verifiers, partially because there are no common specification languages for them to use. The authors show that formal semantics could bridge such a gap. By providing an axiomatic semantics to an existing hardware design language called the Iowa logic specification language (ILSL), the authors show that a circuit description in ILSL can be automatically converted into a set of first-order formulas which is the semantic description of the circuit and is acceptable by an existing theorem prover called the rewrite rule laboratory (RRL). In particular, they show how iterative statements of ILSL are converted into recursive functions of RLL. Their work thus results in a uniform specification language in which both hardware design and automatic verification can be done.<>

INDEX TERMS

formal specification, specification languages, theorem proving

CITATION

Xin Hua and Hantao Zhang, "Axiomatic semantics of a hardware specification language,"

*Proceedings of the Second Great Lakes Symposium on VLSI(GLSV)*, Kalamazoo, MI, USA, , pp. 183-190.

doi:10.1109/GLSV.1992.218347

CITATIONS