使用可达性过度逼近进行验证的方法和系统

摘要

本发明公开了一种用于验证设计符合所需特性的方法、系统和计算机程序产品。该方法包括接收设计、所述设计的第一初始状态以及与所述设计相关的要验证的特性。扩展所述设计的第一初始状态以创建所述第一初始状态的超集，该超集包含从所述设计的所述第一初始状态可达的一个或多个状态。合成超集以定义所述设计的第二初始状态。通过将切割点插入到所述超集来过度逼近针对所述设计的所述超集的应用，以获得修改的超集，然后参考所述修改的超集验证所述特性。

主权项

1. 一种验证电路设计符合所需特性的方法，所述方法包括：接收电路设计、所述电路设计的第一初始状态以及与所述电路设计相关的要验证的特性，其中所述第一初始状态被表示为包括多个节点的二进制决策图；扩展所述电路设计的所述第一初始状态以创建所述第一初始状态的超集，该超集包含从所述电路设计的所述第一初始状态可达的一个或多个状态；合成所述超集以定义所述电路设计的第二初始状态，其中所述第二初始状态通过以下操作被合成为连线表：在参数变量上使用多路复用器表示以允许不同路线通过所述二进制决策图中的所述多个节点，以及将初始值映射更新到在所述连线表中表示的适当的合成门；通过将切割点插入到所述超集，来过度逼近针对所述电路设计的所述超集和所述第二初始状态的应用，以获得修改的超集，其中所述切割点插入用随机门来取代所述连线表中的门；以及通过将所述特性与所述修改的超集进行比较来验证所述特性。