-
公开(公告)号：CN118428285B
公开(公告)日：2024-10-22
申请号：CN202410462685.5
申请日：2024-04-17
Applicant: 中国科学院软件研究所
Abstract: 本发明提出了一种Chisel高层电路设计的转换和验证方法及装置，涉及计算机技术领域，通过分析Chisel代码内容，生成内部语法树结构；分析内部语法树上的每个语句和语句块，识别涉及的信号和变量；基于识别的信号、变量和内部语法树结构，对内部语法树进行展开和变换；对经过展开和变换后的内部语法树，按照信号和变量间的依赖关系进行语句排序，生成排序后的内部语法树；根据排序后的内部语法树，通过软件建模模拟Chisel电路设计的行为，生成Scala模拟代码；使用生成的Scala模拟代码进行仿真测试和形式化验证。本发明可以保留Chisel高层电路设计的参数、结构信息，对Chisel电路设计进行更充分的验证。
-
公开(公告)号：CN119109992A
公开(公告)日：2024-12-10
申请号：CN202310673115.6
申请日：2023-06-07
Applicant: 中国科学院软件研究所
Abstract: 本发明公开一种基于模型精化的网络通信协议代码生成方法，涉及代码生成领域，通过构建的模型和网络通信协议库、加密协议库进行代码生成和精化，其中通过通信方法精化技术对网络通信协议中网络节点的进程之间的通信进行精化，通过加解密算法精化技术对通信数据加解密进行精化，提高生成代码的准确率，进而提高开发效率。
-
公开(公告)号：CN117075969B
公开(公告)日：2024-07-23
申请号：CN202311088711.4
申请日：2023-08-28
Applicant: 中国科学院软件研究所
IPC: G06F9/38 , G06F9/30 , G06F12/1009
Abstract: 本发明公开了一种面向RISC‑V处理器特权指令集一致性的形式验证方法及装置，所述方法包括：在Chisel设计的待验证处理器中引出指令信号、通用寄存器信号、访存信号、控制和状态寄存器信号、TLB页表翻译信号到信号同步模块；将指令信号作为特权指令集参考模型执行的指令输入，并将通用寄存器信号、访存信号、控制和状态寄存器信号、TLB页表翻译信号与特权指令集参考模型的执行结果是否一致设为待验证性质；将特权指令集参考模型、待验证处理器、信号同步模块与待验证性质共同转换迁移系统模型；基于迁移系统模型，交由模型检测算法进行求解，得到待验证处理器的验证结果。本发明可以对RISC‑V特权指令集进行一致性验证。
-
公开(公告)号：CN117075969A
公开(公告)日：2023-11-17
申请号：CN202311088711.4
申请日：2023-08-28
Applicant: 中国科学院软件研究所
IPC: G06F9/38 , G06F9/30 , G06F12/1009
Abstract: 本发明公开了一种面向RISC‑V处理器特权指令集一致性的形式验证方法及装置，所述方法包括：在Chisel设计的待验证处理器中引出指令信号、通用寄存器信号、访存信号、控制和状态寄存器信号、TLB页表翻译信号到信号同步模块；将指令信号作为特权指令集参考模型执行的指令输入，并将通用寄存器信号、访存信号、控制和状态寄存器信号、TLB页表翻译信号与特权指令集参考模型的执行结果是否一致设为待验证性质；将特权指令集参考模型、待验证处理器、信号同步模块与待验证性质共同转换迁移系统模型；基于迁移系统模型，交由模型检测算法进行求解，得到待验证处理器的验证结果。本发明可以对RISC‑V特权指令集进行一致性验证。
-
公开(公告)号：CN118550688A
公开(公告)日：2024-08-27
申请号：CN202410507923.X
申请日：2024-04-25
Applicant: 中国科学院软件研究所
IPC: G06F9/50
Abstract: 本申请提供一种智能合约资源消耗计量方法、装置、电子设备以及介质，涉及区块链智能合约领域。本申请提供的智能合约资源消耗计量方法包括：基于外部代码对应的第一资源消耗计量规则，对外部代码的所有第一指令进行指令资源消耗计算，得到第一指令资源消耗总量；基于调用的内存资源消耗映射表和智能合约的内存页对应的第二资源消耗计量规则，对智能合约的内存页进行内存资源消耗计算，得到内存资源消耗总量；基于第一指令资源消耗总量、内存资源消耗总量至少一种以及预设总资源消耗量上限值确定智能合约的执行状态。本申请能够计算智能合约的外部代码的资源消耗量，更准确的得到智能合约的资源消耗计量结果，并节省计算机存储资源。
-
Patent Agency Ranking
公开(公告)号：CN118428285A
公开(公告)日：2024-08-02
申请号：CN202410462685.5
申请日：2024-04-17
Applicant: 中国科学院软件研究所
Abstract: 本发明提出了一种Chisel高层电路设计的转换和验证方法及装置，涉及计算机技术领域，通过分析Chisel代码内容，生成内部语法树结构；分析内部语法树上的每个语句和语句块，识别涉及的信号和变量；基于识别的信号、变量和内部语法树结构，对内部语法树进行展开和变换；对经过展开和变换后的内部语法树，按照信号和变量间的依赖关系进行语句排序，生成排序后的内部语法树；根据排序后的内部语法树，通过软件建模模拟Chisel电路设计的行为，生成Scala模拟代码；使用生成的Scala模拟代码进行仿真测试和形式化验证。本发明可以保留Chisel高层电路设计的参数、结构信息，对Chisel电路设计进行更充分的验证。
-
公开(公告)号：CN116149671A
公开(公告)日：2023-05-23
申请号：CN202310437229.0
申请日：2023-04-23
Applicant: 中国科学院软件研究所
Abstract: 本申请提出一种用于翻译智能合约语言的方法和装置、电子设备、计算机可读存储介质，所述方法包括响应于加载的所述智能合约语言编写的源代码，生成规范化的抽象语法树；根据所述智能合约语言的类型定义，对所述抽象语法树中的复合数据类型表达式节点进行翻译；根据所述智能合约语言的函数定义，对所述抽象语法树中的函数节点进行翻译；根据可信编译工具的源语言规范，对所述抽象语法树中的其他节点进行翻译，其中，所述其他节点包括所述抽象语法树中除去复合数据类型表达式节点和函数节点外的节点。根据本申请的实施例，实现了对支持复合数据类型和多返回值函数的智能合约语言所编写的程序的翻译，以及对复合数据类型和函数翻译过程的形式化验证。
-
公开(公告)号：CN116701085B
公开(公告)日：2024-03-19
申请号：CN202310648072.6
申请日：2023-06-02
Applicant: 中国科学院软件研究所
Abstract: 本发明提供一种RISC‑V处理器Chisel设计指令集一致性的形式验证方法及装置，所述方法包括：在待验证处理器中引出该待验证处理器的输入信号和第一执行结果；将输入信号传递给指令集参考模型，以得到第二执行结果；将第一执行结果与第二执行结果一致作为待验证性质，并生成指令的验证范围约束；将包含参考模型、待验证性质和验证范围约束的待验证处理器转换为FIRRTL中间表示，并依据FIRRTL中间表示，得到迁移系统；基于迁移系统及其包含的性质和约束，得到待验证处理器的验证结果。本发明通过一个模块化、与原文对应、可参数化配置的参考模型描述RISC‑V指令集规范的行为，减轻了验证人员对形式化验证知识的需求，无需人工编写待验证的性质。
-
公开(公告)号：CN116701085A
公开(公告)日：2023-09-05
申请号：CN202310648072.6
申请日：2023-06-02
Applicant: 中国科学院软件研究所
Abstract: 本发明提供一种RISC‑V处理器Chisel设计指令集一致性的形式验证方法及装置，所述方法包括：在待验证处理器中引出该待验证处理器的输入信号和第一执行结果；将输入信号传递给指令集参考模型，以得到第二执行结果；将第一执行结果与第二执行结果一致作为待验证性质，并生成指令的验证范围约束；将包含参考模型、待验证性质和验证范围约束的待验证处理器转换为FIRRTL中间表示，并依据FIRRTL中间表示，得到迁移系统；基于迁移系统及其包含的性质和约束，得到待验证处理器的验证结果。本发明通过一个模块化、与原文对应、可参数化配置的参考模型描述RISC‑V指令集规范的行为，减轻了验证人员对形式化验证知识的需求，无需人工编写待验证的性质。
-
公开(公告)号：CN115496017A
公开(公告)日：2022-12-20
申请号：CN202211084241.X
申请日：2022-09-06
Applicant: 中国科学院软件研究所
IPC: G06F30/33 , G06F8/41 , G06F119/02
Abstract: 本发明公开了一种Chisel断言语言的类SVA扩展及形式化验证方法，其步骤包括：1)将SVA支持的若干算子引入Chisel断言语言中，得到断言语言中对应的扩展算子；2)接收用户编写的算子序列；3)将Chisel硬件设计代码编译成FIRRTL，并利用FIRRTL生成设计代码的迁移系统；4)在FIRRTL层次生成相应的Büchi自动机；5)将结构调整后的自动机翻译到FIRRTL的迁移系统上，得到断言转换后的迁移系统；6)将转换后的迁移系统与硬件设计对应的迁移系统做同步得到一全局迁移系统；7)根据全局迁移系统生成btor2文件；8)对btor2文件进行模型检测，完成对断言所描述性质的形式化验证。
-
-
-
-
-
-
-
-
-
Search Results
13
records
(took 0.029 seconds)
