形式验证求解器对子模块的激励方式及dblpipe工程相关问题咨询

形式验证求解器不会独立给子模块生成激励，所有子模块的输入完全由你指定的顶层模块的内部连接关系驱动，求解器仅会对顶层模块的输入端口做约束/随机化，子模块的输入跟随顶层连接自动赋值。

相关问题1 子模块时钟与顶层时钟不同步 #

你遇到的现象是VHDL代码在SymbiYosys工具链中的层次路径兼容性问题导致的：

• 你设计里one和two的i_clk已经和顶层i_clk硬连，理论上不可能出现跳变不一致的情况，trace里的偏差是波形查看器的路径解析错误，不是真实的电路激励行为
• 你写的assume约束不生效，是因为SymbiYosys的VHDL前端对跨层次的信号路径引用支持不好，约束没有实际作用
• i_ce信号显示同步是因为它是顶层输入端口，路径解析逻辑更简单，没有匹配错误
  如果要解决这个问题，可以换用该练习的Verilog版本做验证，Verilog的层次路径引用在SymbiYosys中支持更完善。

相关问题2 选择assert而非assume的原因 #

assume和assert的作用有本质区别：

• assume是给求解器指定输入约束，告诉求解器“这个条件我已经保证一定会满足，你不需要验证，直接把它当成前提条件生成输入即可”，如果这里用assume(one.sreg == two.sreg)，相当于你直接人为排除了所有两个寄存器不等的情况，哪怕设计本身有bug，求解器也不会发现，完全失去验证意义
• assert是要求求解器证明的特性：你的设计里两个LFSR的所有输入、初始值、配置参数完全一致，理论上所有时刻sreg都应该相等，这是设计本身要实现的特性，所以要用assert来验证它成立，只有这个断言成立，才能推导出最终的o_data == 1'b0断言成立。

相关问题3 wrapper模块的i_data信号问题 #

你遇到的问题是端口定义的笔误导致的：

• 你写的dblpipe_vhd模块首先漏了i_data的端口声明，还错误的把o_data声明为input类型，导致bind的时候无法正确匹配顶层的i_data信号
• 你即使后续添加了i_data端口，如果没有修正端口方向、也没有对应更新bind的连接逻辑，求解器会默认把未连接的输入设为恒值，所以trace里显示恒0
  修正端口定义为下述格式即可正常查看i_data波形：

module dblpipe_vhd(i_clk, i_ce, i_data, o_data);
    input   wire    i_clk;
    input   wire    i_ce;
    input   wire    i_data;
    output  wire    o_data;

后续如果需要让i_data生成跳变的激励，可以额外增加i_ce的约束，让求解器生成更丰富的输入场景。

内容的提问来源于stack exchange，提问作者Stone