用于芯片系统验证的证明引擎研究

研究系统芯片设计方法和IP芯核的可重用特点，研究定理证明技术在SOC验证中的应用。研究如何把现有的定理证明系统如HOL、PVS等改造成一个轻型的面向通讯领域的定理证明引擎；通过验证实践建立面向通讯领域的证明对策和策略。研究公开的设计验证库OVL和针对通讯领域SOC芯片的验证扩充OVL验证库。探索把定量证明、模型检验和模拟验证有机结合起来的途径和方法。利用上述的OVL和Verilog的PLI编程接口实现面向通讯应用的SOC的基于平台的设计验证环境。