tests/sat/initval.ys

read_verilog -sv initval.v
proc;;

sat -seq 10 -prove-asserts

read_verilog <<EOT
module gold(input clk, input i, output reg [1:0] o);
initial o = 2'b10;
always @(posedge clk)
   o[0] <= {i,i};
endmodule

module gate(input clk, input i, output reg [1:0] o);
initial o = 2'b10;
always @(posedge clk)
   o[0] <= i;
always @*
   o[1] <= o[0];
endmodule
EOT

proc
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -seq 1 -falsify -prove-asserts -show-ports miter