SymbiYosys覆盖模式误将断言视为覆盖语句的技术问询

问题背景 #

我正在学习使用PSL与VHDL结合SymbiYosys做形式验证，写了PSL断言和SBY配置文件后，BMC模式运行正常，但覆盖模式出现未达覆盖的报错，对此有疑问。

PSL断言代码（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};
}

SymbiYosys配置文件（Formal.sby） #

[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.

疑问解答 #

核心疑问与解析 #

1. 为什么覆盖模式会处理断言？
   SymbiYosys的cover模式会自动为每个PSL断言生成对应的覆盖检查，目的是验证断言的前提条件是否可达。如果断言的前提永远不会触发，那这个断言相当于“空真”——逻辑上永远成立，但对实际设计没有验证价值，覆盖模式就是要排查这种无意义的断言。

2. 覆盖模式尝试达成的条件是什么？
   对于蕴含式断言assert always {A} |-> {B}，覆盖检查的目标是找到一个时钟周期，让前提A为真：

   • 针对f_stalls断言，覆盖目标是o_leds /= "00000"，报错说明在深度20的范围内，o_leds始终是"00000"，这个前提从未被触发。
   • 针对f_wren断言，覆盖目标是i_we and not o_stall，如果同样报错，说明该组合状态在指定深度内也从未出现。

3. BMC与覆盖模式的差异
   BMC模式验证的是“断言是否永远成立”——如果前提条件从未触发，断言自然不会失败，所以BMC会通过；但覆盖模式关注的是“断言的约束是否有实际意义”，确保前提有机会触发，这样断言才能真正验证设计逻辑。

内容的提问来源于stack exchange，提问作者xormapmap