Verifying arithmetic hardware in higher-order logic

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

Theorem-based design uses logical inference rather than simulation to determine or verify the properties of design implementations. The initial effort to make such an approach practical is large when compared to conventional simulation. However, the cost of this effort is typically incurred only once. The hardware descriptions are parameterized so that the verification results are applicable to an entire set of designs rather than just one instantiation. To illustrate these ideas, the logical structure used to verify arithmetic hardware in HOL is outlined. In particular, the role of data abstraction, r0ecursion, and induction is shown.

Original languageEnglish (US)
Title of host publicationProceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications
EditorsMyla Archer, Jeffrey J. Joyce, Karl N. Levitt, Phillip J. Windley
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages22-31
Number of pages10
ISBN (Electronic)0818624604, 9780818624605
DOIs
StatePublished - Jan 1 1991
Event1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications - Davis, United States
Duration: Aug 28 1991Aug 30 1991

Publication series

NameProceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications

Conference

Conference1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications
CountryUnited States
CityDavis
Period8/28/918/30/91

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Logic
  • Computer Science Applications
  • Hardware and Architecture
  • Software
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'Verifying arithmetic hardware in higher-order logic'. Together they form a unique fingerprint.

  • Cite this

    Chin, S. K. (1991). Verifying arithmetic hardware in higher-order logic. In M. Archer, J. J. Joyce, K. N. Levitt, & P. J. Windley (Eds.), Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications (pp. 22-31). [596268] (Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/HOL.1991.596268