全数字实时仿真平台
SkyEye，中文全称天目全数字实时仿真软件，应用软件仿真技术，逼真地模拟出被测软件的物理环境。用图形化方式构建虚拟目标系统，有效降低了硬件工程师和软件工程师之间的沟通成本，软件工程师可以不依赖硬件工程师，根据需求对虚拟硬件的配置进行改动，并可以在虚拟硬件模型上运行与真实硬件相同的二进制文件，可以大大缩短产品研发周期，提高软件测试效率。完全自主可控的支持数十种国产芯片仿真的全数字实时仿真平台SkyEye
SkyEye功能
- 更灵活快速的虚拟目标系统搭建–通过可视化图形界面拖拽虚拟硬件组件快速搭建
- 仿真状态可控性、确定性和重复性–在虚拟系统上运行的二进制文件与实际目标上运行的二进制文件相同，仿真过程可以通过运行、暂停控制、可以随时重复执行，每次运行结果是确定的，可以使用软件复现问题
- 提供GDB源码调试和汇编级调试工具，使开发者更高效的分析和定位问题
- 提供代码覆盖率和生成报告功能，进行源码和目标码的覆盖率分析
- 提供故障注入功能，可以进行内存和IO的故障注入进行测试
- 提供协同仿真工具，支持与其他异构模型协同仿真
- 提供外设建模工具和二次开发API接口，方便用户进行二次开发
- 提供Python API接口，可以进行自动化测试脚本构建所需测试环境
- 界面提供自动化测试功能，可以选择所需测试用例自动运行并给出测试结果
同步数据流语义
在从Lustre到C的转换过程中, 经历了同步数据流语义逐步向串行命令式语义的过渡.在现阶段, Vélus的动态语义的形式化定义是从SN-Lustre中间表示开始的, 在Obc, 中间表示被变换至一种基于对象的串行命令式语义; 相应地, L2C的动态语义形式化定义是从LustreS中间表示开始的, 在LustreC, 中间表示彻底变换为一种类C的串行命令式语义.这些中间层语言所处位置, 如图 1和图 2所示.
可以看出, Vélus的同步数据流语义消去仅在一个阶段完成, 而L2C则经历了多个阶段逐步消去.由于L2C的源语言特征相比Vélus要复杂很多, 实践过程决定了跨多层的语义过渡是必然的选择.
Vélus在定义SN-Lustre语义时已完成排序(scheduling), 因此无需考虑同步数据流语言的数据流并发特性.L2C是在LustreS层进行排序(toposort), 在LustreS层有串行语义定义(节点内部的所有等式相互之间存在全序关系), 同时也定义有超粗粒度的并发语义(以等式为粒度, 等式操作是不可分割的原子操作, 等式之间存在由数据依赖所确定的偏序关系).
Vélus和L2C的同步数据流语义都选择了基于操作语义来定义(虽然也存在看似很不错的基于指称语义的基础工作).在Lustre语言的原始论文中, 作者给出了Lustre语言的基本操作语义规则.Vélus和L2C的操作语义定义首先要与学界公认的这些工作相符, 同时也应考虑实现的因素(交互式定理证明的方便性).比如, 采用Coinductive来定义流看似是非常自然的(因为要处理的是infinite对象), 然而无论是Vélus还是L2C均放弃选择这种方法, L2C团队当初遇到的问题主要是因为采用Coq实现整体任务需求的技术难度无法预测.
在Vélus和L2C的同步数据流语义中, 对于流数据对象的基本理解是一致的, 均将其看作是从自然数到取值论域的函数.比如, 可以将一个流s在第n个周期的值记为s(n).然而, 在具体实现上, L2C采取了一些不同的措施.特别是针对同步数据流语义中最具代表性的fby算子.
在定义fby算子的语义时, Vélus使用了一个辅助算子hold, 会将所处理的流数据对象在上一个激活周期的取值保持到其后续的无效周期, 这样, 若当前周期是激活周期, 则fby运算的结果就相当于当前周期hold运算的结果.这一思想在L2C项目开展的初期用来实现一种时钟归一化(clock unifying)算法, 其中定义了类似于hold的算子, 并用来刻画fby算子的语义.然而, 在后来的工作中, L2C摈弃了这种做法.主要原因是, 这种方法仅适合于定义二元fby算子, 而难以推广到实际应用中很有用的三元fby算子.L2C对二元和三元fby算子的语义定义采用了一致的框架, 定义一个大小为n的循环缓冲区, 并设法限定仅在激活周期可访问缓冲区, 这里, n即为三元fby算子的第3个参数(对于二元fby算子, n=1).
定义同步数据流语义的另一个重要方面, 就是语义环境中要保留子环境的状态, 这些子环境对应于当前环境下调用其他节点而形成的实例环境.保存这些子环境的原因是因为存在时态变量(见第4.2节), 需要保存历史状态, 这就导致了在调用的节点实例返回时不能像传统的函数调用那样释放掉变量的存储空间.因而, 我们必须要定义并维护一个树状的语义环境, 这对语义定义以及相应的证明来说, 难度增加了许多, 但这是我们必须要应对的.L2C在定义语义时对是否是时态变量进行了区分, 以方便对应到Clight的语义环境中.Vélus在文献中对这种树状语义环境也有许多描述, 但仅从论文无法了解其进一步的实现详情.
另外, L2C因支持高阶迭代算子以及更多的数组和结构体算子, 使语义定义的难度增大许多, 但相关细节不属本文所要讨论的范围.L2C的多阶段翻译架构(如图 2所示)正是为了适应各种各样的语义复杂度以及与Clight语义之间的巨大差异, 同样, 图 2所示的许多翻译步骤也不在本文所讨论的议题之内.
翻译正确性验证
在形式化定义动态语义阶段, Vélus和L2C的各阶段翻译正确性的验证目标与CompCert所建议的阶段翻译正确性目标从形式上是一致的, 都是要证明一种从高层到低层单向的语义模拟等价关系.这种模拟等价关系之所以可以是单向的, 是由于每一层语言均具有确定的语义(deterministic semantics).
对于同步数据流语义来说, 这种单向的语义模拟等价关系可大致描述为:任意数据流程序G的每个节点f, 若可以将输入流xs映射到输出流ys, 则对于翻译后得到的程序G’中与f对应的节点或函数f '以及这一层次中相应于G’的初始化函数reset, 如果G’在其第1个激活周期先执行reset后执行f ', 而在其他后续激活周期中都重复执行f ', 那么同样可以将xs映射到输出流ys.注意:这一命题中的G、f、xs和ys都是任意的.
虽然各阶段要证明的单向语义模拟等价关系形式上看都是相似的, 但具体到不同阶段, 其含义却都有所不同.首先, 各个阶段的语法和语义互不相同; 其次, 每个阶段可能有或没有语法层面的reset函数, 如果有的话, 不同阶段的reset函数也可能有所不同; 以及还有其他各种不同, 这里不再赘述.
一般来说, 从Lustre源程序到Clight程序的各阶段翻译过程中, 同步数据流语言的语法及语义特征逐渐被消去, C语言语法及语义特征逐渐增加.在定义上述单向语义模拟等价关系时, 所消失的语义特征描述通常会由新增加的语法特征来弥补.比如前面提到的reset特征, 在较高的语言层次, 语法层面并没有对应的函数, 所以是在语义定义中体现其行为, 而在靠后的语言层次(比如图 2所示的LustreE2层)已有语法层面的reset函数, 就不会也不可能通过语义定义来体现reset行为.
因Vélus和L2C的编译框架之间差异较大(如图 1和图 2所示), 可以想象到二者在翻译正确性验证方面存在较大的差异.这种差异体现在各个方面.这里仅列举一例.如果考虑第4.1节~第4.3节提到的核心翻译步骤, 在Vélus中仅由Translation一个阶段完成(如图 1所示), 而在L2C中则是分散到从LustreR1到LustreD的许多阶段实现的(如图 2所示).一般来说, 一个翻译阶段所负责的工作越多, 其正确性证明的难度也越大, 重用性也越差.然而, 另一方面, 翻译阶段也不能太多, 否则会导致语言层次增加太多, 反而加重维护的负担.因此, 应根据源语言的规模合理设计翻译阶段的数量.
Vélus中SN-Lustre之前的阶段未定义动态语义, 这些阶段所保持的特性主要是静态方面的.多数这些阶段, 甚至从SN-Lustre到Obc的过程(Translation), 基本上是继承前人(Bertails、Biernacki和Auger等人)的工作.Bourke等人的论文对这些静态语义相关阶段的介绍很少, 同时, Vélus未开源, 所以具体继承情况的详情未能很好地得到了解, 从Biernacki和Auger等人的论文仅可了解到其中的一些.
Vélus的语法分析器是Bourke等人重新写的, 它基于Jourdan等人提出的对LR(1)自动机进行确认并对确认程序进行验证的方法, 因此可以认为是一个经过形式化验证的语法分析器.L2C中, 最近刚完成与此平行的工作, 并以编译选项的方式集成到了开源L2C编译器中.
对于Vélus中的类型、时钟检查(elaboration)以及接下来的规范化过程(normalization), 仅了解Bertails、Biernacki和Auger等人在Coq中实现了这些过程以及进行了验证, 但他们的论文中未提到是如何进行验证的.L2C中与此对应的过程(LustreWGen、LustreVGen和LustreSGen)的验证在目前的开源版本中尚未发布, 相关工作仍在完善和整理之中.这些翻译过程在Vélus和L2C编译框架中所处位置, 如图 1和图 2所示, 下同.
Vélus对于排序过程(Scheduling)的验证是基于翻译确认的方法 具体实现在相关论文中未加介绍.L2C中的排序过程(Toposort)是经过严格形式化验证的, 证明了经过排序后的LustreS程序的串行语义行为, 与排序前LustreS程序的等式粒度并发语义所刻画的行为是兼容的.从实现角度来看, 对排序过程的形式化验证要比翻译确认的工作量大很多, 所以从通常的观点来看, 是否有必要这样做是值得商榷的.但L2C的这项工作, 对于在项目开展初期积累团队成员在使用Coq进行编程和验证的经验以及检查LustreS操作语义定义的合理性等方面起着重要的作用.
