形式验证结果中出现“已证明”，还需要理解这项性质是否真正涉及目标行为。Siemens保存的Joe Hupcey III文章，在2017年12月6日讨论一种称为vacuous proof的空真证明。作者的总结是，这类结果没有提供原本想验证的待测设计行为信息；文章随后用性质、约束与设计之间的不同关系解释其来源。[1]
第一种来源在性质自身。作者把前件解释为性质中定义条件的一侧：如果它写成内部不一致、永远无法成立的状态，就会出现self-vacuous，也就是自身空真。原文举的逻辑冲突是，把同一个信号与它的补同时要求成立。用普通语言说，就是要求同一个条件既为真又不为真。这个例子用于说明矛盾，不涉及本文实际编写或运行任何验证代码。[1]
这种冲突在文字上显得直白，作者却另给了它可能被遮住的背景：信号经过较多组合逻辑，或者跨越IP边界及层级时改变名称，人便可能失去对同一关系的追踪。因此，性质看似列了不同名称，也未必已经表达彼此独立的条件。文章说的困难在于逻辑关系被多层表达遮住，并没有说只要信号改名就一定产生空真。[1]
第二种来源改变了问题的位置。性质的前件未必自身矛盾，外部约束却可能把输入限制到它永远不能为真的范围。作者将这类情况称为相对于约束的空真。它与第一种的差异在于，阻止前件出现的关系来自所加入的输入条件，而不是仅从前件自己的文字就能读出的冲突。只把两者都称为“条件写错”，会失去这个明确区分。[1]
第三种来源涉及性质与设计实际支持的行为。作者说明，性质描述的行为若不被设计支持，或者规格与待测设计配置不相匹配，也可能产生空真；总结段称之为相对于设计的空真。此时需要理解的是所谈行为属于哪个设计或配置，而非把所有问题归到输入约束。本文保留作者这项关系，没有把文中的假想交通灯例扩大成真实地区规则，也没有据此给任何芯片作配置判断。[1]
作者用一个假想交通灯控制器，把规格与设计的错配展开。假设规格要求红灯转绿灯、绿灯转黄灯、黄灯转红灯，再按这一顺序循环；于是，所写性质针对这组行为。可是，同事实际送来的待测设计代码，描述的是红灯之后先短暂显示黄灯，再转到绿灯的另一类控制器。两份描述在红灯之后的状态次序就有差别。文章在这个设想中写到工具报告空真，并把问题归为规格或待测设计配置的错误，而非约束性质本身的问题。例子交代了两个容易被一句“交通灯控制器”遮住的对象：准备验证的规格，以及实际送来接受验证的设计。它们名称相近，所描述的状态顺序却没有对应；这里采用的只是作者假设，不把它指认为任何地区的实际交通制度。[1]
从逻辑上理解空真，还应把一个条件关系的证明与条件确实出现分开。前件根本无法成立时，证明标签本身没有补出目标情形发生的证据，这正是作者认为结果会产生误导的要点。对设计说明或评审资料而言，保留是哪一类空真，比把标签直接扩写成设计全部正确更准确；它也没有自行交付实物芯片或功能安全的结论。[1]
本文采用原文三种成因和总结的连续文字，不转写修复代码、删除约束或重跑调试步骤。页面题首及发布时间字段支持2017年12月6日，另有2026年的更新字段，后者不作为首次发表日期。[1]
资料：[1] https://blogs.sw.siemens.com/verificationhorizons/2017/12/06/formal-tech-tip-what-are-vacuous-proofs-why-they-are-bad-and-how-to-fix-them/
信息来源
本文基于上述公开资料整理，未使用来源页面的图片、视频或嵌入媒体。