## Abstract

Ascertaining correctness of digital hardware designs through simulation does not scale-up for large designs because of the sheer combinatorics of the problem. Formal verification of hardware designs holds promise because its computational complexity is of the order of number of different types of components (and not number of components in the design). This approach requires the specification of the behavior and the design in a formal language, and reason with them using a theorem prover. In this paper we attempt to develop a methodology for writing and using these specifications for some important classes of hardware circuits. We examine digital hardware verification in the HOL-90 environment. (HOL-90 is a proof checker written in Standard ML which assists in mechanically checking a formal proof of hardware correctness.) In particular, we analyze proofs for a variety of circuits, and develop proof strategies for combinational circuits and restricted sequential circuits. Overall, this approach makes the theorem proving task less tedious and provides guidance to the user in carrying out proofs.

Original language | English |
---|---|

Pages | 451-458 |

Number of pages | 8 |

DOIs | |

State | Published - 1996 |

Event | The IEEE 1996 National Aerospace and Electronics Conference - Dayton, United States Duration: May 20 1996 → May 23 1996 |

### Conference

Conference | The IEEE 1996 National Aerospace and Electronics Conference |
---|---|

Country/Territory | United States |

City | Dayton |

Period | 5/20/96 → 5/23/96 |

## ASJC Scopus Subject Areas

- General Engineering

## Keywords

- Hardware
- Computational modeling
- Combinatorial mathematics
- formal verificatioin
- Computational complexity
- Formal languages
- Writing
- Standards development
- Combinational circuits
- Sequential circuits

## Disciplines

- Communication Technology and New Media
- Databases and Information Systems
- OS and Networks
- Science and Technology Studies