代码之家 › 专栏 › 技术社区 › EEliaz

yosys与verific的正式功能是什么?

yosys

4

EEliaz · 技术社区 · 7 年前

与“read\u verilog-formula”命令相比,yosys with verific的形式验证支持哪些功能? “sva指令对时钟不敏感。不支持未锁定指令”

1 回复 | 直到 7 年前

1

5

CliffordVienna 7 年前

目前,Yosys对SVA的支持非常有限,无论是否有Verific。然而,我们计划在不久的将来通过Verific极大地扩展Yosys对SVA的支持。目标是为Verific可以解析的所有内容提供几乎完整的支持。

关于“sva指令对时钟不敏感。不支持未锁定的指令”错误消息:这是一条Verific错误消息,我认为没有Verific库标志可以绕过它。(但我不确定)从技术上讲,未锁定的属性不是SystemVerilog标准afaik的一部分。(语法允许,但标准文本没有为其定义语义。)

Yosys支持未锁定的SVA属性。(但只有微不足道的表达式属性。)

Verific和Yosys都支持即时断言和假设。(这是always块中的断言和假设。)现在,我建议在大多数情况下使用这种方法,因为大多数模拟器都更好地支持即时断言(或者,如果到目前为止还没有支持,那么添加起来会更容易)。

编辑/更新: 通过Verific的SVA支持现在进展缓慢。看见 this directory 例如,可以通过Verific进行处理。随着新特性添加到Verific绑定中,添加了新的示例。目前 counter.sv 是最先进的例子。