IEICE TRANSACTIONS on Information
TPF: An Effective Method for Verifying Synchronous Circuits with Induction-Based Provers
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E81-D No.1 pp.12-18
- Publication Date
- 1998/01/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Category
- Computer Hardware and Design
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Kazuko TAKAHASHI, Hiroshi FUJITA, "TPF: An Effective Method for Verifying Synchronous Circuits with Induction-Based Provers" in IEICE TRANSACTIONS on Information,
vol. E81-D, no. 1, pp. 12-18, January 1998, doi: .
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.
URL: https://global.ieice.org/en_transactions/information/10.1587/e81-d_1_12/_p
Copy
@ARTICLE{e81-d_1_12,
author={Kazuko TAKAHASHI, Hiroshi FUJITA, },
journal={IEICE TRANSACTIONS on Information},
title={TPF: An Effective Method for Verifying Synchronous Circuits with Induction-Based Provers},
year={1998},
volume={E81-D},
number={1},
pages={12-18},
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.},
keywords={},
doi={},
ISSN={},
month={January},}
Copy
TY - JOUR
TI - TPF: An Effective Method for Verifying Synchronous Circuits with Induction-Based Provers
T2 - IEICE TRANSACTIONS on Information
SP - 12
EP - 18
AU - Kazuko TAKAHASHI
AU - Hiroshi FUJITA
PY - 1998
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E81-D
IS - 1
JA - IEICE TRANSACTIONS on Information
Y1 - January 1998
AB - 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.
ER -
English
