TPF: An effective method for verifying synchronous circuits with induction-based provers

Kazuko Takahashi, Hiroshi Fujita

Research output: Contribution to journalArticle

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 languageEnglish
Pages (from-to)12-18
Number of pages7
JournalIEICE Transactions on Information and Systems
VolumeE81-D
Issue number1
Publication statusPublished - Jan 1 1998

Fingerprint

Networks (circuits)

All Science Journal Classification (ASJC) codes

  • Software
  • Hardware and Architecture
  • Computer Vision and Pattern Recognition
  • Electrical and Electronic Engineering
  • Artificial Intelligence

Cite this

TPF : An effective method for verifying synchronous circuits with induction-based provers. / Takahashi, Kazuko; Fujita, Hiroshi.

In: IEICE Transactions on Information and Systems, Vol. E81-D, No. 1, 01.01.1998, p. 12-18.

Research output: Contribution to journalArticle

@article{c4977ecba21842a59113c392e9ce2854,
title = "TPF: An effective method for verifying synchronous circuits with induction-based provers",
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.",
author = "Kazuko Takahashi and Hiroshi Fujita",
year = "1998",
month = "1",
day = "1",
language = "English",
volume = "E81-D",
pages = "12--18",
journal = "IEICE Transactions on Information and Systems",
issn = "0916-8532",
publisher = "一般社団法人電子情報通信学会",
number = "1",

}

TY - JOUR

T1 - TPF

T2 - An effective method for verifying synchronous circuits with induction-based provers

AU - Takahashi, Kazuko

AU - Fujita, Hiroshi

PY - 1998/1/1

Y1 - 1998/1/1

N2 - 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.

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.

UR - http://www.scopus.com/inward/record.url?scp=0031703114&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0031703114&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0031703114

VL - E81-D

SP - 12

EP - 18

JO - IEICE Transactions on Information and Systems

JF - IEICE Transactions on Information and Systems

SN - 0916-8532

IS - 1

ER -