专利名称：Abstraction for arrays in integrated circuit
models
发明人：Steven M. German申请号：US13197061申请日：20110803公开号：US08473883B2公开日：20130625
专利附图：
摘要：The illustrative embodiments provide a mechanism for abstraction for arrays inintegrated circuit designs. The mechanism constructs abstract models directly from ananalysis of the system. The abstract models are both sound and complete for safety
properties: a safety property holds in the abstract model if and only if the propertyholds in the original model. The mechanism of the illustrative embodiments eliminatesthe need for iterative abstraction refinement. The mechanism of the illustrativeembodiments can find small models that verify a system in some cases where otherapproaches are unable to find a small model. The approach constructs an abstract designfrom the original design. The abstracted design may have smaller arrays than the originaldesign. The mechanism checks the correctness of the abstracted design by modelchecking.
申请人：Steven M. German
地址：Wayland MD US
国籍：US
代理人：Stephen R. Tkacs,Stephen J. Walder, Jr.,Preston J. Young
更多信息请下载全文后查看
因篇幅问题不能全部显示，请点此查看更多更全内容