用于使用下界距离来执行抽象-精化的方法和装置

摘要

本发明的实施方式提供用于验证电路的功能的方法和装置。系统可以确定下界距离(LBD)值，从而LBD值与CUV的不满足性质的LBD抽象模型关联。系统可以使用抽象-精化技术以确定CUV是否满足性质。系统可以为抽象-精化技术中所用抽象模型确定上界距离值并且可以确定LBD值是否大于或者等于上界距离值。如果是这样，则系统可以推断抽象模型不满足性质，因此系统可以判决不对抽象-精化技术中当前所用抽象模型执行可达性分析。

主权项

一种用于为电路设计验证性质的方法，其中使用状态变量集合来限定所述性质，其中各状态变量与所述电路设计中的顺序要素相关联，其中在两个顺序要素之间的路径的长度部分地基于所述路径中的顺序要素的数量，并且其中在两个状态变量之间的距离等于在与所述两个状态变量相关联的两个顺序要素之间的最短路径的长度，所述方法包括：使用所述电路设计的第一抽象模型来为所述性质确定第一反例，其中所述第一抽象模型至少包括与所述状态变量集合中的状态变量的距离小于或者等于下界距离的所有状态变量；并且使用抽象-精化技术来验证所述性质，所述抽象-精化技术包括：为所述电路设计的第二抽象模型确定上界距离，其中所述上界距离等于距离集合中的最大距离，并且其中所述距离集合包括在所述状态变量集合中的第一状态变量与所述第二抽象模型中的第二状态变量之间的距离；并且响应于确定所述下界距离大于或者等于所述上界距离，为所述性质确定第二反例而不对所述第二抽象模型执行可达性分析。