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
%0 Conference Paper
%1 hua_axiomatic_1992
%A Hua, Xin
%A Zhang, Hantao
%B VLSI, 1992., Proceedings of the Second Great Lakes Symposium on
%D 1992
%K automatic axiomatic design; first-order formal formulas; hardware laboratory; language; languages; prover; proving rewrite rule semantics; specification specification; theorem verification; {ILSL}
%P 183--190
%R 10.1109/GLSV.1992.218347
%T Axiomatic semantics of a hardware specification language
%X 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
@inproceedings{hua_axiomatic_1992,
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},
added-at = {2013-02-28T11:13:35.000+0100},
author = {Hua, Xin and Zhang, Hantao},
biburl = {https://www.bibsonomy.org/bibtex/2dea48eef7417074617457ebdb16e9fa1/fritzsolms},
booktitle = {{{VLSI}, 1992., Proceedings of the Second Great Lakes Symposium on}},
doi = {10.1109/GLSV.1992.218347},
interhash = {e93cbc2339003c7713dcb6f5ff4b4194},
intrahash = {dea48eef7417074617457ebdb16e9fa1},
keywords = {automatic axiomatic design; first-order formal formulas; hardware laboratory; language; languages; prover; proving rewrite rule semantics; specification specification; theorem verification; {ILSL}},
lccn = {0008},
month = feb,
pages = {183--190},
timestamp = {2013-02-28T11:13:51.000+0100},
title = {{Axiomatic semantics of a hardware specification language}},
year = 1992
}