Efficient modeling of embedded memories in bounded memory checking
US7386818B2 · kind B2 · utility
9Cited by
0References
22Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Jan 18, 2005 |
| Grant date | Jun 10, 2008 |
| Priority date | — |
| Expiry date | Jun 11, 2025 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG11C2029/0401
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
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.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.