tests/opt/opt_expr_and.ys

   1 # Single-bit $and
   2 read_verilog -noopt <<EOT
   3 module gold(input i, output o);
   4 assign o = 1'bx & i;
   5 endmodule
   6 EOT
   7 select -assert-count 1 t:$and
   8 copy gold coarse
   9 copy gold fine
  10 copy gold coarse_keepdc
  11 copy gold fine_keepdc
  12
  13 cd coarse
  14 opt_expr
  15 select -assert-none c:*
  16
  17 cd fine
  18 simplemap
  19 opt_expr
  20 select -assert-none c:*
  21
  22 cd
  23 miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
  24 sat -verify -prove-asserts -show-ports -enable_undef miter
  25 miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
  26 sat -verify -prove-asserts -show-ports -enable_undef miter2
  27
  28 cd coarse_keepdc
  29 opt_expr -keepdc
  30 select -assert-count 1 c:*
  31
  32 cd fine_keepdc
  33 simplemap
  34 opt_expr -keepdc
  35 select -assert-count 1 c:*
  36
  37 cd
  38 miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
  39 sat -verify -prove-asserts -show-ports -enable_undef miter3
  40 miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
  41 sat -verify -prove-asserts -show-ports -enable_undef miter4
  42
  43
  44 # Multi-bit $and
  45 design -reset
  46 read_verilog -noopt <<EOT
  47 module gold(input i, output [6:0] o);
  48 assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} & {7{i}};
  49 endmodule
  50 EOT
  51 select -assert-count 1 t:$and
  52 copy gold coarse
  53 copy gold fine
  54 copy gold coarse_keepdc
  55 copy gold fine_keepdc
  56
  57 cd coarse
  58 opt_expr -fine
  59 select -assert-none c:*
  60
  61 cd fine
  62 simplemap
  63 opt_expr
  64 select -assert-none c:*
  65
  66 cd
  67 miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
  68 sat -verify -prove-asserts -show-ports -enable_undef miter
  69 miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
  70 sat -verify -prove-asserts -show-ports -enable_undef miter2
  71
  72 cd coarse_keepdc
  73 opt_expr -fine -keepdc
  74 select -assert-count 1 c:*
  75
  76 cd fine_keepdc
  77 simplemap
  78 opt_expr -keepdc
  79 select -assert-count 2 c:*
  80
  81 cd
  82 miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
  83 sat -verify -prove-asserts -show-ports -enable_undef miter3
  84 miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
  85 sat -verify -prove-asserts -show-ports -enable_undef miter4