### 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 language | English (US) |
---|---|

Title of host publication | Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications |

Editors | Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, Phillip J. Windley |

Publisher | Institute of Electrical and Electronics Engineers Inc. |

Pages | 22-31 |

Number of pages | 10 |

ISBN (Electronic) | 0818624604, 9780818624605 |

DOIs | |

State | Published - Jan 1 1991 |

Event | 1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications - Davis, United States Duration: Aug 28 1991 → Aug 30 1991 |

### Publication series

Name | Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications |
---|

### Conference

Conference | 1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications |
---|---|

Country | United States |

City | Davis |

Period | 8/28/91 → 8/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