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

姚广宇 等:芯片开发功能验证的形式化方法 1801

1 建模仿真验证语言 MSVL

MSVL 是一种建模仿真和验证语言,它是投影时序逻辑的一个可执行子集.通过 MSVL,可以对软硬件系统
进行建模,并根据使用逻辑公式描述的系统期望性质,进行软硬件系统的形式化验证.
MSVL 的语句定义如下.
语句名称 语法定义
空语句 empty
skip 语句 skip
区间长度语句 len(n)
下一状态赋值语句 x:=e
当前状态赋值语句 x<==e
选择语句 p 1 or p 2
并行语句 p 1 ||p 2
合取语句 p 1 and p 2
If 条件语句 if b then {p 1 } else {p 2 }
等待语句 await(b)
Always 语句 always(p)
顺序语句 p 1 ;p 2
投影语句 (p 1 ,...,p n )prjp
Next 语句 next(p)
框架变量语句 frame(x)
While 循环语句 while (b) {p}
局部变量语句 local x:p
上述定义中,e 表示算术表达式,b 表示布尔表达式,它们的定义与 C 语言中的定义基本相同.另外,MSVL 中
也定义了丰富的数据类型,包括整型、浮点型、布尔型、字符型、数组、指针和结构体.从程序上看,MSVL 简
单易行,类似于 C 语言;从逻辑角度看,每一条语句又都是一个投影时序逻辑公式.
目前已经开发了 MSVL 编译器 MC 以及解释器,解释器支持 MSVL 程序一次执行过程的仿真和对 MSVL
程序所有路径的建模以及验证.

2 命题投影时序逻辑

命题投影时序逻辑(propositional projection temporal logic,简称 PPTL)是一种基于区间的时序逻辑,它的主
要时序操作符是 prj 和 next.而命题区间时序逻辑(propositional interval temporal logic,简称 PITL)也是一种基于
区间的时序逻辑,它的主要时序操作符是 chop 和 next.文献[17]证明,PPTL 在有穷和无穷区间都是可判定的.这
一结论使我们可以将 PPTL 应用于模型检测.PPTL 公式的语法可定义如下:
P::=p|DP|¬P|P 1 ∨P 2 |(P 1 ,…,P m )prjQ,
其中,p∈可数的命题变元集合 Prop,P 和 P 1 ,…,P m ,Q 都是 PPTL 合式公式.
一个 PPTL 公式 P 可用一个三元组 I=(σ,i,j)来解释,其中,σ=〈s 0 ,s 1 ,…,〉定义为非空的有穷或无穷状态序列,|σ|
表示区间长度.若σ为无穷区间,则|σ|=ω.定义U为≤−{(ω,ω)}.i 和 j 是整数并且 iUj≤|σ|.定义(σ,i,j)BP 表示 P 在σ

的某一子区间〈s i ,…,s j 〉上可满足,其中,s i 表示当前状态,s i :Prop→B={true,flase}.可满足关系可定义如下.
1) IBp⇔对任意原子命题 p 有 s i [p]=true;
2) IB¬P⇔IHP;
3) IBP∨Q⇔IBP 或 IBQ;