基于一阶符号轨迹计算理论的模型检测

符号轨迹计算方法是目前工业界应用最为成功的形式化验证方法之一，在Intel芯片设计的形式化验证中取得了巨大的成功。但到目前为止，STE仅局限于基于布尔类型的硬件电路系统的验证，还不能用于基于字(word)或者整数等一阶数据类型的高层硬件或者软件系统设计的验证。本项目申请将在经典STE研究的基础上，吸取其结合X值抽象与符号模拟的基本思想，对其进行扩展，建立起一阶STE的形式语义理论。主要内容包括：(1)一阶STE语义模型的研究；(2)一阶STE模型检测算法的研究以及实现；(3)基于一阶STE的抽象方法的研究；(4)一阶 STE方法与定理证明技术的结合；(5)一阶STE工具的实现与集成以及在实际软硬件系统验证中的应用。其成果可望对STE理论本身产生积极的影响，拓宽STE技术的研究范围,推动STE技术在高层硬件与软件系统的形式验证方面的应用。

符号轨迹计算方法是目前工业界应用最为成功的形式化验证方法之一，.在Intel芯片设计的形式化验证中取得了巨大的成功。.但到目前为止，STE仅局限于基于布尔类型的硬件电路系统的验证，..现代电路设计都在寄存器传输级别(RTL)或者行为级别上进行，.从而使得验证也逐渐从原来的布尔级别转向.一阶（或项）级别。针对这种情况，本项目在经典STE研究的基础上，对其进行扩展，.建立起一阶STE的形式语义理论以及验证算法。主要内容包括：(1)一阶STE语义模型的研究；.(2)一阶STE模型验证算法的研究以及实现;.(3)一阶 STE方法与定理证明技术的结合；.(4)一阶STE工具的实现与集成以及在实际软硬件系统验证中的应用。.其成果对STE理论本身产生积极的影响，拓宽STE技术的研究范围,.推动STE技术在高层硬件与软件系统的形式验证方面的应用。