The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Kertas kerja ini membentangkan kaedah pengesahan formal berdasarkan simulasi logik. Dalam kaedah kami, beberapa kelas litar terhad yang termasuk laluan data boleh disahkan tanpa pengabstrakan laluan data dengan menggunakan nilai simbolik. Pengesah kami mengekstrak perhubungan peralihan daripada graf keadaan (diberikan sebagai spesifikasi) yang dinyatakan menggunakan nilai simbolik dan mengesahkan berdasarkan simulasi menggunakan nilai simbolik tersebut jika litar berkelakuan betul berkenaan dengan setiap peralihan spesifikasi. Jika pengesah ditamatkan dengan "betul", maka ia boleh dijamin bahawa untuk sebarang jujukan vektor input yang berkenaan, litar dan spesifikasi berkelakuan sama. Kami telah melaksanakan kaedah yang dicadangkan pada stesen kerja Unix dan mengesahkan beberapa litar FIFO dan LIFO dengan menggunakannya.
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.
Salinan
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
Salinan
@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},}
Salinan
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 -