问题标签 [yosys]

不仅使用常规的综合前（行为）仿真验证 Verilog 设计，而且还使用综合后仿真来验证 Verilog 设计是一种很好的设计实践。在调试仿真和硬件之间的不匹配时，这实际上是强制性的。如何使用 iCE40 FPGA 的开源 IceStorm 流程来实现这一点？

我正在尝试将 Yosys 形式验证功能与 Verific 解析器一起使用。

与“read_verilog -formal”命令相比，带有 verific 的 yosys 支持哪些功能进行形式验证？例如，与 read_verilog 一起使用的正式代码的快速编译给了我一个“假设属性”语法错误：“sva 指令对时钟不敏感。不支持非时钟指令”

我不确定是否应该以任何方式修改 Verific 库标志以使其支持更多功能，或者它是不受支持的东西。

作为标题，另外你如何为单端输入/输出指定另一个电压电平，例如 LVCMOS18 - 我猜它不像 pcf 条目中的一个额外动词那么简单......

我在 Verilog 中有一个示例组合循环，我可以按照说明进行逻辑综合并生成 blif 文件。

但是，我需要的是从电路中生成 CNF 公式。ABC 等工具仅允许从组合斜接生成（即，具有 1 个输出）。

我尝试了 yosys 指令“sat -dump_cnf FILE”，确实可以生成 CNF 文件。但是，我不确定如何将 CNF 中的变量与电路中的 I/O 映射。

有没有人研究过 Yosys 的“sat -dump_cnf”功能并可以给我一个指针？

我正在尝试使用 Yosys 来实现连接的综合后操作。即，我想在合成过程完成后手动操作verilog模块之间的连接。

我试着研究了一段时间的代码，我发现我需要创建一个“Pass”结构的子类来实现我需要的确切功能。

我需要找出如何自己操纵连接。所以，我需要知道“设计”结构是否是包含用作工具输入的 Verilog 设计表示的结构。如果这是真的，我在哪里可以找到连接（哪些变量用于表示连接）？

此外，如果我需要自动化连接操作，我需要知道该工具如何为每个连接分配特定名称，以便我能够实现一种自动化算法，该算法可以自动选择要删除的特定连接或添加新连接，基于现有连接的名称。连接的名称是指 Yosys 显示的名称，以防 GraphViz 用于以图形方式呈现设计。

提前致谢。此致

我可以看到icestorm 支持ice40 ultra plus up5k fpga，但是这个芯片有内部osc，有什么我用的例子吗？当然使用yosys，icestorm（开源），有没有一些我可以使用内置IP的例子，比如SPI，I2C，PWM？谢谢

我找不到任何设置转换或驱动速率的 pcf 文件示例。我查看了列出 io 端口原语的技术文件，似乎可以设置驱动器，但不能设置 slew。

我正在尝试使用以下语法创建一个隐式 FSM：

它在模拟中工作正常，但是当我尝试合成时，显示错误：“语法意外@”

yosys不支持这个sintax吗？

谢谢

Yosys 是否有一个命令，它创建一个与 gcc 选项 -MMD 等效的依赖文件？（此选项输出一个小的 Makefile 片段，其中列出了编译单元包含的所有文件。请参阅在 makefile 中使用 g++ 和 -MMD 自动生成依赖项）

背景：我尝试构建一个 Makefile，它使用 Yosys 合成一个 verilog 项目。该项目使用单个顶级verilog 文件，其中包含其他verilog 依赖项。为此，我使用以下 make 规则，它非常有效：

由于我不想明确提及 Makefile 中的其他 verilog 文件，因此我想使用依赖文件。这将允许检测应用于任何依赖文件的更改并触发重新编译。

感谢 Clifford 添加的新 yosys -E 选项，我可以将上面的 Makefile 规则更改如下：

现在，只要隐式引用的 Verilog 文件之一发生更改，就会生成 blif 文件。

我正在尝试使用 miter 和 sat 来证明时序电路的等效性。本质上，两个电路的行为在它们被复位后应该是相同的。不过，我不知道如何告诉 yosys。我试过用-set in_reset 0 -set-at 0 in_reset 1. 这是一个示例电路（移位寄存器）和 yosys 脚本，说明了我正在尝试做的事情：

我的 Yosys 命令：

如果我添加-set-init-zero它可以工作，但这会破坏目的，因为我正在尝试测试重置行为。我也可以更改-seq 0为，-seq 8但这也违背了目的，因为我试图在电路重置后立即检查它们是否等效。

我如何告诉等效检查在检查之前重置电路？