Efficient modeling of embedded memories in bounded memory checking
AssigneeNEC Laboratories America, Inc.
InventorsMalay Ganai, Aarti Gupta, Pranav Ashar
Life of this patent
Estimating the term…
Abstract
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.
Claims22
A 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;
- 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;
- and
- verifying, the design using a suitable bounded analysis.
A 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;
- capturing, the data forwarding semantics as Efficient Memory Modeling (EMM) constraints in a suitable representation;
- 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.
Dependencies are inferred from the claim text.