Formal Verification of Data-Path Circuits Based on Symbolic Simulation

スポンサーリンク

概要

• 論文の詳細を見る

• This paper presents a formal verification method based on logic simulation. In our method, some restricted class of circuits which include data paths can be verified without abstraction of data paths by using symbolic values. Our verifier extracts a transition relation from the state graph (given as a specification) which is expressed using symbolic values, and verifies based on simulation using those symbolic values if the circuit behaves correctly with respect to each transition of the specification. If the verifier terminates with "correct," then it can be guaranteed that for any applicable input vector sequence, the circuit and the specification behaves identically. We have implemented the proposed method on a Unix workstation and verified some FIFO and LIFO circuits by using it.

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

著者

• Yoneda Tomohiro

  Graduate School Of Information Science And Engineering Dept. Of Computer Science Tokyo Institute Of

• MORIHIRO Yoshifumi

  Graduate School of Information Science and Engineering, Dept. of Computer Science, Tokyo Institute o

• Morihiro Yoshifumi

  Graduate School Of Information Science And Engineering Dept. Of Computer Science Tokyo Institute Of

関連論文

• Formal Verification of Data-Path Circuits Based on Symbolic Simulation

スポンサーリンク