时间戳

首页 > 解决方案 > 使用 yosys-smtbmc 证明时是否可以使用 $display 打印一些值？

verilog - 使用 yosys-smtbmc 证明时是否可以使用 $display 打印一些值？

问题描述

在 verilog 中，$display() 函数在模拟中很有用，可以查看常量或宏的值，如下例所示：

/* Display parameters in simulation */
initial
begin
    $display("CLK_PER_NS     : %d", CLK_PER_NS );
    $display("PULSE_PER_NS   : %d", PULSE_PER_NS);
    $display("MAX_COUNT      : %x", `MAX_COUNT);
    $display("MAX_COUNT_SIZE : %x", `MAX_COUNT_SIZE);
end

但是当我启动带有封面、bmc 或证明的 yosys-smtbmc 时，控制台中没有显示任何内容。

有可能吗？

我的 sby 脚本（示例来自我的 github 项目）：

[options]
#mode cover
mode bmc
#mode prove
depth 150

[engines]
smtbmc

[script]
read -formal per2bpm.v
prep -top per2bpm

[files]
../../hdl/per2bpm.v

标签： verilogyosys

解决方案

不，目前不支持此功能。通常，使用 Yosys 的形式验证为您提供了与综合类似的功能集（它呈现给求解器的本质上是一个电路），并添加了断言/假设/覆盖等。使用读取求解器输出的东西可以添加显示，但要正确实施，这也是一项相当重要的工作。

推荐阅读