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
Apesar do crescente esforço de pesquisa em verificação formal, a verificação industrial muitas vezes depende da metodologia de simulação aleatória restrita, que é apoiada por solucionadores de restrições como gerador de estímulos integrado ao simulador, especialmente para projetos grandes com restrições complexas atualmente. Esses geradores de estímulos precisam ser rápidos e bem distribuídos para manter o desempenho da simulação. Neste artigo, propomos um método dinâmico para orientar a geração de estímulos por solucionadores SAT. Uma estratégia de ajuste denominada Busca Tabu com Memória (TSwM) é integrada no gerador de estímulos para os processos de busca e remoção junto com o solucionador de restrições. Resultados experimentais mostram que o método proposto neste artigo poderia gerar estímulos bem distribuídos com bom desempenho.
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.
Copiar
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
Copiar
@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},}
Copiar
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 -