0

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

module shift_reg(
  input clock,
  input reset,
  input in,
  output out
);
  reg [7:0] r;

  assign out = r[7];

  always @(posedge clock) begin
    if (reset)
      r <= 0;
    else
      r <= {r[6:0], in};
  end
endmodule

我的 Yosys 命令：

read_verilog shift_reg.v
rename shift_reg shift_reg_2
read_verilog shift_reg.v
prep; proc; opt; memory
miter -equiv -flatten shift_reg shift_reg_2 miter
hierarchy -top miter
sat -verify -tempinduct -prove trigger 0 -set in_reset 0 -set-at 0 in_reset 1 -seq 0 miter

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

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

4

1 回答 1

1

只需使用以下 SAT 命令：

sat -verify -tempinduct -prove trigger 0 \
    -set in_reset 0 -set-at 1 in_reset 1 -seq 1 miter

与您的脚本相比的更改：

  1. “sat”命令从 1 开始编号步骤。因此 -set-at 选项需要 1 作为第一个参数，以便在第一个循环中重置。

  2. “-seq 1”将禁用第一个周期中的属性检查。这是有道理的，因为复位只会在第 2 个周期生效，因此这两个模块可能确实在第 1 个周期产生不同的输出。

于 2018-01-07T15:23:52.520 回答