tests/various/bug1531.ys

   1 read_verilog <<EOT
   2 module top (y, clk, w);
   3    output reg y = 1'b0;
   4    input clk, w;
   5    reg [1:0] i = 2'b00;
   6    always @(posedge clk)
   7      // If the constant below is set to 2'b00, the correct output is generated.
   8      //       vvvv
   9      for (i = 1'b0; i < 2'b01; i = i + 2'b01)
  10        y <= w || i[1:1];
  11 endmodule
  12 EOT
  13
  14 synth
  15 design -stash gate
  16
  17 read_verilog <<EOT
  18 module gold (y, clk, w);
  19   input clk;
  20   wire [1:0] i;
  21   input w;
  22   output y;
  23   reg y = 1'h0;
  24   always @(posedge clk)
  25       y <= w;
  26   assign i = 2'h0;
  27 endmodule
  28 EOT
  29 proc gold
  30
  31 design -import gate -as gate
  32
  33 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  34 sat -seq 10 -verify -prove-asserts -show-ports miter