基于外部引入逻辑电路的形式验证断言空泛性的纠正方法、存储介质和终端

摘要

本发明涉及基于外部引入逻辑电路的形式验证断言空泛性的纠正方法、存储介质和终端，方法包括如下步骤：将断言的每一子表达式分别置为0和1后进行综合并做自动机最小化处理，得到的两个结果若相同则认为断言具有空泛性。本发明基于最广泛的空泛性定义，增加了测试的完整性；同时由于所使用的综合过程和最小化的可确定性，两个结果只需要进行结构对比，效率很高。