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
하드웨어 설계, 특히 RTL(Register-Transfer-level) 설계의 시뮬레이션 기반 검증이 널리 사용되어 왔으며 설계 프로세스의 주요 병목 현상 중 하나였습니다. 접근 방식 중 하나는 커버리지 기반 검증이며, 그 목표는 커버리지라는 일부 측정항목을 개선하는 것입니다. 이전 연구에서 무작위로 생성된 시뮬레이션 패턴과 SAT(satisfiability) 솔버에서 생성된 패턴을 모두 사용하는 Coverage-Driven 검증을 제안하고 그 효율성을 보여주었습니다. 본 논문에서는 정수, 부동 소수점 또는 비트 벡터 변수 간의 산술 관계를 처리할 수 있는 SMT(만족도 모듈로 이론) 솔버를 사용하여 이 접근 방식을 확장합니다. 실험 결과, 산술 모듈을 많이 포함할수록 SMT 기반 방법이 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.
부
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
부
@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},}
부
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 -