IEICE TRANSACTIONS on Fundamentals
Applying an SMT Solver to Coverage-Driven Design Verification
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E101-A No.7 pp.1053-1056
- Publication Date
- 2018/07/01
- Publicized
- Online ISSN
- 1745-1337
- DOI
- 10.1587/transfun.E101.A.1053
- Type of Manuscript
- Special Section LETTER (Special Section on Design Methodologies for System on a Chip)
- Category
Authors
Kiyoharu HAMAGUCHI
Shimane University
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
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
Copy
@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},}
Copy
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 -
English
