Formal Verification of Data-Path Circuits Based on Symbolic Simulation
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E85-D No.6 pp.965-974
- Publication Date
- 2002/06/01
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- PAPER
- Category
- Fault Tolerance
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Yoshifumi MORIHIRO, Tomohiro YONEDA, "Formal Verification of Data-Path Circuits Based on Symbolic Simulation" in IEICE TRANSACTIONS on Information,
vol. E85-D, no. 6, pp. 965-974, June 2002, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/e85-d_6_965/_p
Copy
@ARTICLE{e85-d_6_965,
author={Yoshifumi MORIHIRO, Tomohiro YONEDA, },
journal={IEICE TRANSACTIONS on Information},
title={Formal Verification of Data-Path Circuits Based on Symbolic Simulation},
year={2002},
volume={E85-D},
number={6},
pages={965-974},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={June},}
Copy
TY - JOUR
TI - Formal Verification of Data-Path Circuits Based on Symbolic Simulation
T2 - IEICE TRANSACTIONS on Information
SP - 965
EP - 974
AU - Yoshifumi MORIHIRO
AU - Tomohiro YONEDA
PY - 2002
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E85-D
IS - 6
JA - IEICE TRANSACTIONS on Information
Y1 - June 2002
AB - 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.
ER -
English
