Abstract
We propose a new method for verifying synchronous circuits using the Boyer-Moore Theorem Prover (BMTP) based on an efficient use of induction. The method contains two techniques. The one is the representation method of signals. Each signal is represented not as a waveform, but as a time parameterized function. The other is the mechanical transformation of the circuit description. A simple description of the logical connection of the components of a circuit is transformed into such a form that is not only acceptable as a definition of BMTP but also adequate for applying induction. We formalize the method and show that it realizes an efficient proof.
| Original language | English |
|---|---|
| Pages (from-to) | 12-18 |
| Number of pages | 7 |
| Journal | IEICE Transactions on Information and Systems |
| Volume | E81-D |
| Issue number | 1 |
| Publication status | Published - Jan 1 1998 |
All Science Journal Classification (ASJC) codes
- Software
- Hardware and Architecture
- Computer Vision and Pattern Recognition
- Electrical and Electronic Engineering
- Artificial Intelligence