Proceedings of the Second Great Lakes Symposium on VLSI (1992)
Kalamazoo, MI, USA
Feb. 28, 1992 to Feb. 29, 1992
Xin Hua , Dept. of Comput. Sci., Iowa Univ., Iowa City, IA, USA
Hantao Zhang , Dept. of Comput. Sci., Iowa Univ., Iowa City, IA, USA
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.<
formal specification, specification languages, theorem proving
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.