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

スポンサーリンク

概要

• 論文の詳細を見る

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

• 社団法人電子情報通信学会の論文
• 1998-01-25

著者

• Fujita Hiroshi

  Advanced Technology R&ampd Center Mitsubishi Electric Corporation:department Of Intelligent Syst

• TAKAHASHI Kazuko

  Advanced Technology R&D Center, Mitsubishi Electric Corporation

• Takahashi Kazuko

  Advanced Technology R&ampd Center Mitsubishi Electric Corporation:jatr Interpreting Telecommunications Research Laboratories

関連論文

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

スポンサーリンク