TPF: An Effective Method for Verifying Synchronous Circuits with Induction-Based Provers

Kazuko TAKAHASHI  Hiroshi FUJITA  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E81-D       pp.12-18
Publication Date: 1998/01/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
Type of Manuscript: Category: Computer Hardware and Design
Keyword: 
design verification,  hardware description,  Boyer-Moore theorem prover,  automated deduction,  synchronous circuits,  

Full Text: PDF>>
Buy this Article


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.