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

龙图腾网获悉中国科学院软件研究所申请的专利基于控制流与数据流信息的Chisel限界模型检测加速方法及系统获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN119720883B 。

龙图腾网通过国家知识产权局官网在2025-07-01发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202411799932.7，技术领域涉及：G06F30/33；该发明授权基于控制流与数据流信息的Chisel限界模型检测加速方法及系统是由董一凡;刘易铖;申世东;宋富;吴志林设计研发完成，并于2024-12-09向国家知识产权局提交的专利申请。

本基于控制流与数据流信息的Chisel限界模型检测加速方法及系统在说明书摘要公布了：本发明公开一种基于控制流与数据流信息的Chisel限界模型检测加速方法及系统，属于硬件设计的形式化验证领域。所述方法包括：编译待验证程序，得到编译过程中的FIRRTL中间表示和待验证程序的FIRRTL抽象语法树；根据所述FIRRTL抽象语法树，获取待验证程序的分支结构信息；结合所述FIRRTL抽象语法树，对待验证程序进行基于断言的切片，并保留和断言相关的FIRRTL中间表示；基于和断言相关的FIRRTL中间表示生成迁移系统S；基于所述迁移系统S和所述分支结构信息进行所述待验证程序的检测。本发明通过利用程序中的控制流和数据流信息，可以加速Chisel生成的硬件设计的BMC验证过程。

本发明授权基于控制流与数据流信息的Chisel限界模型检测加速方法及系统在权利要求书中公布了：1.一种基于控制流与数据流信息的Chisel限界模型检测加速方法，其特征在于，所述方法包括： 编译待验证程序，得到编译过程中的FIRRTL中间表示和待验证程序的FIRRTL抽象语法树； 根据所述FIRRTL抽象语法树，获取待验证程序的分支结构信息；其中，所述分支结构信息包括：分支条件间的顺序或分支条件图的边信息，所述根据所述FIRRTL抽象语法树，获取待验证程序的分支结构信息，包括： 识别FIRRTL抽象语法树中的分支结构，并以分支条件为节点，分支嵌套关系为边，建立分支结构图； 对分支结构图做拓扑排序，获取分支条件间的顺序； 依据所述分支条件间的顺序为分支条件进行编号，并通过FIRRTL内置数据结构annotation来存储； 或， 识别FIRRTL抽象语法树中的分支结构，并以分支条件为节点，分支嵌套关系为边，建立分支结构图， 将分支结构图中的边信息存储在FIRRTL内置数据结构annotation中；其中，分支结构图的每一条边对应所述FIRRTL内置数据结构annotation中的一条annotation； 结合所述FIRRTL抽象语法树，对待验证程序进行基于断言的切片，并保留和断言相关的FIRRTL中间表示；其中，所述断言基于Chisel程序来获取，所述结合所述FIRRTL抽象语法树，对待验证程序进行基于断言的切片，并保留和断言相关的FIRRTL中间表示，包括： 遍历FIRRTL抽象语法树，建立数据流图； 在所述数据流图上进行图可达性分析，并基于分析结果，得到断言内的信号及该信号依赖节点的集合；其中，所述信号包括：端口和寄存器； 对于任一FIRRTL中间表示，若该FIRRTL中间表示引用的信号均不在断言内信号及该信号依赖节点的集合内，则不保留该FIRRTL中间表示； 基于和断言相关的FIRRTL中间表示生成迁移系统S； 基于所述迁移系统S和所述分支结构信息进行所述待验证程序的检测。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人中国科学院软件研究所，其通讯地址为：100190 北京市海淀区中关村南四街4号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。