Despite the growing research effort in formal verification, industrial verification often relies on the constrained random simulation methodology, which is supported by constraint solvers as the stimulus generator integrated within simulator, especially for the large design with complex constraints nowadays. These stimulus generators need to be fast and well-distributed to maintain simulation performance. In this paper, we propose a dynamic method to guide stimulus generation by SAT solvers. An adjusting strategy named Tabu Search with Memory (TSwM) is integrated in the stimulus generator for the search and prune processes along with the constraint solver. Experimental results show that the method proposed in this paper could generate well-distributed stimuli with good performance.
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
Yanni ZHAO, Jinian BIAN, Shujun DENG, Zhiqiu KONG, Kang ZHAO, "Constrained Stimulus Generation with Self-Adjusting Using Tabu Search with Memory" in IEICE TRANSACTIONS on Fundamentals,
vol. E92-A, no. 12, pp. 3086-3093, December 2009, doi: 10.1587/transfun.E92.A.3086.
Abstract: Despite the growing research effort in formal verification, industrial verification often relies on the constrained random simulation methodology, which is supported by constraint solvers as the stimulus generator integrated within simulator, especially for the large design with complex constraints nowadays. These stimulus generators need to be fast and well-distributed to maintain simulation performance. In this paper, we propose a dynamic method to guide stimulus generation by SAT solvers. An adjusting strategy named Tabu Search with Memory (TSwM) is integrated in the stimulus generator for the search and prune processes along with the constraint solver. Experimental results show that the method proposed in this paper could generate well-distributed stimuli with good performance.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.E92.A.3086/_p
Copy
@ARTICLE{e92-a_12_3086,
author={Yanni ZHAO, Jinian BIAN, Shujun DENG, Zhiqiu KONG, Kang ZHAO, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Constrained Stimulus Generation with Self-Adjusting Using Tabu Search with Memory},
year={2009},
volume={E92-A},
number={12},
pages={3086-3093},
abstract={Despite the growing research effort in formal verification, industrial verification often relies on the constrained random simulation methodology, which is supported by constraint solvers as the stimulus generator integrated within simulator, especially for the large design with complex constraints nowadays. These stimulus generators need to be fast and well-distributed to maintain simulation performance. In this paper, we propose a dynamic method to guide stimulus generation by SAT solvers. An adjusting strategy named Tabu Search with Memory (TSwM) is integrated in the stimulus generator for the search and prune processes along with the constraint solver. Experimental results show that the method proposed in this paper could generate well-distributed stimuli with good performance.},
keywords={},
doi={10.1587/transfun.E92.A.3086},
ISSN={1745-1337},
month={December},}
Copy
TY - JOUR
TI - Constrained Stimulus Generation with Self-Adjusting Using Tabu Search with Memory
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 3086
EP - 3093
AU - Yanni ZHAO
AU - Jinian BIAN
AU - Shujun DENG
AU - Zhiqiu KONG
AU - Kang ZHAO
PY - 2009
DO - 10.1587/transfun.E92.A.3086
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E92-A
IS - 12
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - December 2009
AB - Despite the growing research effort in formal verification, industrial verification often relies on the constrained random simulation methodology, which is supported by constraint solvers as the stimulus generator integrated within simulator, especially for the large design with complex constraints nowadays. These stimulus generators need to be fast and well-distributed to maintain simulation performance. In this paper, we propose a dynamic method to guide stimulus generation by SAT solvers. An adjusting strategy named Tabu Search with Memory (TSwM) is integrated in the stimulus generator for the search and prune processes along with the constraint solver. Experimental results show that the method proposed in this paper could generate well-distributed stimuli with good performance.
ER -