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

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

output (signal_light_top_light1[1]) and skip;
output (signal_light_top_light1[0]) and skip;
output (signal_light_top_light2[2]) and skip;
output (signal_light_top_light2[1]) and skip;
output (signal_light_top_light2[0]) and skip;
output (signal_light_top_count[5]) and skip;
output (signal_light_top_count[4]) and skip;
output (signal_light_top_count[3]) and skip;
output (signal_light_top_count[2]) and skip;
output (signal_light_top_count[1]) and skip;
output (signal_light_top_count[0]) and skip;
now:=now+1})

姚广宇(1995－),男,博士生,CCF 学生会 段振华(1948－),男,博士,教授,博士生导
员,主要研究领域为 FPGA 布局,形式化 师,CCF 会士,主要研究领域为高可信软件
验证. 开发及验证.

张南(1984－),女,博士,副教授,博士生导 刘灵敏(1995－),男,硕士生,主要研究领域
师,CCF 高级会员,主要研究领域为形式化 为 Verilog 代码和模型功能一致性验证.
验证.

田聪 (1981 － ), 女 , 博士 , 教授 , 博士生导 孙风津(1995－),男,硕士生,主要研究领域
师,CCF 杰出会员,主要研究领域为软件安 为 Verilog-MSVL 代码转换技术,形式化
全:程序漏洞分析,恶意代码检测. 验证.