Abstract
We propose a new method for hardware verification using the Boyer-Moore Theorem Prover. In this method, each signal of a sequential circuit is represented not as a waveform, but as a time parameterized function. A user simply describes the logical connection of the components of a circuit, and the separated form is mechanically derived. We formalize the method and show that the method not only realizes an efficient proof but also useful for debugging.
| Original language | English |
|---|---|
| Pages | 545-552 |
| Number of pages | 8 |
| Publication status | Published - Dec 1 1995 |
| Externally published | Yes |
| Event | Proceedings of the 1995 Asia and South Pacific Design Automation Conference, ASP-DAC'95 - Chiba, Jpn Duration: Aug 29 1995 → Sep 1 1995 |
Other
| Other | Proceedings of the 1995 Asia and South Pacific Design Automation Conference, ASP-DAC'95 |
|---|---|
| City | Chiba, Jpn |
| Period | 8/29/95 → 9/1/95 |
Fingerprint
All Science Journal Classification (ASJC) codes
- Computer Science Applications
- Computer Graphics and Computer-Aided Design
- Electrical and Electronic Engineering
Cite this
Time parameterized function method : a new method for hardware verification with the Boyer-Moore theorem prover. / Takahashi, Kazuko; Fujita, Hiroshi.
1995. 545-552 Paper presented at Proceedings of the 1995 Asia and South Pacific Design Automation Conference, ASP-DAC'95, Chiba, Jpn, .Research output: Contribution to conference › Paper
}
TY - CONF
T1 - Time parameterized function method
T2 - a new method for hardware verification with the Boyer-Moore theorem prover
AU - Takahashi, Kazuko
AU - Fujita, Hiroshi
PY - 1995/12/1
Y1 - 1995/12/1
N2 - We propose a new method for hardware verification using the Boyer-Moore Theorem Prover. In this method, each signal of a sequential circuit is represented not as a waveform, but as a time parameterized function. A user simply describes the logical connection of the components of a circuit, and the separated form is mechanically derived. We formalize the method and show that the method not only realizes an efficient proof but also useful for debugging.
AB - We propose a new method for hardware verification using the Boyer-Moore Theorem Prover. In this method, each signal of a sequential circuit is represented not as a waveform, but as a time parameterized function. A user simply describes the logical connection of the components of a circuit, and the separated form is mechanically derived. We formalize the method and show that the method not only realizes an efficient proof but also useful for debugging.
UR - http://www.scopus.com/inward/record.url?scp=0029485571&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0029485571&partnerID=8YFLogxK
M3 - Paper
AN - SCOPUS:0029485571
SP - 545
EP - 552
ER -