基于System Verilog Assertions的全局Cache的形式化验证

摘要

随着半导体工艺的进步,片上存储器的设计容量和复杂度日益增加,传统的功能验证方法面临着验证正确性、效率、完备性等方面挑战.采用基于System Verilog Assertions的方法对全局Cache进行形式化验证.利用形式化验证工具Incisive Formal Verifier自动产生符合约束的激励后,对测试表达式进行实时监控、检测,并在断言违反处报错、给出反例波形.通过形式化验证和传统验证的对比实验,得到在模块级层次上形式化验证的模拟效率总体高于传统验证的结论.