子模块是由求解器独立激发的还是通过连接的顶层模块激发的？
Do sub modules get stimulated independently by the solver or through the connected top level module?
我正在尝试完成来自 Dan Gizzelquist 的 tutorial with example exercises。
其中一个练习（练习 4）实现了一个移位寄存器，由两个子模块和一个顶层模块组成。
编辑： 添加练习源代码：
我会 post 此处提供 vhdl 源代码，如果您更喜欢 verilog，this link.[=22= 的 exercise-04 文件夹中也有 verilog 源代码]
lfsr_fib.vhd
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity lfsr_fib is
generic (LN : natural := 8;
TAPS : std_logic_vector(LN-1 downto 0) := x"2d";
INITIAL_FILL : std_logic_vector(LN-1 downto 0) := x"01");
port (i_clk, i_reset, i_ce, i_in : in std_logic;
o_bit : out std_logic := INITIAL_FILL(0));
end entity lfsr_fib;
architecture behavior of lfsr_fib is
signal sreg : std_logic_vector(LN-1 downto 0) := INITIAL_FILL;
begin
process(i_clk)
begin
if (rising_edge(i_clk)) then
if (i_reset = '1') then
sreg <= INITIAL_FILL;
elsif (i_ce = '1') then
sreg(LN-2 downto 0) <= sreg(LN-1 downto 1);
sreg(LN-1) <= (xor (sreg and TAPS)) xor i_in;
end if;
end if;
end process;
process(sreg)
begin
o_bit <= sreg(0);
end process;
end behavior;
dblpipe.vhd
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity dblpipe is
port (i_clk, i_ce, i_data : in std_logic;
o_data : out std_logic := '0');
end entity dblpipe;
architecture behavior of dblpipe is
component lfsr_fib
port(i_clk, i_reset, i_ce, i_in : in std_logic;
o_bit : out std_logic);
end component;
signal a_data, b_data : std_logic;
begin
----
----
one: lfsr_fib port map (
i_clk => i_clk,
i_reset => '0',
i_ce => i_ce,
i_in => i_data,
o_bit => a_data);
two: lfsr_fib port map (
i_clk => i_clk,
i_reset => '0',
i_ce => i_ce,
i_in => i_data,
o_bit => b_data);
process(a_data, b_data)
begin
o_data <= a_data xor b_data;
end process;
----
----
end behavior;
正式属性文件：
`default_nettype none
//
module dblpipe_vhd(i_clk, i_ce, o_data);
input wire i_clk;
input wire i_ce;
input wire o_data;
`ifdef FORMAL
// Your goal: to get the following assertion to pass
//
// assume(one.sreg = two.sreg);
// assert(one.sreg == two.sreg);
always @(*)
begin
assert(o_data == 1'b0);
end
always @(*)
begin
if(i_clk)
begin
assume(one.i_clk);
assume(two.i_clk);
end
else
begin
assume(!one.i_clk);
assume(!two.i_clk);
end
end
//Trigger a counter example at step 18 - to check if the assumptions made where applied
// always @(posedge i_clk)
// if(f_time >= 18)
// assert(f_time < 18);
`endif
endmodule
bind dblpipe dblpipe_vhd copy (.*);
sby 控制脚本：
[options]
mode prove
[engines]
smtbmc
# abc pdr
# abc pdr
# aiger avy
# aiger suprove
[script]
read -vhdl lfsr_fib.vhd
read -vhdl dblpipe.vhd
read -formal dblpipe_vhd.sv
prep -top dblpipe
[files]
lfsr_fib.vhd
dblpipe.vhd
dblpipe_vhd.sv
相关问题一：
尝试不同的断言导致了以下 K 感应跟踪：
我的问题是，为什么跟踪显示子模块的时钟在滴答作响，而顶层时钟却没有？
即使添加以下代码也无法让时钟同时滴答作响：
always @(*)
begin
if(i_clk)
begin
assume(one.i_clk);
assume(two.i_clk);
end
else
begin
assume(!one.i_clk);
assume(!two.i_clk);
end
end
然而 i_ce 显然以某种方式连接，因为它在所有模块之间同步：
i_ce Traces
相关问题2
为什么问题的解决方案是断言两个sreg相等而不是假设它们相等？
当我们定义哪些输入对我来说是理所当然的时，听起来更像是在这种情况下应该使用 assume。
always @(*)
assert(one.sreg == two.sreg);
而不是：
always @(*)
assume(one.sreg = two.sreg);
相关问题3
有人可以向我解释为什么输入数据没有连接到包装器模块中吗？这样我就无法在跟踪视图中看到哪些数据被输入到顶层模块中...但是如果我将它添加到模块定义中，它在跟踪文件中仍然始终为 0。
module dblpipe_vhd(i_clk, i_ce, o_data);
input wire i_clk;
input wire i_ce;
input wire o_data;
我过去遇到的大多数问题都可以通过反复阅读可用的文档来解决，但是对于这些问题我自己找不到解决方案。
关于问题 1
您看到的跟踪可能存在某种工具错误，导致它无法正确设置 dblpipe_vhd .i_clk 的值。我这样说，是因为您的断言似乎正在触发。该工具可能会看到直接在 dblpipe_vhd 下没有时钟逻辑，并将时钟视为冗余。
该工具（以及其他形式验证工具）自动推断时钟并以不同于描述逻辑的“常规”信号的方式处理它们。您为时钟编写的 assumes 可能不会执行任何操作。
（我对 sby 不太熟悉，但我可以想象它实际上使用 smt_clock 信号为逻辑计时，而其他时钟仅用于调试目的。）
关于问题 2
IMO，要通过 o_data 的断言，assume 两个 LSFR 从相同状态开始就足够了。由于您从不应用重置，因此该工具可以自由选择初始状态。我猜作者是想说明这一点。
不知道您为什么要在不先应用重置的情况下进行校样。那里有复位信号以确保可预测的启动状态。如果不先重置它们，您将永远无法真正使用它们。
关于问题 3
dblpipe_vhd 不是顶层模块。 dblpipe 是。 bind 语句在 dblpipe 下添加了一个名为 copy 的 dblpipe_vhd 实例。它只针对 o_data 断言，所以它只需要那个信号。
我正在尝试完成来自 Dan Gizzelquist 的 tutorial with example exercises。
其中一个练习（练习 4）实现了一个移位寄存器，由两个子模块和一个顶层模块组成。
编辑： 添加练习源代码：
我会 post 此处提供 vhdl 源代码，如果您更喜欢 verilog，this link.[=22= 的 exercise-04 文件夹中也有 verilog 源代码]
lfsr_fib.vhd
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity lfsr_fib is
generic (LN : natural := 8;
TAPS : std_logic_vector(LN-1 downto 0) := x"2d";
INITIAL_FILL : std_logic_vector(LN-1 downto 0) := x"01");
port (i_clk, i_reset, i_ce, i_in : in std_logic;
o_bit : out std_logic := INITIAL_FILL(0));
end entity lfsr_fib;
architecture behavior of lfsr_fib is
signal sreg : std_logic_vector(LN-1 downto 0) := INITIAL_FILL;
begin
process(i_clk)
begin
if (rising_edge(i_clk)) then
if (i_reset = '1') then
sreg <= INITIAL_FILL;
elsif (i_ce = '1') then
sreg(LN-2 downto 0) <= sreg(LN-1 downto 1);
sreg(LN-1) <= (xor (sreg and TAPS)) xor i_in;
end if;
end if;
end process;
process(sreg)
begin
o_bit <= sreg(0);
end process;
end behavior;
dblpipe.vhd
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity dblpipe is
port (i_clk, i_ce, i_data : in std_logic;
o_data : out std_logic := '0');
end entity dblpipe;
architecture behavior of dblpipe is
component lfsr_fib
port(i_clk, i_reset, i_ce, i_in : in std_logic;
o_bit : out std_logic);
end component;
signal a_data, b_data : std_logic;
begin
----
----
one: lfsr_fib port map (
i_clk => i_clk,
i_reset => '0',
i_ce => i_ce,
i_in => i_data,
o_bit => a_data);
two: lfsr_fib port map (
i_clk => i_clk,
i_reset => '0',
i_ce => i_ce,
i_in => i_data,
o_bit => b_data);
process(a_data, b_data)
begin
o_data <= a_data xor b_data;
end process;
----
----
end behavior;
正式属性文件：
`default_nettype none
//
module dblpipe_vhd(i_clk, i_ce, o_data);
input wire i_clk;
input wire i_ce;
input wire o_data;
`ifdef FORMAL
// Your goal: to get the following assertion to pass
//
// assume(one.sreg = two.sreg);
// assert(one.sreg == two.sreg);
always @(*)
begin
assert(o_data == 1'b0);
end
always @(*)
begin
if(i_clk)
begin
assume(one.i_clk);
assume(two.i_clk);
end
else
begin
assume(!one.i_clk);
assume(!two.i_clk);
end
end
//Trigger a counter example at step 18 - to check if the assumptions made where applied
// always @(posedge i_clk)
// if(f_time >= 18)
// assert(f_time < 18);
`endif
endmodule
bind dblpipe dblpipe_vhd copy (.*);
sby 控制脚本：
[options]
mode prove
[engines]
smtbmc
# abc pdr
# abc pdr
# aiger avy
# aiger suprove
[script]
read -vhdl lfsr_fib.vhd
read -vhdl dblpipe.vhd
read -formal dblpipe_vhd.sv
prep -top dblpipe
[files]
lfsr_fib.vhd
dblpipe.vhd
dblpipe_vhd.sv
相关问题一：
尝试不同的断言导致了以下 K 感应跟踪：
我的问题是，为什么跟踪显示子模块的时钟在滴答作响，而顶层时钟却没有？
即使添加以下代码也无法让时钟同时滴答作响：
always @(*)
begin
if(i_clk)
begin
assume(one.i_clk);
assume(two.i_clk);
end
else
begin
assume(!one.i_clk);
assume(!two.i_clk);
end
end
然而 i_ce 显然以某种方式连接，因为它在所有模块之间同步： i_ce Traces
相关问题2
为什么问题的解决方案是断言两个sreg相等而不是假设它们相等？
当我们定义哪些输入对我来说是理所当然的时，听起来更像是在这种情况下应该使用 assume。
always @(*)
assert(one.sreg == two.sreg);
而不是：
always @(*)
assume(one.sreg = two.sreg);
相关问题3
有人可以向我解释为什么输入数据没有连接到包装器模块中吗？这样我就无法在跟踪视图中看到哪些数据被输入到顶层模块中...但是如果我将它添加到模块定义中，它在跟踪文件中仍然始终为 0。
module dblpipe_vhd(i_clk, i_ce, o_data);
input wire i_clk;
input wire i_ce;
input wire o_data;
我过去遇到的大多数问题都可以通过反复阅读可用的文档来解决，但是对于这些问题我自己找不到解决方案。
关于问题 1
您看到的跟踪可能存在某种工具错误，导致它无法正确设置 dblpipe_vhd .i_clk 的值。我这样说，是因为您的断言似乎正在触发。该工具可能会看到直接在 dblpipe_vhd 下没有时钟逻辑，并将时钟视为冗余。
该工具（以及其他形式验证工具）自动推断时钟并以不同于描述逻辑的“常规”信号的方式处理它们。您为时钟编写的 assumes 可能不会执行任何操作。
（我对 sby 不太熟悉，但我可以想象它实际上使用 smt_clock 信号为逻辑计时，而其他时钟仅用于调试目的。）
关于问题 2
IMO，要通过 o_data 的断言，assume 两个 LSFR 从相同状态开始就足够了。由于您从不应用重置，因此该工具可以自由选择初始状态。我猜作者是想说明这一点。
不知道您为什么要在不先应用重置的情况下进行校样。那里有复位信号以确保可预测的启动状态。如果不先重置它们，您将永远无法真正使用它们。
关于问题 3
dblpipe_vhd 不是顶层模块。 dblpipe 是。 bind 语句在 dblpipe 下添加了一个名为 copy 的 dblpipe_vhd 实例。它只针对 o_data 断言，所以它只需要那个信号。