首页>
外国专利>
Formal verification using cached search path information to verify previously proved/disproved properties
Formal verification using cached search path information to verify previously proved/disproved properties
展开▼
机译:使用缓存的搜索路径信息进行正式验证,以验证先前证明/拒绝的属性
展开▼
页面导航
摘要
著录项
相似文献
摘要
A formal verification tool that verifies multiple sequentially-generated versions of a core circuit design by obtaining search path information from the formal verification solver for each property that is proven or disproven during a first formal verification session involving an earlier-generated circuit design version, and utilizing the search path information to perform search-path verification processes during a subsequent formal verification session to quickly verify the proven/disproven properties in a later-generated circuit design version. Each property's search path information includes counterexample traces or proof artifacts identifying the search operations utilized to achieve a corresponding counterexample or proof object that proves/disproves the property. Search-path verification involves applying the stored search path information to the later-generated circuit design version, and determining if the same counterexample or proof object is achieved. The stored search path information is also utilized to perform efficient path-influenced search processes when the search-path verification process fails.
展开▼