Automatic symbolic indexing methods for formal verification on a symbolic lattice domain
View Patent ↗Processes for formal verification of circuits and other finite-state systems are disclosed. For one embodiment, a process is disclosed to provide for significantly reduced computation through automated symbolic indexing of a property assertion and to compute the satisfiability of the property assertion directly from a symbolic simulation of the indexed property assertion. For an alternative embodiment a process using indexed property assertions on a symbolic lattice domain to represent and verify properties, provides an efficient symbolic manipulation technique using binary decision diagrams (BDDs). Methods for computing symbolic simulations, and verifying satisfiability may be applicable with respect to property assertions that are symbolically indexed under specific disclosed conditions. A process is also disclosed to compute a constraint abstraction for a property assertion, thereby permitting automated formal verification of symbolically indexed properties under constraints and under specific conditions, which may be automatically checked.
1. A computer software product including one or more recordable media having executable instructions stored thereon which, when executed by a processing device, causes the processing device to:
access a symbolic indexing relation including a first set of target variables and a second set of index variables; and
apply the symbolic indexing relation to an assertion including an antecedent and a consequent to generate an indexed assertion.
2. The computer software product of claim 1 wherein applying the symbolic indexing relation comprises causing the processing device to:
compute a preimage of the consequent with respect to the symbolic indexing relation.
3. The computer software product of claim 2 which, when executed by the processing device, further causes the processing device to:
verify the indexed assertion having as an indexed consequent the preimage of the consequent with respect to the symbolic indexing relation.
4. The computer software product of claim 1 wherein applying the symbolic indexing relation comprises causing the processing device to:
compute a strong preimage of the antecedent with respect to the symbolic indexing relation.
5. The computer software product of claim 4 wherein computing a strong preimage of the antecedent comprises causing the processing device to:
compute a preimage of the antecedent with respect to the symbolic indexing relation; and
compute a preimage of the complement of the antecedent with respect to the symbolic indexing relation.
6. The computer software product of claim 5 wherein computing a strong preimage of the antecedent further comprises causing the processing device to:
compute a relative complement of the preimage of the antecedent and the preimage of the complement of the antecedent.
7. The computer software product of claim 5 wherein computing a strong preimage of the antecedent further comprises causing the processing device to:
compute a first intersection of the preimage of the antecedent and the preimage of the complement of the antecedent; and
compute a relative complement of the preimage of the antecedent and the first intersection.
8. The computer software product of claim 4 wherein applying the symbolic indexing relation further comprises causing the processing device to:
compute a symbolic simulation using the strong preimage of the antecedent as an indexed antecedent of the indexed assertion.
9. The computer software product of claim 4 wherein applying the symbolic indexing relation further comprises causing the processing device to:
apply the strong preimage of the antecedent to a model to generate an indexed model.
compute a symbolic simulation using the indexed model.
10. A method comprising:
specifying a symbolic indexing relation including a first set of index variables and a second set of target variables; and
applying the indexing relation to an assertion including an antecedent and a consequent to generate an indexed assertion.
11. The method of claim 10 wherein applying the indexing relation to the assertion comprises:
performing a first preimage calculation on the consequent to generate an indexed consequent comprising the first preimage.
12. The method of claim 11 wherein applying the indexing relation to the assertion further comprises:
performing a strong preimage calculation on the antecedent to generate an indexed antecedent comprising the strong preimage.
13. The method of claim 12 wherein performing a strong preimage calculation on the antecedent comprises:
performing a second preimage calculation on the antecedent to generate a second preimage;
performing a third preimage calculation on a complement of the antecedent to generate a complement preimage;
intersecting the second preimage and the complement preimage to identify an intersection; and
computing a difference between the second preimage and the intersection to generate the strong preimage.
14. The method of claim 12 wherein performing a strong preimage calculation on the antecedent comprises:
performing a second preimage calculation on the antecedent to generate a second preimage;
performing a third preimage calculation on a complement of the antecedent to generate a complement preimage; and
computing a relative complement between the second preimage and the complement preimage to generate the strong preimage.
15. The method of claim 12 further comprising:
using the first preimage and the strong preimage to verify that the property assertion is satisfied.
16. A verification system comprising:
means for specifying a symbolic indexing relation including a first set of index variables and a second set of target variables; and
means for applying the indexing relation to an assertion including an antecedent and a consequent to generate an indexed assertion.
17. The verification system of claim 16 wherein the means for applying the indexing relation to an assertion comprises:
means for automatically indexing the antecedent to generate an indexed antecedent; and
means for automatically indexing the consequent to generate an indexed consequent.
18. The verification system of claim 16 further comprising:
means for automatically checking a first condition to determine whether the symbolic indexing relation indexes the set of target variables.
19. The verification system of claim 18 further comprising:
means for automatically checking a second condition to determine whether a model that satisfies an assertion including the indexed antecedent and the consequent also satisfies the assertion including the antecedent and the consequent.
20. The verification system of claim 19 further comprising:
means for automatically checking a third condition to determine whether the model that satisfies the indexed assertion including the indexed antecedent and the indexed consequent also satisfies the assertion including the indexed antecedent and the consequent.
21. A method comprising:
receiving a symbolic indexing relation including a first set of index variables and a second set of target variables; and
applying the indexing relation to an assertion including an antecedent and a consequent to generate an indexed assertion.
22. The method of claim 21 wherein applying the indexing relation to an assertion comprises:
computing a strong preimage of the antecedent to generate an indexed antecedent; and
computing a preimage of the consequent to generate an indexed consequent.
23. The method of claim 22 further comprising:
checking a first condition to determine whether the symbolic indexing relation indexes the set of target variables.
24. The method of claim 23 further comprising:
checking a second condition to determine whether a model that satisfies an assertion including the indexed antecedent and the consequent also satisfies the assertion including the antecedent and the consequent.
25. The method of claim 24 further comprising:
checking a third condition to determine whether the model that satisfies the indexed assertion including the indexed antecedent and the indexed consequent also satisfies the assertion including the indexed antecedent and the consequent.
26. An article of manufacture including one or more recordable media having data stored thereon which, when accessed by a processing device, causes the processing device to perform the method of claim 25 .
27. An article of manufacture including one or more recordable media having data stored thereon which, when accessed by a processing device, causes the processing device to perform the method of claim 23 .
28. An article of manufacture including one or more recordable media having data stored thereon which, when accessed by a processing device, causes the processing device to perform the method of claim 22 .
29. A method comprising:
performing a first preimage calculation on an antecedent of an assertion to generate a first preimage;
performing a second preimage calculation on a complement of the antecedent to generate a second preimage; and
intersecting the first preimage and a complement of the second preimage to generate an indexed antecedent.
30. The method of claim 29 further comprising:
checking an indexing relation to determine whether it indexes each variable of the assertion.
31. A method comprising:
performing a first preimage calculation on an antecedent of an assertion to generate a first preimage;
performing a second preimage calculation on a complement of the antecedent to generate a second preimage; and
computing a relative complement between the first preimage and the second preimage to generate a strong preimage.
32. The method of claim 31 further comprising:
performing a third preimage calculation on a consequent of the assertion to generate a third preimage;
checking an indexing relation to determine whether it indexes each variable of the assertion; and
using the third preimage and the strong preimage to verify that the assertion is satisfied.