Formal verification of data-path circuits based on symbolic simulation

Author

Morihiro, Yoshifumi ; Toneda, T.

Author_Institution

Dept. of Comput. Sci., Tokyo Inst. of Technol., Japan

fYear

2000

fDate

2000

Firstpage

329

Lastpage

336

Abstract

This paper presents a formal verification method based on logic simulation. In our method, using symbolic values even circuits which include data paths can be verified without abstraction of data paths. 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 we can guarantee that for any applicable input vector sequences, the circuit and the specification behaves identically. We implemented the proposed method on a Unix workstation and verified some FIFO and LIFO circuits by using it

Keywords

formal verification; graph theory; logic simulation; symbol manipulation; FIFO circuits; LIFO circuits; Unix workstation; data-path circuits; formal verification; input vector sequences; logic simulation; specification; state graph; symbolic simulation; symbolic values; transition relation extraction; Circuit simulation; Computational modeling; Computer science; Computer simulation; Data mining; Formal verification; Information science; Logic circuits; Logic design; Workstations;

fLanguage

English

Publisher

ieee

Conference_Titel

Test Symposium, 2000. (ATS 2000). Proceedings of the Ninth Asian

Conference_Location

Taipei

ISSN

1081-7735

Print_ISBN

0-7695-0887-1

Type

conf

DOI

10.1109/ATS.2000.893645

Filename

893645