基于全局时态逻辑(GTL)的验证和测试生成研究

GTL-based Verification and Test Generation

基于时态逻辑,定义了标准的逻辑操作公式、公理和扩展定理。根据测试生成和验证所要求的初始特性,提出了全局时态逻辑（Global Temporal Logic）GTL,避免了验证和测试中的回溯问题,从而提高验证和测试的效率。另外根据电路节点的扇入和扇出特性,介绍了利用时序线等启发知识来提高搜索策略的方法。

This paper defines the standard logic operation formula, axiom and extended theorem based on the TL (Temporal Logic). In order to avoid backtracking operation in verification and test senera-tion, GTL (Global Temporal Logic) is described in accordance with the initial featares required by the test generation and verification, so that the efficiency is greatly improved. Besides, this paper introduces the method to improve the search strategy through sequential line according to the charateristices of the circuit nodes.