system-verilog - 子模块是由求解器独立刺激还是通过连接的顶层模块刺激？

问题描述

其中一个练习（练习 4）实现了一个移位寄存器，由两个子模块和一个顶层模块组成。

编辑： 添加练习源代码：

我将在此处发布 vhdl 源代码，如果您更喜欢 verilog，在此链接的 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

关于问题 1

您看到的跟踪可能有某种工具错误，导致它无法dblpipe_vhd .i_clk正确设置的值。我这样说，因为您的断言似乎正在触发。该工具可能会看到直接下面没有时钟逻辑dblpipe_vhd并将时钟视为冗余。

该工具（以及其他形式验证工具）自动推断时钟并以不同的方式处理它们，以不同于描述逻辑的“常规”信号。你写的assumes时钟可能不会做任何事情。

（我不太熟悉sby，但我可以想象它实际上使用smt_clock信号来为逻辑提供时钟，而其他时钟只是用于调试目的。）

关于问题 2

IMO，要通过断言，两个 LSFR 从同一状态开始就o_data足够了。assume由于您从不应用重置，因此该工具可以自由选择初始状态。我猜作者试图说明这一点。

不知道为什么要在不先应用重置的情况下进行证明。那里有复位信号以确保可预测的启动状态。如果不先重置它们，您将永远不会真正使用它们。

关于问题 3

dblpipe_vhd不是顶级模块。dblpipe是。在语句下面添加了一个dblpipe_vhd被调用的实例。它只断言反对，所以它只需要那个信号。copydblpipebindo_data

system-verilog - 子模块是由求解器独立刺激还是通过连接的顶层模块刺激？

问题描述

相关问题1：

相关问题 2

相关问题 3

解决方案

关于问题 1

关于问题 2

关于问题 3

推荐阅读