Word-Level Equivalence Checking in Bit-Level Accuracy by Synthesizing Designs onto Identical Datapath
Summary :
Equivalence checking is one of the most important issues in VLSI design to guarantee that bugs do not enter designs during optimization steps or synthesis steps. In this paper, we propose a new word-level equivalence checking method between two models before and after high-level synthesis or behavioral optimization. Our method converts two given designs into RTL models which have same datapaths so that behaviors by identical control signals become the same in the two designs. Also, functional units become common to the two designs. Then word-level equivalence checking techniques can be applied in bit-level accuracy. In addition, we propose a rule-based equivalence checking method which can verify designs which have complicated control structures faster than existing symbolic simulation based methods. Experimental results with realistic examples show that our method can verify such designs in practical periods.
- Publication
- IEICE TRANSACTIONS on Information Vol.E92-D No.5 pp.972-984
- Publication Date
- 2009/05/01
- Publicized
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.E92.D.972
- Type of Manuscript
- Special Section PAPER (Special Section on Formal Approach)
- Category
- Hardware Verification
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
Tasuku NISHIHARA, Takeshi MATSUMOTO, Masahiro FUJITA, "Word-Level Equivalence Checking in Bit-Level Accuracy by Synthesizing Designs onto Identical Datapath" in IEICE TRANSACTIONS on Information,
vol. E92-D, no. 5, pp. 972-984, May 2009, doi: 10.1587/transinf.E92.D.972.
Abstract: Equivalence checking is one of the most important issues in VLSI design to guarantee that bugs do not enter designs during optimization steps or synthesis steps. In this paper, we propose a new word-level equivalence checking method between two models before and after high-level synthesis or behavioral optimization. Our method converts two given designs into RTL models which have same datapaths so that behaviors by identical control signals become the same in the two designs. Also, functional units become common to the two designs. Then word-level equivalence checking techniques can be applied in bit-level accuracy. In addition, we propose a rule-based equivalence checking method which can verify designs which have complicated control structures faster than existing symbolic simulation based methods. Experimental results with realistic examples show that our method can verify such designs in practical periods.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E92.D.972/_p
Copy
@ARTICLE{e92-d_5_972,
author={Tasuku NISHIHARA, Takeshi MATSUMOTO, Masahiro FUJITA, },
journal={IEICE TRANSACTIONS on Information},
title={Word-Level Equivalence Checking in Bit-Level Accuracy by Synthesizing Designs onto Identical Datapath},
year={2009},
volume={E92-D},
number={5},
pages={972-984},
abstract={Equivalence checking is one of the most important issues in VLSI design to guarantee that bugs do not enter designs during optimization steps or synthesis steps. In this paper, we propose a new word-level equivalence checking method between two models before and after high-level synthesis or behavioral optimization. Our method converts two given designs into RTL models which have same datapaths so that behaviors by identical control signals become the same in the two designs. Also, functional units become common to the two designs. Then word-level equivalence checking techniques can be applied in bit-level accuracy. In addition, we propose a rule-based equivalence checking method which can verify designs which have complicated control structures faster than existing symbolic simulation based methods. Experimental results with realistic examples show that our method can verify such designs in practical periods.},
keywords={},
doi={10.1587/transinf.E92.D.972},
ISSN={1745-1361},
month={May},}
Copy
TY - JOUR
TI - Word-Level Equivalence Checking in Bit-Level Accuracy by Synthesizing Designs onto Identical Datapath
T2 - IEICE TRANSACTIONS on Information
SP - 972
EP - 984
AU - Tasuku NISHIHARA
AU - Takeshi MATSUMOTO
AU - Masahiro FUJITA
PY - 2009
DO - 10.1587/transinf.E92.D.972
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E92-D
IS - 5
JA - IEICE TRANSACTIONS on Information
Y1 - May 2009
AB - Equivalence checking is one of the most important issues in VLSI design to guarantee that bugs do not enter designs during optimization steps or synthesis steps. In this paper, we propose a new word-level equivalence checking method between two models before and after high-level synthesis or behavioral optimization. Our method converts two given designs into RTL models which have same datapaths so that behaviors by identical control signals become the same in the two designs. Also, functional units become common to the two designs. Then word-level equivalence checking techniques can be applied in bit-level accuracy. In addition, we propose a rule-based equivalence checking method which can verify designs which have complicated control structures faster than existing symbolic simulation based methods. Experimental results with realistic examples show that our method can verify such designs in practical periods.
ER -
English
