Page 226 - 《软件学报》2021年第6期

1800 Journal of Software 软件学报 Vol.32, No.6, June 2021

随着集成电路的规模越来越大,集成密度越来越高,相应的设计越来越复杂,电路设计已经由手工设计转向
使用硬件描述语言(Verilog 或 VHDL)来完成电路设计.而使用硬件描述语言设计的电路可以经过行为综合、工
艺映射、打包、布局和布线,快速的烧录到现场可编程门阵列(field-programmable gate array,简称 FPGA) [1,2] 上
进行测试,这也是现在集成电路设计的主流技术.
由于采用 FPGA 设计专用集成电路(application specific integrated circuit,简称 ASIC),用户可以在确认系统
正确后才进行流片,所以能得到合格的芯片,它是 ASIC 电路中设计周期较短、开发费用较低、风险较小的方法
之一.所以,FPGA 被广泛用于电信、汽车导航、通信卫星、航空航天等领域芯片开发 [3−6] .
模型驱动的 FPGA 设计方法能够利用模型驱动的优点,使设计更加安全可靠.特别是,能够使用图形语言描
述和验证业务需求和系统设计,使得设计更合理、更稳定、更具适应性.因为设计是基于模型的,并且在构建模
型前进行全面地分析,基于模型的规格说明设计系统时,更容易得到符合需求的设计模型.
而模型驱动的 FPGA 设计需要证明 FPGA 设计模型与硬件描述语言生成代码的一致性.这是芯片开发领域
一个关键性问题.
[7]
国防科大 提出了一种系统级模型和寄存器级(register transfer level,简称 RTL)模型顺序等效检查方法.所
提出的方法基于带有数据路径等效检查方法的有限状态机,使用机器学习技术从所有路径中识别有限状态机
的对应路径序偶对.然后,通过符号仿真比较相应的路径序偶对,将所有路径分开对应的路径序偶对,避免了路
径序偶对的盲目比较.这种方法可以处理截然不同的系统级模型和 RTL 级模型设计,并大大降低了基于路径的
[8]
有限状态机等效性检查问题的复杂性.得克萨斯大学奥斯汀分校的 Vasudevan 等人 提出了一种用于顺序等效
检查的系统级规范及其在 RTL 中实现的新颖技术,在源代码级别上为这些系统构建了 Kripke 结构或状态转换
[9]
图,来进行模型和 RTL 代码的等价性验证.圣保罗大学的 Marquez 等人 提出了一种用于电子系统级规范和
RTL 实现之间的时序等价性检查形式和算法,该方法基于深度状态序列的概念以及序列之间的功能覆盖关系,
用带数据路径的有限状态机分别对高级参考模型和待验证设计的行为进行建模,对模型的状态机中的每一个
深度状态序列,如果都能在待验证设计的状态机中找到在功能上覆盖它的深度状态序列,说明待验证设计的状
态机在功能上覆盖模型的状态机,从而验证了电子系统级规范和 RTL 描述之间的时序等价性.波特兰州立大学
的 Yang [10] 提出了一种等价性检查框架,该框架通过 3 个阶段来进行电子系统级规范和 RTL 实现的等价性验证:
(1) 编译器转换;(2) 为每个操作分配一个时钟周期,并满足用户指定的约束;(3) 局部优化和 RTL 生成,然后逐
个检查每个阶段的等价性.目前,已提出的仿真方法和一致性验证方法能够在一定程度上保障模型和代码的一
致性,但是这些方法都存在验证效率低、工作量大等问题.本文提出了一种新的基于代码运行时验证方法来检
查设计模型和生成代码的一致性.
运行时验证(runtime verification) [11] 是近年来发展起来的一种新兴的验证技术.在运行时验证中,所关注的
只有系统在运行时所表现出的行为,并在系统实际运行的时候对其监控,最终可根据系统运行时的状态信息来
验证所期望的性质是否满足.
我们拟提出基于建模仿真验证语言(modeling simulation verification language,简称 MSVL) [12,13] 的运行时验
证方法,来验证模型和生成代码的一致性.该方法用 MSVL 语言描述系统的模型,用命题投影时序逻辑
(propositional projection temporal logic,简称 PPTL) [14,15] 公式来描述期望的性质.在实践中,我们通常将一个
Verilog 程序自动转换为 MSVL 程序 M 1 ,将期望的性质 P 的非转换为另一个 MSVL 程序 M 2 ,从而得到一个新的
MSVL 程序 M 3 =M 1 and M 2 .为了执行 M 3 ,我们将 M 3 通过 MSVL 编译器 MC [16] 进行编译,得到可执行代码 M 3 .exe.
对 M 3 .exe 选择合适的输入,运行 M 3 .exe,若程序运行为真,则我们找到一个违反性质的一条路径;否则,我们仅知
道当前执行是满足性质的.该方法的主要优点是:(1) 可以对大规模电路设计进行验证;(2) 验证过程可以自动
化实现.
本文第 1 节主要介绍建模仿真验证语言 MSVL 的基本语法.第 2 节主要介绍命题投影时序逻辑的主要知
识.第 3 节主要介绍使用的 V2M 转换工具.第 4 节主要介绍 UMC4M 验证工具框架和验证方法.第 5 节主要通过
信号灯控制电路系统的例子进行建模和验证.第 6 节是对论文方法的总结概述.