首页>
外国专利>
Method and system for design verification using proof-based abstraction
Method and system for design verification using proof-based abstraction
展开▼
机译:使用基于证明的抽象进行设计验证的方法和系统
展开▼
页面导航
摘要
著录项
相似文献
摘要
A design verifier includes a bounded model checker, an abstractor and an unbounded model checker. The bounded model checker verifies a property to a depth K and either finds a counterexample, or generates a proof in the form of a directed acyclic graph. If no counterexample is found, the abstractor generates an abstracted design description using a proof generated by the bounded model checker. The unbounded model checker verifies the property of the abstracted design description. If a counterexample is found, the bounded model checker increases K and verifies the property to the new larger depth. If no counterexample is found, the design is verified.
展开▼