Title :
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
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;
Conference_Titel :
Test Symposium, 2000. (ATS 2000). Proceedings of the Ninth Asian
Conference_Location :
Taipei
Print_ISBN :
0-7695-0887-1
DOI :
10.1109/ATS.2000.893645
