买专利卖专利找龙图腾，真高效！ 查专利查商标用IPTOP,全免费！专利年费监控用IP管家,真方便！

龙图腾网获悉深圳国微芯科技有限公司申请的专利动态的集成电路对应的子句的管理方法、形式验证方法获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN120805820B 。

龙图腾网通过国家知识产权局官网在2026-01-06发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202511301478.2，技术领域涉及：G06F30/39；该发明授权动态的集成电路对应的子句的管理方法、形式验证方法是由刘美华;冷文达;苏宇;杨成涛设计研发完成，并于2025-09-12向国家知识产权局提交的专利申请。

本动态的集成电路对应的子句的管理方法、形式验证方法在说明书摘要公布了：本发明公开了动态的集成电路对应的子句的管理方法、形式验证方法。其中动态的集成电路对应的子句的管理方法，包括：步骤1，将集成电路设计的待验证属性转化为SMT问题进行求解；步骤2，将学习子句集合中的学习子句根据学习子句的LBD值大小分为多个区间；步骤3，对于没有评估值的各学习子句，根据其LBD值计算评估值；步骤4，将LBD值最大的区间以外的区间之间的学习子句根据评估值进行挪动；将LBD值最大的区间中评估值较大的一部分学习子句进行删除；步骤5，在对子句进行冲突分析时，更新该学习子句的评估值，并将冲突分析得到的学习子句加入学习子句集中，返回步骤2。本发明能够有效保留高质量学习子句，并将低质量的学习子句进行及时删除。

本发明授权动态的集成电路对应的子句的管理方法、形式验证方法在权利要求书中公布了：1.一种动态的集成电路对应的子句的管理方法，其特征在于，包括： 步骤1，将集成电路设计的待验证属性转化为满足性模理论问题，利用满足性模理论求解器进行求解； 步骤2，获取当前的学习子句集合，将学习子句集合中的学习子句根据学习子句的LBD值大小分为多个区间； 步骤3，针对于没有评估值的各学习子句，根据其LBD值计算评估值；根据评估值的大小对各区间内的学习子句进行排序； 步骤4，将LBD值最小以及最大的区间以外的其他区间进行以下处理：将当前处理的区间内评估值较大的一部分学习子句挪至比当前处理的区间的LBD值大的后一个相邻区间，将评估值较小的一部分学习子句挪至比当前处理的区间的LBD值小的前一个相邻区间； 将LBD值最小的区间中评估值较大的一部分学习子句挪至比该区间的LBD值大的后一个相邻区间； 将LBD值最大的区间中评估值较大的一部分学习子句进行删除； 步骤5，在对子句进行冲突分析时，判断当前子句是否为学习子句，若是，则根据学习子句的LBD值以及产生该学习子句时的冲突数量以及在冲突分析时用到的冲突数量，来更新该学习子句的评估值，并将冲突分析得到的学习子句加入学习子句集中，返回步骤2； 根据学习子句的LBD值以及产生该学习子句时的冲突数量以及在冲突分析时用到的冲突数量，来更新该学习子句的评估值具体采用公式Ei+1=A*P+1-A*E进行更新，A为衰减因子，P=Pi-1+1S2–S1，S1为产生该学习子句时的冲突数量，S2为冲突分析时用到的冲突数量，并在得到P值后，使用S2的值替换S1的值，当S1=S2时，P=1。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人深圳国微芯科技有限公司，其通讯地址为：518000 广东省深圳市前海深港合作区前湾一路1号A栋201室(入住深圳市前海商务秘书有限公司)；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。

以上内容由龙图腾AI智能生成。