公开(公告)号：CN109725900B

公开(公告)日：2021-01-05

申请号：CN201910010500.6

申请日：2019-01-07

申请人： 西北工业大学 ,  华芯安信(北京)科技有限公司

发明人： 沈利香 ,  慕德俊 ,  曹国 ,  徐强 ,  时翔 ,  袁晓宇 ,  潘群

IPC分类号： G06F8/35

摘要： 本发明公开了一种寄存器传输级Verilog代码的SMV模型构建方法，用于解决现有寄存器传输级的SMV模型构建方法独立性差的技术问题。技术方案是采用静态分析Verilog代码的方法得到每个模块对应的控制流图，深度遍历控制流图得到模块中每个变量的 列表，利用 列表构建模块对应的SMV模型。其中，pc是路径条件，exp是在pc为真的情况下变量的表达式。本发明在读入Verilog代码后，针对生成的Verilog代码的解析树，不需要依赖第三方工具进行数据格式的转换和存储，可以作为一个独立的方法将输入的Verilog代码直接转换为SMV模型，实用性好。

公开(公告)号：CN107367686B

公开(公告)日：2019-11-22

申请号：CN201710462372.X

申请日：2017-06-19

申请人： 西北工业大学

发明人： 沈利香 ,  慕德俊 ,  时翔 ,  徐强 ,  邢业新 ,  何松 ,  袁晓宇

IPC分类号： G06F21/56

摘要： 本发明公开了一种RTL硬件木马测试向量的生成方法，主要包括生成控制流程图；并发符号执行；可满足性求解和生成测试向量。本发明采用静态分析Veri log代码的方法，采用多线程并发技术实现Veri log代码的并发符号执行，从而达到快速生成高路径覆盖率的测试向量的目的。

公开(公告)号：CN109725900A

公开(公告)日：2019-05-07

申请号：CN201910010500.6

申请日：2019-01-07

申请人： 西北工业大学

发明人： 沈利香 ,  慕德俊 ,  曹国 ,  徐强 ,  时翔 ,  袁晓宇 ,  潘群

IPC分类号： G06F8/35

摘要： 本发明公开了一种寄存器传输级Verilog代码的SMV模型构建方法，用于解决现有寄存器传输级的SMV模型构建方法独立性差的技术问题。技术方案是采用静态分析Verilog代码的方法得到每个模块对应的控制流图，深度遍历控制流图得到模块中每个变量的 列表，利用 列表构建模块对应的SMV模型。其中，pc是路径条件，exp是在pc为真的情况下变量的表达式。本发明在读入Verilog代码后，针对生成的Verilog代码的解析树，不需要依赖第三方工具进行数据格式的转换和存储，可以作为一个独立的方法将输入的Verilog代码直接转换为SMV模型，实用性好。

公开(公告)号：CN107367686A

公开(公告)日：2017-11-21

申请号：CN201710462372.X

申请日：2017-06-19

申请人： 西北工业大学

发明人： 沈利香 ,  慕德俊 ,  时翔 ,  徐强 ,  邢业新 ,  何松 ,  袁晓宇

IPC分类号： G01R31/3183 ,  G01R31/317

摘要： 本发明公开了一种RTL硬件木马测试向量的生成方法，主要包括生成控制流程图；并发符号执行；可满足性求解和生成测试向量。本发明采用静态分析Veri log代码的方法，采用多线程并发技术实现Veri log代码的并发符号执行，从而达到快速生成高路径覆盖率的测试向量的目的。