符号轨迹计值的形式化语义及模型检测技术研究

符号轨迹计值方法(Symbloic Trajectory evaluation,简称为STE)是工业界目前应用最为成功的硬件形式化验证方法之一，在Intel，Motorola,IBM等公司的形式化验证项目中取得了巨大的成功。但这种来自工业界的验证方法的形式化语义基础，以及与经典的基于模型检测与定理证明的形式化验证方法之间的联系还远未被学术界深入系统的研究。本项目旨在研究STE的形式化语义，及其模型检测算法。主要内容包括：（1）STE(及其各种扩展)的形式化语义研究，弄清STE的四值逻辑语义模型与经典的符号模型检测的语义模型的联系；(2)STE模型检测算法的研究；(3)基于STE的性质组合理论的研究；(4)STE方法在复杂电路的验证中的应用。这些工作将完善STE的理论基础，扩展STE的应用范围，提高STE模型检测算法的效率，并将推动STE在复杂硬件系统验证中的应用。