02_symbiyosys快速入门

卑微大学社畜生

395人浏览 · 2026-03-24 21:12:13

卑微大学社畜生 · 2026-03-24 21:12:13 发布

symbiyosys快速入门

原文来源：Getting started - YosysHQ SBY documentation

注意：本教程假设已按照安装指南完成 sby 和 boolector 的安装。同时建议安装 GTKWave（一款开源 VCD 查看器）。教程所用源文件可在 sby git 仓库中的 docs/examples/fifo 目录下找到。

本文档来自于官方英文教程，本文只做翻译处理

先进先出（FIFO）缓冲区

根据维基百科，FIFO 是：

一种数据结构（通常是数据缓冲区）的操作方式，最早（第一个）入队的条目——即队列的"头部"——最先被处理。
这类似于按先来先服务（FCFS）方式服务排队人群，即按照到达队尾的顺序进行服务。

在硬件中，可通过向寄存器文件提供两个地址来实现这种结构。本教程将使用 fifo.sv 中提供的示例实现。

首先是地址生成器模块：

// address generator/counter
module addr_gen
#( parameter MAX_DATA=16
) ( input en, clk, rst,
    output reg [3:0] addr
);
    initial addr <= 0;

    // async reset
    // increment address when enabled
    always @(posedge clk or posedge rst)
    if (rst)
        addr <= 0;
    else if (en) begin
        if (addr == MAX_DATA-1)
            addr <= 0;
        else
            addr <= addr + 1;
    end
endmodule

该模块被实例化两次：一次用于写地址，一次用于读地址。两种情况下，地址都从 0 开始，接收到使能信号后递增 1。当地址指针从最大存储值递增时，会回绕到 0，从而构成一个循环队列。

接下来是寄存器文件：

// fifo storage
// async read, sync write
wire [3:0] waddr, raddr;
reg [7:0] data [MAX_DATA-1:0];
always @(posedge clk)
    if (wen)
        data[waddr] <= wdata;
assign rdata = data[raddr];

注意该寄存器设计采用同步写、异步读。每个字为 8 位，缓冲区最多可存储 16 个字。

验证属性

为了验证设计，首先需要定义其必须满足的属性。例如，缓冲区中的值数量绝不能超过可用内存。通过分配一个信号来计数缓冲区中的值，可以在代码中添加如下断言：

a_oflow: assert (count <= MAX_DATA);

也可以使用信号的先前值进行比较。例如，可以确保计数只能增加或减少 1。需要额外处理直接复位到 0 以及计数不变的情况。以下代码展示了这一点：若设计正确，以下条件中至少有一个必须始终为真。

a_counts: assert (count == 0
    || count == $past(count)
    || count == $past(count) + 1
    || count == $past(count) - 1);

由于计数信号独立于读写指针，必须验证计数始终正确。写指针始终在读指针处或之后，但循环缓冲区意味着写地址可能回绕，看起来比读地址小。因此需要先进行简单的算术运算来求地址的绝对差值，再与计数信号比较。

assign addr_diff = waddr >= raddr
    ? waddr - raddr
    : waddr + MAX_DATA - raddr;

a_count_diff: assert (count == addr_diff
    || count == MAX_DATA && addr_diff == 0);

SymbiYosys

SymbiYosys（sby）使用 .sby 文件定义一组验证任务：

basic：对设计进行有界模型检查
nofullskip：使用无界模型检查演示失败模型
cover：覆盖模式（测试 cover 语句）
noverific：测试回退到默认 Verilog 前端

:default 标签表示若未指定任务（例如运行下面的命令时），默认运行 basic 和 cover：

sby fifo.sby

注意：默认测试集应全部通过。若未通过，则可能是 sby 或其某个求解器的安装存在问题。

若要查看测试失败时的情况，可使用以下命令。注意 -f 标志用于自动覆盖已有的任务输出。虽然第一次运行时可能不需要，但在修改代码后重新运行测试时非常有用。

sby -f fifo.sby nofullskip

nofullskip 任务会禁用下面展示的代码。由于 count 信号被设计为不能超过 MAX_DATA，移除这段代码将导致 a_count_diff 断言失败。没有这个断言，就无法保证在发生溢出且最旧数据被覆盖的情况下，数据仍能按写入顺序读出。

`ifndef NO_FULL_SKIP
    // write while full => overwrite oldest data, move read pointer
    assign rskip = wen && !ren && data_count >= MAX_DATA;
    // read while empty => read invalid data, keep write pointer in sync
    assign wskip = ren && !wen && data_count == 0;
`endif // NO_FULL_SKIP

nofullskip 任务最后几行输出应类似如下：

SBY [fifo_nofullskip] engine_0.basecase: ## Assert failed in fifo: a_count_diff
SBY [fifo_nofullskip] engine_0.basecase: ## Writing trace to VCD file: engine_0/trace.vcd
SBY [fifo_nofullskip] engine_0.basecase: ## Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY [fifo_nofullskip] engine_0.basecase: ## Writing trace to constraints file: engine_0/trace.smtc
SBY [fifo_nofullskip] engine_0.basecase: ## Status: failed
SBY [fifo_nofullskip] engine_0.basecase: finished (returncode=1)
SBY [fifo_nofullskip] engine_0: Status returned by engine for basecase: FAIL
SBY [fifo_nofullskip] engine_0.induction: terminating process
SBY [fifo_nofullskip] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:02 (2)
SBY [fifo_nofullskip] summary: Elapsed process time unvailable on Windows
SBY [fifo_nofullskip] summary: engine_0 (smtbmc boolector) returned FAIL for basecase
SBY [fifo_nofullskip] summary: counterexample trace: fifo_nofullskip/engine_0/trace.vcd
SBY [fifo_nofullskip] DONE (FAIL, rc=2)
SBY The following tasks failed: ['nofullskip']

使用提供的 noskip.gtkw 文件，通过以下命令查看错误轨迹：

gtkwave fifo_nofullskip/engine_0/trace.vcd noskip.gtkw

可以立即看到 data_count 和 addr_diff 不同。进一步分析可发现，要到达此状态，第一个时钟周期读使能信号为高而写使能为低，这导致了下溢——在缓冲区为空时读取一个值，使读地址递增到高于写地址。

在正确操作时，w_underfill cover 语句会覆盖下溢情况。检查 fifo_cover/logfile.txt 可找到包含所需 cover 语句的轨迹文件。如果该文件不存在，运行：

sby fifo.sby cover

在文件中搜索 w_underfill 会发现：

$ grep "w_underfill" fifo_cover/logfile.txt -A 1
SBY [fifo_cover] engine_0: ## Reached cover statement at w_underfill in step 2.
SBY [fifo_cover] engine_0: ## Writing trace to VCD file: engine_0/trace4.vcd

然后使用指定的轨迹文件运行 gtkwave 查看正确操作：

gtkwave fifo_cover/engine_0/trace4.vcd noskip.gtkw

当缓冲区为空时，无写操作的读将导致 wskip 信号拉高，同时递增读写地址，避免下溢。

注意：w_underfill cover 语句的实现取决于是否使用 Verific。详见后面的"并发断言"节。

练习

将 fifo.sby 的 [script] 段修改为如下内容：

[script]
nofullskip: read -define NO_FULL_SKIP=1
noverific: read -noverific
read -formal fifo.sv
hierarchy -check -top fifo -chparam MAX_DATA 17
prep -top fifo

添加的 hierarchy 命令将顶层模块的 MAX_DATA 参数改为 17。现在运行 basic 任务，会看到类似 Assert failed in fifo: a_count_diff 的错误。你能修改 Verilog 代码使其在更大的 MAX_DATA 值下也能通过所有测试吗？

提示：尝试增加地址线的位宽。4 位最多支持 2⁴=16 个地址。其他信号是否也需要加宽？能否将位宽参数化以支持任意大小的缓冲区？

在 MAX_DATA=17 下测试通过后，尝试更大的值，如 64 或 100。basic 任务还能通过吗？cover 呢？默认情况下，bmc 和 cover 模式运行深度为 20 个时钟周期。如果每个周期最多加载一个值，加载 100 个值需要多少周期？参考 .sby 参考文档，尝试将 cover 模式深度增加到至少比 MAX_DATA 大几个周期。

注意：参考文件位于 fifo/golden 目录，展示了如何修改 Verilog 代码以及如何添加 bigtest 任务。

并发断言

到目前为止描述的所有属性都是即时断言。顾名思义，即时断言会立即求值，而并发断言则允许捕获跨时钟周期发生的事件序列，需要更高级的验证手段。

比较 w_underfill 在有无 Verific 时的实现差异。w_underfill 查找写使能为低但写地址在下一周期发生变化的事件序列，这是空读（读空缓冲区）时的预期行为，意味着 wskip 信号拉高。Verific 支持 SystemVerilog 断言（SVA）属性的细化。此处使用了这样一个属性 write_skip：

property write_skip;
    @(posedge clk) disable iff (rst)
    !wen |=> $changed(waddr);
endproperty
w_underfill: cover property (write_skip);

该属性描述了在 clk 信号上发生的、当 rst 信号为高时禁用/重启的事件序列。属性首先等待 wen 为低，然后在下一周期等待 waddr 发生变化。w_underfill 是对该属性的覆盖，用于验证其可达性。

下面是不使用 Verific 的实现：

reg past_nwen;
initial past_nwen <= 0;
always @(posedge clk) begin
    if (rst) past_nwen <= 0;
    if (!rst) begin
        w_underfill: cover (past_nwen && $changed(waddr));
        past_nwen <= !wen;
    end
end

在这种情况下，我们无法使用 SVA 属性，可用工具受到更多限制。理想情况下，我们会使用 $past 读取上一周期 wen 的值，然后检查 waddr 是否变化。然而，在仿真第一个周期中，读取 $past 将返回 X，导致属性误触发。因此改为实现寄存器 past_nwen，将其初始化为 0，确保第一个周期不会触发。

随着验证属性变得更复杂、需要检查更长的序列，不使用 SVA 属性手动编码的额外工作量将变得非常困难。使用 Verific 这样的解析器可以支持这些检查，而无需编写可能很复杂的状态机。Verific 包含在 Tabby CAD Suite 中。