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