通过斜接等效检查重置行为

Question

我正在尝试使用 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 但这也达不到目的，因为我试图检查电路在重置后是否等效。

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

Answer 1

只需使用以下 SAT 命令：

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

与您的脚本相比的变化：

"sat" 命令编号从 1 开始的步骤。因此 -set-at 选项需要 1 作为第一个参数以在第一个循环中重置。
“-seq 1”将在第一个循环中禁用属性检查。这是有道理的，因为重置只会在第 2 个周期生效，因此两个模块确实可能在第 1 个周期产生不同的输出。

通过斜接等效检查重置行为

Reset behavior with miter equivalence checking

yosys