基于下一代验证引擎的事务级形式验证方法的研究

验证已成为集成电路设计的瓶颈，为了缩小验证与设计之间的差距，高层次的建模和验证显得越来越重要。研究内容主要是把SAT和SMT的方法引入到国际最前沿的更高层次的事务级模型（TLM），研究高效的事务级自动形式验证方法。研究工作主要分为三点：1. 从理论和方法上研究满足TLM的SAT问题和SMT问题。2.以SystemC验证库SCV为基础，研究使用下一代验证引擎- - 字位混合SAT求解器和可满足性模理论（SMT）中的先进技术进行事务级验证的相关算法，该算法包括随机化、定界模型检验、抽象细化等技术点。3.研究开发包含传输层、协议层、用户层的三层结构TLM验证平台，便于进行自动的数据检查、事务检查、基于断言的验证以及基于时态逻辑的性质检验。以上工作紧密相关，其中前两步工作是第三步工作的基础。本项目的研究成果将对事务级的验证产生重要影响。