Verification of logic designs has been a long-standing bottleneck in the process of hardware design, where its automation and improvement of efficiency has demanding needs. Mainly simulation-based verification has been used for this purpose, and recently, coverage-driven verification has been widely used, of which target is improvement of some metric called coverage. Our target is the metric called toggle coverage. To find input patterns which cause some toggles on each signal, a SAT solver could be used, but this is computationally costly. In this paper, we study the effect of combination of random simulation and usage of a SAT solver. In particular, we use a SAT solver which can find multiple “diverse” solutions. With this solver, we can avoid generating similar patterns, which are unlikely to improve coverage. The experimental results show that, a small number of calls of a SAT solver can improve entire toggle coverage effectively, compared with simple random simulation.
Yosuke KAKIUCHI
Hiroshima Institute of Technology
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.
Copy
Yosuke KAKIUCHI, Kiyoharu HAMAGUCHI, "Coverage-Driven Design Verification Using a Diverse SAT Solver" in IEICE TRANSACTIONS on Fundamentals,
vol. E100-A, no. 7, pp. 1481-1487, July 2017, doi: 10.1587/transfun.E100.A.1481.
Abstract: Verification of logic designs has been a long-standing bottleneck in the process of hardware design, where its automation and improvement of efficiency has demanding needs. Mainly simulation-based verification has been used for this purpose, and recently, coverage-driven verification has been widely used, of which target is improvement of some metric called coverage. Our target is the metric called toggle coverage. To find input patterns which cause some toggles on each signal, a SAT solver could be used, but this is computationally costly. In this paper, we study the effect of combination of random simulation and usage of a SAT solver. In particular, we use a SAT solver which can find multiple “diverse” solutions. With this solver, we can avoid generating similar patterns, which are unlikely to improve coverage. The experimental results show that, a small number of calls of a SAT solver can improve entire toggle coverage effectively, compared with simple random simulation.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.E100.A.1481/_p
Copy
@ARTICLE{e100-a_7_1481,
author={Yosuke KAKIUCHI, Kiyoharu HAMAGUCHI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Coverage-Driven Design Verification Using a Diverse SAT Solver},
year={2017},
volume={E100-A},
number={7},
pages={1481-1487},
abstract={Verification of logic designs has been a long-standing bottleneck in the process of hardware design, where its automation and improvement of efficiency has demanding needs. Mainly simulation-based verification has been used for this purpose, and recently, coverage-driven verification has been widely used, of which target is improvement of some metric called coverage. Our target is the metric called toggle coverage. To find input patterns which cause some toggles on each signal, a SAT solver could be used, but this is computationally costly. In this paper, we study the effect of combination of random simulation and usage of a SAT solver. In particular, we use a SAT solver which can find multiple “diverse” solutions. With this solver, we can avoid generating similar patterns, which are unlikely to improve coverage. The experimental results show that, a small number of calls of a SAT solver can improve entire toggle coverage effectively, compared with simple random simulation.},
keywords={},
doi={10.1587/transfun.E100.A.1481},
ISSN={1745-1337},
month={July},}
Copy
TY - JOUR
TI - Coverage-Driven Design Verification Using a Diverse SAT Solver
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1481
EP - 1487
AU - Yosuke KAKIUCHI
AU - Kiyoharu HAMAGUCHI
PY - 2017
DO - 10.1587/transfun.E100.A.1481
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E100-A
IS - 7
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - July 2017
AB - Verification of logic designs has been a long-standing bottleneck in the process of hardware design, where its automation and improvement of efficiency has demanding needs. Mainly simulation-based verification has been used for this purpose, and recently, coverage-driven verification has been widely used, of which target is improvement of some metric called coverage. Our target is the metric called toggle coverage. To find input patterns which cause some toggles on each signal, a SAT solver could be used, but this is computationally costly. In this paper, we study the effect of combination of random simulation and usage of a SAT solver. In particular, we use a SAT solver which can find multiple “diverse” solutions. With this solver, we can avoid generating similar patterns, which are unlikely to improve coverage. The experimental results show that, a small number of calls of a SAT solver can improve entire toggle coverage effectively, compared with simple random simulation.
ER -