Formal Verification of Data-Path Circuits Based on Symbolic Simulation

Yoshifumi MORIHIRO  Tomohiro YONEDA  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E85-D    No.6    pp.965-974
Publication Date: 2002/06/01
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Fault Tolerance
Keyword: 
formal verification,  simulation,  state transition graph,  data path,  abstraction,  

Full Text: PDF>>
Buy this Article


Summary: 
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.