For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
TPF: An Effective Method for Verifying Synchronous Circuits with Induction-Based Provers
Kazuko TAKAHASHI Hiroshi FUJITA
IEICE TRANSACTIONS on Information and Systems
Publication Date: 1998/01/25
Print ISSN: 0916-8532
Type of Manuscript: Category: Computer Hardware and Design
design verification, hardware description, Boyer-Moore theorem prover, automated deduction, synchronous circuits,
Full Text: PDF>>
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.