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
Pengesahan reka bentuk perkakasan berasaskan simulasi, khususnya, reka bentuk peringkat pemindahan daftar (RTL), telah digunakan secara meluas, dan telah menjadi salah satu kesesakan utama dalam proses reka bentuk. Salah satu pendekatan ialah pengesahan didorong liputan, sasarannya ialah peningkatan beberapa metrik yang dipanggil liputan. Dalam kerja kami sebelum ini, kami telah mencadangkan pengesahan didorong liputan menggunakan kedua-dua corak simulasi yang dijana secara rawak dan corak yang dijana oleh penyelesai SAT (kepuasan hati), dan telah menunjukkan keberkesanannya. Dalam makalah ini, kami melanjutkan pendekatan ini dengan penyelesai SMT (teori modulo kepuasan), yang boleh mengendalikan perhubungan aritmetik antara pembolehubah integer, titik terapung atau bit-vektor. Keputusan eksperimen menunjukkan bahawa lebih banyak modul aritmetik dimasukkan, lebih banyak kaedah berasaskan SMT menjadi lebih baik daripada kaedah hanya menggunakan penyelesai SAT.
Kiyoharu HAMAGUCHI
Shimane University
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
Kiyoharu HAMAGUCHI, "Applying an SMT Solver to Coverage-Driven Design Verification" in IEICE TRANSACTIONS on Fundamentals,
vol. E101-A, no. 7, pp. 1053-1056, July 2018, doi: 10.1587/transfun.E101.A.1053.
Abstract: Simulation-based verification of hardware designs, in particular, register-transfer-level (RTL) designs, has been widely used, and has been one of the major bottlenecks in design processes. One of the approaches is coverage-driven verification, of its target is improvement of some metric called coverage. In a prior work of ours, we have proposed a coverage-driven verification using both randomly generated simulation patterns and patterns generated by a SAT (satisfiability) solver, and have shown its effectiveness. In this paper, we extend this approach with an SMT (satisfiability modulo theory) solver, which can handle arithmetic relations among integer, floating-point or bit-vector variables. Experimental results show that the more arithmetic modules are included, the more an SMT-based method gets superior to the method using only a SAT solver.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.E101.A.1053/_p
Salinan
@ARTICLE{e101-a_7_1053,
author={Kiyoharu HAMAGUCHI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Applying an SMT Solver to Coverage-Driven Design Verification},
year={2018},
volume={E101-A},
number={7},
pages={1053-1056},
abstract={Simulation-based verification of hardware designs, in particular, register-transfer-level (RTL) designs, has been widely used, and has been one of the major bottlenecks in design processes. One of the approaches is coverage-driven verification, of its target is improvement of some metric called coverage. In a prior work of ours, we have proposed a coverage-driven verification using both randomly generated simulation patterns and patterns generated by a SAT (satisfiability) solver, and have shown its effectiveness. In this paper, we extend this approach with an SMT (satisfiability modulo theory) solver, which can handle arithmetic relations among integer, floating-point or bit-vector variables. Experimental results show that the more arithmetic modules are included, the more an SMT-based method gets superior to the method using only a SAT solver.},
keywords={},
doi={10.1587/transfun.E101.A.1053},
ISSN={1745-1337},
month={July},}
Salinan
TY - JOUR
TI - Applying an SMT Solver to Coverage-Driven Design Verification
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1053
EP - 1056
AU - Kiyoharu HAMAGUCHI
PY - 2018
DO - 10.1587/transfun.E101.A.1053
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E101-A
IS - 7
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - July 2018
AB - Simulation-based verification of hardware designs, in particular, register-transfer-level (RTL) designs, has been widely used, and has been one of the major bottlenecks in design processes. One of the approaches is coverage-driven verification, of its target is improvement of some metric called coverage. In a prior work of ours, we have proposed a coverage-driven verification using both randomly generated simulation patterns and patterns generated by a SAT (satisfiability) solver, and have shown its effectiveness. In this paper, we extend this approach with an SMT (satisfiability modulo theory) solver, which can handle arithmetic relations among integer, floating-point or bit-vector variables. Experimental results show that the more arithmetic modules are included, the more an SMT-based method gets superior to the method using only a SAT solver.
ER -