prove mode seems to be ignoring assumes during induction

[Topi-ab]

Problem description

prove_1 induction (boolector) fails with depth of 30 (as it should).
The produced waveform has illegal (as per assumes) transitions.
The a_in is assumed to have minimum pulse width of 2 clock cycles (assume a_3).
The waveform shows a_in pulsing with width of 1 clock cycle.

prove_2 induction (yices) fails, but produces consistent waveform (which isn't a proof that it couldn't fail).

How to reporoduce

. prove_01.sh prove_1

prove_01.vhdl:

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

entity prove_01 is
    port(
        clk_in: in std_logic;
        sreset_in: in std_logic;

        a_in: in std_logic;

        b_out: out std_logic
    );
end;

architecture rtl of prove_01 is
    signal state: unsigned(7 downto 0);
begin
    process(clk_in)
    begin
        if rising_edge(clk_in) then
            if a_in = '1' then
                state <= (state + 1) mod 32;
            end if;
            if state = 0 then
                b_out <= a_in;
            else
                b_out <= '0';
            end if;

            if sreset_in = '1' then
                state <= (others => '0');
                b_out <= '0';
            end if;
        end if;
    end process;

    default clock is rising_edge(clk_in);

    a_1: assume {sreset_in[*2]};
    a_2: assume {not sreset_in; sreset_in} |=> {sreset_in};
    a_3: assume always {not a_in; a_in} |=> {a_in};
    a_4: assume always {a_in; not a_in} |=> {not a_in};

    f_1: assert always {b_out='1'} |=> {b_out='0'[*31]} abort prev(sreset_in);
end;

prove_01.sby

[tasks]
bmc
prove_1
prove_2

[options]
bmc: mode bmc
depth 20
prove_1: mode prove
prove_1: depth 30
prove_2: mode prove
prove_2: depth 30

[engines]
smtbmc boolector
prove_1: smtbmc boolector
prove_2: smtbmc yices

[script]
ghdl --std=08 prove_01.vhdl -e prove_01
prep -top prove_01

[files]
prove_01.vhdl

prove_01.sh

#!/bin/bash

docker run -v $PWD:/formal -w /formal --rm -it hdlc/formal:all bash -c "sby --yosys 'yosys -m ghdl' -f prove_01.sby $@"

[Topi-ab]

I managed to make it fail on boolector, yices and z3.

prove_01.vhdl:

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

entity prove_01 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
    );
end;

architecture rtl of prove_01 is
    signal state: unsigned(7 downto 0);
begin
    process(clk_in)
    begin
        if rising_edge(clk_in) then
            if a_in = '1' then
                state <= (state + 1) mod 32;
            end if;
            if state = 0 then
                b_out <= a_in;
            else
                b_out <= '0';
            end if;

            if sreset_in = '1' then
                state <= (others => '0');
                b_out <= '0';
            end if;
        end if;
    end process;

    c_out <= a_in;

    default clock is rising_edge(clk_in);

    a_1: assume {sreset_in[*2]};
    a_2: assume {not sreset_in; sreset_in} |=> {sreset_in};
    a_3: assume always {not a_in; a_in} |=> {a_in};
    a_4: assume always {a_in; not a_in} |=> {not a_in};

    f_test: assert always {not c_out; c_out} |=> c_out;

    f_1: assert always {b_out='1'} |=> {b_out='0'[*31]} abort prev(sreset_in);

    f_2: assert always state <= 31 abort sreset_in;
end;

It produces c_out with high pulse of 1 clk.

[jix]

Note that the docker container you're using provides outdated versions of yosys and SBY. While I cannot reproduce the specific traces with an up to date https://github.com/YosysHQ/oss-cad-suite-build release, I can reproduce the underlying issue that is causing this:

The problem seems to be that the state machine that GHDL (or the ghdl yosys plugin?) generates for the PSL assumption contains a state in which the actual input sequence is ignored. That state is not reachable from the initial state of the design, but induction requires that every state is considered as possible initial state, so an induction trace might end up starting in that otherwise unreachable state.

In this particular instance the unreachable state consists of a FF where the Q output feeds directly back into D, making it a constant value. Yosys is able to optimize this away, ensuring that induction cannot pick the unreachable constant value, but this requires the additional optimization pass "opt_dff -keepdc" after the "prep" pass. Depending on how GHDL produces these state machines that might not be sufficient for more complex PSL expressions.

To avoid this in general, GHDL would need to change its PSL state machine generation to avoid unreachable states and/or ensure to transition out of unreachable states. An alternative would be to use the "abc pdr" engine instead of "smtbmc" as PDR will consider the reachability of states and will always produce counter-example traces starting from the initial state.

[Topi-ab]

I ran the code through yosys:

ghdl --std=08 prove_01.vhdl -e prove_01

flatten

rename -enumerate -pattern unnamed_assert_% t:$assert
rename -enumerate -pattern unnamed_assume_% t:$assume
rename -enumerate -pattern unnamed_cover_% t:$cover

expose -evert t:$assert t:$assume t:$cover

opt

write_verilog prove_01.v

And then used Quartus to pretty-print it to a netlist schematic.

Which part of this synthesized checker has the problem you described? Or did it got opimized away during the process?

[Topi-ab]

I found it. Yosys indeed optimized it away. Using GHDL synthesis command to generated vhdl netlist, and then manually renaming relevant netnames so that quartus doesn't combine the registers together. I will escalate this as GHDL issue...

https://github.com/ghdl/ghdl/issues/2672https://github.com/ghdl/ghdl/issues/2672

[jix]

I'm closing this issue as this is working as intended on the Yosys side. The default set of optimizations performed by prep for FV is intentionally lightweight, as there is value in preserving more structure of the input design and in reducing the potential exposure to undiscovered bugs in the more advanced optimizations. As far as I can tell, this also doesn't affect the System Verilog Assertions implementation that is part of Yosys[^1], which doesn't generate unreachable states like this, so I wouldn't expect this to be an inherent obstacle when implementing PSL either, although that doesn't mean that any specific implementation could be easily changed to avoid this. Finally, even with such a state machine encoding, there is always the option to manually add opt_dff -keepdc as part of the SBY script to enable this specific optimization or to use an engine that implements a method that is not sensitive to unreachable states in the way that k-induction is.

[^1]: While the SVA implementation itself is open source, it does depend on, and is closely tied to, the commercial-only verific frontend.