一种形式验证方法、装置、形式验证平台及可读存储介质

摘要

本发明公开了一种形式验证方法、装置、形式验证平台及可读存储介质，该形式验证方法包括如下步骤：获取输入待测模型的待验证源操作数；判断待验证源操作数是否属于必要验证源操作数；如果待验证源操作数不属于必要验证源操作数，则确定将待验证源操作数作为输入时，待测模型与参考模型的输出结果相等；如果待验证源操作数属于必要验证源操作数，则启动形式验证工具，将验证待验证源操作数作为输入，根据待测模型的输出结果与参考模型的输出结果进行验证。通过在启用形式验证工具验证待测模型和参考模型的输出结果是否相等之前，判断待验证源操作数是否属于待测模型的必须要验证源操作数，降低了形式验证方法出现空间爆炸问题的风险。