Режим обложки SymbiYosys не работает при проверках, которые не являются обложками

Question

Я изучаю формальную верификацию с использованием PSL и VHDL с SymbiYosys.

У меня есть следующий тест в 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};
}

У меня есть следующее в Formal.sby, так что я использую как BMC, так и режим обложки:

      [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

Когда я запускаю его, проверка BMC проходит (т.е. ни одно утверждение не было достигнуто).

Однако, когда запускается проверка покрытия, я получаю:

      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.

Мой вопрос: почему режим прикрытия рассматривает мои два утверждения как прикрытия?

Какого состояния он пытается (и не может) достичь?

Меня смущает то, что режим BMC работает нормально, что, по-видимому, указывает на то, что мои утверждения не достигнуты. Но режим укрытия рассматривает их как укрытия, до которых, очевидно, никогда не добраться.

Answer 1

GHDL автоматически генерирует директивы покрытия для каждой директивы утверждения (с оператором импликации) автоматически во время синтеза. Это можно использовать, чтобы обнаружить, есть ли у вас бесполезные доказательства во время BMC или в режиме доказательства. Пустые доказательства — это свойства, предпосылки которых не выполнены. Например:

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

Еслиo_ledsвсегда"00000"тогда предварительное условие никогда не выполняется, поэтому свойство никогда не активируется. В этом случае оно будет успешно доказано, даже если предварительное условие никогда не будет истинным. Это такое пустое доказательство.

Директива покрытия, которую генерирует GHDL, выглядит примерно так:

      cover {o_leds /= "00000"};

Обычно вам нужно обнаружить такие свойства, поскольку они не могут выйти из строя во время формального запуска. С бегущим покрытием вы можете очень легко обнаружить такие свойства.

Вы можете отключить генерацию директивы покрытия, используя опцию GHDL.--no-assert-cover.

В разделе синтеза документов GHDL содержится дополнительная информация: https://ghdl.github.io/ghdl/using/Synthesis.html#assertions-psl-and-formal-verification.