For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Formal Verification of Data-Path Circuits Based on Symbolic Simulation
Yoshifumi MORIHIRO Tomohiro YONEDA
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2002/06/01
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Fault Tolerance
formal verification, simulation, state transition graph, data path, abstraction,
Full Text: PDF>>
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.