Efficient modeling of embedded memories in bounded memory checking
A computer-implemented method for augmenting SAT-based BMC to handle embedded memory designs without explicitly modeling memory bits. As is known, verifying designs having large embedded memories is typically handled by abstracting out (over-approximating) the memories. Such abstraction is not useful for finding real bugs. SAT-based BMC, as of now, is incapable of handling designs with explicit memory modeling due to enormously increased search space complexity. Advantageously, our method does not require analyzing the designs and also guarantees not to generate false negatives.
1. A computer implemented method of modeling an electronic design having one or more embedded memories, such that some or all of the memory bits comprising the one or more embedded memories need not be explicitly modeled, the method comprising the steps of:
removing, one or more of the memories from the design while retaining data forwarding semantics of a memory read operation;
capturing, the data forwarding semantics and memory preservation constraints for preserving an arbitrary initial memory state as Efficient Memory Modeling (EMM) constraints in a suitable representation wherein said EMM is a memory modeling technique where memory semantics is maintained without using an explicit register array model and said EMM constraints do not create structure where intermediate variables do not fan-out and do not create unnecessary 2-literal clauses; and
verifying, the design using a suitable bounded analysis; and
generating an output indicative of the verification
wherein according to the data forwarding semantics, a memory read operation from a memory address returns a data value that was last written at that same memory address in a previous memory write operation or, if there is no previous write operation at that address then the memory read operation returns the initial data value.
2. The method according to claim 1 further comprising the step(s) of:
adding exclusivity constraints to the suitable representation such that when a valid matching read and write combination is determined, other read and write combinations are immediately implied invalid as a result of the exclusivity constraints;
wherein said exclusivity constraints refer to those constraints that capture matching read and write operations for a memory address, explicitly.
3. The method according to claim 1 , wherein the capturing step uses proof-based abstractions (PBA) in addition to EMM.
4. The method according to claim 3 , further comprising the step(s) of:
automatically determining, through the use of PBA irrelevant memories and irrelevant ports, such that the corresponding EMM constraints are removed during verification.
5. The method according to claim 4 , further comprising the step(s) of:
removing, during the verification step, any corresponding EMM constraints.
6. The method according to claim 1 , wherein the suitable representation is a hybrid representation that includes both a circuit formulation and a clausal formulation.
7. The method according to claim 1 wherein the verifying step includes a SAT-based bounded analysis.
8. The method according to claim 2 wherein the verifying step includes a SAT-based bounded analysis.
9. The method according to claim 1 wherein the verifying step includes a proof by induction.
10. The method according to claim 2 wherein the verifying step includes a proof by induction.
11. The method according to claim 1 wherein the verifying step includes a SAT-based induction.
12. The method according to claim 2 wherein the verifying step includes a SAT-based induction.
13. The method according to claim 1 wherein the verifying step includes an equivalence checking.
14. The method according to claim 2 wherein the verifying step includes an equivalence checking.
15. A computer implemented method of modeling an electronic design having one or more embedded memories, wherein the modeling is performed such that some or all of the memory bits comprising the one or more embedded memories need not be explicitly modeled, the modeling method comprising the steps of:
removing, one or more of the memories from the design while retaining data forwarding semantics of a memory read operation;
capturing, the data forwarding semantics as Efficient Memory Modeling (EMM) constraints in a suitable representation wherein said EMM is a memory modeling technique where memory semantics is maintained without using an explicit register array model and said EMM constraints do not create structure where intermediate variables do not fan-out and do not create unnecessary 2-literal clauses;
adding exclusivity constraints to the representation; and
verifying, the design using a suitable bounded analysis such that when a valid matching read and write combination is determined, other combinations are immediately implied invalid as a result of the exclusivity constraints; and
generating an output indicative of the verification
wherein according to the data forwarding semantics, a memory read operation from a memory address returns a data value that was last written at that same memory address in a previous memory write operation or, if there is no previous write operation at that address then the memory read operation returns the initial data value.
16. The method according to claim 15 further comprising the step(s) of:
utilizing, proof-based abstractions (PBA) in addition to EMM during the capturing step.
17. The method according to claim 16 further comprising the step(s) of:
automatically determining, through the use of PBA, irrelevant memories and irrelevant ports, such the corresponding EMM constraints are removed during verification.
18. The method according to claim 17 , further comprising the step(s) of:
removing, during the verification step, any corresponding EMM constraints.
19. The method according to claim 15 , wherein the suitable representation is a hybrid representation that includes both a circuit formulation and a clausal formulation.
20. The method according to claim 18 , wherein the suitable representation is a hybrid representation that includes both a circuit formulation and a clausal formulation.
21. The method according to claim 15 wherein the verifying step includes a SAT-based bounded analysis.
22. The method according to claim 18 wherein the verifying step includes a SAT-based bounded analysis.