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

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

define p 3 :signal_light_top_light1[0]=1;
define p 4 :signal_light_top_light2[2]=1;
define p 5 :signal_light_top_light2[1]=1;
define p 6 :signal_light_top_light2[0]=1;
alw((!p 1 and !p 2 and p 3 ) or (!p 1 and p 2 and !p 3 ) or (p 1 and !p 2 and !p 3 ))
/〉
5.5 利用工具进行验证
将 MSVL 程序与.p 文件作为 UMC4M 工具的输入,进行运行时验证,在终端输入命令:
UMC4M.exe signal_light.p signal_light.m
等待运行结束就可以得到运行结果.以性质 2 验证为例,其验证结果如图 9 所示.

Fig.9 Validation result
图 9 验证结果
5.6 实验结果

然后,根据运行结果判断 PPTL 公式对于 MSVL 程序是否有效,从而可以判断被提取的性质对于 Verilog 代
码是否有效.所有性质的验证结果见表 1.
Table 1 Experimental result
表 1 实验结果
性质 PPTL 公式 验证结果 运行验证时间 运行总时间
性质 1 Q 1= (¬p 0→(p 2∧p 5)) 有效 312ms 4353ms
性质 2 Q 2= (p 0→(◊p 3∧◊p 6)) 有效 226ms 1857ms
性质 3 Q 3= ¬(p 3∧p 6) 有效 218ms 1832ms
性质 4 Q 4= ((p 1⊕p 2⊕p 3)∧¬(p 1∧p 2∧p 3)) 有效 253ms 2884ms
6 结 论

本文通过使用基于 MSVL 的代码级运行时验证技术,完成了对模型建模和功能验证,将模型的 Verilog 代码
通过 V2M 工具转换成 MSVL 程序,完成 MSVL 建模,再使用 PPTL 公式将模型的性质提取出来,最后使用
UMC4M 验证工具,将性质和 MSVL 程序一起运行,得到验证结果.本文采用信号灯控制电路系统作为实验用例,
完成了整体实验流程和最后实验结果的正确输出.将来的工作是:通过该验证方法,可以对更多的模型进行功能
验证.

References:
[1] Alexander MJ, Cohoon JP, Ganley JL, Robins G. Performance-Oriented placement and routing for field-programmable gate arrays.
In: Proc. of the European Design Automation Conf. (EURO-DAC). IEEE, 1995. 80−85.
[2] Andraka R. A survey of CORDIC algorithms for FPGA based computers. In: Proc. of the 1998 ACM/SIGDA 6th Int’l Symp. on
Field Programmable Gate Arrays. New York: Association for Computing Machinery, 1998. 191−200.