Page 231 - 《软件学报》2021年第6期
P. 231
姚广宇 等:芯片开发功能验证的形式化方法 1805
在利用 V2M 工具进行转换的过程中,需要判断转换结果正确与否.可以采用如下方法:转化的结果是
MSVL 代码,可以对 MSVL 代码使用 MSVL 编译器进行编译执行,如果执行的结果与源 Verilog 代码在 iverilog
下仿真的结果一致,则证明转换正确,不一致则转换错误.具体可通过对比波形和对比 01 结果串两种方式进行
判断.
以交通信号灯控制电路系统为测试用例,对判断转化的 MSVL 代码是否正确的过程进行说明.
首先对测试用例在 iverilog 软件上进行编译和逻辑仿真,结果如图 7 所示.
主模块中有两个 1 位的输入信号 clk,rst 和两个 3 位的输出信号 light1,light2.clk 与 rst 代表着时钟信号和复
位信号,light1 与 light2 代表两个方向的信号灯的状态.
将交通信号灯控制电路系统的源代码用 V2M 转换器进行转换,转换后的 MSVL 代码在编译器上进行编译
执行,然后输入与 Verilog 仿真输入相同的数据,通过 01 结果串对比,即,将 MSVL 程序运行结果的每位的输出值
与 iverilog 下仿真值进行比较.为了便于观察也可通过波形比较他们结果是否一致,从图 7 和图 8 中我们可以看
出两者结果一致,证明 V2M 转换器在转换交通信号灯控制电路系统这一测试用例时,能正确转换.
Fig.7 Verilog simulation result
图 7 Verilog 仿真结果
Fig.8 MSVL simulation result
图 8 MSVL 仿真结果
5.3 提取性质
从系统的功能需求中提取待验证的性质,并使用 PPTL 公式描述.
使用 p 0 ,p 1 ,p 2 ,p 3 ,p 4 ,p 5 ,p 6 分别表示启动系统、主干道红灯亮、主干道黄灯亮、主干道绿灯亮、支干道红灯
亮、支干道黄灯亮和支干道绿灯亮这 7 个原子命题,则可以提取以下几条性质.
性质 1. 如果系统没启动,那么保持所有方向黄灯亮:
Q 1 = (¬p 0 →(p 2 ∧p 5 )).
性质 2. 将来某个时刻主干道绿灯亮,且将来某个时刻支干道绿灯亮:
Q 2 = (p 0 →(◊p 3 ∧◊p 6 )).
性质 3. 在任意时刻,主干道和支干道绿灯不能同时亮:
