tests/verilog/const_arst.ys

   1 read_verilog <<EOT
   2 module test (
   3         input clk, d,
   4         output reg q
   5 );
   6 wire nop = 1'h0;
   7 always @(posedge clk, posedge nop) begin
   8         if (nop) q <= 1'b0;
   9         else q <= d;
  10 end
  11 endmodule
  12 EOT
  13 prep -top test
  14 write_verilog const_arst.v
  15 design -stash gold
  16 read_verilog const_arst.v
  17 prep -top test
  18 design -stash gate
  19 design -copy-from gold -as gold A:top
  20 design -copy-from gate -as gate A:top
  21 miter -equiv -flatten -make_assert gold gate miter
  22 prep -top miter
  23 clk2fflogic
  24 sat -set-init-zero -tempinduct -prove-asserts -verify