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

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

4) IBDP⇔i<j 并且(σ,i+1,j)BP;
5) IB(P 1 ,…,P m )prjQ⇔存在整数 i=r 0 ≤…Ur m ≤j,使得(σ,r l−1 ,r l )BP l (1≤l≤m);且对如下两种σ′,有(σ′,0,
|σ′|)BQ:
i. r m =j 且σ′=σ↓(r 0 ,…,r h ),0≤h≤m;
ii. r m <j 且 σ σ′ = ↓ ( ,..., )r 0 r m σ ⋅ ( m r + 1 ,..., )j .

如果(σ,0,|σ|)BP,则表示公式 P 在区间σ上被满足,简写为σBP.若存在σ,σBP,则称公式 P 是可满足的;若对任
意σ,σBP,则称公式 P 是有效的.因此,公式 P 有效等价于公式¬P 不可满足.

3 V2M 转换工具

V2M 转换工具是一个将 Verilog 语言自动转换成 MSVL 语言的工具,其基本原理是:将 Verilog 源程序通过
词法分析和语法分析转换成语法树结构,该语法树结构可以作为一种中间表示形式,然后对中间表示的数据结
构通过转换算法转换为 MSVL 程序.其中:词法分析可以将源程序识别成 token 流,进而交给语法处理器去处理;
还可以自动将空格或者回车等无用成分进行过滤;并且识别错误信息,进行错误处理.词法分析的输出是 token
流,将词法分析的输出作为语法分析的输入,即可进行 Verilog 源程序的语法分析.语法分析的作用是分析 token
流,并且要排除语法错误,进而根据 token 流分析源代码的结构,最后生成语法树,作为一种中间表示.经过词法分
析和语法分析的转换,Verilog 源程序已经从一种硬件描述语言的程序变成了以语法树作为中间表示的一种存
储结构,将中间表示转换成 MSVL 程序的过程,就是将中间存储结构翻译成 MSVL 语言.Verilog 中的模块和函数
对应 MSVL 语句中的 function 模块,在 Verilog 中,各种基本语句在 MSVL 语言中都有其一一对应的表达形式.
这就是 V2M 工具的基本原理和基本组成结构.图 1 呈现了 Verilog 到 MSVL 转换器的工具流程图.

Fig.1 Flow chart of V2M tool
图 1 V2M 工具流程图

4 UMC4M 验证工具
UMC4M 是一种基于 MSVL 动态执行的代码级运行时验证工具,其原理是结合模型检测的一些策略,将程
序的时序性质验证转换为 MSVL 程序源代码的动态执行.该工具输入为 MSVL 程序和 PPTL 公式,MSVL 程序
用以描述系统的模型,而 PPTL 公式用以描述系统的性质.UMC4M 利用统一模型检测(UMC)原理 [18] ,将检测模
型是否满足性质的问题转化为程序的动态执行问题.验证过程如图 2 所示,主要步骤简要描述如下.
1) 利用工具 V2M 将待验证的 Verilog 程序转换为 MSVL 程序 M 1 ;
2) 利用 PPTL 公式 P 描述待验证的性质;
3) 利用工具 P2M [17] 将¬p 转化为 MSVL 程序 M 2 ;
4) 利用 MSVL 编译器 MC 对新得到的 MSVL 程序 M 3 =M 1 and M 2 进行编译,生成二进制代码 M 3 .exe;
5) 选择电路中所有二进制变量一组合适的值(01 串)作为 M 3 .exe 的输入;
6) 执行程序 M 3. exe:如果运行成功,则发现反例路径,即输入变量导致的运行轨迹;如果运行失败,则说明
本次运行满足性质.
该方法与模型检测方法不同,模型检测方法是要检测模型是否满足性质的有效性,就是要检测性质是否被
模型中的所有路径所满足.相比之下,对运行时验证方法,如所看到的程序的一次执行依赖于程序的一组输入,
而且仅检查了一条执行路径.这种方法简单易行,可以对大规模的程序电路进行验证.但是该方法的挑战是:如
n
何选择合适的输入集,使得程序运行能够覆盖所有路径.对于 n 个输入变量来说,它的输入集合是 2 ,这就迫使我