Enhanced case-splitting based property checking

摘要

An approach is provided in which a model verification system partitions one of a design specification's circuit design properties into multiple unsolved cases. The model verification system then performs property checking on one of the unsolved cases against a corresponding circuit design model, which results in a property checked solved case and a subset of unsolved cases. In turn, the model verification system performs sequential equivalence checking on one or more of the subset of unsolved cases by checking their sequential equivalence against the property checked solved case. As a result, the model verification system stores the cases as sequentially equivalent solved cases and verifies of a portion of the design specification against a portion of the circuit design model.

主权项

1. A method comprising:
partitioning a circuit design property into a plurality of unsolved cases, the circuit design property corresponding to a design specification; property checking, by one or more processors, a selected one of the plurality of unsolved cases against a circuit design model corresponding to the design specification, the property checking resulting in a property checked solved case and a subset of the plurality of unsolved cases; logging a property checked time that indicates an amount of time taken to perform the property checking of the selected unsolved case; and sequential equivalence checking, by at least one of the one or more processors, one or more of the subset of the plurality of unsolved cases against the property checked solved case, resulting in one or more sequentially equivalent solved cases and verification of a portion of the design specification against a portion of the circuit design model.