论文部分内容阅读
随着集成电路复杂度的增加，通过编写定向测试为主导的传统验证方法已经无法满足集成电路设计的需求，硬件验证难度也越来越大，集成电路验证成为硬件开发中的瓶颈。同时，随着人们对安全意识的不断提高，硬件安全性也成为硬件设计中需要考虑的重要问题之一。 本文立足ARMv8处理器，从功能性和安全性两个角度对硬件验证进行了研究。本文的主要工作如下: (1)在基于VMM（Verification Methodology Manual）验证方法学，以及传统功能正确性验证的研究上，结合受约束的随机测试方法，设计开发出层次化、可重用、高扩展的验证平台。在对ARMv8处理器核进行设计验证过程中，该验证平台发挥了重要的作用。ARMv8处理器核验证过程中一共使用39条测试用例(testcase)，测试用例采用4线程结构，每个线程包含大约10万条指令，累计执行约1500万条指令，使得ARMv8主要功能模块的覆盖率都在70％以上，许多模块达到80％-90％的覆盖率。 (2)设计开发ARMv8处理器中重要模块FPU的验证平台。通过已经实现ARMv8架构的gem5平台，利用SystemVerilog中的DPI接口，将作为参考模型的gem5中浮点运算单元模块嵌入到FPU验证平台中。使用该设计方案完成的FPU验证平台在指令执行性能和bug查找方面都有显著的表现; (3)通过形式化辅助工具——Coq语言，将ARMv8处理器中的模块转化成形式化语言可以理解的形式，从而能够通过数学化的推演方式对ARMv8处理器中的模块进行安全性验证。通过对ARMv8处理器中全加器和寄存器模块的形式化处理，验证了处理器的功能性安全特性和存储性安全特性。在针对处理器的安全性验证研究方面进行了积极的探索。