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

All Science Journal Classification (ASJC) codes

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

Fingerprint Dive into the research topics of 'TPF: An effective method for verifying synchronous circuits with induction-based provers'. Together they form a unique fingerprint.

  • Cite this