我正在尝试将 Yosys 形式验证功能与 Verific 解析器一起使用。
与“read_verilog -formal”命令相比，yosys with verific 对于形式验证支持哪些功能？例如，使用 read_verilog 快速编译正式代码时，出现“假设属性”语法错误：“sva 指令对时钟不敏感。不支持非时钟指令”
我不确定是否应该以任何方式修改 Verific 库标志以使其支持更多功能，或者它不受支持。
目前，Yosys 对带或不带 Verific 的 SVA 的支持非常有限。不过，我们计划在不久的将来通过 Verific 大幅扩展 Yosys 对 SVA 的支持。目标是为 Verific 可以解析的所有内容提供几乎完整的支持。
关于“sva 指令对时钟不敏感。不支持非时钟指令”错误消息：这是一条 Verific 错误消息，我认为没有 Verific 库标志可以绕过它。（但我不确定。）从技术上讲，非时钟属性并不是 SystemVerilog 标准的一部分。（语法允许这样做，但标准文本没有为其定义语义。）
Yosys 支持非时钟 SVA 属性。（但只是简单的表达式属性。）
Verific 和 Yosys 都支持直接断言和假设。（这是always块中的断言和假设。）现在，对于人们编写新属性的大多数情况，我建议这样做，也是因为大多数模拟器对立即断言有更好的支持（或者如果支持的话添加会更容易）至今失踪）。
现在我想说，将 Verific 与 Yosys 结合使用的最大优势是支持非 SVA 系统 Verilog（和 VHDL）代码。几个月后，我们有望通过 Verific 支持更多 SVA 构造，但这尚未实现。
编辑/更新：通过 Verific 的 SVA 支持现在正在缓慢改进。请参阅此目录以获取可以通过 Verific 处理的示例。随着新功能添加到 Verific 绑定，也会添加新示例。目前counter.sv是最先进的示例。
| 归档时间： |
|
| 查看次数： |
1344 次 |
| 最近记录： |