I'm trying to prove equivalence using miter and sat for a sequential circuit. Essentially, the behavior of the two circuits should be identical as soon as they are reset. I cannot figure out how to tell yosys this though. I have tried reseting the designs with -set in_reset 0 -set-at 0 in_reset 1. Here is an example circuit (a shift register) and yosys script that illustrate what I'm trying to do:
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
My Yosys commands:
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
If I add -set-init-zero it works, but that defeats the purpose because I'm trying to test reset behavior. I can also change -seq 0 to -seq 8 but that also defeats the purpose because I'm trying to check that the circuits are equivalent as soon as they are reset.
How do I tell equivalence checking to reset the circuits before checking?
Simply use the following SAT command:
sat -verify -tempinduct -prove trigger 0 \
-set in_reset 0 -set-at 1 in_reset 1 -seq 1 miter
Changes compared to your script:
The "sat" command numbers steps starting with 1. So the -set-at option needs 1 as first argument for resetting in the first cycle.
The "-seq 1" will disable checking of properties in the first cycle. This make sense because the reset will only have taken effect in the 2nd cycle, so the two modules might indeed produce different outputs in cycle 1.