tests/sat/initval.ys

   1 read_verilog -sv initval.v
   2 proc;;
   3
   4 sat -seq 10 -prove-asserts
   5
   6 design -reset
   7 read_verilog -icells <<EOT
   8 module top(input clk, i, output [1:0] o);
   9 (* init = 2'bx0 *)
  10 wire [1:0] o;
  11 assign o[1] = o[0];
  12 $_DFF_P_ dff (.C(clk), .D(i), .Q(o[0]));
  13 endmodule
  14 EOT
  15 sat -seq 1