tests/various/signext.ys

   1
   2 read_verilog -formal <<EOT
   3 module gate(input clk, output [32:0] o, p, q, r, s, t, u);
   4 assign o = 'bx;
   5 assign p = 1'bx;
   6 assign q = 'bz;
   7 assign r = 1'bz;
   8 assign s = 1'b0;
   9 assign t = 'b1;
  10 assign u = -'sb1;
  11 endmodule
  12 EOT
  13
  14 proc
  15
  16 ## Equivalence checking
  17
  18 read_verilog -formal <<EOT
  19 module gold(input clk, output [32:0] o, p, q, r, s, t, u);
  20 assign o = {33{1'bx}};
  21 assign p = {{32{1'b0}}, 1'bx};
  22 assign q = {33{1'bz}};
  23 assign r = {{32{1'b0}}, 1'bz};
  24 assign s = {33{1'b0}};
  25 assign t = {{32{1'b0}}, 1'b1};
  26 assign u = {33{1'b1}};
  27 endmodule
  28 EOT
  29
  30 proc
  31
  32 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  33 sat -verify -prove-asserts -show-ports -enable_undef miter