公开(公告)号：CN109725900B

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

申请号：CN201910010500.6

申请日：2019-01-07

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

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

IPC分类号： G06F8/35

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

公开(公告)号：CN109725900A

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

申请号：CN201910010500.6

申请日：2019-01-07

申请人： 西北工业大学

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

IPC分类号： G06F8/35

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