近年来,随着硬件系统(尤其是超大规模集成电路)规模不断增大,单纯的动态模拟方法已经无法提供足够的覆盖率,以满足系统验证的充分性和完备性要求。因此模型检验等形式化验证方法成为复杂硬件系统验证的重要手段。与定理证明等其他形式化验证方法相比,模型检验的主要优点在于:当断言被违反时,模型检验方法能够给出反例,以解释断言被违反的原因。 然而复杂系统的反例非常难以理解,需要花费大量时间检查大量的变量和事件,才能够找到错误的根源。这就导致模型检验带来的验证效率提升,被浪费在低效的反例理解和错误定位上。因此从反例中提取有用信息,以帮助验证工程师高效地理解反例和定位错误,成为目前的研究热点。另外,许多模型检验算法需要存储和处理反例或证例(witness)。从反例中剔除无关变量,可以使这些算法在空间和时间复杂度上获得指数改进。因此,根据不同应用的要求,对模型检验的反例作进一步处理,具有重要的意义。我们将这些方法统称为反例解释。 不同的应用环境,对反例解释方法有不同的要求,主要反映在完备性、时间开销和结果尺寸方面。当反例解释的结果需要由验证工程师阅读、理解和定位错误时,对完备性和时间开销的要求不高,但要求结果一定要紧凑和精简。我们称之为″非完备的错误定位方法″。另一方面,当反例解释的结果需要由其他算法作进一步处理时(比如抽象精化模型检验方法),对完备性和时间开销的要求非常高,而将结果尺寸放在第二位。我们称之为″完备的反例压缩方法″。 本文对非完备和完备方法都进行了深入研究,完成的主要研究工作和取得的主要研究成果如下: 1.在非完备错误定位方法方面,提出了迭代式证例搜索算法。在对现有最近证例搜索算法进行深入分析时,我们发现:在广度优先的代码检查过程中,多个最近证例和高扇入节点会对错误定位的精度产生巨大影响。为了解决这一问题,我们提出了迭代式证例搜索算法。该算法迭代地搜索最近证例,每次迭代产生一个谓词差异集合,并添加到一个谓词列表的后端。越是位于列表前端的谓词,越有可能是实际的错误。使用该谓词列表作为定位结果,可以避免广度优先搜索导致的精度损失。试验结果证明,本算法与单纯的最近证例搜索算法相比,定位精度有很大提高。 2.针对确定性系统的路径反例(path-like counterexample),提出了基于悖论分析和增量式SAT求解的反例压缩算法,以降低BFL算法的时间开销。BFL是目前压缩效率最高的算法,通常能够剔除70%以上的无关变量。然而,BFL的线性收敛特性导致其时间开销过大。为此我们在BFL中引进了悖论分析方法。该算法通过分析导致悖论的原因,从而能够一次剔除多个无关变量,而不是象BFL那样一次只能剔除一个无关变量。同时我们发现,BFL中的相邻SAT问题非常相似,存在着大量的重叠状态空间。单独的求解这些SAT问题,将导致这些重叠状态空间被反复