Do sub modules get stimulated independently by the solver or through the connected top level module?

Question

I am trying to work through a tutorial with example exercises from Dan Gizzelquist.

One of those exercises (exercise 4) implements a shift register, composed by two sub module and a top module.

Edit: Added Exercise source code:

I'll post the vhdl sources here, if you prefer verilog, there are also verilog sources in the exercise-04 folder at this link.

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;

formal properties file:

`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 control script:

[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

Related Question 1:

Playing around with different assertations led to the following K-Induction Trace:

My questions is, why does the trace show that the clock of the submodules are ticking while the top-level clock does not?

Even adding the following code did not get the clocks to tick simultaneously:

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

However i_ce is apparently connected somehow as it is in sync amongst all modules: i_ce Traces

Related Question 2

And why is the solution to the problem to assert that both sregs are equal instead of to assume that they are equal?

As we are defining which inputs shall be taken for granted for me it sounds more like assume should be used in this case.

always @(*)
    assert(one.sreg == two.sreg);

instead of:

always @(*)
    assume(one.sreg = two.sreg);

Related Question 3

Can somebody explain to me why the input data is not wired-up in the wrapper module? This way I cannot see what data is fed into the top-level module in the trace view... But if I add it to the module definition it still stays always 0 in the trace file.

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

Most questions that I had in the past could be solved by reading the available documentation again and again, but regarding these questions I just could not find a solution on my own.

Answer 1

On question 1

The trace you're seeing might have some kind of tool bug which causes it to not set the value of dblpipe_vhd .i_clk properly. I say this, because it seems that your assertion is firing. The tool probably sees that there is no clocked logic directly under dblpipe_vhd and treats the clock as redundant.

The tool (and other formal verification tools as well) infers clocks automatically and handles them differently to "regular" signals that describe logic. The assumes you wrote for the clocks will probably not do anything.

(I'm not that familiar with sby, but I can imagine that it actually uses the smt_clock signal to clock the logic and the other clocks are there just for debug purposes.)

On question 2

IMO, for the assertion on o_data to pass, it should be enough to assume that the two LSFRs start out from the same state. Since you never apply reset, the tool is free to choose the initial state. I'm guessing the author is trying to make a point of this.

No idea why you would want to do proofs without applying reset first. Reset signals are there to ensure predictable start states. You'll never really use them without resetting them first.

On question 3

dblpipe_vhd is not the top module. dblpipe is. An instance of dblpipe_vhd called copy is added under dblpipe by the bind statement. It only asserts against o_data, so it only needs that signal.