tests/various/signext.ys

   1
   2 read_verilog -formal <<EOT
   3 module gate(input clk, output [1:0] o);
   4 assign o = 1'bx;
   5 endmodule
   6 EOT
   7
   8 proc
   9
  10 ## Equivalence checking
  11
  12 read_verilog -formal <<EOT
  13 module gold(input clk, output [1:0] o);
  14 assign o = 2'bxx;
  15 endmodule
  16 EOT
  17
  18 proc
  19
  20 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  21 sat -verify -prove-asserts -show-ports -enable_undef miter