The search functionality is under construction.

The search functionality is under construction.

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

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.

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 -