中文摘要：

该文提出了一种针对多个难达目标状态的激励生成方法,该方法基于抽象引导的半形式化方法框架.采用一个评估函数对候选状态进行评价,该评估函数综合考虑了从一个状态到不同目标状态的全局抽象距离信息,评价出从各个状态到达某个目标状态或者同时到达多个目标状态的潜能,并以此指导模拟过程直到最终搜索到一条能同时覆盖多个目标状态的状态序列.此外,该文采用了基于路径约束求解的激励生成方式,这种方式结合了具体模拟和符号模拟技术,符号模拟沿着具体执行路径提取分支条件构成路径约束,通过约束条件的翻转与求解能够有效地产生输入向量,以一种较均衡的模式遍历设计的状态空间,帮助验证快速覆盖到目标.实验结果表明,该文方法能够有效地同时验证设计中的多个目标状态.

英文摘要：

In this paper, we propose a test generation method to cover multiple hard-to-reach states, which operates in an abstraction-guided simulation framework. An evaluation function, which considers the global abstract distance information for one state to different target states, is used to evaluate the potentiality of each candidate next state to targets and guide the simulation processes to cover multiple target states. In addition, a path constraint solving based test generation method which combines concrete simulation and symbolic simulation is used. Symbolic simulation walks in the design following the concrete path and extracts the corresponding symbolic expressions of the branch conditions in the path as path constraints. The test generation engine can generate valid input vectors through constraint mutation and solving, and it helps to search state in the design state space in a balanced manner. Experimental results show that our approach is effective in covering multiple target states.