SymbiYosys cover mode fails on checks that aren't covers

Question

I am learning formal verification using PSL and VHDL with SymbiYosys.

I have the following test in Formal.psl:

vunit f_top_asm_verify(TopAssembly(Rtl))
{
   default clock is rising_edge(i_clk);

   f_stalls: assert always {o_leds /= "00000"   } |-> {o_stall};
   f_wren:   assert always {i_we and not o_stall} |=> {o_stall};
}

I have following in Formal.sby, such that I am running both BMC and cover mode:

[tasks]
bmc
cover

[options]
bmc: mode bmc
bmc: depth 10
cover: mode cover
cover: depth 20

[engines]
smtbmc

[script]
ghdl --std=08 -gCLOCK_SPEED=3 TopAssembly.vhd Formal.psl -e TopAssembly
prep -top TopAssembly

[files]
TopAssembly.vhd
Formal.psl

When I run it, the BMC check passes (i.e. neither assert was reached).

However, when the cover check runs, I get:

SBY  9:09:58 [Formal_cover] engine_0: ##   0:00:00  Checking cover reachability in step 19..
SBY  9:09:58 [Formal_cover] engine_0: ##   0:00:00  Unreached cover statement at f_top_asm_verify.f_stalls.cover.

My question is, why does the cover mode treat my two asserts as cover statements?

What condition is it trying (and failing) to reach?

My confusion is because the BMC mode works fine, which would seem to indicate my asserts are not reached. But the cover mode treats them as covers which are obviously never reached.

Answer 1

GHDL automatically generates cover directives for each assert directive (with an implication operator) automatically during synthesis. This can be used to detect if you have vacuous proofs during BMC or prove mode. Vacuous proofs are properties which preconditions aren't fullfilled. For example:

f_stalls: assert always {o_leds /= "00000"} |-> {o_stall};

If o_leds is always "00000" then the precondition is never fullfilled, so the property is never activated. In this case it would be proven successfully, even if the precondition never was true. This is such a vacuous proof.

The cover directive GHDL generates looks similar like this:

cover {o_leds /= "00000"};

Normally you want to detect such properties as they can't fail during the formal run. With running cover you can detect such properties very easily.

You can disable the cover directive generation by using the GHDL option --no-assert-cover.

GHDL docs synthesis section has more information: https://ghdl.github.io/ghdl/using/Synthesis.html#assertions-psl-and-formal-verification