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.
展开▼
机译：尽管形式验证方面的研究工作越来越多，但工业验证通常依赖于约束随机仿真方法，该方法由约束求解器作为集成在仿真器中的激励发生器支持，特别是对于当今具有复杂约束的大型设计。这些激励发生器需要快速且分布良好，以保持仿真性能。在本文中，我们提出了一种动态方法来指导SAT求解器的激励生成。一种名为 Tabu Search with Memory （TSwM） 的调整策略与约束求解器一起集成在用于搜索和修剪过程的激励生成器中。实验结果表明，本文提出的方法可以产生分布良好的刺激，并具有良好的性能。
展开▼
