PSL synthesized checker has "constant loopback", which makes symbiyosys k-induction fail

[Topi-ab]

Description
prove mode checking with symbiyosys finds violation of asserts, where assume is also violated.

It seems that GHDL synthesized "constant loopback" (see below image with yellow circles) is the root problem.

For symbiyosys k-induction this makes it misbehave.

Expected behaviour
Synthesized netlist which is not having "constant loopbacks".

How to reproduce?
Files and background info here:
YosysHQ/sby#280

synthesizing the vhdl file with
ghdl -a --std=08 prove_01.vhdl; ghdl --synth --std=08 prove_01>file.vhdl
and manually routing a_3 assume and f_test assert to output ports

entity synth is
  port (
    clk_in: in std_logic;
    sreset_in: in std_logic;
    a_in: in std_logic;
    b_out: out std_logic;
    c_out: out std_logic;
    a_3_out: out std_logic;
    f_test_out: out std_logic
  );
...
  -- signal n90_q : std_logic_vector (3 downto 0) := "0001";
  signal n90_q_0_a : std_logic := '1';
  signal n90_q_1_b : std_logic := '0';
  signal n90_q_2_c : std_logic := '0';
  signal n90_q_3_d : std_logic := '0';
...
  process (wrap_clk_in)
  begin
    if rising_edge (wrap_clk_in) then
      -- n90_q <= n102_o;
      n90_q_0_a <= n102_o(0);
      n90_q_1_b <= n102_o(1);
      n90_q_2_c <= n102_o(2);
      n90_q_3_d <= n102_o(3);
    end if;
  end process;
...
  -- n91_o <= n90_q (0);
  n91_o <= n90_q_0_a;
...
  -- n96_o <= n90_q (1);
  n96_o <= n90_q_1_b;
...
  -- n98_o <= n90_q (2);
  n98_o <= n90_q_2_c;
...
  a_3: assert n71_o = '1' severity warning; --  assume
  a_3_out <= n71_o;
...
  f_test: postponed assert n104_o = '1' severity error; --  assert
  f_test_out <= n104_o;

And then synthesizing with Quartus to get nice schematic:

The yellow marks show loopback without any real function (or is there?).

The problem can be seen here:

c_out has pulse width of one clock cycle (assert failure), even though the assume a_3 prevents it.

Context
Using latest hdlc/formal:all docker image.

• OS:
• Origin:
  • Package manager: version
  • Released binaries: tarball_url
  • Built from sources: commit SHA

Additional context

[Topi-ab]

It seems that the "constant loopback" DFF is result of PSL always.

1. Is always the only construct which creates such structure?
2. Could it be changed so that it is replaced with constant '1'?

[tgingold]

Yes, I am pretty sure that only always creates such structure.

I will try to optimize away this state. Meanwhile, you have to use the yosys optimization pass.

Rq: probably, it is possible to reproduce the issue using user code (ie, something like assume never unstable_a;). So I fear the yosys optimization is somewhat required.

[Topi-ab]

probably, it is possible to reproduce the issue using user code (ie, something like assume never unstable_a;)

I didn't follow this: assume always is also user code.

What is special in never vs always? Both propably shall generate similar constant loopback register...

[tgingold]

I mean, the user can write such de-optimized code by itself for assume/restrict and then sby would violate them.

Anyway.

[tgingold]

I am still investigating this issue.
I think these the second assume is not correct.
The first one is

	a_1: assume {sreset_in[*2]};

The second one:

	a_2: assume {not sreset_in; sreset_in} |=> {sreset_in};

cannot happen, as sreset_in must be set in the first cycle. Did you forget an always ?

[NikLeberg]

I can attest that this also fixed numerous failures of symbiyosys prove mode tasks of mine. Previously the k-induction prove would fail with VHDL/GHDL but a seemingly identical verilog implementation with plain yosys did not fail the prove.

You do the heavens work.

[tgingold]

Thank you. It took me a while to fully understand the issue and to create a reproducer, but I have learnt for this issue.