Page 288 - 《软件学报》2026年第3期

徐雄 等: 嵌入式软件 IP 通用模型 1251

足的约束. 因此, IP 不变式类似于面向对象编程中类不变式的概念.

5 软件 IP 的实现

软件 IP 的实现包含两部分: 头文件 (.h) 和源代码文件 (.c). 源代码文件实现了软件 IP 的功能, 而头文件主要
包含了源代码中使用的变量的声明. 这些声明的变量包括如下.
(1) 输入变量: 对应软件 IP 的输入端口, 软件 IP 从输入变量 (端口) 读取数据.
(2) 输出变量: 对应软件 IP 的输出端口, 软件 IP 的计算结果通过输出变量 (端口) 传送出去.
(3) 状态变量: 用于记录在软件 IP 后续执行中会被再次用到的值. 例如, 累加器的软件 IP 中会使用状态变量
来存储上一次的累加结果.
(4) 参数变量: 可以被视为软件 IP 的“出厂配置”. 例如, 上面累加器软件 IP 的参数变量可以是累加值的上限
和下限值. 与以上状态变量不同, 参数变量在软件 IP 的执行过程中应保持不变, 因为更改“出厂配置”通常是不合
理的.
除了声明变量之外, 头文件中还会声明软件 IP 的句柄程序. 该句柄程序相当于该软件 IP 的“主函数”, 其具体
实现包含在源代码文件 (.c) 中. 通过这种方式, 环境可以通过调用该软件 IP 句柄函数来使用其功能, 而无需暴露
其实现细节. 具体而言, 环境可以通过包含 (#include) 该软件 IP 的头文件来使用它. 关于软件 IP 实现的具体形式
及使用方法, 可参见案例文档: https://github.com/BearHeroWithErrow/poweronjudge-ip-instance/blob/main/
PowerOnJudge 的软件 IP 实例.pdf.
6 软件 IP 的一致性

软件 IP 由知识模型 (第 3 节)、形式模型 (第 4 节) 和实现 (第 5 节) 这 3 部分构成, 因此这 3 部分之间应保持
一致性关系. 知识模型通常采用自然语言文本、图表等非形式的方式描述; 形式模型以形式化的方式描述软件 IP
的功能和非功能行为; 实现部分通过代码的方式实现了软件 IP 的功能. 软件 IP 三要素之间的相互转换如图 11
所示.

知识模型

理解 生成 合成 理解

精化
形式模型 实现
抽象
图 11 软件 IP 三要素之间的转换关系

6.1 知识模型与形式模型
知识模型包括软件 IP 功能的自然语言和/或图形描述 (如 Simulink/Stateflow 和 UML 图等), 据此可生成形式
描述作为该软件 IP 的形式模型. 例如, 已有相关研究 [85] 将 (非形式的) AADL 和 Simulink/Stateflow 模型转换为形
式 HCSP 模型 [86] , 之后可使用相应的工具 [87] 对其进行形式验证. 近年随着大型语言模型 (large language model,
LLM) 的普及, 从自然语言描述生成形式描述的研究成果也不断涌现. 例如, 工具 nl2spec [88] 可交互式地将用英文描
述的需求转换为 LTL 公式. 在从知识模型生成形式模型之后, 我们可以借助某些工具检查原始形式模型与生成的
形式模型之间的逻辑等价性, 以此验证一致性.
另一方面, 可以将软件 IP 的形式模型输入到训练好的 LLM 中, 然后得到基于文本的描述作为输出, 即对该形
式模型的自然语言理解. 可以通过检查知识模型中的原始文本与从形式模型中生成的自然语言理解之间的语义等