我正在尝试将 Yosys 形式验证功能与 Verific 解析器一起使用。
与“read_verilog -formal”命令相比，带有 verific 的 yosys 支持哪些功能进行形式验证？例如，与 read_verilog 一起使用的正式代码的快速编译给了我一个“假设属性”语法错误：“sva 指令对时钟不敏感。不支持非时钟指令”
我不确定是否应该以任何方式修改 Verific 库标志以使其支持更多功能，或者它是不受支持的东西。
问问题
993 次
1 回答
5
目前，无论有没有 Verific，Yosys 对 SVA 的支持都非常有限。但是，我们计划在不久的将来通过 Verific 大幅扩展 Yosys 对 SVA 的支持。目标是为 Verific 可以解析的所有内容提供几乎完整的支持。
关于“sva 指令对时钟不敏感。不支持非时钟指令”错误消息：这是一条 Verific 错误消息，我认为没有 Verific 库标志可以绕过它。（但我不确定。）技术上非时钟属性不是 SystemVerilog 标准 afaik 的一部分。（语法允许，但标准文本没有为它定义语义。）
Yosys 支持非时钟 SVA 属性。（但只是简单的表达式属性。）
Verific 和 Yosys 都支持即时断言和假设。（即总是块中的断言和假设。）现在，对于大多数人们编写新属性的情况，这是我推荐的东西，也是因为大多数模拟器对立即断言有更好的支持（或者如果支持是，它会更容易添加）失踪至今）。
现在我想说，将 Verific 与 Yosys 一起使用的最大优势是支持非 SVA System Verilog（和 VHDL）代码。几个月后，我们希望通过 Verific 支持更多的 SVA 构造，但这还没有实现。
编辑/更新：通过 Verific 的 SVA 支持现在正在缓慢改进。有关可以通过 Verific 处理的示例，请参见此目录。随着新特性被添加到 Verific 绑定中，新示例被添加。目前counter.sv是那里最先进的例子。
于 2017-07-21T17:03:38.733 回答