基于广义符号轨迹赋值理论的模型检测

项目名称： 基于广义符号轨迹赋值理论的模型检测

项目编号： No.60973016

项目类型： 面上项目

立项/批准年度： 2010

项目学科： 自动化技术、计算机技术

项目作者： 杨国武

作者单位： 电子科技大学

项目金额： 30万元

中文摘要： 广义符号轨迹赋值（GSTE）是一种针对超大规模集成化电路设计的符号轨迹赋值的推广。符号轨迹赋值在Intel、IBM和Motorola等公司得到成功的应用。广义符号轨迹赋值可以验证无限时间区间上的omega性质，在Intel得到成功应用。但它发展时间不长，还不成熟。本项目针对五个方面：GSTE中断言图之间的蕴涵关系，细化与反例的产生，GSTE与传统模型检验的关系，软硬件协同验证，系统并发性质的验证，进行研究。目标是丰富GSTE理论，实现基于这些理论的高效、准确的形式化验证工具。基于语言的蕴涵关系可以转换为传统模型检验有限状态机之间的蕴涵关系。基于模型的蕴涵关系可以通过求断言图的极大模型来判断。如何在GSTE中引入SAT和按断言图作同步模拟是细化与产生反例的重要手段。比较GSTE检验方法与传统模型检验方法的差别，融合它们的优点，设计高效的形式化验证算法。同时建立软硬件统一的形式化描述方法。

中文关键词： 广义符号轨迹赋值；模型检测；SAT求解器；布尔网络；

英文摘要：

英文关键词： Generalized Symbolic Trajector；Model checking；SAT solver；Boolean network；