基于人字等值检查的复位行为

Question

我正试着用弥勒来证明等价性，然后坐在一个时序电路上。本质上，这两个电路的行为应该是相同的，一旦它们被重置。但我想不出该怎么告诉你。我试过用-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

我的约西斯的命令：

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

与脚本相比较的更改：

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