大规模verilog程序层次化抽象验证方法及系统

本发明公开了一种大规模verilog程序层次化抽象验证方法及系统，本发明方法包括为被验证的大规模verilog程序的模块进行分层；针对各层模块采用自下而上的层次化抽象验证，包括从将底层的模块开始遍历直至遍历完顶层的模块，且针对遍历得到的任意第i层模块：若第i层模块为底层的模块则基于精确语义进行功能规范验证；否则基于第i‑1层模块状态迁移关系的抽象语义构造第i层模块的抽象模型，并根据第i层模块的抽象模型完成对第i层模块的功能规范验证。本发明旨在实现适用于大规模verilog程序功能正确性的形式化验证，解决形式化验证方法中大规模verilog程序的状态空间爆炸问题。